src/HOL/Lim.thy
 changeset 44568 e6f291cb5810 parent 44532 a2e9b39df938 child 44570 b93d1b3ee300
equal inserted replaced
`   208   also have "g x \<le> f x" by (rule 2 [OF x])`
`   208   also have "g x \<le> f x" by (rule 2 [OF x])`
`   209   also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)`
`   209   also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)`
`   210   also have "\<bar>f x\<bar> = norm (f x - 0)" by simp`
`   210   also have "\<bar>f x\<bar> = norm (f x - 0)" by simp`
`   211   finally show "norm (g x - 0) \<le> norm (f x - 0)" .`
`   211   finally show "norm (g x - 0) \<le> norm (f x - 0)" .`
`   212 qed`
`   212 qed`
`   258 `
`   213 `
`   259 `
`   214 `
`   260 subsection {* Continuity *}`
`   215 subsection {* Continuity *}`
`   261 `
`   216 `
`   262 lemma LIM_isCont_iff:`
`   217 lemma LIM_isCont_iff:`
`   493 lemma LIMSEQ_SEQ_conv:`
`   448 lemma LIMSEQ_SEQ_conv:`
`   494   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =`
`   449   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> (a::'a::metric_space) \<longrightarrow> (\<lambda>n. X (S n)) ----> L) =`
`   495    (X -- a --> (L::'b::topological_space))"`
`   450    (X -- a --> (L::'b::topological_space))"`
`   496   using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..`
`   451   using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..`
`   497 `
`   452 `
`   523 end`
`   453 end`