compl_support_eq_sUnion — Mathlib

English

The complement of the support equals the sUnion of open sets with zero measure.

Русский

Дополнение опоры есть объединение по открытым множествам с нулевой мерой.

LaTeX

$$\\mathrm{supp}(\\mu)^{c} = \\bigcup_{t:\\, \\text{Set},\\, \\text{IsOpen}(t) \\wedge \\mu(t)=0} t$$

Lean4

theorem compl_support_eq_sUnion : μ.supportᶜ = ⋃₀ {t : Set X | IsOpen t ∧ μ t = 0} :=
  by
  ext x
  simp only [Set.mem_compl_iff, Set.mem_sUnion, Set.mem_setOf_eq, and_right_comm,
    nhds_basis_opens x |>.notMem_measureSupport, fun t ↦ and_comm (b := x ∈ t)]

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