lt_def — Mathlib

English

Let α be a preorder and consider the extension WithZero α. The relation x < y holds exactly when there exists b ∈ α such that y is the embedding of b and, for every a ∈ α, if x is the embedding of a then a < b.

Русский

Пусть α — предорядок. Расширение WithZero α имеет отношение x < y, которое выполняется тогда и только тогда, когда существует b ∈ α такое, что y равно образованию b, и для каждого a ∈ α если x равно образованию a, то a < b.

LaTeX

$$$ x < y \iff \exists b : \alpha, y = \uparrow b \land \forall a : \alpha, x = \uparrow a \rightarrow a < b $$$

Lean4

theorem lt_def : x < y ↔ ∃ b : α, y = ↑b ∧ ∀ a : α, x = ↑a → a < b :=
  .rfl

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