support_eq_forall_isOpen — Mathlib

English

The support consists of exactly those points x for which every open neighborhood of x has positive μ-measure.

Русский

Опора состоит из тех точек x, для которых каждая открытая окрестность x имеет положительную меру μ.

LaTeX

$$\\mathrm{supp}(\\mu) = \\{ x \\in X \\mid \\forall \\; U \\text{ open}, x \\in U \\Rightarrow \\mu(U) > 0 \\}$$

Lean4

/-- The support of a measure equals the set of points whose open neighborhoods
all have positive measure. -/
theorem support_eq_forall_isOpen : μ.support = {x : X | ∀ u : Set X, x ∈ u → IsOpen u → 0 < μ u} := by
  simp [Set.ext_iff, nhds_basis_opens _ |>.mem_measureSupport]

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