integrableOn_Ioi_iff_integrableAtFilter_atTop_nhdsWithin

English

Integrability on Ioi(a) is equivalent to integrability at atTop, integrability at nhdsWithin(a, Ioi(a)), and local integrability on Ioi(a).

Русский

Интегрируемость на Ioi(a) эквивалентна интегрируемости на atTop, интегрируемости на nhdsWithin(a, Ioi(a)) и локальной интегрируемости на Ioi(a).

LaTeX

$$$\operatorname{IntegrableOn}(f, \mathrm{Ioi}(a), \mu) \iff (\operatorname{IntegrableAtFilter}(f, \text{atTop}, \mu) \land \operatorname{IntegrableAtFilter}(f, \mathcal{nhdsWithin}(a, \mathrm{Ioi}(a)), \mu) \land \operatorname{LocallyIntegrableOn}(f, \mathrm{Ioi}(a), \mu))$$$

Lean4

theorem integrableOn_Ioi_iff_integrableAtFilter_atTop_nhdsWithin [LinearOrder X] [CompactIccSpace X] [NoMaxOrder X]
    [OrderTopology X] :
    IntegrableOn f (Ioi a) μ ↔
      IntegrableAtFilter f atTop μ ∧ IntegrableAtFilter f (𝓝[>] a) μ ∧ LocallyIntegrableOn f (Ioi a) μ :=
  integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithin (X := Xᵒᵈ)

Похожие утверждения