English
Under mild hypotheses, the space of continuous maps C(X,Y) inherits a second-countable topology from X and Y: the instance provides SecondCountableTopology C(X,Y).
Русский
При умеренных гипотезах пространство непрерывных отображений C(X,Y) наследует вторую счетность топологии от X и Y; данный инстанс обеспечивает SecondCountableTopology C(X,Y).
LaTeX
$$$[SecondCountableTopology\\;X]\\,[LocallyCompactSpace\\;X]\\,[SecondCountableTopology\\;Y]\\Rightarrow SecondCountableTopology\\;C(X,Y)$$$
Lean4
/-- A version of `instSecondCountableTopology` with a technical assumption
instead of `[SecondCountableTopology X] [LocallyCompactSpace X]`.
It is here as a reminder of what could be an intermediate goal,
if someone tries to weaken the assumptions in the instance
(e.g., from `[LocallyCompactSpace X]` to `[LocallyCompactPair X Y]` - not sure if it's true). -/
theorem secondCountableTopology [SecondCountableTopology Y]
(hX :
∃ S : Set (Set X),
S.Countable ∧
(∀ K ∈ S, IsCompact K) ∧ ∀ f : C(X, Y), ∀ V, IsOpen V → ∀ x ∈ f ⁻¹' V, ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo f K V) :
SecondCountableTopology C(X, Y) where
is_open_generated_countable := by
rcases hX with ⟨S, hScount, hScomp, hS⟩
refine ⟨_, ?_, compactOpen_eq_generateFrom (S := S) hScomp (isBasis_countableBasis _) ?_⟩
· exact .image2 hScount (countable_setOf_finite_subset (countable_countableBasis Y)) _
· intro f x V hV hx
apply hS
exacts [isOpen_of_mem_countableBasis hV, hx]
