mem_support_iff_forall — Mathlib

English

Let X be a topological space with a measure μ. A point x belongs to the support of μ if and only if every neighborhood U of x has positive measure, i.e., μ(U) > 0 for all U in 𝒩(x).

Русский

Пусть X — топологическое пространство с мерой μ. Точка x принадлежит опоре μ тогда и только тогда, когда любая окрестность U точки x имеет положительную меру, т.е. μ(U) > 0 для всех U в 𝒩(x).

LaTeX

$$$x \\in \\mathrm{supp}(\\mu) \\iff \\forall U \\in \\mathcal{N}(x), \\mu(U) > 0$$$

Lean4

/-- A point `x` is in the support of measure `μ` iff every neighborhood of `x` has positive
measure. -/
theorem mem_support_iff_forall (x : X) : x ∈ μ.support ↔ ∀ U ∈ 𝓝 x, 0 < μ U :=
  (𝓝 x).basis_sets.mem_measureSupport

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