Theorem NNReal.tendsto_of_antitone

Modification history

2024-05-10 17:03
Mathlib/Topology/Instances/NNReal.lean
feat(Topology/Instances/NNReal): add tendsto_of_antitone (#12430)
Added NNReal.tendsto_of_antitoneView on Github →