epi_of_epi_left — Mathlib

English

If f.left is epi, then f is epi (under typical additional assumptions).

Русский

Если f.left эпиморфизм, то и f является эпиморфизм (при обычных дополнительных предпосылках).

LaTeX

$$$\\mathrm{Epi}(f.left) \\Rightarrow \\mathrm{Epi}(f)$$$

Lean4

/-- The converse of this is true with additional assumptions, see `epi_iff_epi_left`. -/
theorem epi_of_epi_left {A B : CostructuredArrow S T} (f : A ⟶ B) [h : Epi f.left] : Epi f :=
  (proj S T).epi_of_epi_map h

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