mathlib3

438381a5 - feat(data/set/intervals/basic): Injectivity of half-infinite intervals (#17157)

feat(data/set/intervals/basic): Injectivity of half-infinite intervals (#17157) Adds lemma `set.Ici_eq_Ici_iff`, required by #17037. For completeness, the equivalent result for `Iic` is also included. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>