integrable_iff_integrableAtFilter_atTop

English

If f is integrable, then it is integrable at the top filter together with local integrability.

Русский

Если f интегрируема, то она интегрируема на фильтре atTop вместе с локальной интегрируемостью.

LaTeX

$$$\operatorname{Integrable}(f, \mu) \Rightarrow (\operatorname{IntegrableAtFilter}(f, \text{atTop}, \mu) \land \operatorname{LocallyIntegrable}(f, \mu))$$$

Lean4

theorem integrable_iff_integrableAtFilter_atTop [LinearOrder X] [OrderBot X] [CompactIccSpace X] :
    Integrable f μ ↔ IntegrableAtFilter f atTop μ ∧ LocallyIntegrable f μ :=
  integrable_iff_integrableAtFilter_atBot (X := Xᵒᵈ)

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