instHasBesicovitchCovering — Mathlib

English

There exists a canonical Besicovitch covering structure on any finite-dimensional normed space using multiplicity, goodτ, goodδ and isEmpty_satelliteConfig_multiplicity.

Русский

Существуют канонические покрытия Бесиковича на любом конечномерном нормированном пространстве, заданные через множительность, goodτ, goodδ и isEmpty_satelliteConfig_multiplicity.

LaTeX

$$IsBesicovitchCovering E$$

Lean4

instance (priority := 100) instHasBesicovitchCovering : HasBesicovitchCovering E :=
  ⟨⟨multiplicity E, goodτ E, one_lt_goodτ E, isEmpty_satelliteConfig_multiplicity E⟩⟩

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