ae_smul_measure_le — Mathlib

English

For any scalar c, the almost everywhere set under c • μ is contained in the almost everywhere set under μ: ae(c • μ) ≤ ae μ.

Русский

Для любого скаляра c множество ae(c•μ) содержится в ae μ: ae(c•μ) ≤ ae μ.

LaTeX

$$$\ae(c\cdot \mu) \leq \ae(\mu).$$$

Lean4

theorem ae_smul_measure_le [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (c : R) : ae (c • μ) ≤ ae μ := fun _ h ↦
  ae_smul_measure h c

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