surjective_of_epi — Mathlib

English

If f is an epimorphism in GrpCat, then the underlying function f is surjective.

Русский

Если f является эпиморфизмом в GrpCat, то соответствующая функция f сюръективна.

LaTeX

$$$$ \text{Epi}(f) \Rightarrow \text{Surjective}(f). $$$$

Lean4

theorem surjective_of_epi [Epi f] : Function.Surjective f :=
  by
  by_contra r
  dsimp [Function.Surjective] at r
  push_neg at r
  rcases r with ⟨b, hb⟩
  exact
    SurjectiveOfEpiAuxs.g_ne_h f b (fun ⟨c, hc⟩ => hb _ hc)
      (congr_arg GrpCat.Hom.hom ((cancel_epi f).1 (SurjectiveOfEpiAuxs.comp_eq f)))

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