measure_union_add_inter' — Mathlib

English

If μ s ≠ ∞ and μ t = ∞, then μ(s Δ t) = ∞.

Русский

Если μ(s) не бесконечна и μ(t) бесконечно, то μ(s Δ t) бесконечно.

LaTeX

$$$$\\forall s,t:\\mathrm Set,\\; \\mu(s) \\neq \\infty \\land \\mu(t) = \\infty \\rightarrow \\mu(s\\Delta t) = \\infty.$$$$

Lean4

theorem measure_union_add_inter' (hs : MeasurableSet s) (t : Set α) : μ (s ∪ t) + μ (s ∩ t) = μ s + μ t := by
  rw [union_comm, inter_comm, measure_union_add_inter t hs, add_comm]

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