feat(set_theory/principal): Principal ordinals are unbounded (#11755)

Amazingly, this theorem requires no conditions on the operation.



Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

src/set_theory/ordinal_arithmetic.lean

@@ -2107,7 +2107,10 @@ le_sup _ n
 theorem le_nfp_self (f a) : a ≤ nfp f a :=
 iterate_le_nfp f a 0
 
-theorem is_normal.lt_nfp {f} (H : is_normal f) {a b} : f b < nfp f a ↔ b < nfp f a :=
+theorem lt_nfp {f : ordinal → ordinal} {a b} : a < nfp f b ↔ ∃ n, a < (f^[n]) b :=
+lt_sup
+
+protected theorem is_normal.lt_nfp {f} (H : is_normal f) {a b} : f b < nfp f a ↔ b < nfp f a :=
 lt_sup.trans $ iff.trans
   (by exact
    ⟨λ ⟨n, h⟩, ⟨n, lt_of_le_of_lt (H.le_self _) h⟩,

src/set_theory/principal.lean

@@ -19,6 +19,8 @@ We define principal or indecomposable ordinals, and we prove the standard proper
 
 universe u
 
+noncomputable theory
+
 namespace ordinal
 
 /-! ### Principal ordinals -/
@@ -67,4 +69,38 @@ theorem nfp_le_of_principal {op : ordinal → ordinal → ordinal}
   {a o : ordinal} (hao : a < o) (ho : principal op o) : nfp (op a) a ≤ o :=
 nfp_le.2 $ λ n, le_of_lt (ho.iterate_lt hao n)
 
+/-! ### Principal ordinals are unbounded -/
+
+/-- The least strict upper bound of `op` applied to all pairs of ordinals less than `o`. This is
+essentially a two-argument version of `ordinal.blsub`. -/
+def blsub₂ (op : ordinal → ordinal → ordinal) (o : ordinal) : ordinal :=
+lsub (λ x : o.out.α × o.out.α, op (typein o.out.r x.1) (typein o.out.r x.2))
+
+theorem lt_blsub₂ (op : ordinal → ordinal → ordinal) {o : ordinal} {a b : ordinal} (ha : a < o)
+  (hb : b < o) : op a b < blsub₂ op o :=
+begin
+  convert lt_lsub _ (prod.mk (enum o.out.r a (by rwa type_out)) (enum o.out.r b (by rwa type_out))),
+  simp only [typein_enum]
+end
+
+theorem principal_nfp_blsub₂ (op : ordinal → ordinal → ordinal) (o : ordinal) :
+  principal op (nfp (blsub₂.{u u} op) o) :=
+begin
+  intros a b ha hb,
+  rw lt_nfp at *,
+  cases ha with m hm,
+  cases hb with n hn,
+  cases le_total ((blsub₂.{u u} op)^[m] o) ((blsub₂.{u u} op)^[n] o) with h h,
+  { use n + 1,
+    rw function.iterate_succ',
+    exact lt_blsub₂ op (hm.trans_le h) hn },
+  { use m + 1,
+    rw function.iterate_succ',
+    exact lt_blsub₂ op hm (hn.trans_le h) },
+end
+
+theorem unbounded_principal (op : ordinal → ordinal → ordinal) :
+  set.unbounded (<) {o | principal op o} :=
+λ o, ⟨_, principal_nfp_blsub₂ op o, (le_nfp_self _ o).not_lt⟩
+
 end ordinal