# HG changeset patch
# User wenzelm
# Date 1645222333 -3600
# Node ID a29d49a636edb5199d72fa18c3d55dacf87e3924
# Parent  f0e2023f361a9e615b4d57db6bec366314a543d9# Parent  678fae02f9b3bf5ab5f9b24f7fd61da8b40abd89
merged

diff -r 678fae02f9b3 -r a29d49a636ed src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri Feb 18 23:10:33 2022 +0100
+++ b/src/HOL/Set_Interval.thy	Fri Feb 18 23:12:13 2022 +0100
@@ -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