epi_iff_surjective — Mathlib

English

In AddGrpCat, epi f is equivalent to the underlying function being surjective.

Русский

В AddGrpCat эпиморфизм f эквивалентен сюръективности соответствующей функции.

LaTeX

$$$$ \text{epi}(f) \iff \text{Surjective}(f). $$$$

Lean4

theorem epi_iff_surjective : Epi f ↔ Function.Surjective f :=
  by
  have i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f) :=
    by
    refine ⟨?_, groupAddGroupEquivalence.inverse.epi_of_epi_map⟩
    intro e'
    apply groupAddGroupEquivalence.inverse.map_epi
  rwa [GrpCat.epi_iff_surjective] at i1

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