[Merged by Bors] - feat: Exterior of a set #6982
Conversation
In an Alexandrov-discrete space, every set has a smallest neighborhood. We call this neighborhood the *exterior* of the set. It is completely analogous to the interior, except that all inclusions are reversed.
YaelDillies
added
awaiting-review
t-topology
YaelDillies
added
the
blocked-by-other-PR
leanprover-community-mathlib4-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on:
|
| (interior_maximal (iInter_mono λ _ ↦ interior_subset) $ isOpen_iInter λ _ ↦ | ||
| isOpen_interior).antisymm' $ subset_iInter λ _ ↦ interior_mono $ iInter_subset _ _ |
There was a problem hiding this comment.
I'm pretty sure that our new convention is to indent the body of all declarations, even in term mode. Also, <| is preferred to $, and fun to λ.
There was a problem hiding this comment.
How is <| preferred over $? This does not appear in the style guide.
This to me looks like a mathportism. Mathport output code which uses <| even though we haven't decided on using it over $.
There was a problem hiding this comment.
Well it mentions <| but not $.
There was a problem hiding this comment.
I'm not looking for style suggestions, really. Especially when they involve more ASCII art than the alternative.
There was a problem hiding this comment.
I'm unresolving this at least for the indentation part, which is clearly stated in the style guide.
There was a problem hiding this comment.
Regarding "mathportism", I really don't think that's what's happening here. People have already spent quite some time doing new maths in Lean4, and there's been complains about a lot of things but almost none about this. I can't speak for everyone, but at least I willingly embraced the new style for the most part, and not because it was used by mathport.
Of course that doesn't mean that it's clearly better, but I would say that for now it's better to stick to what's used in the existing human-written codebase, and that means fun and <|.
There was a problem hiding this comment.
Then your argument is saying that I can stick to λ and $: λ is used 395 times across 79 files, and $ at least 619 times across 202 files.
Again, I am not looking for style suggestions.
ADedecker
added
awaiting-author
YaelDillies
added
awaiting-review
and removed
awaiting-author
ADedecker
added
awaiting-author
YaelDillies
added
awaiting-review
and removed
awaiting-author
leanprover-community-mathlib4-bot
added
ready-to-merge
In an Alexandrov-discrete space, every set has a smallest neighborhood. We call this neighborhood the *exterior* of the set. It is completely analogous to the interior, except that all inclusions are reversed.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
In an Alexandrov-discrete space, every set has a smallest neighborhood. We call this neighborhood the *exterior* of the set. It is completely analogous to the interior, except that all inclusions are reversed.
In an Alexandrov-discrete space, every set has a smallest neighborhood. We call this neighborhood the exterior of the set. It is completely analogous to the interior, except that all inclusions are reversed.