Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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>
- Loading branch information
1 parent
fde3d78
commit 2543b68
Showing
23 changed files
with
347 additions
and
313 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.