1956 lemma Lim_dist_ubound: |
1956 lemma Lim_dist_ubound: |
1957 assumes "\<not>(trivial_limit net)" |
1957 assumes "\<not>(trivial_limit net)" |
1958 and "(f ---> l) net" |
1958 and "(f ---> l) net" |
1959 and "eventually (\<lambda>x. dist a (f x) \<le> e) net" |
1959 and "eventually (\<lambda>x. dist a (f x) \<le> e) net" |
1960 shows "dist a l \<le> e" |
1960 shows "dist a l \<le> e" |
1961 proof - |
1961 using assms by (fast intro: tendsto_le tendsto_intros) |
1962 have "dist a l \<in> {..e}" |
|
1963 proof (rule Lim_in_closed_set) |
|
1964 show "closed {..e}" |
|
1965 by simp |
|
1966 show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net" |
|
1967 by (simp add: assms) |
|
1968 show "\<not> trivial_limit net" |
|
1969 by fact |
|
1970 show "((\<lambda>x. dist a (f x)) ---> dist a l) net" |
|
1971 by (intro tendsto_intros assms) |
|
1972 qed |
|
1973 then show ?thesis by simp |
|
1974 qed |
|
1975 |
1962 |
1976 lemma Lim_norm_ubound: |
1963 lemma Lim_norm_ubound: |
1977 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1964 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1978 assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) \<le> e) net" |
1965 assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) \<le> e) net" |
1979 shows "norm(l) \<le> e" |
1966 shows "norm(l) \<le> e" |
1980 proof - |
1967 using assms by (fast intro: tendsto_le tendsto_intros) |
1981 have "norm l \<in> {..e}" |
|
1982 proof (rule Lim_in_closed_set) |
|
1983 show "closed {..e}" |
|
1984 by simp |
|
1985 show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net" |
|
1986 by (simp add: assms) |
|
1987 show "\<not> trivial_limit net" |
|
1988 by fact |
|
1989 show "((\<lambda>x. norm (f x)) ---> norm l) net" |
|
1990 by (intro tendsto_intros assms) |
|
1991 qed |
|
1992 then show ?thesis by simp |
|
1993 qed |
|
1994 |
1968 |
1995 lemma Lim_norm_lbound: |
1969 lemma Lim_norm_lbound: |
1996 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1970 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
1997 assumes "\<not> trivial_limit net" |
1971 assumes "\<not> trivial_limit net" |
1998 and "(f ---> l) net" |
1972 and "(f ---> l) net" |
1999 and "eventually (\<lambda>x. e \<le> norm (f x)) net" |
1973 and "eventually (\<lambda>x. e \<le> norm (f x)) net" |
2000 shows "e \<le> norm l" |
1974 shows "e \<le> norm l" |
2001 proof - |
1975 using assms by (fast intro: tendsto_le tendsto_intros) |
2002 have "norm l \<in> {e..}" |
|
2003 proof (rule Lim_in_closed_set) |
|
2004 show "closed {e..}" |
|
2005 by simp |
|
2006 show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net" |
|
2007 by (simp add: assms) |
|
2008 show "\<not> trivial_limit net" |
|
2009 by fact |
|
2010 show "((\<lambda>x. norm (f x)) ---> norm l) net" |
|
2011 by (intro tendsto_intros assms) |
|
2012 qed |
|
2013 then show ?thesis by simp |
|
2014 qed |
|
2015 |
1976 |
2016 text{* Limit under bilinear function *} |
1977 text{* Limit under bilinear function *} |
2017 |
1978 |
2018 lemma Lim_bilinear: |
1979 lemma Lim_bilinear: |
2019 assumes "(f ---> l) net" |
1980 assumes "(f ---> l) net" |