instIsCofilteredOrEmptyFullSubcategoryCofilteredClosure

English

The full subcategory induced by the cofiltered closure of a family is cofiltered-or-empty.

Русский

Полная подпредкатегория, порождённая кофильтрованным замыканием семейства, является кофильтрованной или пустой.

LaTeX

$$$\\operatorname{IsCofilteredOrEmpty}((\\mathrm{cofilteredClosure} f).\\mathrm{FullSubcategory})$$$

Lean4

/-- The full subcategory induced by the cofiltered closure of a family is cofiltered. -/
instance : IsCofilteredOrEmpty (cofilteredClosure f).FullSubcategory
    where
  cone_objs j j' := ⟨⟨min j.1 j'.1, cofilteredClosure.min j.2 j'.2⟩, minToLeft _ _, minToRight _ _, trivial⟩
  cone_maps {j j'} f f' := ⟨⟨eq f f', cofilteredClosure.eq j.2 j'.2 f f'⟩, eqHom (C := C) f f', eq_condition _ _⟩

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