Commit 2024-05-10 17:03 c052670b

View on Github →

feat(Topology/Instances/NNReal): add tendsto_of_antitone (#12430)

Estimated changes

Modified Mathlib/Data/Real/Archimedean.lean

added theorem Real.exists_isGLB

modified theorem Real.exists_isLUB

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/Topology/Instances/NNReal.lean

added theorem NNReal.tendsto_of_antitone

added theorem Real.tendsto_of_bddAbove_monotone

added theorem Real.tendsto_of_bddBelow_antitone