From e9f9114307491a5191ae6f110743bd68a74589a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= Date: Wed, 30 Oct 2024 12:33:31 -0600 Subject: [PATCH] instance --- Mathlib/Order/Interval/Set/Infinite.lean | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/Mathlib/Order/Interval/Set/Infinite.lean b/Mathlib/Order/Interval/Set/Infinite.lean index 4390b048091c8..9ab4354e14add 100644 --- 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