final_post — Mathlib

English

StructuredArrow.post X T S is final if T and S are final and the domain of T is filtered.

Русский

StructuredArrow.post X T S финален, если T и S финальны, а домен T фильтрован.

LaTeX

$$[IsFiltered C] {E} [CategoryTheory.Category E] (X : D) (T : C ⥤ D) [T.Final] (S : D ⥤ E) [S.Final] ⇒ Final (StructuredArrow.post X T S)$$

Lean4

/-- `StructuredArrow.post X T S` is final if `T` and `S` are final and the domain of `T` is
filtered. -/
instance final_post [IsFiltered C] {E : Type u₃} [Category.{v₃} E] (X : D) (T : C ⥤ D) [T.Final] (S : D ⥤ E) [S.Final] :
    Final (post X T S) := by apply final_of_natIso (postIsoMap₂ X T S).symm

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