isBoundedUnder

Mathlib.Order.Filter.IsBounded

URI: https://scilib.ai/kg/mathlib#BddBelow.isBoundedUnder

← MathLib Explorer

English

If s ∈ f and u''s is bounded below, then f is bounded under ≥ by u.

Русский

Если s ∈ f и u''s ограничено снизу, то f ограничен снизу по ≥ через u.

LaTeX

$$$ (s \in f) \land BddBelow (u'' s) \Rightarrow f.IsBoundedUnder (\ge) u $$$

Lean4

theorem _root_.BddBelow.isBoundedUnder (hs : s ∈ f) (hu : BddBelow (u '' s)) : f.IsBoundedUnder (· ≥ ·) u :=
  isBoundedUnder_iff_eventually_bddBelow.2 ⟨_, hu, hs⟩

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

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

Разделы

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

Аффилиация

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