card_le_multiplicity — Mathlib

English

For any finite set s in a normed space, if s is contained in the ball of radius 2 and pairwise distances are at least 1, then |s| ≤ multiplicity(E).

Русский

Для любого конечного множества s в нормированном пространстве, если ∥c∥ ≤ 2 для всех c ∈ s и расстояния между различными элементами не менее 1, то |s| ≤ multiplicity(E).

LaTeX

$$$$s.card \\le Besicovitch.multiplicity(E)$$$$

Lean4

theorem card_le_multiplicity {s : Finset E} (hs : ∀ c ∈ s, ‖c‖ ≤ 2) (h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖) :
    s.card ≤ multiplicity E := by
  apply le_csSup
  · refine ⟨5 ^ finrank ℝ E, ?_⟩
    rintro _ ⟨s, ⟨rfl, h⟩⟩
    exact Besicovitch.card_le_of_separated s h.1 h.2
  · simp only [mem_setOf_eq, Ne]
    exact ⟨s, rfl, hs, h's⟩

Похожие утверждения