instMetricSpace — Mathlib

English

The space of bounded continuous functions, with the uniform distance, is a pseudometric space.

Русский

Пространство ограниченно непрерывных функций с единичным расстоянием является псевдометрическим пространством.

LaTeX

$$Instance: PseudoMetricSpace (α →ᵇ β)$$

Lean4

/-- The type of bounded continuous functions, with the uniform distance, is a metric space. -/
instance instMetricSpace {β} [MetricSpace β] : MetricSpace (α →ᵇ β) where
  eq_of_dist_eq_zero
    hfg := by
    ext x
    exact eq_of_dist_eq_zero (le_antisymm (hfg ▸ dist_coe_le_dist _) dist_nonneg)

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