mathlib3

a0e2c623 - 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)

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) This PR adds antitone versions of lemmas about supremum and infimum under monotone functions and moves those lemmas to monotone/antitone namespaces. Simultaneously, the type class assumption on the codomain is weakened from `order_topology` to `order_closed_topology`. Moreover, lemmas about limsup and liminf under monotone/antitone functions are added: `antitone.map_Limsup_of_continuous_at` etc. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com>