equal
deleted
inserted
replaced
54 lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})" |
54 lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})" |
55 by blast |
55 by blast |
56 |
56 |
57 lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})" |
57 lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})" |
58 by blast |
58 by blast |
|
59 |
|
60 lemma mem_UN_compreh_ex_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)" |
|
61 by blast |
|
62 |
|
63 lemma UN_compreh_ex_eq_eq: |
|
64 "\<Union>{y. \<exists>x\<in>A. y = {}} = {}" |
|
65 "\<Union>{y. \<exists>x\<in>A. y = {x}} = A" |
|
66 by blast+ |
59 |
67 |
60 lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd" |
68 lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd" |
61 by (unfold comp_apply collect_def SUP_def) |
69 by (unfold comp_apply collect_def SUP_def) |
62 |
70 |
63 lemma wpull_cong: |
71 lemma wpull_cong: |