Documentation

Mathlib.Topology.Instances.Rat

Topology on the rational numbers #

The structure of a metric space on is introduced in this file, induced from .

theorem Rat.dist_eq (x y : ) :
dist x y = |x - y|
@[simp]
theorem Rat.dist_cast (x y : ) :
dist x y = dist x y
@[deprecated Rat.isEmbedding_coe_real (since := "2024-10-26")]

Alias of Rat.isEmbedding_coe_real.

@[simp]
theorem Nat.dist_cast_rat (x y : ) :
dist x y = dist x y
@[simp]
theorem Int.dist_cast_rat (x y : ) :
dist x y = dist x y
theorem NNRat.dist_eq (p q : ℚ≥0) :
dist p q = dist p q
theorem NNRat.nndist_eq (p q : ℚ≥0) :
nndist p q = nndist p q