of_equivalence — Mathlib

English

If C and D are equivalent categories 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

/-- Being cofiltered or empty is preserved by equivalence of categories. -/
theorem of_equivalence (h : C ≌ D) : IsCofilteredOrEmpty D :=
  of_left_adjoint h.toAdjunction

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