continuous_restrict — Mathlib

English

For any subset s ⊆ X, the restriction map from C(X,Y) to C(s,Y) is continuous with respect to the compact-open topologies.

Русский

Для любой подмножества s ⊆ X отображение ограничения F ↦ F|_s непрерывно по отношению к компактно-открытым топологиям.

LaTeX

$$$\text{restrict}_s: C(X,Y) \to C(s,Y) \text{ is continuous}$$$

Lean4

/-- For any subset `s` of `X`, the restriction of continuous functions to `s` is continuous
as a function from `C(X, Y)` to `C(s, Y)` with their respective compact-open topologies. -/
theorem continuous_restrict (s : Set X) : Continuous fun F : C(X, Y) => F.restrict s :=
  continuous_precomp <| restrict s <| .id X

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