Images of intervals under Nat.cast : ℕ → ℤ

In this file we prove that the image of each Set.Ixx interval under Nat.cast : ℕ → ℤ is the corresponding interval in ℤ.

@[simp]

theorem Nat.range_cast_int : Set.range Nat.cast = Set.Ici 0

theorem Nat.image_cast_int_Icc (a : ℕ) (b : ℕ) : Nat.cast '' Set.Icc a b = Set.Icc ↑a ↑b

theorem Nat.image_cast_int_Ico (a : ℕ) (b : ℕ) : Nat.cast '' Set.Ico a b = Set.Ico ↑a ↑b

theorem Nat.image_cast_int_Ioc (a : ℕ) (b : ℕ) : Nat.cast '' Set.Ioc a b = Set.Ioc ↑a ↑b

theorem Nat.image_cast_int_Ioo (a : ℕ) (b : ℕ) : Nat.cast '' Set.Ioo a b = Set.Ioo ↑a ↑b

theorem Nat.image_cast_int_Iic (a : ℕ) : Nat.cast '' Set.Iic a = Set.Icc 0 ↑a

theorem Nat.image_cast_int_Iio (a : ℕ) : Nat.cast '' Set.Iio a = Set.Ico 0 ↑a

theorem Nat.image_cast_int_Ici (a : ℕ) : Nat.cast '' Set.Ici a = Set.Ici ↑a

theorem Nat.image_cast_int_Ioi (a : ℕ) : Nat.cast '' Set.Ioi a = Set.Ioi ↑a