goodδ

Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

URI: https://scilib.ai/kg/mathlib#Besicovitch.goodδ

← MathLib Explorer

English

The chosen δ from exists_goodδ satisfies goodδ < 1.

Русский

Выбранное δ из exists_goodδ меньше единицы.

LaTeX

$$$$goodδ(E) < 1$$$$

Lean4

/-- A small positive number such that any `1 - δ`-separated set in the ball of radius `2` has
cardinality at most `Besicovitch.multiplicity E`. -/
def goodδ : ℝ :=
  (exists_goodδ E).choose

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru