Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(topology): completion of separable space is separable #4399

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(topology): completion of separable space is separable #4399

wants to merge 5 commits into from

Conversation

PatrickMassot
Copy link
Member

@PatrickMassot PatrickMassot commented Oct 4, 2020 •
edited by urkud
Loading

API change:

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

This was asked on Zulip

@PatrickMassot PatrickMassot added the awaiting-review The author would like community review of the PR label Oct 4, 2020
@urkud
Copy link
Member

urkud commented Oct 4, 2020

Two minor comments:

  1. What do you think about renaming separable lemmas to separable_space and making them protected?
  2. Your dense_range lemmas come before the definition of dense_range, so they use ∀ y, y ∈ closure (range f) instead of dense_range f. What do you think about moving them to topology/dense_embedding and into the dense_range namespace (or moving the definition of dense_range to topology/basic)?

@PatrickMassot
Copy link
Member Author

I don't understand the first suggestion. Do you want to put lemmas in a separable_space namespace? I prefer putting them in name spaces that can be used with the dot notation, like continuous or dense_inducing.

About the second point, I guess the easiest thing is to move dense_range to topology.basic. Maybe we should also define dense : set X -> Prop.

@urkud
Copy link
Member

urkud commented Oct 4, 2020

I don't understand the first suggestion. Do you want to put lemmas in a separable_space namespace? I prefer putting them in name spaces that can be used with the dot notation, like continuous or dense_inducing.

No, I meant using dense_range.separable_space instead of dense_range.separable because this is the name convention we use in equiv.decidable_eq etc. Then these lemmas should be protected to avoid name conflict.

About the second point, I guess the easiest thing is to move dense_range to topology.basic. Maybe we should also define dense : set X -> Prop.

Looks good to me.

@urkud urkud added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 4, 2020
@PatrickMassot PatrickMassot added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 4, 2020
@urkud
Copy link
Member

urkud commented Oct 5, 2020

I've started looking into dense_range API, and I want to update it. But this will go to another PR.
bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Oct 5, 2020
bors bot pushed a commit that referenced this pull request Oct 5, 2020
@PatrickMassot
feat(topology): completion of separable space is separable (#4399)
916b5d3 
API change:

* `dense` renamed to `exists_between`;
* new `dense (s : set α)` means `∀ x, x ∈ closure s`.
@bors
Copy link

bors bot commented Oct 5, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(topology): completion of separable space is separable [Merged by Bors] - feat(topology): completion of separable space is separable Oct 5, 2020
@bors bors bot closed this Oct 5, 2020
@bors bors bot deleted the separable_completion branch October 5, 2020 04:07
@urkud urkud mentioned this pull request Oct 5, 2020
Closed
5 tasks
adomani pushed a commit that referenced this pull request Oct 7, 2020
@PatrickMassot @adomani
feat(topology): completion of separable space is separable (#4399)
dd60b03 
API change:

* `dense` renamed to `exists_between`;
* new `dense (s : set α)` means `∀ x, x ∈ closure s`.
bors bot pushed a commit that referenced this pull request Oct 13, 2020
@urkud @PatrickMassot @sgouezel
refactor(*): migrate to dense API (#4447)
2543b68 
@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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@PatrickMassot @urkud