under — Mathlib

English

If C is filtered or empty, then for any object c in C the under category Under c is filtered.

Русский

Если C фильтрована или пустая, то для любого объекта c ∈ C категория подмножество Under c является фильтрованной.

LaTeX

$$[IsFilteredOrEmpty C] (c ∈ C) → IsFiltered(Under c)$$

Lean4

/-- Any under category on a filtered or empty category is filtered.
(Note that under categories are always cofiltered since they have an initial object.) -/
instance under [IsFilteredOrEmpty C] (c : C) : IsFiltered (Under c) :=
  isFiltered_structuredArrow_of_isFiltered_of_exists _ (fun c' => ⟨c', ⟨𝟙 _⟩⟩)
    (fun s s' => IsFilteredOrEmpty.cocone_maps s s') c

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