feat(set_theory/cardinal): lift_sup (#8675)

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

Author: kim-em

src/set_theory/cardinal.lean

@@ -605,6 +605,54 @@ begin
   exact quotient.sound ⟨equiv.sigma_equiv_prod ι α⟩,
 end
 
+protected lemma le_sup_iff {ι : Type v} {f : ι → cardinal.{max v w}} {c : cardinal} :
+  (c ≤ sup f) ↔ (∀ b, (∀ i, f i ≤ b) → c ≤ b) :=
+⟨λ h b hb, le_trans h (sup_le.mpr hb), λ h, h _ $ λ i, le_sup f i⟩
+
+/-- The lift of a supremum is the supremum of the lifts. -/
+lemma lift_sup {ι : Type v} (f : ι → cardinal.{max v w}) :
+  lift.{(max v w) u} (sup.{v w} f) =
+    sup.{v (max u w)} (λ i : ι, lift.{(max v w) u} (f i)) :=
+begin
+  apply le_antisymm,
+  { rw [cardinal.le_sup_iff], intros c hc, by_contra h,
+    obtain ⟨d, rfl⟩ := cardinal.lift_down (not_le.mp h).le,
+    simp only [lift_le, sup_le] at h hc,
+    exact h hc },
+  { simp only [cardinal.sup_le, lift_le, le_sup, implies_true_iff] }
+end
+
+/-- To prove that the lift of a supremum is bounded by some cardinal `t`,
+it suffices to show that the lift of each cardinal is bounded by `t`. -/
+lemma lift_sup_le {ι : Type v} (f : ι → cardinal.{max v w})
+  (t : cardinal.{max u v w}) (w : ∀ i, lift.{_ u} (f i) ≤ t) :
+  lift.{(max v w) u} (sup f) ≤ t :=
+by { rw lift_sup, exact sup_le.mpr w, }
+
+@[simp] lemma lift_sup_le_iff {ι : Type v} (f : ι → cardinal.{max v w}) (t : cardinal.{max u v w}) :
+  lift.{(max v w) u} (sup f) ≤ t ↔ ∀ i, lift.{_ u} (f i) ≤ t :=
+⟨λ h i, (lift_le.mpr (le_sup f i)).trans h,
+ λ h, lift_sup_le f t h⟩
+
+universes v' w'
+
+/--
+To prove an inequality between the lifts to a common universe of two different supremums,
+it suffices to show that the lift of each cardinal from the smaller supremum
+if bounded by the lift of some cardinal from the larger supremum.
+-/
+lemma lift_sup_le_lift_sup
+  {ι : Type v} {ι' : Type v'} (f : ι → cardinal.{max v w}) (f' : ι' → cardinal.{max v' w'})
+  (g : ι → ι') (h : ∀ i, lift.{_ (max v' w')} (f i) ≤ lift.{_ (max v w)} (f' (g i))) :
+  lift.{_ (max v' w')} (sup f) ≤ lift.{_ (max v w)} (sup f') :=
+begin
+  apply lift_sup_le.{(max v' w')} f,
+  intro i,
+  apply le_trans (h i),
+  simp only [lift_le],
+  apply le_sup,
+end
+
 /-- `ω` is the smallest infinite cardinal, also known as ℵ₀. -/
 def omega : cardinal.{u} := lift (mk ℕ)