mathlib documentation

measure_theory.lebesgue_measure

Lebesgue measure on the real line

Length of an interval. This is the largest monotonic function which correctly measures all intervals.

Equations
theorem measure_theory.lebesgue_length_subadditive {a b : } {c d : } :
(set.Icc a b ⋃ (i : ), set.Ioo (c i) (d i))(ennreal.of_real (b - a) ∑' (i : ), ennreal.of_real (d i - c i))

@[instance]

Lebesgue measure on the Borel sets

The outer Lebesgue measure is the completion of this measure. (TODO: proof this)

Equations
theorem filter.eventually.volume_pos_of_nhds_real {p : → Prop} {a : } :
(∀ᶠ (x : ) in 𝓝 a, p x)0 < measure_theory.measure_space.volume {x : | p x}