multiplicity_le — Mathlib

English

The Besicovitch.multiplicity is an upper bound for the maximal size of any 1-separated family in terms of finrank(E).

Русский

Besicovitch.multiplicity служит верхней границей максимального размера 1-разделённой семьи в зависимости от финразмера пространства.

LaTeX

$$$$Besicovitch.multiplicity\\;E \\ge s.card \\text{ for every suitable } s$$$$

Lean4

theorem multiplicity_le : multiplicity E ≤ 5 ^ finrank ℝ E :=
  by
  apply csSup_le
  · refine ⟨0, ⟨∅, by simp⟩⟩
  · rintro _ ⟨s, ⟨rfl, h⟩⟩
    exact Besicovitch.card_le_of_separated s h.1 h.2

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