equal
deleted
inserted
replaced
79 proof |
79 proof |
80 fix a b :: "'a set" assume "a \<subseteq> b" |
80 fix a b :: "'a set" assume "a \<subseteq> b" |
81 let ?S = "\<lambda>n::nat. if n=0 then a else b" |
81 let ?S = "\<lambda>n::nat. if n=0 then a else b" |
82 have "chain ?S" using \<open>a \<subseteq> b\<close> by(auto simp: chain_def) |
82 have "chain ?S" using \<open>a \<subseteq> b\<close> by(auto simp: chain_def) |
83 hence "f(UN n. ?S n) = (UN n. f(?S n))" |
83 hence "f(UN n. ?S n) = (UN n. f(?S n))" |
84 using assms by(simp add: cont_def) |
84 using assms by (simp add: cont_def del: if_image_distrib) |
85 moreover have "(UN n. ?S n) = b" using \<open>a \<subseteq> b\<close> by (auto split: if_splits) |
85 moreover have "(UN n. ?S n) = b" using \<open>a \<subseteq> b\<close> by (auto split: if_splits) |
86 moreover have "(UN n. f(?S n)) = f a \<union> f b" by (auto split: if_splits) |
86 moreover have "(UN n. f(?S n)) = f a \<union> f b" by (auto split: if_splits) |
87 ultimately show "f a \<subseteq> f b" by (metis Un_upper1) |
87 ultimately show "f a \<subseteq> f b" by (metis Un_upper1) |
88 qed |
88 qed |
89 |
89 |