equal
deleted
inserted
replaced
1318 (*injectivity's required. Left-to-right inclusion holds even if A is empty*) |
1318 (*injectivity's required. Left-to-right inclusion holds even if A is empty*) |
1319 lemma image_INT: "inj_on f C \<Longrightarrow> \<forall>x\<in>A. B x \<subseteq> C \<Longrightarrow> j \<in> A \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)" |
1319 lemma image_INT: "inj_on f C \<Longrightarrow> \<forall>x\<in>A. B x \<subseteq> C \<Longrightarrow> j \<in> A \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)" |
1320 by (auto simp add: inj_on_def) blast |
1320 by (auto simp add: inj_on_def) blast |
1321 |
1321 |
1322 lemma bij_image_INT: "bij f \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)" |
1322 lemma bij_image_INT: "bij f \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)" |
1323 apply (simp only: bij_def) |
1323 by (auto simp: bij_def inj_def surj_def) blast |
1324 apply (simp only: inj_on_def surj_def) |
|
1325 apply auto |
|
1326 apply blast |
|
1327 done |
|
1328 |
1324 |
1329 lemma UNION_fun_upd: "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})" |
1325 lemma UNION_fun_upd: "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})" |
1330 by (auto simp add: set_eq_iff) |
1326 by (auto simp add: set_eq_iff) |
1331 |
1327 |
1332 lemma bij_betw_Pow: |
1328 lemma bij_betw_Pow: |