equal
deleted
inserted
replaced
90 |
90 |
91 text{*The Identity Function: @{term id}*} |
91 text{*The Identity Function: @{term id}*} |
92 lemma id_apply [simp]: "id x = x" |
92 lemma id_apply [simp]: "id x = x" |
93 by (simp add: id_def) |
93 by (simp add: id_def) |
94 |
94 |
95 lemma inj_on_id: "inj_on id A" |
95 lemma inj_on_id[simp]: "inj_on id A" |
96 by (simp add: inj_on_def) |
96 by (simp add: inj_on_def) |
97 |
97 |
98 lemma surj_id: "surj id" |
98 lemma inj_on_id2[simp]: "inj_on (%x. x) A" |
|
99 by (simp add: inj_on_def) |
|
100 |
|
101 lemma surj_id[simp]: "surj id" |
99 by (simp add: surj_def) |
102 by (simp add: surj_def) |
100 |
103 |
101 lemma bij_id: "bij id" |
104 lemma bij_id[simp]: "bij id" |
102 by (simp add: bij_def inj_on_id surj_id) |
105 by (simp add: bij_def inj_on_id surj_id) |
103 |
106 |
104 |
107 |
105 |
108 |
106 subsection{*The Composition Operator: @{term "f \<circ> g"}*} |
109 subsection{*The Composition Operator: @{term "f \<circ> g"}*} |