Mathlib v3 is deprecated. Go to Mathlib v4

Theorem monotone.tendsto_nhds_within_Ioi

Modification history

2022-07-27 05:09
src/topology/algebra/order/basic.lean
refactor(topology/algebra/order/basic): Add antitone versions of sup and inf lemmas for continuous monotone functions and move them to monotone/antitone namespaces. (#15218) …
Modified monotone.tendsto_nhds_within_IoiView on Github →
2021-08-12 17:46
src/topology/algebra/ordered/basic.lean
feat(measure_theory/stieltjes_measure): Stieltjes measures associated to monotone functions (#8266) …
Added monotone.tendsto_nhds_within_IoiView on Github →