measure_ne_top_iff_of_symmDiff — Mathlib

English

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

Русский

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

LaTeX

$$$$ \\mu(s) \\neq \\infty \\iff \\mu(t) \\neq \\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 finite measure if and only if the other one does. -/
theorem measure_ne_top_iff_of_symmDiff (hμst : μ (s ∆ t) ≠ ∞) : μ s ≠ ∞ ↔ μ t ≠ ∞ :=
  (measure_eq_top_iff_of_symmDiff hμst).ne

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