isCoatom_iff_ge_of_le — Mathlib

English

In a preorder with a top element, a is a coatom if and only if a ≠ ⊤ and for all b ≠ ⊤, a ≤ b ⇒ b ≤ a.

Русский

В частично упорядоченном множестве с верхним элементом a является коатомом тогда, когда a ≠ ⊤ и для всех b ≠ ⊤ выполняется a ≤ b ⇒ b ≤ a.

LaTeX

$$IsCoatom a ↔ a \neq ⊤ ∧ ∀ b ≠ ⊤, a ≤ b → b ≤ a$$

Lean4

theorem isCoatom_iff_ge_of_le : IsCoatom a ↔ a ≠ ⊤ ∧ ∀ b ≠ ⊤, a ≤ b → b ≤ a :=
  isAtom_iff_le_of_ge (α := αᵒᵈ)

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