equal
deleted
inserted
replaced
130 by (unfold Id_on_def) (iprover elim!: UN_E singletonE) |
130 by (unfold Id_on_def) (iprover elim!: UN_E singletonE) |
131 |
131 |
132 lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)" |
132 lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)" |
133 by blast |
133 by blast |
134 |
134 |
135 lemma Id_on_def' [nitpick_unfold, code]: |
135 lemma Id_on_def' [nitpick_unfold]: |
136 "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)" |
136 "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)" |
137 by auto |
137 by auto |
138 |
138 |
139 lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A" |
139 lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A" |
140 by blast |
140 by blast |