IsCoatom — Mathlib

English

A coatom is an element not equal to the top, such that there is no element strictly between it and the top.

Русский

Коатом — это элемент, не равный верхнему, для которого не существует элемента между ним и верхом.

LaTeX

$$$ a \\neq \\top \\land \\forall b, a < b \\rightarrow b = \\top $$$

Lean4

/-- A coatom of an `OrderTop` is an element with no other element between it and `⊤`,
  which is not `⊤`. -/
def IsCoatom [OrderTop α] (a : α) : Prop :=
  a ≠ ⊤ ∧ ∀ b, a < b → b = ⊤

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