of_isLeftAdjoint — Mathlib

English

If C ≌ D and C is cofiltered or empty, then D is cofiltered or empty.

Русский

Если C эквивалентна D и C кофильтрована или пуста, тогда D кофильтрована или пуста.

LaTeX

$$$\text{Equivalence}(C,D) \land \mathrm{IsCofilteredOrEmpty}(C) \Rightarrow \mathrm{IsCofilteredOrEmpty}(D)$$$

Lean4

/-- If `C` is cofiltered, and we have a left adjoint functor `L : C ⥤ D`, then `D` is cofiltered. -/
theorem of_isLeftAdjoint (L : C ⥤ D) [L.IsLeftAdjoint] : IsCofiltered D :=
  of_left_adjoint (Adjunction.ofIsLeftAdjoint L)

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