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
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 b → f a = f b) → β
theorem
quot.induction_on
{α : Sort u}
{r : α → α → Prop}
{β : quot r → Prop}
(q : quot r) :
(∀ (a : α), β (quot.mk r a)) → β q
def
quot.indep
{α : Sort u}
{r : α → α → Prop}
{β : quot r → Sort v} :
(Π (a : α), β (quot.mk r a)) → α → psigma β
Equations
- quot.indep f a = ⟨quot.mk r a, f a⟩
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
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
def
quot.rec_on_subsingleton
{α : Sort u}
{r : α → α → Prop}
{β : quot r → Sort v}
[h : ∀ (a : α), subsingleton (β (quot.mk r a))]
(q : quot r) :
(Π (a : α), β (quot.mk r a)) → β q
Equations
- q.rec_on_subsingleton f = quot.rec f _ q
Equations
Equations
- quotient.lift f = quot.lift f
Equations
- q.lift_on f c = quot.lift_on q f c
def
quotient.rec_on_subsingleton
{α : Sort u}
[s : setoid α]
{β : quotient s → Sort v}
[h : ∀ (a : α), subsingleton (β ⟦a⟧)]
(q : quotient s) :
Equations
def
quotient.lift₂
{α : Sort u_a}
{β : Sort u_b}
{φ : Sort u_c}
[s₁ : setoid α]
[s₂ : setoid β]
(f : α → β → φ) :
Equations
- quotient.lift₂ f c q₁ q₂ = quotient.lift (λ (a₁ : α), quotient.lift (f a₁) _ q₂) _ q₁
def
quotient.lift_on₂
{α : Sort u_a}
{β : Sort u_b}
{φ : Sort u_c}
[s₁ : setoid α]
[s₂ : setoid β]
(q₁ : quotient s₁)
(q₂ : quotient s₂)
(f : α → β → φ) :
Equations
- q₁.lift_on₂ q₂ f c = quotient.lift₂ f c q₁ q₂
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₂) :
Equations
- q₁.rec_on_subsingleton₂ q₂ f = q₁.rec_on_subsingleton (λ (a : α), q₂.rec_on_subsingleton (λ (b : β), f a b))
- rel : ∀ {α : Type u} (r : α → α → Prop) (x y : α), r x y → eqv_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 y → eqv_gen r y x
- trans : ∀ {α : Type u} (r : α → α → Prop) (x y z : α), eqv_gen r x y → eqv_gen r y z → eqv_gen r x z
@[instance]
def
quotient.decidable_eq
{α : Sort u}
{s : setoid α}
[d : Π (a b : α), decidable (a ≈ b)] :
decidable_eq (quotient s)
Equations
- quotient.decidable_eq = λ (q₁ q₂ : quotient s), q₁.rec_on_subsingleton₂ q₂ (λ (a₁ a₂ : α), quotient.decidable_eq._match_1 a₁ a₂ (d a₁ a₂))
- quotient.decidable_eq._match_1 a₁ a₂ (decidable.is_true h₁) = decidable.is_true _
- quotient.decidable_eq._match_1 a₁ a₂ (decidable.is_false h₂) = decidable.is_false _