ae_smul_measure_eq

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.ae_smul_measure_eq

English

If c ≠ 0, then ae (c • μ) = ae μ; the almost-everywhere sets are identical.

Русский

Если c ≠ 0, то ae(c•μ) = ae(μ); множества ae совпадают.

LaTeX

$$$ (hc : c \neq 0) \; ⇒ \; ae(c \cdot \mu) = ae(\mu). $$$

Lean4

@[simp]
theorem ae_smul_measure_eq (hc : c ≠ 0) (μ : Measure α) : ae (c • μ) = ae μ := by ext; exact ae_smul_measure_iff hc

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru