instMetricSpace — Mathlib

English

If β is a metric space, then C0(α,β) becomes a metric space under the induced distance from toBCF.

Русский

Если β является метрическим пространством, то C0(α,β) оснащается метрикой, получаемой индукцией через toBCF.

LaTeX

$$MetricSpace(C0(α,β)) via d(f,g) = d(toBCF(f), toBCF(g))$$

Lean4

/-- The type of continuous functions vanishing at infinity, with the uniform distance induced by the
inclusion `ZeroAtInftyContinuousMap.toBCF`, is a metric space. -/
noncomputable instance instMetricSpace {β : Type*} [MetricSpace β] [Zero β] : MetricSpace C₀(α, β) :=
  fast_instance%MetricSpace.induced _ (toBCF_injective α β) inferInstance

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