Mathlib v3 is deprecated. Go to Mathlib v4

Def rational_cau_seq_pkg

Modification history

2023-02-27 22:32
src/topology/uniform_space/compare_reals.lean
refactor(topology/*): add `uniform_space.of_fun`, use it (#18495) …
Modified rational_cau_seq_pkgView on Github →
2019-09-03 13:42
src/topology/uniform_space/compare_reals.lean
feat(topology/uniform_space): Abstract completions (#1374) …
Added rational_cau_seq_pkgView on Github →