mathlib

d8d09271 - 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)

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) The new `tendsto_of_tendsto_of_tendsto_of_le_of_le` assumes that the inequalities hold everywhere. Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>