locallyFinite_volume — Mathlib

English

The Lebesgue measure on ℝ is locally finite: for every x there exists a neighborhood of x with finite volume.

Русский

Мера Лебега на ℝ является локально конечной: для каждого x существует окрестность x с конечным объемом.

LaTeX

$$$\text{IsLocallyFiniteMeasure}(\operatorname{volume})$$$

Lean4

instance locallyFinite_volume : IsLocallyFiniteMeasure (volume : Measure ℝ) :=
  ⟨fun x =>
    ⟨Ioo (x - 1) (x + 1), IsOpen.mem_nhds isOpen_Ioo ⟨sub_lt_self _ zero_lt_one, lt_add_of_pos_right _ zero_lt_one⟩, by
      simp only [Real.volume_Ioo, ENNReal.ofReal_lt_top]⟩⟩

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