isLUB_Iio — Mathlib

English

If a is a successor-prelimit, then a is the least upper bound of the open interval Iio(a).

Русский

Если a является SuccPrelimit, то a является наименьшей верхней границей множества Iio(a).

LaTeX

$$$\IsSuccPrelimit(a) \Rightarrow \IsLUB(\Iio a)\ a$$$

Lean4

theorem isLUB_Iio (ha : IsSuccPrelimit a) : IsLUB (Iio a) a :=
  by
  refine ⟨fun _ ↦ le_of_lt, fun b hb ↦ le_of_forall_lt fun c hc ↦ ?_⟩
  obtain ⟨d, hd, hd'⟩ := ha.lt_iff_exists_lt.1 hc
  exact hd'.trans_le (hb hd)

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