data.quot - mathlib docs

source

theorem setoid.ext {α : Sort u_1} {s t : setoid α} :

(∀ (a b : α), setoid.r a b ↔ setoid.r a b) → s = t

source

@[protected, instance]

def quot.inhabited {α : Sort u_1} {ra : α → α → Prop} [inhabited α] :

inhabited (quot ra)

Equations

quot.inhabited = {default := quot.mk ra (default α)}

source

@[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

qa.hrec_on₂ qb f ca cb = qa.hrec_on (λ (a : α), qb.hrec_on (f a) _) _

source

@[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

quot.map f h = quot.lift (λ (x : α), quot.mk rb (f x)) _

source

@[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

quot.map_right h = quot.map id h

source

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

Equations

quot.factor r s h = quot.lift (quot.mk s) _

source

theorem quot.factor_mk_eq {α : Type u_1} (r s : α → α → Prop) (h : ∀ (x y : α), r x y → s x y) :

quot.factor r s h ∘ quot.mk r = quot.mk s

source

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.

source

@[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

source

@[protected]

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

quot.lift₂ f hr hs q₁ q₂ = quot.lift (λ (a : α), quot.lift (f a) _) _ q₁ q₂

source

@[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

source

@[protected]

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

p.lift_on₂ q f hr hs = quot.lift₂ f hr hs p q

source

@[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

source

@[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

quot.map₂ f hr hs q₁ q₂ = quot.lift₂ (λ (a : α) (b : β), quot.mk t (f a b)) _ _ q₁ q₂

source

@[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)

source

@[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₂

source

@[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₃

source

@[protected, instance]

def quotient.inhabited {α : Sort u_1} [sa : setoid α] [inhabited α] :

inhabited (quotient sa)

Equations

quotient.inhabited = {default := ⟦default α⟧}

source

@[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

qa.hrec_on₂ qb f c = quot.hrec_on₂ qa qb f _ _

source

@[protected]

def quotient.map {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] (f : α → β) (h : (has_equiv.equiv ⇒ has_equiv.equiv) f f) :

quotient sa → quotient 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

quotient.map f h = quot.map f h

source

@[simp]

theorem quotient.map_mk {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] (f : α → β) (h : (has_equiv.equiv ⇒ has_equiv.equiv) f f) (x : α) :

quotient.map f h ⟦x⟧ = ⟦f x⟧

source

@[protected]

def quotient.map₂ {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] {γ : Sort u_4} [sc : setoid γ] (f : α → β → γ) (h : (has_equiv.equiv ⇒ has_equiv.equiv ⇒ has_equiv.equiv) f f) :

quotient sa → quotient sb → quotient 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

quotient.map₂ f h = quotient.lift₂ (λ (x : α) (y : β), ⟦f x y⟧) _

source

@[simp]

theorem quotient.map₂_mk {α : Sort u_1} {β : Sort u_2} [sa : setoid α] [sb : setoid β] {γ : Sort u_4} [sc : setoid γ] (f : α → β → γ) (h : (has_equiv.equiv ⇒ has_equiv.equiv ⇒ has_equiv.equiv) f f) (x : α) (y : β) :

quotient.map₂ f h ⟦x⟧ ⟦y⟧ = ⟦f x y⟧

source

theorem quot.eq {α : Type u_1} {r : α → α → Prop} {x y : α} :

quot.mk r x = quot.mk r y ↔ eqv_gen r x y

source

@[simp]

theorem quotient.eq {α : Sort u_1} [r : setoid α] {x y : α} :

⟦x⟧ = ⟦y⟧ ↔ x ≈ y

source

theorem forall_quotient_iff {α : Type u_1} [r : setoid α] {p : quotient r → Prop} :

(∀ (a : quotient r), p a) ↔ ∀ (a : α), p ⟦a⟧

source

@[simp]

theorem quotient.lift_mk {α : Sort u_1} {β : Sort u_2} [s : setoid α] (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b) (x : α) :

quotient.lift f h ⟦x⟧ = f x

source

@[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 : β) :

quotient.lift₂ f h ⟦a⟧ ⟦b⟧ = f a b

source

@[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

source

@[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 : α) :

⟦x⟧.lift_on₂ ⟦y⟧ f h = f x y

source

theorem surjective_quot_mk {α : Sort u_1} (r : α → α → Prop) :

function.surjective (quot.mk r)

quot.mk r is a surjective function.

source

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

function.surjective quotient.mk

quotient.mk is a surjective function.

source

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 = classical.some _

source

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.

source

@[simp]

theorem quot.out_eq {α : Sort u_1} {r : α → α → Prop} (q : quot r) :

quot.mk r q.out = q

source

noncomputable def quotient.out {α : Sort u_1} [s : setoid α] :

quotient s → α

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

Equations

quotient.out = quot.out

source

@[simp]

theorem quotient.out_eq {α : Sort u_1} [s : setoid α] (q : quotient s) :

⟦q.out ⟧ = q

source

theorem quotient.mk_out {α : Sort u_1} [s : setoid α] (a : α) :

⟦a⟧.out ≈ a

source

theorem quotient.mk_eq_iff_out {α : Sort u_1} [s : setoid α] {x : α} {y : quotient s} :

⟦x⟧ = y ↔ x ≈ y.out

source

theorem quotient.eq_mk_iff_out {α : Sort u_1} [s : setoid α] {x : quotient s} {y : α} :

x = ⟦y⟧ ↔ x.out ≈ y

source

@[simp]

theorem quotient.out_equiv_out {α : Sort u_1} [s : setoid α] {x y : quotient s} :

x.out ≈ y.out ↔ x = y

source

@[simp]

theorem quotient.out_inj {α : Sort u_1} [s : setoid α] {x y : quotient s} :

x.out = y.out ↔ x = y

source

@[protected, instance]

def pi_setoid {ι : Sort u_1} {α : ι → Sort u_2} [Π (i : ι), setoid (α i)] :

setoid (Π (i : ι), α i)

Equations

pi_setoid = {r := λ (a b : Π (i : ι), α i), ∀ (i : ι), a i ≈ b i, iseqv := _}

source

noncomputable def quotient.choice {ι : Type u_1} {α : ι → Type u_2} [S : Π (i : ι), setoid (α i)] (f : Π (i : ι), quotient (S i)) :

quotient pi_setoid

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

quotient.choice f = ⟦λ (i : ι), (f i).out⟧

source

theorem quotient.choice_eq {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), setoid (α i)] (f : Π (i : ι), α i) :

quotient.choice (λ (i : ι), ⟦f i⟧) = ⟦f⟧

source

theorem nonempty_quotient_iff {α : Sort u_1} (s : setoid α) :

nonempty (quotient s) ↔ nonempty α

source

def trunc (α : Sort u) :

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

trunc α = quot (λ (_x _x : α), true)

source

theorem true_equivalence {α : Sort u_1} :

equivalence (λ (_x _x : α), true)

source

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

trunc α

Constructor for trunc α

Equations

trunc.mk a = quot.mk (λ (_x _x : α), true) a

source

@[protected, instance]

def trunc.inhabited {α : Sort u_1} [inhabited α] :

inhabited (trunc α)

Equations

trunc.inhabited = {default := trunc.mk (default α)}

source

def trunc.lift {α : Sort u_1} {β : Sort u_2} (f : α → β) (c : ∀ (a b : α), f a = f b) :

trunc α → β

Any constant function lifts to a function out of the truncation

Equations

trunc.lift f c = quot.lift f _

source

theorem trunc.ind {α : Sort u_1} {β : trunc α → Prop} :

(∀ (a : α), β (trunc.mk a)) → ∀ (q : trunc α), β q

source

@[protected]

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

source

@[protected]

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

q.lift_on f c = trunc.lift f c q

source

@[protected]

theorem trunc.induction_on {α : Sort u_1} {β : trunc α → Prop} (q : trunc α) (h : ∀ (a : α), β (trunc.mk a)) :

β q

source

theorem trunc.exists_rep {α : Sort u_1} (q : trunc α) :

∃ (a : α), trunc.mk a = q

source

@[protected]

theorem trunc.induction_on₂ {α : Sort u_1} {β : Sort u_2} {C : trunc α → trunc β → Prop} (q₁ : trunc α) (q₂ : trunc β) (h : ∀ (a : α) (b : β), C (trunc.mk a) (trunc.mk b)) :

C q₁ q₂

source

@[protected]

theorem trunc.eq {α : Sort u_1} (a b : trunc α) :

a = b

source

@[protected, instance]

def trunc.subsingleton {α : Sort u_1} :

subsingleton (trunc α)

source

def trunc.bind {α : Sort u_1} {β : Sort u_2} (q : trunc α) (f : α → trunc β) :

trunc β

The bind operator for the trunc monad.

Equations

q.bind f = q.lift_on f _

source

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

trunc β

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

Equations

trunc.map f q = q.bind (trunc.mk ∘ f)

source

@[protected, instance]

def trunc.monad :

monad trunc

Equations

trunc.monad = monad.mk

source

@[protected, instance]

def trunc.is_lawful_monad :

is_lawful_monad trunc

source

@[protected]

def trunc.rec {α : Sort u_1} {C : trunc α → 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

trunc.rec f h q = quot.rec f _ q

source

@[protected]

def trunc.rec_on {α : Sort u_1} {C : trunc α → 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

q.rec_on f h = trunc.rec f h q

source

@[protected]

def trunc.rec_on_subsingleton {α : Sort u_1} {C : trunc α → 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.rec_on_subsingleton f = trunc.rec f _ q

source

noncomputable def trunc.out {α : Sort u_1} :

trunc α → α

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

Equations

trunc.out = quot.out

source

@[simp]

theorem trunc.out_eq {α : Sort u_1} (q : trunc α) :

trunc.mk q.out = q

source

@[protected]

theorem trunc.nonempty {α : Sort u_1} (q : trunc α) :

nonempty α

source

@[protected]

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

quotient s₁

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

Equations

quotient.mk' a = quot.mk setoid.r a

source

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

function.surjective quotient.mk'

quotient.mk' is a surjective function.

source

@[protected]

def quotient.lift_on' {α : Sort u_1} {φ : Sort u_4} {s₁ : setoid α} (q : quotient s₁) (f : α → φ) (h : ∀ (a b : α), setoid.r a b → f a = f b) :

φ

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

Equations

q.lift_on' f h = q.lift_on f h

source

@[protected, simp]

theorem quotient.lift_on'_mk' {α : Sort u_1} {φ : Sort u_4} {s₁ : setoid α} (f : α → φ) (h : ∀ (a b : α), setoid.r a b → f a = f b) (x : α) :

(quotient.mk' x).lift_on' f h = f x

source

@[protected]

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

q₁.lift_on₂' q₂ f h = q₁.lift_on₂ q₂ f h

source

@[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' a).lift_on₂' (quotient.mk' b) f h = f a b

source

@[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.

source

@[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.

source

@[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.

source

@[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.

source

@[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.

source

@[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

q.rec_on_subsingleton' f = q.rec_on_subsingleton f

source

@[protected]

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

q₁.rec_on_subsingleton₂' q₂ f = q₁.rec_on_subsingleton₂ q₂ f

source

@[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

qa.hrec_on' f c = quot.hrec_on qa f c

source

@[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

source

@[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

qa.hrec_on₂' qb f c = qa.hrec_on₂ qb f c

source

@[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₂) :

(quotient.mk' x).hrec_on₂' qb f c = qb.hrec_on' (f x) _

source

@[protected]

def quotient.map' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} (f : α → β) (h : (has_equiv.equiv ⇒ has_equiv.equiv) 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

quotient.map' f h = quot.map f h

source

@[simp]

theorem quotient.map'_mk' {α : Sort u_1} {β : Sort u_2} {s₁ : setoid α} {s₂ : setoid β} (f : α → β) (h : (has_equiv.equiv ⇒ has_equiv.equiv) f f) (x : α) :

quotient.map' f h (quotient.mk' x) = quotient.mk' (f x)

source

@[protected]

def quotient.map₂' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ} (f : α → β → γ) (h : (has_equiv.equiv ⇒ has_equiv.equiv ⇒ has_equiv.equiv) f f) :

quotient s₁ → quotient s₂ → quotient s₃

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

Equations

quotient.map₂' f h = quotient.map₂ f h

source

@[simp]

theorem quotient.map₂'_mk' {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ} (f : α → β → γ) (h : (has_equiv.equiv ⇒ has_equiv.equiv ⇒ has_equiv.equiv) f f) (x : α) :

quotient.map₂' f h (quotient.mk' x) = quotient.map' (f x) _

source