avoid using vec1 in continuity lemmas
authorhuffman
Fri Jun 12 16:04:55 2009 -0700 (2009-06-12)
changeset 31589eeebb2915035
parent 31588 2651f172c38b
child 31590 776d6a4c1327
avoid using vec1 in continuity lemmas
src/HOL/Library/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Jun 12 15:46:21 2009 -0700
     1.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Jun 12 16:04:55 2009 -0700
     1.3 @@ -5149,58 +5149,37 @@
     1.4  
     1.5  subsection{* Closure of halfspaces and hyperplanes.                                    *}
     1.6  
     1.7 -lemma Lim_vec1_dot: fixes f :: "real^'m \<Rightarrow> real^'n::finite"
     1.8 -  assumes "(f ---> l) net"  shows "((vec1 o (\<lambda>y. a \<bullet> (f y))) ---> vec1(a \<bullet> l)) net"
     1.9 -proof(cases "a = vec 0")
    1.10 -  case True thus ?thesis using dot_lzero and Lim_const[of 0 net] unfolding vec1_vec and o_def by auto
    1.11 -next
    1.12 -  case False
    1.13 -  { fix e::real
    1.14 -    assume "0 < e"
    1.15 -    with `a \<noteq> vec 0` have "0 < e / norm a" by (simp add: divide_pos_pos)
    1.16 -    with assms(1) have "eventually (\<lambda>x. dist (f x) l < e / norm a) net"
    1.17 -      by (rule tendstoD)
    1.18 -    moreover
    1.19 -    { fix z assume "dist (f z) l < e / norm a"
    1.20 -      hence "norm a * norm (f z - l) < e" unfolding dist_norm and
    1.21 -	pos_less_divide_eq[OF False[unfolded vec_0 zero_less_norm_iff[of a, THEN sym]]] and real_mult_commute by auto
    1.22 -      hence "\<bar>a \<bullet> f z - a \<bullet> l\<bar> < e"
    1.23 -        using order_le_less_trans[OF norm_cauchy_schwarz_abs[of a "f z - l"], of e]
    1.24 -        unfolding dot_rsub[symmetric] by auto  }
    1.25 -    ultimately have "eventually (\<lambda>x. \<bar>a \<bullet> f x - a \<bullet> l\<bar> < e) net"
    1.26 -      by (auto elim: eventually_rev_mono)
    1.27 -  }
    1.28 -  thus ?thesis unfolding tendsto_iff
    1.29 -    by (auto simp add: dist_vec1)
    1.30 -qed
    1.31 -
    1.32 -lemma continuous_at_vec1_dot:
    1.33 +lemma Lim_dot: fixes f :: "real^'m \<Rightarrow> real^'n::finite"
    1.34 +  assumes "(f ---> l) net"  shows "((\<lambda>y. a \<bullet> (f y)) ---> a \<bullet> l) net"
    1.35 +  unfolding dot_def by (intro tendsto_intros assms)
    1.36 +
    1.37 +lemma continuous_at_dot:
    1.38    fixes x :: "real ^ _"
    1.39 -  shows "continuous (at x) (vec1 o (\<lambda>y. a \<bullet> y))"
    1.40 +  shows "continuous (at x) (\<lambda>y. a \<bullet> y)"
    1.41  proof-
    1.42    have "((\<lambda>x. x) ---> x) (at x)" unfolding Lim_at by auto
    1.43 -  thus ?thesis unfolding continuous_at and o_def using Lim_vec1_dot[of "\<lambda>x. x" x "at x" a] by auto
    1.44 -qed
    1.45 -
    1.46 -lemma continuous_on_vec1_dot:
    1.47 +  thus ?thesis unfolding continuous_at and o_def using Lim_dot[of "\<lambda>x. x" x "at x" a] by auto
    1.48 +qed
    1.49 +
    1.50 +lemma continuous_on_dot:
    1.51    fixes s :: "(real ^ _) set"
    1.52 -  shows "continuous_on s (vec1 o (\<lambda>y. a \<bullet> y)) "
    1.53 -  using continuous_at_imp_continuous_on[of s "vec1 o (\<lambda>y. a \<bullet> y)"]
    1.54 -  using continuous_at_vec1_dot
    1.55 +  shows "continuous_on s (\<lambda>y. a \<bullet> y)"
    1.56 +  using continuous_at_imp_continuous_on[of s "\<lambda>y. a \<bullet> y"]
    1.57 +  using continuous_at_dot
    1.58    by auto
    1.59  
    1.60  lemma closed_halfspace_le: fixes a::"real^'n::finite"
    1.61    shows "closed {x. a \<bullet> x \<le> b}"
    1.62  proof-
    1.63 -  have *:"{x \<in> UNIV. (vec1 \<circ> op \<bullet> a) x \<in> vec1 ` {r. \<exists>x. a \<bullet> x = r \<and> r \<le> b}} = {x. a \<bullet> x \<le> b}" by auto
    1.64 -  let ?T = "{x::real^1. (\<forall>i. x$i \<le> (vec1 b)$i)}"
    1.65 -  have "closed ?T" using closed_interval_left[of "vec1 b"] by simp
    1.66 -  moreover have "vec1 ` {r. \<exists>x. a \<bullet> x = r \<and> r \<le> b} = range (vec1 \<circ> op \<bullet> a) \<inter> ?T" unfolding all_1
    1.67 +  have *:"{x \<in> UNIV. (op \<bullet> a) x \<in> {r. \<exists>x. a \<bullet> x = r \<and> r \<le> b}} = {x. a \<bullet> x \<le> b}" by auto
    1.68 +  let ?T = "{..b}"
    1.69 +  have "closed ?T" by (rule closed_real_atMost)
    1.70 +  moreover have "{r. \<exists>x. a \<bullet> x = r \<and> r \<le> b} = range (op \<bullet> a) \<inter> ?T"
    1.71      unfolding image_def by auto
    1.72 -  ultimately have "\<exists>T. closed T \<and> vec1 ` {r. \<exists>x. a \<bullet> x = r \<and> r \<le> b} = range (vec1 \<circ> op \<bullet> a) \<inter> T" by auto
    1.73 -  hence "closedin euclidean {x \<in> UNIV. (vec1 \<circ> op \<bullet> a) x \<in> vec1 ` {r. \<exists>x. a \<bullet> x = r \<and> r \<le> b}}"
    1.74 -    using continuous_on_vec1_dot[of UNIV a, unfolded continuous_on_closed subtopology_UNIV] unfolding closedin_closed
    1.75 -    by (auto elim!: allE[where x="vec1 ` {r. (\<exists>x. a \<bullet> x = r \<and> r \<le> b)}"])
    1.76 +  ultimately have "\<exists>T. closed T \<and> {r. \<exists>x. a \<bullet> x = r \<and> r \<le> b} = range (op \<bullet> a) \<inter> T" by fast
    1.77 +  hence "closedin euclidean {x \<in> UNIV. (op \<bullet> a) x \<in> {r. \<exists>x. a \<bullet> x = r \<and> r \<le> b}}"
    1.78 +    using continuous_on_dot[of UNIV a, unfolded continuous_on_closed subtopology_UNIV] unfolding closedin_closed
    1.79 +    by (fast elim!: allE[where x="{r. (\<exists>x. a \<bullet> x = r \<and> r \<le> b)}"])
    1.80    thus ?thesis unfolding closed_closedin[THEN sym] and * by auto
    1.81  qed
    1.82