isAtom_dual_iff_isCoatom — Mathlib

English

In a preorder with a top element, an element a is an atom in the dual order if and only if it is a coatom in the original order.

Русский

В частично упорядоченном множестве с верхней границей элемент a является атомом в двойственном порядке тогда и только тогда, когда он является коатомом в исходном порядке.

LaTeX

$$$IsAtom(OrderDual.toDual(a)) \; \Leftrightarrow \; IsCoatom(a)$$$

Lean4

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

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