measure_eq_top_iff_of_symmDiff — Mathlib

English

If μ(s ∆ t) ≠ ∞, then μ s = ∞ iff μ t = ∞.

Русский

Если μ(s Δ t) ≠ ∞, то μ(s) = ∞ тогда и только тогда, когда μ(t) = ∞.

LaTeX

$$$$ \\mu(s) = \\infty \\iff \\mu(t) = \\infty, \\quad \\text{provided } \\mu(s \\triangle t) \\neq \\infty. $$$$

Lean4

/-- If the measure of the symmetric difference of two sets is finite,
then one has infinite measure if and only if the other one does. -/
theorem measure_eq_top_iff_of_symmDiff (hμst : μ (s ∆ t) ≠ ∞) : μ s = ∞ ↔ μ t = ∞ :=
  by
  suffices h : ∀ u v, μ (u ∆ v) ≠ ∞ → μ u = ∞ → μ v = ∞ from ⟨h s t hμst, h t s (symmDiff_comm s t ▸ hμst)⟩
  intro u v hμuv hμu
  by_contra! hμv
  apply hμuv
  rw [Set.symmDiff_def, eq_top_iff]
  calc
    ∞ = μ u - μ v := by rw [ENNReal.sub_eq_top_iff.2 ⟨hμu, hμv⟩]
    _ ≤ μ (u \ v) := le_measure_diff
    _ ≤ μ (u \ v ∪ v \ u) := measure_mono subset_union_left

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