isLUB_norm — Mathlib

English

For nonempty index set, the lp∞ norm is the least upper bound of the set {‖f i‖}.

Русский

Для непустого множества индексов норма lp∞ равна наименьшему верхнему пределу множества {‖f_i‖}.

LaTeX

$$$$ \|f\| = \sup_i \|f_i\|. $$$$

Lean4

theorem isLUB_norm [Nonempty α] (f : lp E ∞) : IsLUB (Set.range fun i => ‖f i‖) ‖f‖ :=
  by
  rw [lp.norm_eq_ciSup]
  exact isLUB_ciSup (lp.memℓp f)

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