[Merged by Bors] - feat(order/filter): change definition of inf #8657
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
PatrickMassot
added
the
awaiting-review
sgouezel
reviewed
Aug 13, 2021
|
LGTM. I'll leave some time for others to have a look if they want, but still I think we should merge this pretty quickly to avoid conflicts. |
|
✌️ PatrickMassot can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
I golfed a few proofs. LGTM. Thanks! |
|
✌️ PatrickMassot can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
the
merge-conflict
also renames lots of lemmas to remove the word "sets" that was a remnant of the very early days.
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
PatrickMassot
force-pushed
the
filter_stuff
branch
from
9796462
to
6dc4f77
Compare
|
bors merge |
|
👎 Rejected by label |
github-actions
bot
added
ready-to-merge
|
bors merge |
bors bot
pushed a commit
that referenced
this pull request
Aug 13, 2021
The current definition of `filter.inf` came directly from the Galois insertion: `u ∈ f ⊓ g` if it contains `s ∩ t` for some `s ∈ f` and `t ∈ g`, but the new one is tidier: `u ∈ f ⊓ g` if `u = s ∩ t` for some `s ∈ f` and `t ∈ g`. This gives a stronger assertion to work with when assuming a set belongs to a filter inf. On the other hand it makes it harder to prove such a statement so we keep the old version as a lemma `filter.mem_inf_of_inter : ∀ {f g : filter α} {s t u : set α}, s ∈ f → t ∈ g → s ∩ t ⊆ u → u ∈ f ⊓ g`.
Also renames lots of lemmas to remove the word "sets" that was a remnant of the very early days.
In passing I also changed the simp lemma `filter.mem_map` from `t ∈ map m f ↔ {x | m x ∈ t} ∈ f` to
`t ∈ map m f ↔ m ⁻¹' t ∈ f` which seemed more normal form to me. But this led to a lot of breakage, so I also kept the old version as `mem_map'`.
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
PatrickMassot
added a commit
that referenced
this pull request
Aug 15, 2021
Also finishes the filter inf work from #8657 proving stronger lemmas for filter.infi
bors bot
pushed a commit
that referenced
this pull request
Aug 23, 2021
Also finishes the filter inf work from #8657 proving stronger lemmas for filter.infi Co-authored-by: Johan Commelin <johan@commelin.net>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The current definition of
filter.infcame directly from the Galois insertion:u ∈ f ⊓ gif it containss ∩ tfor somes ∈ fandt ∈ g, but the new one is tidier:u ∈ f ⊓ gifu = s ∩ tfor somes ∈ fandt ∈ g. This gives a stronger assertion to work with when assuming a set belongs to a filter inf. On the other hand it makes it harder to prove such a statement so we keep the old version as a lemmafilter.mem_inf_of_inter : ∀ {f g : filter α} {s t u : set α}, s ∈ f → t ∈ g → s ∩ t ⊆ u → u ∈ f ⊓ g.Also renames lots of lemmas to remove the word "sets" that was a remnant of the very early days.
In passing I also changed the simp lemma
filter.mem_mapfromt ∈ map m f ↔ {x | m x ∈ t} ∈ ftot ∈ map m f ↔ m ⁻¹' t ∈ fwhich seemed more normal form to me. But this led to a lot of breakage, so I also kept the old version asmem_map'.