Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-16 16:32 8985a433

View on Github →

feat(data/set/intervals): some interval lemmas (#942)

  • feat(data/set/intervals): a few more lemmas
  • one-liners

Estimated changes

added theorem set.Ioc_self
added theorem set.Ioc_subset_Ioc
added theorem set.left_mem_Icc
added theorem set.left_mem_Ico
added theorem set.left_mem_Ioc
added theorem set.left_mem_Ioo
added theorem set.right_mem_Icc
added theorem set.right_mem_Ico
added theorem set.right_mem_Ioc
added theorem set.right_mem_Ioo