initial_snd — Mathlib

English

The functor Prod.snd is initial under dual cofiltred/empty assumptions with the first category cofiltered.

Русский

Функтор Prod.snd инициален при соответствующих условиях cofiltro/empty и второйкатегории фильтрована.

LaTeX

$$$[IsCofiltered(C)] [IsCofilteredOrEmpty(D)] \Rightarrow (\mathrm{Prod.snd}\, C\, D).Initial$$$

Lean4

instance initial_snd [IsCofiltered C] [IsCofilteredOrEmpty D] : (Prod.snd C D).Initial :=
  inferInstanceAs ((Prod.braiding C D).functor ⋙ Prod.fst D C).Initial

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