volume_Ioi — Mathlib

English

For any a ∈ ℝ, the volume of the closed ray [a, ∞) is infinite.

Русский

Для любого a ∈ ℝ, объем луча [a, ∞) бесконечен.

LaTeX

$$$\operatorname{volume}(\mathrm{Ici}(a)) = \infty$$$

Lean4

@[simp]
theorem volume_Ioi {a : ℝ} : volume (Ioi a) = ∞ :=
  top_unique <|
    le_of_tendsto' ENNReal.tendsto_nat_nhds_top fun n =>
      calc
        (n : ℝ≥0∞) = volume (Ioo a (a + n)) := by simp
        _ ≤ volume (Ioi a) := measure_mono Ioo_subset_Ioi_self

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