notMem_support_iff_exists — Mathlib

English

A point x lies outside the support iff there exists a neighborhood U of x with μ(U) = 0.

Русский

Точка x не принадлежит опоре тогда, когда существует окрестность U(x) с μ(U) = 0.

LaTeX

$$x \\notin \\mathrm{supp}(\\mu) \\iff \\exists U \\in \\mathcal{N}(x), \\mu(U) = 0$$

Lean4

/-- A point `x` lies outside the support of `μ` iff some neighborhood of `x` has measure zero. -/
theorem notMem_support_iff_exists {x : X} : x ∉ μ.support ↔ ∃ U ∈ 𝓝 x, μ U = 0 := by simp [mem_support_iff_forall]

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