IsEverywherePos — Mathlib

English

A variant version of the scaling inequality, providing a bound for μ(B(x, t r)) in terms of μ(B(x,r)) with a possibly different radius scaling.

Русский

Вариант леммы масштабирования, дающий оценку μ(B(x, t r)) через μ(B(x,r)) с иным масштабированием радиуса.

LaTeX

$$$$ \\exists R>0,\\ ∀ x,t,r,\\ t∈Ioc(0,K) ∧ r≤R → μ(\\overline{B}(x,t r)) ≤ scalingConstantOf(μ,K) μ(\\overline{B}(x,r)). $$$$

Lean4

/-- A set `s` is *everywhere positive* (also called *self-supporting*) with respect to a
measure `μ` if it has positive measure around each of its points, i.e., if all neighborhoods `n`
of points of `s` satisfy `μ (s ∩ n) > 0`. -/
def IsEverywherePos (μ : Measure α) (s : Set α) : Prop :=
  ∀ x ∈ s, ∀ n ∈ 𝓝[s] x, 0 < μ n

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