isCofilteredOrEmpty_of_isFilteredOrEmpty_op

English

If C is IsFilteredOrEmpty, then Cᵒᵖ is IsCofilteredOrEmpty.

Русский

Если C является IsFilteredOrEmpty, то Cᵒᵖ является IsCofilteredOrEmpty.

LaTeX

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

Lean4

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

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