metricSpaceNatNat — Mathlib

English

There is a canonical metric on the space ℕ→ℕ given by dist x y = (1/2)^{firstDiff x y}.

Русский

Существует каноническая метрика на пространство ℕ→ℕ, заданная dist(x,y) = (1/2)^{firstDiff(x,y)}.

LaTeX

$$$$ \operatorname{dist}(x,y)=\begin{cases}0, & x=y \\ (1/2)^{\operatorname{firstDiff}(x,y)}, & x\neq y\end{cases} $$$$

Lean4

/-- Metric space structure on `ℕ → ℕ` where the distance is given by `dist x y = (1/2)^n`,
where `n` is the smallest index where `x` and `y` differ.
Not registered as a global instance by default. -/
def metricSpaceNatNat : MetricSpace (ℕ → ℕ) :=
  PiNat.metricSpaceOfDiscreteUniformity fun _ => rfl

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