epi_iff_surjective — Mathlib

English

For morphism f: A ⟶ B in CommGrpCat, f is epi if and only if the underlying function f.hom is surjective.

Русский

Для морфизма f: A → B в CommGrpCat, f является эпиморфизмом тогда и только тогда, когда соответствующая функция сюръективна.

LaTeX

$$$$ \mathrm{Epi}(f) \iff \mathrm{Function.Surjective}(f.\mathrm{hom}) $$$$

Lean4

@[to_additive]
theorem epi_iff_surjective : Epi f ↔ Function.Surjective f := by rw [epi_iff_range_eq_top, MonoidHom.range_eq_top]

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