equal
deleted
inserted
replaced
1266 hence "i-k\<le>n \<and> x \<in> M((i-k)+k)" by auto |
1266 hence "i-k\<le>n \<and> x \<in> M((i-k)+k)" by auto |
1267 thus "x \<in> ?A" by blast |
1267 thus "x \<in> ?A" by blast |
1268 qed |
1268 qed |
1269 qed |
1269 qed |
1270 |
1270 |
|
1271 lemma UN_le_add_shift_strict: |
|
1272 "(\<Union>i<n::nat. M(i+k)) = (\<Union>i\<in>{k..<n+k}. M i)" (is "?A = ?B") |
|
1273 proof |
|
1274 show "?B \<subseteq> ?A" |
|
1275 proof |
|
1276 fix x assume "x \<in> ?B" |
|
1277 then obtain i where i: "i \<in> {k..<n+k}" "x \<in> M(i)" by auto |
|
1278 then have "i - k < n \<and> x \<in> M((i-k) + k)" by auto |
|
1279 then show "x \<in> ?A" using UN_le_add_shift by blast |
|
1280 qed |
|
1281 qed (fastforce) |
|
1282 |
1271 lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)" |
1283 lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)" |
1272 by (auto simp add: atLeast0LessThan) |
1284 by (auto simp add: atLeast0LessThan) |
1273 |
1285 |
1274 lemma UN_finite_subset: |
1286 lemma UN_finite_subset: |
1275 "(\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C" |
1287 "(\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C" |