not_bddAbove_of_tendsto_atTop — Mathlib

English

If β has no maximum (NoMaxOrder) and f tends to atTop along l, then range f is unbounded above.

Русский

Если у β нет максимального элемента (NoMaxOrder) и f стремится к верхней грани вдоль l, тогда множество значений f не ограничено сверху.

LaTeX

$$$$[NoMaxOrder(\beta)]\to (\operatorname{Tendsto} f\ l\ \\text{atTop} \Rightarrow \neg \operatorname{BddAbove}(\operatorname{range} f))$$$$

Lean4

theorem not_bddAbove_of_tendsto_atTop [NoMaxOrder β] (h : Tendsto f l atTop) : ¬BddAbove (range f) :=
  by
  rintro ⟨M, hM⟩
  have : ∀ x, f x ≤ M := by aesop
  have : ∅ = f ⁻¹' Ioi M := by aesop (add forward safe not_le_of_gt)
  apply Filter.empty_notMem l
  aesop (add safe Ioi_mem_atTop)

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