English
If β is a complete space, then α →ᵤ[𝔖] β is also complete, and the instance is constructed via a standard completeness argument.
Русский
Если β — полное пространство, то и α →ᵤ[𝔖] β полно; конструктор обеспечивает соответствующий экземпляр.
LaTeX
$$[CompleteSpace β] ⇒ CompleteSpace (α →ᵤ[𝔖] β).$$
Lean4
instance [CompleteSpace β] : CompleteSpace (α →ᵤ[𝔖] β) :=
by
rcases isEmpty_or_nonempty β
· infer_instance
· refine ⟨fun {F} hF ↦ ?_⟩
have := hF.1
have : ∀ x ∈ ⋃₀ 𝔖, ∃ y : β, Tendsto (toFun 𝔖 · x) F (𝓝 y) := fun x hx ↦
CompleteSpace.complete (hF.map (uniformContinuous_eval_of_mem_sUnion _ _ hx))
choose! g hg using this
use ofFun 𝔖 g
simp_rw [UniformOnFun.nhds_eq_of_basis _ _ uniformity_hasBasis_closed, le_iInf₂_iff, le_principal_iff]
intro s hs U ⟨hU, hUc⟩
rcases cauchy_iff.mp hF |>.2 _ <| UniformOnFun.gen_mem_uniformity _ _ hs hU with ⟨V, hV, hVU⟩
filter_upwards [hV] with f hf x hx
refine hUc.mem_of_tendsto ((hg x ⟨s, hs, hx⟩).prodMk_nhds tendsto_const_nhds) ?_
filter_upwards [hV] with g' hg' using hVU (mk_mem_prod hg' hf) _ hx
