English
If V and W are nontrivial and there is a separating dual, then the space of continuous linear maps V → W is nontrivial; there exists a nonzero continuous linear map from V to W.
Русский
Если V и W ненулевые и существует разделяющее двойственное, то пространство непрерывных линейных отображений V → W ненулевое; существует ненулевое отображение.
LaTeX
$$$\exists T \in \mathrm{L}(V,W) \setminus \{0\}$$$
Lean4
/-- If a space of linear maps from `E` to `F` is complete, and `E` is nontrivial, then `F` is
complete. -/
theorem completeSpace_of_completeSpace_continuousLinearMap [CompleteSpace (E →L[𝕜] F)] : CompleteSpace F :=
by
refine Metric.complete_of_cauchySeq_tendsto fun f hf => ?_
obtain ⟨v, hv⟩ : ∃ (v : E), v ≠ 0 := exists_ne 0
obtain ⟨φ, hφ⟩ : ∃ φ : StrongDual 𝕜 E, φ v = 1 := exists_eq_one hv
let g : ℕ → (E →L[𝕜] F) := fun n ↦ ContinuousLinearMap.smulRightL 𝕜 E F φ (f n)
have : CauchySeq g := (ContinuousLinearMap.smulRightL 𝕜 E F φ).lipschitz.cauchySeq_comp hf
obtain ⟨a, ha⟩ : ∃ a, Tendsto g atTop (𝓝 a) := cauchy_iff_exists_le_nhds.mp this
refine ⟨a v, ?_⟩
have : Tendsto (fun n ↦ g n v) atTop (𝓝 (a v)) :=
by
have : Continuous (fun (i : E →L[𝕜] F) ↦ i v) := by fun_prop
exact (this.tendsto _).comp ha
simpa [g, ContinuousLinearMap.smulRightL, hφ]
