volume_univ — Mathlib

English

Let a ∈ ℝ. The Lebesgue volume of the whole real line is infinite.

Русский

Пусть a ∈ ℝ. Объем всей прямой ℝ равен бесконечности.

LaTeX

$$$\operatorname{volume}(\mathbb{R}) = \infty$$$

Lean4

theorem volume_univ : volume (univ : Set ℝ) = ∞ :=
  ENNReal.eq_top_of_forall_nnreal_le fun r =>
    calc
      (r : ℝ≥0∞) = volume (Icc (0 : ℝ) r) := by simp
      _ ≤ volume univ := measure_mono (subset_univ _)

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