[Merged by Bors] - feat(topology/vector_bundle): topological_vector_prebundle
#8154
Conversation
Nicknamen
added
the
awaiting-review
Nicknamen
force-pushed
the
topological_vector_prebundle
branch
from
7b7684f
to
cbcacb0
Compare
sgouezel
added
awaiting-author
Nicknamen
added
awaiting-review
github-actions
bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
github-actions
bot
added
the
merge-conflict
leanprover-community-bot-assistant
removed
the
merge-conflict
Nicknamen
added
awaiting-review
src/topology/constructions.lean
Outdated
| @@ -628,6 +628,11 @@ end sum | |||
| section subtype | |||
| variables [topological_space α] [topological_space β] [topological_space γ] {p : α → Prop} | |||
|
|
|||
| lemma inducing_coe {b : set β} : inducing (coe : b → β) := ⟨rfl⟩ | |||
|
|
|||
| lemma inducing_of_inducing_cod_restrict {f : α → β} {b : set β} (hb : ∀ a, f a ∈ b) | |||
There was a problem hiding this comment.
| lemma inducing_of_inducing_cod_restrict {f : α → β} {b : set β} (hb : ∀ a, f a ∈ b) | |
| lemma inducing.of_cod_restrict {f : α → β} {b : set β} {hb : ∀ a, f a ∈ b} |
In this way, you can use dot notation.
There was a problem hiding this comment.
Totally agree for the name but why the curly brackets? When can lean guess that?
| lemma inducing_of_inducing_cod_restrict {f : α → β} {b : set β} (hb : ∀ a, f a ∈ b) | |
| lemma inducing.of_cod_restrict {f : α → β} {b : set β} (hb : ∀ a, f a ∈ b) |
There was a problem hiding this comment.
I will start merging this to move on with the other PRs. If the parentheses are important feel free to stop the merge
There was a problem hiding this comment.
The parentheses are not really important. It would be better with the curly brackets, as I wrote, because hb can already be seen explicitly in the next argument h so there's no need to write it twice. In the way it's currently written, it will just lead to useless underscores when you apply the lemma. But since you have already sent it to bors, let's not stop the build for that.
There was a problem hiding this comment.
Oh, I see, I think I wrote it that way because the only place where I used that was with an apply and so the last argument was not passed and lean could not guess it on its own, but I will for sure change it as you say the next time I use it in the standard way!
|
✌️ Nicknamen can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
|
bors r+ |
In this PR we implement a new standard construction for topological vector bundles: namely a structure that permits to define a vector bundle when trivializations are given as local equivalences but there is not yet a topology on the total space. The total space is hence given a topology in such a way that there is a vector bundle structure for which the local equivalences are also local homeomorphism and hence local trivializations.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
topological_vector_prebundletopological_vector_prebundle
In this PR we implement a new standard construction for topological vector bundles: namely a structure that permits to define a vector bundle when trivializations are given as local equivalences but there is not yet a topology on the total space. The total space is hence given a topology in such a way that there is a vector bundle structure for which the local equivalences
are also local homeomorphism and hence local trivializations.
Hopefully this should be easy.