equal
deleted
inserted
replaced
17 begin |
17 begin |
18 |
18 |
19 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}" |
19 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}" |
20 by blast |
20 by blast |
21 |
21 |
22 lemma image_Collect_subsetI: |
22 lemma image_Collect_subsetI: "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B" |
23 "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B" |
|
24 by blast |
23 by blast |
25 |
24 |
26 lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X" |
25 lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X" |
27 by auto |
26 by auto |
28 |
27 |