continuousLinearMapOfTendsto — Mathlib

English

The image of the range under a map g equals the range of the composition g ∘ f.

Русский

Образ подмножества набора по g равен образу композиции g ∘ f.

LaTeX

$$$\operatorname{image} g (\operatorname{range} f) = \operatorname{range} (\mathrm{Function}.comp g f)$$$

Lean4

/-- Given a *sequence* of continuous linear maps which converges pointwise and for which the
domain is complete, the Banach-Steinhaus theorem is used to guarantee that the limit map
is a *continuous* linear map as well. -/
abbrev continuousLinearMapOfTendsto {α : Type*} [CompleteSpace E] [T2Space F] {l : Filter α} [l.IsCountablyGenerated]
    [l.NeBot] (g : α → E →SL[σ₁₂] F) {f : E → F} (h : Tendsto (fun n x ↦ g n x) l (𝓝 f)) : E →SL[σ₁₂] F :=
  (norm_withSeminorms 𝕜₂ F).continuousLinearMapOfTendsto g h

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