Mathlib Map

Theorems · Theorem · general topology

Rat.dist_cast

∀ (x y : ℚ), dist ↑x ↑y = dist x y
Defined in
Mathlib.Topology.Instances.Rat
Cited by
2 results in Mathlib
Foundations
Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Nat.dist_cast_rat · cited by 2Nat.dist_cast_ratInt.dist_cast_rat · cited by 2Int.dist_cast_ratReal · cited by 25697RealDist.dist · cited by 1539Dist.distRat.dist_castCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Realstatement · cited by 25,697
  • Dist.diststatement · cited by 1,539

Cited by2

Results whose statement or proof uses this declaration.