of_null_right

Mathlib.MeasureTheory.Measure.AEDisjoint

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEDisjoint.of_null_right

English

If μ t = 0, then s is μ-almost everywhere disjoint from t.

Русский

Если μ(t) = 0, то s и t μ-почти что несовместны.

LaTeX

$$$\\\\mu t = 0 \\\\Rightarrow \\\\operatorname{AEDisjoint} \\\\mu \\\\; s \\\\; t$$$

Lean4

theorem of_null_right (h : μ t = 0) : AEDisjoint μ s t :=
  measure_mono_null inter_subset_right h

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

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

Разделы

Аффилиация

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