add — Mathlib

English

Dual to bottom: IntegrableAtFilter f atTop μ iff exists a with IntegrableOn f (Ici a) μ.

Русский

Дуал к нижней границе: IntegrableAtFilter f atTop μ эквивалентно существованию a с IntegrableOn(f, Ici a) μ.

LaTeX

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

Lean4

protected theorem add [ContinuousAdd ε'] {f g : α → ε'} (hf : IntegrableAtFilter f l μ)
    (hg : IntegrableAtFilter g l μ) : IntegrableAtFilter (f + g) l μ :=
  by
  rcases hf with ⟨s, sl, hs⟩
  rcases hg with ⟨t, tl, ht⟩
  refine ⟨s ∩ t, inter_mem sl tl, ?_⟩
  exact (hs.mono_set inter_subset_left).add (ht.mono_set inter_subset_right)

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