nonempty_gt — Mathlib

English

Let α be a type with a linear order and no maximum. Then for every a ∈ α, there exists b ∈ α with a < b.

Русский

Пусть α имеет линейный порядок и не содержит максимального элемента. Тогда для каждого a ∈ α существует b ∈ α такой, что a < b.

LaTeX

$$$\forall a \in \alpha\,\exists b \in \alpha:\, a < b$$$

Lean4

instance nonempty_gt [LT α] [NoMaxOrder α] (a : α) : Nonempty { x // a < x } :=
  nonempty_subtype.2 (exists_gt a)

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