# Quotient types #

This module extends the core library's treatment of quotient types (Init.Core).

## Tags #

quotient

theorem Setoid.ext {α : Sort u_3} {s : } {t : } :
(∀ (a b : α), Setoid.r a b Setoid.r a b)s = t
theorem Quot.induction_on {α : Sort u_4} {r : ααProp} {β : Quot rProp} (q : Quot r) (h : ∀ (a : α), β (Quot.mk r a)) :
β q
instance Quot.instInhabited_mathlib {α : Sort u_1} (r : ααProp) [] :
Equations
instance Quot.Subsingleton {α : Sort u_1} {ra : ααProp} [] :
Equations
• =
@[deprecated Quot.recOn]
def Quot.recOn' {α : Sort u} {r : ααProp} {motive : Quot rSort v} (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), f a = f b) :
motive q

Alias of Quot.recOn.

Dependent recursion principle for Quot. This constructor can be tricky to use, so you should consider the simpler versions if they apply:

• Quot.lift, for nondependent functions
• Quot.ind, for theorems / proofs of propositions about quotients
• Quot.recOnSubsingleton, when the target type is a Subsingleton
• Quot.hrecOn, which uses HEq (f a) (f b) instead of a sound p ▸ f a = f b assummption
Equations
Instances For
@[deprecated Quot.recOnSubsingleton]
def Quot.recOnSubsingleton' {α : Sort u} {r : ααProp} {motive : Quot rSort v} [h : ∀ (a : α), Subsingleton (motive (Quot.mk r a))] (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) :
motive q

Alias of Quot.recOnSubsingleton.

Dependent induction principle for a quotient, when the target type is a Subsingleton. In this case the quotient's side condition is trivial so any function can be lifted.

Equations
Instances For
instance Quot.instUnique {α : Sort u_1} {ra : ααProp} [] :
Equations
def Quot.hrecOn₂ {α : Sort u_1} {β : Sort u_2} {ra : ααProp} {rb : ββProp} {φ : Quot raQuot rbSort 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₂HEq (f a₁ b) (f a₂ b)) (cb : ∀ {a : α} {b₁ b₂ : β}, rb b₁ b₂HEq (f a b₁) (f a b₂)) :
φ qa qb

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

Equations
Instances For
def Quot.map {α : Sort u_1} {β : Sort u_2} {ra : ααProp} {rb : ββProp} (f : αβ) (h : (ra rb) f f) :
Quot raQuot rb

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

Equations
Instances For
def Quot.mapRight {α : Sort u_1} {ra : ααProp} {ra' : ααProp} (h : ∀ (a₁ a₂ : α), ra a₁ a₂ra' a₁ a₂) :
Quot raQuot ra'

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

Equations
Instances For
def Quot.factor {α : Type u_4} (r : ααProp) (s : ααProp) (h : ∀ (x y : α), r x ys x y) :
Quot rQuot s

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

Equations
Instances For
theorem Quot.factor_mk_eq {α : Type u_4} (r : ααProp) (s : ααProp) (h : ∀ (x y : α), r x ys x y) :
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
theorem Quot.liftOn_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).liftOn 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₂) :
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
Instances For
@[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 : β) :
Quot.lift₂ f hr hs (Quot.mk r a) (Quot.mk s b) = f a b
def Quot.liftOn₂ {α : 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
Instances For
@[simp]
theorem Quot.liftOn₂_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).liftOn₂ (Quot.mk s b) f hr hs = f a b
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) :

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

Equations
Instances For
@[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 : β) :
Quot.map₂ f hr hs (Quot.mk r a) (Quot.mk s b) = Quot.mk t (f a b)
def Quot.recOnSubsingleton₂ {α : Sort u_1} {β : Sort u_2} {r : ααProp} {s : ββProp} {φ : Quot rQuot sSort u_5} [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.recOnSubsingleton.

Equations
Instances For
theorem Quot.induction_on₂ {α : Sort u_1} {β : Sort u_2} {r : ααProp} {s : ββProp} {δ : Quot rQuot sProp} (q₁ : Quot r) (q₂ : Quot s) (h : ∀ (a : α) (b : β), δ (Quot.mk r a) (Quot.mk s b)) :
δ q₁ q₂
theorem Quot.induction_on₃ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_4} {r : ααProp} {s : ββProp} {t : γγProp} {δ : Quot rQuot sQuot tProp} (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₃
instance Quot.lift.decidablePred {α : Sort u_1} (r : ααProp) (f : αProp) (h : ∀ (a b : α), r a bf a = f b) [hf : ] :
Equations
instance Quot.lift₂.decidablePred {α : 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 : α) → DecidablePred (f a)] (q₁ : Quot r) :

Note that this provides DecidableRel (Quot.Lift₂ f ha hb) when α = β.

Equations
instance Quot.instDecidableLiftOnOfDecidablePred_mathlib {α : Sort u_1} (r : ααProp) (q : Quot r) (f : αProp) (h : ∀ (a b : α), r a bf a = f b) [] :
Decidable (q.liftOn f h)
Equations
instance Quot.instDecidableLiftOn₂OfDecidablePred {α : 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 : α) → DecidablePred (f a)] :
Decidable (q₁.liftOn₂ q₂ f ha hb)
Equations

The canonical quotient map into a Quotient.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Pretty printer defined by notation3 command.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance Quotient.instInhabitedQuotient {α : Sort u_1} (s : ) [] :
Equations
• = { default := default }
instance Quotient.instSubsingletonQuotient {α : Sort u_1} (s : ) [] :
Equations
• =
instance Quotient.instUniqueQuotient {α : Sort u_1} (s : ) [] :
Equations
instance Quotient.instIsEquivEquiv {α : Type u_4} [] :
IsEquiv α fun (x1 x2 : α) => x1 x2
Equations
• =
def Quotient.hrecOn₂ {α : Sort u_1} {β : Sort u_2} [sa : ] [sb : ] {φ : Quotient saQuotient sbSort u_3} (qa : Quotient sa) (qb : Quotient sb) (f : (a : α) → (b : β) → φ a b) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂HEq (f a₁ b₁) (f a₂ b₂)) :
φ qa qb

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

Equations
Instances For
def Quotient.map {α : Sort u_1} {β : Sort u_2} [sa : ] [sb : ] (f : αβ) (h : ((fun (x1 x2 : α) => x1 x2) fun (x1 x2 : β) => x1 x2) f f) :
Quotient saQuotient sb

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
Instances For
@[simp]
theorem Quotient.map_mk {α : Sort u_1} {β : Sort u_2} [sa : ] [sb : ] (f : αβ) (h : ((fun (x1 x2 : α) => x1 x2) fun (x1 x2 : β) => x1 x2) f f) (x : α) :
Quotient.map f h x = f x
def Quotient.map₂ {α : Sort u_1} {β : Sort u_2} [sa : ] [sb : ] {γ : Sort u_4} [sc : ] (f : αβγ) (h : ((fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) fun (x1 x2 : γ) => x1 x2) f f) :
Quotient saQuotient sbQuotient sc

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
Instances For
@[simp]
theorem Quotient.map₂_mk {α : Sort u_1} {β : Sort u_2} [sa : ] [sb : ] {γ : Sort u_4} [sc : ] (f : αβγ) (h : ((fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) fun (x1 x2 : γ) => x1 x2) f f) (x : α) (y : β) :
Quotient.map₂ f h x y = f x y
instance Quotient.lift.decidablePred {α : Sort u_1} [sa : ] (f : αProp) (h : ∀ (a b : α), a bf a = f b) [] :
Equations
instance Quotient.lift₂.decidablePred {α : Sort u_1} {β : Sort u_2} [sa : ] [sb : ] (f : αβProp) (h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂f a₁ b₁ = f a₂ b₂) [hf : (a : α) → DecidablePred (f a)] (q₁ : Quotient sa) :

Note that this provides DecidableRel (Quotient.lift₂ f h) when α = β.

Equations
instance Quotient.instDecidableLiftOnOfDecidablePred_mathlib {α : Sort u_1} [sa : ] (q : Quotient sa) (f : αProp) (h : ∀ (a b : α), a bf a = f b) [] :
Decidable (q.liftOn f h)
Equations
• q.instDecidableLiftOnOfDecidablePred_mathlib f h =
instance Quotient.instDecidableLiftOn₂OfDecidablePred_mathlib {α : Sort u_1} {β : Sort u_2} [sa : ] [sb : ] (q₁ : Quotient sa) (q₂ : Quotient sb) (f : αβProp) (h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂f a₁ b₁ = f a₂ b₂) [(a : α) → DecidablePred (f a)] :
Decidable (q₁.liftOn₂ q₂ f h)
Equations
• q₁.instDecidableLiftOn₂OfDecidablePred_mathlib q₂ f h =
theorem Quot.eq {α : Type u_3} {r : ααProp} {x : α} {y : α} :
Quot.mk r x = Quot.mk r y
@[simp]
theorem Quotient.eq {α : Sort u_1} [r : ] {x : α} {y : α} :
x = y x y
theorem Quotient.forall {α : Sort u_3} {s : } {p : Prop} :
(∀ (a : ), p a) ∀ (a : α), p a
theorem Quotient.exists {α : Sort u_3} {s : } {p : Prop} :
(∃ (a : ), p a) ∃ (a : α), p a
@[simp]
theorem Quotient.lift_mk {α : Sort u_1} {β : Sort u_2} [s : ] (f : αβ) (h : ∀ (a b : α), a bf a = f b) (x : α) :
Quotient.lift f h x = f x
@[simp]
theorem Quotient.lift_comp_mk {α : Sort u_1} {β : Sort u_2} [] (f : αβ) (h : ∀ (a b : α), a bf a = f b) :
Quotient.mk inst✝ = f
@[simp]
theorem Quotient.lift₂_mk {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} [] [] (f : αβγ) (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ b₁a₂ b₂f a₁ a₂ = f b₁ b₂) (a : α) (b : β) :
Quotient.lift₂ f h a b = f a b
theorem Quotient.liftOn_mk {α : Sort u_1} {β : Sort u_2} [s : ] (f : αβ) (h : ∀ (a b : α), a bf a = f b) (x : α) :
x.liftOn f h = f x
@[simp]
theorem Quotient.liftOn₂_mk {α : Sort u_3} {β : Sort u_4} [] (f : ααβ) (h : ∀ (a₁ a₂ b₁ b₂ : α), a₁ b₁a₂ b₂f a₁ a₂ = f b₁ b₂) (x : α) (y : α) :
x.liftOn₂ y f h = f x y
theorem surjective_quot_mk {α : Sort u_1} (r : ααProp) :

Quot.mk r is a surjective function.

theorem surjective_quotient_mk {α : Sort u_3} (s : ) :

Quotient.mk is a surjective function.

theorem surjective_quotient_mk' (α : Sort u_3) [s : ] :
Function.Surjective Quotient.mk'

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
• q.out =
Instances For
unsafe 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.

Instances For
@[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 : ] :
α

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

Equations
• Quotient.out = Quot.out
Instances For
@[simp]
theorem Quotient.out_eq {α : Sort u_1} [s : ] (q : ) :
q.out = q
theorem Quotient.mk_out {α : Sort u_1} [] (a : α) :
a.out a
theorem Quotient.mk_eq_iff_out {α : Sort u_1} [s : ] {x : α} {y : } :
x = y x y.out
theorem Quotient.eq_mk_iff_out {α : Sort u_1} [s : ] {x : } {y : α} :
x = y x.out y
@[simp]
theorem Quotient.out_equiv_out {α : Sort u_1} {s : } {x : } {y : } :
x.out y.out x = y
theorem Quotient.out_injective {α : Sort u_1} {s : } :
Function.Injective Quotient.out
@[simp]
theorem Quotient.out_inj {α : Sort u_1} {s : } {x : } {y : } :
x.out = y.out x = y
instance piSetoid {ι : Sort u_3} {α : ιSort u_4} [(i : ι) → Setoid (α i)] :
Setoid ((i : ι) → α i)
Equations
• piSetoid = { r := fun (a b : (i : ι) → α i) => ∀ (i : ι), a i b i, iseqv := }
noncomputable def Quotient.choice {ι : Type u_3} {α : ιType u_4} [S : (i : ι) → Setoid (α i)] (f : (i : ι) → Quotient (S i)) :
Quotient inferInstance

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
• = fun (i : ι) => (f i).out
Instances For
@[simp]
theorem Quotient.choice_eq {ι : Type u_3} {α : ιType u_4} [(i : ι) → Setoid (α i)] (f : (i : ι) → α i) :
(Quotient.choice fun (i : ι) => f i) = f
theorem Quotient.induction_on_pi {ι : Type u_3} {α : ιSort u_4} [s : (i : ι) → Setoid (α i)] {p : ((i : ι) → Quotient (s i))Prop} (f : (i : ι) → Quotient (s i)) (h : ∀ (a : (i : ι) → α i), p fun (i : ι) => a i) :
p f
theorem nonempty_quotient_iff {α : Sort u_1} (s : ) :

### Truncation #

theorem true_equivalence {α : Sort u_1} :
Equivalence fun (x x : α) => True
def trueSetoid {α : Sort u_1} :

Always-true relation as a Setoid.

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

Equations
• trueSetoid = { r := fun (x x : α) => True, iseqv := }
Instances For
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
def Trunc.mk {α : Sort u_1} (a : α) :

Constructor for Trunc α

Equations
Instances For
instance Trunc.instInhabited {α : Sort u_1} [] :
Equations
• Trunc.instInhabited = { default := Trunc.mk default }
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
Instances For
theorem Trunc.ind {α : Sort u_1} {β : Prop} :
(∀ (a : α), β (Trunc.mk a))∀ (q : ), β q
theorem Trunc.lift_mk {α : Sort u_1} {β : Sort u_2} (f : αβ) (c : ∀ (a b : α), f a = f b) (a : α) :
Trunc.lift f c (Trunc.mk a) = f a
def Trunc.liftOn {α : Sort u_1} {β : Sort u_2} (q : ) (f : αβ) (c : ∀ (a b : α), f a = f b) :
β

Lift a constant function on q : Trunc α.

Equations
Instances For
theorem Trunc.induction_on {α : Sort u_1} {β : Prop} (q : ) (h : ∀ (a : α), β (Trunc.mk a)) :
β q
theorem Trunc.exists_rep {α : Sort u_1} (q : ) :
∃ (a : α), = q
theorem Trunc.induction_on₂ {α : Sort u_1} {β : Sort u_2} {C : Prop} (q₁ : ) (q₂ : ) (h : ∀ (a : α) (b : β), C (Trunc.mk a) (Trunc.mk b)) :
C q₁ q₂
theorem Trunc.eq {α : Sort u_1} (a : ) (b : ) :
a = b
instance Trunc.instSubsingletonTrunc {α : Sort u_1} :
Equations
• =
def Trunc.bind {α : Sort u_1} {β : Sort u_2} (q : ) (f : α) :

The bind operator for the Trunc monad.

Equations
• q.bind f = q.liftOn f
Instances For
def Trunc.map {α : Sort u_1} {β : Sort u_2} (f : αβ) (q : ) :

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

Equations
• = q.bind (Trunc.mk f)
Instances For
Equations
Equations
def Trunc.rec {α : Sort u_1} {C : Sort u_3} (f : (a : α) → C (Trunc.mk a)) (h : ∀ (a b : α), f a = f b) (q : ) :
C q

Recursion/induction principle for Trunc.

Equations
Instances For
def Trunc.recOn {α : Sort u_1} {C : Sort u_3} (q : ) (f : (a : α) → C (Trunc.mk a)) (h : ∀ (a b : α), f a = f b) :
C q

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

Equations
Instances For
def Trunc.recOnSubsingleton {α : Sort u_1} {C : Sort u_3} [∀ (a : α), Subsingleton (C (Trunc.mk a))] (q : ) (f : (a : α) → C (Trunc.mk a)) :
C q

A version of Trunc.recOn assuming the codomain is a Subsingleton.

Equations
Instances For
noncomputable def Trunc.out {α : Sort u_1} :
α

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

Equations
• Trunc.out = Quot.out
Instances For
@[simp]
theorem Trunc.out_eq {α : Sort u_1} (q : ) :
Trunc.mk q.out = q
theorem Trunc.nonempty {α : Sort u_1} (q : ) :

### 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.

def Quotient.mk'' {α : Sort u_1} {s₁ : } (a : α) :

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

Equations
Instances For
theorem Quotient.surjective_Quotient_mk'' {α : Sort u_1} {s₁ : } :
Function.Surjective Quotient.mk''

Quotient.mk'' is a surjective function.

def Quotient.liftOn' {α : Sort u_1} {φ : Sort u_4} {s₁ : } (q : Quotient s₁) (f : αφ) (h : ∀ (a b : α), Setoid.r a bf a = f b) :
φ

A version of Quotient.liftOn taking {s : Setoid α} as an implicit argument instead of an instance argument.

Equations
• q.liftOn' f h = q.liftOn f h
Instances For
@[simp]
theorem Quotient.liftOn'_mk'' {α : Sort u_1} {φ : Sort u_4} {s₁ : } (f : αφ) (h : ∀ (a b : α), Setoid.r a bf a = f b) (x : α) :
.liftOn' f h = f x
@[simp]
theorem Quotient.surjective_liftOn' {α : Sort u_1} {φ : Sort u_4} {s₁ : } {f : αφ} (h : ∀ (a b : α), Setoid.r a bf a = f b) :
(Function.Surjective fun (x : Quotient s₁) => x.liftOn' f h)
def Quotient.liftOn₂' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : } {s₂ : } (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.liftOn₂ taking {s₁ : Setoid α} {s₂ : Setoid β} as implicit arguments instead of instance arguments.

Equations
• q₁.liftOn₂' q₂ f h = q₁.liftOn₂ q₂ f h
Instances For
@[simp]
theorem Quotient.liftOn₂'_mk'' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : } {s₂ : } (f : αβγ) (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), Setoid.r a₁ b₁Setoid.r a₂ b₂f a₁ a₂ = f b₁ b₂) (a : α) (b : β) :
.liftOn₂' f h = f a b
theorem Quotient.ind' {α : Sort u_1} {s₁ : } {p : Quotient s₁Prop} (h : ∀ (a : α), p ) (q : Quotient s₁) :
p q

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

theorem Quotient.ind₂' {α : Sort u_1} {β : Sort u_2} {s₁ : } {s₂ : } {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.

theorem Quotient.inductionOn' {α : Sort u_1} {s₁ : } {p : Quotient s₁Prop} (q : Quotient s₁) (h : ∀ (a : α), p ) :
p q

A version of Quotient.inductionOn taking {s : Setoid α} as an implicit argument instead of an instance argument.

theorem Quotient.inductionOn₂' {α : Sort u_1} {β : Sort u_2} {s₁ : } {s₂ : } {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.inductionOn₂ taking {s₁ : Setoid α} {s₂ : Setoid β} as implicit arguments instead of instance arguments.

theorem Quotient.inductionOn₃' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : } {s₂ : } {s₃ : } {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.inductionOn₃ taking {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid γ} as implicit arguments instead of instance arguments.

def Quotient.recOnSubsingleton' {α : Sort u_1} {s₁ : } {φ : Quotient s₁Sort u_5} [∀ (a : α), Subsingleton (φ a)] (q : Quotient s₁) (f : (a : α) → φ ) :
φ q

A version of Quotient.recOnSubsingleton taking {s₁ : Setoid α} as an implicit argument instead of an instance argument.

Equations
• q.recOnSubsingleton' f =
Instances For
def Quotient.recOnSubsingleton₂' {α : Sort u_1} {β : Sort u_2} {s₁ : } {s₂ : } {φ : Quotient s₁Quotient s₂Sort u_5} [∀ (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.recOnSubsingleton₂ taking {s₁ : Setoid α} {s₂ : Setoid α} as implicit arguments instead of instance arguments.

Equations
• q₁.recOnSubsingleton₂' q₂ f =
Instances For
def Quotient.hrecOn' {α : Sort u_1} {s₁ : } {φ : Quotient s₁Sort u_5} (qa : Quotient s₁) (f : (a : α) → φ ) (c : ∀ (a₁ a₂ : α), a₁ a₂HEq (f a₁) (f a₂)) :
φ qa

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

Equations
Instances For
@[simp]
theorem Quotient.hrecOn'_mk'' {α : Sort u_1} {s₁ : } {φ : Quotient s₁Sort u_5} (f : (a : α) → φ ) (c : ∀ (a₁ a₂ : α), a₁ a₂HEq (f a₁) (f a₂)) (x : α) :
.hrecOn' f c = f x
def Quotient.hrecOn₂' {α : Sort u_1} {β : Sort u_2} {s₁ : } {s₂ : } {φ : Quotient s₁Quotient s₂Sort u_5} (qa : Quotient s₁) (qb : Quotient s₂) (f : (a : α) → (b : β) → φ ) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂HEq (f a₁ b₁) (f a₂ b₂)) :
φ qa qb

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

Equations
• qa.hrecOn₂' qb f c = qa.hrecOn₂ qb f c
Instances For
@[simp]
theorem Quotient.hrecOn₂'_mk'' {α : Sort u_1} {β : Sort u_2} {s₁ : } {s₂ : } {φ : Quotient s₁Quotient s₂Sort u_5} (f : (a : α) → (b : β) → φ ) (c : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ a₂b₁ b₂HEq (f a₁ b₁) (f a₂ b₂)) (x : α) (qb : Quotient s₂) :
.hrecOn₂' qb f c = qb.hrecOn' (f x)
def Quotient.map' {α : Sort u_1} {β : Sort u_2} {s₁ : } {s₂ : } (f : αβ) (h : (Setoid.r Setoid.r) f f) :
Quotient s₁Quotient s₂

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
Instances For
@[simp]
theorem Quotient.map'_mk'' {α : Sort u_1} {β : Sort u_2} {s₁ : } {s₂ : } (f : αβ) (h : (Setoid.r Setoid.r) f f) (x : α) :
def Quotient.map₂' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : } {s₂ : } {s₃ : } (f : αβγ) (h : (Setoid.r Setoid.r Setoid.r) f f) :
Quotient s₁Quotient s₂Quotient s₃

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

Equations
Instances For
@[simp]
theorem Quotient.map₂'_mk'' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : } {s₂ : } {s₃ : } (f : αβγ) (h : (Setoid.r Setoid.r Setoid.r) f f) (x : α) :
= Quotient.map' (f x)
theorem Quotient.exact' {α : Sort u_1} {s₁ : } {a : α} {b : α} :
Setoid.r a b
theorem Quotient.sound' {α : Sort u_1} {s₁ : } {a : α} {b : α} :
Setoid.r a b
@[simp]
theorem Quotient.eq' {α : Sort u_1} [s₁ : ] {a : α} {b : α} :
@[simp]
theorem Quotient.eq'' {α : Sort u_1} {s₁ : } {a : α} {b : α} :
noncomputable def Quotient.out' {α : Sort u_1} {s₁ : } (a : Quotient s₁) :
α

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

Equations
• a.out' = a.out
Instances For
@[simp]
theorem Quotient.out_eq' {α : Sort u_1} {s₁ : } (q : Quotient s₁) :
Quotient.mk'' q.out' = q
theorem Quotient.mk_out' {α : Sort u_1} {s₁ : } (a : α) :
Setoid.r .out' a
theorem Quotient.mk''_eq_mk {α : Sort u_1} [s : ] :
Quotient.mk'' =
@[simp]
theorem Quotient.liftOn'_mk {α : Sort u_1} {β : Sort u_2} [s : ] (x : α) (f : αβ) (h : ∀ (a b : α), Setoid.r a bf a = f b) :
x.liftOn' f h = f x
@[simp]
theorem Quotient.liftOn₂'_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [s : ] [t : ] (f : αβγ) (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), Setoid.r a₁ b₁Setoid.r a₂ b₂f a₁ a₂ = f b₁ b₂) (a : α) (b : β) :
a.liftOn₂' b f h = f a b
@[simp]
theorem Quotient.map'_mk {α : Sort u_1} {β : Sort u_2} [s : ] [t : ] (f : αβ) (h : (Setoid.r Setoid.r) f f) (x : α) :
Quotient.map' f h x = f x
instance Quotient.instDecidableLiftOn'OfDecidablePred {α : Sort u_1} {s₁ : } (q : Quotient s₁) (f : αProp) (h : ∀ (a b : α), Setoid.r a bf a = f b) [] :
Decidable (q.liftOn' f h)
Equations
• q.instDecidableLiftOn'OfDecidablePred f h =
instance Quotient.instDecidableLiftOn₂'OfDecidablePred {α : Sort u_1} {β : Sort u_2} {s₁ : } {s₂ : } (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 : α) → DecidablePred (f a)] :
Decidable (q₁.liftOn₂' q₂ f h)
Equations
• q₁.instDecidableLiftOn₂'OfDecidablePred q₂ f h =
@[simp]
theorem Equivalence.quot_mk_eq_iff {α : Type u_3} {r : ααProp} (h : ) (x : α) (y : α) :
Quot.mk r x = Quot.mk r y r x y