Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-09 00:48 40f673ee

View on Github →

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 ι → ℝ.

Estimated changes

added theorem set.pi_mono
added theorem set.pi_univ_Icc
added theorem set.pi_univ_Ici
added theorem set.pi_univ_Ico_subset
added theorem set.pi_univ_Iic
added theorem set.pi_univ_Iio_subset
added theorem set.pi_univ_Ioc_subset
added theorem set.pi_univ_Ioi_subset
added theorem set.pi_univ_Ioo_subset
added theorem pi.le_def
added theorem Icc_mem_nhds
added theorem Ici_mem_nhds
added theorem Ico_mem_nhds
added theorem Iic_mem_nhds
added theorem Ioc_mem_nhds
added theorem pi_Icc_mem_nhds'
added theorem pi_Icc_mem_nhds
added theorem pi_Ici_mem_nhds'
added theorem pi_Ici_mem_nhds
added theorem pi_Ico_mem_nhds'
added theorem pi_Ico_mem_nhds
added theorem pi_Iic_mem_nhds'
added theorem pi_Iic_mem_nhds
added theorem pi_Iio_mem_nhds'
added theorem pi_Iio_mem_nhds
added theorem pi_Ioc_mem_nhds'
added theorem pi_Ioc_mem_nhds
added theorem pi_Ioi_mem_nhds'
added theorem pi_Ioi_mem_nhds
added theorem pi_Ioo_mem_nhds'
added theorem pi_Ioo_mem_nhds
added theorem set_pi_mem_nhds
added theorem compact_pi_Icc