dist — Mathlib

English

The distance on the product space is defined by dist(x,y) = 0 if x = y, and dist(x,y) = (1/2)^{firstDiff x y} otherwise.

Русский

Расстояние в произведении задаётся как dist(x,y)=0, если x=y, и dist(x,y)=(1/2)^{firstDiff(x,y)} иначе.

LaTeX

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

Lean4

/-- The distance function on a product space `Π n, E n`, given by `dist x y = (1/2)^n` where `n` is
the first index at which `x` and `y` differ. -/
protected def dist : Dist (∀ n, E n) :=
  ⟨fun x y => if x ≠ y then (1 / 2 : ℝ) ^ firstDiff x y else 0⟩

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