isAtomistic_dual_iff_isCoatomistic

English

With OrderTop α, IsAtomistic(OrderDual α) ↔ IsCoatomistic α.

Русский

При наличии OrderTop α: IsAtomistic(OrderDual α) ⇔ IsCoatomistic α.

LaTeX

$$$[OrderTop \\alpha] \\Rightarrow (\\mathrm{IsAtomistic}(\\alpha^\\mathrm{op}) \\iff \\mathrm{IsCoatomistic}(\\alpha))$$$

Lean4

@[simp]
theorem isAtomistic_dual_iff_isCoatomistic [OrderTop α] : IsAtomistic αᵒᵈ ↔ IsCoatomistic α :=
  ⟨fun h => ⟨fun b => by apply h.isLUB_atoms⟩, fun h => ⟨fun b => by apply h.isGLB_coatoms⟩⟩

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