theorem integrable_iff_integrableAtFilter_atBot_atTop {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} [LinearOrder X] [CompactIccSpace X] : MeasureTheory.Integrable f μ ↔ (MeasureTheory.IntegrableAtFilter f Filter.atBot μ ∧ MeasureTheory.IntegrableAtFilter f Filter.atTop μ) ∧ MeasureTheory.LocallyIntegrable f μ

theorem integrable_iff_integrableAtFilter_atBot {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} [LinearOrder X] [OrderTop X] [CompactIccSpace X] : MeasureTheory.Integrable f μ ↔ MeasureTheory.IntegrableAtFilter f Filter.atBot μ ∧ MeasureTheory.LocallyIntegrable f μ

theorem integrable_iff_integrableAtFilter_atTop {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} [LinearOrder X] [OrderBot X] [CompactIccSpace X] : MeasureTheory.Integrable f μ ↔ MeasureTheory.IntegrableAtFilter f Filter.atTop μ ∧ MeasureTheory.LocallyIntegrable f μ

theorem integrableOn_Iic_iff_integrableAtFilter_atBot {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} {a : X} [LinearOrder X] [CompactIccSpace X] : MeasureTheory.IntegrableOn f (Set.Iic a) μ ↔ MeasureTheory.IntegrableAtFilter f Filter.atBot μ ∧ MeasureTheory.LocallyIntegrableOn f (Set.Iic a) μ

theorem integrableOn_Ici_iff_integrableAtFilter_atTop {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} {a : X} [LinearOrder X] [CompactIccSpace X] : MeasureTheory.IntegrableOn f (Set.Ici a) μ ↔ MeasureTheory.IntegrableAtFilter f Filter.atTop μ ∧ MeasureTheory.LocallyIntegrableOn f (Set.Ici a) μ