src/HOL/Library/Topology_Euclidean_Space.thy
 changeset 31654 83662a8604c2 parent 31592 61ee6256d863 child 31655 bcb1eb2197f8
equal 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)`
`  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 `