epi_of_surjective — Mathlib

English

If f is an isomorphism in the category C, then the underlying function is bijective.

Русский

Если f является изоморфизмом в категории C, то соответствующая базовая функция биективна.

LaTeX

$$$\\text{IsIso}(f) \\Rightarrow \\text{Bijective}(\\underline{f})$$$

Lean4

/-- In any concrete category, surjective morphisms are epimorphisms. -/
theorem epi_of_surjective {X Y : C} (f : X ⟶ Y) (s : Function.Surjective f) : Epi f :=
  (forget C).epi_of_epi_map ((epi_iff_surjective ((forget C).map f)).2 s)

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