From 68033a229019de90e4eb220ec767d16dc9171a17 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= <vi.hdz.p@gmail.com>
Date: Wed, 16 Mar 2022 08:21:51 +0000
Subject: [PATCH] feat(set_theory/ordinal_arithmetic): A set of ordinals is
 bounded above iff it's small (#11870)

---
 src/logic/small.lean                   |  4 ++++
 src/set_theory/ordinal_arithmetic.lean | 29 ++++++++++++++++++++++++++
 2 files changed, 33 insertions(+)

diff --git a/src/logic/small.lean b/src/logic/small.lean
index ebb835962ea57..3dc653d7687d7 100644
--- a/src/logic/small.lean
+++ b/src/logic/small.lean
@@ -78,6 +78,10 @@ theorem small_of_surjective {α : Type v} {β : Type w} [small.{u} α] {f : α 
   (hf : function.surjective f) : small.{u} β :=
 small_of_injective (function.injective_surj_inv hf)
 
+theorem small_subset {α : Type v} {s t : set α} (hts : t ⊆ s) [small.{u} s] : small.{u} t :=
+let f : t → s := λ x, ⟨x, hts x.prop⟩ in
+  @small_of_injective _ _ _ f (λ x y hxy, subtype.ext (subtype.mk.inj hxy))
+
 @[priority 100]
 instance small_subsingleton (α : Type v) [subsingleton α] : small.{w} α :=
 begin
diff --git a/src/set_theory/ordinal_arithmetic.lean b/src/set_theory/ordinal_arithmetic.lean
index c152c79958ab9..3bdd846c47b92 100644
--- a/src/set_theory/ordinal_arithmetic.lean
+++ b/src/set_theory/ordinal_arithmetic.lean
@@ -1096,6 +1096,35 @@ lemma unbounded_range_of_sup_ge {α β : Type u} (r : α → α → Prop) [is_we
   (sup_le.2 $ λ y, le_of_lt $ (typein_lt_typein r).2 $ hx _ $ mem_range_self y)
   (typein_lt_type r x)
 
+theorem le_sup_shrink_equiv {s : set ordinal.{u}} (hs : small.{u} s) (a) (ha : a ∈ s) :
+  a ≤ sup.{u u} (λ x, ((@equiv_shrink s hs).symm x).val) :=
+by { convert le_sup.{u u} _ ((@equiv_shrink s hs) ⟨a, ha⟩), rw symm_apply_apply }
+
+theorem small_Iio (o : ordinal.{u}) : small.{u} (set.Iio o) :=
+let f : o.out.α → set.Iio o := λ x, ⟨typein (<) x, typein_lt_self x⟩ in
+let hf : surjective f := λ b, ⟨enum (<) b.val (by { rw type_lt, exact b.prop }),
+  subtype.ext (typein_enum _ _)⟩ in
+small_of_surjective hf
+
+theorem bdd_above_iff_small {s : set ordinal.{u}} : bdd_above s ↔ small.{u} s :=
+⟨λ ⟨a, h⟩, @small_subset _ _ _ (by exact λ b hb, lt_succ.2 (h hb)) (small_Iio a.succ),
+λ h, ⟨sup.{u u} (λ x, ((@equiv_shrink s h).symm x).val), le_sup_shrink_equiv h⟩⟩
+
+theorem sup_eq_Sup {s : set ordinal.{u}} (hs : small.{u} s) :
+  sup.{u u} (λ x, (@equiv_shrink s hs).symm x) = Sup s :=
+let hs' := bdd_above_iff_small.2 hs in
+  ((cSup_le_iff' hs').2 (le_sup_shrink_equiv hs)).antisymm'
+  (sup_le.2 (λ x, le_cSup hs' (subtype.mem _)))
+
+private theorem sup_le_sup {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop)
+  [is_well_order ι r] [is_well_order ι' r'] {o} (ho : type r = o) (ho' : type r' = o)
+  (f : Π a < o, ordinal) : sup (family_of_bfamily' r ho f) ≤ sup (family_of_bfamily' r' ho' f) :=
+sup_le.2 $ λ i, begin
+  cases typein_surj r' (by { rw [ho', ←ho], exact typein_lt_type r i }) with j hj,
+  simp_rw [family_of_bfamily', ←hj],
+  apply le_sup
+end
+
 theorem sup_eq_sup {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [is_well_order ι r]
   [is_well_order ι' r'] {o : ordinal.{u}} (ho : type r = o) (ho' : type r' = o)
   (f : Π a < o, ordinal.{max u v}) :