isometry_ofFun_continuousMap — Mathlib

English

For [TopologicalSpace α] [CompactSpace α], the same isometry holds when starting from ContinuousMap α → β into UniformFun α β.

Русский

При [TopologicalSpace α] [CompactSpace α] та же изометрия сохраняется, если начинать с ContinuousMap α → β.

LaTeX

$$Isometry (Function.comp (UniformFun.ofFun) ContinuousMap.instFunLike.coe)$$

Lean4

theorem isometry_ofFun_continuousMap [TopologicalSpace α] [CompactSpace α] :
    Isometry (ofFun ∘ DFunLike.coe : C(α, β) → α →ᵤ β) :=
  isometry_ofFun_boundedContinuousFunction.comp <| ContinuousMap.isometryEquivBoundedOfCompact α β |>.isometry

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