isCoatomistic_dual_iff_isAtomistic

English

In the presence of OrderBot, IsCoatomistic αᵒᵈ ↔ IsAtomistic α.

Русский

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

LaTeX

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

Lean4

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

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