mathlib3 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 b quot.mk r a = quot.mk r b
@[protected]
theorem quot.lift_beta {α : Sort u} {r : α α Prop} {β : Sort v} (f : α β) (c : (a b : α), r a b f 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 b f 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 r Sort v} (f : Π (a : α), β (quot.mk r a)) (a : α) :
Equations
@[protected]
theorem quot.indep_coherent {α : Sort u} {r : α α Prop} {β : quot r Sort v} (f : Π (a : α), β (quot.mk r a)) (h : (a b : α) (p : r a b), eq.rec (f a) _ = f b) (a b : α) :
r a b quot.indep f a = quot.indep f b
@[protected]
theorem quot.lift_indep_pr1 {α : Sort u} {r : α α Prop} {β : quot r Sort 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 r Sort 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 r Sort 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 r Sort 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 r Sort v} (q : quot r) (f : Π (a : α), β (quot.mk r a)) (c : (a b : α), r a b f a == f b) :
β q
Equations
@[protected]
def quotient.mk {α : Sort u} [s : setoid α] (a : α) :
Equations
theorem quotient.sound {α : Sort u} [s : setoid α] {a b : α} :
@[protected, reducible]
def quotient.lift {α : Sort u} {β : Sort v} [s : setoid α] (f : α β) :
( (a b : α), a b f 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 b f 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 s Sort 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 s Sort 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 s Sort v} [h : (a : α), subsingleton a)] (q : quotient s) (f : Π (a : α), β a) :
β q
Equations
@[protected, reducible]
def quotient.hrec_on {α : Sort u} [s : setoid α] {β : quotient s Sort v} (q : quotient s) (f : Π (a : α), β a) (c : (a b : α), a b f 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 : α} :
@[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
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