ordered): rename `tendsto_of_tendsto_of_tendsto_of_le_of_le` to `tendsto_of_tendsto_of_tendsto_of_le_of_le'`
#2111

Merged

refactor(topology/algebra/ordered): rename `tendsto_of_tendsto_of_tendsto_of_le_of_le` to `tendsto_of_tendsto_of_tendsto_of_le_of_le'` #2111

mergify merged 2 commits into master from squeeze-prime

refactor(topology/algebra/ordered): rename `tendsto_of_tendsto_of_ten…

0752af60

cipher1024 assigned

sgouezel 6 years ago

sgouezel approved these changes on 2020-03-09

sgouezel added ready-to-merge

Merge branch 'master' into squeeze-prime

5f03c040

mergify merged d8d09271 into master 6 years ago

mergify deleted the squeeze-prime branch 6 years ago

Reviewers

sgouezel

Assignees

sgouezel

Labels

ready-to-merge

Milestone

No milestone