mathlib documentation

core.init.data.quot

theorem iff_subst {a b : Prop} {p : Prop → Prop} :
(a b)p ap b

constant quot.sound {α : Sort u} {r : α → α → Prop} {a b : α} :
r a bquot.mk r a = quot.mk r b

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

theorem quot.ind_beta {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} (p : ∀ (a : α), β (quot.mk r a)) (a : α) :
_ = _

def quot.lift_on {α : Sort u} {β : Sort v} {r : α → α → Prop} (q : quot r) (f : α → β) :
(∀ (a b : α), r a bf a = f b) → β

Equations
theorem quot.induction_on {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} (q : quot r) :
(∀ (a : α), β (quot.mk r a))β q

theorem quot.exists_rep {α : Sort u} {r : α → α → Prop} (q : quot r) :
∃ (a : α), quot.mk r a = q

def quot.indep {α : Sort u} {r : α → α → Prop} {β : quot rSort v} :
(Π (a : α), β (quot.mk r a))α → psigma β

Equations
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

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

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
def quot.rec_on {α : Sort u} {r : α → α → Prop} {β : quot rSort v} (q : quot r) (f : Π (a : α), β (quot.mk r a)) :
(∀ (a b : α) (p : r a b), eq.rec (f a) _ = f b)β q

Equations
def quot.rec_on_subsingleton {α : Sort u} {r : α → α → Prop} {β : quot rSort v} [h : ∀ (a : α), subsingleton (quot.mk r a))] (q : quot r) :
(Π (a : α), β (quot.mk r a))β q

Equations
def quot.hrec_on {α : Sort u} {r : α → α → Prop} {β : quot rSort v} (q : quot r) (f : Π (a : α), β (quot.mk r a)) :
(∀ (a b : α), r a bf a == f b)β q

Equations
def quotient {α : Sort u} :
setoid αSort u

Equations
def quotient.mk {α : Sort u} [s : setoid α] :
α → quotient s

Equations
def quotient.sound {α : Sort u} [s : setoid α] {a b : α} :
a ba = b

def quotient.lift {α : Sort u} {β : Sort v} [s : setoid α] (f : α → β) :
(∀ (a b : α), a bf a = f b)quotient s → β

Equations
theorem quotient.ind {α : Sort u} [s : setoid α] {β : quotient s → Prop} (a : ∀ (a : α), β a) (q : quotient s) :
β q

def quotient.lift_on {α : Sort u} {β : Sort v} [s : setoid α] (q : quotient s) (f : α → β) :
(∀ (a b : α), a bf a = f b) → β

Equations
theorem quotient.induction_on {α : Sort u} [s : setoid α] {β : quotient s → Prop} (q : quotient s) :
(∀ (a : α), β a)β q

theorem quotient.exists_rep {α : Sort u} [s : setoid α] (q : quotient s) :
∃ (a : α), a = q

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
def quotient.rec_on {α : Sort u} [s : setoid α] {β : quotient sSort v} (q : quotient s) (f : Π (a : α), β a) :
(∀ (a b : α) (p : a b), eq.rec (f a) _ = f b)β q

Equations
def quotient.rec_on_subsingleton {α : Sort u} [s : setoid α] {β : quotient sSort v} [h : ∀ (a : α), subsingleton a)] (q : quotient s) :
(Π (a : α), β a)β q

Equations
def quotient.hrec_on {α : Sort u} [s : setoid α] {β : quotient sSort v} (q : quotient s) (f : Π (a : α), β a) :
(∀ (a b : α), a bf a == f b)β q

Equations
def quotient.lift₂ {α : Sort u_a} {β : Sort u_b} {φ : Sort u_c} [s₁ : setoid α] [s₂ : setoid β] (f : α → β → φ) :
(∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ b₁a₂ b₂f a₁ a₂ = f b₁ b₂)quotient s₁quotient s₂ → φ

Equations
def quotient.lift_on₂ {α : Sort u_a} {β : Sort u_b} {φ : Sort u_c} [s₁ : setoid α] [s₂ : setoid β] (q₁ : quotient s₁) (q₂ : quotient s₂) (f : α → β → φ) :
(∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ b₁a₂ b₂f a₁ a₂ = f b₁ b₂) → φ

Equations
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₂

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₂) :
(∀ (a : α) (b : β), φ a b)φ q₁ q₂

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₃) :
(∀ (a : α) (b : β) (c : φ), δ a b c)δ q₁ q₂ q₃

theorem quotient.exact {α : Sort u} [s : setoid α] {a b : α} :
a = ba b

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₂) :
(Π (a : α) (b : β), φ a b)φ q₁ q₂

Equations
inductive eqv_gen {α : Type u} :
(α → α → 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} :
(α → α → Prop)setoid α

Equations
theorem quot.exact {α : Type u} (r : α → α → Prop) {a b : α} :
quot.mk r a = quot.mk r beqv_gen r a b

theorem quot.eqv_gen_sound {α : Type u} {r : α → α → Prop} {a b : α} :
eqv_gen r a bquot.mk r a = quot.mk r b

@[instance]
def quotient.decidable_eq {α : Sort u} {s : setoid α} [d : Π (a b : α), decidable (a b)] :

Equations