norm_norm' — Mathlib

English

Let s be a finite set, f: s→E, n: s→NNReal, and suppose ∀ b∈s, ‖f(b)‖₊ ≤ n(b). Then ‖∏ b∈s f(b)‖₊ ≤ ∑ b∈s n(b).

Русский

Пусть s~конечное, f: s→E, n:s→ℝ≥0, и предположим ∀ b∈s, ‖f(b)‖₊ ≤ n(b). Тогда ‖∏ b∈s f(b)‖₊ ≤ ∑ b∈s n(b).

LaTeX

$$$\displaystyle \forall s:\ Finset\ ι,\; \forall f:\ ι\to E,\; \forall n:\ ι\to ℝ_{≥0},\; (\forall b∈s,\; \|f(b)\|_+ ≤ n(b)) \Rightarrow \|\prod_{b∈s} f(b)\|_+ ≤ \sum_{b∈s} n(b).$$$

Lean4

@[to_additive (attr := simp high) norm_norm] -- Higher priority as a shortcut lemma.

theorem norm_norm' (x : E) : ‖‖x‖‖ = ‖x‖ :=
  Real.norm_of_nonneg (norm_nonneg' _)

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