instMetricSpace — Mathlib

English

When α is compact and β is a metric space, the isometric equivalence is established between C(α,β) and α →ᵇ β.

Русский

При компактности α и метрическом β изометрическое соответствие между C(α,β) и α →ᵇ β осуществляется.

LaTeX

$$$C(\alpha, \beta) \cong_i (\alpha \to^b \beta)$$$

Lean4

instance instMetricSpace {β : Type*} [MetricSpace β] : MetricSpace C(α, β) :=
  (isUniformEmbedding_equivBoundedOfCompact α β).comapMetricSpace _

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