English
If β is a bounded space, then UniformOnFun α 𝔖 β is a bounded space as well.
Русский
Если β ограничено, то и UniformOnFun α 𝔖 β также ограничено.
LaTeX
$$$[\text{BoundedSpace }\beta] \Rightarrow [\text{BoundedSpace } (\alpha \to_{\mathfrak{S}} \beta)].$$$
Lean4
noncomputable instance [BoundedSpace β] : BoundedSpace (α →ᵤ[𝔖] β) where
bounded_univ :=
by
convert lipschitzWith_one_ofFun_toFun (𝔖 := 𝔖) (β := β) |>.isBounded_image (.all Set.univ)
ext f
simp only [Set.mem_univ, Function.comp_apply, Set.image_univ, Set.mem_range, true_iff]
exact ⟨UniformFun.ofFun (toFun 𝔖 f), by simp⟩