equal
deleted
inserted
replaced
117 |
117 |
118 |
118 |
119 text{* |
119 text{* |
120 illustrates Union as well as image |
120 illustrates Union as well as image |
121 *} |
121 *} |
|
122 |
122 lemma "f`A \<union> g`A = (\<Union>x\<in>A. {f x, g x})" |
123 lemma "f`A \<union> g`A = (\<Union>x\<in>A. {f x, g x})" |
123 apply (blast) |
124 by blast |
124 done |
|
125 |
125 |
126 lemma "f ` {(x,y). P x y} = {f(x,y) | x y. P x y}" |
126 lemma "f ` {(x,y). P x y} = {f(x,y) | x y. P x y}" |
127 apply (blast) |
127 by blast |
128 done |
|
129 |
128 |
130 text{*actually a macro!*} |
129 text{*actually a macro!*} |
131 |
130 |
132 lemma "range f = f`UNIV" |
131 lemma "range f = f`UNIV" |
133 apply (blast) |
132 by blast |
134 done |
|
135 |
133 |
136 |
134 |
137 text{* |
135 text{* |
138 inverse image |
136 inverse image |
139 *} |
137 *} |