measure_inter_conull'

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measure_inter_conull'

English

If μ(s \\ t) = 0, then μ(s ∩ t) = μ s.

Русский

Если μ(s \\ t) = 0, то μ(s ∩ t) = μ(s).

LaTeX

$$$$ \\mu(s \\cap t) = \\mu(s). $$$$

Lean4

theorem measure_inter_conull' (ht : μ (s \ t) = 0) : μ (s ∩ t) = μ s := by rw [← diff_compl, measure_diff_null'];
  rwa [← diff_eq]

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

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

Разделы

Аффилиация

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