feat: images of intervals under (↑) : ℕ → ℤ (#9927)

Also generalize `IsUpperSet.Ioi_subset` and `IsLowerSet.Iio_subset`
from a `PartialOrder` to a `Preorder`.

Mathlib.lean

@@ -1778,6 +1778,7 @@ import Mathlib.Data.Nat.Cast.Field
 import Mathlib.Data.Nat.Cast.NeZero
 import Mathlib.Data.Nat.Cast.Order
 import Mathlib.Data.Nat.Cast.Prod
+import Mathlib.Data.Nat.Cast.SetInterval
 import Mathlib.Data.Nat.Cast.Synonym
 import Mathlib.Data.Nat.Cast.WithTop
 import Mathlib.Data.Nat.Choose.Basic

Mathlib/Data/Nat/Cast/SetInterval.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2024 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Data.Nat.Cast.Order
+import Mathlib.Data.Int.Order.Basic
+import Mathlib.Order.UpperLower.Basic
+
+/-!
+# 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 `ℤ`.
+-/
+
+open Set
+
+namespace Nat
+
+@[simp]
+theorem range_cast_int : range ((↑) : ℕ → ℤ) = Ici 0 :=
+  Subset.antisymm (range_subset_iff.2 Int.ofNat_nonneg) CanLift.prf
+
+theorem image_cast_int_Icc (a b : ℕ) : (↑) '' Icc a b = Icc (a : ℤ) b :=
+  (castOrderEmbedding (α := ℤ)).image_Icc (by simp [ordConnected_Ici]) a b
+
+theorem image_cast_int_Ico (a b : ℕ) : (↑) '' Ico a b = Ico (a : ℤ) b :=
+  (castOrderEmbedding (α := ℤ)).image_Ico (by simp [ordConnected_Ici]) a b
+
+theorem image_cast_int_Ioc (a b : ℕ) : (↑) '' Ioc a b = Ioc (a : ℤ) b :=
+  (castOrderEmbedding (α := ℤ)).image_Ioc (by simp [ordConnected_Ici]) a b
+
+theorem image_cast_int_Ioo (a b : ℕ) : (↑) '' Ioo a b = Ioo (a : ℤ) b :=
+  (castOrderEmbedding (α := ℤ)).image_Ioo (by simp [ordConnected_Ici]) a b
+
+theorem image_cast_int_Iic (a : ℕ) : (↑) '' Iic a = Icc (0 : ℤ) a := by
+  rw [← Icc_bot, image_cast_int_Icc]; rfl
+
+theorem image_cast_int_Iio (a : ℕ) : (↑) '' Iio a = Ico (0 : ℤ) a := by
+  rw [← Ico_bot, image_cast_int_Ico]; rfl
+
+theorem image_cast_int_Ici (a : ℕ) : (↑) '' Ici a = Ici (a : ℤ) :=
+  (castOrderEmbedding (α := ℤ)).image_Ici (by simp [isUpperSet_Ici]) a
+
+theorem image_cast_int_Ioi (a : ℕ) : (↑) '' Ioi a = Ioi (a : ℤ) :=
+  (castOrderEmbedding (α := ℤ)).image_Ioi (by simp [isUpperSet_Ici]) a
+
+end Nat

Mathlib/Order/UpperLower/Basic.lean

@@ -258,6 +258,14 @@ alias ⟨IsUpperSet.Ici_subset, _⟩ := isUpperSet_iff_Ici_subset
 alias ⟨IsLowerSet.Iic_subset, _⟩ := isLowerSet_iff_Iic_subset
 #align is_lower_set.Iic_subset IsLowerSet.Iic_subset
 
+theorem IsUpperSet.Ioi_subset (h : IsUpperSet s) ⦃a⦄ (ha : a ∈ s) : Ioi a ⊆ s :=
+  Ioi_subset_Ici_self.trans <| h.Ici_subset ha
+#align is_upper_set.Ioi_subset IsUpperSet.Ioi_subset
+
+theorem IsLowerSet.Iio_subset (h : IsLowerSet s) ⦃a⦄ (ha : a ∈ s) : Iio a ⊆ s :=
+  h.toDual.Ioi_subset ha
+#align is_lower_set.Iio_subset IsLowerSet.Iio_subset
+
 theorem IsUpperSet.ordConnected (h : IsUpperSet s) : s.OrdConnected :=
   ⟨fun _ ha _ _ => Icc_subset_Ici_self.trans <| h.Ici_subset ha⟩
 #align is_upper_set.ord_connected IsUpperSet.ordConnected
@@ -286,6 +294,24 @@ theorem IsLowerSet.image (hs : IsLowerSet s) (f : α ≃o β) : IsLowerSet (f ''
   exact hs.preimage f.symm.monotone
 #align is_lower_set.image IsLowerSet.image
 
+theorem OrderEmbedding.image_Ici (e : α ↪o β) (he : IsUpperSet (range e)) (a : α) :
+    e '' Ici a = Ici (e a) := by
+  rw [← e.preimage_Ici, image_preimage_eq_inter_range,
+    inter_eq_left.2 <| he.Ici_subset (mem_range_self _)]
+
+theorem OrderEmbedding.image_Iic (e : α ↪o β) (he : IsLowerSet (range e)) (a : α) :
+    e '' Iic a = Iic (e a) :=
+  e.dual.image_Ici he a
+
+theorem OrderEmbedding.image_Ioi (e : α ↪o β) (he : IsUpperSet (range e)) (a : α) :
+    e '' Ioi a = Ioi (e a) := by
+  rw [← e.preimage_Ioi, image_preimage_eq_inter_range,
+    inter_eq_left.2 <| he.Ioi_subset (mem_range_self _)]
+
+theorem OrderEmbedding.image_Iio (e : α ↪o β) (he : IsLowerSet (range e)) (a : α) :
+    e '' Iio a = Iio (e a) :=
+  e.dual.image_Ioi he a
+
 @[simp]
 theorem Set.monotone_mem : Monotone (· ∈ s) ↔ IsUpperSet s :=
   Iff.rfl
@@ -410,12 +436,6 @@ theorem isLowerSet_iff_Iio_subset : IsLowerSet s ↔ ∀ ⦃a⦄, a ∈ s → Ii
   simp [isLowerSet_iff_forall_lt, subset_def, @forall_swap (_ ∈ s)]
 #align is_lower_set_iff_Iio_subset isLowerSet_iff_Iio_subset
 
-alias ⟨IsUpperSet.Ioi_subset, _⟩ := isUpperSet_iff_Ioi_subset
-#align is_upper_set.Ioi_subset IsUpperSet.Ioi_subset
-
-alias ⟨IsLowerSet.Iio_subset, _⟩ := isLowerSet_iff_Iio_subset
-#align is_lower_set.Iio_subset IsLowerSet.Iio_subset
-
 end PartialOrder
 
 section LinearOrder