equal
deleted
inserted
replaced
882 by (unfold UNION_def) blast |
882 by (unfold UNION_def) blast |
883 |
883 |
884 lemma UN_cong [cong]: |
884 lemma UN_cong [cong]: |
885 "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)" |
885 "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)" |
886 by (simp add: UNION_def) |
886 by (simp add: UNION_def) |
|
887 |
|
888 lemma strong_UN_cong: |
|
889 "A = B ==> (!!x. x:B =simp=> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)" |
|
890 by (simp add: UNION_def simp_implies_def) |
887 |
891 |
888 |
892 |
889 subsubsection {* Intersections of families *} |
893 subsubsection {* Intersections of families *} |
890 |
894 |
891 text {* @{term [source] "INT x:A. B x"} is @{term "Inter (B`A)"}. *} |
895 text {* @{term [source] "INT x:A. B x"} is @{term "Inter (B`A)"}. *} |