Theorems · Theorem · general topology

IsUltrametricDist.norm_sum_le_of_forall_le_of_nonneg

∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ι → M}
  {C : ℝ}, 0 ≤ C → (∀ i ∈ s, ‖f i‖ ≤ C) → ‖∑ i ∈ s, f i‖ ≤ C

Generalised ultrametric triangle inequality for finite sums in additive commutative groups with an ultrametric norm.

Defined in

Mathlib.Analysis.Normed.Group.Ultra

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupIsUltrametricDist