finiteAtBot — Mathlib

English

For any x in a space with a locally finite measure μ, there exists an open neighborhood of x with finite μ-measure.

Русский

Для любого x в пространстве с локально конечной мерой μ существует окрестность x, у которой мера μ конечна.

LaTeX

$$$\exists s: Set\,\alpha, x \in s \land IsOpen s \land μ s < ∞$$$

Lean4

theorem finiteAtBot {m0 : MeasurableSpace α} (μ : Measure α) : μ.FiniteAtFilter ⊥ :=
  ⟨∅, mem_bot, by simp only [measure_empty, zero_lt_top]⟩

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