isometry_ofFun_boundedContinuousFunction

English

There is an isometry from the space of continuous maps C(α, β) into the space of uniform functions α →ᵤ β given by composing with the functor that sends a map to its UniformFun representation.

Русский

Существует изометрия между пространством непрерывных отображений C(α,β) и пространством UniformFun α β, задаваемая отображением в UniformFun-представление функции.

LaTeX

$$Isometry (\mathrm{ofFun} \circ \mathrm{DFunLike.coe} : C(\alpha,\beta) → α →^{\mathrm{u}} β)$$

Lean4

theorem isometry_ofFun_boundedContinuousFunction [TopologicalSpace α] :
    Isometry (ofFun ∘ DFunLike.coe : (α →ᵇ β) → α →ᵤ β) := by simp [Isometry, edist_def, edist_eq_iSup]

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