integrableAtFilter_atTop_iff — Mathlib

English

For any f, μ, and directed preorder with a bottom, IntegrableAtFilter f atBot μ is equivalent to existence of a real a with IntegrableOn f on Iic a.

Русский

Для всякой f, μ и направленного порядка с нижней границей, IntegrableAtFilter f atBot μ эквивалентно существованию вещественного a с IntegrableOn f (Iic a) μ.

LaTeX

$$$\\operatorname{IntegrableAtFilter}(f, \\operatorname{atBot}, \\mu) \\iff \\exists a, \\operatorname{IntegrableOn}(f, Iic(a), \\mu).$$$

Lean4

theorem integrableAtFilter_atTop_iff [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] [Nonempty α] :
    IntegrableAtFilter f atTop μ ↔ ∃ a, IntegrableOn f (Ici a) μ :=
  integrableAtFilter_atBot_iff (α := αᵒᵈ)

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