integrableOn_Ici_iff_integrableAtFilter_atTop

English

For a fixed a, integrability on Iic(a) is equivalent to integrability at atBot together with local integrability on Iic(a).

Русский

Для фиксированного a интегрируемость на Iic(a) эквивалентна интегрируемости на atBot вместе с локальной интегрируемостью на Iic(a).

LaTeX

$$$\operatorname{IntegrableOn}(f, \mathrm{Iic}(a), \mu) \iff (\operatorname{IntegrableAtFilter}(f, \text{atBot}, \mu) \land \operatorname{LocallyIntegrableOn}(f, \mathrm{Iic}(a), \mu))$$$

Lean4

theorem integrableOn_Ici_iff_integrableAtFilter_atTop [LinearOrder X] [CompactIccSpace X] :
    IntegrableOn f (Ici a) μ ↔ IntegrableAtFilter f atTop μ ∧ LocallyIntegrableOn f (Ici a) μ :=
  integrableOn_Iic_iff_integrableAtFilter_atBot (X := Xᵒᵈ)

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