isCoatom_dual_iff_isAtom — Mathlib

English

An element is an atom in the original order if and only if it is a coatom in the dual order (OrderDual).

Русский

Элемент является атомом в исходном порядке тогда и только тогда, когда он является коатомом в двойственном порядке.

LaTeX

$$$ \\mathrm{IsAtom}(a^{\\mathrm{op}}) \\iff \\mathrm{IsCoatom}(a) $$$

Lean4

@[simp]
theorem isCoatom_dual_iff_isAtom [OrderBot α] {a : α} : IsCoatom (OrderDual.toDual a) ↔ IsAtom a :=
  Iff.rfl

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