isSplitMono_P_δ — Mathlib

English

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

Русский

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

LaTeX

$$$\mathrm{IsSplitMono}(m) \quad\text{when } m \text{ has } P_\delta$$$

Lean4

/-- All `P_δ` are split monos as composition of such. -/
theorem isSplitMono_P_δ {x y : SimplexCategoryGenRel} {m : x ⟶ y} (hm : P_δ m) : IsSplitMono m := by
  induction hm with
  | of x hx => cases hx; infer_instance
  | id => infer_instance
  | comp_of _ _ _ h => cases h; infer_instance

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