measure_eq_measure_smaller_of_between_null_diff

Mathlib.MeasureTheory.Measure.MeasureSpace

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

← MathLib Explorer

English

From the equality in 145072, deduce μ s1 = μ s2.

Русский

Из равенства в предыдущем выводе следует μ(s1) = μ(s2).

LaTeX

$$$$ \\mu(s_1) = \\mu(s_2). $$$$

Lean4

theorem measure_eq_measure_smaller_of_between_null_diff {s₁ s₂ s₃ : Set α} (h12 : s₁ ⊆ s₂) (h23 : s₂ ⊆ s₃)
    (h_nulldiff : μ (s₃ \ s₁) = 0) : μ s₁ = μ s₂ :=
  (measure_eq_measure_of_between_null_diff h12 h23 h_nulldiff).1

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

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

Разделы

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

Аффилиация

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