comments and imports

leanprover-community · Oct 13, 2024 · 5cad993 · 5cad993
1 parent 5c9cb52
commit 5cad993
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 1 deletion.
diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
@@ -1181,6 +1181,7 @@ set_option linter.deprecated false in
 theorem sup_le_iff {ι : Type u} {f : ι → Ordinal.{max u v}} {a} : sup.{_, v} f ≤ a ↔ ∀ i, f i ≤ a :=
   Ordinal.iSup_le_iff
 
+/-- `ciSup_le'` whenever the input type is small in the output universe. -/
 protected theorem iSup_le {ι} {f : ι → Ordinal.{u}} {a} :
     (∀ i, f i ≤ a) → iSup f ≤ a :=
   ciSup_le'

diff --git a/Mathlib/SetTheory/Ordinal/FixedPoint.lean b/Mathlib/SetTheory/Ordinal/FixedPoint.lean
@@ -5,7 +5,6 @@ Authors: Violeta Hernández Palacios, Mario Carneiro
 -/
 import Mathlib.SetTheory.Ordinal.Enum
 import Mathlib.SetTheory.Ordinal.Exponential
-import Mathlib.Logic.UnivLE
 
 /-!
 # Fixed points of normal functions