Mathlib.Data.Quot

Setoid.instCoeFunForallForallProp_mathlib instance

: CoeFun (Setoid α) (fun _ ↦ α → α → Prop)

Full source

/-- When writing a lemma about `someSetoid x y` (which uses this instance),
call it `someSetoid_apply` not `someSetoid_r`. -/
instance : CoeFun (Setoid α) (fun _ ↦ α → α → Prop) where
  coe := @Setoid.r _

Setoid as a Function

Informal description

For any type `α`, a setoid (equivalence relation) on `α` can be treated as a function from `α` to `α` to `Prop`, where the function represents the equivalence relation.

Setoid.ext theorem

{α : Sort*} : ∀ {s t : Setoid α}, (∀ a b, s a b ↔ t a b) → s = t

Full source

theorem ext {α : Sort*} : ∀ {s t : Setoid α}, (∀ a b, s a b ↔ t a b) → s = t
  | ⟨r, _⟩, ⟨p, _⟩, Eq =>
  by have : r = p := funext fun a ↦ funext fun b ↦ propext <| Eq a b
     subst this
     rfl

Extensionality of Equivalence Relations

Informal description

For any type `α` and any two equivalence relations `s` and `t` on `α`, if for all elements `a` and `b` in `α`, the relation `s(a, b)` holds if and only if `t(a, b)` holds, then `s` and `t` are equal as equivalence relations.

Quot.induction_on theorem

{α : Sort*} {r : α → α → Prop} {β : Quot r → Prop} (q : Quot r) (h : ∀ a, β (Quot.mk r a)) : β q

Full source

@[elab_as_elim]
protected theorem induction_on {α : Sort*} {r : α → α → Prop} {β : Quot r → Prop} (q : Quot r)
    (h : ∀ a, β (Quot.mk r a)) : β q :=
  ind h q

Induction Principle for Quotient Types

Informal description

Let $\alpha$ be a type and $r$ be a binary relation on $\alpha$. For any predicate $\beta$ on the quotient type $\text{Quot } r$ and any element $q$ of $\text{Quot } r$, if $\beta$ holds for the equivalence class of every element $a \in \alpha$, then $\beta$ holds for $q$.

Quot.instInhabited_mathlib instance

(r : α → α → Prop) [Inhabited α] : Inhabited (Quot r)

Full source

instance (r : α → α → Prop) [Inhabited α] : Inhabited (Quot r) :=
  ⟨⟦default⟧⟩

Inhabited Quotient of Inhabited Type

Informal description

For any type $\alpha$ with an inhabitant and any binary relation $r$ on $\alpha$, the quotient type $\mathrm{Quot}\,r$ is inhabited.

Quot.Subsingleton instance

[Subsingleton α] : Subsingleton (Quot ra)

Full source

protected instance Subsingleton [Subsingleton α] : Subsingleton (Quot ra) :=
  ⟨fun x ↦ Quot.induction_on x fun _ ↦ Quot.ind fun _ ↦ congr_arg _ (Subsingleton.elim _ _)⟩

Quotient of Subsingleton is Subsingleton

Informal description

For any type $\alpha$ that is a subsingleton (i.e., all elements are equal) and any binary relation $r$ on $\alpha$, the quotient type $\mathrm{Quot}\,r$ is also a subsingleton.

Quot.instUnique instance

[Unique α] : Unique (Quot ra)

Full source

instance [Unique α] : Unique (Quot ra) := Unique.mk' _

Quotient of Unique Type is Unique

Informal description

For any type $\alpha$ with a unique element and any binary relation $r$ on $\alpha$, the quotient type $\mathrm{Quot}\,r$ also has a unique element.

Quot.hrecOn₂ definition

 (qa : Quot ra) (qb : Quot rb) (f : ∀ a b, φ ⟦a⟧ ⟦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

Full source

/-- Recursion on two `Quotient` arguments `a` and `b`, result type depends on `⟦a⟧` and `⟦b⟧`. -/
protected def hrecOn₂ (qa : Quot ra) (qb : Quot rb) (f : ∀ a b, φ ⟦a⟧ ⟦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 :=
  Quot.hrecOn (motive := fun qa ↦ φ qa qb) qa
    (fun a ↦ Quot.hrecOn qb (f a) (fun _ _ pb ↦ cb pb))
    fun a₁ a₂ pa ↦
      Quot.induction_on qb fun b ↦
        have h₁ : HEq (@Quot.hrecOn _ _ (φ _) ⟦b⟧ (f a₁) (@cb _)) (f a₁ b) := by
          simp [heq_self_iff_true]
        have h₂ : HEq (f a₂ b) (@Quot.hrecOn _ _ (φ _) ⟦b⟧ (f a₂) (@cb _)) := by
          simp [heq_self_iff_true]
        (h₁.trans (ca pa)).trans h₂

Heterogeneous recursion on two quotient elements

Informal description

Given two quotient elements `qa : Quot ra` and `qb : Quot rb`, a function `f : ∀ a b, φ ⟦a⟧ ⟦b⟧` where `φ` depends on the equivalence classes of `a` and `b`, and compatibility conditions `ca` and `cb` ensuring that `f` respects the relations `ra` and `rb`, the function `Quot.hrecOn₂` constructs an element of type `φ qa qb`. More precisely: - For any `b`, the function `f` must respect `ra` in its first argument (condition `ca`) - For any `a`, the function `f` must respect `rb` in its second argument (condition `cb`)

Quot.map definition

(f : α → β) (h : ∀ ⦃a b : α⦄, ra a b → rb (f a) (f b)) : Quot ra → Quot rb

Full source

/-- Map a function `f : α → β` such that `ra x y` implies `rb (f x) (f y)`
to a map `Quot ra → Quot rb`. -/
protected def map (f : α → β) (h : ∀ ⦃a b : α⦄, ra a b → rb (f a) (f b)) : Quot ra → Quot rb :=
  Quot.lift (fun x => Quot.mk rb (f x)) fun _ _ hra ↦ Quot.sound <| h hra

Lifting a relation-preserving function to quotients

Informal description

Given a function $f : \alpha \to \beta$ and relations $r_a$ on $\alpha$ and $r_b$ on $\beta$, if $f$ preserves the relations (i.e., $r_a(x,y)$ implies $r_b(f(x), f(y))$ for all $x,y \in \alpha$), then $f$ induces a map $\text{Quot } r_a \to \text{Quot } r_b$ between the quotient types.

Quot.mapRight definition

{ra' : α → α → Prop} (h : ∀ a₁ a₂, ra a₁ a₂ → ra' a₁ a₂) : Quot ra → Quot ra'

Full source

/-- If `ra` is a subrelation of `ra'`, then we have a natural map `Quot ra → Quot ra'`. -/
protected def mapRight {ra' : α → α → Prop} (h : ∀ a₁ a₂, ra a₁ a₂ → ra' a₁ a₂) :
    Quot ra → Quot ra' :=
  Quot.map id h

Quotient map induced by relation inclusion

Informal description

Given a type $\alpha$ and two relations $r_a$ and $r_a'$ on $\alpha$, if $r_a$ is a subrelation of $r_a'$ (i.e., $r_a(x,y)$ implies $r_a'(x,y)$ for all $x,y \in \alpha$), then there exists a natural map $\text{Quot } r_a \to \text{Quot } r_a'$ that sends the equivalence class of $x$ under $r_a$ to its equivalence class under $r_a'$.

Quot.factor definition

{α : Type*} (r s : α → α → Prop) (h : ∀ x y, r x y → s x y) : Quot r → Quot s

Full source

/-- Weaken the relation of a quotient. This is the same as `Quot.map id`. -/
def factor {α : Type*} (r s : α → α → Prop) (h : ∀ x y, r x y → s x y) : Quot r → Quot s :=
  Quot.lift (Quot.mk s) fun x y rxy ↦ Quot.sound (h x y rxy)

Quotient relation weakening

Informal description

Given a type $\alpha$ and two relations $r, s$ on $\alpha$, if $r$ implies $s$ (i.e., $r(x,y) \to s(x,y)$ for all $x,y \in \alpha$), then there exists a function $\text{Quot } r \to \text{Quot } s$ that maps the equivalence class of $x$ under $r$ to its equivalence class under $s$.

Quot.factor_mk_eq theorem

{α : Type*} (r s : α → α → Prop) (h : ∀ x y, r x y → s x y) : factor r s h ∘ Quot.mk _ = Quot.mk _

Full source

theorem factor_mk_eq {α : Type*} (r s : α → α → Prop) (h : ∀ x y, r x y → s x y) :
    factorfactor r s h ∘ Quot.mk _ = Quot.mk _ :=
  rfl

Commutativity of Quotient Relation Weakening with Quotient Maps

Informal description

For any type $\alpha$ and two relations $r, s$ on $\alpha$, if $r$ implies $s$ (i.e., $r(x,y) \to s(x,y)$ for all $x,y \in \alpha$), then the composition of the quotient map $\text{Quot.mk}_r$ with the relation-weakening function $\text{factor}_{r,s,h}$ equals the quotient map $\text{Quot.mk}_s$. In other words, the following diagram commutes: $$\text{factor}_{r,s,h} \circ [\cdot]_r = [\cdot]_s$$ where $[\cdot]_r$ and $[\cdot]_s$ denote the quotient maps for relations $r$ and $s$ respectively.

Quot.lift_mk theorem

(f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) (a : α) : Quot.lift f h (Quot.mk r a) = f a

Full source

theorem lift_mk (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) (a : α) :
    Quot.lift f h (Quot.mk r a) = f a :=
  rfl

Lifting a Function to Quotient Preserves Values on Representatives

Informal description

Let $r$ be a binary relation on a type $\alpha$, and let $f : \alpha \to \gamma$ be a function that respects $r$ (i.e., for any $a_1, a_2 \in \alpha$, if $r(a_1, a_2)$ holds, then $f(a_1) = f(a_2)$). Then for any $a \in \alpha$, the function `Quot.lift f h` applied to the equivalence class of $a$ under $r$ (denoted `Quot.mk r a`) equals $f(a)$. In mathematical notation: $$\text{Quot.lift}\, f\, h\, ([a]_r) = f(a)$$ where $[a]_r$ denotes the equivalence class of $a$ under $r$.

Quot.liftOn_mk theorem

(a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) : Quot.liftOn (Quot.mk r a) f h = f a

Full source

theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
    Quot.liftOn (Quot.mk r a) f h = f a :=
  rfl

Quotient Lift-On Evaluation on Equivalence Class

Informal description

For any element $a$ of type $\alpha$, any function $f \colon \alpha \to \gamma$, and any relation $r$ on $\alpha$ such that $f$ respects $r$ (i.e., $r(a_1, a_2)$ implies $f(a_1) = f(a_2)$), the value of the quotient operation `Quot.liftOn` applied to the equivalence class of $a$ under $r$ with $f$ and $h$ is equal to $f(a)$. In other words, if $[a]_r$ denotes the equivalence class of $a$ under $r$, then $\text{Quot.liftOn}([a]_r, f, h) = f(a)$.

Quot.surjective_lift theorem

 {f : α → γ} (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) : Function.Surjective (lift f h) ↔ Function.Surjective f

Full source

@[simp] theorem surjective_lift {f : α → γ} (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
    Function.SurjectiveFunction.Surjective (lift f h) ↔ Function.Surjective f :=
  ⟨fun hf => hf.comp Quot.exists_rep, fun hf y => let ⟨x, hx⟩ := hf y; ⟨Quot.mk _ x, hx⟩⟩

Surjectivity of Lifted Function on Quotient Space

Informal description

Let $r$ be a binary relation on a type $\alpha$, and let $f \colon \alpha \to \gamma$ be a function that respects $r$ (i.e., $r(a_1, a_2)$ implies $f(a_1) = f(a_2)$). Then the lifted function $\text{lift}\, f\, h \colon \text{Quot}\, r \to \gamma$ is surjective if and only if $f$ is surjective.

Quot.lift₂ definition

 (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) : γ

Full source

/-- Descends a function `f : α → β → γ` to quotients of `α` and `β`. -/
protected def lift₂ (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) : γ :=
  Quot.lift (fun a ↦ Quot.lift (f a) (hr a))
    (fun a₁ a₂ ha ↦ funext fun q ↦ Quot.induction_on q fun b ↦ hs a₁ a₂ b ha) q₁ q₂

Lifting a binary function to quotients

Informal description

Given a function $f : \alpha \to \beta \to \gamma$ and equivalence relations $r$ on $\alpha$ and $s$ on $\beta$, the function `Quot.lift₂` descends $f$ to a function on the quotients $\text{Quot } r$ and $\text{Quot } s$. This requires that $f$ respects the relations in the following ways: 1. For fixed $a \in \alpha$, $f(a, \cdot)$ must respect $s$ (i.e., $s(b_1, b_2) \implies f(a, b_1) = f(a, b_2)$) 2. For fixed $b \in \beta$, $f(\cdot, b)$ must respect $r$ (i.e., $r(a_1, a_2) \implies f(a_1, b) = f(a_2, b)$) The resulting function takes $q_1 \in \text{Quot } r$ and $q_2 \in \text{Quot } s$ and returns an element of $\gamma$.

Quot.lift₂_mk theorem

 (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

Full source

@[simp]
theorem lift₂_mk (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 :=
  rfl

Lifted Binary Function on Quotients Evaluates as Original on Representatives

Informal description

Given a function $f : \alpha \to \beta \to \gamma$ and equivalence relations $r$ on $\alpha$ and $s$ on $\beta$, if $f$ respects these relations (i.e., for fixed $a \in \alpha$, $f(a, \cdot)$ respects $s$, and for fixed $b \in \beta$, $f(\cdot, b)$ respects $r$), then applying the lifted function $\text{Quot.lift}_2\, f$ to the equivalence classes $[a]_r$ and $[b]_s$ yields the same result as applying $f$ directly to $a$ and $b$. That is, $\text{Quot.lift}_2\, f\, \text{hr}\, \text{hs}\, [a]_r\, [b]_s = f\, a\, b$.

Quot.liftOn₂ definition

 (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) : γ

Full source

/-- Descends a function `f : α → β → γ` to quotients of `α` and `β` and applies it. -/
protected def liftOn₂ (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) : γ :=
  Quot.lift₂ f hr hs p q

Lifting a binary function to quotients with explicit arguments

Informal description

Given a function $f : \alpha \to \beta \to \gamma$ and equivalence relations $r$ on $\alpha$ and $s$ on $\beta$, the function `Quot.liftOn₂` applies $f$ to representatives of equivalence classes in the quotients $\text{Quot } r$ and $\text{Quot } s$. This requires that $f$ respects the relations in the following ways: 1. For fixed $a \in \alpha$, $f(a, \cdot)$ must respect $s$ (i.e., $s(b_1, b_2) \implies f(a, b_1) = f(a, b_2)$) 2. For fixed $b \in \beta$, $f(\cdot, b)$ must respect $r$ (i.e., $r(a_1, a_2) \implies f(a_1, b) = f(a_2, b)$) The function takes $p \in \text{Quot } r$, $q \in \text{Quot } s$, and the appropriate respectfulness conditions, and returns an element of $\gamma$.

Quot.liftOn₂_mk theorem

 (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.liftOn₂ (Quot.mk r a) (Quot.mk s b) f hr hs = f a b

Full source

@[simp]
theorem liftOn₂_mk (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.liftOn₂ (Quot.mk r a) (Quot.mk s b) f hr hs = f a b :=
  rfl

Lifted Binary Function on Quotient Representatives Equals Original Function

Informal description

Given a binary function $f : \alpha \to \beta \to \gamma$ and equivalence relations $r$ on $\alpha$ and $s$ on $\beta$, if $f$ respects these relations (i.e., for fixed $a \in \alpha$, $f(a, \cdot)$ respects $s$, and for fixed $b \in \beta$, $f(\cdot, b)$ respects $r$), then applying the lifted function $\text{Quot.liftOn}_2$ to the equivalence classes $[a]_r$ and $[b]_s$ yields the same result as applying $f$ directly to $a$ and $b$. That is, $\text{Quot.liftOn}_2\, [a]_r\, [b]_s\, f\, \text{hr}\, \text{hs} = f\, a\, b$.

Quot.map₂ definition

 (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

Full source

/-- Descends a function `f : α → β → γ` to quotients of `α` and `β` with values in a quotient of
`γ`. -/
protected def map₂ (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 :=
  Quot.lift₂ (fun a b ↦ Quot.mk t <| f a b) (fun a b₁ b₂ hb ↦ Quot.sound (hr a b₁ b₂ hb))
    (fun a₁ a₂ b ha ↦ Quot.sound (hs a₁ a₂ b ha)) q₁ q₂

Lifting a binary function to quotients with respect to equivalence relations

Informal description

Given a binary function $f : \alpha \to \beta \to \gamma$ and equivalence relations $r$ on $\alpha$, $s$ on $\beta$, and $t$ on $\gamma$, the function `Quot.map₂` lifts $f$ to a function that maps elements of the quotients $\text{Quot}\, r$ and $\text{Quot}\, s$ to the quotient $\text{Quot}\, t$. This requires that $f$ respects the relations in the following ways: 1. For fixed $a \in \alpha$, $f(a, \cdot)$ must map $s$-related elements to $t$-related elements (i.e., $s(b_1, b_2) \implies t(f(a, b_1), f(a, b_2))$) 2. For fixed $b \in \beta$, $f(\cdot, b)$ must map $r$-related elements to $t$-related elements (i.e., $r(a_1, a_2) \implies t(f(a_1, b), f(a_2, b))$) The resulting function takes $q_1 \in \text{Quot}\, r$ and $q_2 \in \text{Quot}\, s$ and returns an element of $\text{Quot}\, t$.

Quot.map₂_mk theorem

 (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)

Full source

@[simp]
theorem map₂_mk (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) :=
  rfl

Lifted Binary Function on Quotient Classes Equals Class of Function Values

Informal description

Given a binary function $f \colon \alpha \to \beta \to \gamma$ and equivalence relations $r$ on $\alpha$, $s$ on $\beta$, and $t$ on $\gamma$, suppose that: 1. For any fixed $a \in \alpha$, $f(a, \cdot)$ respects $s$ (i.e., $s(b_1, b_2) \implies t(f(a, b_1), f(a, b_2))$) 2. For any fixed $b \in \beta$, $f(\cdot, b)$ respects $r$ (i.e., $r(a_1, a_2) \implies t(f(a_1, b), f(a_2, b))$) Then for any $a \in \alpha$ and $b \in \beta$, the lifted function $\text{Quot.map}_2\, f\, \text{hr}\, \text{hs}$ applied to the equivalence classes $[a]_r$ and $[b]_s$ equals the equivalence class of $f(a, b)$ under $t$, i.e., \[ \text{Quot.map}_2\, f\, \text{hr}\, \text{hs}\, [a]_r\, [b]_s = [f(a, b)]_t. \]

Quot.recOnSubsingleton₂ definition

 {φ : Quot r → Quot s → Sort*} [h : ∀ a b, Subsingleton (φ ⟦a⟧ ⟦b⟧)] (q₁ : Quot r) (q₂ : Quot s)
  (f : ∀ a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂

Full source

/-- A binary version of `Quot.recOnSubsingleton`. -/
@[elab_as_elim]
protected def recOnSubsingleton₂ {φ : Quot r → Quot s → Sort*}
    [h : ∀ a b, Subsingleton (φ ⟦a⟧ ⟦b⟧)] (q₁ : Quot r)
    (q₂ : Quot s) (f : ∀ a b, φ ⟦a⟧ ⟦b⟧) : φ q₁ q₂ :=
  @Quot.recOnSubsingleton _ r (fun q ↦ φ q q₂)
    (fun a ↦ Quot.ind (β := fun b ↦ Subsingleton (φ (mk r a) b)) (h a) q₂) q₁
    fun a ↦ Quot.recOnSubsingleton q₂ fun b ↦ f a b

Binary recursion on subsingleton-valued quotient pairs

Informal description

Given a type-valued function $\varphi$ on pairs of quotient types $\text{Quot}\, r$ and $\text{Quot}\, s$, if $\varphi$ is subsingleton-valued on all pairs of equivalence classes (i.e., for any $a$ and $b$, the type $\varphi \llbracket a \rrbracket \llbracket b \rrbracket$ has at most one element), then we can define a function on $\text{Quot}\, r \times \text{Quot}\, s$ by specifying its values on representatives. Specifically, given $q_1 : \text{Quot}\, r$, $q_2 : \text{Quot}\, s$, and a function $f : \forall a\, b, \varphi \llbracket a \rrbracket \llbracket b \rrbracket$, the term $\text{Quot.recOnSubsingleton₂}\, q_1\, q_2\, f$ yields an element of $\varphi\, q_1\, q_2$.

Quot.induction_on₂ theorem

 {δ : Quot r → Quot s → Prop} (q₁ : Quot r) (q₂ : Quot s) (h : ∀ a b, δ (Quot.mk r a) (Quot.mk s b)) : δ q₁ q₂

Full source

@[elab_as_elim]
protected theorem induction_on₂ {δ : Quot r → Quot s → Prop} (q₁ : Quot r) (q₂ : Quot s)
    (h : ∀ a b, δ (Quot.mk r a) (Quot.mk s b)) : δ q₁ q₂ :=
  Quot.ind (β := fun a ↦ δ a q₂) (fun a₁ ↦ Quot.ind (fun a₂ ↦ h a₁ a₂) q₂) q₁

Induction Principle for Binary Quotient Predicates

Informal description

Let $r$ and $s$ be relations on types $\alpha$ and $\beta$ respectively, and let $\delta$ be a predicate on $\text{Quot } r \times \text{Quot } s$. Given two quotient elements $q_1 \in \text{Quot } r$ and $q_2 \in \text{Quot } s$, if $\delta$ holds for all representatives $a \in \alpha$ and $b \in \beta$ (i.e., $\delta([a]_r, [b]_s)$ holds), then $\delta(q_1, q_2)$ holds. Here, $\text{Quot } r$ denotes the quotient type of $\alpha$ by relation $r$, and $[a]_r$ denotes the equivalence class of $a$ under $r$.

Quot.induction_on₃ theorem

 {δ : 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₃

Full source

@[elab_as_elim]
protected theorem induction_on₃ {δ : 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₃ :=
  Quot.ind (β := fun a ↦ δ a q₂ q₃) (fun a₁ ↦ Quot.ind (β := fun b ↦ δ _ b q₃)
    (fun a₂ ↦ Quot.ind (fun a₃ ↦ h a₁ a₂ a₃) q₃) q₂) q₁

Triple Induction Principle for Quotient Types

Informal description

Let $r$, $s$, and $t$ be relations on types $\alpha$, $\beta$, and $\gamma$ respectively. For any predicate $\delta$ on the quotient types $\text{Quot } r \times \text{Quot } s \times \text{Quot } t$, if $\delta$ holds for all equivalence classes $\llbracket a \rrbracket_r$, $\llbracket b \rrbracket_s$, $\llbracket c \rrbracket_t$ (where $a \in \alpha$, $b \in \beta$, $c \in \gamma$), then $\delta$ holds for any three elements $q_1 \in \text{Quot } r$, $q_2 \in \text{Quot } s$, and $q_3 \in \text{Quot } t$.

Quot.lift.decidablePred instance

 (r : α → α → Prop) (f : α → Prop) (h : ∀ a b, r a b → f a = f b) [hf : DecidablePred f] : DecidablePred (Quot.lift f h)

Full source

instance lift.decidablePred (r : α → α → Prop) (f : α → Prop) (h : ∀ a b, r a b → f a = f b)
    [hf : DecidablePred f] :
    DecidablePred (Quot.lift f h) :=
  fun q ↦ Quot.recOnSubsingleton (motive := fun _ ↦ Decidable _) q hf

Decidability of Lifted Predicates on Quotients

Informal description

Given a type $\alpha$ with a relation $r$ and a decidable predicate $f$ on $\alpha$ that respects $r$ (i.e., $r(a,b)$ implies $f(a) = f(b)$), the lifted predicate $\text{Quot.lift}\,f\,h$ on the quotient $\text{Quot}\,r$ is also decidable.

Quot.lift₂.decidablePred instance

 (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) :
  DecidablePred (Quot.lift₂ f ha hb q₁)

Full source

/-- Note that this provides `DecidableRel (Quot.Lift₂ f ha hb)` when `α = β`. -/
instance lift₂.decidablePred (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) :
    DecidablePred (Quot.lift₂ f ha hb q₁) :=
  fun q₂ ↦ Quot.recOnSubsingleton₂ q₁ q₂ hf

Decidability of Binary Predicates Lifted to Quotients

Informal description

Given a type $\alpha$ with a relation $r$, a type $\beta$ with a relation $s$, and a decidable binary predicate $f : \alpha \to \beta \to \text{Prop}$ that respects $s$ in its second argument (i.e., $s(b_1, b_2) \implies f(a, b_1) = f(a, b_2)$) and $r$ in its first argument (i.e., $r(a_1, a_2) \implies f(a_1, b) = f(a_2, b)$), the lifted predicate $\text{Quot.lift₂}\,f\,ha\,hb\,q_1$ on the quotient $\text{Quot}\,s$ is decidable for any $q_1 \in \text{Quot}\,r$.

Quot.instDecidableLiftOnOfDecidablePred_mathlib instance

 (r : α → α → Prop) (q : Quot r) (f : α → Prop) (h : ∀ a b, r a b → f a = f b) [DecidablePred f] :
  Decidable (Quot.liftOn q f h)

Full source

instance (r : α → α → Prop) (q : Quot r) (f : α → Prop) (h : ∀ a b, r a b → f a = f b)
    [DecidablePred f] :
    Decidable (Quot.liftOn q f h) :=
  Quot.lift.decidablePred _ _ _ _

Decidability of Lifted Predicates on Quotients via LiftOn

Informal description

Given a type $\alpha$ with a relation $r$, a quotient $q$ of $\alpha$ by $r$, and a decidable predicate $f$ on $\alpha$ that respects $r$ (i.e., $r(a,b)$ implies $f(a) = f(b)$), the value of the lifted function $\text{Quot.liftOn}\,q\,f\,h$ is decidable.

Quot.instDecidableLiftOn₂OfDecidablePred instance

 (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 (Quot.liftOn₂ q₁ q₂ f ha hb)

Full source

instance (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 (Quot.liftOn₂ q₁ q₂ f ha hb) :=
  Quot.lift₂.decidablePred _ _ _ _ _ _ _

Decidability of Binary Functions Lifted to Quotients via `liftOn₂`

Informal description

Given a type $\alpha$ with a relation $r$, a type $\beta$ with a relation $s$, and a decidable binary predicate $f : \alpha \to \beta \to \text{Prop}$ that respects $s$ in its second argument (i.e., $s(b_1, b_2) \implies f(a, b_1) = f(a, b_2)$) and $r$ in its first argument (i.e., $r(a_1, a_2) \implies f(a_1, b) = f(a_2, b)$), the value of the lifted function $\text{Quot.liftOn₂}\,q_1\,q_2\,f\,ha\,hb$ is decidable for any $q_1 \in \text{Quot}\,r$ and $q_2 \in \text{Quot}\,s$.

Quotient.term⟦_⟧ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc Quotient.mk]
notation3:arg "⟦" a "⟧" => Quotient.mk _ a

Equivalence class notation

Informal description

The notation `⟦a⟧` represents the equivalence class of `a` under a given equivalence relation, where `a` is an element of the type being quotiented. This is a shorthand for `Quotient.mk _ a`, which constructs the equivalence class of `a` in the quotient type.

Quotient.term⟦_⟧.delab_app.Quotient.mk definition

: Delab✝

Full source

@[inherit_doc Quotient.mk]
notation3:arg "⟦" a "⟧" => Quotient.mk _ a

Quotient notation

Informal description

The notation `⟦a⟧` represents the canonical projection of element `a` into the quotient type defined by an implicit equivalence relation (setoid). This is syntactic sugar for `Quotient.mk _ a`.

Quotient.instInhabitedQuotient instance

(s : Setoid α) [Inhabited α] : Inhabited (Quotient s)

Full source

instance instInhabitedQuotient (s : Setoid α) [Inhabited α] : Inhabited (Quotient s) :=
  ⟨⟦default⟧⟩

Inhabited Quotient from Inhabited Type

Informal description

For any type $\alpha$ with an equivalence relation $s$ and an inhabitant, the quotient type $\alpha/s$ is also inhabited.

Quotient.instSubsingletonQuotient instance

(s : Setoid α) [Subsingleton α] : Subsingleton (Quotient s)

Full source

instance instSubsingletonQuotient (s : Setoid α) [Subsingleton α] : Subsingleton (Quotient s) :=
  Quot.Subsingleton

Quotient of Subsingleton is Subsingleton

Informal description

For any type $\alpha$ that is a subsingleton (i.e., all elements are equal) and any equivalence relation $s$ on $\alpha$, the quotient type $\alpha/s$ is also a subsingleton.

Quotient.instUniqueQuotient instance

(s : Setoid α) [Unique α] : Unique (Quotient s)

Full source

instance instUniqueQuotient (s : Setoid α) [Unique α] : Unique (Quotient s) := Unique.mk' _

Quotient of Unique Type is Unique

Informal description

For any type $\alpha$ with a unique element and any equivalence relation $s$ on $\alpha$, the quotient type $\alpha/s$ also has a unique element.

Quotient.instIsEquivEquiv instance

{α : Type*} [Setoid α] : IsEquiv α (· ≈ ·)

Full source

instance {α : Type*} [Setoid α] : IsEquiv α (· ≈ ·) where
  refl := Setoid.refl
  symm _ _ := Setoid.symm
  trans _ _ _ := Setoid.trans

Setoid Relations are Equivalence Relations

Informal description

For any type $\alpha$ equipped with a setoid structure (i.e., an equivalence relation $\approx$), the relation $\approx$ is an equivalence relation on $\alpha$.

Quotient.hrecOn₂ definition

 (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

Full source

/-- Induction on two `Quotient` arguments `a` and `b`, result type depends on `⟦a⟧` and `⟦b⟧`. -/
protected def hrecOn₂ (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 :=
  Quot.hrecOn₂ qa qb f (fun p ↦ c _ _ _ _ p (Setoid.refl _)) fun p ↦ c _ _ _ _ (Setoid.refl _) p

Heterogeneous recursion on two quotient elements respecting equivalence relations

Informal description

Given two quotient elements $qa$ and $qb$ with respect to setoids $sa$ and $sb$ respectively, a function $f$ that maps pairs of elements to a type $\phi$ depending on their equivalence classes, and a compatibility condition $c$ ensuring that $f$ respects the equivalence relations, the function $\text{Quotient.hrecOn₂}$ constructs an element of type $\phi(qa, qb)$. The compatibility condition requires that for any elements $a_1, a_2$ related by $sa$ and $b_1, b_2$ related by $sb$, the values $f(a_1, b_1)$ and $f(a_2, b_2)$ are heterogeneously equal.

Quotient.map definition

(f : α → β) (h : ∀ ⦃a b : α⦄, a ≈ b → f a ≈ f b) : Quotient sa → Quotient sb

Full source

/-- 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. -/
protected def map (f : α → β) (h : ∀ ⦃a b : α⦄, a ≈ b → f a ≈ f b) : Quotient sa → Quotient sb :=
  Quot.map f h

Lifting a relation-respecting function to quotient types

Informal description

Given a function $f : \alpha \to \beta$ that respects the equivalence relation $\approx$ on $\alpha$ (i.e., for any $a, b \in \alpha$, if $a \approx b$ then $f(a) \approx f(b)$), the function `Quotient.map` lifts $f$ to a function between the quotient types $\text{Quotient } s_a \to \text{Quotient } s_b$, where $s_a$ and $s_b$ are the setoids (equivalence relations) on $\alpha$ and $\beta$ respectively. This is useful for defining unary operations on quotient types.

Quotient.map_mk theorem

(f : α → β) (h) (x : α) : Quotient.map f h (⟦x⟧ : Quotient sa) = (⟦f x⟧ : Quotient sb)

Full source

@[simp]
theorem map_mk (f : α → β) (h) (x : α) :
    Quotient.map f h (⟦x⟧ : Quotient sa) = (⟦f x⟧ : Quotient sb) :=
  rfl

Lifting a Function to Quotients Preserves Equivalence Classes

Informal description

Given a function $f : \alpha \to \beta$ that respects the equivalence relation $\approx$ on $\alpha$ (i.e., for any $a, b \in \alpha$, if $a \approx b$ then $f(a) \approx f(b)$), and an element $x \in \alpha$, the application of the lifted function $\mathrm{Quotient.map}\, f\, h$ to the equivalence class $[x]$ equals the equivalence class of $f(x)$, i.e., \[ \mathrm{Quotient.map}\, f\, h\, [x] = [f(x)]. \]

Quotient.map₂ definition

 (f : α → β → γ) (h : ∀ ⦃a₁ a₂⦄, a₁ ≈ a₂ → ∀ ⦃b₁ b₂⦄, b₁ ≈ b₂ → f a₁ b₁ ≈ f a₂ b₂) :
  Quotient sa → Quotient sb → Quotient sc

Full source

/-- 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. -/
protected def map₂ (f : α → β → γ)
    (h : ∀ ⦃a₁ a₂⦄, a₁ ≈ a₂ → ∀ ⦃b₁ b₂⦄, b₁ ≈ b₂ → f a₁ b₁ ≈ f a₂ b₂) :
    Quotient sa → Quotient sb → Quotient sc :=
  Quotient.lift₂ (fun x y ↦ ⟦f x y⟧) fun _ _ _ _ h₁ h₂ ↦ Quot.sound <| h h₁ h₂

Lifting a binary operation to quotient types

Informal description

Given a function $f : \alpha \to \beta \to \gamma$ that respects equivalence relations on $\alpha$ and $\beta$ (i.e., if $a_1 \approx a_2$ and $b_1 \approx b_2$ then $f(a_1, b_1) \approx f(a_2, b_2)$), the function `Quotient.map₂` lifts $f$ to a function between quotient types $\text{Quotient } s_a \to \text{Quotient } s_b \to \text{Quotient } s_c$. This is useful for defining binary operations on quotient types.

Quotient.map₂_mk theorem

 (f : α → β → γ) (h) (x : α) (y : β) :
  Quotient.map₂ f h (⟦x⟧ : Quotient sa) (⟦y⟧ : Quotient sb) = (⟦f x y⟧ : Quotient sc)

Full source

@[simp]
theorem map₂_mk (f : α → β → γ) (h) (x : α) (y : β) :
    Quotient.map₂ f h (⟦x⟧ : Quotient sa) (⟦y⟧ : Quotient sb) = (⟦f x y⟧ : Quotient sc) :=
  rfl

Lifting a Binary Operation to Quotients Preserves Equivalence Classes

Informal description

Given a function $f : \alpha \to \beta \to \gamma$ that respects equivalence relations $\approx$ on $\alpha$ and $\beta$ (i.e., $a_1 \approx a_2$ and $b_1 \approx b_2$ implies $f(a_1, b_1) \approx f(a_2, b_2)$), then for any elements $x \in \alpha$ and $y \in \beta$, the application of the lifted function $\mathrm{Quotient.map}_2\, f\, h$ to the equivalence classes $[x]$ and $[y]$ equals the equivalence class of $f(x, y)$, i.e., \[ \mathrm{Quotient.map}_2\, f\, h\, [x]\, [y] = [f(x, y)]. \]

Quotient.lift.decidablePred instance

(f : α → Prop) (h : ∀ a b, a ≈ b → f a = f b) [DecidablePred f] : DecidablePred (Quotient.lift f h)

Full source

instance lift.decidablePred (f : α → Prop) (h : ∀ a b, a ≈ b → f a = f b) [DecidablePred f] :
    DecidablePred (Quotient.lift f h) :=
  Quot.lift.decidablePred _ _ _

Decidability of Lifted Predicates on Quotients

Informal description

For any type $\alpha$ with an equivalence relation $\approx$, if a predicate $f : \alpha \to \mathrm{Prop}$ is decidable and respects $\approx$ (i.e., $a \approx b$ implies $f(a) = f(b)$), then the lifted predicate $\mathrm{Quotient.lift}\,f\,h$ on the quotient $\alpha/{\approx}$ is also decidable.

Quotient.lift₂.decidablePred instance

 (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) : DecidablePred (Quotient.lift₂ f h q₁)

Full source

/-- Note that this provides `DecidableRel (Quotient.lift₂ f h)` when `α = β`. -/
instance lift₂.decidablePred (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) : DecidablePred (Quotient.lift₂ f h q₁) :=
  fun q₂ ↦ Quotient.recOnSubsingleton₂ q₁ q₂ hf

Decidability of Lifted Binary Predicates on Quotients

Informal description

For any function $f : \alpha \to \beta \to \mathrm{Prop}$ that respects the equivalence relations on $\alpha$ and $\beta$ (i.e., $f a_1 b_1 = f a_2 b_2$ whenever $a_1 \approx a_2$ and $b_1 \approx b_2$), if for every $a \in \alpha$ the predicate $f(a, \cdot)$ is decidable, then the lifted function $\mathrm{Quotient.lift}_2\, f\, h$ is also decidable on the quotient type $\mathrm{Quotient}\, s_a$.

Quotient.instDecidableLiftOnOfDecidablePred_mathlib instance

 (q : Quotient sa) (f : α → Prop) (h : ∀ a b, a ≈ b → f a = f b) [DecidablePred f] : Decidable (Quotient.liftOn q f h)

Full source

instance (q : Quotient sa) (f : α → Prop) (h : ∀ a b, a ≈ b → f a = f b) [DecidablePred f] :
    Decidable (Quotient.liftOn q f h) :=
  Quotient.lift.decidablePred _ _ _

Decidability of Lifted Predicates on Quotient Types

Informal description

For any quotient type $\alpha/{\approx}$ and decidable predicate $f : \alpha \to \mathrm{Prop}$ that respects the equivalence relation $\approx$, the lifted predicate $\mathrm{Quotient.liftOn}\,q\,f\,h$ on the quotient is also decidable.

Quotient.instDecidableLiftOn₂OfDecidablePred_mathlib instance

 (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 (Quotient.liftOn₂ q₁ q₂ f h)

Full source

instance (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 (Quotient.liftOn₂ q₁ q₂ f h) :=
  Quotient.lift₂.decidablePred _ _ _ _

Decidability of Lifted Binary Predicates on Quotient Types

Informal description

For any two quotient types $\mathrm{Quotient}\, s_a$ and $\mathrm{Quotient}\, s_b$, and any binary predicate $f : \alpha \to \beta \to \mathrm{Prop}$ that respects the equivalence relations on $\alpha$ and $\beta$ (i.e., $f a_1 b_1 = f a_2 b_2$ whenever $a_1 \approx a_2$ and $b_1 \approx b_2$), if for every $a \in \alpha$ the predicate $f(a, \cdot)$ is decidable, then the lifted function $\mathrm{Quotient.liftOn}_2\, q_1\, q_2\, f\, h$ is decidable.

Quot.eq theorem

{α : Type*} {r : α → α → Prop} {x y : α} : Quot.mk r x = Quot.mk r y ↔ Relation.EqvGen r x y

Full source

theorem Quot.eq {α : Type*} {r : α → α → Prop} {x y : α} :
    Quot.mkQuot.mk r x = Quot.mk r y ↔ Relation.EqvGen r x y :=
  ⟨Quot.eqvGen_exact, Quot.eqvGen_sound⟩

Equivalence of Quotient Equality and Equivalence Closure

Informal description

For any type $\alpha$ and relation $r$ on $\alpha$, the equivalence classes of elements $x$ and $y$ under $r$ are equal if and only if $x$ and $y$ are related by the equivalence closure of $r$. In symbols: $$\text{Quot.mk}_r(x) = \text{Quot.mk}_r(y) \leftrightarrow \text{EqvGen}\,r\,x\,y$$

Quotient.eq theorem

{r : Setoid α} {x y : α} : Quotient.mk r x = ⟦y⟧ ↔ r x y

Full source

@[simp]
theorem Quotient.eq {r : Setoid α} {x y : α} : Quotient.mkQuotient.mk r x = ⟦y⟧ ↔ r x y :=
  ⟨Quotient.exact, Quotient.sound⟩

Equivalence of Quotient Equality and Setoid Relation

Informal description

For any setoid $r$ on a type $\alpha$ and elements $x, y \in \alpha$, the equivalence class of $x$ under $r$ equals the equivalence class of $y$ if and only if $x$ is related to $y$ under the setoid relation $r$. In symbols: $$\text{Quotient.mk}_r(x) = [y]_r \leftrightarrow r(x,y)$$

Quotient.forall theorem

{α : Sort*} {s : Setoid α} {p : Quotient s → Prop} : (∀ a, p a) ↔ ∀ a : α, p ⟦a⟧

Full source

theorem Quotient.forall {α : Sort*} {s : Setoid α} {p : Quotient s → Prop} :
    (∀ a, p a) ↔ ∀ a : α, p ⟦a⟧ :=
  ⟨fun h _ ↦ h _, fun h a ↦ a.ind h⟩

Universal Quantification over Quotient is Equivalent to Quantification over Representatives

Informal description

For any type $\alpha$ with a setoid $s$ (an equivalence relation) and any predicate $p$ on the quotient type $\alpha/s$, the universal quantification over the quotient satisfies $(\forall a \in \alpha/s, p(a))$ if and only if for all $a \in \alpha$, $p([a])$ holds, where $[a]$ denotes the equivalence class of $a$.

Quotient.exists theorem

{α : Sort*} {s : Setoid α} {p : Quotient s → Prop} : (∃ a, p a) ↔ ∃ a : α, p ⟦a⟧

Full source

theorem Quotient.exists {α : Sort*} {s : Setoid α} {p : Quotient s → Prop} :
    (∃ a, p a) ↔ ∃ a : α, p ⟦a⟧ :=
  ⟨fun ⟨q, hq⟩ ↦ q.ind (motive := (p · → _)) .intro hq, fun ⟨a, ha⟩ ↦ ⟨⟦a⟧, ha⟩⟩

Existence in Quotient Types via Representatives

Informal description

For any type $\alpha$ with a setoid $s$ (an equivalence relation) and a predicate $p$ on the quotient type $\text{Quotient } s$, the following equivalence holds: there exists an element $a$ in the quotient satisfying $p(a)$ if and only if there exists an element $a$ in $\alpha$ such that $p$ holds for the equivalence class $\llbracket a \rrbracket$ of $a$ in the quotient.

Quotient.lift_mk theorem

 {s : Setoid α} (f : α → β) (h : ∀ a b : α, a ≈ b → f a = f b) (x : α) : Quotient.lift f h (Quotient.mk s x) = f x

Full source

@[simp]
theorem Quotient.lift_mk {s : Setoid α} (f : α → β) (h : ∀ a b : α, a ≈ b → f a = f b) (x : α) :
    Quotient.lift f h (Quotient.mk s x) = f x :=
  rfl

Lift of Function to Quotient Evaluated at Equivalence Class Equals Original Function

Informal description

Let $\alpha$ be a type with a setoid $s$ (an equivalence relation), and let $f : \alpha \to \beta$ be a function that respects the equivalence relation (i.e., $a \approx b$ implies $f(a) = f(b)$ for all $a, b \in \alpha$). Then for any $x \in \alpha$, the lift of $f$ to the quotient $\alpha/s$ evaluated at the equivalence class of $x$ equals $f(x)$. In symbols: \[ \text{Quotient.lift}\, f\, h\, [x] = f(x) \] where $[x]$ denotes the equivalence class of $x$ in $\alpha/s$.

Quotient.lift_comp_mk theorem

{_ : Setoid α} (f : α → β) (h : ∀ a b : α, a ≈ b → f a = f b) : Quotient.lift f h ∘ Quotient.mk _ = f

Full source

@[simp]
theorem Quotient.lift_comp_mk {_ : Setoid α} (f : α → β) (h : ∀ a b : α, a ≈ b → f a = f b) :
    Quotient.liftQuotient.lift f h ∘ Quotient.mk _ = f :=
  rfl

Composition of Quotient Lift with Quotient Map Preserves Original Function

Informal description

Let $\alpha$ be a type with a setoid (equivalence relation) structure, and let $f : \alpha \to \beta$ be a function that respects the equivalence relation (i.e., $a \approx b$ implies $f(a) = f(b)$ for all $a, b \in \alpha$). Then the composition of the quotient lift of $f$ with the quotient map equals $f$ itself, i.e., $\text{Quotient.lift}\, f\, h \circ \text{Quotient.mk} = f$.

Quotient.lift_surjective_iff theorem

 {α β : Sort*} {s : Setoid α} (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b) :
  Function.Surjective (Quotient.lift f h : Quotient s → β) ↔ Function.Surjective f

Full source

@[simp]
theorem Quotient.lift_surjective_iff {α β : Sort*} {s : Setoid α} (f : α → β)
    (h : ∀ (a b : α), a ≈ b → f a = f b) :
    Function.SurjectiveFunction.Surjective (Quotient.lift f h : Quotient s → β) ↔ Function.Surjective f :=
  Quot.surjective_lift h

Surjectivity of Quotient Lift if and only if Original Function is Surjective

Informal description

Let $\alpha$ and $\beta$ be types, and let $s$ be a setoid (equivalence relation) on $\alpha$. Given a function $f \colon \alpha \to \beta$ that respects the equivalence relation (i.e., $a \approx b$ implies $f(a) = f(b)$ for all $a, b \in \alpha$), the lifted function $\overline{f} \colon \alpha / s \to \beta$ defined by $\overline{f}([a]) = f(a)$ is surjective if and only if $f$ is surjective.

Quotient.lift_surjective theorem

 {α β : Sort*} {s : Setoid α} (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b) (hf : Function.Surjective f) :
  Function.Surjective (Quotient.lift f h : Quotient s → β)

Full source

theorem Quotient.lift_surjective {α β : Sort*} {s : Setoid α} (f : α → β)
    (h : ∀ (a b : α), a ≈ b → f a = f b) (hf : Function.Surjective f):
    Function.Surjective (Quotient.lift f h : Quotient s → β) :=
  (Quot.surjective_lift h).mpr hf

Surjectivity of Lifted Function on Quotient Space

Informal description

Let $\alpha$ and $\beta$ be types, and let $s$ be a setoid (equivalence relation) on $\alpha$. Given a function $f \colon \alpha \to \beta$ that respects the equivalence relation (i.e., $a \approx b$ implies $f(a) = f(b)$ for all $a, b \in \alpha$), if $f$ is surjective, then the lifted function $\overline{f} \colon \alpha / s \to \beta$ defined by $\overline{f}([a]) = f(a)$ is also surjective.

Quotient.lift₂_mk theorem

 {α : Sort*} {β : Sort*} {γ : Sort*} {_ : Setoid α} {_ : Setoid β} (f : α → β → γ)
  (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) (a : α) (b : β) :
  Quotient.lift₂ f h (Quotient.mk _ a) (Quotient.mk _ b) = f a b

Full source

@[simp]
theorem Quotient.lift₂_mk {α : Sort*} {β : Sort*} {γ : Sort*} {_ : Setoid α} {_ : Setoid β}
    (f : α → β → γ)
    (h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂)
    (a : α) (b : β) :
    Quotient.lift₂ f h (Quotient.mk _ a) (Quotient.mk _ b) = f a b :=
  rfl

Lifting a Binary Function to Quotients Preserves Evaluation on Representatives

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types with equivalence relations (setoids) on $\alpha$ and $\beta$. Given a function $f: \alpha \to \beta \to \gamma$ that respects these equivalence relations (i.e., for any $a_1, a_2 \in \alpha$ and $b_1, b_2 \in \beta$, if $a_1 \approx b_1$ and $a_2 \approx b_2$, then $f(a_1, a_2) = f(b_1, b_2)$), then for any $a \in \alpha$ and $b \in \beta$, the lifted function $\text{lift}_2 f h$ applied to the equivalence classes $[a]$ and $[b]$ equals $f(a,b)$. In symbols: $$\text{lift}_2 f h ([a], [b]) = f(a, b)$$

Quotient.liftOn_mk theorem

 {s : Setoid α} (f : α → β) (h : ∀ a b : α, a ≈ b → f a = f b) (x : α) : Quotient.liftOn (Quotient.mk s x) f h = f x

Full source

theorem Quotient.liftOn_mk {s : Setoid α} (f : α → β) (h : ∀ a b : α, a ≈ b → f a = f b) (x : α) :
    Quotient.liftOn (Quotient.mk s x) f h = f x :=
  rfl

Lifting a Function to a Quotient Preserves Values on Representatives

Informal description

Let $\alpha$ be a type with a setoid structure $s$ (an equivalence relation $\approx$), and let $f : \alpha \to \beta$ be a function that respects the equivalence relation (i.e., $a \approx b$ implies $f(a) = f(b)$). Then for any $x \in \alpha$, the value of the lifted function `Quotient.liftOn` applied to the equivalence class of $x$ is equal to $f(x)$, i.e., \[ \text{Quotient.liftOn} (\text{Quotient.mk}_s \, x) \, f \, h = f(x). \]

Quotient.liftOn₂_mk theorem

 {α : Sort*} {β : Sort*} {_ : Setoid α} (f : α → α → β) (h : ∀ a₁ a₂ b₁ b₂ : α, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂)
  (x y : α) : Quotient.liftOn₂ (Quotient.mk _ x) (Quotient.mk _ y) f h = f x y

Full source

@[simp]
theorem Quotient.liftOn₂_mk {α : Sort*} {β : Sort*} {_ : Setoid α} (f : α → α → β)
    (h : ∀ a₁ a₂ b₁ b₂ : α, a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) (x y : α) :
    Quotient.liftOn₂ (Quotient.mk _ x) (Quotient.mk _ y) f h = f x y :=
  rfl

Lifting a Binary Function to Quotients Preserves Evaluation on Representatives (Binary Case)

Informal description

Let $\alpha$ be a type with an equivalence relation $\approx$ (given by a setoid), and let $f : \alpha \to \alpha \to \beta$ be a binary function that respects the equivalence relation (i.e., for any $a_1, a_2, b_1, b_2 \in \alpha$, if $a_1 \approx b_1$ and $a_2 \approx b_2$, then $f(a_1, a_2) = f(b_1, b_2)$). Then for any $x, y \in \alpha$, the lifted function $\text{liftOn}_2$ applied to the equivalence classes $[x]$ and $[y]$ equals $f(x,y)$. In symbols: $$\text{liftOn}_2 f h ([x], [y]) = f(x, y)$$

Quot.mk_surjective theorem

{r : α → α → Prop} : Function.Surjective (Quot.mk r)

Full source

/-- `Quot.mk r` is a surjective function. -/
theorem Quot.mk_surjective {r : α → α → Prop} : Function.Surjective (Quot.mk r) :=
  Quot.exists_rep

Surjectivity of Quotient Construction

Informal description

For any type $\alpha$ and any binary relation $r$ on $\alpha$, the function $\operatorname{Quot.mk}_r : \alpha \to \operatorname{Quot} r$ that maps each element to its equivalence class is surjective. That is, for every element $q$ in the quotient $\operatorname{Quot} r$, there exists an element $a \in \alpha$ such that $\operatorname{Quot.mk}_r(a) = q$.

Quotient.mk_surjective theorem

{s : Setoid α} : Function.Surjective (Quotient.mk s)

Full source

/-- `Quotient.mk` is a surjective function. -/
theorem Quotient.mk_surjective {s : Setoid α} :
    Function.Surjective (Quotient.mk s) :=
  Quot.exists_rep

Surjectivity of the Quotient Projection Map

Informal description

For any type $\alpha$ equipped with an equivalence relation (given by a setoid $s$), the canonical projection function $\text{Quotient.mk} : \alpha \to \text{Quotient } s$ is surjective. That is, for every element $q$ in the quotient type $\text{Quotient } s$, there exists an element $a \in \alpha$ such that $\text{Quotient.mk } a = q$.

Quotient.mk'_surjective theorem

[s : Setoid α] : Function.Surjective (Quotient.mk' : α → Quotient s)

Full source

/-- `Quotient.mk'` is a surjective function. -/
theorem Quotient.mk'_surjective [s : Setoid α] :
    Function.Surjective (Quotient.mk' : α → Quotient s) :=
  Quot.exists_rep

Surjectivity of the Quotient Map `Quotient.mk'`

Informal description

For any setoid `s` on a type `α`, the quotient map `Quotient.mk' : α → Quotient s` is surjective. That is, for every element `q` in the quotient type `Quotient s`, there exists an element `a : α` such that `Quotient.mk' a = q`.

Quot.out definition

{r : α → α → Prop} (q : Quot r) : α

Full source

/-- Choose an element of the equivalence class using the axiom of choice.
  Sound but noncomputable. -/
noncomputable def Quot.out {r : α → α → Prop} (q : Quot r) : α :=
  Classical.choose (Quot.exists_rep q)

Representative selection from a quotient type

Informal description

For any equivalence relation `r` on a type `α` and any element `q` of the quotient type `Quot r`, the function `Quot.out` selects a representative element of `α` from the equivalence class of `q`, using the axiom of choice. This selection is sound but noncomputable.

Quot.unquot definition

{r : α → α → Prop} : Quot r → α

Full source

/-- Unwrap the VM representation of a quotient to obtain an element of the equivalence class.
  Computable but unsound. -/
unsafe def Quot.unquot {r : α → α → Prop} : Quot r → α :=
  cast lcProof

Representative extraction from quotient type

Informal description

The function takes a quotient element `q` of type `Quot r` (where `r` is a binary relation on type `α`) and returns an arbitrary representative from the equivalence class of `q`. This operation is computable but not sound in general, as it does not preserve the quotient structure.

Quot.out_eq theorem

{r : α → α → Prop} (q : Quot r) : Quot.mk r q.out = q

Full source

@[simp]
theorem Quot.out_eq {r : α → α → Prop} (q : Quot r) : Quot.mk r q.out = q :=
  Classical.choose_spec (Quot.exists_rep q)

Representative Selection Preserves Quotient Equality

Informal description

For any equivalence relation $r$ on a type $\alpha$ and any element $q$ of the quotient type $\mathrm{Quot}\,r$, the equivalence class of the representative selected by $\mathrm{Quot.out}\,q$ equals $q$ itself, i.e., $\mathrm{Quot.mk}\,r\,(\mathrm{Quot.out}\,q) = q$.

Quotient.out definition

{s : Setoid α} : Quotient s → α

Full source

/-- Choose an element of the equivalence class using the axiom of choice.
  Sound but noncomputable. -/
noncomputable def Quotient.out {s : Setoid α} : Quotient s → α :=
  Quot.out

Representative selection from a quotient type

Informal description

For a type $\alpha$ equipped with a setoid (equivalence relation) $s$, the function selects a representative element from each equivalence class in the quotient type $\text{Quotient } s$. This selection uses the axiom of choice and is sound but noncomputable.

Quotient.out_eq theorem

{s : Setoid α} (q : Quotient s) : ⟦q.out⟧ = q

Full source

@[simp]
theorem Quotient.out_eq {s : Setoid α} (q : Quotient s) : ⟦q.out⟧ = q :=
  Quot.out_eq q

Quotient Representative Equality: $\llbracket q.\mathrm{out} \rrbracket = q$

Informal description

For any type $\alpha$ equipped with a setoid (equivalence relation) $s$ and any element $q$ of the quotient type $\mathrm{Quotient}\,s$, the equivalence class of the representative selected by $\mathrm{Quotient.out}\,q$ equals $q$ itself, i.e., $\llbracket \mathrm{Quotient.out}\,q \rrbracket = q$.

Quotient.mk_out theorem

{s : Setoid α} (a : α) : s (⟦a⟧ : Quotient s).out a

Full source

theorem Quotient.mk_out {s : Setoid α} (a : α) : s (⟦a⟧ : Quotient s).out a :=
  Quotient.exact (Quotient.out_eq _)

Representative of Equivalence Class is Equivalent to Original Element

Informal description

For any type $\alpha$ equipped with a setoid (equivalence relation) $s$ and any element $a \in \alpha$, the representative selected from the equivalence class $\llbracket a \rrbracket$ is equivalent to $a$ under $s$. In symbols: $$a \approx (\llbracket a \rrbracket).\mathrm{out}$$

Quotient.mk_eq_iff_out theorem

{s : Setoid α} {x : α} {y : Quotient s} : ⟦x⟧ = y ↔ x ≈ Quotient.out y

Full source

theorem Quotient.mk_eq_iff_out {s : Setoid α} {x : α} {y : Quotient s} :
    ⟦x⟧⟦x⟧ = y ↔ x ≈ Quotient.out y := by
  refine Iff.trans ?_ Quotient.eq
  rw [Quotient.out_eq y]

Equivalence Class Equality via Representative: $[x] = y \leftrightarrow x \approx y.\mathrm{out}$

Informal description

For any type $\alpha$ equipped with a setoid (equivalence relation) $s$, an element $x \in \alpha$, and an element $y$ of the quotient type $\mathrm{Quotient}\,s$, the equivalence class of $x$ equals $y$ if and only if $x$ is equivalent to the representative of $y$ under $s$. In symbols: $$[x]_s = y \leftrightarrow x \approx \mathrm{Quotient.out}\,y$$

Quotient.out_equiv_out theorem

{s : Setoid α} {x y : Quotient s} : x.out ≈ y.out ↔ x = y

Full source

@[simp]
theorem Quotient.out_equiv_out {s : Setoid α} {x y : Quotient s} : x.out ≈ y.outx.out ≈ y.out ↔ x = y := by
  rw [← Quotient.eq_mk_iff_out, Quotient.out_eq]

Equivalence of Quotient Representatives Characterizes Equality in Quotient

Informal description

For any type $\alpha$ equipped with a setoid (equivalence relation) $s$ and any elements $x, y$ of the quotient type $\mathrm{Quotient}\,s$, the representatives selected by $\mathrm{Quotient.out}$ are equivalent under $s$ if and only if $x$ and $y$ are equal in the quotient, i.e., $x.\mathrm{out} \approx y.\mathrm{out} \leftrightarrow x = y$.

Quotient.out_injective theorem

{s : Setoid α} : Function.Injective (@Quotient.out α s)

Full source

theorem Quotient.out_injective {s : Setoid α} : Function.Injective (@Quotient.out α s) :=
  fun _ _ h ↦ Quotient.out_equiv_out.1 <| h ▸ Setoid.refl _

Injectivity of Quotient Representative Selection

Informal description

For any type $\alpha$ equipped with a setoid (equivalence relation) $s$, the function $\mathrm{Quotient.out} : \mathrm{Quotient}\,s \to \alpha$ is injective. That is, for any $x, y \in \mathrm{Quotient}\,s$, if $x.\mathrm{out} = y.\mathrm{out}$, then $x = y$.

Quotient.out_inj theorem

{s : Setoid α} {x y : Quotient s} : x.out = y.out ↔ x = y

Full source

@[simp]
theorem Quotient.out_inj {s : Setoid α} {x y : Quotient s} : x.out = y.out ↔ x = y :=
  ⟨fun h ↦ Quotient.out_injective h, fun h ↦ h ▸ rfl⟩

Equality of Quotient Elements via Representative Equality

Informal description

For any type $\alpha$ equipped with a setoid (equivalence relation) $s$ and any elements $x, y$ of the quotient type $\mathrm{Quotient}\,s$, the representatives selected by $\mathrm{Quotient.out}$ are equal if and only if $x$ and $y$ are equal in the quotient, i.e., $x.\mathrm{out} = y.\mathrm{out} \leftrightarrow x = y$.

piSetoid instance

{ι : Sort*} {α : ι → Sort*} [∀ i, Setoid (α i)] : Setoid (∀ i, α i)

Full source

instance piSetoid {ι : Sort*} {α : ι → Sort*} [∀ i, Setoid (α i)] : Setoid (∀ i, α i) where
  r a b := ∀ i, a i ≈ b i
  iseqv := ⟨fun _ _ ↦ Setoid.refl _,
            fun h _ ↦ Setoid.symm (h _),
            fun h₁ h₂ _ ↦ Setoid.trans (h₁ _) (h₂ _)⟩

Setoid Structure on Dependent Function Types

Informal description

For any family of types $\alpha_i$ indexed by $\iota$, where each $\alpha_i$ is equipped with a setoid (equivalence relation) structure, the function type $\forall i, \alpha_i$ inherits a setoid structure where two functions are equivalent if they are equivalent at every index.

Quotient.eval definition

 {ι : Type*} {α : ι → Sort*} {S : ∀ i, Setoid (α i)} (q : @Quotient (∀ i, α i) (by infer_instance)) (i : ι) :
  Quotient (S i)

Full source

/-- Given a class of functions `q : @Quotient (∀ i, α i) _`, returns the class of `i`-th projection
`Quotient (S i)`. -/
def Quotient.eval {ι : Type*} {α : ι → Sort*} {S : ∀ i, Setoid (α i)}
    (q : @Quotient (∀ i, α i) (by infer_instance)) (i : ι) : Quotient (S i) :=
  q.map (· i) fun _ _ h ↦ by exact h i

Evaluation of Quotient of Dependent Functions

Informal description

Given a family of types $\alpha_i$ indexed by $\iota$, each equipped with a setoid (equivalence relation) $S_i$, and a quotient element $q$ of the dependent function type $\forall i, \alpha_i$ (with the induced setoid structure), the function `Quotient.eval` evaluates $q$ at index $i$ to produce a quotient element in $\text{Quotient } S_i$.

Quotient.eval_mk theorem

 {ι : Type*} {α : ι → Type*} {S : ∀ i, Setoid (α i)} (f : ∀ i, α i) : Quotient.eval (S := S) ⟦f⟧ = fun i ↦ ⟦f i⟧

Full source

@[simp]
theorem Quotient.eval_mk {ι : Type*} {α : ι → Type*} {S : ∀ i, Setoid (α i)} (f : ∀ i, α i) :
    Quotient.eval (S := S) ⟦f⟧ = fun i ↦ ⟦f i⟧ :=
  rfl

Evaluation of Quotient Function at Representative

Informal description

For any family of types $\alpha_i$ indexed by $\iota$, each equipped with a setoid (equivalence relation) $S_i$, and any function $f \colon \forall i, \alpha_i$, the evaluation of the quotient element $\llbracket f \rrbracket$ at any index $i$ equals the quotient element $\llbracket f_i \rrbracket$ in $\text{Quotient } S_i$. In other words, $\text{Quotient.eval} \llbracket f \rrbracket = \lambda i, \llbracket f_i \rrbracket$.

Quotient.choice definition

 {ι : Type*} {α : ι → Type*} {S : ∀ i, Setoid (α i)} (f : ∀ i, Quotient (S i)) :
  @Quotient (∀ i, α i) (by infer_instance)

Full source

/-- 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`. -/
noncomputable def Quotient.choice {ι : Type*} {α : ι → Type*} {S : ∀ i, Setoid (α i)}
    (f : ∀ i, Quotient (S i)) :
    @Quotient (∀ i, α i) (by infer_instance) :=
  ⟦fun i ↦ (f i).out⟧

Lifting a family of quotient elements to a quotient of functions

Informal description

Given a family of types $\alpha_i$ indexed by $\iota$, each equipped with a setoid (equivalence relation) $S_i$, and a family of quotient elements $f_i \in \text{Quotient } S_i$ for each $i$, the function constructs a quotient element of the dependent function type $\forall i, \alpha_i$ (with the induced setoid structure) by selecting representatives for each $f_i$ and forming the corresponding function.

Quotient.choice_eq theorem

 {ι : Type*} {α : ι → Type*} {S : ∀ i, Setoid (α i)} (f : ∀ i, α i) : (Quotient.choice (S := S) fun i ↦ ⟦f i⟧) = ⟦f⟧

Full source

@[simp]
theorem Quotient.choice_eq {ι : Type*} {α : ι → Type*} {S : ∀ i, Setoid (α i)} (f : ∀ i, α i) :
    (Quotient.choice (S := S) fun i ↦ ⟦f i⟧) = ⟦f⟧ :=
  Quotient.sound fun _ ↦ Quotient.mk_out _

Quotient Choice of Function Classes Equals Function Class

Informal description

For any family of types $\alpha_i$ indexed by $\iota$, each equipped with a setoid (equivalence relation) $S_i$, and any function $f \colon \forall i, \alpha_i$, the quotient element obtained by applying `Quotient.choice` to the family of equivalence classes $\llbracket f_i \rrbracket$ is equal to the equivalence class $\llbracket f \rrbracket$ of the function itself. In symbols: $$\text{Quotient.choice} (\lambda i, \llbracket f_i \rrbracket) = \llbracket f \rrbracket$$

Quotient.induction_on_pi theorem

 {ι : Type*} {α : ι → Sort*} {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

Full source

@[elab_as_elim]
theorem Quotient.induction_on_pi {ι : Type*} {α : ι → Sort*} {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 := by
  rw [← (funext fun i ↦ Quotient.out_eq (f i) : (fun i ↦ ⟦(f i).out⟧) = f)]
  apply h

Induction Principle for Functions into Quotient Types

Informal description

Let $\iota$ be a type, and for each $i \in \iota$, let $\alpha_i$ be a type equipped with an equivalence relation $s_i$. Given a predicate $p$ on functions $\prod_{i \in \iota} \text{Quotient } s_i$, if $p$ holds for all functions of the form $\lambda i, \llbracket a_i \rrbracket$ where $a_i \in \alpha_i$, then $p$ holds for any function $f \in \prod_{i \in \iota} \text{Quotient } s_i$.

nonempty_quotient_iff theorem

(s : Setoid α) : Nonempty (Quotient s) ↔ Nonempty α

Full source

theorem nonempty_quotient_iff (s : Setoid α) : NonemptyNonempty (Quotient s) ↔ Nonempty α :=
  ⟨fun ⟨a⟩ ↦ Quotient.inductionOn a Nonempty.intro, fun ⟨a⟩ ↦ ⟨⟦a⟧⟩⟩

Non-emptiness of Quotient Type and Original Type

Informal description

For any setoid `s` on a type `α`, the quotient type `Quotient s` is nonempty if and only if the original type `α` is nonempty.

true_equivalence theorem

: @Equivalence α fun _ _ ↦ True

Full source

theorem true_equivalence : @Equivalence α fun _ _ ↦ True :=
  ⟨fun _ ↦ trivial, fun _ ↦ trivial, fun _ _ ↦ trivial⟩

Trivial Relation is an Equivalence Relation

Informal description

The relation defined by $\lambda (x y : \alpha), \text{True}$ is an equivalence relation on any type $\alpha$.

trueSetoid definition

: Setoid α

Full source

/-- Always-true relation as a `Setoid`.

Note that in later files the preferred spelling is `⊤ : Setoid α`. -/
def trueSetoid : Setoid α :=
  ⟨_, true_equivalence⟩

Trivial setoid

Informal description

The trivial setoid on a type $\alpha$, where every pair of elements is related (i.e., the relation is always true). This is equivalent to using the universal relation $\top$ as a setoid.

Trunc definition

(α : Sort u) : Sort u

Full source

/-- `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. -/
def Trunc.{u} (α : Sort u) : Sort u :=
  @Quotient α trueSetoid

Truncation of a type by the trivial relation

Informal description

The type `Trunc α` is the quotient of a type `α` by the trivial equivalence relation (where all elements are considered equivalent). This construction is analogous to the propositional truncation in homotopy type theory and serves a similar purpose to `Nonempty α`, but unlike `Nonempty α`, `Trunc α` retains computational content, with its virtual machine representation matching that of `α`. This ensures that computability is preserved when using `Trunc α`.

Trunc.mk definition

(a : α) : Trunc α

Full source

/-- Constructor for `Trunc α` -/
def mk (a : α) : Trunc α :=
  Quot.mk _ a

Truncation constructor

Informal description

The function maps an element $a$ of type $\alpha$ to its equivalence class in the truncation `Trunc α`, where all elements of $\alpha$ are considered equivalent.

Trunc.instInhabited instance

[Inhabited α] : Inhabited (Trunc α)

Full source

instance [Inhabited α] : Inhabited (Trunc α) :=
  ⟨mk default⟩

Inhabitedness of Truncation

Informal description

For any inhabited type $\alpha$, the truncation $\text{Trunc } \alpha$ is also inhabited.

Trunc.lift definition

(f : α → β) (c : ∀ a b : α, f a = f b) : Trunc α → β

Full source

/-- Any constant function lifts to a function out of the truncation -/
def lift (f : α → β) (c : ∀ a b : α, f a = f b) : Trunc α → β :=
  Quot.lift f fun a b _ ↦ c a b

Lifting a constant function to the truncation

Informal description

Given a constant function $f : \alpha \to \beta$ (i.e., $f$ takes the same value on all inputs), there exists a function from the truncation $\text{Trunc } \alpha$ to $\beta$ that lifts $f$. Specifically, for any $a, b : \alpha$, if $f a = f b$, then this function is well-defined on the equivalence classes in $\text{Trunc } \alpha$.

Trunc.ind theorem

{β : Trunc α → Prop} : (∀ a : α, β (mk a)) → ∀ q : Trunc α, β q

Full source

theorem ind {β : Trunc α → Prop} : (∀ a : α, β (mk a)) → ∀ q : Trunc α, β q :=
  Quot.ind

Induction Principle for Truncation

Informal description

For any predicate $\beta$ on the truncation $\text{Trunc } \alpha$, if $\beta$ holds for the equivalence class of every element $a : \alpha$, then $\beta$ holds for every element of $\text{Trunc } \alpha$.

Trunc.lift_mk theorem

(f : α → β) (c) (a : α) : lift f c (mk a) = f a

Full source

protected theorem lift_mk (f : α → β) (c) (a : α) : lift f c (mk a) = f a :=
  rfl

Lifted Function on Truncation Preserves Value: $\text{lift } f \ c \ (\text{mk } a) = f(a)$

Informal description

For any function $f : \alpha \to \beta$ and any proof $c$ that $f$ is constant (i.e., $f(a) = f(b)$ for all $a, b \in \alpha$), the lifted function $\text{lift } f \ c$ applied to the truncation of an element $a \in \alpha$ equals $f(a)$. That is, $\text{lift } f \ c \ (\text{mk } a) = f(a)$.

Trunc.liftOn definition

(q : Trunc α) (f : α → β) (c : ∀ a b : α, f a = f b) : β

Full source

/-- Lift a constant function on `q : Trunc α`. -/
protected def liftOn (q : Trunc α) (f : α → β) (c : ∀ a b : α, f a = f b) : β :=
  lift f c q

Lifting a constant function on truncation elements

Informal description

Given an element $q$ of the truncation type $\text{Trunc } \alpha$, a function $f : \alpha \to \beta$, and a proof that $f$ is constant (i.e., $f(a) = f(b)$ for all $a, b \in \alpha$), this function returns the value of $f$ applied to any representative of $q$.

Trunc.induction_on theorem

{β : Trunc α → Prop} (q : Trunc α) (h : ∀ a, β (mk a)) : β q

Full source

@[elab_as_elim]
protected theorem induction_on {β : Trunc α → Prop} (q : Trunc α) (h : ∀ a, β (mk a)) : β q :=
  ind h q

Induction Principle for Truncation Type

Informal description

For any predicate $\beta$ on the truncation type $\operatorname{Trunc}(\alpha)$ and any element $q \in \operatorname{Trunc}(\alpha)$, if $\beta$ holds for the equivalence class of every element $a \in \alpha$, then $\beta$ holds for $q$.

Trunc.exists_rep theorem

(q : Trunc α) : ∃ a : α, mk a = q

Full source

theorem exists_rep (q : Trunc α) : ∃ a : α, mk a = q :=
  Quot.exists_rep q

Existence of Representative in Truncation Type

Informal description

For any element $q$ of the truncation type $\operatorname{Trunc}(\alpha)$, there exists an element $a$ of type $\alpha$ such that the equivalence class of $a$ in $\operatorname{Trunc}(\alpha)$ equals $q$.

Trunc.induction_on₂ theorem

{C : Trunc α → Trunc β → Prop} (q₁ : Trunc α) (q₂ : Trunc β) (h : ∀ a b, C (mk a) (mk b)) : C q₁ q₂

Full source

@[elab_as_elim]
protected theorem induction_on₂ {C : Trunc α → Trunc β → Prop} (q₁ : Trunc α) (q₂ : Trunc β)
    (h : ∀ a b, C (mk a) (mk b)) : C q₁ q₂ :=
  Trunc.induction_on q₁ fun a₁ ↦ Trunc.induction_on q₂ (h a₁)

Double Induction Principle for Truncation Types

Informal description

For any predicate $C$ on pairs of elements from the truncation types $\operatorname{Trunc}(\alpha)$ and $\operatorname{Trunc}(\beta)$, and for any elements $q_1 \in \operatorname{Trunc}(\alpha)$ and $q_2 \in \operatorname{Trunc}(\beta)$, if $C$ holds for the equivalence classes of every pair $(a, b) \in \alpha \times \beta$, then $C$ holds for $(q_1, q_2)$.

Trunc.eq theorem

(a b : Trunc α) : a = b

Full source

protected theorem eq (a b : Trunc α) : a = b :=
  Trunc.induction_on₂ a b fun _ _ ↦ Quot.sound trivial

All Elements Equal in Truncation Type

Informal description

For any two elements $a$ and $b$ of the truncation type $\operatorname{Trunc}(\alpha)$, they are equal, i.e., $a = b$.

Trunc.instSubsingletonTrunc instance

: Subsingleton (Trunc α)

Full source

instance instSubsingletonTrunc : Subsingleton (Trunc α) :=
  ⟨Trunc.eq⟩

Truncation Types are Subsingletons

Informal description

The truncation type $\operatorname{Trunc}(\alpha)$ is a subsingleton, meaning any two elements of $\operatorname{Trunc}(\alpha)$ are equal.

Trunc.bind definition

(q : Trunc α) (f : α → Trunc β) : Trunc β

Full source

/-- The `bind` operator for the `Trunc` monad. -/
def bind (q : Trunc α) (f : α → Trunc β) : Trunc β :=
  Trunc.liftOn q f fun _ _ ↦ Trunc.eq _ _

Monadic bind for truncation

Informal description

The `bind` operation for the `Trunc` monad takes an element `q` of `Trunc α` and a function `f : α → Trunc β`, and returns an element of `Trunc β`. This operation ensures that the result is independent of the choice of representative for `q` by requiring that `f` produces equivalent results for any two elements of `α`.

Trunc.map definition

(f : α → β) (q : Trunc α) : Trunc β

Full source

/-- A function `f : α → β` defines a function `map f : Trunc α → Trunc β`. -/
def map (f : α → β) (q : Trunc α) : Trunc β :=
  bind q (Trunc.mkTrunc.mk ∘ f)

Mapping a function over a truncation

Informal description

Given a function $f : \alpha \to \beta$ and an element $q$ of the truncation type $\text{Trunc}\,\alpha$, the function $\text{Trunc.map}\,f\,q$ applies $f$ to the (implicit) representative of $q$ and returns the result in $\text{Trunc}\,\beta$. This operation is well-defined since all elements of $\alpha$ are considered equivalent in $\text{Trunc}\,\alpha$.

Trunc.instMonad instance

: Monad Trunc

Full source

instance : Monad Trunc where
  pure := @Trunc.mk
  bind := @Trunc.bind

Monad Structure on Truncation

Informal description

The truncation construction `Trunc` forms a monad on types, where the unit operation maps an element to its equivalence class under the trivial relation, and the bind operation lifts functions while respecting the equivalence relation.

Trunc.instLawfulMonad instance

: LawfulMonad Trunc

Full source

instance : LawfulMonad Trunc where
  id_map _ := Trunc.eq _ _
  pure_bind _ _ := rfl
  bind_assoc _ _ _ := Trunc.eq _ _
  map_const := rfl
  seqLeft_eq _ _ := Trunc.eq _ _
  seqRight_eq _ _ := Trunc.eq _ _
  pure_seq _ _ := rfl
  bind_pure_comp _ _ := rfl
  bind_map _ _ := rfl

Truncation as a Lawful Monad

Informal description

The truncation construction `Trunc` forms a lawful monad on types, where the unit operation maps an element to its equivalence class under the trivial relation, and the bind operation lifts functions while respecting the equivalence relation, satisfying all monad laws.

Trunc.rec definition

 (f : ∀ a, C (mk a)) (h : ∀ a b : α, (Eq.ndrec (f a) (Trunc.eq (mk a) (mk b)) : C (mk b)) = f b) (q : Trunc α) : C q

Full source

/-- Recursion/induction principle for `Trunc`. -/
@[elab_as_elim]
protected def rec (f : ∀ a, C (mk a))
    (h : ∀ a b : α, (Eq.ndrec (f a) (Trunc.eq (mk a) (mk b)) : C (mk b)) = f b)
    (q : Trunc α) : C q :=
  Quot.rec f (fun a b _ ↦ h a b) q

Recursion principle for truncation

Informal description

The recursion principle for the truncation type `Trunc α`, which allows defining a function on `Trunc α` by specifying its values on representatives from `α`. Given a function $f : \forall a, C(\text{mk } a)$ and a proof $h$ that $f$ respects the truncation equivalence (i.e., for any $a, b \in \alpha$, the value of $f$ at $\text{mk } b$ is equal to the value of $f$ at $\text{mk } a$ when transported along the equality $\text{mk } a = \text{mk } b$), the principle constructs a function that maps any element $q \in \text{Trunc } \alpha$ to an element of $C(q)$.

Trunc.recOn definition

 (q : Trunc α) (f : ∀ a, C (mk a)) (h : ∀ a b : α, (Eq.ndrec (f a) (Trunc.eq (mk a) (mk b)) : C (mk b)) = f b) : C q

Full source

/-- A version of `Trunc.rec` taking `q : Trunc α` as the first argument. -/
@[elab_as_elim]
protected def recOn (q : Trunc α) (f : ∀ a, C (mk a))
    (h : ∀ a b : α, (Eq.ndrec (f a) (Trunc.eq (mk a) (mk b)) : C (mk b)) = f b) : C q :=
  Trunc.rec f h q

Recursion on truncation with explicit element

Informal description

Given an element $q$ of the truncation type $\operatorname{Trunc}(\alpha)$, a function $f : \forall a, C(\text{mk } a)$, and a proof $h$ that $f$ respects the truncation equivalence (i.e., for any $a, b \in \alpha$, the value of $f$ at $\text{mk } b$ is equal to the value of $f$ at $\text{mk } a$ when transported along the equality $\text{mk } a = \text{mk } b$), the function constructs an element of $C(q)$ by applying the recursion principle for truncation to $q$, $f$, and $h$.

Trunc.recOnSubsingleton definition

[∀ a, Subsingleton (C (mk a))] (q : Trunc α) (f : ∀ a, C (mk a)) : C q

Full source

/-- A version of `Trunc.recOn` assuming the codomain is a `Subsingleton`. -/
@[elab_as_elim]
protected def recOnSubsingleton [∀ a, Subsingleton (C (mk a))] (q : Trunc α) (f : ∀ a, C (mk a)) :
    C q :=
  Trunc.rec f (fun _ b ↦ Subsingleton.elim _ (f b)) q

Truncation recursion principle for subsingleton codomain

Informal description

A version of the truncation recursion principle `Trunc.recOn` where the codomain type family `C` is assumed to be a subsingleton (i.e., all elements of `C (mk a)` are equal for any `a : α`). Given a function `f : ∀ a, C (mk a)` and an element `q : Trunc α`, this constructs an element of `C q` by using the subsingleton property to simplify the required coherence condition.

Trunc.out definition

: Trunc α → α

Full source

/-- Noncomputably extract a representative of `Trunc α` (using the axiom of choice). -/
noncomputable def out : Trunc α → α :=
  Quot.out

Representative selection from truncation

Informal description

The function selects a representative from the truncation of a type $\alpha$ (using the axiom of choice). For any element $q$ of $\text{Trunc}\,\alpha$, $\text{Trunc.out}\,q$ returns an element of $\alpha$ that represents the equivalence class of $q$ under the trivial relation.

Trunc.out_eq theorem

(q : Trunc α) : mk q.out = q

Full source

@[simp]
theorem out_eq (q : Trunc α) : mk q.out = q :=
  Trunc.eq _ _

Representative Equality in Truncation Type

Informal description

For any element $q$ of the truncation type $\operatorname{Trunc}(\alpha)$, the equivalence class of its representative (selected via $\operatorname{out}$) equals $q$ itself, i.e., $\operatorname{mk}(q.\operatorname{out}) = q$.

Trunc.nonempty theorem

(q : Trunc α) : Nonempty α

Full source

protected theorem nonempty (q : Trunc α) : Nonempty α :=
  nonempty_of_exists q.exists_rep

Nonemptiness of Base Type from Truncation Element

Informal description

For any element $q$ of the truncation type $\operatorname{Trunc}(\alpha)$, the type $\alpha$ is nonempty.

Quotient.mk'' abbrev

(a : α) : Quotient s₁

Full source

/-- A version of `Quotient.mk` taking `{s : Setoid α}` as an implicit argument instead of an
instance argument. -/
protected abbrev mk'' (a : α) : Quotient s₁ :=
  ⟦a⟧

Quotient Construction with Implicit Setoid

Informal description

Given a type $\alpha$ and a setoid $s_1$ on $\alpha$, the function $\text{Quotient.mk''}$ maps an element $a \in \alpha$ to its equivalence class in the quotient type $\text{Quotient } s_1$.

Quotient.mk''_surjective theorem

: Function.Surjective (Quotient.mk'' : α → Quotient s₁)

Full source

/-- `Quotient.mk''` is a surjective function. -/
theorem mk''_surjective : Function.Surjective (Quotient.mk'' : α → Quotient s₁) :=
  Quot.exists_rep

Surjectivity of Quotient Construction with Implicit Setoid

Informal description

The function $\text{Quotient.mk''} : \alpha \to \text{Quotient } s_1$ is surjective, meaning that for every element $q$ in the quotient type $\text{Quotient } s_1$, there exists an element $a \in \alpha$ such that $\text{Quotient.mk''}(a) = q$.

Quotient.liftOn' definition

(q : Quotient s₁) (f : α → φ) (h : ∀ a b, s₁ a b → f a = f b) : φ

Full source

/-- A version of `Quotient.liftOn` taking `{s : Setoid α}` as an implicit argument instead of an
instance argument. -/
protected def liftOn' (q : Quotient s₁) (f : α → φ) (h : ∀ a b, s₁ a b → f a = f b) :
    φ :=
  Quotient.liftOn q f h

Lifting a function to a quotient (implicit setoid version)

Informal description

Given a quotient type `Quotient s₁` where `s₁` is an implicit equivalence relation on type `α`, a function `f : α → φ`, and a proof `h` that `f` respects the equivalence relation `s₁`, the function `Quotient.liftOn'` lifts `f` to a function from `Quotient s₁` to `φ`. Specifically, for any equivalence class `q` in `Quotient s₁`, `Quotient.liftOn' q f h` applies `f` to any representative of `q`, with the guarantee that the result is independent of the choice of representative due to `h`.

Quotient.liftOn'_mk'' theorem

(f : α → φ) (h) (x : α) : Quotient.liftOn' (@Quotient.mk'' _ s₁ x) f h = f x

Full source

@[simp]
protected theorem liftOn'_mk'' (f : α → φ) (h) (x : α) :
    Quotient.liftOn' (@Quotient.mk'' _ s₁ x) f h = f x :=
  rfl

Lifting a Function on Quotient Class Yields Original Function

Informal description

For any function $f : \alpha \to \varphi$ that respects the equivalence relation $s_1$ (i.e., $f(a) = f(b)$ whenever $a \sim_{s_1} b$), and for any element $x \in \alpha$, applying the lifted function $\text{Quotient.liftOn'}$ to the equivalence class of $x$ yields $f(x)$. In other words, $\text{Quotient.liftOn'}(\text{Quotient.mk''}(x), f, h) = f(x)$.

Quotient.surjective_liftOn' theorem

{f : α → φ} (h) : Function.Surjective (fun x : Quotient s₁ ↦ x.liftOn' f h) ↔ Function.Surjective f

Full source

@[simp] lemma surjective_liftOn' {f : α → φ} (h) :
    Function.SurjectiveFunction.Surjective (fun x : Quotient s₁ ↦ x.liftOn' f h) ↔ Function.Surjective f :=
  Quot.surjective_lift _

Surjectivity of Lifted Function on Quotient Space (Implicit Setoid Version)

Informal description

Let $s_1$ be an equivalence relation on a type $\alpha$, and let $f \colon \alpha \to \varphi$ be a function that respects $s_1$ (i.e., $s_1(a, b)$ implies $f(a) = f(b)$). Then the lifted function $\overline{f} \colon \text{Quotient}\, s_1 \to \varphi$ defined by $\overline{f}([x]) = f(x)$ is surjective if and only if $f$ is surjective.

Quotient.liftOn₂' definition

 (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → γ) (h : ∀ a₁ a₂ b₁ b₂, s₁ a₁ b₁ → s₂ a₂ b₂ → f a₁ a₂ = f b₁ b₂) : γ

Full source

/-- A version of `Quotient.liftOn₂` taking `{s₁ : Setoid α} {s₂ : Setoid β}` as implicit arguments
instead of instance arguments. -/
protected def liftOn₂' (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → γ)
    (h : ∀ a₁ a₂ b₁ b₂, s₁ a₁ b₁ → s₂ a₂ b₂ → f a₁ a₂ = f b₁ b₂) : γ :=
  Quotient.liftOn₂ q₁ q₂ f h

Lifting a binary function to quotients with implicit setoids

Informal description

Given two quotient types $\text{Quotient}\, s₁$ and $\text{Quotient}\, s₂$ with respect to equivalence relations $s₁$ on $\alpha$ and $s₂$ on $\beta$, and a function $f : \alpha \to \beta \to \gamma$ that respects these equivalence relations (i.e., $f\, a₁\, a₂ = f\, b₁\, b₂$ whenever $a₁ \sim_{s₁} b₁$ and $a₂ \sim_{s₂} b₂$), the function $\text{Quotient.liftOn₂'}$ lifts $f$ to a function on the quotient types. Specifically, for any $q₁ : \text{Quotient}\, s₁$ and $q₂ : \text{Quotient}\, s₂$, $\text{Quotient.liftOn₂'}\, q₁\, q₂\, f\, h$ applies $f$ to representative elements of $q₁$ and $q₂$ in a way that is independent of the choice of representatives.

Quotient.liftOn₂'_mk'' theorem

 (f : α → β → γ) (h) (a : α) (b : β) : Quotient.liftOn₂' (@Quotient.mk'' _ s₁ a) (@Quotient.mk'' _ s₂ b) f h = f a b

Full source

@[simp]
protected theorem liftOn₂'_mk'' (f : α → β → γ) (h) (a : α) (b : β) :
    Quotient.liftOn₂' (@Quotient.mk'' _ s₁ a) (@Quotient.mk'' _ s₂ b) f h = f a b :=
  rfl

Lifted Binary Function on Quotient Classes Equals Original Function

Informal description

Given a binary function $f : \alpha \to \beta \to \gamma$ that respects the equivalence relations $s_1$ on $\alpha$ and $s_2$ on $\beta$ (i.e., $f\, a_1\, a_2 = f\, b_1\, b_2$ whenever $a_1 \sim_{s_1} b_1$ and $a_2 \sim_{s_2} b_2$), and elements $a \in \alpha$ and $b \in \beta$, the lifted function $\text{Quotient.liftOn₂'}$ applied to the equivalence classes of $a$ and $b$ via $\text{Quotient.mk''}$ satisfies: \[ \text{Quotient.liftOn₂'}\, (\text{Quotient.mk''}\, a)\, (\text{Quotient.mk''}\, b)\, f\, h = f\, a\, b. \]

Quotient.ind' theorem

{p : Quotient s₁ → Prop} (h : ∀ a, p (Quotient.mk'' a)) (q : Quotient s₁) : p q

Full source

/-- A version of `Quotient.ind` taking `{s : Setoid α}` as an implicit argument instead of an
instance argument. -/
@[elab_as_elim]
protected theorem ind' {p : Quotient s₁ → Prop} (h : ∀ a, p (Quotient.mk'' a)) (q : Quotient s₁) :
    p q :=
  Quotient.ind h q

Induction Principle for Quotient Types with Implicit Setoid

Informal description

Let $s_1$ be a setoid on a type $\alpha$, and let $p$ be a predicate on the quotient type $\text{Quotient}\, s_1$. If for every element $a \in \alpha$, the predicate $p$ holds for the equivalence class of $a$ (i.e., $p(\text{Quotient.mk''}\, a)$), then $p$ holds for every element $q$ of the quotient type $\text{Quotient}\, s_1$.

Quotient.ind₂' theorem

 {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₂

Full source

/-- A version of `Quotient.ind₂` taking `{s₁ : Setoid α} {s₂ : Setoid β}` as implicit arguments
instead of instance arguments. -/
@[elab_as_elim]
protected theorem ind₂' {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₂ :=
  Quotient.ind₂ h q₁ q₂

Induction Principle for Binary Predicates on Quotient Types with Implicit Setoids

Informal description

Let $s_1$ and $s_2$ be setoids on types $\alpha$ and $\beta$ respectively, and let $p$ be a predicate on $\text{Quotient}\, s_1 \times \text{Quotient}\, s_2$. If for all elements $a_1 \in \alpha$ and $a_2 \in \beta$, the predicate $p$ holds for the pair of their equivalence classes $(\text{Quotient.mk''}\, a_1, \text{Quotient.mk''}\, a_2)$, then $p$ holds for all pairs $(q_1, q_2)$ where $q_1 \in \text{Quotient}\, s_1$ and $q_2 \in \text{Quotient}\, s_2$.

Quotient.inductionOn' theorem

{p : Quotient s₁ → Prop} (q : Quotient s₁) (h : ∀ a, p (Quotient.mk'' a)) : p q

Full source

/-- A version of `Quotient.inductionOn` taking `{s : Setoid α}` as an implicit argument instead
of an instance argument. -/
@[elab_as_elim]
protected theorem inductionOn' {p : Quotient s₁ → Prop} (q : Quotient s₁)
    (h : ∀ a, p (Quotient.mk'' a)) : p q :=
  Quotient.inductionOn q h

Induction Principle for Quotient Types with Implicit Setoid

Informal description

Let $s_1$ be a setoid on a type $\alpha$, and let $p$ be a predicate on the quotient type $\text{Quotient}\, s_1$. Given an element $q$ of $\text{Quotient}\, s_1$, if for every $a \in \alpha$ the predicate $p$ holds for the equivalence class of $a$ (i.e., $p(\text{Quotient.mk''}\, a)$), then $p$ holds for $q$.

Quotient.inductionOn₂' theorem

 {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₂

Full source

/-- A version of `Quotient.inductionOn₂` taking `{s₁ : Setoid α} {s₂ : Setoid β}` as implicit
arguments instead of instance arguments. -/
@[elab_as_elim]
protected theorem inductionOn₂' {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₂ :=
  Quotient.inductionOn₂ q₁ q₂ h

Induction Principle for Pairs of Quotient Types with Implicit Setoids

Informal description

Let $s_1$ and $s_2$ be setoids on types $\alpha$ and $\beta$ respectively. For any predicate $p$ on $\text{Quotient } s_1 \times \text{Quotient } s_2$, if $p$ holds for all pairs of equivalence classes constructed from elements $(a_1, a_2) \in \alpha \times \beta$, then $p$ holds for any given pair of equivalence classes $(q_1, q_2) \in \text{Quotient } s_1 \times \text{Quotient } s_2$.

Quotient.inductionOn₃' theorem

 {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₃

Full source

/-- A version of `Quotient.inductionOn₃` taking `{s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid γ}`
as implicit arguments instead of instance arguments. -/
@[elab_as_elim]
protected theorem inductionOn₃' {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₃ :=
  Quotient.inductionOn₃ q₁ q₂ q₃ h

Triple Induction Principle for Quotient Types with Implicit Setoids

Informal description

Let $s_1$, $s_2$, and $s_3$ be setoids on types $\alpha$, $\beta$, and $\gamma$ respectively. Given a predicate $p$ on $\text{Quotient } s_1 \times \text{Quotient } s_2 \times \text{Quotient } s_3$, and elements $q_1 \in \text{Quotient } s_1$, $q_2 \in \text{Quotient } s_2$, $q_3 \in \text{Quotient } s_3$, if $p$ holds for all triples of equivalence classes constructed from arbitrary elements $a_1 \in \alpha$, $a_2 \in \beta$, $a_3 \in \gamma$, then $p$ holds for $(q_1, q_2, q_3)$.

Quotient.recOnSubsingleton' definition

 {φ : Quotient s₁ → Sort*} [∀ a, Subsingleton (φ ⟦a⟧)] (q : Quotient s₁) (f : ∀ a, φ (Quotient.mk'' a)) : φ q

Full source

/-- A version of `Quotient.recOnSubsingleton` taking `{s₁ : Setoid α}` as an implicit argument
instead of an instance argument. -/
@[elab_as_elim]
protected def recOnSubsingleton' {φ : Quotient s₁ → Sort*} [∀ a, Subsingleton (φ ⟦a⟧)]
    (q : Quotient s₁)
    (f : ∀ a, φ (Quotient.mk'' a)) : φ q :=
  Quotient.recOnSubsingleton q f

Recursion on quotient with subsingleton condition (implicit setoid version)

Informal description

Given a type $\alpha$ with an implicit setoid $s_1$, a type family $\varphi$ on the quotient type $\text{Quotient } s_1$ such that $\varphi$ is subsingleton on each equivalence class, and an element $q$ of $\text{Quotient } s_1$, the function $\text{Quotient.recOnSubsingleton'}$ allows defining a value in $\varphi(q)$ by providing a function $f$ that defines values for all representatives $a$ of the equivalence class.

Quotient.recOnSubsingleton₂' definition

 {φ : Quotient s₁ → Quotient s₂ → Sort*} [∀ a b, Subsingleton (φ ⟦a⟧ ⟦b⟧)] (q₁ : Quotient s₁) (q₂ : Quotient s₂)
  (f : ∀ a₁ a₂, φ (Quotient.mk'' a₁) (Quotient.mk'' a₂)) : φ q₁ q₂

Full source

/-- A version of `Quotient.recOnSubsingleton₂` taking `{s₁ : Setoid α} {s₂ : Setoid α}`
as implicit arguments instead of instance arguments. -/
@[elab_as_elim]
protected def recOnSubsingleton₂' {φ : Quotient s₁ → Quotient s₂ → Sort*}
    [∀ a b, Subsingleton (φ ⟦a⟧ ⟦b⟧)]
    (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : ∀ a₁ a₂, φ (Quotient.mk'' a₁) (Quotient.mk'' a₂)) :
    φ q₁ q₂ :=
  Quotient.recOnSubsingleton₂ q₁ q₂ f

Dependent recursion on pairs of quotient elements with subsingleton condition (implicit setoid version)

Informal description

Given two quotient types $\text{Quotient } s_1$ and $\text{Quotient } s_2$ with implicit setoids $s_1$ and $s_2$, and a dependent function $\varphi$ on pairs of equivalence classes such that $\varphi \llbracket a \rrbracket \llbracket b \rrbracket$ is a subsingleton for all $a \in \alpha$ and $b \in \beta$, the function $\text{Quotient.recOnSubsingleton₂'}$ allows defining a value of type $\varphi q_1 q_2$ for any $q_1 \in \text{Quotient } s_1$ and $q_2 \in \text{Quotient } s_2$ by providing a function $f$ that defines $\varphi$ on representatives.

Quotient.hrecOn' definition

 {φ : Quotient s₁ → Sort*} (qa : Quotient s₁) (f : ∀ a, φ (Quotient.mk'' a))
  (c : ∀ a₁ a₂, a₁ ≈ a₂ → HEq (f a₁) (f a₂)) : φ qa

Full source

/-- Recursion on a `Quotient` argument `a`, result type depends on `⟦a⟧`. -/
protected def hrecOn' {φ : Quotient s₁ → Sort*} (qa : Quotient s₁) (f : ∀ a, φ (Quotient.mk'' a))
    (c : ∀ a₁ a₂, a₁ ≈ a₂ → HEq (f a₁) (f a₂)) : φ qa :=
  Quot.hrecOn qa f c

Heterogeneous recursion on quotient elements with implicit setoid

Informal description

Given a type $\alpha$ with a setoid $s_1$, a dependent type $\varphi$ on the quotient $\text{Quotient } s_1$, and a quotient element $q_a \in \text{Quotient } s_1$, the function $\text{Quotient.hrecOn'}$ allows defining a value in $\varphi(q_a)$ by providing: 1. A function $f$ that defines values for representatives: $\forall a \in \alpha, f(a) \in \varphi(\llbracket a \rrbracket)$ 2. A proof $c$ that $f$ respects the equivalence relation: $\forall a_1 a_2 \in \alpha, a_1 \approx a_2 \Rightarrow \text{HEq}(f(a_1), f(a_2))$ Here $\llbracket a \rrbracket$ denotes the equivalence class of $a$ in the quotient, and $\text{HEq}$ denotes heterogeneous equality.

Quotient.hrecOn'_mk'' theorem

 {φ : Quotient s₁ → Sort*} (f : ∀ a, φ (Quotient.mk'' a)) (c : ∀ a₁ a₂, a₁ ≈ a₂ → HEq (f a₁) (f a₂)) (x : α) :
  (Quotient.mk'' x).hrecOn' f c = f x

Full source

@[simp]
theorem hrecOn'_mk'' {φ : Quotient s₁ → Sort*} (f : ∀ a, φ (Quotient.mk'' a))
    (c : ∀ a₁ a₂, a₁ ≈ a₂ → HEq (f a₁) (f a₂))
    (x : α) : (Quotient.mk'' x).hrecOn' f c = f x :=
  rfl

Heterogeneous Recursion on Quotient Representatives with Implicit Setoid

Informal description

Given a type $\alpha$ with a setoid $s_1$, a dependent type $\varphi$ on the quotient $\text{Quotient } s_1$, a function $f \colon \forall a \in \alpha, \varphi(\llbracket a \rrbracket)$, and a proof $c$ that $f$ respects the equivalence relation (i.e., $\forall a_1 a_2 \in \alpha, a_1 \approx a_2 \Rightarrow \text{HEq}(f(a_1), f(a_2))$), then for any $x \in \alpha$, applying heterogeneous recursion to the equivalence class $\llbracket x \rrbracket$ yields $f(x)$: $$(\text{Quotient.mk'' } x).\text{hrecOn'} f c = f(x)$$

Quotient.hrecOn₂' definition

 {φ : Quotient s₁ → Quotient s₂ → Sort*} (qa : Quotient s₁) (qb : Quotient s₂)
  (f : ∀ a b, φ (Quotient.mk'' a) (Quotient.mk'' b)) (c : ∀ a₁ b₁ a₂ b₂, a₁ ≈ a₂ → b₁ ≈ b₂ → HEq (f a₁ b₁) (f a₂ b₂)) :
  φ qa qb

Full source

/-- Recursion on two `Quotient` arguments `a` and `b`, result type depends on `⟦a⟧` and `⟦b⟧`. -/
protected def hrecOn₂' {φ : Quotient s₁ → Quotient s₂ → Sort*} (qa : Quotient s₁)
    (qb : Quotient s₂) (f : ∀ a b, φ (Quotient.mk'' a) (Quotient.mk'' b))
    (c : ∀ a₁ b₁ a₂ b₂, a₁ ≈ a₂ → b₁ ≈ b₂ → HEq (f a₁ b₁) (f a₂ b₂)) :
    φ qa qb :=
  Quotient.hrecOn₂ qa qb f c

Heterogeneous recursion on two quotient elements with implicit setoids

Informal description

Given two quotient elements $qa$ and $qb$ with respect to setoids $s_1$ and $s_2$ respectively, a dependent type $\varphi$ on pairs of quotient elements, a function $f$ that defines values for pairs of representatives, and a compatibility condition $c$ ensuring that $f$ respects the equivalence relations, the function $\text{Quotient.hrecOn₂'}$ constructs an element of type $\varphi(qa, qb)$. The compatibility condition requires that for any elements $a_1, a_2$ related by $s_1$ and $b_1, b_2$ related by $s_2$, the values $f(a_1, b_1)$ and $f(a_2, b_2)$ are heterogeneously equal.

Quotient.hrecOn₂'_mk'' theorem

 {φ : Quotient s₁ → Quotient s₂ → Sort*} (f : ∀ a b, φ (Quotient.mk'' a) (Quotient.mk'' b))
  (c : ∀ a₁ b₁ a₂ b₂, a₁ ≈ a₂ → b₁ ≈ b₂ → HEq (f a₁ b₁) (f a₂ b₂)) (x : α) (qb : Quotient s₂) :
  (Quotient.mk'' x).hrecOn₂' qb f c = qb.hrecOn' (f x) fun _ _ ↦ c _ _ _ _ (Setoid.refl _)

Full source

@[simp]
theorem hrecOn₂'_mk'' {φ : Quotient s₁ → Quotient s₂ → Sort*}
    (f : ∀ a b, φ (Quotient.mk'' a) (Quotient.mk'' b))
    (c : ∀ a₁ b₁ a₂ b₂, a₁ ≈ a₂ → b₁ ≈ b₂ → HEq (f a₁ b₁) (f a₂ b₂)) (x : α) (qb : Quotient s₂) :
    (Quotient.mk'' x).hrecOn₂' qb f c = qb.hrecOn' (f x) fun _ _ ↦ c _ _ _ _ (Setoid.refl _) :=
  rfl

Heterogeneous Recursion on Quotient Pairs with Implicit Setoids: Base Case for First Argument

Informal description

Given a type $\alpha$ with a setoid $s_1$, a type $\beta$ with a setoid $s_2$, a dependent type $\varphi$ on pairs of quotient elements, and a function $f \colon \forall (a \in \alpha) (b \in \beta), \varphi(\llbracket a \rrbracket, \llbracket b \rrbracket)$ that respects the equivalence relations (i.e., $\forall a_1 a_2 b_1 b_2, a_1 \approx a_2 \land b_1 \approx b_2 \Rightarrow \text{HEq}(f(a_1, b_1), f(a_2, b_2))$), then for any $x \in \alpha$ and $q_b \in \text{Quotient } s_2$, the following equality holds: $$(\text{Quotient.mk'' } x).\text{hrecOn₂'} q_b f c = q_b.\text{hrecOn'} (f x) \left(\lambda \_ \_ \Rightarrow c \_ \_ \_ \_ (\text{Setoid.refl } \_)\right)$$ where $\llbracket a \rrbracket$ denotes the equivalence class of $a$ in $\text{Quotient } s_1$ and $\text{HEq}$ denotes heterogeneous equality.

Quotient.map' definition

(f : α → β) (h : ∀ a b, s₁.r a b → s₂.r (f a) (f b)) : Quotient s₁ → Quotient s₂

Full source

/-- 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. -/
protected def map' (f : α → β) (h : ∀ a b, s₁.r a b → s₂.r (f a) (f b)) :
    Quotient s₁ → Quotient s₂ :=
  Quot.map f h

Lifting a relation-preserving function to quotient types

Informal description

Given a function $f : \alpha \to \beta$ and equivalence relations $s_1$ on $\alpha$ and $s_2$ on $\beta$, if $f$ preserves the relations (i.e., $s_1(x,y)$ implies $s_2(f(x), f(y))$ for all $x,y \in \alpha$), then $f$ induces a map $\text{Quotient } s_1 \to \text{Quotient } s_2$ between the quotient types.

Quotient.map'_mk'' theorem

(f : α → β) (h) (x : α) : (Quotient.mk'' x : Quotient s₁).map' f h = (Quotient.mk'' (f x) : Quotient s₂)

Full source

@[simp]
theorem map'_mk'' (f : α → β) (h) (x : α) :
    (Quotient.mk'' x : Quotient s₁).map' f h = (Quotient.mk'' (f x) : Quotient s₂) :=
  rfl

Commutativity of Quotient Map with Quotient Construction

Informal description

For any function $f : \alpha \to \beta$ that preserves the relations of setoids $s_1$ on $\alpha$ and $s_2$ on $\beta$ (i.e., $s_1(a,b) \Rightarrow s_2(f(a), f(b))$ for all $a,b \in \alpha$), and for any element $x \in \alpha$, the map induced by $f$ on the quotient $\text{Quotient } s_1$ applied to the equivalence class of $x$ equals the equivalence class of $f(x)$ in $\text{Quotient } s_2$. In symbols: $\text{map}'_f h ([x]_{s_1}) = [f(x)]_{s_2}$ where $[x]_{s_1}$ denotes the equivalence class of $x$ under $s_1$.

Quotient.exact' theorem

{a b : α} : (Quotient.mk'' a : Quotient s₁) = Quotient.mk'' b → s₁ a b

Full source

theorem exact' {a b : α} :
    (Quotient.mk'' a : Quotient s₁) = Quotient.mk'' b → s₁ a b :=
  Quotient.exact

Equality in Quotient Implies Setoid Relation

Informal description

For any elements $a$ and $b$ of type $\alpha$ with a setoid $s_1$, if the equivalence classes of $a$ and $b$ in the quotient type $\text{Quotient } s_1$ are equal, then $a$ and $b$ are related by the setoid relation $s_1$.

Quotient.sound' theorem

{a b : α} : s₁ a b → @Quotient.mk'' α s₁ a = Quotient.mk'' b

Full source

theorem sound' {a b : α} : s₁ a b → @Quotient.mk'' α s₁ a = Quotient.mk'' b :=
  Quotient.sound

Equivalence Implies Equal Quotient Elements

Informal description

For any elements $a$ and $b$ of a type $\alpha$ with a setoid $s_1$, if $a$ is related to $b$ under $s_1$, then their equivalence classes in the quotient $\text{Quotient } s_1$ are equal.

Quotient.eq' theorem

{s₁ : Setoid α} {a b : α} : @Quotient.mk' α s₁ a = @Quotient.mk' α s₁ b ↔ s₁ a b

Full source

@[simp]
protected theorem eq' {s₁ : Setoid α} {a b : α} :
    @Quotient.mk' α s₁ a = @Quotient.mk' α s₁ b ↔ s₁ a b :=
  Quotient.eq

Quotient Equality Equivalence for Setoids

Informal description

For any setoid $s₁$ on a type $\alpha$ and elements $a, b \in \alpha$, the equivalence class of $a$ under $s₁$ equals the equivalence class of $b$ if and only if $a$ is related to $b$ under the setoid relation $s₁$. In symbols: $$[a]_{s₁} = [b]_{s₁} \leftrightarrow s₁(a,b)$$

Quotient.eq'' theorem

{a b : α} : @Quotient.mk'' α s₁ a = Quotient.mk'' b ↔ s₁ a b

Full source

protected theorem eq'' {a b : α} : @Quotient.mk'' α s₁ a = Quotient.mk'' b ↔ s₁ a b :=
  Quotient.eq

Quotient Equality Criterion for Implicit Setoids

Informal description

For any elements $a$ and $b$ of a type $\alpha$ with an implicit setoid $s₁$, the equivalence class of $a$ equals the equivalence class of $b$ if and only if $a$ is related to $b$ under $s₁$. In symbols: $$[a] = [b] \leftrightarrow a \sim b$$

Quotient.out_eq' theorem

(q : Quotient s₁) : Quotient.mk'' q.out = q

Full source

theorem out_eq' (q : Quotient s₁) : Quotient.mk'' q.out = q :=
  q.out_eq

Quotient Representative Equality for Implicit Setoids

Informal description

For any element $q$ of the quotient type $\mathrm{Quotient}\,s₁$ with implicit setoid $s₁$, the equivalence class of the representative selected by $\mathrm{out}$ equals $q$ itself, i.e., $[\mathrm{out}(q)] = q$.

Quotient.mk_out' theorem

(a : α) : s₁ (Quotient.mk'' a : Quotient s₁).out a

Full source

theorem mk_out' (a : α) : s₁ (Quotient.mk'' a : Quotient s₁).out a :=
  Quotient.exact (Quotient.out_eq _)

Representative of Quotient Class is Related to Original Element

Informal description

For any element $a$ of type $\alpha$ with an implicit setoid $s_1$, the representative selected from the equivalence class of $a$ in the quotient type $\text{Quotient } s_1$ is related to $a$ under $s_1$. In symbols: $$(\text{Quotient.mk'' } a).\text{out} \sim a$$

Quotient.mk''_eq_mk theorem

: Quotient.mk'' = Quotient.mk s

Full source

protected theorem mk''_eq_mk : Quotient.mk'' = Quotient.mk s :=
  rfl

Equality of Quotient Construction Functions

Informal description

The function $\text{Quotient.mk''}$ is equal to the quotient map $\text{Quotient.mk}$ with respect to the setoid $s$.

Quotient.liftOn'_mk theorem

(x : α) (f : α → β) (h) : (Quotient.mk s x).liftOn' f h = f x

Full source

@[simp]
protected theorem liftOn'_mk (x : α) (f : α → β) (h) : (Quotient.mk s x).liftOn' f h = f x :=
  rfl

Lifting a Function on Quotient Representatives Preserves Application

Informal description

For any element $x$ of type $\alpha$, function $f : \alpha \to \beta$, and proof $h$ that $f$ respects the equivalence relation $s$, the result of lifting $f$ to the quotient via `Quotient.liftOn'` applied to the equivalence class of $x$ equals $f(x)$. That is, $(\text{Quotient.mk } s\ x).\text{liftOn}' f h = f(x)$.

Quotient.liftOn₂'_mk theorem

 {t : Setoid β} (f : α → β → γ) (h) (a : α) (b : β) : Quotient.liftOn₂' (Quotient.mk s a) (Quotient.mk t b) f h = f a b

Full source

@[simp]
protected theorem liftOn₂'_mk {t : Setoid β} (f : α → β → γ) (h) (a : α) (b : β) :
    Quotient.liftOn₂' (Quotient.mk s a) (Quotient.mk t b) f h = f a b :=
  Quotient.liftOn₂'_mk'' _ _ _ _

Lifted Binary Function on Quotient Classes Equals Original Function

Informal description

Let $s$ be a setoid on $\alpha$ and $t$ a setoid on $\beta$. Given a function $f : \alpha \to \beta \to \gamma$ that respects the equivalence relations (i.e., $f\, a_1\, a_2 = f\, b_1\, b_2$ whenever $a_1 \sim_s b_1$ and $a_2 \sim_t b_2$), then for any $a \in \alpha$ and $b \in \beta$, the lifted function applied to the equivalence classes satisfies: \[ \text{Quotient.liftOn₂'}\, [a]_s\, [b]_t\, f\, h = f\, a\, b \] where $[a]_s$ and $[b]_t$ denote the equivalence classes of $a$ and $b$ under $s$ and $t$ respectively.

Quotient.map'_mk theorem

{t : Setoid β} (f : α → β) (h) (x : α) : (Quotient.mk s x).map' f h = (Quotient.mk t (f x))

Full source

theorem map'_mk {t : Setoid β} (f : α → β) (h) (x : α) :
    (Quotient.mk s x).map' f h = (Quotient.mk t (f x)) :=
  rfl

Equivalence Class Mapping via Relation-Preserving Function

Informal description

Given a function $f : \alpha \to \beta$ and equivalence relations $s$ on $\alpha$ and $t$ on $\beta$, if $f$ preserves the relations (i.e., $s(x,y)$ implies $t(f(x), f(y))$ for all $x,y \in \alpha$), then for any $x \in \alpha$, the image of the equivalence class of $x$ under the induced map $\text{Quotient.map}'$ is equal to the equivalence class of $f(x)$. That is, $(\text{Quotient.mk } s\ x).\text{map}' f h = \text{Quotient.mk } t (f x)$.

Quotient.instDecidableLiftOn'OfDecidablePred instance

 (q : Quotient s₁) (f : α → Prop) (h : ∀ a b, s₁ a b → f a = f b) [DecidablePred f] : Decidable (Quotient.liftOn' q f h)

Full source

instance (q : Quotient s₁) (f : α → Prop) (h : ∀ a b, s₁ a b → f a = f b)
    [DecidablePred f] :
    Decidable (Quotient.liftOn' q f h) :=
  Quotient.lift.decidablePred _ _ q

Decidability of Lifted Predicates on Quotients with Implicit Setoids

Informal description

For any quotient type $\alpha/{\sim}$ with respect to an equivalence relation $\sim$, a decidable predicate $f : \alpha \to \mathrm{Prop}$ that respects $\sim$ (i.e., $a \sim b$ implies $f(a) = f(b)$), and an equivalence class $q \in \alpha/{\sim}$, the lifted predicate $\mathrm{Quotient.liftOn'}\, q\, f\, h$ is decidable.

Quotient.instDecidableLiftOn₂'OfDecidablePred instance

 (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → Prop) (h : ∀ a₁ b₁ a₂ b₂, s₁ a₁ a₂ → s₂ b₁ b₂ → f a₁ b₁ = f a₂ b₂)
  [∀ a, DecidablePred (f a)] : Decidable (Quotient.liftOn₂' q₁ q₂ f h)

Full source

instance (q₁ : Quotient s₁) (q₂ : Quotient s₂) (f : α → β → Prop)
    (h : ∀ a₁ b₁ a₂ b₂, s₁ a₁ a₂ → s₂ b₁ b₂ → f a₁ b₁ = f a₂ b₂)
    [∀ a, DecidablePred (f a)] :
    Decidable (Quotient.liftOn₂' q₁ q₂ f h) :=
  Quotient.lift₂.decidablePred _ h _ _

Decidability of Lifted Binary Predicates on Quotients with Implicit Setoids

Informal description

Given two quotient types $\text{Quotient}\, s₁$ and $\text{Quotient}\, s₂$ with respect to equivalence relations $s₁$ on $\alpha$ and $s₂$ on $\beta$, a function $f : \alpha \to \beta \to \mathrm{Prop}$ that respects these equivalence relations (i.e., $f\, a₁\, b₁ = f\, a₂\, b₂$ whenever $a₁ \sim_{s₁} a₂$ and $b₁ \sim_{s₂} b₂$), and the assumption that for every $a \in \alpha$, the predicate $f(a, \cdot)$ is decidable, then the lifted function $\text{Quotient.liftOn₂'}\, q₁\, q₂\, f\, h$ is decidable.

Equivalence.quot_mk_eq_iff theorem

{α : Type*} {r : α → α → Prop} (h : Equivalence r) (x y : α) : Quot.mk r x = Quot.mk r y ↔ r x y

Full source

@[simp]
lemma Equivalence.quot_mk_eq_iff {α : Type*} {r : α → α → Prop} (h : Equivalence r) (x y : α) :
    Quot.mkQuot.mk r x = Quot.mk r y ↔ r x y := by
  constructor
  · rw [Quot.eq]
    intro hxy
    induction hxy with
    | rel _ _ H => exact H
    | refl _ => exact h.refl _
    | symm _ _ _ H => exact h.symm H
    | trans _ _ _ _ _ h₁₂ h₂₃ => exact h.trans h₁₂ h₂₃
  · exact Quot.sound

Equivalence Class Equality Criterion for Quotient Types

Informal description

For any type $\alpha$ with an equivalence relation $r$ on $\alpha$ (i.e., $r$ is reflexive, symmetric, and transitive), the equivalence classes of elements $x$ and $y$ under $r$ are equal if and only if $x$ and $y$ are related by $r$. In symbols: $$\text{Quot.mk}_r(x) = \text{Quot.mk}_r(y) \leftrightarrow r(x, y)$$

Tags