English
If φ: Δ→Δ'' factors as φ = e ≫ i with e epi and i mono, then the image of φ is Δ'.
Русский
Если φ: Δ→Δ'' факторизуется как φ = e ∘ i с e эпиморфизмом и i моно, то образ φ равен Δ'.
LaTeX
$$$\\forall \\Delta,\\Delta' ,\\Delta'' ,\\phi:\\Delta\\to\\Delta'',\\ (\\exists e:\\Delta\\to\\Delta',\\text{ epi},\\exists i:\\Delta'\\to\\Delta'',\\text{ mono})\\text{ with } \\phi=e\\circ i \\Rightarrow \\mathrm{image}\\,\\phi=\\Delta'.$$$
Lean4
theorem image_eq {Δ Δ' Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ Δ'} [Epi e] {i : Δ' ⟶ Δ''} [Mono i]
(fac : e ≫ i = φ) : image φ = Δ' := by
haveI := strongEpi_of_epi e
let e := image.isoStrongEpiMono e i fac
ext
exact le_antisymm (len_le_of_epi e.hom) (len_le_of_mono e.hom)