filter_mono — Mathlib

English

If l ≤ l' and f is IntegrableAtFilter on l', then it is IntegrableAtFilter on l.

Русский

Если l ≤ l' и f интегрируемо на l', то f интегрируемо на l.

LaTeX

$$$\\text{If } \\ell \\le \\ell' \\text{ and } \\operatorname{IntegrableAtFilter}(f, \\ell', \\mu), \\text{ then } \\operatorname{IntegrableAtFilter}(f, \\ell, \\mu).$$$

Lean4

theorem filter_mono (hl : l ≤ l') (hl' : IntegrableAtFilter f l' μ) : IntegrableAtFilter f l μ :=
  let ⟨s, hs, hsf⟩ := hl'
  ⟨s, hl hs, hsf⟩

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