[Merged by Bors] - refactor(data/nat/lattice): move code, add lemmas #8708
Conversation
| namespace enat | ||
| open_locale classical | ||
|
|
||
| noncomputable instance : complete_linear_order enat := |
There was a problem hiding this comment.
Does it make more sense to put this in data.nat.enat and change the imports a bit? Or does that not work?
There was a problem hiding this comment.
I have no opinion here. Actually, I wanted to add nat.supr_lt_succ etc and there was no good home for these lemmas, so I moved code around. If you want me to make data.nat.enat import data.nat.lattice, then I can do it. OTOH, having all *nat (conditionally) complete lattice instances in one file makes sense too.
There was a problem hiding this comment.
I also don't care and don't think it matters much, just caught my eye that this was the only mention of enat in the new file and it came at the very end. Up to you.
| /-- This instance is necessary, otherwise the lattice operations would be derived via | ||
| conditionally_complete_linear_order_bot and marked as noncomputable. -/ | ||
| instance : lattice ℕ := lattice_of_linear_order |
There was a problem hiding this comment.
Should this go here?
mathlib/src/order/lattice.lean
Lines 622 to 623 in e6e5718
There was a problem hiding this comment.
I don't want to move more instances from files deeper in the import chain without a reason.
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors merge |
github-actions
bot
added
the
ready-to-merge
* move `nat.conditionally_complete_linear_order_with_bot` and `enat.complete_linear_order` to a new file `data.nat.lattice`; * add a few lemmas (`nat.supr_lt_succ` etc), move `set.bUnion_lt_succ` to the same file; * use `galois_insertion.lift_complete_lattice` to define `enat.complete_linear_order`.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
| /-! | ||
| # Conditionally complete linear order structure on `ℕ` | ||
|
|
||
| In this file we |
There was a problem hiding this comment.
Can somebody fix this broken docstring?
nat.conditionally_complete_linear_order_with_botandenat.complete_linear_orderto a new filedata.nat.lattice;nat.supr_lt_succetc), moveset.bUnion_lt_succto the same file;galois_insertion.lift_complete_latticeto defineenat.complete_linear_order.