tendsto_compactOpen_iff_forall — Mathlib

English

Tendsto in the compact-open topology is equivalent to Tendsto after restriction to every compact subset K.

Русский

Сходность в компактно-открытой топологии эквивалентна сходности после ограничения к каждому компактному множества K.

LaTeX

$$$\text{Tendsto } F l (\mathcal{N} f) \iff \forall K,\ IsCompact(K) \to \text{Tendsto}(i \mapsto (F i)\restriction K) l (\mathcal{N}(f\restriction K))$$$

Lean4

theorem tendsto_compactOpen_iff_forall {ι : Type*} {l : Filter ι} (F : ι → C(X, Y)) (f : C(X, Y)) :
    Tendsto F l (𝓝 f) ↔ ∀ K, IsCompact K → Tendsto (fun i => (F i).restrict K) l (𝓝 (f.restrict K)) :=
  by
  rw [compactOpen_eq_iInf_induced]
  simp [nhds_iInf, nhds_induced, Filter.tendsto_comap_iff, Function.comp_def]

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