Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-15 22:29 699da421

View on Github →

feat(data/set/intervals): add nonempty_Icc etc, image_(add/mul)_(left/right)_Icc (#1803)

Estimated changes

deleted theorem ivl_stretch
deleted theorem ivl_translate
added theorem set.image_add_left_Icc
added theorem set.image_mul_left_Icc
added theorem set.nonempty_Icc
added theorem set.nonempty_Ici
added theorem set.nonempty_Ico
added theorem set.nonempty_Iic
added theorem set.nonempty_Ioc