isLUB_Iio_iff_isSuccPrelimit — Mathlib

English

For a linear order, IsLUB(Iio(a)) a is equivalent to IsSuccPrelimit a.

Русский

Для линейного порядка эквивалентны IsLUB(Iio(a)) a и IsSuccPrelimit a.

LaTeX

$$$\IsLUB(\Iio a, a) \iff \IsSuccPrelimit(a)$$$

Lean4

theorem isLUB_Iio_iff_isSuccPrelimit : IsLUB (Iio a) a ↔ IsSuccPrelimit a :=
  by
  refine ⟨fun ha b hb ↦ ?_, IsSuccPrelimit.isLUB_Iio⟩
  rw [hb.Iio_eq] at ha
  obtain rfl := isLUB_Iic.unique ha
  cases hb.lt.false

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