Mathlib v3 is deprecated. Go to Mathlib v4

Theorem separated_separation

Modification history

2018-10-15 13:33

analysis/topology/uniform_space.lean

feat(analysis/topology): group completion

Deleted separated_separation View on Github →

2017-08-10 16:36

topology/uniform_space.lean

construct reals as complete, linear ordered field

Added separated_separation View on Github →