feat: SuccOrder and recursion principle on well-ordered type (#11290)

Order/SuccPred/Basic.lean: add `SuccOrder.ofLinearWellFoundedLT`, which puts a SuccOrder on an arbitrary well-ordered type. Also add the dual, `PredOrder` version. Add missing `pred` lemmas corresponding to existing `succ` lemmas.

Order/SuccPred/Limit.lean: add `SuccOrder.limitRecOn` generalizing `Ordinal.limitRecOn` to allow definition by transfinite recursion on an arbitrary well-ordered type. (It turns out a **partial** well-founded order is enough.)

SetTheory/Ordinal/Arithmetic.lean: refactor `Ordinal.limitRecOn` to use `SuccOrder.limitRecOn`.

SetTheory/Cardinal/Ordinal.lean: add a lemma saying that the initial ordinal of an infinite cardinal is a NoMaxOrder.

SetTheory/Ordinal/Basic.lean: add `mk_Iio_ord_out_α`, a restatement of `card_typein_out_lt`.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/Order/SuccPred/Basic.lean

@@ -6,6 +6,7 @@ Authors: Yaël Dillies
 import Mathlib.Order.CompleteLattice
 import Mathlib.Order.Cover
 import Mathlib.Order.Iterate
+import Mathlib.Order.WellFounded
 
 #align_import order.succ_pred.basic from "leanprover-community/mathlib"@"0111834459f5d7400215223ea95ae38a1265a907"
 
@@ -193,6 +194,23 @@ def PredOrder.ofLePredIff (pred : α → α) (hle_pred_iff : ∀ {a b}, a ≤ pr
     le_of_pred_lt := fun {_ _} h => le_of_not_lt ((not_congr hle_pred_iff).1 h.not_le) }
 #align pred_order.of_le_pred_iff PredOrder.ofLePredIff
 
+open scoped Classical
+
+variable (α)
+
+/-- A well-order is a `SuccOrder`. -/
+noncomputable def SuccOrder.ofLinearWellFoundedLT [WellFoundedLT α] : SuccOrder α :=
+  ofCore (fun a ↦ if h : (Ioi a).Nonempty then wellFounded_lt.min _ h else a)
+    (fun ha _ ↦ by
+      rw [not_isMax_iff] at ha
+      simp_rw [Set.Nonempty, mem_Ioi, dif_pos ha]
+      exact ⟨(wellFounded_lt.min_le · ha), lt_of_lt_of_le (wellFounded_lt.min_mem _ ha)⟩)
+    fun a ha ↦ dif_neg (not_not_intro ha <| not_isMax_iff.mpr ·)
+
+/-- A linear order with well-founded greater-than relation is a `PredOrder`. -/
+noncomputable def PredOrder.ofLinearWellFoundedGT (α) [LinearOrder α] [WellFoundedGT α] :
+    PredOrder α := letI := SuccOrder.ofLinearWellFoundedLT αᵒᵈ; inferInstanceAs (PredOrder αᵒᵈᵒᵈ)
+
 end LinearOrder
 
 /-! ### Successor order -/
@@ -646,6 +664,14 @@ theorem le_pred_iff_of_not_isMin (ha : ¬IsMin a) : b ≤ pred a ↔ b < a :=
 lemma pred_lt_pred_of_not_isMin (h : a < b) (ha : ¬ IsMin a) : pred a < pred b :=
   (pred_lt_iff_of_not_isMin ha).2 <| le_pred_of_lt h
 
+theorem pred_lt_pred_iff_of_not_isMin (ha : ¬IsMin a) (hb : ¬IsMin b) :
+    pred a < pred b ↔ a < b := by
+  rw [pred_lt_iff_of_not_isMin ha, le_pred_iff_of_not_isMin hb]
+
+theorem pred_le_pred_iff_of_not_isMin (ha : ¬IsMin a) (hb : ¬IsMin b) :
+    pred a ≤ pred b ↔ a ≤ b := by
+  rw [le_pred_iff_of_not_isMin hb, pred_lt_iff_of_not_isMin ha]
+
 @[simp, mono]
 theorem pred_le_pred {a b : α} (h : a ≤ b) : pred a ≤ pred b :=
   succ_le_succ h.dual
@@ -777,6 +803,11 @@ theorem pred_eq_iff_isMin : pred a = a ↔ IsMin a :=
 alias ⟨_, _root_.IsMin.pred_eq⟩ := pred_eq_iff_isMin
 #align is_min.pred_eq IsMin.pred_eq
 
+theorem pred_eq_pred_iff_of_not_isMin (ha : ¬IsMin a) (hb : ¬IsMin b) :
+    pred a = pred b ↔ a = b := by
+  rw [eq_iff_le_not_lt, eq_iff_le_not_lt, pred_le_pred_iff_of_not_isMin ha hb,
+    pred_lt_pred_iff_of_not_isMin ha hb]
+
 theorem pred_le_le_iff {a b : α} : pred a ≤ b ∧ b ≤ a ↔ b = a ∨ b = pred a := by
   refine'
     ⟨fun h =>

Mathlib/Order/SuccPred/Limit.lean

@@ -185,6 +185,41 @@ theorem isSuccLimitRecOn_succ' (hs : ∀ a, ¬IsMax a → C (succ a)) (hl : ∀
     exact proof_irrel_heq H.left hb
 #align order.is_succ_limit_rec_on_succ' Order.isSuccLimitRecOn_succ'
 
+section limitRecOn
+
+variable [WellFoundedLT α]
+  (H_succ : ∀ a, ¬IsMax a → C a → C (succ a))
+  (H_lim : ∀ a, IsSuccLimit a → (∀ b < a, C b) → C a)
+
+open scoped Classical in
+variable (a) in
+/-- Recursion principle on a well-founded partial `SuccOrder`. -/
+@[elab_as_elim] noncomputable def _root_.SuccOrder.limitRecOn : C a :=
+  wellFounded_lt.fix
+    (fun a IH ↦ if h : IsSuccLimit a then H_lim a h IH else
+      let x := Classical.indefiniteDescription _ (not_isSuccLimit_iff.mp h)
+      x.2.2 ▸ H_succ x x.2.1 (IH x <| x.2.2.subst <| lt_succ_of_not_isMax x.2.1))
+    a
+
+@[simp]
+theorem _root_.SuccOrder.limitRecOn_succ (ha : ¬ IsMax a) :
+    SuccOrder.limitRecOn (succ a) H_succ H_lim
+      = H_succ a ha (SuccOrder.limitRecOn a H_succ H_lim) := by
+  have h := not_isSuccLimit_succ_of_not_isMax ha
+  rw [SuccOrder.limitRecOn, WellFounded.fix_eq, dif_neg h]
+  have {b c hb hc} {x : ∀ a, C a} (h : b = c) :
+    congr_arg succ h ▸ H_succ b hb (x b) = H_succ c hc (x c) := by subst h; rfl
+  let x := Classical.indefiniteDescription _ (not_isSuccLimit_iff.mp h)
+  exact this ((succ_eq_succ_iff_of_not_isMax x.2.1 ha).mp x.2.2)
+
+@[simp]
+theorem _root_.SuccOrder.limitRecOn_limit (ha : IsSuccLimit a) :
+    SuccOrder.limitRecOn a H_succ H_lim
+      = H_lim a ha fun x _ ↦ SuccOrder.limitRecOn x H_succ H_lim := by
+  rw [SuccOrder.limitRecOn, WellFounded.fix_eq, dif_pos ha]; rfl
+
+end limitRecOn
+
 section NoMaxOrder
 
 variable [NoMaxOrder α]
@@ -382,6 +417,41 @@ theorem isPredLimitRecOn_pred' (hs : ∀ a, ¬IsMin a → C (pred a)) (hl : ∀
   isSuccLimitRecOn_succ' _ _ _
 #align order.is_pred_limit_rec_on_pred' Order.isPredLimitRecOn_pred'
 
+section limitRecOn
+
+variable [WellFoundedGT α]
+  (H_pred : ∀ a, ¬IsMin a → C a → C (pred a))
+  (H_lim : ∀ a, IsPredLimit a → (∀ b > a, C b) → C a)
+
+open scoped Classical in
+variable (a) in
+/-- Recursion principle on a well-founded partial `PredOrder`. -/
+@[elab_as_elim] noncomputable def _root_.PredOrder.limitRecOn : C a :=
+  wellFounded_gt.fix
+    (fun a IH ↦ if h : IsPredLimit a then H_lim a h IH else
+      let x := Classical.indefiniteDescription _ (not_isPredLimit_iff.mp h)
+      x.2.2 ▸ H_pred x x.2.1 (IH x <| x.2.2.subst <| pred_lt_of_not_isMin x.2.1))
+    a
+
+@[simp]
+theorem _root_.PredOrder.limitRecOn_pred (ha : ¬ IsMin a) :
+    PredOrder.limitRecOn (pred a) H_pred H_lim
+      = H_pred a ha (PredOrder.limitRecOn a H_pred H_lim) := by
+  have h := not_isPredLimit_pred_of_not_isMin ha
+  rw [PredOrder.limitRecOn, WellFounded.fix_eq, dif_neg h]
+  have {b c hb hc} {x : ∀ a, C a} (h : b = c) :
+    congr_arg pred h ▸ H_pred b hb (x b) = H_pred c hc (x c) := by subst h; rfl
+  let x := Classical.indefiniteDescription _ (not_isPredLimit_iff.mp h)
+  exact this ((pred_eq_pred_iff_of_not_isMin x.2.1 ha).mp x.2.2)
+
+@[simp]
+theorem _root_.PredOrder.limitRecOn_limit (ha : IsPredLimit a) :
+    PredOrder.limitRecOn a H_pred H_lim
+      = H_lim a ha fun x _ ↦ PredOrder.limitRecOn x H_pred H_lim := by
+  rw [PredOrder.limitRecOn, WellFounded.fix_eq, dif_pos ha]; rfl
+
+end limitRecOn
+
 section NoMinOrder
 
 variable [NoMinOrder α]

Mathlib/SetTheory/Cardinal/Ordinal.lean

@@ -70,6 +70,8 @@ theorem ord_isLimit {c} (co : ℵ₀ ≤ c) : (ord c).IsLimit := by
       exact omega_isLimit
 #align cardinal.ord_is_limit Cardinal.ord_isLimit
 
+theorem noMaxOrder {c} (h : ℵ₀ ≤ c) : NoMaxOrder c.ord.out.α :=
+  Ordinal.out_no_max_of_succ_lt (ord_isLimit h).2
 
 /-! ### Aleph cardinals -/
 section aleph

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -240,10 +240,14 @@ def IsLimit (o : Ordinal) : Prop :=
   o ≠ 0 ∧ ∀ a < o, succ a < o
 #align ordinal.is_limit Ordinal.IsLimit
 
+theorem IsLimit.isSuccLimit {o} (h : IsLimit o) : IsSuccLimit o := isSuccLimit_iff_succ_lt.mpr h.2
+
 theorem IsLimit.succ_lt {o a : Ordinal} (h : IsLimit o) : a < o → succ a < o :=
   h.2 a
 #align ordinal.is_limit.succ_lt Ordinal.IsLimit.succ_lt
 
+theorem isSuccLimit_zero : IsSuccLimit (0 : Ordinal) := isSuccLimit_bot
+
 theorem not_zero_isLimit : ¬IsLimit 0
   | ⟨h, _⟩ => h rfl
 #align ordinal.not_zero_is_limit Ordinal.not_zero_isLimit
@@ -308,36 +312,25 @@ theorem zero_or_succ_or_limit (o : Ordinal) : o = 0 ∨ (∃ a, o = succ a) ∨
 @[elab_as_elim]
 def limitRecOn {C : Ordinal → Sort*} (o : Ordinal) (H₁ : C 0) (H₂ : ∀ o, C o → C (succ o))
     (H₃ : ∀ o, IsLimit o → (∀ o' < o, C o') → C o) : C o :=
-  lt_wf.fix
-    (fun o IH =>
-      if o0 : o = 0 then by rw [o0]; exact H₁
-      else
-        if h : ∃ a, o = succ a then by
-          rw [← succ_pred_iff_is_succ.2 h]; exact H₂ _ (IH _ <| pred_lt_iff_is_succ.2 h)
-        else H₃ _ ⟨o0, fun a => (succ_lt_of_not_succ h).2⟩ IH)
-    o
+  SuccOrder.limitRecOn o (fun o _ ↦ H₂ o) fun o hl ↦
+    if h : o = 0 then fun _ ↦ h ▸ H₁ else H₃ o ⟨h, fun _ ↦ hl.succ_lt⟩
 #align ordinal.limit_rec_on Ordinal.limitRecOn
 
 @[simp]
 theorem limitRecOn_zero {C} (H₁ H₂ H₃) : @limitRecOn C 0 H₁ H₂ H₃ = H₁ := by
-  rw [limitRecOn, lt_wf.fix_eq, dif_pos rfl]; rfl
+  rw [limitRecOn, SuccOrder.limitRecOn_limit _ _ isSuccLimit_zero, dif_pos rfl]
 #align ordinal.limit_rec_on_zero Ordinal.limitRecOn_zero
 
 @[simp]
 theorem limitRecOn_succ {C} (o H₁ H₂ H₃) :
     @limitRecOn C (succ o) H₁ H₂ H₃ = H₂ o (@limitRecOn C o H₁ H₂ H₃) := by
-  have h : ∃ a, succ o = succ a := ⟨_, rfl⟩
-  rw [limitRecOn, lt_wf.fix_eq, dif_neg (succ_ne_zero o), dif_pos h]
-  generalize limitRecOn.proof_2 (succ o) h = h₂
-  generalize limitRecOn.proof_3 (succ o) h = h₃
-  revert h₂ h₃; generalize e : pred (succ o) = o'; intros
-  rw [pred_succ] at e; subst o'; rfl
+  rw [limitRecOn, SuccOrder.limitRecOn_succ _ _ (not_isMax _)]; rfl
 #align ordinal.limit_rec_on_succ Ordinal.limitRecOn_succ
 
 @[simp]
 theorem limitRecOn_limit {C} (o H₁ H₂ H₃ h) :
     @limitRecOn C o H₁ H₂ H₃ = H₃ o h fun x _h => @limitRecOn C x H₁ H₂ H₃ := by
-  rw [limitRecOn, lt_wf.fix_eq, dif_neg h.1, dif_neg (not_succ_of_isLimit h)]; rfl
+  rw [limitRecOn, SuccOrder.limitRecOn_limit _ _ h.isSuccLimit, dif_neg h.1]; rfl
 #align ordinal.limit_rec_on_limit Ordinal.limitRecOn_limit
 
 instance orderTopOutSucc (o : Ordinal) : OrderTop (succ o).out.α :=

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -1451,6 +1451,8 @@ theorem card_typein_out_lt (c : Cardinal) (x : c.ord.out.α) :
   apply typein_lt_self
 #align cardinal.card_typein_out_lt Cardinal.card_typein_out_lt
 
+theorem mk_Iio_ord_out_α {c : Cardinal} (i : c.ord.out.α) : #(Iio i) < c := card_typein_out_lt c i
+
 theorem ord_injective : Injective ord := by
   intro c c' h
   rw [← card_ord c, ← card_ord c', h]