Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-19 07:18 e3fac0b5

View on Github →

refactor(topology/uniform_space/separated): drop is_separated (#16458) This predicate is no longer used outside of this file. If we'll need it in the future, then we can redefine it for any topological space in terms of inseparable. Also rename topology.uniform_space.compact_separated to topology.uniform_space.compact.

Estimated changes