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
@[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
Equations
  • One or more equations did not get rendered due to their size.
@[deprecated continuous_mul]
theorem Rat.continuous_mul :
Continuous fun p => p.fst * p.snd