1922 "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow> |
1922 "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow> |
1923 \<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x \<Longrightarrow> |
1923 \<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x \<Longrightarrow> |
1924 continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)" |
1924 continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)" |
1925 by (rule continuous_on_If) auto |
1925 by (rule continuous_on_If) auto |
1926 |
1926 |
1927 lemma continuous_on_id[continuous_intros]: "continuous_on s (\<lambda>x. x)" |
1927 lemma continuous_on_id[continuous_intros,simp]: "continuous_on s (\<lambda>x. x)" |
1928 unfolding continuous_on_def by fast |
1928 unfolding continuous_on_def by fast |
1929 |
1929 |
1930 lemma continuous_on_id'[continuous_intros]: "continuous_on s id" |
1930 lemma continuous_on_id'[continuous_intros,simp]: "continuous_on s id" |
1931 unfolding continuous_on_def id_def by fast |
1931 unfolding continuous_on_def id_def by fast |
1932 |
1932 |
1933 lemma continuous_on_const[continuous_intros]: "continuous_on s (\<lambda>x. c)" |
1933 lemma continuous_on_const[continuous_intros,simp]: "continuous_on s (\<lambda>x. c)" |
1934 unfolding continuous_on_def by auto |
1934 unfolding continuous_on_def by auto |
1935 |
1935 |
1936 lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f" |
1936 lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f" |
1937 unfolding continuous_on_def |
1937 unfolding continuous_on_def |
1938 by (metis subset_eq tendsto_within_subset) |
1938 by (metis subset_eq tendsto_within_subset) |