isSplitMono_toSimplexCategory_map_of_P_δ

English

If m has P_δ, then toSimplexCategory.map m is a split mono.

Русский

Если m обладает P_δ, то toSimplexCategory.map m является разложимым моно.

LaTeX

$$$\mathrm{IsSplitMono} \bigl( \mathrm{toSimplexCategory.map}(m) \bigr)$$$

Lean4

theorem isSplitMono_toSimplexCategory_map_of_P_δ {x y : SimplexCategoryGenRel} {m : x ⟶ y} (hm : P_δ m) :
    IsSplitMono <| toSimplexCategory.map m := by
  constructor
  constructor
  apply SplitMono.map
  exact isSplitMono_P_δ hm |>.exists_splitMono.some

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