null_mono

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

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

English

If μ is absolutely continuous with respect to ν and ν(t) = 0 for a set t, then μ(t) = 0 for that t.

Русский

Если μ ≪ ν и ν(t) = 0 для множества t, то μ(t) = 0.

LaTeX

$$$\nu(t) = 0 \Rightarrow \mu(t) = 0$$$

Lean4

theorem null_mono {μ ν : Measure α} (hμν : μ ≪ ν) ⦃t : Set α⦄ (ht : ν t = 0) : μ t = 0 :=
  hμν ht

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

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

Разделы

Аффилиация

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