mutuallySingular_iff_disjoint_ae

Mathlib.MeasureTheory.Measure.MutuallySingular

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

English

μ ⟂ₘ ν iff Disjoint (ae μ) (ae ν).

Русский

μ ⟂ₘ ν эквивалентно несовместности ae μ и ae ν.

LaTeX

$$$$ μ ⟂_{m} ν \\iff Disjoint(ae \\, μ, ae \\, ν). $$$$

Lean4

theorem mutuallySingular_iff_disjoint_ae : μ ⟂ₘ ν ↔ Disjoint (ae μ) (ae ν) :=
  mutuallySingular_tfae.out 0 2

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

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

Разделы

Аффилиация

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