Commit 2023-03-08 20:49 68fcf1e0

View on Github →

feat Port/Topology.UniformSpace.CompareReals (#2702) Also names instances in Topology.UniformSpace.Completion

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UniformSpace/CompareReals.lean

added def CompareReals.Bourbakiℝ

added def CompareReals.Q

added def CompareReals.bourbakiPkg

added theorem CompareReals.compare_uc

added theorem CompareReals.compare_uc_symm

added theorem Rat.uniformSpace_eq

added def rationalCauSeqPkg

Modified Mathlib/Topology/UniformSpace/Completion.lean