tendsto_compactOpen_restrict — Mathlib

English

If a family F_i tends to f in the compact-open topology, then for any subset s, the restricted family F_i|_s tends to f|_s in the compact-open topology of C(s,Y).

Русский

Если семейство F_i стремится к f в компактно-открытой топологии, то для любого подмножества s семейство F_i|_s стремится к f|_s в соответствующей топологии.

LaTeX

$$$\text{Tendsto}(i \mapsto F(i)\restriction s)\, l\, (\mathcal{N}(f\restriction s))$$$

Lean4

theorem tendsto_compactOpen_restrict {ι : Type*} {l : Filter ι} {F : ι → C(X, Y)} {f : C(X, Y)}
    (hFf : Filter.Tendsto F l (𝓝 f)) (s : Set X) : Tendsto (fun i => (F i).restrict s) l (𝓝 (f.restrict s)) :=
  (continuous_restrict s).continuousAt.tendsto.comp hFf

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