case inl
X : Type u_1
Y : Type ?u.1878962
E : Type u_2
R : Type ?u.1878968
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : NormedAddCommGroup E
f : X → E
μ : MeasureTheory.Measure X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact ∅
hmono : MonotoneOn f ∅
⊢ IntegrableOn f ∅

case inr
X : Type u_1
Y : Type ?u.1878962
E : Type u_2
R : Type ?u.1878968
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : NormedAddCommGroup E
f : X → E
μ : MeasureTheory.Measure X
s : Set X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
h : Set.Nonempty s
⊢ IntegrableOn f s
X : Type u_1
Y : Type ?u.1878962
E : Type u_2
R : Type ?u.1878968
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : NormedAddCommGroup E
f : X → E
μ : MeasureTheory.Measure X
s : Set X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
⊢ IntegrableOn f s
obtain rfl | h := s.eq_empty_or_nonempty
no goals
case inl
X : Type u_1
Y : Type ?u.1878962
E : Type u_2
R : Type ?u.1878968
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : NormedAddCommGroup E
f : X → E
μ : MeasureTheory.Measure X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact ∅
hmono : MonotoneOn f ∅
⊢ IntegrableOn f ∅
exact integrableOn_empty
no goals
case inr
X : Type u_1
Y : Type ?u.1878962
E : Type u_2
R : Type ?u.1878968
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : NormedAddCommGroup E
f : X → E
μ : MeasureTheory.Measure X
s : Set X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
h : Set.Nonempty s
⊢ IntegrableOn f s
exact
  hmono.integrableOn_of_measure_ne_top (hs.isLeast_sInf h) (hs.isGreatest_sSup h)
    hs.measure_lt_top.ne hs.measurableSet