feat(set_theory/ordinal_arithmetic): Normal functions evaluated at ω (

#11687)

src/set_theory/ordinal.lean

@@ -1151,6 +1151,9 @@ wf.conditionally_complete_linear_order_with_bot 0 $ le_antisymm (ordinal.zero_le
 protected theorem not_lt_zero (o : ordinal) : ¬ o < 0 :=
 not_lt_bot
 
+theorem eq_zero_or_pos : ∀ a : ordinal, a = 0 ∨ 0 < a :=
+eq_bot_or_bot_lt
+
 lemma Inf_eq_omin {s : set ordinal} (hs : s.nonempty) :
   Inf s = omin s hs :=
 begin

src/set_theory/ordinal_arithmetic.lean

@@ -1890,6 +1890,9 @@ theorem omega_le {o : ordinal.{u}} : omega ≤ o ↔ ∀ n : ℕ, (n : ordinal)
    let ⟨n, e⟩ := lt_omega.1 h in
    by rw [e, ← succ_le]; exact H (n+1)⟩
 
+theorem sup_nat_cast : sup nat.cast = omega :=
+(sup_le.2 $ λ n, (nat_lt_omega n).le).antisymm $ omega_le.2 $ le_sup _
+
 theorem nat_lt_limit {o} (h : is_limit o) : ∀ n : ℕ, (n : ordinal) < o
 | 0     := lt_of_le_of_ne (ordinal.zero_le o) h.1.symm
 | (n+1) := h.2 _ (nat_lt_limit n)
@@ -2056,6 +2059,31 @@ le_antisymm
     (λ b hb, le_of_lt (opow_lt_omega h hb)))
   (le_opow_self _ a1)
 
+theorem is_normal.apply_omega {f : ordinal.{u} → ordinal.{u}} (hf : is_normal f) :
+  sup.{0 u} (f ∘ nat.cast) = f omega :=
+by rw [←sup_nat_cast, is_normal.sup.{0 u u} hf ⟨0⟩]
+
+theorem sup_add_nat (o : ordinal.{u}) : sup (λ n : ℕ, o + n) = o + omega :=
+(add_is_normal o).apply_omega
+
+theorem sup_mul_nat (o : ordinal) : sup (λ n : ℕ, o * n) = o * omega :=
+begin
+  rcases eq_zero_or_pos o with rfl | ho,
+  { rw zero_mul, exact sup_eq_zero_iff.2 (λ n, zero_mul n) },
+  { exact (mul_is_normal ho).apply_omega }
+end
+
+theorem sup_opow_nat {o : ordinal.{u}} (ho : 0 < o) :
+  sup (λ n : ℕ, o ^ n) = o ^ omega :=
+begin
+  rcases lt_or_eq_of_le (one_le_iff_pos.2 ho) with ho₁ | rfl,
+  { exact (opow_is_normal ho₁).apply_omega },
+  { rw one_opow,
+    refine le_antisymm (sup_le.2 (λ n, by rw one_opow)) _,
+    convert le_sup _ 0,
+    rw [nat.cast_zero, opow_zero] }
+end
+
 /-! ### Fixed points of normal functions -/
 
 /-- The next fixed point function, the least fixed point of the normal function `f` above `a`. -/