mathlib documentation

core / init.data.quot

theorem iff_subst {a b : Prop} {p : Prop → Prop} (h₁ : a b) (h₂ : p a) :
p b
constant quot.sound {α : Sort u} {r : α → α → Prop} {a b : α} :
r a bquot.mk r a = quot.mk r b
@[protected]
theorem quot.lift_beta {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (c : ∀ (a b : α), r a bf a = f b) (a : α) :
quot.lift f c (quot.mk r a) = f a
@[protected]
theorem quot.ind_beta {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} (p : ∀ (a : α), β (quot.mk r a)) (a : α) :
_ = _
@[protected, reducible]
def quot.lift_on {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : quot r) (f : α → β) (c : ∀ (a b : α), r a bf a = f b) :
β
Equations
@[protected]
theorem quot.induction_on {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} (q : quot r) (h : ∀ (a : α), β (quot.mk r a)) :
β q
theorem quot.exists_rep {α : Sort u} {r : α → α → Prop} (q : quot r) :
∃ (a : α), quot.mk r a = q
@[protected, reducible]
def quot.indep {α : Sort u} {r : α → α → Prop} {β : quot rSort v} (f : Π (a : α), β (quot.mk r a)) (a : α) :
Equations
@[protected]
theorem quot.indep_coherent {α : Sort u} {r : α → α → Prop} {β : quot rSort v} (f : Π (a : α), β (quot.mk r a)) (h : ∀ (a b : α) (p : r a b), eq.rec (f a) _ = f b) (a b : α) :
r a bquot.indep f a = quot.indep f b
@[protected]
theorem quot.lift_indep_pr1 {α : Sort u} {r : α → α → Prop} {β : quot rSort v} (f : Π (a : α), β (quot.mk r a)) (h : ∀ (a b : α) (p : r a b), eq.rec (f a) _ = f b) (q : quot r) :
(quot.lift (quot.indep f) _ q).fst = q
@[protected, reducible]
def quot.rec {α : Sort u} {r : α → α → Prop} {β : quot rSort v} (f : Π (a : α), β (quot.mk r a)) (h : ∀ (a b : α) (p : r a b), eq.rec (f a) _ = f b) (q : quot r) :
β q
Equations
@[protected, reducible]
def quot.rec_on {α : Sort u} {r : α → α → Prop} {β : quot rSort v} (q : quot r) (f : Π (a : α), β (quot.mk r a)) (h : ∀ (a b : α) (p : r a b), eq.rec (f a) _ = f b) :
β q
Equations
@[protected, reducible]
def quot.rec_on_subsingleton {α : Sort u} {r : α → α → Prop} {β : quot rSort v} [h : ∀ (a : α), subsingleton (quot.mk r a))] (q : quot r) (f : Π (a : α), β (quot.mk r a)) :
β q
Equations
@[protected, reducible]
def quot.hrec_on {α : Sort u} {r : α → α → Prop} {β : quot rSort v} (q : quot r) (f : Π (a : α), β (quot.mk r a)) (c : ∀ (a b : α), r a bf a == f b) :
β q
Equations
@[protected]
def quotient.mk {α : Sort u} [s : setoid α] (a : α) :
Equations
theorem quotient.sound {α : Sort u} [s : setoid α] {a b : α} :
a ba = b
@[protected, reducible]
def quotient.lift {α : Sort u} {β : Sort v} [s : setoid α] (f : α → β) :
(∀ (a b : α), a bf a = f b)quotient s → β
Equations
@[protected]
theorem quotient.ind {α : Sort u} [s : setoid α] {β : quotient s → Prop} :
(∀ (a : α), β a)∀ (q : quotient s), β q
@[protected, reducible]
def quotient.lift_on {α : Sort u} {β : Sort v} [s : setoid α] (q : quotient s) (f : α → β) (c : ∀ (a b : α), a bf a = f b) :
β
Equations
@[protected]
theorem quotient.induction_on {α : Sort u} [s : setoid α] {β : quotient s → Prop} (q : quotient s) (h : ∀ (a : α), β a) :
β q
theorem quotient.exists_rep {α : Sort u} [s : setoid α] (q : quotient s) :
∃ (a : α), a = q
@[protected]
def quotient.rec {α : Sort u} [s : setoid α] {β : quotient sSort v} (f : Π (a : α), β a) (h : ∀ (a b : α) (p : a b), eq.rec (f a) _ = f b) (q : quotient s) :
β q
Equations
@[protected, reducible]
def quotient.rec_on {α : Sort u} [s : setoid α] {β : quotient sSort v} (q : quotient s) (f : Π (a : α), β a) (h : ∀ (a b : α) (p : a b), eq.rec (f a) _ = f b) :
β q
Equations
@[protected, reducible]
def quotient.rec_on_subsingleton {α : Sort u} [s : setoid α] {β : quotient sSort v} [h : ∀ (a : α), subsingleton a)] (q : quotient s) (f : Π (a : α), β a) :
β q
Equations
@[protected, reducible]
def quotient.hrec_on {α : Sort u} [s : setoid α] {β : quotient sSort v} (q : quotient s) (f : Π (a : α), β a) (c : ∀ (a b : α), a bf a == f b) :
β q
Equations
@[protected, reducible]
def quotient.lift₂ {α : Sort u_a} {β : Sort u_b} {φ : Sort u_c} [s₁ : setoid α] [s₂ : setoid β] (f : α → β → φ) (c : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ b₁a₂ b₂f a₁ a₂ = f b₁ b₂) (q₁ : quotient s₁) (q₂ : quotient s₂) :
φ
Equations
@[protected, reducible]
def quotient.lift_on₂ {α : Sort u_a} {β : Sort u_b} {φ : Sort u_c} [s₁ : setoid α] [s₂ : setoid β] (q₁ : quotient s₁) (q₂ : quotient s₂) (f : α → β → φ) (c : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ b₁a₂ b₂f a₁ a₂ = f b₁ b₂) :
φ
Equations
@[protected]
theorem quotient.ind₂ {α : Sort u_a} {β : Sort u_b} [s₁ : setoid α] [s₂ : setoid β] {φ : quotient s₁quotient s₂ → Prop} (h : ∀ (a : α) (b : β), φ a b) (q₁ : quotient s₁) (q₂ : quotient s₂) :
φ q₁ q₂
@[protected]
theorem quotient.induction_on₂ {α : Sort u_a} {β : Sort u_b} [s₁ : setoid α] [s₂ : setoid β] {φ : quotient s₁quotient s₂ → Prop} (q₁ : quotient s₁) (q₂ : quotient s₂) (h : ∀ (a : α) (b : β), φ a b) :
φ q₁ q₂
@[protected]
theorem quotient.induction_on₃ {α : Sort u_a} {β : Sort u_b} {φ : Sort u_c} [s₁ : setoid α] [s₂ : setoid β] [s₃ : setoid φ] {δ : quotient s₁quotient s₂quotient s₃ → Prop} (q₁ : quotient s₁) (q₂ : quotient s₂) (q₃ : quotient s₃) (h : ∀ (a : α) (b : β) (c : φ), δ a b c) :
δ q₁ q₂ q₃
theorem quotient.exact {α : Sort u} [s : setoid α] {a b : α} :
a = ba b
@[protected, reducible]
def quotient.rec_on_subsingleton₂ {α : Sort u_a} {β : Sort u_b} [s₁ : setoid α] [s₂ : setoid β] {φ : quotient s₁quotient s₂Sort u_c} [h : ∀ (a : α) (b : β), subsingleton a b)] (q₁ : quotient s₁) (q₂ : quotient s₂) (f : Π (a : α) (b : β), φ a b) :
φ q₁ q₂
Equations
inductive eqv_gen {α : Type u} (r : α → α → Prop) :
α → α → Prop
  • rel : ∀ {α : Type u} {r : α → α → Prop} (x y : α), r x yeqv_gen r x y
  • refl : ∀ {α : Type u} {r : α → α → Prop} (x : α), eqv_gen r x x
  • symm : ∀ {α : Type u} {r : α → α → Prop} (x y : α), eqv_gen r x yeqv_gen r y x
  • trans : ∀ {α : Type u} {r : α → α → Prop} (x y z : α), eqv_gen r x yeqv_gen r y zeqv_gen r x z
theorem eqv_gen.is_equivalence {α : Type u} (r : α → α → Prop) :
def eqv_gen.setoid {α : Type u} (r : α → α → Prop) :
Equations
theorem quot.exact {α : Type u} (r : α → α → Prop) {a b : α} (H : quot.mk r a = quot.mk r b) :
eqv_gen r a b
theorem quot.eqv_gen_sound {α : Type u} {r : α → α → Prop} {a b : α} (H : eqv_gen r a b) :
quot.mk r a = quot.mk r b
@[protected, instance]
def quotient.decidable_eq {α : Sort u} {s : setoid α} [d : Π (a b : α), decidable (a b)] :
Equations