Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-04 13:46 c43b3329

View on Github →

feat(data/set/intervals): more properties of intervals (#1753)

  • feat(data/set/intervals): more properties of intervals
  • fix docstrings
  • blank space
  • iff versions
  • fix docstring
  • more details in docstrings

Estimated changes

modified theorem set.Ico_subset_Iio_self
added theorem set.Iio_subset_Iic
added theorem set.Iio_subset_Iic_iff
added theorem set.Iio_subset_Iio
added theorem set.Iio_subset_Iio_iff
added theorem set.Ioi_subset_Ici
added theorem set.Ioi_subset_Ici_iff
added theorem set.Ioi_subset_Ioi
added theorem set.Ioi_subset_Ioi_iff
added theorem set.is_glb_Icc
added theorem set.is_glb_Ici
added theorem set.is_glb_Ico
added theorem set.is_glb_Ioc
added theorem set.is_glb_Ioi
added theorem set.is_glb_Ioo
added theorem set.is_lub_Icc
added theorem set.is_lub_Ico
added theorem set.is_lub_Iic
added theorem set.is_lub_Iio
added theorem set.is_lub_Ioc
added theorem set.is_lub_Ioo
added theorem closure_Ico
added theorem closure_Iio'
added theorem closure_Iio
added theorem closure_Ioc
added theorem closure_Ioi'
added theorem closure_Ioi
added theorem closure_Ioo
added theorem is_closed_Ici
added theorem is_closed_Iic
modified theorem mem_nhds_within