final_snd — 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

$$Final (StructuredArrow.post X T S) under [T.Final], [S.Final], [IsFiltered] on domain of T.$$

Lean4

instance final_snd [IsFiltered C] [IsFilteredOrEmpty D] : (Prod.snd C D).Final :=
  inferInstanceAs ((Prod.braiding C D).functor ⋙ Prod.fst D C).Final

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