refactor(set_theory/ordinal_arithmetic): Reworked sup and bsup API (

#11048)

This PR does two things:

- It reworks and matches, for the most part, the API for `ordinal.sup` and `ordinal.bsup`.
- It introduces `ordinal.lsub` and `ordinal.blsub` for (bounded) least strict upper bounds, and proves the expected results.

src/set_theory/ordinal.lean

@@ -585,10 +585,12 @@ begin
   cases quotient.out α, cases quotient.out β, exact classical.choice ∘ quotient.exact
 end
 
-theorem typein_lt_type (r : α → α → Prop) [is_well_order α r]
-  (a : α) : typein r a < type r :=
+theorem typein_lt_type (r : α → α → Prop) [is_well_order α r] (a : α) : typein r a < type r :=
 ⟨principal_seg.of_element _ _⟩
 
+theorem typein_lt_self {o : ordinal} (i : o.out.α) : typein o.out.r i < o :=
+by { simp_rw ←type_out o, apply typein_lt_type }
+
 @[simp] theorem typein_top {α β} {r : α → α → Prop} {s : β → β → Prop}
   [is_well_order α r] [is_well_order β s] (f : r ≺i s) :
   typein s f.top = type r :=
@@ -986,6 +988,8 @@ sum.inr punit.star, λ b, sum.rec_on b
   (λ x, ⟨λ _, ⟨x, rfl⟩, λ _, sum.lex.sep _ _⟩)
   (λ x, sum.lex_inr_inr.trans ⟨false.elim, λ ⟨x, H⟩, sum.inl_ne_inr H⟩)⟩⟩
 
+theorem succ_ne_self (o : ordinal.{u}) : succ o ≠ o := (lt_succ_self o).ne'
+
 theorem succ_le {a b : ordinal} : succ a ≤ b ↔ a < b :=
 ⟨lt_of_lt_of_le (lt_succ_self _),
 induction_on a $ λ α r hr, induction_on b $ λ β s hs ⟨⟨f, t, hf⟩⟩, begin

src/set_theory/ordinal_arithmetic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Floris van Doorn
 -/
 import set_theory.ordinal
+import tactic.by_contra
 
 /-!
 # Ordinal arithmetic
@@ -870,6 +871,16 @@ theorem sup_le {ι} {f : ι → ordinal} {a} : sup f ≤ a ↔ ∀ i, f i ≤ a
 theorem lt_sup {ι} {f : ι → ordinal} {a} : a < sup f ↔ ∃ i, a < f i :=
 by simpa only [not_forall, not_le] using not_congr (@sup_le _ f a)
 
+theorem lt_sup_of_ne_sup {ι} {f : ι → ordinal} : (∀ i, f i ≠ sup f) ↔ ∀ i, f i < sup f :=
+⟨λ hf _, lt_of_le_of_ne (le_sup _ _) (hf _), λ hf _, ne_of_lt (hf _)⟩
+
+theorem sup_not_succ_of_ne_sup {ι} {f : ι → ordinal} (hf : ∀ i, f i ≠ sup f) {a}
+  (hao : a < sup f) : succ a < sup f :=
+begin
+  by_contra' hoa,
+  exact hao.not_le (sup_le.2 (λ i, lt_succ.1 ((lt_of_le_of_ne (le_sup _ _) (hf i)).trans_le hoa)))
+end
+
 theorem is_normal.sup {f} (H : is_normal f)
   {ι} {g : ι → ordinal} (h : nonempty ι) : f (sup g) = sup (f ∘ g) :=
 eq_of_forall_ge_iff $ λ a,
@@ -879,9 +890,6 @@ by rw [sup_le, comp, H.le_set' (λ_:ι, true) g (let ⟨i⟩ := h in ⟨i, ⟨
 theorem sup_ord {ι} (f : ι → cardinal) : sup (λ i, (f i).ord) = (cardinal.sup f).ord :=
 eq_of_forall_ge_iff $ λ a, by simp only [sup_le, cardinal.ord_le, cardinal.sup_le]
 
-lemma sup_succ {ι} (f : ι → ordinal) : sup (λ i, succ (f i)) ≤ succ (sup f) :=
-by { rw [ordinal.sup_le], intro i, rw ordinal.succ_le_succ, apply ordinal.le_sup }
-
 lemma unbounded_range_of_sup_ge {α β : Type u} (r : α → α → Prop) [is_well_order α r] (f : β → α)
   (h : type r ≤ sup.{u u} (typein r ∘ f)) : unbounded r (range f) :=
 begin
@@ -908,38 +916,172 @@ match o, o.out, o.out_eq, f :
   ⟨λ H i h, by simpa only [typein_enum] using H (enum r i h), λ H b, H _ _⟩
 end
 
+theorem le_bsup {o} (f : Π a < o, ordinal) (i h) : f i h ≤ bsup o f :=
+bsup_le.1 (le_refl _) _ _
+
+theorem lt_bsup {o} (f : Π a < o, ordinal) {a} : a < bsup o f ↔ ∃ i hi, a < f i hi :=
+by simpa only [not_forall, not_le] using not_congr (@bsup_le _ f a)
+
 theorem bsup_type (r : α → α → Prop) [is_well_order α r] (f) :
   bsup (type r) f = sup (λ a, f (typein r a) (typein_lt_type _ _)) :=
 eq_of_forall_ge_iff $ λ o,
 by rw [bsup_le, sup_le]; exact
   ⟨λ H b, H _ _, λ H i h, by simpa only [typein_enum] using H (enum r i h)⟩
 
-theorem le_bsup {o} (f : Π a < o, ordinal) (i h) : f i h ≤ bsup o f :=
-bsup_le.1 (le_refl _) _ _
+theorem sup_eq_bsup {ι} (f : ι → ordinal) :
+  sup f = bsup (type well_ordering_rel) (λ a ha, f (enum well_ordering_rel a ha)) :=
+by simp [bsup_type]
 
-theorem lt_bsup {o : ordinal} {f : Π a < o, ordinal}
-  (hf : ∀{a a'} (ha : a < o) (ha' : a' < o), a < a' → f a ha < f a' ha')
-  (ho : o.is_limit) (i h) : f i h < bsup o f :=
-lt_of_lt_of_le (hf _ _ $ lt_succ_self i) (le_bsup f i.succ $ ho.2 _ h)
-
-theorem bsup_id {o} (ho : is_limit o) : bsup.{u u} o (λ x _, x) = o :=
+theorem bsup_eq_sup {o} (f : Π a < o, ordinal) : bsup o f = sup (λ i, f _ (typein_lt_self i)) :=
 begin
-  apply le_antisymm, rw [bsup_le], intro i, apply le_of_lt,
-  rw [←not_lt], intro h, apply lt_irrefl (bsup.{u u} o (λ x _, x)),
-  apply lt_of_le_of_lt _ (lt_bsup _ ho _ h), refl, intros, assumption
+  apply le_antisymm,
+  { rw bsup_le,
+    intros a hao,
+    rw ←type_out o at hao,
+    cases typein_surj _ hao with i hi,
+    simp_rw ←hi,
+    exact le_sup _ _ },
+  rw sup_le,
+  exact λ i, le_bsup _ _ _
 end
 
-theorem is_normal.bsup {f} (H : is_normal f)
-  {o : ordinal} : ∀ (g : Π a < o, ordinal) (h : o ≠ 0),
-  f (bsup o g) = bsup o (λ a h, f (g a h)) :=
+theorem is_normal.bsup {f} (H : is_normal f) {o} :
+  ∀ (g : Π a < o, ordinal) (h : o ≠ 0), f (bsup o g) = bsup o (λ a h, f (g a h)) :=
 induction_on o $ λ α r _ g h,
 by resetI; rw [bsup_type,
      H.sup (type_ne_zero_iff_nonempty.1 h), bsup_type]
 
+theorem lt_bsup_of_ne_bsup {o : ordinal} {f : Π a < o, ordinal} :
+  (∀ i h, f i h ≠ o.bsup f) ↔ ∀ i h, f i h < o.bsup f :=
+⟨λ hf _ _, lt_of_le_of_ne (le_bsup _ _ _) (hf _ _), λ hf _ _, ne_of_lt (hf _ _)⟩
+
+theorem bsup_not_succ_of_ne_bsup {o} {f : Π a < o, ordinal}
+  (hf : ∀ {i : ordinal} (h : i < o), f i h ≠ o.bsup f) (a) :
+  a < bsup o f → succ a < bsup o f :=
+by { rw bsup_eq_sup at *, exact sup_not_succ_of_ne_sup (λ i, hf _) }
+
+theorem lt_bsup_of_limit {o : ordinal} {f : Π a < o, ordinal}
+  (hf : ∀ {a a'} (ha : a < o) (ha' : a' < o), a < a' → f a ha < f a' ha')
+  (ho : o.is_limit) (i h) : f i h < bsup o f :=
+lt_of_lt_of_le (hf _ _ $ lt_succ_self i) (le_bsup f i.succ $ ho.2 _ h)
+
+theorem bsup_id {o} (ho : is_limit o) : bsup.{u u} o (λ x _, x) = o :=
+le_antisymm (bsup_le.2 (λ i hi, hi.le))
+  (not_lt.1 (λ h, (lt_bsup_of_limit.{u u} (λ _ _ _ _, id) ho _ h).false))
+
 theorem is_normal.bsup_eq {f} (H : is_normal f) {o : ordinal} (h : is_limit o) :
-  bsup.{u} o (λx _, f x) = f o :=
+  bsup.{u} o (λ x _, f x) = f o :=
 by { rw [←is_normal.bsup.{u u} H (λ x _, x) h.1, bsup_id h] }
 
+/-- The least strict upper bound of a family of ordinals. -/
+def lsub {ι} (f : ι → ordinal) : ordinal :=
+sup (λ i, (f i).succ)
+
+theorem lsub_le_iff_lt {ι} {f : ι → ordinal} {a} : lsub f ≤ a ↔ ∀ i, f i < a :=
+by { convert sup_le, simp [succ_le] }
+
+theorem lt_lsub {ι} (f : ι → ordinal) (i) : f i < lsub f :=
+succ_le.1 (le_sup _ i)
+
+theorem sup_le_lsub {ι} (f : ι → ordinal) : sup f ≤ lsub f :=
+sup_le.2 (λ i, le_of_lt (lt_lsub f i))
+
+theorem lsub_le_sup_succ {ι} (f : ι → ordinal) : lsub f ≤ succ (sup f) :=
+lsub_le_iff_lt.2 (λ i, lt_succ.2 (le_sup f i))
+
+theorem sup_succ_le_lsub {ι} (f : ι → ordinal) : (sup f).succ ≤ lsub f ↔ ∃ i, f i = sup f :=
+begin
+  refine ⟨λ h, _, _⟩,
+  { by_contra' hf,
+    exact ne_of_lt (succ_le.1 h) (le_antisymm (sup_le_lsub f)
+      (lsub_le_iff_lt.2 (lt_sup_of_ne_sup.1 hf))) },
+  rintro ⟨_, hf⟩,
+  rw [succ_le, ←hf],
+  exact lt_lsub _ _
+end
+
+theorem sup_succ_eq_lsub {ι} (f : ι → ordinal) : (sup f).succ = lsub f ↔ ∃ i, f i = sup f :=
+begin
+  rw iff.intro le_of_eq (λ h, le_antisymm h (lsub_le_sup_succ f)),
+  exact sup_succ_le_lsub f
+end
+
+theorem sup_eq_lsub {ι} (f : ι → ordinal) : sup f = lsub f ↔ ∀ a < lsub f, succ a < lsub f :=
+begin
+  refine ⟨λ h, _, λ hf, le_antisymm (sup_le_lsub f) _⟩,
+  { rw ←h,
+    exact λ a, sup_not_succ_of_ne_sup (λ i, ne_of_lt (lsub_le_iff_lt.1 (le_of_eq h.symm) i)) },
+  rw lsub_le_iff_lt,
+  intros i,
+  by_contra' hle,
+  have heq := (sup_succ_eq_lsub f).2 ⟨i, le_antisymm (le_sup _ _) hle⟩,
+  have := hf (sup f) ( by { rw ←heq, exact lt_succ_self _ } ),
+  rw heq at this,
+  exact lt_irrefl _ this
+end
+
+/-- The bounded least strict upper bound of a family of ordinals. -/
+def blsub (o : ordinal.{u}) (f : Π a < o, ordinal.{max u v}) : ordinal.{max u v} :=
+o.bsup (λ a ha, (f a ha).succ)
+
+theorem lsub_eq_blsub {ι} (f : ι → ordinal) :
+  lsub f = blsub (type well_ordering_rel) (λ a ha, f (enum well_ordering_rel a ha)) :=
+sup_eq_bsup _
+
+theorem blsub_eq_lsub {o} (f : Π a < o, ordinal) :
+  blsub o f = lsub (λ i, f _ (typein_lt_self i)) :=
+bsup_eq_sup _
+
+theorem blsub_le_iff_lt {o f a} : blsub o f ≤ a ↔ ∀ i h, f i h < a :=
+by { convert bsup_le, apply propext, simp [succ_le] }
+
+theorem lt_blsub {o} (f : Π a < o, ordinal) (i h) : f i h < blsub o f :=
+blsub_le_iff_lt.1 (le_refl _) _ _
+
+theorem bsup_le_blsub {o} (f : Π a < o, ordinal) : bsup o f ≤ blsub o f :=
+bsup_le.2 (λ i h, le_of_lt (lt_blsub f i h))
+
+theorem blsub_le_bsup_succ {o} (f : Π a < o, ordinal) : blsub o f ≤ (bsup o f).succ :=
+blsub_le_iff_lt.2 (λ i h, lt_succ.2 (le_bsup f i h))
+
+theorem bsup_succ_le_blsub {o} (f : Π a < o, ordinal) :
+  (bsup o f).succ ≤ blsub o f ↔ ∃ i hi, f i hi = bsup o f :=
+begin
+  refine ⟨λ h, _, _⟩,
+  { by_contra' hf,
+    exact ne_of_lt (succ_le.1 h) (le_antisymm (bsup_le_blsub f)
+      (blsub_le_iff_lt.2 (lt_bsup_of_ne_bsup.1 hf))) },
+  rintro ⟨_, _, hf⟩,
+  rw [succ_le, ←hf],
+  exact lt_blsub _ _ _
+end
+
+theorem bsup_succ_eq_blsub {o} (f : Π a < o, ordinal) :
+  (bsup o f).succ = blsub o f ↔ ∃ i hi, f i hi = bsup o f :=
+begin
+  rw iff.intro le_of_eq (λ h, le_antisymm h (blsub_le_bsup_succ f)),
+  exact bsup_succ_le_blsub f
+end
+
+theorem bsup_eq_blsub {o} (f : Π a < o, ordinal) :
+  bsup o f = blsub o f ↔ ∀ a < blsub o f, succ a < blsub o f :=
+by { rw [bsup_eq_sup, blsub_eq_lsub], exact sup_eq_lsub _ }
+
+theorem blsub_type (r : α → α → Prop) [is_well_order α r] (f) :
+  blsub (type r) f = lsub (λ a, f (typein r a) (typein_lt_type _ _)) :=
+eq_of_forall_ge_iff $ λ o,
+by rw [blsub_le_iff_lt, lsub_le_iff_lt]; exact
+  ⟨λ H b, H _ _, λ H i h, by simpa only [typein_enum] using H (enum r i h)⟩
+
+theorem blsub_id {o} : blsub.{u u} o (λ x _, x) = o :=
+begin
+  apply le_antisymm,
+  { rw blsub_le_iff_lt,
+    exact λ _, id },
+  by_contra' h,
+  exact lt_irrefl _ (lt_blsub.{u u} (λ x _, x) _ h)
+end
+
 /-! ### Ordinal exponential -/
 
 /-- The ordinal exponential, defined by transfinite recursion. -/