Theorems · Theorem · general topology

IsUltrametricDist.exists_norm_finsetSum_le_of_nonempty

∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] {t : Finset ι},
  t.Nonempty → ∀ (f : ι → M), ∃ i ∈ t, ‖∑ j ∈ t, f j‖ ≤ ‖f i‖

Given a function f : ι → M and a nonempty finite set t ⊆ ι, we can always find i ∈ t such that ‖∑ j ∈ t, f j‖ ≤ ‖f i‖.

Defined in

Mathlib.Analysis.Normed.Group.Ultra

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupIsUltrametricDist