[Merged by Bors] - feat: Extra sups lemmas
#7382
Conversation
YaelDillies
commented
Sep 26, 2023
YaelDillies
commented
Co-authored-by: Eric Wieser <[email protected]>
| subset_sups_self.le.le_iff_eq.symm.trans sups_self_subset | ||
|
|
||
| lemma sep_sups_le (s t : Set α) (a : α) : | ||
| {b ∈ s ⊻ t | b ≤ a} = {b ∈ s | b ≤ a} ⊻ {b ∈ t | b ≤ a} := by ext; aesop |
There was a problem hiding this comment.
Would it make sense to state this as (s ⊻ t) \inter Iic a = ...? Or is that less useful to you?
There was a problem hiding this comment.
For the Finset version, I must use filter since my order isn't locally finite. For the Set version, I don't really mind, except that using sep is more consistent than intersecting with Iic a.
What do you think? (I don't think it's too important so I'll merge the PR as is, but I'll modify that file quite a lot in the next few weeks so I'm happy to change later)
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks. That was quick! bors merge |
|
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
sups lemmassups lemmas
Match leanprover-community/mathlib3#18612. The lemmas were already added in #7382, though a slight difference in the statement means that we need a new `decidableExistsAndFinsetCoe` instance.
