mathlib3
feat(order/omega-cpo): cpos form a cartesian closed category
#4348

Open

feat(order/omega-cpo): cpos form a cartesian closed category #4348

cipher1024 wants to merge 7 commits into master from cpos-form-a-ccc

feat(order/omega-cpo): cpos form a cartesian closed category

1ab14957

use lint

e289e0bf

remove redundant `exp`

2f884dea

squeeze simp

9be2c6a9

separate out adjunction

b1413986

cipher1024 requested a review from

b-mehta 5 years ago

the re-lintening

f33ebedf

little fix

f4b85690

bryangingechen added awaiting-review

kim-em commented on 2020-10-02

kim-em removed awaiting-review

kim-em added awaiting-author

cipher1024 removed awaiting-author

cipher1024 added awaiting-review

kim-em removed awaiting-review

kim-em added awaiting-author

github-actions added merge-conflict

kim-em added too-late

Reviewers

b-mehta

kim-em

Assignees

No one assigned

Labels

awaiting-author merge-conflict too-late

Milestone

No milestone