equal
deleted
inserted
replaced
602 by (auto simp: analytic_on_def) |
602 by (auto simp: analytic_on_def) |
603 |
603 |
604 lemma analytic_on_Un: "f analytic_on (s \<union> t) \<longleftrightarrow> f analytic_on s \<and> f analytic_on t" |
604 lemma analytic_on_Un: "f analytic_on (s \<union> t) \<longleftrightarrow> f analytic_on s \<and> f analytic_on t" |
605 by (auto simp: analytic_on_def) |
605 by (auto simp: analytic_on_def) |
606 |
606 |
607 lemma analytic_on_Union: "f analytic_on (\<Union> s) \<longleftrightarrow> (\<forall>t \<in> s. f analytic_on t)" |
607 lemma analytic_on_Union: "f analytic_on (\<Union>s) \<longleftrightarrow> (\<forall>t \<in> s. f analytic_on t)" |
608 by (auto simp: analytic_on_def) |
608 by (auto simp: analytic_on_def) |
609 |
609 |
610 lemma analytic_on_UN: "f analytic_on (\<Union>i\<in>I. s i) \<longleftrightarrow> (\<forall>i\<in>I. f analytic_on (s i))" |
610 lemma analytic_on_UN: "f analytic_on (\<Union>i\<in>I. s i) \<longleftrightarrow> (\<forall>i\<in>I. f analytic_on (s i))" |
611 by (auto simp: analytic_on_def) |
611 by (auto simp: analytic_on_def) |
612 |
612 |