instance

leanprover-community · Oct 30, 2024 · e9f9114 · e9f9114
1 parent 305a53d
commit e9f9114
Showing 1 changed file with 4 additions and 6 deletions.
diff --git a/Mathlib/Order/Interval/Set/Infinite.lean b/Mathlib/Order/Interval/Set/Infinite.lean
@@ -16,15 +16,13 @@ preorder is an infinite type.
 
 variable {α : Type*} [Preorder α]
 
-/-- A nonempty preorder with no maximal element is infinite. This is not an instance to avoid
-a cycle with `Infinite α → Nontrivial α → Nonempty α`. -/
-theorem NoMaxOrder.infinite [Nonempty α] [NoMaxOrder α] : Infinite α :=
+/-- A nonempty preorder with no maximal element is infinite. -/
+instance NoMaxOrder.infinite [Nonempty α] [NoMaxOrder α] : Infinite α :=
   let ⟨f, hf⟩ := Nat.exists_strictMono α
   Infinite.of_injective f hf.injective
 
-/-- A nonempty preorder with no minimal element is infinite. This is not an instance to avoid
-a cycle with `Infinite α → Nontrivial α → Nonempty α`. -/
-theorem NoMinOrder.infinite [Nonempty α] [NoMinOrder α] : Infinite α :=
+/-- A nonempty preorder with no minimal element is infinite. -/
+instance NoMinOrder.infinite [Nonempty α] [NoMinOrder α] : Infinite α :=
   @NoMaxOrder.infinite αᵒᵈ _ _ _
 
 namespace Set