monotone_convergence): add `antitone.{ge,le}_of_tendsto` (#11754)

Commit

3 years ago

feat(topology/algebra/ordered/monotone_convergence): add `antitone.{ge,le}_of_tendsto` (#11754)

Author

ecstatic-morse

Parents