mathlib

92a20e64 - feat(order/filter/extr, topology/local_extr): links between extremas of two eventually le/eq functions (#3624)

feat(order/filter/extr, topology/local_extr): links between extremas of two eventually le/eq functions (#3624) Add many lemmas that look similar to e.g : if f and g are equal at `a`, and `f ≤ᶠ[l] g` for some filter `l`, then `is_min_filter l f a`implies `is_min_filter l g a`