measure_eq_measure_of_between_null_diff

English

If s1 ⊆ s2 ⊆ s3 and μ(s3 \\ s1) = 0, then μ s1 = μ s2 = μ s3.

Русский

Если s1 ⊆ s2 ⊆ s3 и μ(s3 \\ s1) = 0, то μ s1 = μ s2 = μ s3.

LaTeX

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

Lean4

theorem measure_eq_measure_of_between_null_diff {s₁ s₂ s₃ : Set α} (h12 : s₁ ⊆ s₂) (h23 : s₂ ⊆ s₃)
    (h_nulldiff : μ (s₃ \ s₁) = 0) : μ s₁ = μ s₂ ∧ μ s₂ = μ s₃ :=
  by
  have le12 : μ s₁ ≤ μ s₂ := measure_mono h12
  have le23 : μ s₂ ≤ μ s₃ := measure_mono h23
  have key : μ s₃ ≤ μ s₁ :=
    calc
      μ s₃ = μ (s₃ \ s₁ ∪ s₁) := by rw [diff_union_of_subset (h12.trans h23)]
      _ ≤ μ (s₃ \ s₁) + μ s₁ := (measure_union_le _ _)
      _ = μ s₁ := by simp only [h_nulldiff, zero_add]
  exact ⟨le12.antisymm (le23.trans key), le23.antisymm (key.trans le12)⟩

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