instPseudoMetricSpace — Mathlib

English

The space of zero-at-infinity continuous maps C0(α,β), equipped with the distance induced by the inclusion to BCФ, is a pseudo-metric space.

Русский

Множество нулей на бесконечности непрерывных отображений C0(α,β), оснащённое расстоянием, индуцированным включением в BCФ, является псевдометрическим пространством.

LaTeX

$$PseudoMetricSpace(C0(α,β)) with distance 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 pseudo-metric space. -/
noncomputable instance instPseudoMetricSpace : PseudoMetricSpace C₀(α, β) :=
  fast_instance%PseudoMetricSpace.induced toBCF inferInstance

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