mathlib3 documentation

core / init.data.quot

source
theorem iff_subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) :
p b
source
constant quot.sound {α : Sort u} {r : α → α → Prop} {a b : α} :
r a b → quot.mk r a = quot.mk r b
source
@[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
source
@[protected]
theorem quot.ind_beta {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} (p : ∀ (a : α), β (quot.mk r a)) (a : α) :
_ = _
source
@[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
source
@[protected]
theorem quot.induction_on {α : Sort u} {r : α → α → Prop} {β : quot r → Prop} (q : quot r) (h : ∀ (a : α), β (quot.mk r a)) :
β q
source
theorem quot.exists_rep {α : Sort u} {r : α → α → Prop} (q : quot r) :
∃ (a : α), quot.mk r a = q
source
@[protected, reducible]
def quot.indep {α : Sort u} {r : α → α → Prop} {β : quot r → Sort v} (f : Π (a : α), β (quot.mk r a)) (a : α) :
psigma β
Equations
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
def quotient {α : Sort u} (s : setoid α) :
Sort u
Equations
Instances for quotient
source
@[protected]
def quotient.mk {α : Sort u} [s : setoid α] (a : α) :
quotient s
Equations
source
theorem quotient.sound {α : Sort u} [s : setoid α] {a b : α} :
a ≈ b → ⟦a⟧ = ⟦b⟧
source
@[protected, reducible]
def quotient.lift {α : Sort u} {β : Sort v} [s : setoid α] (f : α → β) :
(∀ (a b : α), a ≈ b → f a = f b) → quotient s → β
Equations
source
@[protected]
theorem quotient.ind {α : Sort u} [s : setoid α] {β : quotient s → Prop} :
(∀ (a : α), β ⟦a⟧) → ∀ (q : quotient s), β q
source
@[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
source
@[protected]
theorem quotient.induction_on {α : Sort u} [s : setoid α] {β : quotient s → Prop} (q : quotient s) (h : ∀ (a : α), β ⟦a⟧) :
β q
source
theorem quotient.exists_rep {α : Sort u} [s : setoid α] (q : quotient s) :
∃ (a : α), ⟦a⟧ = q
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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₂
source
@[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₂
source
@[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₃
source
theorem quotient.exact {α : Sort u} [s : setoid α] {a b : α} :
⟦a⟧ = ⟦b⟧ → a ≈ b
source
@[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
source
inductive eqv_gen {α : Type u} (r : α → α → Prop) :
α → α → Prop
source
theorem eqv_gen.is_equivalence {α : Type u} (r : α → α → Prop) :
equivalence (eqv_gen r)
source
def eqv_gen.setoid {α : Type u} (r : α → α → Prop) :
setoid α
Equations
source
theorem quot.exact {α : Type u} (r : α → α → Prop) {a b : α} (H : quot.mk r a = quot.mk r b) :
eqv_gen r a b
source
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
source
@[protected, instance]
def quotient.decidable_eq {α : Sort u} {s : setoid α} [d : Π (a b : α), decidable (a ≈ b)] :
decidable_eq (quotient s)
Equations