Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-05 02:16 916b5d3a

View on Github →

feat(topology): completion of separable space is separable (#4399) API change:

  • dense renamed to exists_between;
  • new dense (s : set α) means ∀ x, x ∈ closure s.

Estimated changes

deleted theorem dense
added theorem exists_between
added theorem dense.closure_eq
added def dense
added theorem dense_iff_closure_eq
modified theorem dense_of_subset_dense
added theorem dense_range.comp
added theorem dense_range.nonempty
added def dense_range
added theorem dense_range.prod
deleted theorem dense_range.closure_range
deleted theorem dense_range.comp
deleted theorem dense_range.nonempty
deleted theorem dense_range.prod
deleted def dense_range