epi_iff_range_eq_top — Mathlib

English

For any f: A ⟶ B in GrpCat, epi f is equivalent to the range of f being the top subgroup.

Русский

Для любого f: A ⟶ B в GrpCat, epi f эквивалентно тому, что образ f равен верхней подгруппе (top).

LaTeX

$$$$ \text{Epi}(f) \iff f.\operatorname{hom.range} = \top. $$$$

Lean4

theorem epi_iff_range_eq_top : Epi f ↔ f.hom.range = ⊤ :=
  Iff.trans (epi_iff_surjective _) (Subgroup.eq_top_iff' f.hom.range).symm

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