Theorems · Theorem · measure theory

MeasureTheory.integral_Icc_eq_integral_Ico

∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x y : X} [MeasureTheory.NullSingletonClass μ],
  ∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ico x y, f t ∂μ

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Set

Cited by

1 results in Mathlib

Foundations

Depth 252 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpacePartialOrderMeasureTheory.NullSingletonClass