Theorems · Theorem · measure theory

Besicovitch.card_le_of_separated

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (s : Finset E),
  (∀ c ∈ s, ‖c‖ ≤ 2) → (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖) → s.card ≤ 5 ^ Module.finrank ℝ E

Any 1-separated set in the ball of radius 2 has cardinality at most 5 ^ dim. This is useful to show that the supremum in the definition of Besicovitch.multiplicity E is well behaved.

Defined in

Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensional