Measure_of_Interval_is_Length

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analysislebesgue-measuremeasure-theoryproofwiki

The Lebesgue measure of a closed interval [a,b] is b - a.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic

theorem Measure_of_Interval_is_Length (a b : ℝ) (hab : a ≤ b) : MeasureTheory.volume (Set.Icc a b) = ENNReal.ofReal (b - a) := by sorry

Source

https://proofwiki.org/wiki/Measure_of_Interval_is_Length

View graph