epi_of_surjective — Mathlib

English

Every surjective morphism in CompHausLike P is an epimorphism.

Русский

Любой сюръективный морфизм в CompHausLike P является эпиморфизмом.

LaTeX

$$$\forall {P},\ {X,Y : CompHausLike P},\ f:\,X \to Y,\ Surjective(f) \Rightarrow Epi(f)$$$

Lean4

theorem epi_of_surjective {X Y : CompHausLike.{u} P} (f : X ⟶ Y) (hf : Function.Surjective f) : Epi f :=
  by
  rw [← CategoryTheory.epi_iff_surjective] at hf
  exact (forget (CompHausLike P)).epi_of_epi_map hf

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