feat(SpaceAndTime/Space/Basic): IsManifold instance for Space #1176
feat(SpaceAndTime/Space/Basic): IsManifold instance for Space #1176Bergschaf wants to merge 4 commits into
Conversation
|
Thank you for this PR, which will now be reviewed. Please If you want to bring attention to this PR, please write a message on this |
|
|
||
| lemma toOpenPartialHomeomorph_trans_localInverseAt (φ : X ≃ₜ Y) (m : X) : | ||
| (φ.toOpenPartialHomeomorph.trans (φ.isLocalHomeomorph.localInverseAt m)).EqOnSource | ||
| <| .ofSet (φ ⁻¹' (φ.isLocalHomeomorph.localInverseAt m).source) |
There was a problem hiding this comment.
This ofSet just needs to be added to the list of allowed words.
There was a problem hiding this comment.
Sorry, I don't understand what you mean here
There was a problem hiding this comment.
Sorry - I meant the spell-check linter is picking ofSet up as a mis-spelling of offset. We just need to add ofSet to:
https://github.com/leanprover-community/physlib/blob/master/.codespellignore
2 participants
No description provided.