final_diag_of_isFiltered — Mathlib

English

The diagonal functor on any filtered category is final.

Русский

Диагональный функтор на любой фильтрованной категории финален.

LaTeX

$$Final (Functor.diag C)$$

Lean4

/-- The diagonal functor on any filtered category is final. -/
instance final_diag_of_isFiltered [IsFilteredOrEmpty C] : Final (Functor.diag C) :=
  final_of_isFiltered_structuredArrow
    _
      -- Adding this instance causes performance problems elsewhere, even with low priority

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