mk''_surjective — Mathlib

English

The map a ↦ ⟦a⟧ (Quotient.mk'') is surjective onto the quotient; every quotient class has a representative.

Русский

Отображение a ↦ ⟦a⟧ (Quotient.mk'') оно сюръективно на множества факторов; каждая класс экваментности имеет представителя.

LaTeX

$$$\\forall q:\\,\\operatorname{Quotient}(s_1),\\ \\exists a:\\,\\alpha,\\ \\operatorname{Quotient.mk''} a = q$$$

Lean4

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

Похожие утверждения