instHasFactorizationP_σP_δ — Mathlib

English

There is an instance providing that every morphism admits a P_σ ∘ P_δ factorization.

Русский

Существуют данные экземпляра, обеспечивающие разложение каждого морфизма через P_σ ∘ P_δ.

LaTeX

$$$\text{SimplexCategoryGenRel.P_σ.HasFactorization SimplexCategoryGenRel.P_δ}$$$

Lean4

instance : MorphismProperty.HasFactorization P_σ P_δ where
  nonempty_mapFactorizationData
    f := by
    obtain ⟨z, e, m, he, hm, fac⟩ := exists_P_σ_P_δ_factorization f
    exact ⟨⟨z, e, m, fac.symm, he, hm⟩⟩

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