English
If ι is countable and each X(a) is a second-countable space, then the space of all functions a ↦ X(a) is second-countable.
Русский
Если индексный множественный ι счётный и каждая X(i) имеет вторую счетность, то пространство функций a ↦ X(a) по счёту второй счетности.
LaTeX
$$$\forall ι\, X: ι \to Type*,\; Countable(ι) \land \forall a, SecondCountableTopology(X(a)) \Rightarrow SecondCountableTopology(\forall a, X(a))$$$
Lean4
instance (priority := 100) [Countable α] [FirstCountableTopology α] : SecondCountableTopology α where
is_open_generated_countable := by
-- The countable union of the countable neighborhood bases at each point is a countable basis.
choose b hxb hbb using fun x : α => (nhds_basis_opens x).exists_antitone_subbasis
use range b.uncurry, countable_range b.uncurry
apply le_antisymm
· rw [le_generateFrom_iff_subset_isOpen]
rintro _ ⟨⟨x, n⟩, rfl⟩
exact (hxb x n).right
· rw [le_iff_nhds]
intro x
rw [(hbb x).ge_iff]
intro n _
refine @IsOpen.mem_nhds α (generateFrom (range b.uncurry)) x (b x n) ?_ (hxb x n).left
exact isOpen_generateFrom_of_mem ⟨⟨x, n⟩, rfl⟩
