mathlib

7130d75d - chore(*): introduce notation for left/right/punctured nhds (#10694)

chore(*): introduce notation for left/right/punctured nhds (#10694) New notation: * `𝓝[≤] x`: the filter `nhds_within x (set.Iic x)` of left-neighborhoods of `x`; * `𝓝[≥] x`: the filter `nhds_within x (set.Ici x)` of right-neighborhoods of `x`; * `𝓝[<] x`: the filter `nhds_within x (set.Iio x)` of punctured left-neighborhoods of `x`; * `𝓝[>] x`: the filter `nhds_within x (set.Ioi x)` of punctured right-neighborhoods of `x`; * `𝓝[≠] x`: the filter `nhds_within x {x}ᶜ` of punctured neighborhoods of `x`.