isLUB_image_Iio_of_isSuccLimit — Mathlib

English

If f is normal, then the image of the interval Iio under f has f(a) as its least upper bound.

Русский

Если f нормальна, образ Iio под действием f имеет f(a) как наименьшую верхнюю грань.

LaTeX

$$$\IsLUB\left( f''Iio(a) , f(a) \right)$$$

Lean4

theorem isLUB_image_Iio_of_isSuccLimit {f : α → β} (hf : IsNormal f) {a : α} (ha : IsSuccLimit a) :
    IsLUB (f '' Iio a) (f a) := by
  refine ⟨?_, hf.2 ha⟩
  rintro - ⟨b, hb, rfl⟩
  exact (hf.1 hb).le

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