Theorems · Theorem · measure theory

AntitoneOn.memLp_isCompact

∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} [BorelSpace X] [inst_4 : ConditionallyCompleteLinearOrder X]
  [inst_5 : ConditionallyCompleteLinearOrder E] [OrderTopology X] [OrderTopology E] [SecondCountableTopology E]
  {p : ENNReal} {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ],
  IsCompact s → AntitoneOn f s → MeasureTheory.MemLp f p (μ.restrict s)

Defined in

Mathlib.MeasureTheory.Function.LocallyIntegrable

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceNormedAddCommGroupBorelSpaceConditionallyCompleteLinearOrderConditionallyCompleteLinearOrderOrderTopologyOrderTopologySecondCountableTopologyMeasureTheory.IsFiniteMeasureOnCompacts