isBoundedUnder_ge_atTop

Mathlib.Order.Filter.IsBounded

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

English

If a function tends to atTop along f, then it is bounded below with respect to ≥.

Русский

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

LaTeX

$$$\text{Tendsto } u\ f\ atTop \Rightarrow f.IsBoundedUnder(\ge)\ u$$$

Lean4

theorem isBoundedUnder_ge_atTop (h : Tendsto u f atTop) : f.IsBoundedUnder (· ≥ ·) u :=
  isBounded_ge_atTop.mono h

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

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

Разделы

Аффилиация

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