Theorems · Theorem · general topology

IsUltrametricDist.exists_norm_finsetProd_le

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

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

Defined in

Mathlib.Analysis.Normed.Group.Ultra

Cited by

1 results in Mathlib

Foundations

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

Assumes

SeminormedCommGroupIsUltrametricDistNonempty