instBoundedSpace — Mathlib

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⟩

Похожие утверждения