BadInfinities

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