unbounded_lt_univ — Mathlib

English

Let α be a preorder with no top element. Then for every a in α there exists b in α such that a < b.

Русский

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

LaTeX

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

Lean4

theorem unbounded_lt_univ [Preorder α] [NoTopOrder α] : Unbounded (· < ·) (@Set.univ α) :=
  unbounded_lt_of_unbounded_le unbounded_le_univ

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