goodδ_lt_one

Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

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

English

A parameter τ > 1 is defined by τ = 1 + goodδ(E)/4, providing a small slack in Besicovitch coverings.

Русский

Параметр τ > 1 задаётся как τ = 1 + goodδ(E)/4 и задаёт малый запас в покрытии Бесиковичем.

LaTeX

$$$$goodτ(E) = 1 + \\dfrac{goodδ(E)}{4}$$$$

Lean4

theorem goodδ_lt_one : goodδ E < 1 :=
  (exists_goodδ E).choose_spec.2.1

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

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

Разделы

Аффилиация

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