refactor(*): migrate to `dense` API (#4447)
@PatrickMassot introduced `dense` in #4399. In this PR I review the API and migrate many definitions and lemmas
to use `dense s` instead of `closure s = univ`. I also generalize `second_countable_of_separable` to a `uniform_space`
with a countably generated uniformity filter.
## API changes
### Use `dense` or `dense_range` instead of `closure _ = univ`
#### Lemmas
- `has_fderiv_within_at.unique_diff_within_at`;
- `exists_dense_seq`;
- `dense_Inter_of_open_nat`;
- `dense_sInter_of_open`;
- `dense_bInter_of_open`;
- `dense_Inter_of_open`;
- `dense_sInter_of_Gδ`;
- `dense_bInter_of_Gδ`;
- `eventually_residual`;
- `mem_residual`;
- `dense_bUnion_interior_of_closed`;
- `dense_sUnion_interior_of_closed`;
- `dense_Union_interior_of_closed`;
- `Kuratowski_embeddinng.embedding_of_subset_isometry`;
- `continuous_extend_from`;
#### Definitions
- `unique_diff_within_at`;
- `residual`;
### Rename
- `submodule.linear_eq_on` → `linear_map.eq_on_span`, `linear_map.eq_on_span'`;
- `submodule.linear_map.ext_on` → `linear_map.ext_on_range`;
- `filter.is_countably_generated.has_antimono_basis` →
`filter.is_countably_generated.exists_antimono_basis`;
- `exists_countable_closure_eq_univ` → `exists_countable_dense`, use `dense`;
- `dense_seq_dense` → `dense_range_dense_seq`, use `dense`;
- `dense_range.separable_space` is now `protected`;
- `dense_of_subset_dense` → `dense.mono`;
- `dense_inter_of_open_left` → `dense.inter_of_open_left`;
- `dense_inter_of_open_right` → `dense.inter_of_open_right`;
- `continuous.dense_image_of_dense_range` → `dense_range.dense_image`;
- `dense_range.inhabited`, `dense_range.nonempty`: changed API, TODO;
- `quotient_dense_of_dense` → `dense.quotient`, use `dense`;
- `dense_inducing.separable` → `dense_inducing.separable_space`, add `protected`;
- `dense_embedding.separable` → `dense_embedding.separable_space`, add `protected`;
- `dense_inter_of_Gδ` → `dense.inter_of_Gδ`;
- `stone_cech_unit_dense` → `dense_range_stone_cech_unit`;
- `abstract_completion.dense'` → `abstract_completion.closure_range`;
- `Cauchy.pure_cauchy_dense` → `Cauchy.dense_range_pure_cauchy`;
- `completion.dense` → `completion.dense_range_coe`;
- `completion.dense₂` → `completion.dense_range_coe₂`;
- `completion.dense₃` → `completion.dense_range_coe₃`;
### New
- `has_fderiv_within_at.unique_on` : if `f'` and `f₁'` are two derivatives of `f`
within `s` at `x`, then they are equal on the tangent cone to `s` at `x`;
- `local_homeomorph.mdifferentiable.mfderiv_bijective`,
`local_homeomorph.mdifferentiable.mfderiv_surjective`
- `continuous_linear_map.eq_on_closure_span`: if two continuous linear maps are equal on `s`,
then they are equal on `closure (submodule.span s)`;
- `continuous_linear_map.ext_on`: if two continuous linear maps are equal on a set `s` such that
`submodule.span s` is dense, then they are equal;
- `dense_closure`: `closure s` is dense iff `s` is dense;
- `dense.of_closure`, `dense.closure`: aliases for `dense_closure.mp` and `dense_closure.mpr`;
- `dense_univ`: `univ` is dense;
- `dense.inter_open_nonempty`: alias for `dense_iff_inter_open.mp`;
- `dense.nonempty_iff`: if `s : set α` is a dense set, then `s` is nonempty iff `α` is nonempty;
- `dense.nonempty`: a dense set in a nonempty type is nonempty;
- `dense_range.some`: given a function with `dense_range` and a point in the codomain, returns a point in the domain;
- `function.surjective.dense_range`: a surjective function has dense range;
- `continuous.range_subset_closure_image_dense`: closure of the image of a dense set under
a continuous function includes the range of this function;
- `dense_range.dense_of_maps_to`: if a function with dense range maps a dense set `s` to `t`, then
`t` is dense in the codomain;
- `dense_range.quotient`;
- `dense.prod`: product of two dense sets is dense in the product;
- `set.eq_on.closure`;
- `continuous.ext_on`;
- `linear_map.ext_on`
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
