-
Notifications
You must be signed in to change notification settings - Fork 298
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] - feat(topology/topological_fiber_bundle): topological fiber bundle over [a, b]
is trivial
#6555
Conversation
urkud
commented
Mar 5, 2021
•
edited
edited
I assume you will refactor this in terms of |
I'm sorry for forgetting to set |
65cb090
to
5d51a86
Compare
local_equiv.piecewise
[a, b]
is trivial
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.
LGTM, thanks!
e.trans_fiber_homeomorph h x = ((e x).1, h (e x).2) := | ||
rfl | ||
|
||
/-- Coordinate transformation in the fiber induced by a pair of bundle trivializations. -/ |
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.
Can you mention the homeomorphism version in this docstring, as this is the one one will use most often?
(h : is_topological_fiber_bundle F proj) (a b : B) : | ||
∃ e : bundle_trivialization F proj, Icc a b ⊆ e.base_set := | ||
begin | ||
classical, |
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.
Could you add a few comments to this proof (replacing some rcases
with obtain
could also improve a little bit the readability, although the current version is already pretty readable)?
bf86553
to
197f376
Compare
@sgouezel There was no formal |
bors r+ |
…r `[a, b]` is trivial (#6555)
Build failed (retrying...): |
…r `[a, b]` is trivial (#6555)
…r `[a, b]` is trivial (#6555)
Pull request successfully merged into master. Build succeeded: |
[a, b]
is trivial[a, b]
is trivial