isBoundedUnder_le_atBot

Mathlib.Order.Filter.IsBounded

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

English

If a function tends to atBot along f, then it is bounded above with respect to ≤.

Русский

Если функция стремится к atBot по фильтру f, то она ограничена сверху по ≤.

LaTeX

$$$\text{Tendsto } u\ f\ atBot \Rightarrow f.IsBoundedUnder(≤)\ u$$$

Lean4

theorem isBoundedUnder_le_atBot (h : Tendsto u f atBot) : f.IsBoundedUnder (· ≤ ·) u :=
  isBounded_le_atBot.mono h

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

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

Разделы

Аффилиация

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