notMem_support_iff — Mathlib

English

A point x lies outside the support of μ if and only if all sufficiently small neighborhoods around x have μ-measure zero (in a precise sense using small sets).

Русский

Точка x не принадлежит опоре μ тогда и только тогда, когда все достаточно маленькие окрестности x имеют меру μ равную нулю (в точности через малые множества).

LaTeX

$$x \\notin \\mathrm{supp}(\\mu) \\iff \\exists \\text{(frequently small sets) } u, \\; u \\in (\\mathcal{N}(x)).smallSets \\text{ and } \\mu(u) = 0$$

Lean4

/-- A point `x` lies outside the support of `μ` iff all of the subsets of one of its neighborhoods
have measure zero. -/
theorem notMem_support_iff {x : X} : x ∉ μ.support ↔ ∀ᶠ u in (𝓝 x).smallSets, μ u = 0 := by simp [mem_support_iff]

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