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.
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
[Merged by Bors] - refactor(topology/bases): use structure
for `is_topological_basis
#6947
Conversation
* add `set.range_prod_map` and `set.countable.image2`; * move `@[simp]` from `set.mem_image2` to `set.mem_image2_eq` so that `dsimp` can use it; * rename `set.countable_prod` to `set.countable.prod`.
🎉 Great news! Looks like all the dependencies have been resolved:
💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
Can you merge master to hide from the diff what has already been merged? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Much better, thanks!
bors d+
src/topology/bases.lean
Outdated
⟨λ ha, let ⟨b, hb, ab, bu⟩ := mem_basis_subset_of_mem_open hB ha ou in | ||
⟨b, ⟨hb, bu⟩, ab⟩, | ||
λ ⟨b, ⟨hb, bu⟩, ab⟩, bu ab⟩⟩ | ||
⟨{s ∈ B | s ⊆ u}, λ s h, h.1, hB.open_eq_sUnion' ou⟩ | ||
|
||
lemma Union_basis_of_is_open {B : set (set α)} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
dot notation also for this one?
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…6947) * turn `topological_space.is_topological_basis` into a `structure`; * rename `mem_nhds_of_is_topological_basis` to `is_topological_basis.mem_nhds_iff`; * rename `is_open_of_is_topological_basis` to `is_topological_basis.is_open`; * rename `mem_basis_subset_of_mem_open` to `is_topological_basis.exists_subset_of_mem_open`; * rename `sUnion_basis_of_is_open` to `is_topological_basis.open_eq_sUnion`, add prime version; * add `is_topological_basis.prod`; * add convenience lemma `is_topological_basis.second_countable_topology`; * rename `is_open_generated_countable_inter` to `exists_countable_basis`; * add `topological_space.countable_basis` and API around it; * add `@[simp]` to `opens.mem_supr`, add `opens.mem_Sup`; * golf
Pull request successfully merged into master. Build succeeded: |
structure
for `is_topological_basisstructure
for `is_topological_basis
…6947) * turn `topological_space.is_topological_basis` into a `structure`; * rename `mem_nhds_of_is_topological_basis` to `is_topological_basis.mem_nhds_iff`; * rename `is_open_of_is_topological_basis` to `is_topological_basis.is_open`; * rename `mem_basis_subset_of_mem_open` to `is_topological_basis.exists_subset_of_mem_open`; * rename `sUnion_basis_of_is_open` to `is_topological_basis.open_eq_sUnion`, add prime version; * add `is_topological_basis.prod`; * add convenience lemma `is_topological_basis.second_countable_topology`; * rename `is_open_generated_countable_inter` to `exists_countable_basis`; * add `topological_space.countable_basis` and API around it; * add `@[simp]` to `opens.mem_supr`, add `opens.mem_Sup`; * golf
topological_space.is_topological_basis
into astructure
;mem_nhds_of_is_topological_basis
tois_topological_basis.mem_nhds_iff
;is_open_of_is_topological_basis
tois_topological_basis.is_open
;mem_basis_subset_of_mem_open
tois_topological_basis.exists_subset_of_mem_open
;sUnion_basis_of_is_open
tois_topological_basis.open_eq_sUnion
, add prime version;is_topological_basis.prod
;is_topological_basis.second_countable_topology
;is_open_generated_countable_inter
toexists_countable_basis
;topological_space.countable_basis
and API around it;@[simp]
toopens.mem_supr
, addopens.mem_Sup
;set.countable.prod