integrableAtFilter_top — Mathlib

English

For suitable ε', IntegrableAtFilter f ⊤ μ ↔ Integrable f μ.

Русский

При подходящем ε' имеем IntegrableAtFilter f ⊤ μ ⇔ Integrable f μ.

LaTeX

$$$\\operatorname{IntegrableAtFilter}(f, \\top, \\mu) \\;\\Longleftrightarrow\\; \\operatorname{Integrable}(f, \\mu).$$$

Lean4

@[simp]
theorem integrableAtFilter_top [PseudoMetrizableSpace ε'] {f : α → ε'} : IntegrableAtFilter f ⊤ μ ↔ Integrable f μ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ h.integrableAtFilter ⊤⟩
  obtain ⟨s, hsf, hs⟩ := h
  exact (integrableOn_iff_integrable_of_support_subset fun _ _ ↦ hsf _).mp hs

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