src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 44250 9133bc634d9c parent 44233 aa74ce315bae child 44252 10362a07eb7c
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 17 18:05:31 2011 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 17 09:59:10 2011 -0700
1.3 @@ -4882,56 +4882,28 @@
1.4
1.5  (* Moved interval_open_subset_closed a bit upwards *)
1.6
1.7 -lemma open_interval_lemma: fixes x :: "real" shows
1.8 - "a < x \<Longrightarrow> x < b ==> (\<exists>d>0. \<forall>x'. abs(x' - x) < d --> a < x' \<and> x' < b)"
1.9 -  by(rule_tac x="min (x - a) (b - x)" in exI, auto)
1.10 -
1.11 -lemma open_interval[intro]: fixes a :: "'a::ordered_euclidean_space" shows "open {a<..<b}"
1.12 +lemma open_interval[intro]:
1.13 +  fixes a b :: "'a::ordered_euclidean_space" shows "open {a<..<b}"
1.14  proof-
1.15 -  { fix x assume x:"x\<in>{a<..<b}"
1.16 -    { fix i assume "i<DIM('a)"
1.17 -      hence "\<exists>d>0. \<forall>x'. abs (x' - (x\$\$i)) < d \<longrightarrow> a\$\$i < x' \<and> x' < b\$\$i"
1.18 -        using x[unfolded mem_interval, THEN spec[where x=i]]
1.19 -        using open_interval_lemma[of "a\$\$i" "x\$\$i" "b\$\$i"] by auto  }
1.20 -    hence "\<forall>i\<in>{..<DIM('a)}. \<exists>d>0. \<forall>x'. abs (x' - (x\$\$i)) < d \<longrightarrow> a\$\$i < x' \<and> x' < b\$\$i" by auto
1.21 -    from bchoice[OF this] guess d .. note d=this
1.22 -    let ?d = "Min (d ` {..<DIM('a)})"
1.23 -    have **:"finite (d ` {..<DIM('a)})" "d ` {..<DIM('a)} \<noteq> {}" by auto
1.24 -    have "?d>0" using Min_gr_iff[OF **] using d by auto
1.25 -    moreover
1.26 -    { fix x' assume as:"dist x' x < ?d"
1.27 -      { fix i assume i:"i<DIM('a)"
1.28 -        hence "\<bar>x'\$\$i - x \$\$ i\<bar> < d i"
1.29 -          using norm_bound_component_lt[OF as[unfolded dist_norm], of i]
1.30 -          unfolding euclidean_simps Min_gr_iff[OF **] by auto
1.31 -        hence "a \$\$ i < x' \$\$ i" "x' \$\$ i < b \$\$ i" using i and d[THEN bspec[where x=i]] by auto  }
1.32 -      hence "a < x' \<and> x' < b" apply(subst(2) eucl_less,subst(1) eucl_less) by auto  }
1.33 -    ultimately have "\<exists>e>0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a<..<b}" by auto
1.34 -  }
1.35 -  thus ?thesis unfolding open_dist using open_interval_lemma by auto
1.36 -qed
1.37 -
1.38 -lemma closed_interval[intro]: fixes a :: "'a::ordered_euclidean_space" shows "closed {a .. b}"
1.39 +  have "open (\<Inter>i<DIM('a). (\<lambda>x. x\$\$i) -` {a\$\$i<..<b\$\$i})"
1.40 +    by (intro open_INT finite_lessThan ballI continuous_open_vimage allI
1.41 +      linear_continuous_at bounded_linear_euclidean_component
1.42 +      open_real_greaterThanLessThan)
1.43 +  also have "(\<Inter>i<DIM('a). (\<lambda>x. x\$\$i) -` {a\$\$i<..<b\$\$i}) = {a<..<b}"
1.44 +    by (auto simp add: eucl_less [where 'a='a])
1.45 +  finally show "open {a<..<b}" .
1.46 +qed
1.47 +
1.48 +lemma closed_interval[intro]:
1.49 +  fixes a b :: "'a::ordered_euclidean_space" shows "closed {a .. b}"
1.50  proof-
1.51 -  { fix x i assume i:"i<DIM('a)"
1.52 -    assume as:"\<forall>e>0. \<exists>x'\<in>{a..b}. x' \<noteq> x \<and> dist x' x < e"(* and xab:"a\$\$i > x\$\$i \<or> b\$\$i < x\$\$i"*)
1.53 -    { assume xa:"a\$\$i > x\$\$i"
1.54 -      with as obtain y where y:"y\<in>{a..b}" "y \<noteq> x" "dist y x < a\$\$i - x\$\$i" by(erule_tac x="a\$\$i - x\$\$i" in allE)auto
1.55 -      hence False unfolding mem_interval and dist_norm
1.56 -        using component_le_norm[of "y-x" i, unfolded euclidean_simps] and xa using i
1.57 -        by(auto elim!: allE[where x=i])
1.58 -    } hence "a\$\$i \<le> x\$\$i" by(rule ccontr)auto
1.59 -    moreover
1.60 -    { assume xb:"b\$\$i < x\$\$i"
1.61 -      with as obtain y where y:"y\<in>{a..b}" "y \<noteq> x" "dist y x < x\$\$i - b\$\$i"
1.62 -        by(erule_tac x="x\$\$i - b\$\$i" in allE)auto
1.63 -      hence False unfolding mem_interval and dist_norm
1.64 -        using component_le_norm[of "y-x" i, unfolded euclidean_simps] and xb using i
1.65 -        by(auto elim!: allE[where x=i])
1.66 -    } hence "x\$\$i \<le> b\$\$i" by(rule ccontr)auto
1.67 -    ultimately
1.68 -    have "a \$\$ i \<le> x \$\$ i \<and> x \$\$ i \<le> b \$\$ i" by auto }
1.69 -  thus ?thesis unfolding closed_limpt islimpt_approachable mem_interval by auto
1.70 +  have "closed (\<Inter>i<DIM('a). (\<lambda>x. x\$\$i) -` {a\$\$i .. b\$\$i})"
1.71 +    by (intro closed_INT ballI continuous_closed_vimage allI
1.72 +      linear_continuous_at bounded_linear_euclidean_component
1.73 +      closed_real_atLeastAtMost)
1.74 +  also have "(\<Inter>i<DIM('a). (\<lambda>x. x\$\$i) -` {a\$\$i .. b\$\$i}) = {a .. b}"
1.75 +    by (auto simp add: eucl_le [where 'a='a])
1.76 +  finally show "closed {a .. b}" .
1.77  qed
1.78
1.79  lemma interior_closed_interval[intro]: fixes a :: "'a::ordered_euclidean_space" shows
```