Theorems · Theorem · measure theory

AntitoneOn.intervalIntegrable

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

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupMeasureTheory.IsLocallyFiniteMeasureConditionallyCompleteLinearOrderOrderTopologySecondCountableTopology