integrable_iff_integrableAtFilter_atBot

English

If f is integrable, then it is integrable at both atBot and atTop filters, and locally integrable.

Русский

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

LaTeX

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

Lean4

theorem integrable_iff_integrableAtFilter_atBot [LinearOrder X] [OrderTop X] [CompactIccSpace X] :
    Integrable f μ ↔ IntegrableAtFilter f atBot μ ∧ LocallyIntegrable f μ :=
  by
  constructor
  · exact fun hf ↦ ⟨hf.integrableAtFilter _, hf.locallyIntegrable⟩
  · refine fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩
    exact h.1.filter_mono cocompact_le_atBot

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