ae_smul_measure — Mathlib

English

If c ≠ 0, then the equality of ae statements for c • μ and μ holds; precise equivalence under nonzero scaling.

Русский

Если c ≠ 0, то эквивалентность ae для c•μ и μ сохраняется; точная эквивалентность при ненулевом масштабе.

LaTeX

$$$\forall c:\, R\; (c \neq 0) \Rightarrow (\ae_{c\cdot\mu} (p) \Leftrightarrow \ae_{\mu}(p)).$$$

Lean4

theorem ae_smul_measure {p : α → Prop} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (h : ∀ᵐ x ∂μ, p x) (c : R) :
    ∀ᵐ x ∂c • μ, p x :=
  ae_iff.2 <| by rw [smul_apply, ae_iff.1 h, ← smul_one_smul ℝ≥0∞, smul_zero]

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