src/HOL/Set_Interval.thy

--- a/src/HOL/Set_Interval.thy	Fri Feb 18 18:58:49 2022 +0100
+++ b/src/HOL/Set_Interval.thy	Fri Feb 18 21:40:01 2022 +0000
@@ -1728,6 +1728,9 @@
   "bij_betw of_nat N A \<longleftrightarrow> of_nat ` N = A"
   by (simp add: bij_betw_def)
 
+lemma Nats_infinite: "infinite (\<nat> :: 'a set)"
+  by (metis Nats_def finite_imageD infinite_UNIV_char_0 inj_on_of_nat)
+
 end
 
 context comm_monoid_set