dist_cast_rat — Mathlib

English

The distance in ℚ between integers x,y equals the distance in ℤ between x,y (via embedding).

Русский

Расстояние в ℚ между целыми x,y равно расстоянию в ℤ между x,y (через вложение).

LaTeX

$$$\\operatorname{dist}_{\\mathbb{Q}}(x, y) = \\operatorname{dist}_{\\mathbb{Z}}(x, y)$$$

Lean4

@[norm_cast, simp]
theorem dist_cast_rat (x y : ℤ) : dist (x : ℚ) y = dist x y := by rw [← Int.dist_cast_real, ← Rat.dist_cast]; congr

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