dist_def — Mathlib

English

If β is a bounded metric space, then the space of uniform functions α →ᵤ β carries a natural metric, turning it into a metric space (hence T0).

Русский

Если β — ограниченное метрическое пространство, то пространство UniformFun α β имеет естественную метрику, образуя метрическое пространство (T0).

LaTeX

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

Lean4

theorem dist_def [BoundedSpace β] (f g : α →ᵤ β) : dist f g = ⨆ x, dist (toFun f x) (toFun g x) :=
  rfl

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