Theorems · Theorem · functional analysis

BoundedContinuousFunction.nnnorm_sum_eq_sup

∀ {α : Type u} [inst : TopologicalSpace α] {R : Type u_1} [inst_1 : NonUnitalSeminormedRing R] [IsCancelMulZero R]
  {ι : Type u_2} {f : ι → BoundedContinuousFunction α R} (s : Finset ι),
  Pairwise (Function.onFun (fun x1 x2 => x1 * x2 = 0) f) → ‖∑ i ∈ s, f i‖₊ = s.sup fun x => ‖f x‖₊

If the pairwise products of bounded continuous functions are all zero, then the norm of their sum is the maximum of their norms.

Defined in

Mathlib.Topology.ContinuousMap.Bounded.Normed

Cited by

0 results in Mathlib

Foundations

Depth 178 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceNonUnitalSeminormedRingIsCancelMulZero