Theorems · Theorem · measure theory

Monotone.locallyIntegrable

∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [BorelSpace X] [inst_4 : ConditionallyCompleteLinearOrder X]
  [inst_5 : ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E]
  {f : X → E} [MeasureTheory.IsLocallyFiniteMeasure μ], Monotone f → MeasureTheory.LocallyIntegrable f μ

Defined in: Mathlib.MeasureTheory.Function.LocallyIntegrable
Cited by: 1 results in Mathlib
Foundations: Depth 217 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace TopologicalSpace NormedAddCommGroup BorelSpace ConditionallyCompleteLinearOrder ConditionallyCompleteLinearOrder OrderTopology OrderTopology SecondCountableTopology MeasureTheory.IsLocallyFiniteMeasure

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites27

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Setproof · cited by 53,352
TopologicalSpacestatement and proof · cited by 24,529
NormedAddCommGroupstatement and proof · cited by 15,752
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
Top.topproof · cited by 9,680
nhdsproof · cited by 5,554
LE.le.transproof · cited by 3,151
Set.Iccproof · cited by 1,702
BorelSpacestatement and proof · cited by 1,602
Monotonestatement and proof · cited by 1,397

Cited by1

Results whose statement or proof uses this declaration.

Antitone.locallyIntegrableproof · cited by 0