dist_cast_real — Mathlib

English

Distance between integers matches the distance between their real counterparts after casting.

Русский

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

LaTeX

$$$\\mathrm{dist}(x,y) = \\mathrm{dist}( (x: \\mathbb{R}), y)$$$

Lean4

@[norm_cast, simp]
theorem dist_cast_real (x y : ℤ) : dist (x : ℝ) y = dist x y :=
  rfl

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