English
If E is finite-dimensional and F is second-countable, then the space of continuous linear maps E → F is second-countable.
Русский
Пусть E конечномерное, а F — пространства с второй счётностью; множество непрерывных линейных отображений E → F также имеет вторую счётность.
LaTeX
$$$[\\\\text{FiniteDimensional } 𝕜 E] \\\\Rightarrow [\\\\text{SecondCountableTopology } F] \\\\Rightarrow \\\\text{SecondCountableTopology}(E \\\\to_L[𝕜] F)$$$
Lean4
instance [FiniteDimensional 𝕜 E] [SecondCountableTopology F] : SecondCountableTopology (E →L[𝕜] F) :=
by
set d := Module.finrank 𝕜 E
suffices ∀ ε > (0 : ℝ), ∃ n : (E →L[𝕜] F) → Fin d → ℕ, ∀ f g : E →L[𝕜] F, n f = n g → dist f g ≤ ε from
Metric.secondCountable_of_countable_discretization fun ε ε_pos => ⟨Fin d → ℕ, by infer_instance, this ε ε_pos⟩
intro ε ε_pos
obtain ⟨u : ℕ → F, hu : DenseRange u⟩ := exists_dense_seq F
let v := Module.finBasis 𝕜 E
obtain ⟨C : ℝ, C_pos : 0 < C, hC : ∀ {φ : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ‖φ (v i)‖ ≤ M) → ‖φ‖ ≤ C * M⟩ :=
v.exists_opNorm_le (E := E) (F := F)
have h_2C : 0 < 2 * C := mul_pos zero_lt_two C_pos
have hε2C : 0 < ε / (2 * C) := div_pos ε_pos h_2C
have : ∀ φ : E →L[𝕜] F, ∃ n : Fin d → ℕ, ‖φ - (v.constrL <| u ∘ n)‖ ≤ ε / 2 :=
by
intro φ
have : ∀ i, ∃ n, ‖φ (v i) - u n‖ ≤ ε / (2 * C) :=
by
simp only [norm_sub_rev]
intro i
have : φ (v i) ∈ closure (range u) := hu _
obtain ⟨n, hn⟩ : ∃ n, ‖u n - φ (v i)‖ < ε / (2 * C) :=
by
rw [mem_closure_iff_nhds_basis Metric.nhds_basis_ball] at this
specialize this (ε / (2 * C)) hε2C
simpa [dist_eq_norm]
exact ⟨n, le_of_lt hn⟩
choose n hn using this
use n
replace hn : ∀ i : Fin d, ‖(φ - (v.constrL <| u ∘ n)) (v i)‖ ≤ ε / (2 * C) := by simp [hn]
have : C * (ε / (2 * C)) = ε / 2 := by
rw [eq_div_iff (two_ne_zero : (2 : ℝ) ≠ 0), mul_comm, ← mul_assoc, mul_div_cancel₀ _ (ne_of_gt h_2C)]
specialize hC (le_of_lt hε2C) hn
rwa [this] at hC
choose n hn using this
set Φ := fun φ : E →L[𝕜] F => v.constrL <| u ∘ n φ
change ∀ z, dist z (Φ z) ≤ ε / 2 at hn
use n
intro x y hxy
calc
dist x y ≤ dist x (Φ x) + dist (Φ x) y := dist_triangle _ _ _
_ = dist x (Φ x) + dist y (Φ y) := by simp [Φ, hxy, dist_comm]
_ ≤ ε := by linarith [hn x, hn y]
