English
Under finite-dimensional E and second-countable F, the space of continuous linear maps ContinuousLinearMap (RingHom.id 𝕜) E F is second-countable.
Русский
При конечномерности E и вторичной счётности F пространство непрерывно линейных отображений E → F также имеет вторую счётность.
LaTeX
$$$[FiniteDimensional 𝕜 E] [SecondCountableTopology F] \\\\Rightarrow \\\\text{SecondCountableTopology}(ContinuousLinearMap (RingHom.id 𝕜) E F)$$$
Lean4
/-- In an infinite-dimensional space, given a finite number of points, one may find a point
with norm at most `R` which is at distance at least `1` of all these points. -/
theorem exists_norm_le_le_norm_sub_of_finset {c : 𝕜} (hc : 1 < ‖c‖) {R : ℝ} (hR : ‖c‖ < R) (h : ¬FiniteDimensional 𝕜 E)
(s : Finset E) : ∃ x : E, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖ :=
by
let F := Submodule.span 𝕜 (s : Set E)
haveI : FiniteDimensional 𝕜 F :=
Module.finite_def.2 ((Submodule.fg_top _).2 (Submodule.fg_def.2 ⟨s, Finset.finite_toSet _, rfl⟩))
have Fclosed : IsClosed (F : Set E) := Submodule.closed_of_finiteDimensional _
have : ∃ x, x ∉ F := by
contrapose! h
have : (⊤ : Submodule 𝕜 E) = F := by
ext x
simp [h]
have : FiniteDimensional 𝕜 (⊤ : Submodule 𝕜 E) := by rwa [this]
exact Module.finite_def.2 ((Submodule.fg_top _).1 (Module.finite_def.1 this))
obtain ⟨x, xR, hx⟩ : ∃ x : E, ‖x‖ ≤ R ∧ ∀ y : E, y ∈ F → 1 ≤ ‖x - y‖ := riesz_lemma_of_norm_lt hc hR Fclosed this
have hx' : ∀ y : E, y ∈ F → 1 ≤ ‖y - x‖ := by
intro y hy
rw [← norm_neg]
simpa using hx y hy
exact ⟨x, xR, fun y hy => hx' _ (Submodule.subset_span hy)⟩
