src/HOL/Library/Topology_Euclidean_Space.thy
changeset 31654 83662a8604c2
parent 31592 61ee6256d863
child 31655 bcb1eb2197f8
equal deleted inserted replaced
31593:dc65b2f78664 31654:83662a8604c2
  1100 
  1100 
  1101 subsection{* Limits, defined as vacuously true when the limit is trivial. *}
  1101 subsection{* Limits, defined as vacuously true when the limit is trivial. *}
  1102 
  1102 
  1103   text{* Notation Lim to avoid collition with lim defined in analysis *}
  1103   text{* Notation Lim to avoid collition with lim defined in analysis *}
  1104 definition
  1104 definition
  1105   Lim :: "'a net \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b" where
  1105   Lim :: "'a net \<Rightarrow> ('a \<Rightarrow> 'b::t2_space) \<Rightarrow> 'b" where
  1106   "Lim net f = (THE l. (f ---> l) net)"
  1106   "Lim net f = (THE l. (f ---> l) net)"
  1107 
  1107 
  1108 lemma Lim:
  1108 lemma Lim:
  1109  "(f ---> l) net \<longleftrightarrow>
  1109  "(f ---> l) net \<longleftrightarrow>
  1110         trivial_limit net \<or>
  1110         trivial_limit net \<or>
  1400 qed
  1400 qed
  1401 
  1401 
  1402 text{* Uniqueness of the limit, when nontrivial. *}
  1402 text{* Uniqueness of the limit, when nontrivial. *}
  1403 
  1403 
  1404 lemma Lim_unique:
  1404 lemma Lim_unique:
  1405   fixes f :: "'a \<Rightarrow> 'b::metric_space"
  1405   fixes f :: "'a \<Rightarrow> 'b::t2_space"
  1406   assumes "\<not> trivial_limit net"  "(f ---> l) net"  "(f ---> l') net"
  1406   assumes "\<not> trivial_limit net"  "(f ---> l) net"  "(f ---> l') net"
  1407   shows "l = l'"
  1407   shows "l = l'"
  1408 proof (rule ccontr)
  1408 proof (rule ccontr)
  1409   let ?d = "dist l l' / 2"
       
  1410   assume "l \<noteq> l'"
  1409   assume "l \<noteq> l'"
  1411   then have "0 < ?d" by (simp add: dist_nz)
  1410   obtain U V where "open U" "open V" "l \<in> U" "l' \<in> V" "U \<inter> V = {}"
  1412   have "eventually (\<lambda>x. dist (f x) l < ?d) net"
  1411     using hausdorff [OF `l \<noteq> l'`] by fast
  1413     using `(f ---> l) net` `0 < ?d` by (rule tendstoD)
  1412   have "eventually (\<lambda>x. f x \<in> U) net"
       
  1413     using `(f ---> l) net` `open U` `l \<in> U` by (rule topological_tendstoD)
  1414   moreover
  1414   moreover
  1415   have "eventually (\<lambda>x. dist (f x) l' < ?d) net"
  1415   have "eventually (\<lambda>x. f x \<in> V) net"
  1416     using `(f ---> l') net` `0 < ?d` by (rule tendstoD)
  1416     using `(f ---> l') net` `open V` `l' \<in> V` by (rule topological_tendstoD)
  1417   ultimately
  1417   ultimately
  1418   have "eventually (\<lambda>x. False) net"
  1418   have "eventually (\<lambda>x. False) net"
  1419   proof (rule eventually_elim2)
  1419   proof (rule eventually_elim2)
  1420     fix x
  1420     fix x
  1421     assume *: "dist (f x) l < ?d" "dist (f x) l' < ?d"
  1421     assume "f x \<in> U" "f x \<in> V"
  1422     have "dist l l' \<le> dist (f x) l + dist (f x) l'"
  1422     hence "f x \<in> U \<inter> V" by simp
  1423       by (rule dist_triangle_alt)
  1423     with `U \<inter> V = {}` show "False" by simp
  1424     also from * have "\<dots> < ?d + ?d"
       
  1425       by (rule add_strict_mono)
       
  1426     also have "\<dots> = dist l l'" by simp
       
  1427     finally show "False" by simp
       
  1428   qed
  1424   qed
  1429   with `\<not> trivial_limit net` show "False"
  1425   with `\<not> trivial_limit net` show "False"
  1430     by (simp add: eventually_False)
  1426     by (simp add: eventually_False)
  1431 qed
  1427 qed
  1432 
  1428 
  1433 lemma tendsto_Lim:
  1429 lemma tendsto_Lim:
  1434   fixes f :: "'a \<Rightarrow> 'b::metric_space"
  1430   fixes f :: "'a \<Rightarrow> 'b::t2_space"
  1435   shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
  1431   shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
  1436   unfolding Lim_def using Lim_unique[of net f] by auto
  1432   unfolding Lim_def using Lim_unique[of net f] by auto
  1437 
  1433 
  1438 text{* Limit under bilinear function *}
  1434 text{* Limit under bilinear function *}
  1439 
  1435