zero_left

Mathlib.MeasureTheory.Measure.MutuallySingular

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

English

Zero measure is mutually singular with any μ.

Русский

Нулевая мера взаимно неразделима с любой мерой μ.

LaTeX

$$$0 \\perp_m \\mu$$$

Lean4

@[simp]
theorem zero_left : 0 ⟂ₘ μ :=
  zero_right.symm

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

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

Разделы

Аффилиация

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