mutuallySingular_iff_disjoint

Mathlib.MeasureTheory.Measure.MutuallySingular

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

English

μ ⟂ₘ ν if and only if μ and ν are disjoint in the sense of measures.

Русский

μ ⟂ₘ ν эквивалентно тому, что μ и ν взаимно диссоциированы в смысле мер.

LaTeX

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

Lean4

theorem mutuallySingular_iff_disjoint : μ ⟂ₘ ν ↔ Disjoint μ ν :=
  mutuallySingular_tfae.out 0 1

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

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

Разделы

Аффилиация

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