Commit 2020-07-26 10:41 f4106afc

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