dist_cast — Mathlib

English

For x,y ∈ ℚ, the real distance between their real embeddings equals the rational distance: dist((x:ℝ) , y) = dist(x,y).

Русский

Для x,y ∈ ℚ расстояние между вещественными образами равно расстоянию в ℚ: dist((x:ℝ), y) = dist(x,y).

LaTeX

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

Lean4

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

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