English
An atom of an OrderBot is a non-bottom element with no element strictly between bottom and it.
Русский
Атом порядка OrderBot — это ненулевой элемент без элементов строго между ⊥ и ним.
LaTeX
$$$\\text{IsAtom}(a) \\;:=\\; a \\neq \\bot \\land \\forall b,\\; b < a \\Rightarrow b = \\bot.$$$
Lean4
/-- An atom of an `OrderBot` is an element with no other element between it and `⊥`,
which is not `⊥`. -/
def IsAtom (a : α) : Prop :=
a ≠ ⊥ ∧ ∀ b, b < a → b = ⊥