tendsto_setToL1 — Mathlib

English

If f_i → f in L1, then setToL1 hT f_i → setToL1 hT f in L1.

Русский

Если f_i сходится к f в L1, то setToL1 hT f_i сходится к setToL1 hT f в L1.

LaTeX

$$$\text{Tendsto } (i \mapsto setToL1\, h_T\, f_i)\; l\; (\mathcal{N}\; (setToL1\, h_T\, f))$$$

Lean4

/-- If `fs i → f` in `L1`, then `setToL1 hT (fs i) → setToL1 hT f`. -/
theorem tendsto_setToL1 (hT : DominatedFinMeasAdditive μ T C) (f : α →₁[μ] E) {ι} (fs : ι → α →₁[μ] E) {l : Filter ι}
    (hfs : Tendsto fs l (𝓝 f)) : Tendsto (fun i => setToL1 hT (fs i)) l (𝓝 <| setToL1 hT f) :=
  ((setToL1 hT).continuous.tendsto _).comp hfs

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