data.quot

# Quotient types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This module extends the core library's treatment of quotient types (init.data.quot).

## Tags #

quotient

theorem setoid.ext {α : Sort u_1} {s t : setoid α} :
( (a b : α), b b) s = t
@[protected, instance]
def quot.inhabited {α : Sort u_1} (r : α α Prop) [inhabited α] :
inhabited (quot r)
Equations
@[protected, instance]
def quot.subsingleton {α : Sort u_1} {ra : α α Prop} [subsingleton α] :
subsingleton (quot ra)
@[protected]
def quot.hrec_on₂ {α : Sort u_1} {β : Sort u_2} {ra : α α Prop} {rb : β β Prop} {φ : quot ra quot rb Sort u_3} (qa : quot ra) (qb : quot rb) (f : Π (a : α) (b : β), φ (quot.mk ra a) (quot.mk rb b)) (ca : {b : β} {a₁ a₂ : α}, ra a₁ a₂ f a₁ b == f a₂ b) (cb : {a : α} {b₁ b₂ : β}, rb b₁ b₂ f a b₁ == f a b₂) :
φ qa qb

Recursion on two quotient arguments a and b, result type depends on ⟦a⟧ and ⟦b⟧.

Equations
@[protected]
def quot.map {α : Sort u_1} {β : Sort u_2} {ra : α α Prop} {rb : β β Prop} (f : α β) (h : (ra rb) f f) :
quot ra quot rb

Map a function f : α → β such that ra x y implies rb (f x) (f y) to a map quot ra → quot rb.

Equations
• h = quot.lift (λ (x : α), quot.mk rb (f x)) _
@[protected]
def quot.map_right {α : Sort u_1} {ra ra' : α α Prop} (h : (a₁ a₂ : α), ra a₁ a₂ ra' a₁ a₂) :
quot ra quot ra'

If ra is a subrelation of ra', then we have a natural map quot ra → quot ra'.

Equations
def quot.factor {α : Type u_1} (r s : α α Prop) (h : (x y : α), r x y s x y) :
quot r quot s

Weaken the relation of a quotient. This is the same as quot.map id.

Equations
• s h = quot.lift (quot.mk s) _
theorem quot.factor_mk_eq {α : Type u_1} (r s : α α Prop) (h : (x y : α), r x y s x y) :
s h quot.mk r = quot.mk s
theorem quot.lift_mk {α : Sort u_1} {γ : Sort u_4} {r : α α Prop} (f : α γ) (h : (a₁ a₂ : α), r a₁ a₂ f a₁ = f a₂) (a : α) :
quot.lift f h (quot.mk r a) = f a

Alias of quot.lift_beta.

@[simp]
theorem quot.lift_on_mk {α : Sort u_1} {γ : Sort u_4} {r : α α Prop} (a : α) (f : α γ) (h : (a₁ a₂ : α), r a₁ a₂ f a₁ = f a₂) :
(quot.mk r a).lift_on f h = f a
@[simp]
theorem quot.surjective_lift {α : Sort u_1} {γ : Sort u_4} {r : α α Prop} {f : α γ} (h : (a₁ a₂ : α), r a₁ a₂ f a₁ = f a₂) :
function.surjective (quot.lift f h)
@[protected, reducible]
def quot.lift₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α α Prop} {s : β β Prop} (f : α β γ) (hr : (a : α) (b₁ b₂ : β), s b₁ b₂ f a b₁ = f a b₂) (hs : (a₁ a₂ : α) (b : β), r a₁ a₂ f a₁ b = f a₂ b) (q₁ : quot r) (q₂ : quot s) :
γ

Descends a function f : α → β → γ to quotients of α and β.

Equations
• hr hs q₁ q₂ = quot.lift (λ (a : α), quot.lift (f a) _) _ q₁ q₂
@[simp]
theorem quot.lift₂_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α α Prop} {s : β β Prop} (f : α β γ) (hr : (a : α) (b₁ b₂ : β), s b₁ b₂ f a b₁ = f a b₂) (hs : (a₁ a₂ : α) (b : β), r a₁ a₂ f a₁ b = f a₂ b) (a : α) (b : β) :
hr hs (quot.mk r a) (quot.mk s b) = f a b
@[protected, reducible]
def quot.lift_on₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α α Prop} {s : β β Prop} (p : quot r) (q : quot s) (f : α β γ) (hr : (a : α) (b₁ b₂ : β), s b₁ b₂ f a b₁ = f a b₂) (hs : (a₁ a₂ : α) (b : β), r a₁ a₂ f a₁ b = f a₂ b) :
γ

Descends a function f : α → β → γ to quotients of α and β and applies it.

Equations
@[simp]
theorem quot.lift_on₂_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α α Prop} {s : β β Prop} (a : α) (b : β) (f : α β γ) (hr : (a : α) (b₁ b₂ : β), s b₁ b₂ f a b₁ = f a b₂) (hs : (a₁ a₂ : α) (b : β), r a₁ a₂ f a₁ b = f a₂ b) :
(quot.mk r a).lift_on₂ (quot.mk s b) f hr hs = f a b
@[protected]
def quot.map₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} (f : α β γ) (hr : (a : α) (b₁ b₂ : β), s b₁ b₂ t (f a b₁) (f a b₂)) (hs : (a₁ a₂ : α) (b : β), r a₁ a₂ t (f a₁ b) (f a₂ b)) (q₁ : quot r) (q₂ : quot s) :
quot t

Descends a function f : α → β → γ to quotients of α and β wih values in a quotient of γ.

Equations
• hr hs q₁ q₂ = quot.lift₂ (λ (a : α) (b : β), quot.mk t (f a b)) _ _ q₁ q₂
@[simp]
theorem quot.map₂_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} (f : α β γ) (hr : (a : α) (b₁ b₂ : β), s b₁ b₂ t (f a b₁) (f a b₂)) (hs : (a₁ a₂ : α) (b : β), r a₁ a₂ t (f a₁ b) (f a₂ b)) (a : α) (b : β) :
hr hs (quot.mk r a) (quot.mk s b) = quot.mk t (f a b)
@[protected, reducible]
def quot.rec_on_subsingleton₂ {α : Sort u_1} {β : Sort u_2} {r : α α Prop} {s : β β Prop} {φ : quot r quot s Sort u_3} [h : (a : α) (b : β), subsingleton (quot.mk r a) (quot.mk s b))] (q₁ : quot r) (q₂ : quot s) (f : Π (a : α) (b : β), φ (quot.mk r a) (quot.mk s b)) :
φ q₁ q₂

A binary version of quot.rec_on_subsingleton.

Equations
@[protected]
theorem quot.induction_on₂ {α : Sort u_1} {β : Sort u_2} {r : α α Prop} {s : β β Prop} {δ : quot r quot s Prop} (q₁ : quot r) (q₂ : quot s) (h : (a : α) (b : β), δ (quot.mk r a) (quot.mk s b)) :
δ q₁ q₂
@[protected]
theorem quot.induction_on₃ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : α α Prop} {s : β β Prop} {t : γ γ Prop} {δ : quot r quot s quot t Prop} (q₁ : quot r) (q₂ : quot s) (q₃ : quot t) (h : (a : α) (b : β) (c : γ), δ (quot.mk r a) (quot.mk s b) (quot.mk t c)) :
δ q₁ q₂ q₃
@[protected, instance]
def quot.lift.decidable_pred {α : Sort u_1} (r : α α Prop) (f : α Prop) (h : (a b : α), r a b f a = f b) [hf : decidable_pred f] :
decidable_pred (quot.lift f h)
Equations
• = λ (q : quot (λ (a b : α), r a b)),
@[protected, instance]
def quot.lift₂.decidable_pred {α : Sort u_1} {β : Sort u_2} (r : α α Prop) (s : β β Prop) (f : α β Prop) (ha : (a : α) (b₁ b₂ : β), s b₁ b₂ f a b₁ = f a b₂) (hb : (a₁ a₂ : α) (b : β), r a₁ a₂ f a₁ b = f a₂ b) [hf : Π (a : α), decidable_pred (f a)] (q₁ : quot r) :
decidable_pred ha hb q₁)

Note that this provides decidable_rel (quot.lift₂ f ha hb) when α = β.

Equations
@[protected, instance]
def quot.lift_on.decidable {α : Sort u_1} (r : α α Prop) (q : quot r) (f : α Prop) (h : (a b : α), r a b f a = f b)  :
Equations
@[protected, instance]
def quot.lift_on₂.decidable {α : Sort u_1} {β : Sort u_2} (r : α α Prop) (s : β β Prop) (q₁ : quot r) (q₂ : quot s) (f : α β Prop) (ha : (a : α) (b₁ b₂ : β), s b₁ b₂ f a b₁ = f a b₂) (hb : (a₁ a₂ : α) (b : β), r a₁ a₂ f a₁ b = f a₂ b) [Π (a : α), decidable_pred (f a)] :
decidable (q₁.lift_on₂ q₂ f ha hb)
Equations
@[protected, instance]
def quotient.inhabited {α : Sort u_1} (s : setoid α) [inhabited α] :
Equations
@[protected, instance]
def quotient.subsingleton {α : Sort u_1} (s : setoid α) [subsingleton α] :
@[protected, instance]
@[protected]
def quotient.hrec_on₂ {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] {φ : quotient sa quotient sb Sort u_3} (qa : quotient sa) (qb : quotient sb) (f : Π (a : α) (b : β), φ a b) (c : (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂ b₁ b₂ f a₁ b₁ == f a₂ b₂) :
φ qa qb

Induction on two quotient arguments a and b, result type depends on ⟦a⟧ and ⟦b⟧.

Equations
@[protected]
def quotient.map {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] (f : α β) (h : f) :

Map a function f : α → β that sends equivalent elements to equivalent elements to a function quotient sa → quotient sb. Useful to define unary operations on quotients.

Equations
• h = h
@[simp]
theorem quotient.map_mk {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] (f : α β) (h : f) (x : α) :
h x = f x
@[protected]
def quotient.map₂ {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] {γ : Sort u_4} [sc : setoid γ] (f : α β γ) (h : f) :

Map a function f : α → β → γ that sends equivalent elements to equivalent elements to a function f : quotient sa → quotient sb → quotient sc. Useful to define binary operations on quotients.

Equations
@[simp]
theorem quotient.map₂_mk {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] {γ : Sort u_4} [sc : setoid γ] (f : α β γ) (h : f) (x : α) (y : β) :
@[protected, instance]
def quotient.lift.decidable_pred {α : Sort u_1} [sa : setoid α] (f : α Prop) (h : (a b : α), a b f a = f b)  :
Equations
@[protected, instance]
def quotient.lift₂.decidable_pred {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] (f : α β Prop) (h : (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂ b₁ b₂ f a₁ b₁ = f a₂ b₂) [hf : Π (a : α), decidable_pred (f a)] (q₁ : quotient sa) :

Note that this provides decidable_rel (quotient.lift₂ f h) when α = β.

Equations
@[protected, instance]
def quotient.lift_on.decidable {α : Sort u_1} [sa : setoid α] (q : quotient sa) (f : α Prop) (h : (a b : α), a b f a = f b)  :
Equations
@[protected, instance]
def quotient.lift_on₂.decidable {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] (q₁ : quotient sa) (q₂ : quotient sb) (f : α β Prop) (h : (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂ b₁ b₂ f a₁ b₁ = f a₂ b₂) [Π (a : α), decidable_pred (f a)] :
decidable (q₁.lift_on₂ q₂ f h)
Equations
• f h = q₂
theorem quot.eq {α : Type u_1} {r : α α Prop} {x y : α} :
quot.mk r x = quot.mk r y x y
@[simp]
theorem quotient.eq {α : Sort u_1} [r : setoid α] {x y : α} :
theorem forall_quotient_iff {α : Type u_1} [r : setoid α] {p : Prop} :
( (a : quotient r), p a) (a : α), p a
@[simp]
theorem quotient.lift_mk {α : Sort u_1} {β : Sort u_2} [s : setoid α] (f : α β) (h : (a b : α), a b f a = f b) (x : α) :
x = f x
@[simp]
theorem quotient.lift_comp_mk {α : Sort u_1} {β : Sort u_2} [setoid α] (f : α β) (h : (a b : α), a b f a = f b) :
= f
@[simp]
theorem quotient.lift₂_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [setoid α] [setoid β] (f : α β γ) (h : (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ b₁ a₂ b₂ f a₁ a₂ = f b₁ b₂) (a : α) (b : β) :
a b = f a b
@[simp]
theorem quotient.lift_on_mk {α : Sort u_1} {β : Sort u_2} [s : setoid α] (f : α β) (h : (a b : α), a b f a = f b) (x : α) :
x.lift_on f h = f x
@[simp]
theorem quotient.lift_on₂_mk {α : Sort u_1} {β : Sort u_2} [setoid α] (f : α α β) (h : (a₁ a₂ b₁ b₂ : α), a₁ b₁ a₂ b₂ f a₁ a₂ = f b₁ b₂) (x y : α) :
theorem surjective_quot_mk {α : Sort u_1} (r : α α Prop) :

quot.mk r is a surjective function.

theorem surjective_quotient_mk (α : Sort u_1) [s : setoid α] :

quotient.mk is a surjective function.

noncomputable def quot.out {α : Sort u_1} {r : α α Prop} (q : quot r) :
α

Choose an element of the equivalence class using the axiom of choice. Sound but noncomputable.

Equations
meta def quot.unquot {α : Sort u_1} {r : α α Prop} :
quot r α

Unwrap the VM representation of a quotient to obtain an element of the equivalence class. Computable but unsound.

@[simp]
theorem quot.out_eq {α : Sort u_1} {r : α α Prop} (q : quot r) :
quot.mk r q.out = q
noncomputable def quotient.out {α : Sort u_1} [s : setoid α] :
α

Choose an element of the equivalence class using the axiom of choice. Sound but noncomputable.

Equations
@[simp]
theorem quotient.out_eq {α : Sort u_1} [s : setoid α] (q : quotient s) :
theorem quotient.mk_out {α : Sort u_1} [s : setoid α] (a : α) :
theorem quotient.mk_eq_iff_out {α : Sort u_1} [s : setoid α] {x : α} {y : quotient s} :
x = y x y.out
theorem quotient.eq_mk_iff_out {α : Sort u_1} [s : setoid α] {x : quotient s} {y : α} :
x = y x.out y
@[simp]
theorem quotient.out_equiv_out {α : Sort u_1} {s : setoid α} {x y : quotient s} :
x.out y.out x = y
theorem quotient.out_injective {α : Sort u_1} {s : setoid α} :
@[simp]
theorem quotient.out_inj {α : Sort u_1} {s : setoid α} {x y : quotient s} :
x.out = y.out x = y
@[protected, instance]
def pi_setoid {ι : Sort u_1} {α : ι Sort u_2} [Π (i : ι), setoid (α i)] :
setoid (Π (i : ι), α i)
Equations
noncomputable def quotient.choice {ι : Type u_1} {α : ι Type u_2} [S : Π (i : ι), setoid (α i)] (f : Π (i : ι), quotient (S i)) :

Given a function f : Π i, quotient (S i), returns the class of functions Π i, α i sending each i to an element of the class f i.

Equations
@[simp]
theorem quotient.choice_eq {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), setoid (α i)] (f : Π (i : ι), α i) :
quotient.choice (λ (i : ι), f i) = f
theorem quotient.induction_on_pi {ι : Type u_1} {α : ι Sort u_2} [s : Π (i : ι), setoid (α i)] {p : (Π (i : ι), quotient (s i)) Prop} (f : Π (i : ι), quotient (s i)) (h : (a : Π (i : ι), α i), p (λ (i : ι), a i)) :
p f
theorem nonempty_quotient_iff {α : Sort u_1} (s : setoid α) :

### Truncation #

theorem true_equivalence {α : Sort u_1} :
equivalence (λ (_x _x : α), true)
def true_setoid {α : Sort u_1} :

Always-true relation as a setoid.

Note that in later files the preferred spelling is ⊤ : setoid α.

Equations
def trunc (α : Sort u) :

trunc α is the quotient of α by the always-true relation. This is related to the propositional truncation in HoTT, and is similar in effect to nonempty α, but unlike nonempty α, trunc α is data, so the VM representation is the same as α, and so this can be used to maintain computability.

Equations
Instances for trunc
def trunc.mk {α : Sort u_1} (a : α) :

Constructor for trunc α

Equations
@[protected, instance]
def trunc.inhabited {α : Sort u_1} [inhabited α] :
Equations
def trunc.lift {α : Sort u_1} {β : Sort u_2} (f : α β) (c : (a b : α), f a = f b) :
β

Any constant function lifts to a function out of the truncation

Equations
• c = quot.lift f _
theorem trunc.ind {α : Sort u_1} {β : Prop} :
( (a : α), β (trunc.mk a)) (q : trunc α), β q
@[protected]
theorem trunc.lift_mk {α : Sort u_1} {β : Sort u_2} (f : α β) (c : (a b : α), f a = f b) (a : α) :
c (trunc.mk a) = f a
@[protected, reducible]
def trunc.lift_on {α : Sort u_1} {β : Sort u_2} (q : trunc α) (f : α β) (c : (a b : α), f a = f b) :
β

Lift a constant function on q : trunc α.

Equations
@[protected]
theorem trunc.induction_on {α : Sort u_1} {β : Prop} (q : trunc α) (h : (a : α), β (trunc.mk a)) :
β q
theorem trunc.exists_rep {α : Sort u_1} (q : trunc α) :
(a : α), = q
@[protected]
theorem trunc.induction_on₂ {α : Sort u_1} {β : Sort u_2} {C : Prop} (q₁ : trunc α) (q₂ : trunc β) (h : (a : α) (b : β), C (trunc.mk a) (trunc.mk b)) :
C q₁ q₂
@[protected]
theorem trunc.eq {α : Sort u_1} (a b : trunc α) :
a = b
@[protected, instance]
def trunc.subsingleton {α : Sort u_1} :
def trunc.bind {α : Sort u_1} {β : Sort u_2} (q : trunc α) (f : α ) :

The bind operator for the trunc monad.

Equations
def trunc.map {α : Sort u_1} {β : Sort u_2} (f : α β) (q : trunc α) :

A function f : α → β defines a function map f : trunc α → trunc β.

Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, reducible]
def trunc.rec {α : Sort u_1} {C : Sort u_3} (f : Π (a : α), C (trunc.mk a)) (h : (a b : α), eq.rec (f a) _ = f b) (q : trunc α) :
C q

Recursion/induction principle for trunc.

Equations
• h q = _ q
@[protected, reducible]
def trunc.rec_on {α : Sort u_1} {C : Sort u_3} (q : trunc α) (f : Π (a : α), C (trunc.mk a)) (h : (a b : α), eq.rec (f a) _ = f b) :
C q

A version of trunc.rec taking q : trunc α as the first argument.

Equations
@[protected, reducible]
def trunc.rec_on_subsingleton {α : Sort u_1} {C : Sort u_3} [ (a : α), subsingleton (C (trunc.mk a))] (q : trunc α) (f : Π (a : α), C (trunc.mk a)) :
C q

A version of trunc.rec_on assuming the codomain is a subsingleton.

Equations
• = _ q
noncomputable def trunc.out {α : Sort u_1} :
α

Noncomputably extract a representative of trunc α (using the axiom of choice).

Equations
@[simp]
theorem trunc.out_eq {α : Sort u_1} (q : trunc α) :
= q
@[protected]
theorem trunc.nonempty {α : Sort u_1} (q : trunc α) :

### quotient with implicit setoid#

Versions of quotient definitions and lemmas ending in ' use unification instead of typeclass inference for inferring the setoid argument. This is useful when there are several different quotient relations on a type, for example quotient groups, rings and modules.

@[protected]
def quotient.mk' {α : Sort u_1} {s₁ : setoid α} (a : α) :

A version of quotient.mk taking {s : setoid α} as an implicit argument instead of an instance argument.

Equations
theorem quotient.surjective_quotient_mk' {α : Sort u_1} {s₁ : setoid α} :

quotient.mk' is a surjective function.

@[protected, reducible]
def quotient.lift_on' {α : Sort u_1} {φ : Sort u_4} {s₁ : setoid α} (q : quotient s₁) (f : α φ) (h : (a b : α), b f a = f b) :
φ

A version of quotient.lift_on taking {s : setoid α} as an implicit argument instead of an instance argument.

Equations
@[protected, simp]
theorem quotient.lift_on'_mk' {α : Sort u_1} {φ : Sort u_4} {s₁ : setoid α} (f : α φ) (h : (a b : α), b f a = f b) (x : α) :
(quotient.mk' x).lift_on' f h = f x
@[simp]
theorem quotient.surjective_lift_on' {α : Sort u_1} {φ : Sort u_4} {s₁ : setoid α} {f : α φ} (h : (a b : α), b f a = f b) :
function.surjective (λ (x : quotient s₁), x.lift_on' f h)
@[protected, reducible]
def quotient.lift_on₂' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} (q₁ : quotient s₁) (q₂ : quotient s₂) (f : α β γ) (h : (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), setoid.r a₁ b₁ setoid.r a₂ b₂ f a₁ a₂ = f b₁ b₂) :
γ

A version of quotient.lift_on₂ taking {s₁ : setoid α} {s₂ : setoid β} as implicit arguments instead of instance arguments.

Equations
@[protected, simp]
theorem quotient.lift_on₂'_mk' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} (f : α β γ) (h : (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), setoid.r a₁ b₁ setoid.r a₂ b₂ f a₁ a₂ = f b₁ b₂) (a : α) (b : β) :
(quotient.mk' b) f h = f a b
@[protected]
theorem quotient.ind' {α : Sort u_1} {s₁ : setoid α} {p : quotient s₁ Prop} (h : (a : α), p (quotient.mk' a)) (q : quotient s₁) :
p q

A version of quotient.ind taking {s : setoid α} as an implicit argument instead of an instance argument.

@[protected]
theorem quotient.ind₂' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} {p : quotient s₁ quotient s₂ Prop} (h : (a₁ : α) (a₂ : β), p (quotient.mk' a₁) (quotient.mk' a₂)) (q₁ : quotient s₁) (q₂ : quotient s₂) :
p q₁ q₂

A version of quotient.ind₂ taking {s₁ : setoid α} {s₂ : setoid β} as implicit arguments instead of instance arguments.

@[protected]
theorem quotient.induction_on' {α : Sort u_1} {s₁ : setoid α} {p : quotient s₁ Prop} (q : quotient s₁) (h : (a : α), p (quotient.mk' a)) :
p q

A version of quotient.induction_on taking {s : setoid α} as an implicit argument instead of an instance argument.

@[protected]
theorem quotient.induction_on₂' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} {p : quotient s₁ quotient s₂ Prop} (q₁ : quotient s₁) (q₂ : quotient s₂) (h : (a₁ : α) (a₂ : β), p (quotient.mk' a₁) (quotient.mk' a₂)) :
p q₁ q₂

A version of quotient.induction_on₂ taking {s₁ : setoid α} {s₂ : setoid β} as implicit arguments instead of instance arguments.

@[protected]
theorem quotient.induction_on₃' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ} {p : quotient s₁ quotient s₂ quotient s₃ Prop} (q₁ : quotient s₁) (q₂ : quotient s₂) (q₃ : quotient s₃) (h : (a₁ : α) (a₂ : β) (a₃ : γ), p (quotient.mk' a₁) (quotient.mk' a₂) (quotient.mk' a₃)) :
p q₁ q₂ q₃

A version of quotient.induction_on₃ taking {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ} as implicit arguments instead of instance arguments.

@[protected]
def quotient.rec_on_subsingleton' {α : Sort u_1} {s₁ : setoid α} {φ : quotient s₁ Sort u_2} [h : (a : α), subsingleton a)] (q : quotient s₁) (f : Π (a : α), φ (quotient.mk' a)) :
φ q

A version of quotient.rec_on_subsingleton taking {s₁ : setoid α} as an implicit argument instead of an instance argument.

Equations
@[protected, reducible]
def quotient.rec_on_subsingleton₂' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} {φ : quotient s₁ quotient s₂ Sort u_3} [h : (a : α) (b : β), subsingleton a b)] (q₁ : quotient s₁) (q₂ : quotient s₂) (f : Π (a₁ : α) (a₂ : β), φ (quotient.mk' a₁) (quotient.mk' a₂)) :
φ q₁ q₂

A version of quotient.rec_on_subsingleton₂ taking {s₁ : setoid α} {s₂ : setoid α} as implicit arguments instead of instance arguments.

Equations
@[protected]
def quotient.hrec_on' {α : Sort u_1} {s₁ : setoid α} {φ : quotient s₁ Sort u_2} (qa : quotient s₁) (f : Π (a : α), φ (quotient.mk' a)) (c : (a₁ a₂ : α), a₁ a₂ f a₁ == f a₂) :
φ qa

Recursion on a quotient argument a, result type depends on ⟦a⟧.

Equations
@[simp]
theorem quotient.hrec_on'_mk' {α : Sort u_1} {s₁ : setoid α} {φ : quotient s₁ Sort u_2} (f : Π (a : α), φ (quotient.mk' a)) (c : (a₁ a₂ : α), a₁ a₂ f a₁ == f a₂) (x : α) :
(quotient.mk' x).hrec_on' f c = f x
@[protected]
def quotient.hrec_on₂' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} {φ : quotient s₁ quotient s₂ Sort u_3} (qa : quotient s₁) (qb : quotient s₂) (f : Π (a : α) (b : β), φ (quotient.mk' a) (quotient.mk' b)) (c : (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂ b₁ b₂ f a₁ b₁ == f a₂ b₂) :
φ qa qb

Recursion on two quotient arguments a and b, result type depends on ⟦a⟧ and ⟦b⟧.

Equations
@[simp]
theorem quotient.hrec_on₂'_mk' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} {φ : quotient s₁ quotient s₂ Sort u_3} (f : Π (a : α) (b : β), φ (quotient.mk' a) (quotient.mk' b)) (c : (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂ b₁ b₂ f a₁ b₁ == f a₂ b₂) (x : α) (qb : quotient s₂) :
qb f c = qb.hrec_on' (f x) _
@[protected]
def quotient.map' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} (f : α β) (h : f f) :

Map a function f : α → β that sends equivalent elements to equivalent elements to a function quotient sa → quotient sb. Useful to define unary operations on quotients.

Equations
• = h
@[simp]
theorem quotient.map'_mk' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} (f : α β) (h : f f) (x : α) :
@[protected]
def quotient.map₂' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ} (f : α β γ) (h : f f) :

A version of quotient.map₂ using curly braces and unification.

Equations
@[simp]
theorem quotient.map₂'_mk' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ} (f : α β γ) (h : f f) (x : α) :
theorem quotient.exact' {α : Sort u_1} {s₁ : setoid α} {a b : α} :
b
theorem quotient.sound' {α : Sort u_1} {s₁ : setoid α} {a b : α} :
b
@[protected, simp]
theorem quotient.eq' {α : Sort u_1} {s₁ : setoid α} {a b : α} :
b
noncomputable def quotient.out' {α : Sort u_1} {s₁ : setoid α} (a : quotient s₁) :
α

A version of quotient.out taking {s₁ : setoid α} as an implicit argument instead of an instance argument.

Equations
@[simp]
theorem quotient.out_eq' {α : Sort u_1} {s₁ : setoid α} (q : quotient s₁) :
theorem quotient.mk_out' {α : Sort u_1} {s₁ : setoid α} (a : α) :
a
@[protected]
theorem quotient.mk'_eq_mk {α : Sort u_1} [setoid α] (x : α) :
@[protected, simp]
theorem quotient.lift_on'_mk {α : Sort u_1} {β : Sort u_2} [setoid α] (x : α) (f : α β) (h : (a b : α), b f a = f b) :
x.lift_on' f h = f x
@[protected, simp]
theorem quotient.lift_on₂'_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [setoid α] [setoid β] (f : α β γ) (h : (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), setoid.r a₁ b₁ setoid.r a₂ b₂ f a₁ a₂ = f b₁ b₂) (a : α) (b : β) :
f h = f a b
@[simp]
theorem quotient.map'_mk {α : Sort u_1} {β : Sort u_2} [setoid α] [setoid β] (f : α β) (h : f f) (x : α) :
@[protected, instance]
def quotient.lift_on'.decidable {α : Sort u_1} {s₁ : setoid α} (q : quotient s₁) (f : α Prop) (h : (a b : α), b f a = f b)  :
Equations
@[protected, instance]
def quotient.lift_on₂'.decidable {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} (q₁ : quotient s₁) (q₂ : quotient s₂) (f : α β Prop) (h : (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), setoid.r a₁ a₂ setoid.r b₁ b₂ f a₁ b₁ = f a₂ b₂) [Π (a : α), decidable_pred (f a)] :
decidable (q₁.lift_on₂' q₂ f h)
Equations