norm_le_of_forall_le' — Mathlib

English

If every coordinate ≤ C, then ‖f‖ ≤ C. More precisely, for Nonempty α, given C with ∀ i, ‖f i‖ ≤ C, we have ‖f‖ ≤ C.

Русский

Если все координаты ограничены сверху на C, то ‖f‖ ≤ C.

LaTeX

$$$$ \forall i, \|f_i\| \le C \quad \Rightarrow \quad \|f\| \le C. $$$$

Lean4

theorem norm_le_of_forall_le' [Nonempty α] {f : lp E ∞} (C : ℝ) (hCf : ∀ i, ‖f i‖ ≤ C) : ‖f‖ ≤ C :=
  by
  refine (isLUB_norm f).2 ?_
  rintro - ⟨i, rfl⟩
  exact hCf i

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