measureReal_union_null — Mathlib

English

If μ.real s1 = 0 and μ.real s2 = 0, then μ.real (s1 ∪ s2) = 0.

Русский

Если μ.real s1 = 0 и μ.real s2 = 0, то μ.real (s1 ∪ s2) = 0.

LaTeX

$$$ \\mu.real (s_{1} \\cup s_{2}) = 0 \\;\\text{если} \\; \\mu.real s_{1} = 0 \\text{ и } \\mu.real s_{2} = 0 $$$

Lean4

theorem measureReal_union_null (h₁ : μ.real s₁ = 0) (h₂ : μ.real s₂ = 0) : μ.real (s₁ ∪ s₂) = 0 :=
  le_antisymm ((measureReal_union_le s₁ s₂).trans (by simp [h₁, h₂])) measureReal_nonneg

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