English
The specialization relation is preserved under passing to the continuous-map level: specializes (f) (g) for f,g:C(X,Y) is equivalent to specializes of their coercions to functions X→Y.
Русский
Специализация сохраняется при переходе к отображениям в пространстве непрерывных функций: specializes f g в C(X,Y) эквивалентна specializes их отображений-коэф.
LaTeX
$$$\\bigl( f \\xrightarrow{\\text{coe}} g \\bigr)\\ \\,\\iff \\text{Specializes}(f,g)$$$
Lean4
@[norm_cast]
theorem specializes_coe {f g : C(X, Y)} : ⇑f ⤳ ⇑g ↔ f ⤳ g :=
by
refine ⟨fun h ↦ ?_, fun h ↦ h.map continuous_coeFun⟩
suffices ∀ K, IsCompact K → ∀ U, IsOpen U → MapsTo g K U → MapsTo f K U by
simpa [specializes_iff_pure, nhds_compactOpen]
exact fun K _ U hU hg x hx ↦ (h.map (continuous_apply x)).mem_open hU (hg hx)
