measure_eq_measure_of_null_diff

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measure_eq_measure_of_null_diff

← MathLib Explorer

English

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

Русский

Пусть s ⊆ t и μ(t \ s) = 0, тогда μ(s) = μ(t).

LaTeX

$$$$ \\mu(s) = \\mu(t) \\quad\\text{если } \\mu(t \\setminus s) = 0. $$$$

Lean4

theorem measure_eq_measure_of_null_diff {s t : Set α} (hst : s ⊆ t) (h_nulldiff : μ (t \ s) = 0) : μ s = μ t :=
  measure_congr <| EventuallyLE.antisymm (HasSubset.Subset.eventuallyLE hst) (ae_le_set.mpr h_nulldiff)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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