mathlib

40f673ee - feat(data/set/intervals/pi): lemmas about intervals in `Π i, π i` (#4951)

feat(data/set/intervals/pi): lemmas about intervals in `Π i, π i` (#4951) Also add missing lemmas `Ixx_mem_nhds` and lemmas `pi_Ixx_mem_nhds`. For each `pi_Ixx_mem_nhds` I add a non-dependent version `pi_Ixx_mem_nhds'` because sometimes Lean fails to unify different instances while trying to apply the dependent version to `ι → ℝ`.