dist_cast_real — Mathlib

English

For x,y ∈ ℕ, the real distance between their real embeddings equals the nat 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_real (x y : ℕ) : dist (x : ℝ) y = dist x y :=
  rfl

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