isLUB_Iio — Mathlib

English

Let γ be a linear order with density. Then for every a ∈ γ, a is the least upper bound of Iio(a) = { x ∈ γ | x < a }.

Русский

Пусть γ — линейный упорядоченный плотный порядок. Тогда для любого a ∈ γ число a является наименьшей верхней границей множества Iio(a) = { x | x < a }.

LaTeX

$$$ IsLUB(Iio(a))\ a. $$$

Lean4

theorem isLUB_Iio {a : γ} : IsLUB (Iio a) a :=
  ⟨fun _ hx => le_of_lt hx, fun _ hy => le_of_forall_lt_imp_le_of_dense hy⟩

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