equal
deleted
inserted
replaced
517 using \<open>b > 0\<close> \<open>e > 0\<close> by auto |
517 using \<open>b > 0\<close> \<open>e > 0\<close> by auto |
518 then show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (inverse (f x y)) ((inverse \<circ> l) y) < e" |
518 then show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (inverse (f x y)) ((inverse \<circ> l) y) < e" |
519 using lte by (force intro: eventually_mono) |
519 using lte by (force intro: eventually_mono) |
520 qed |
520 qed |
521 |
521 |
522 lemma uniform_lim_div: |
522 lemma uniform_lim_divide: |
523 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_field" |
523 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_field" |
524 assumes f: "uniform_limit S f l F" |
524 assumes f: "uniform_limit S f l F" |
525 and g: "uniform_limit S g m F" |
525 and g: "uniform_limit S g m F" |
526 and l: "bounded (l ` S)" |
526 and l: "bounded (l ` S)" |
527 and b: "\<And>x. x \<in> S \<Longrightarrow> b \<le> norm(m x)" |
527 and b: "\<And>x. x \<in> S \<Longrightarrow> b \<le> norm(m x)" |