[Merged by Bors] - feat: the set of points where IsImmersionAt(OfComplement) holds is open #30356
[Merged by Bors] - feat: the set of points where IsImmersionAt(OfComplement) holds is open #30356grunweg wants to merge 4 commits intoleanprover-community:masterfrom
Conversation
PR summary fc14f3da77Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
e84a18d to
8bafa11
Compare
|
This pull request has conflicts, please merge |
|
This PR/issue depends on:
|
8bafa11 to
f259784
Compare
🚨 PR Title Needs FormattingPlease update the title to match our commit style conventions. Errors from script: Details on the required title formatThe title should fit the following format:
|
|
@chrisflav Here's the missing API lemma you asked for, on #28793. Feel free to review (but not obliged, I can easily ask somebody else). |
|
The failing PR title check is a bug in the checker... |
| /- The set of points where `LiftSourceTargetPropertyAt` holds is open. -/ | ||
| lemma _root_.isOpen_liftSourceTargetPropertyAt : |
There was a problem hiding this comment.
Why the _root_ namespace? For dot notation, this one could be in the IsSourceLocalTargetProperty namespace. Or in IsOpen for anonymous dot notation.
There was a problem hiding this comment.
I wasn't sure about a natural namespace. I have moved it to isOpen now.
|
-awaiting-author |
|
🚀 Pull request has been placed on the maintainer queue by chrisflav. |
|
bors r+ |
|
Pull request successfully merged into master. Build succeeded: |
Prove an API lemma which
chrisflavrequested in #28793, which was split from that PR to keep the diff smaller.