mathlib

f4106afc - feat(order/filters, topology): relation between neighborhoods of a in [a, u), [a, u] and [a,+inf) + various nhds_within lemmas (#3516)

feat(order/filters, topology): relation between neighborhoods of a in [a, u), [a, u] and [a,+inf) + various nhds_within lemmas (#3516) Content : - two lemmas about filters, namely `tendsto_sup` and `eventually_eq_inf_principal_iff` - a few lemmas about `nhds_within` - duplicate and move parts of the lemmas `tfae_mem_nhds_within_[Ioi/Iio/Ici/Iic]` that only require `order_closed_topology α` instead of `order_topology α`. This allows to turn any left/right neighborhood of `a` into its "canonical" form (i.e `Ioi`/`Iio`/`Ici`/`Iic`) with a weaker assumption than before Co-authored-by: Anatole Dedecker <48656793+ADedecker@users.noreply.github.com>