[Merged by Bors] - feat(data/fintype/order): complete order instances for fintype #7123

apnelson1 · 2021-04-08T19:08:03Z

This PR adds several instances (as defs) for fintypes:

order_bot from semilattice_inf, order_top from semilattice_sup, bounded_order from lattice.
complete_lattice from lattice.
complete_linear_order from linear_order.

We use this last one to give a complete_linear_order instance for fin (n + 1) .

src/data/fintype/order.lean

hrmacbeth

silly tweaks :)

src/data/fintype/order.lean

Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>

src/data/fintype/order.lean

added explicit instance for fin n+1

src/data/fintype/order.lean

lattice -> bounded_lattice -> complete_lattice instead of going through complete_semilattice_Sup

src/data/fintype/order.lean

jcommelin · 2021-08-09T13:42:40Z

@apnelson1 What's the status of this PR? Do you intend to return to it in the near future? Or would you like someone else to adopt it?

apnelson1 · 2021-08-09T13:44:32Z

@apnelson1 What's the status of this PR? Do you intend to return to it in the near future? Or would you like someone else to adopt it?

The status is 'parental leave'. I will return to work next month - I am happy to have someone else adopt the PR in the meantime if that makes sense, though.

jcommelin · 2021-08-12T09:51:51Z

Ok, thanks for the update! Enjoy your time with your family!

…near_order

src/data/fintype/order.lean

eric-wieser

Don't all the lemmas here hold generally for any complete lattice on a fintype, not just these ones?

src/data/fintype/order.lean

urkud · 2021-12-02T22:02:16Z

src/data/fintype/order.lean

+equality for `⊥` and `⊤`. -/
+noncomputable def fintype.to_complete_linear_order [h : linear_order α] : complete_linear_order α :=
+{ .. fintype.to_complete_lattice_of_lattice α,
+  .. h }


Could you please create two versions of this def (one with [bounded_order α] and one without)? Otherwise API for complete_lattice is inconsistent with API for complete_order.
Otherwise LGTM. Thanks!
bors d+

You might want to delegate me instead. I'm not sure Peter is checking much on mathlib these days.

bors · 2021-12-02T22:02:18Z

✌️ apnelson1 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

urkud · 2021-12-02T22:04:50Z

UPD: Probably, all these defs should be @[reducible].

jcommelin

Thanks 🎉

bors merge

This PR adds several instances (as defs) for fintypes: * `order_bot` from `semilattice_inf`, `order_top` from `semilattice_sup`, `bounded_order` from `lattice`. * `complete_lattice` from `lattice`. * `complete_linear_order` from `linear_order`. We use this last one to give a `complete_linear_order` instance for `fin (n + 1)` . Co-authored-by: Peter Nelson <apnelson@uwaterloo.ca> Co-authored-by: Peter Nelson <71660771+apnelson1@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: YaelDillies <yael.dillies@gmail.com>

bors · 2021-12-03T14:32:08Z

Pull request successfully merged into master.

Build succeeded:

This PR adds several instances (as defs) for fintypes: * `order_bot` from `semilattice_inf`, `order_top` from `semilattice_sup`, `bounded_order` from `lattice`. * `complete_lattice` from `lattice`. * `complete_linear_order` from `linear_order`. We use this last one to give a `complete_linear_order` instance for `fin (n + 1)` . Co-authored-by: Peter Nelson <apnelson@uwaterloo.ca> Co-authored-by: Peter Nelson <71660771+apnelson1@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: YaelDillies <yael.dillies@gmail.com>

apnelson1 added the awaiting-review The author would like community review of the PR label Apr 8, 2021

bryangingechen changed the title ~~feat(data.fintype.order): complete order instances for fintype~~ feat(data/fintype/order): complete order instances for fintype Apr 8, 2021

b-mehta reviewed Apr 8, 2021

View reviewed changes

src/data/fintype/order.lean Outdated Show resolved Hide resolved

src/data/fintype/order.lean Outdated Show resolved Hide resolved

src/data/fintype/order.lean Outdated Show resolved Hide resolved

src/data/fintype/order.lean Outdated Show resolved Hide resolved

b-mehta and others added 2 commits April 8, 2021 20:46

golf, move and dualise proof

6798752

incorporated exists_min

3f737c7

apnelson1 force-pushed the fintype_complete_linear_order branch from 276ce6a to 3f737c7 Compare April 8, 2021 20:17

github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 8, 2021

hrmacbeth reviewed Apr 8, 2021

View reviewed changes

src/data/fintype/order.lean Outdated Show resolved Hide resolved

src/data/fintype/order.lean Outdated Show resolved Hide resolved

src/data/fintype/order.lean Outdated Show resolved Hide resolved

src/data/fintype/order.lean Outdated Show resolved Hide resolved

apnelson1 and others added 4 commits April 8, 2021 16:32

Update src/data/fintype/order.lean

35793ac

Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>

Update src/data/fintype/order.lean

bb4b7a3

Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>

Update src/data/fintype/order.lean

949142d

Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>

Update src/data/fintype/order.lean

9c687bf

Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>

eric-wieser reviewed Apr 8, 2021

View reviewed changes

src/data/fintype/order.lean Outdated Show resolved Hide resolved

b-mehta reviewed Apr 8, 2021

View reviewed changes

src/data/fintype/order.lean Outdated Show resolved Hide resolved

github-actions bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Apr 9, 2021

apnelson1 added 3 commits April 9, 2021 08:51

docstring

b0c07ce

fixed instance name

38cb76a

whitespace

fb404dc

gebner reviewed Apr 9, 2021

View reviewed changes

src/data/fintype/order.lean Outdated Show resolved Hide resolved

gebner added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Apr 9, 2021

changed instances to defs to avoid instance search problems

48ddf41

added explicit instance for fin n+1

eric-wieser reviewed Apr 12, 2021

View reviewed changes

src/data/fintype/order.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Apr 12, 2021

View reviewed changes

src/data/fintype/order.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Apr 12, 2021

View reviewed changes

src/data/fintype/order.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Apr 12, 2021

View reviewed changes

src/data/fintype/order.lean Outdated Show resolved Hide resolved

apnelson1 added 2 commits April 12, 2021 17:40

substantial rewrite -

b1ab13b

lattice -> bounded_lattice -> complete_lattice instead of going through complete_semilattice_Sup

added computable stuff

495e79e

apnelson1 added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 12, 2021

eric-wieser reviewed May 4, 2021

View reviewed changes

src/data/fintype/order.lean Outdated Show resolved Hide resolved

add fintype.(supr|infi)_eq

899b764

YaelDillies added 2 commits November 26, 2021 10:30

Merge remote-tracking branch 'origin/master' into fintype_complete_li…

556fbef

…near_order

bump mathlib

f25c406

YaelDillies self-assigned this Nov 26, 2021

YaelDillies added 2 commits November 27, 2021 09:33

fix, add fin lemmas

149fd62

simping

4ae7f3f

YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Nov 27, 2021

eric-wieser reviewed Nov 27, 2021

View reviewed changes

src/data/fintype/order.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Nov 27, 2021

View reviewed changes

src/data/fintype/order.lean Outdated Show resolved Hide resolved

trim off lemmas

0561d48

urkud reviewed Dec 2, 2021

View reviewed changes

YaelDillies added 2 commits December 2, 2021 22:48

add bounded_order version, reducible

d1d44ac

fix unused argument

85fe686

jcommelin approved these changes Dec 3, 2021

View reviewed changes

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Dec 3, 2021

bors bot changed the title ~~feat(data/fintype/order): complete order instances for fintype~~ [Merged by Bors] - feat(data/fintype/order): complete order instances for fintype Dec 3, 2021

bors bot closed this Dec 3, 2021

bors bot deleted the fintype_complete_linear_order branch December 3, 2021 14:32

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(data/fintype/order): complete order instances for fintype #7123

[Merged by Bors] - feat(data/fintype/order): complete order instances for fintype #7123

apnelson1 commented Apr 8, 2021 •

edited by YaelDillies

hrmacbeth left a comment

jcommelin commented Aug 9, 2021

apnelson1 commented Aug 9, 2021

jcommelin commented Aug 12, 2021

eric-wieser left a comment

urkud Dec 2, 2021

YaelDillies Dec 2, 2021

bors bot commented Dec 2, 2021

urkud commented Dec 2, 2021

jcommelin left a comment

bors bot commented Dec 3, 2021

[Merged by Bors] - feat(data/fintype/order): complete order instances for fintype #7123

[Merged by Bors] - feat(data/fintype/order): complete order instances for fintype #7123

Conversation

apnelson1 commented Apr 8, 2021 • edited by YaelDillies

hrmacbeth left a comment

Choose a reason for hiding this comment

jcommelin commented Aug 9, 2021

apnelson1 commented Aug 9, 2021

jcommelin commented Aug 12, 2021

eric-wieser left a comment

Choose a reason for hiding this comment

urkud Dec 2, 2021

Choose a reason for hiding this comment

YaelDillies Dec 2, 2021

Choose a reason for hiding this comment

bors bot commented Dec 2, 2021

urkud commented Dec 2, 2021

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Dec 3, 2021

apnelson1 commented Apr 8, 2021 •

edited by YaelDillies