equal
deleted
inserted
replaced
103 lemma sum_case_o_inj: |
103 lemma sum_case_o_inj: |
104 "sum_case f g \<circ> Inl = f" |
104 "sum_case f g \<circ> Inl = f" |
105 "sum_case f g \<circ> Inr = g" |
105 "sum_case f g \<circ> Inr = g" |
106 by auto |
106 by auto |
107 |
107 |
108 lemma ident_o_ident: "(\<lambda>x. x) \<circ> (\<lambda>x. x) = (\<lambda>x. x)" |
|
109 by (rule o_def) |
|
110 |
|
111 lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)" |
108 lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)" |
112 by blast |
109 by blast |
113 |
110 |
114 lemma UN_compreh_eq_eq: |
111 lemma UN_compreh_eq_eq: |
115 "\<Union>{y. \<exists>x\<in>A. y = {}} = {}" |
112 "\<Union>{y. \<exists>x\<in>A. y = {}} = {}" |