nonempty_lt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance nonempty_lt [LT α] [NoMinOrder α] (a : α) : Nonempty { x // x < a } :=
  nonempty_subtype.2 (exists_lt a)

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