core / init.data.quot - mathlib docs

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

source

@[protected]

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

_ = _

source

@[protected]

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

q.lift_on f c = quot.lift f c q

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]

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

psigma β

Equations

quot.indep f a = ⟨quot.mk r a, f a⟩

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]

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

quot.rec f h q = _.rec_on (quot.lift (quot.indep f) _ q).snd

source

@[protected]

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

q.rec_on f h = quot.rec f h q

source

@[protected]

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

q.rec_on_subsingleton f = quot.rec f _ q

source

@[protected]

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

q.hrec_on f c = q.rec_on f _

source

def quotient {α : Sort u} (s : setoid α) :

Sort u

Equations

quotient s = quot setoid.r

Instances for quotient

source

@[protected]

def quotient.mk {α : Sort u} [s : setoid α] (a : α) :

quotient s

Equations

⟦a⟧ = quot.mk setoid.r a

source

theorem quotient.sound {α : Sort u} [s : setoid α] {a b : α} :

a ≈ b → ⟦a⟧ = ⟦b⟧

source

@[protected]

def quotient.lift {α : Sort u} {β : Sort v} [s : setoid α] (f : α → β) :

(∀ (a b : α), a ≈ b → f a = f b) → quotient s → β

Equations

quotient.lift f = quot.lift f

source

@[protected]

theorem quotient.ind {α : Sort u} [s : setoid α] {β : quotient s → Prop} :

(∀ (a : α), β ⟦a⟧) → ∀ (q : quotient s), β q

source

@[protected]

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

β

Equations

q.lift_on f c = quot.lift_on q f c

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

quotient.rec f h q = quot.rec f h q

source

@[protected]

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

q.rec_on f h = quot.rec_on q f h

source

@[protected]

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

q.rec_on_subsingleton f = quot.rec_on_subsingleton q f

source

@[protected]

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

q.hrec_on f c = quot.hrec_on q f c

source

@[protected]

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

quotient.lift₂ f c q₁ q₂ = quotient.lift (λ (a₁ : α), quotient.lift (f a₁) _ q₂) _ q₁

source

@[protected]

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

q₁.lift_on₂ q₂ f c = quotient.lift₂ f c q₁ q₂

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]

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

q₁.rec_on_subsingleton₂ q₂ f = q₁.rec_on_subsingleton (λ (a : α), q₂.rec_on_subsingleton (λ (b : β), f a b))

source

inductive eqv_gen {α : Type u} (r : α → α → Prop) :

α → α → Prop

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

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

eqv_gen.setoid r = {r := eqv_gen r, iseqv := _}

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

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 _