linear orders
#820

Merged

feat(order/lexicographic): lexicographic pre/partial/linear orders #820

mergify merged 11 commits into master from lexicographic

kim-em requested a review from

digama0 6 years ago

kim-em requested a review from

ChrisHughes24 6 years ago

cipher1024 assigned

rwbarton 6 years ago

kim-em force pushed from fc0b1dd9 to cd966e85 6 years ago

jcommelin dismissed these changes on 2019-03-29

remove prod.(*)order instances

7173a373

feat(order/lexicographic): lexicographic pre/partial/linear orders

f2f69c47

add lex_decidable_linear_order

ebdbb4f9

identical constructions for dependent pairs

4608e50b

cleaning up

75b97cd4

Update lexicographic.lean

def4f93f

restore product instances, and add lex type synonym for lexicographic…

9f6b7a10

proofs in progress

2270f580

* define lt

38248a2c

kim-em force pushed from 3db2860e to 38248a2c 6 years ago

Merge branch 'master' into lexicographic

ea64bae5

kim-em requested a review 6 years ago

mergify dismissed their stale review 6 years ago

Pull request has been modified.

cipher1024 dismissed these changes on 2019-04-08

Merge branch 'master' into lexicographic

071485b0

mergify dismissed their stale review 6 years ago

Pull request has been modified.

cipher1024 approved these changes on 2019-04-09

cipher1024 added ready-to-merge

mergify merged eb024dc8 into master 6 years ago

mergify deleted the lexicographic branch 6 years ago

Reviewers

cipher1024

jcommelin

digama0

ChrisHughes24

Assignees

rwbarton

Labels

ready-to-merge

Milestone

No milestone

mathlib3 feat(order/lexicographic): lexicographic pre/partial/linear orders #820 Merged

feat(order/lexicographic): lexicographic pre/partial/linear orders #820

mathlib3
feat(order/lexicographic): lexicographic pre/partial/linear orders
#820

Merged