chore(SetTheory/Ordinal/Basic): Ordinal.lt_iSup → Ordinal.lt_iSup_iff (leanprover-community#18903)

This matches `lt_ciSup_iff`.

Author: vihdzp

Mathlib/SetTheory/Cardinal/Arithmetic.lean

@@ -861,7 +861,7 @@ theorem lift_card_iSup_le_sum_card {ι : Type u} [Small.{v} ι] (f : ι → Ordi
     (mem_Iio.mp ((enumIsoToType _).symm _).2).trans_le (Ordinal.le_iSup _ _)⟩))
   rw [EquivLike.comp_surjective]
   rintro ⟨x, hx⟩
-  obtain ⟨i, hi⟩ := Ordinal.lt_iSup.mp hx
+  obtain ⟨i, hi⟩ := Ordinal.lt_iSup_iff.mp hx
   exact ⟨⟨i, enumIsoToType _ ⟨x, hi⟩⟩, by simp⟩
 
 theorem card_iSup_le_sum_card {ι : Type u} (f : ι → Ordinal.{max u v}) :

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -1248,10 +1248,12 @@ theorem sup_le {ι : Type u} {f : ι → Ordinal.{max u v}} {a} : (∀ i, f i 
   Ordinal.iSup_le
 
 /-- `lt_ciSup_iff'` whenever the input type is small in the output universe. -/
-protected theorem lt_iSup {ι} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u} ι] :
+protected theorem lt_iSup_iff {ι} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u} ι] :
     a < iSup f ↔ ∃ i, a < f i :=
   lt_ciSup_iff' (bddAbove_of_small _)
 
+@[deprecated (since := "2024-11-12")] alias lt_iSup := lt_iSup_iff
+
 set_option linter.deprecated false in
 @[deprecated Ordinal.lt_iSup (since := "2024-08-27")]
 theorem lt_sup {ι : Type u} {f : ι → Ordinal.{max u v}} {a} : a < sup.{_, v} f ↔ ∃ i, a < f i := by

Mathlib/SetTheory/Ordinal/FixedPoint.lean

@@ -65,7 +65,7 @@ theorem le_nfpFamily [Small.{u} ι] (f : ι → Ordinal.{u} → Ordinal.{u}) (a)
   foldr_le_nfpFamily f a []
 
 theorem lt_nfpFamily [Small.{u} ι] {a b} : a < nfpFamily f b ↔ ∃ l, a < List.foldr f b l :=
-  Ordinal.lt_iSup
+  Ordinal.lt_iSup_iff
 
 theorem nfpFamily_le_iff [Small.{u} ι] {a b} : nfpFamily f a ≤ b ↔ ∀ l, List.foldr f a l ≤ b :=
   Ordinal.iSup_le_iff
@@ -257,7 +257,7 @@ theorem le_nfpBFamily {o : Ordinal} (f : ∀ b < o, Ordinal → Ordinal) (a) :
 @[deprecated (since := "2024-10-14")]
 theorem lt_nfpBFamily {a b} :
     a < nfpBFamily.{u, v} o f b ↔ ∃ l, a < List.foldr (familyOfBFamily o f) b l :=
-  Ordinal.lt_iSup
+  Ordinal.lt_iSup_iff
 
 @[deprecated (since := "2024-10-14")]
 theorem nfpBFamily_le_iff {o : Ordinal} {f : ∀ b < o, Ordinal → Ordinal} {a b} :
@@ -448,7 +448,7 @@ theorem le_nfp (f a) : a ≤ nfp f a :=
 
 theorem lt_nfp {a b} : a < nfp f b ↔ ∃ n, a < f^[n] b := by
   rw [← iSup_iterate_eq_nfp]
-  exact Ordinal.lt_iSup
+  exact Ordinal.lt_iSup_iff
 
 theorem nfp_le_iff {a b} : nfp f a ≤ b ↔ ∀ n, f^[n] a ≤ b := by
   rw [← iSup_iterate_eq_nfp]

Mathlib/SetTheory/Ordinal/Rank.lean

@@ -45,7 +45,7 @@ theorem mem_range_rank_of_le {o : Ordinal} (ha : Acc r a) (ho : o ≤ ha.rank) :
   · exact ⟨a, ha, rfl⟩
   · revert ho
     refine ha.recOn fun a ha IH ho ↦ ?_
-    rw [rank_eq, Ordinal.lt_iSup] at ho
+    rw [rank_eq, Ordinal.lt_iSup_iff] at ho
     obtain ⟨⟨b, hb⟩, ho⟩ := ho
     rw [Order.lt_succ_iff] at ho
     obtain rfl | ho := ho.eq_or_lt

Mathlib/SetTheory/ZFC/Rank.lean

@@ -117,7 +117,7 @@ theorem rank_eq_wfRank : lift.{u + 1, u} (rank x) = IsWellFounded.rank (α := PS
   apply (le_of_forall_lt _).antisymm (Ordinal.iSup_le _) <;> intro h
   · rw [lt_lift_iff]
     rintro ⟨o, h, rfl⟩
-    simpa [Ordinal.lt_iSup] using lt_rank_iff.1 h
+    simpa [Ordinal.lt_iSup_iff] using lt_rank_iff.1 h
   · simpa using rank_lt_of_mem h.2
 
 end PSet
@@ -203,7 +203,7 @@ theorem rank_eq_wfRank : lift.{u + 1, u} (rank x) = IsWellFounded.rank (α := ZF
   apply (le_of_forall_lt _).antisymm (Ordinal.iSup_le _) <;> intro h
   · rw [lt_lift_iff]
     rintro ⟨o, h, rfl⟩
-    simpa [Ordinal.lt_iSup] using lt_rank_iff.1 h
+    simpa [Ordinal.lt_iSup_iff] using lt_rank_iff.1 h
   · simpa using rank_lt_of_mem h.2
 
 end ZFSet