Commit 2024-01-30 14:58 ae98c3f2

View on Github →

feat: images of intervals under (↑) : ℕ → ℤ (#9927) Also generalize IsUpperSet.Ioi_subset and IsLowerSet.Iio_subset from a PartialOrder to a Preorder.

Estimated changes

added theorem Nat.image_cast_int_Icc
added theorem Nat.image_cast_int_Ici
added theorem Nat.image_cast_int_Ico
added theorem Nat.image_cast_int_Iic
added theorem Nat.image_cast_int_Iio
added theorem Nat.image_cast_int_Ioc
added theorem Nat.image_cast_int_Ioi
added theorem Nat.image_cast_int_Ioo
added theorem Nat.range_cast_int
added theorem IsLowerSet.Iio_subset
added theorem IsUpperSet.Ioi_subset