Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-19 02:27 5d5da7e6

View on Github →

feat(data/set/intervals): more lemmas (#1665)

  • feat(data/set/intervals): more lemmas
  • Use simp in more proofs, drop two @[simp] attrs
  • Drop more @[simp] attrs It's not clear which side is simpler.

Estimated changes

added theorem set.Icc_inter_Icc
added theorem set.Ici_inter_Ici
added theorem set.Ici_inter_Iic
added theorem set.Ici_inter_Iio
added theorem set.Ico_inter_Ico
added theorem set.Iic_inter_Iic
added theorem set.Iio_inter_Iio
added theorem set.Ioc_inter_Ioc
added theorem set.Ioi_inter_Iic
added theorem set.Ioi_inter_Iio
added theorem set.Ioi_inter_Ioi
modified theorem set.Ioo_inter_Ioo
modified theorem set.left_mem_Icc
added theorem set.left_mem_Ici
modified theorem set.left_mem_Ico
modified theorem set.left_mem_Ioc
modified theorem set.left_mem_Ioo
modified theorem set.right_mem_Icc
modified theorem set.right_mem_Ico
added theorem set.right_mem_Iic
modified theorem set.right_mem_Ioc
modified theorem set.right_mem_Ioo