From 59d9058103ff37f4ec4ae3a8fb9af2d89c9c517a Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Tue, 8 Apr 2025 22:31:48 -0400
Subject: [PATCH] BadInfinities

---
 SimpleCounterexamples/BadInfinities.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 SimpleCounterexamples/BadInfinities.lean

diff --git a/SimpleCounterexamples/BadInfinities.lean b/SimpleCounterexamples/BadInfinities.lean
new file mode 100644
index 0000000..59fe492
--- /dev/null
+++ b/SimpleCounterexamples/BadInfinities.lean
@@ -0,0 +1,17 @@
+abbrev HasInfinity (α : Type) [LT α] := ∃(inf : α), ∀n, n < inf
+
+theorem lt_irrefl_imp_no_infinity
+    (α : Type) [LT α] (irrefl : ∀(n : α), ¬n < n) : ¬HasInfinity α := by
+  intro h
+  have ⟨inf, h⟩ := h
+  have hlt : inf < inf := h inf
+  exact irrefl inf hlt
+
+
+theorem no_nat_infinity : ¬HasInfinity Nat :=
+  lt_irrefl_imp_no_infinity Nat Nat.lt_irrefl
+
+theorem no_int_infinity : ¬HasInfinity Nat :=
+  lt_irrefl_imp_no_infinity Nat Nat.lt_irrefl
+
+-- it's… not difficult to see the pattern