instDist — Mathlib

English

The distance on integers is defined by the real distance between their real representatives.

Русский

Расстояние между целыми числами определено как расстояние между их образами в действительных числах.

LaTeX

$$$\\mathrm{Dist}\\,\\mathbb{Z} := \\langle \\lambda x\,y, \\; \\mathrm{dist}( (x:\\mathbb{R}), y) \\rangle$$$

Lean4

instance : Dist ℤ :=
  ⟨fun x y => dist (x : ℝ) y⟩

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