initial_post — Mathlib

English

CostructuredArrow.post T S X is initial if T and S are initial and the domain of T is cofiltered.

Русский

CostructuredArrow.post T S X начален, если T и S начальны, а область определения T кофакторна.

LaTeX

$$∧[IsCofiltered C] {E} [CategoryTheory.Category E] (X : D) (T : C ⥤ D) [T.Initial] (S : D ⥤ E) [S.Initial] ⇒ Initial (post T S X)$$

Lean4

/-- `CostructuredArrow.post T S X` is initial if `T` and `S` are initial and the domain of `T` is
cofiltered. -/
instance initial_post [IsCofiltered C] {E : Type u₃} [Category.{v₃} E] (X : D) (T : C ⥤ D) [T.Initial] (S : D ⥤ E)
    [S.Initial] : Initial (post T S X) := by apply initial_of_natIso (postIsoMap₂ X T S).symm

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