equal
deleted
inserted
replaced
32 "id = (\<lambda>x. x)" |
32 "id = (\<lambda>x. x)" |
33 |
33 |
34 lemma id_apply [simp]: "id x = x" |
34 lemma id_apply [simp]: "id x = x" |
35 by (simp add: id_def) |
35 by (simp add: id_def) |
36 |
36 |
37 lemma image_ident [simp]: "(%x. x) ` Y = Y" |
|
38 by blast |
|
39 |
|
40 lemma image_id [simp]: "id ` Y = Y" |
37 lemma image_id [simp]: "id ` Y = Y" |
41 by (simp add: id_def) |
38 by (simp add: id_def) |
42 |
|
43 lemma vimage_ident [simp]: "(%x. x) -` Y = Y" |
|
44 by blast |
|
45 |
39 |
46 lemma vimage_id [simp]: "id -` A = A" |
40 lemma vimage_id [simp]: "id -` A = A" |
47 by (simp add: id_def) |
41 by (simp add: id_def) |
48 |
42 |
49 |
43 |