bddAbove

Mathlib.Analysis.Normed.Lp.lpSpace

URI: https://scilib.ai/kg/mathlib#Memℓp.bddAbove

English

If Memℓp f ∞, then the norms ‖f(i)‖ are bounded above.

Русский

Если Memℓp f ∞, то нормы ‖f(i)‖ ограничены сверху.

LaTeX

$$$$ \mathrm{Mem}_{\ell^p}(f,\infty) \Rightarrow \mathrm{BddAbove}(\{ \|f(i)\| : i \}). $$$$

Lean4

theorem bddAbove {f : ∀ i, E i} (hf : Memℓp f ∞) : BddAbove (Set.range fun i => ‖f i‖) :=
  memℓp_infty_iff.1 hf

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

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

Разделы

Аффилиация

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