English
If the base nhds at c in Y has a basis, then the nhds of the constant map Const X c in C(X,Y) has a basis described by IsCompact of the first component and the basis element of the second.
Русский
Если базис для nhds c в Y существует, тогда и у константной карты Const X c в C(X,Y) есть база, описываемая через IsCompact первого компонента и базис второго.
LaTeX
$$$ (\\nhds c).HasBasis p U \\to (\\nhds (\\text{ContinuousMap.const } X c)).HasBasis (\\lambda Ki, \\text{And (IsCompact Ki.1) (p Ki.2)}) (\\lambda Ki, {f : C(X,Y) | MapsTo (f) Ki.1 (Ki.2)}) $$$
Lean4
protected theorem mem_nhds_iff {f : C(X, Y)} {s : Set C(X, Y)} :
s ∈ 𝓝 f ↔
∃ S : Set (Set X × Set Y),
S.Finite ∧
(∀ K U, (K, U) ∈ S → IsCompact K ∧ IsOpen U ∧ MapsTo f K U) ∧
{g : C(X, Y) | ∀ K U, (K, U) ∈ S → MapsTo g K U} ⊆ s :=
by simp [f.hasBasis_nhds.mem_iff, ← setOf_forall, and_assoc]
