From 4f26b501bfe6f119703f454348bfde836a3596a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= <vi.hdz.p@gmail.com>
Date: Sun, 5 Jan 2025 22:58:53 -0600
Subject: [PATCH] normal functions!

---
 Mathlib/Order/Normal.lean | 68 +++++++++++++++++++++++----------------
 1 file changed, 40 insertions(+), 28 deletions(-)

diff --git a/Mathlib/Order/Normal.lean b/Mathlib/Order/Normal.lean
index aae350bcd81ac..c72240e42d5e7 100644
--- a/Mathlib/Order/Normal.lean
+++ b/Mathlib/Order/Normal.lean
@@ -22,10 +22,10 @@ TODO: replace `Ordinal.IsNormal` by this more general notion.
 
 open Order Set
 
-variable {α β γ : Type*} {a b : α} [LinearOrder α] [LinearOrder β] [LinearOrder γ]
+variable {α β γ : Type*} {a b : α} {f : α → β} {g : β → γ}
 
 /-- A normal function between well-orders is a strictly monotonic continuous function. -/
-structure IsNormal (f : α → β) : Prop where
+structure IsNormal [LinearOrder α] [LinearOrder β] (f : α → β) : Prop where
   strictMono : StrictMono f
   /-- Combined with strict monotonicity, this condition implies that `f a` is the *least* upper
   bound for `f '' Iio a`. -/
@@ -33,7 +33,9 @@ structure IsNormal (f : α → β) : Prop where
     f a ∈ lowerBounds (upperBounds (f '' Iio a))
 
 namespace IsNormal
-variable {f : α → β} {g : β → γ}
+
+section LinearOrder
+variable [LinearOrder α] [LinearOrder β] [LinearOrder γ]
 
 theorem of_succ_lt [SuccOrder α] [WellFoundedLT α]
     (hs : ∀ a, f a < f (succ a)) (hl : ∀ {a}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)) :
@@ -65,7 +67,7 @@ theorem id_le {f : α → α} (hf : IsNormal f) [WellFoundedLT α] : id ≤ f :=
 theorem le_apply {f : α → α} (hf : IsNormal f) [WellFoundedLT α] : a ≤ f a :=
   hf.strictMono.le_apply
 
-theorem isLUB_of_isSuccLimit (hf : IsNormal f) {a : α} (ha : IsSuccLimit a) :
+theorem isLUB_image_Iio_of_isSuccLimit (hf : IsNormal f) {a : α} (ha : IsSuccLimit a) :
     IsLUB (f '' Iio a) (f a) := by
   refine ⟨?_, mem_lowerBounds_upperBounds hf ha⟩
   rintro _ ⟨b, hb, rfl⟩
@@ -73,34 +75,12 @@ theorem isLUB_of_isSuccLimit (hf : IsNormal f) {a : α} (ha : IsSuccLimit a) :
 
 theorem le_iff_forall_le (hf : IsNormal f) (ha : IsSuccLimit a) {b : β} :
     f a ≤ b ↔ ∀ a' < a, f a' ≤ b := by
-  simpa [mem_upperBounds] using isLUB_le_iff (hf.isLUB_of_isSuccLimit ha)
+  simpa [mem_upperBounds] using isLUB_le_iff (hf.isLUB_image_Iio_of_isSuccLimit ha)
 
 theorem lt_iff_exists_lt (hf : IsNormal f) (ha : IsSuccLimit a) {b : β} :
     b < f a ↔ ∃ a' < a, b < f a' := by
-  simpa [mem_upperBounds] using lt_isLUB_iff (hf.isLUB_of_isSuccLimit ha)
+  simpa [mem_upperBounds] using lt_isLUB_iff (hf.isLUB_image_Iio_of_isSuccLimit ha)
 
-theorem map_isLUB (hf : IsNormal f) {s : Set α} (hs : s.Nonempty) (hs' : IsLUB s a) :
-    IsLUB (f '' s) (f a) := by
-  constructor
-  · simp_rw [mem_upperBounds, forall_mem_image, hf.le_iff_le]
-    exact hs'.1
-  · intro b hb
-    by_cases ha : a ∈ s
-    · simp_rw [mem_upperBounds, forall_mem_image] at hb
-      exact hb ha
-    · have ha' : ¬ IsMin a := by
-        obtain ⟨c, hc⟩ := hs
-        obtain rfl | hc := (hs'.1 hc).eq_or_lt
-        · contradiction
-        · exact hc.not_isMin
-      have ha' := (IsLUB.isSuccPrelimit_of_not_mem hs' ha).isSuccLimit_of_not_isMin ha'
-      rw [le_iff_forall_le hf ha']
-      simp [mem_upperBounds] at hb
-      intro c hc
-      obtain ⟨d, hd, hcd, hda⟩ := hs'.exists_between hc
-      exact (hf.strictMono hcd).le.trans (hb d hd)
-
-#exit
 theorem map_isSuccLimit (hf : IsNormal f) (ha : IsSuccLimit a) : IsSuccLimit (f a) := by
   refine ⟨?_, fun b hb ↦ ?_⟩
   · obtain ⟨b, hb⟩ := not_isMin_iff.1 ha.not_isMin
@@ -110,6 +90,21 @@ theorem map_isSuccLimit (hf : IsNormal f) (ha : IsSuccLimit a) : IsSuccLimit (f
     rw [hf.le_iff_le] at hc'
     exact hc.not_le hc'
 
+theorem map_isLUB (hf : IsNormal f) {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) :
+    IsLUB (f '' s) (f a) := by
+  refine ⟨?_, fun b hb ↦ ?_⟩
+  · simp_rw [mem_upperBounds, forall_mem_image, hf.le_iff_le]
+    exact hs.1
+  · by_cases ha : a ∈ s
+    · simp_rw [mem_upperBounds, forall_mem_image] at hb
+      exact hb ha
+    · have ha' := hs.isSuccLimit_of_not_mem hs' ha
+      rw [le_iff_forall_le hf ha']
+      intro c hc
+      obtain ⟨d, hd, hcd, hda⟩ := hs.exists_between hc
+      simp_rw [mem_upperBounds, forall_mem_image] at hb
+      exact (hf.strictMono hcd).le.trans (hb hd)
+
 theorem _root_.InitialSeg.isNormal (f : α ≤i β) : IsNormal f where
   strictMono := f.strictMono
   mem_lowerBounds_upperBounds := by
@@ -131,5 +126,22 @@ theorem trans (hg : IsNormal g) (hf : IsNormal f) : IsNormal (g ∘ f) where
     simpa [hg.le_iff_forall_le (hf.map_isSuccLimit ha), hf.lt_iff_exists_lt ha] using
       fun c d hd hc ↦ (hg.strictMono hc).le.trans (hb hd)
 
+end LinearOrder
+
+section ConditionallyCompleteLinearOrder
+
+variable [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLinearOrder β]
+
+theorem map_sSup (hf : IsNormal f) {s : Set α} (hs : s.Nonempty) (hs' : BddAbove s) :
+    f (sSup s) = sSup (f '' s) :=
+  ((hf.map_isLUB (isLUB_csSup hs hs') hs).csSup_eq (hs.image f)).symm
+
+theorem map_iSup {ι} [Nonempty ι] {g : ι → α} (hf : IsNormal f) (hg : BddAbove (range g)) :
+    f (⨆ i, g i) = ⨆ i, f (g i) := by
+  unfold iSup
+  convert map_sSup hf (range_nonempty g) hg
+  ext; simp
+
+end ConditionallyCompleteLinearOrder
 
 end IsNormal