mathlib3
refactor(order/bounds): make the first argument of `x ∈ upper_bounds s` implicit
#1691

Merged

refactor(order/bounds): make the first argument of `x ∈ upper_bounds s` implicit #1691

mergify merged 3 commits into master from bounds-implicit-arg

refactor(order/bounds): make the first argument of `x ∈ upper_bounds …

4160f4a5

Use `∈ *_bounds` in the definition of `conditionally_complete_lattice`.

b2d3f2bb

jcommelin commented on 2019-11-15

urkud added awaiting-review

sgouezel approved these changes on 2019-11-17

sgouezel added ready-to-merge

Merge branch 'master' into bounds-implicit-arg

01b35b5a

urkud removed awaiting-review

mergify merged 1805f16a into master 6 years ago

mergify deleted the bounds-implicit-arg branch 6 years ago

Reviewers

sgouezel

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone