measure_mul_le_scalingConstantOf_mul

English

For given K, x, t, r with t∈Ioc(0,K) and r ≤ scalingScaleOf μ K, μ(closedBall(x,t r)) ≤ scalingConstantOf μ K μ(closedBall(x,r)).

Русский

Для заданного K, x, t и r с t∈Ioc(0,K) и r ≤ scalingScaleOf μ K выполняется μ( B(x,t r) ) ≤ scalingConstantOf μ K μ( B(x,r) ).

LaTeX

$$$$ \\forall K, \\forall x, \\forall t, r,\\ t\\in Ioc(0,K) \\Rightarrow r \\le scalingScaleOf(\\mu,K) \\,\\Rightarrow \\, μ(\\overline{B}(x,t r)) \\le scalingConstantOf(\\mu,K) \\cdot μ(\\overline{B}(x,r)). $$$$

Lean4

theorem measure_mul_le_scalingConstantOf_mul {K : ℝ} {x : α} {t r : ℝ} (ht : t ∈ Ioc 0 K)
    (hr : r ≤ scalingScaleOf μ K) : μ (closedBall x (t * r)) ≤ scalingConstantOf μ K * μ (closedBall x r) :=
  (eventually_measure_mul_le_scalingConstantOf_mul μ K).choose_spec.2 x t r ht hr

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