IsAtom — Mathlib

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 = ⊥

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