card_le_multiplicity_of_δ — Mathlib

English

For any finite set s, if ∥c∥ ≤ 2 for all c ∈ s and ∥c−d∥ ≥ 1−goodδ(E) for distinct c,d, then s.card ≤ multiplicity(E).

Русский

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

LaTeX

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

Lean4

theorem card_le_multiplicity_of_δ {s : Finset E} (hs : ∀ c ∈ s, ‖c‖ ≤ 2)
    (h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - goodδ E ≤ ‖c - d‖) : s.card ≤ multiplicity E :=
  (Classical.choose_spec (exists_goodδ E)).2.2 s hs h's

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