bddAbove_range

Mathlib.Topology.Order.LiminfLimsup

URI: https://scilib.ai/kg/mathlib#Filter.Tendsto.bddAbove_range

← MathLib Explorer

English

If a Tendsto to nhds a holds, then the range is bounded above.

Русский

Если есть стремление к nhds a, то множество значений ограничено сверху.

LaTeX

$$$$ \operatorname{Tendsto} u\, f\, (nhds a) \Rightarrow BddAbove(\text{range } u). $$$$

Lean4

theorem bddAbove_range [IsDirected α (· ≤ ·)] {u : ℕ → α} (h : Tendsto u atTop (𝓝 a)) : BddAbove (Set.range u) :=
  h.isBoundedUnder_le.bddAbove_range

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru