English
If f is surjective and c ≤ ker f, then the lift c.lift f h is also surjective onto P.
Русский
Если f сюръективно и c ≤ ker f, то лифт c.lift f h также образует сюръективное отображение на P.
LaTeX
$$$\text{lift_surjective_of_surjective } h hf : Surjective (c.lift f h)$$$
Lean4
/-- Surjective monoid homomorphisms constant on a congruence relation `c`'s equivalence classes
induce a surjective homomorphism on `c`'s quotient. -/
@[to_additive /-- Surjective `AddMonoid` homomorphisms constant on an additive congruence
relation `c`'s equivalence classes induce a surjective homomorphism on `c`'s quotient. -/
]
theorem lift_surjective_of_surjective (h : c ≤ ker f) (hf : Surjective f) : Surjective (c.lift f h) := fun y =>
(Exists.elim (hf y)) fun w hw => ⟨w, (lift_mk' h w).symm ▸ hw⟩
