Theorems · Theorem · general topology
IsUltrametricDist.exists_norm_multiset_prod_le
∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] (s : Multiset ι) [Nonempty ι]
{f : ι → M}, ∃ i, (s ≠ 0 → i ∈ s) ∧ ‖(Multiset.map f s).prod‖ ≤ ‖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).prod‖ ≤ ‖f i‖.
- Defined in
- Mathlib.Analysis.Normed.Group.Ultra
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Norm.normstatement and proof · cited by 5,413
- Multisetstatement and proof · cited by 2,627
- LT.lt.leproof · cited by 2,189
- le_reflproof · cited by 2,061
- eq_or_neproof · cited by 1,117
- le_transproof · cited by 985
- Multiset.mapstatement and proof · cited by 876
- Multiset.prodstatement and proof · cited by 528
- SeminormedCommGroupstatement and proof · cited by 191
- IsUltrametricDiststatement and proof · cited by 177
- Multiset.induction_onproof · cited by 109
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.