norm_prod_eq_sup'_of_pairwise_ne — Mathlib

English

When norms are pairwise distinct, the norm of the product equals the supremum over the finite set of the norms of the factors.

Русский

Если нормы попарно различны, то норма произведения равна supremum норм множителей.

LaTeX

$$$\\text{If } s \\neq \\varnothing \\text{ and } (s.toSet).Pairwise (\\|f(i)\\|) \\Rightarrow \\|\\prod_{i\\in s} f(i)\\| = s.sup' (\\|f(i)\\|)$$$

Lean4

@[to_additive]
theorem norm_prod_eq_sup'_of_pairwise_ne {s : Finset ι} {f : ι → M} (hs' : s.Nonempty)
    (hs : Set.Pairwise s (fun i j ↦ ‖f i‖ ≠ ‖f j‖)) : ‖∏ i ∈ s, f i‖ = s.sup' hs' (fun i ↦ ‖f i‖) :=
  by
  rw [← coe_nnnorm', nnnorm_prod_eq_sup_of_pairwise_ne, ← Finset.sup'_eq_sup hs']
  · exact s.comp_sup'_eq_sup'_comp hs' _ (by tauto)
  · simpa [← NNReal.coe_inj] using hs

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