instMetricSpaceOfBoundedSpace — Mathlib

English

If β is a metric space and bounded, the space of bounded uniform functions α →ᵤ β is equipped with a natural metric, making it a metric space.

Русский

Если β — метрическое и ограниченное, пространство ограниченных UniformFun α β обладает естественной метрикой и является метрическим пространством.

LaTeX

$$$[MetricSpace\;\beta] \wedge [BoundedSpace\;\beta] \Rightarrow MetricSpace (\alpha \to^{\mathrm{u}} \beta)$$$

Lean4

noncomputable instance {β : Type*} [MetricSpace β] [BoundedSpace β] : MetricSpace (α →ᵤ β) :=
  .ofT0PseudoMetricSpace _

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