exists_isOpen_measure_lt_top — Mathlib

English

There exists an open neighborhood around every point that has finite μ-measure.

Русский

Для каждой точки существует открытая окрестность с конечной мерой μ.

LaTeX

$$$\exists O \text{ open}, x ∈ O, μ(O) < ∞$$$

Lean4

theorem exists_isOpen_measure_lt_top [TopologicalSpace α] (μ : Measure α) [IsLocallyFiniteMeasure μ] (x : α) :
    ∃ s : Set α, x ∈ s ∧ IsOpen s ∧ μ s < ∞ := by
  simpa only [and_assoc] using (μ.finiteAt_nhds x).exists_mem_basis (nhds_basis_opens x)

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