Theorems · Theorem · general topology

IsUltrametricDist.exists_norm_multiset_sum_le

∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] (s : Multiset ι) [Nonempty ι]
  {f : ι → M}, ∃ i, (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).sum‖ ≤ ‖f i‖

Given a function f : ι → M and a multiset t : Multiset ι, we can always find i : ι, belonging to t if t is nonempty, such that ‖(s.map f).sum‖ ≤ ‖f i‖.

Defined in

Mathlib.Analysis.Normed.Group.Ultra

Cited by

0 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupIsUltrametricDistNonempty