mem_support_iff — Mathlib

English

Let X be a topological space with a measure μ. Then a point x lies in the support of μ if and only if every neighborhood of x contains a subset of positive μ-measure.

Русский

Пусть X — топологическое пространство с мерой μ. Точка x принадлежит опоре μ тогда и только тогда, когда любое окрестность точки 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 any neighborhood of `x` contains a
subset with positive measure. -/
theorem mem_support_iff {x : X} : x ∈ μ.support ↔ ∃ᶠ u in (𝓝 x).smallSets, 0 < μ u :=
  Iff.rfl

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