English
CompleteSpace of continuous linear maps L(E,F) is equivalent to CompleteSpace F under appropriate nontriviality hypotheses.
Русский
Полнота пространства непрерывных линейных отображений L(E,F) эквивалентна полноте F при соответствующих условиях ненулевого E.
LaTeX
$$$\text{CompleteSpace}(E \to_L[F] F) \iff \text{CompleteSpace}(F)$$$
Lean4
/-- If a space of multilinear maps from `Π i, E i` to `F` is complete, and each `E i` has a nonzero
element, then `F` is complete. -/
theorem completeSpace_of_completeSpace_continuousMultilinearMap [CompleteSpace (ContinuousMultilinearMap 𝕜 M F)]
{m : ∀ i, M i} (hm : ∀ i, m i ≠ 0) : CompleteSpace F :=
by
refine Metric.complete_of_cauchySeq_tendsto fun f hf => ?_
have : ∀ i, ∃ φ : StrongDual 𝕜 (M i), φ (m i) = 1 := fun i ↦ exists_eq_one (hm i)
choose φ hφ using this
cases nonempty_fintype ι
let g : ℕ → (ContinuousMultilinearMap 𝕜 M F) := fun n ↦
compContinuousLinearMapL φ
(ContinuousMultilinearMap.smulRightL 𝕜 _ F ((ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι 𝕜)) (f n))
have : CauchySeq g := by
refine (ContinuousLinearMap.lipschitz _).cauchySeq_comp ?_
exact (ContinuousLinearMap.lipschitz _).cauchySeq_comp hf
obtain ⟨a, ha⟩ : ∃ a, Tendsto g atTop (𝓝 a) := cauchy_iff_exists_le_nhds.mp this
refine ⟨a m, ?_⟩
have : Tendsto (fun n ↦ g n m) atTop (𝓝 (a m)) := ((continuous_eval_const _).tendsto _).comp ha
simpa [g, hφ]
