Theorems · Theorem · measure theory

MonotoneOn.intervalIntegrable

∀ {E : Type u_5} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ]
  [inst_2 : ConditionallyCompleteLinearOrder E] [OrderTopology E] [SecondCountableTopology E] {u : ℝ → E} {a b : ℝ},
  MonotoneOn u (Set.uIcc a b) → IntervalIntegrable u μ a b

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupMeasureTheory.IsLocallyFiniteMeasureConditionallyCompleteLinearOrderOrderTopologySecondCountableTopology