4157 shows "continuous (at x) g" |
4157 shows "continuous (at x) g" |
4158 using continuous_transform_within [of d x UNIV f g] assms by simp |
4158 using continuous_transform_within [of d x UNIV f g] assms by simp |
4159 |
4159 |
4160 subsubsection {* Structural rules for pointwise continuity *} |
4160 subsubsection {* Structural rules for pointwise continuity *} |
4161 |
4161 |
4162 lemma continuous_within_id: "continuous (at a within s) (\<lambda>x. x)" |
4162 ML {* |
|
4163 |
|
4164 structure Continuous_Intros = Named_Thms |
|
4165 ( |
|
4166 val name = @{binding continuous_intros} |
|
4167 val description = "Structural introduction rules for pointwise continuity" |
|
4168 ) |
|
4169 |
|
4170 *} |
|
4171 |
|
4172 setup Continuous_Intros.setup |
|
4173 |
|
4174 lemma continuous_within_id[continuous_intros]: "continuous (at a within s) (\<lambda>x. x)" |
4163 unfolding continuous_within by (rule tendsto_ident_at_within) |
4175 unfolding continuous_within by (rule tendsto_ident_at_within) |
4164 |
4176 |
4165 lemma continuous_at_id: "continuous (at a) (\<lambda>x. x)" |
4177 lemma continuous_at_id[continuous_intros]: "continuous (at a) (\<lambda>x. x)" |
4166 unfolding continuous_at by (rule tendsto_ident_at) |
4178 unfolding continuous_at by (rule tendsto_ident_at) |
4167 |
4179 |
4168 lemma continuous_const: "continuous F (\<lambda>x. c)" |
4180 lemma continuous_const[continuous_intros]: "continuous F (\<lambda>x. c)" |
4169 unfolding continuous_def by (rule tendsto_const) |
4181 unfolding continuous_def by (rule tendsto_const) |
4170 |
4182 |
4171 lemma continuous_fst: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))" |
4183 lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))" |
4172 unfolding continuous_def by (rule tendsto_fst) |
4184 unfolding continuous_def by (rule tendsto_fst) |
4173 |
4185 |
4174 lemma continuous_snd: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))" |
4186 lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))" |
4175 unfolding continuous_def by (rule tendsto_snd) |
4187 unfolding continuous_def by (rule tendsto_snd) |
4176 |
4188 |
4177 lemma continuous_Pair: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))" |
4189 lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))" |
4178 unfolding continuous_def by (rule tendsto_Pair) |
4190 unfolding continuous_def by (rule tendsto_Pair) |
4179 |
4191 |
4180 lemma continuous_dist: |
4192 lemma continuous_dist[continuous_intros]: |
4181 assumes "continuous F f" and "continuous F g" |
4193 assumes "continuous F f" and "continuous F g" |
4182 shows "continuous F (\<lambda>x. dist (f x) (g x))" |
4194 shows "continuous F (\<lambda>x. dist (f x) (g x))" |
4183 using assms unfolding continuous_def by (rule tendsto_dist) |
4195 using assms unfolding continuous_def by (rule tendsto_dist) |
4184 |
4196 |
4185 lemma continuous_infdist: |
4197 lemma continuous_infdist[continuous_intros]: |
4186 assumes "continuous F f" |
4198 assumes "continuous F f" |
4187 shows "continuous F (\<lambda>x. infdist (f x) A)" |
4199 shows "continuous F (\<lambda>x. infdist (f x) A)" |
4188 using assms unfolding continuous_def by (rule tendsto_infdist) |
4200 using assms unfolding continuous_def by (rule tendsto_infdist) |
4189 |
4201 |
4190 lemma continuous_norm: |
4202 lemma continuous_norm[continuous_intros]: |
4191 shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))" |
4203 shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))" |
4192 unfolding continuous_def by (rule tendsto_norm) |
4204 unfolding continuous_def by (rule tendsto_norm) |
4193 |
4205 |
4194 lemma continuous_infnorm: |
4206 lemma continuous_infnorm[continuous_intros]: |
4195 shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))" |
4207 shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))" |
4196 unfolding continuous_def by (rule tendsto_infnorm) |
4208 unfolding continuous_def by (rule tendsto_infnorm) |
4197 |
4209 |
4198 lemma continuous_add: |
4210 lemma continuous_add[continuous_intros]: |
4199 fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" |
4211 fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" |
4200 shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x + g x)" |
4212 shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x + g x)" |
4201 unfolding continuous_def by (rule tendsto_add) |
4213 unfolding continuous_def by (rule tendsto_add) |
4202 |
4214 |
4203 lemma continuous_minus: |
4215 lemma continuous_minus[continuous_intros]: |
4204 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" |
4216 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" |
4205 shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)" |
4217 shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)" |
4206 unfolding continuous_def by (rule tendsto_minus) |
4218 unfolding continuous_def by (rule tendsto_minus) |
4207 |
4219 |
4208 lemma continuous_diff: |
4220 lemma continuous_diff[continuous_intros]: |
4209 fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" |
4221 fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" |
4210 shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x - g x)" |
4222 shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x - g x)" |
4211 unfolding continuous_def by (rule tendsto_diff) |
4223 unfolding continuous_def by (rule tendsto_diff) |
4212 |
4224 |
4213 lemma continuous_scaleR: |
4225 lemma continuous_scaleR[continuous_intros]: |
4214 fixes g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" |
4226 fixes g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector" |
4215 shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x *\<^sub>R g x)" |
4227 shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x *\<^sub>R g x)" |
4216 unfolding continuous_def by (rule tendsto_scaleR) |
4228 unfolding continuous_def by (rule tendsto_scaleR) |
4217 |
4229 |
4218 lemma continuous_mult: |
4230 lemma continuous_mult[continuous_intros]: |
4219 fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra" |
4231 fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra" |
4220 shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x * g x)" |
4232 shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x * g x)" |
4221 unfolding continuous_def by (rule tendsto_mult) |
4233 unfolding continuous_def by (rule tendsto_mult) |
4222 |
4234 |
4223 lemma continuous_inner: |
4235 lemma continuous_inner[continuous_intros]: |
4224 assumes "continuous F f" and "continuous F g" |
4236 assumes "continuous F f" and "continuous F g" |
4225 shows "continuous F (\<lambda>x. inner (f x) (g x))" |
4237 shows "continuous F (\<lambda>x. inner (f x) (g x))" |
4226 using assms unfolding continuous_def by (rule tendsto_inner) |
4238 using assms unfolding continuous_def by (rule tendsto_inner) |
4227 |
4239 |
4228 lemma continuous_inverse: |
4240 lemma continuous_inverse[continuous_intros]: |
4229 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra" |
4241 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra" |
4230 assumes "continuous F f" and "f (netlimit F) \<noteq> 0" |
4242 assumes "continuous F f" and "f (netlimit F) \<noteq> 0" |
4231 shows "continuous F (\<lambda>x. inverse (f x))" |
4243 shows "continuous F (\<lambda>x. inverse (f x))" |
4232 using assms unfolding continuous_def by (rule tendsto_inverse) |
4244 using assms unfolding continuous_def by (rule tendsto_inverse) |
4233 |
4245 |
4234 lemma continuous_at_within_inverse: |
4246 lemma continuous_at_within_inverse[continuous_intros]: |
4235 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra" |
4247 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra" |
4236 assumes "continuous (at a within s) f" and "f a \<noteq> 0" |
4248 assumes "continuous (at a within s) f" and "f a \<noteq> 0" |
4237 shows "continuous (at a within s) (\<lambda>x. inverse (f x))" |
4249 shows "continuous (at a within s) (\<lambda>x. inverse (f x))" |
4238 using assms unfolding continuous_within by (rule tendsto_inverse) |
4250 using assms unfolding continuous_within by (rule tendsto_inverse) |
4239 |
4251 |
4240 lemma continuous_at_inverse: |
4252 lemma continuous_at_inverse[continuous_intros]: |
4241 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra" |
4253 fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra" |
4242 assumes "continuous (at a) f" and "f a \<noteq> 0" |
4254 assumes "continuous (at a) f" and "f a \<noteq> 0" |
4243 shows "continuous (at a) (\<lambda>x. inverse (f x))" |
4255 shows "continuous (at a) (\<lambda>x. inverse (f x))" |
4244 using assms unfolding continuous_at by (rule tendsto_inverse) |
4256 using assms unfolding continuous_at by (rule tendsto_inverse) |
4245 |
|
4246 lemmas continuous_intros = continuous_at_id continuous_within_id |
|
4247 continuous_const continuous_dist continuous_norm continuous_infnorm |
|
4248 continuous_add continuous_minus continuous_diff continuous_scaleR continuous_mult |
|
4249 continuous_inner continuous_at_inverse continuous_at_within_inverse |
|
4250 |
4257 |
4251 subsubsection {* Structural rules for setwise continuity *} |
4258 subsubsection {* Structural rules for setwise continuity *} |
4252 |
4259 |
4253 lemma continuous_on_id: "continuous_on s (\<lambda>x. x)" |
4260 lemma continuous_on_id: "continuous_on s (\<lambda>x. x)" |
4254 unfolding continuous_on_def by (fast intro: tendsto_ident_at_within) |
4261 unfolding continuous_on_def by (fast intro: tendsto_ident_at_within) |