[Merged by Bors] - refactor(order/upper_lower): Reverse the order on upper_set
#14982
Conversation
YaelDillies
added
the
awaiting-review
Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
|
I think it's worth adding a docstring somewhere explaining the rationale for the change: your justification is sound to me, but I can imagine others reading the library later and not realising the purpose |
| by simp_rw lower_set.compl_infi | ||
|
|
||
| end lower_set | ||
|
|
||
| /-- Upper sets are order-isomorphic to lower sets under complementation. -/ | ||
| @[simps] def upper_set_iso_lower_set : upper_set α ≃o lower_set α := |
There was a problem hiding this comment.
If you put this just after compl_le_compl, does it give one-line proofs of compl_top and all of those lemmas?
There was a problem hiding this comment.
It would, but the proofs still would end up being longer by virtue of upper_set_iso_lower_set being a long name. Further, I can't really see how to incorporate this in the flow of the file, given that it would need to be out of the namespaces but come between upper_set.compl/lower_set.compl and their API.
|
bors d+ |
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
Thanks Bhavik! bors merge |
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
upper_setupper_set
| @@ -370,40 +386,39 @@ def Ioi (a : α) : upper_set α := ⟨Ioi a, is_upper_set_Ioi a⟩ | |||
| @[simp] lemma mem_Ici_iff : b ∈ Ici a ↔ a ≤ b := iff.rfl | |||
| @[simp] lemma mem_Ioi_iff : b ∈ Ioi a ↔ a < b := iff.rfl | |||
|
|
|||
| lemma Ioi_le_Ici (a : α) : Ioi a ≤ Ici a := Ioi_subset_Ici_self | |||
| lemma Icoi_le_Ioi (a : α) : Ici a ≤ Ioi a := Ioi_subset_Ici_self | |||
Having
upper_setbeing ordered by reverse inclusion makes it order-isomorphic tolower_set(and antichains once we have them as a type) and it matches the order onfilter.