# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1645220401 0
# Node ID f0e2023f361a9e615b4d57db6bec366314a543d9
# Parent  6eff5c260381efcded1ddac45a637d1928a4b3d7
one new lemma

diff -r 6eff5c260381 -r f0e2023f361a 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