nhds_compactOpen_eq_iInf_nhds_induced

English

The neighborhood filter at f in the compact-open topology equals the infimum of the restricted neighborhood filters over all compact K: nhds f = inf_K (nhds (f|_K)).comap (restrict_K).

Русский

Сверху nhds f в компактно-открытой топологии равно наименьшее из nhds (f|_K), переходящим через ограничение restrict_K для всех компактных K.

LaTeX

$$$\mathcal{N}(f) = \bigwedge_{K\,\text{IsCompact}} \; \mathcal{N}(f\restriction K) \circ \mathrm{restrict}_K$$$

Lean4

theorem nhds_compactOpen_eq_iInf_nhds_induced (f : C(X, Y)) :
    𝓝 f = ⨅ (s) (_ : IsCompact s), (𝓝 (f.restrict s)).comap (ContinuousMap.restrict s) :=
  by
  rw [compactOpen_eq_iInf_induced]
  simp only [nhds_iInf, nhds_induced]

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