measure_symmDiff_eq_top — Mathlib

English

Symmetric difference measure top lemma: μ(s Δ t) = μ(s) + μ(t) - 2 μ(s ∩ t) in appropriate cases.

Русский

Лемма о мере симметрической разности: в подходящем случае μ(s Δ t) = μ(s) + μ(t) - 2 μ(s ∩ t).

LaTeX

$$$$\\forall s,t:\\mathrm Set,\\; \\mu(s\\Delta t) = \\mu(s) + \\mu(t) - 2\\mu(s\\cap t)$$ (при надлежащих условиях).$$

Lean4

theorem measure_symmDiff_eq_top (hs : μ s ≠ ∞) (ht : μ t = ∞) : μ (s ∆ t) = ∞ :=
  measure_mono_top subset_union_right (measure_diff_eq_top ht hs)

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