Commit 2020-08-01 15:55 92a20e64

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 aimplies is_min_filter l g a