dist_cast_rat — Mathlib

English

For x,y \\in \\mathbb{N}, the distance in ℚ between x and y equals the distance in ℕ between x and y (viewed in ℚ).

Русский

Для x,y \\in \\mathbb{N} расстояние в ℚ между x и y равно расстоянию в ℕ между x и y (с учетом отображения в ℚ).

LaTeX

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

Lean4

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

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