isFilteredOrEmpty_of_isCofilteredOrEmpty_op

English

If Cᵒᵖ is cofiltered or empty, then C is filtered or empty.

Русский

Если Cᵒᵖ кофильтрована или пуста, то C фильтрована или пуста.

LaTeX

$$[IsCofilteredOrEmpty C^{op}] ⇒ IsFilteredOrEmpty C$$

Lean4

/-- If Cᵒᵖ is cofiltered or empty, then C is filtered or empty. -/
theorem isFilteredOrEmpty_of_isCofilteredOrEmpty_op [IsCofilteredOrEmpty Cᵒᵖ] : IsFilteredOrEmpty C :=
  IsFilteredOrEmpty.of_equivalence (opOpEquivalence _)

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