mathlib3
chore(order/liminf_limsup): lint and cleanup the file
#2162

Merged

chore(order/liminf_limsup): lint and cleanup the file #2162

mergify merged 4 commits into master from sgouezel_liminf

chore(order/liminf_limsup): lint and cleanup the file, add some state…

0f0255c2

urkud commented on 2020-03-15

use eventually_mono

464b34d8

robertylewis approved these changes on 2020-03-16

robertylewis added ready-to-merge

Merge branch 'master' into sgouezel_liminf

5bbc62df

Merge branch 'master' into sgouezel_liminf

1d2cca34

mergify merged 7a5496f6 into master 6 years ago

mergify deleted the sgouezel_liminf branch 6 years ago

Reviewers

robertylewis

urkud

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone