not_bddBelow_of_tendsto_atBot — Mathlib

English

Dually, if β has no minimum (NoMinOrder) and f tends to atBot, then range f is unbounded below.

Русский

Аналогично понижению: если у β нет минимального элемента (NoMinOrder) и f стремится к нижней грани вдоль l, тогда множество значений f не ограничено снизу.

LaTeX

$$$$[NoMinOrder(\beta)]\to (\operatorname{Tendsto} f\ l\ atBot) \Rightarrow \neg \operatorname{BddBelow}(\operatorname{range} f)$$$$

Lean4

theorem not_bddBelow_of_tendsto_atBot [NoMinOrder β] (h : Tendsto f l atBot) : ¬BddBelow (range f) :=
  not_bddAbove_of_tendsto_atTop (β := βᵒᵈ) h

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