notMem_measureSupport — Mathlib

English

If the neighborhood basis around x has a basis {s_i} with μ(s_i)=0, then x is not in the support.

Русский

Если вокруг x есть базис окрестностей {s_i} с μ(s_i)=0, то x не принадлежит опоре.

LaTeX

$$x \\notin \\mathrm{supp}(\\mu) \\iff \\exists i, p(i) \\wedge \\mu(s(i)) = 0$$

Lean4

theorem _root_.Filter.HasBasis.notMem_measureSupport {ι : Sort*} {p : ι → Prop} {s : ι → Set X} {x : X}
    (hl : (𝓝 x).HasBasis p s) : x ∉ μ.support ↔ ∃ i, p i ∧ μ (s i) = 0 := by simp [hl.mem_measureSupport]

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