instEpiFactorThruImage — Mathlib

English

For every morphism θ: Δ→Δ' the canonical factorization through its image is epi.

Русский

Для любого морфизма θ: Δ→Δ' каноническая факторизация через образ θ является эпиморфизмом.

LaTeX

$$$\\forall \\Delta,\\Delta',\\theta:\\Delta\\to\\Delta',\\ Epi(\\mathrm{factorThruImage}\\,\\theta).$$$

Lean4

instance (Δ Δ' : SimplexCategory) (θ : Δ ⟶ Δ') : Epi (factorThruImage θ) :=
  StrongEpi.epi

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