finiteAt_nhdsWithin — Mathlib

English

Let μ be a locally finite measure on a topological space. Then for every point x and every subset s, the measure of the nhdsWithin x s is finite.

Русский

Пусть μ — локально конечная мера на топологическом пространстве. Тогда для каждого элемента x и произвольного подмножества s мера множеством 𝓝_s(x) конечна.

LaTeX

$$$$\forall x, \forall s \subseteq X:\ \mu(\mathcal{N}_s(x)) < \infty,$$$$

Lean4

theorem finiteAt_nhdsWithin [TopologicalSpace α] {_m0 : MeasurableSpace α} (μ : Measure α) [IsLocallyFiniteMeasure μ]
    (x : α) (s : Set α) : μ.FiniteAtFilter (𝓝[s] x) :=
  (finiteAt_nhds μ x).inf_of_left

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