Commit 2022-06-01 15:09 dba797a4

feat(order/liminf_limsup): composition g ∘ f is bounded iff f is bounded (#14479)

• If g is a monotone function that tends to infinity at infinity, then a filter is bounded from above under g ∘ f iff it is bounded under f, similarly for antitone functions and/or filter bounded from below.
• A filter is bounded from above under real.exp ∘ f iff it is is bounded from above under f.
• Use monotone in real.exp_monotone.
• Add @[mono] to real.exp_strict_mono.