2022-07-27 05:09
src/topology/algebra/order/liminf_limsup.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) …
Added monotone.map_Limsup_of_continuous_at