ordered): `le_of_tendsto`: use `∀ᶠ`, add primed versions
#2270

Merged

chore(topology/algebra/ordered): `le_of_tendsto`: use `∀ᶠ`, add primed versions #2270

mergify merged 2 commits into master from le-of-tendsto

chore(topology/algebra/ordered): `le_of_tendsto`: use `∀ᶠ`, add prime…

e04f739a

sgouezel added ready-to-merge

sgouezel approved these changes on 2020-03-29

Merge branch 'master' into le-of-tendsto

abc25134

mergify merged c14c84e4 into master 6 years ago

urkud deleted the le-of-tendsto branch 6 years ago

Reviewers

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone