exists_measure_closedBall_le_mul — Mathlib

English

For a locally doubling measure μ on a pseudo-metric space α, there exists a constant C such that for sufficiently small ε and all x, μ(B(x,2ε)) ≤ C μ(B(x,ε)).

Русский

Для локально удваивающейся меры μ на псевдометриальном пространстве α существует константа C, такая что для достаточно малых ε и для всех x выполняется μ( B(x,2ε) ) ≤ C μ( B(x,ε) ).

LaTeX

$$$$ \\exists C\\in \\mathbb{R}_{\\ge 0},\\ \\forall^*\\,\\varepsilon>0,\\ \\forall x,\\ \\mu(\\overline{B}(x,2\\varepsilon)) \\le C\\,\\mu(\\overline{B}(x,\\varepsilon)). $$$$

Lean4

theorem exists_measure_closedBall_le_mul :
    ∃ C : ℝ≥0, ∀ᶠ ε in 𝓝[>] 0, ∀ x, μ (closedBall x (2 * ε)) ≤ C * μ (closedBall x ε) :=
  exists_measure_closedBall_le_mul''

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