memℓp_infty_iff — Mathlib

English

For a family f, membership in ℓ^p with exponent ∞ is equivalent to the family (‖f(i)‖) being bounded.

Русский

Для функции f условие принадлежности к ℓ^p на бесконечном индексе эквивалентно тому, что множество значений ‖f(i)‖ ограничено сверху.

LaTeX

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

Lean4

theorem memℓp_infty_iff {f : ∀ i, E i} : Memℓp f ∞ ↔ BddAbove (Set.range fun i => ‖f i‖) := by simp [Memℓp]

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