added lemma
authorAndreas Lochbihler
Fri, 15 Feb 2013 10:52:47 +0100
changeset 51152 b52cc015429a
parent 51140 59e311235de4
child 51153 b14ee572cc7b
added lemma
src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri Feb 15 09:59:46 2013 +0100
+++ b/src/HOL/Set_Interval.thy	Fri Feb 15 10:52:47 2013 +0100
@@ -564,6 +564,9 @@
   qed
 qed auto
 
+lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}"
+by(auto intro!: image_eqI[where x="nat x", standard])
+
 context ordered_ab_group_add
 begin