equal
deleted
inserted
replaced
354 by blast |
354 by blast |
355 |
355 |
356 lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s" |
356 lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s" |
357 by blast |
357 by blast |
358 |
358 |
|
359 lemma fst_eq_Domain: "fst ` R = Domain R"; |
|
360 apply auto |
|
361 apply (rule image_eqI, auto) |
|
362 done |
|
363 |
359 |
364 |
360 subsection {* Range *} |
365 subsection {* Range *} |
361 |
366 |
362 lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)" |
367 lemma Range_iff: "(a : Range r) = (EX y. (y, a) : r)" |
363 by (simp add: Domain_def Range_def) |
368 by (simp add: Domain_def Range_def) |
389 lemma Range_Diff_subset: "Range(A) - Range(B) \<subseteq> Range(A - B)" |
394 lemma Range_Diff_subset: "Range(A) - Range(B) \<subseteq> Range(A - B)" |
390 by blast |
395 by blast |
391 |
396 |
392 lemma Range_Union: "Range (Union S) = (\<Union>A\<in>S. Range A)" |
397 lemma Range_Union: "Range (Union S) = (\<Union>A\<in>S. Range A)" |
393 by blast |
398 by blast |
|
399 |
|
400 lemma snd_eq_Range: "snd ` R = Range R"; |
|
401 apply auto |
|
402 apply (rule image_eqI, auto) |
|
403 done |
394 |
404 |
395 |
405 |
396 subsection {* Image of a set under a relation *} |
406 subsection {* Image of a set under a relation *} |
397 |
407 |
398 lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)" |
408 lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)" |