mathlib3
refactor(order/bounds): use dot notation, reorder, prove more properties
#2028

Merged

refactor(order/bounds): use dot notation, reorder, prove more properties #2028

mergify merged 8 commits into master from bounds-rewrite

refactor(order/bounds): use dot notation, prove more properties

0df4835a

sgouezel commented on 2020-02-20

Comments

242d6d43

Add a module docstring

1955f5ae

urkud added awaiting-review

sgouezel commented on 2020-02-23

urkud removed awaiting-review

urkud added awaiting-author

Fixes from review, +4 lemmas about images

0cde4cf2

urkud removed awaiting-author

urkud added awaiting-review

Fix a typo in the previous commit

a9ff01b0

sgouezel commented on 2020-02-25

Update src/order/bounds.lean

ce9bc8a2

Update src/order/bounds.lean

727ae110

sgouezel approved these changes on 2020-02-25

sgouezel removed awaiting-review

sgouezel added ready-to-merge

Merge branch 'master' into bounds-rewrite

64383c02

mergify merged 450dcdf9 into master 5 years ago

mergify deleted the bounds-rewrite branch 5 years ago

Reviewers

sgouezel

digama0

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone