English
The uniqueness part of the universal property for quotients: if H ≤ ker f and g: Quotient r → β with f = g ∘ mk, then Quotient.lift f H = g.
Русский
Единичность отображения в фактор-множстве: если H ≤ ker f и g: Quotient r → β удовлетворяет f = g ∘ mk, то Quotient.lift f H = g.
LaTeX
$$$$ Quotient.lift f H = g. $$$$
Lean4
/-- The uniqueness part of the universal property for quotients of an arbitrary type. -/
theorem lift_unique {r : Setoid α} {f : α → β} (H : r ≤ ker f) (g : Quotient r → β) (Hg : f = g ∘ Quotient.mk'') :
Quotient.lift f H = g := by
ext ⟨x⟩
rw [← Quotient.mk, Quotient.lift_mk f H, Hg, Function.comp_apply, Quotient.mk''_eq_mk]
