isSplitEpi_toSimplexCategory_map_of_P_σ

English

If e has P_σ, then toSimplexCategory.map e is a split epi.

Русский

Если e имеет P_σ, то toSimplexCategory.map e является разложимым эпиморфизмом.

LaTeX

$$$\mathrm{IsSplitEpi} \bigl( \mathrm{toSimplexCategory.map}(e) \bigr)$$$

Lean4

theorem isSplitEpi_toSimplexCategory_map_of_P_σ {x y : SimplexCategoryGenRel} {e : x ⟶ y} (he : P_σ e) :
    IsSplitEpi <| toSimplexCategory.map e := by
  constructor
  constructor
  apply SplitEpi.map
  exact isSplitEpi_P_σ he |>.exists_splitEpi.some

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