symmDiff — Mathlib

English

The symmetric difference of two null measurable sets is null measurable.

Русский

Симметрическая разность двух нулевых измеримых множеств — нулевое измеримое множество.

LaTeX

$$$\\text{NullMeasurableSet } s μ \\land \\text{NullMeasurableSet } t μ \\Rightarrow \\text{NullMeasurableSet } (\\mathrm{symmDiff } s t) μ$$$

Lean4

@[simp]
protected theorem symmDiff {s₁ s₂ : Set α} (h₁ : NullMeasurableSet s₁ μ) (h₂ : NullMeasurableSet s₂ μ) :
    NullMeasurableSet (symmDiff s₁ s₂) μ :=
  (h₁.diff h₂).union (h₂.diff h₁)

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