mathlib

5776f4c0 - feat(topology): more lemmas about Ici and Iic neighborhoods (#3474)

feat(topology): more lemmas about Ici and Iic neighborhoods (#3474) Main feature : add `tfae_mem_nhds_within_Ici` and `tfae_mem_nhds_within_Iic`, analogous to the existing `tfae_mem_nhds_within_Ioi` and `tfae_mem_nhds_within_Iio`, as well as related lemmas (again imitating the open case) I also added a few lemmas in `data/set/intervals/basic.lean` that were useful for this and a few upcoming PRs Co-authored-by: Anatole Dedecker <48656793+ADedecker@users.noreply.github.com>