exact h.1.filter_mono cocompact_le_atBot
case mpr
X : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderTop X
inst✝ : CompactIccSpace X
h : IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ
no goals