From ad2070232732195e0fcbfb18d91c729d775ad2fe Mon Sep 17 00:00:00 2001 From: mehbark Date: Tue, 8 Apr 2025 23:05:57 -0400 Subject: [PATCH] BadInfinities: chore redundant newline --- SimpleCounterexamples/BadInfinities.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/SimpleCounterexamples/BadInfinities.lean b/SimpleCounterexamples/BadInfinities.lean index daf035a..23e27ac 100644 --- a/SimpleCounterexamples/BadInfinities.lean +++ b/SimpleCounterexamples/BadInfinities.lean @@ -7,7 +7,6 @@ theorem lt_irrefl_imp_no_infinity 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