measure_mono_null_ae

Mathlib.MeasureTheory.OuterMeasure.AE

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measure_mono_null_ae

English

If s ≤ᵐ[μ] t and μ t = 0, then μ s = 0.

Русский

Если s включено в t почти по μ и μ t = 0, то μ s = 0.

LaTeX

$$$(s \leq_{\mathrm{ae}}^{\mu} t) \land (\mu t = 0) \Rightarrow \mu s = 0$$$

Lean4

theorem measure_mono_null_ae (H : s ≤ᵐ[μ] t) (ht : μ t = 0) : μ s = 0 :=
  nonpos_iff_eq_zero.1 <| ht ▸ H.measure_le

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

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

Разделы

Аффилиация

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