src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 44233 aa74ce315bae parent 44219 f738e3200e24 child 44250 9133bc634d9c
1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 16 13:07:52 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 16 09:31:23 2011 -0700
1.3 @@ -5229,37 +5229,37 @@
1.4    unfolding continuous_on by (rule ballI) (intro tendsto_intros)
1.6  lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
1.7 -  by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
1.8 +  by (simp add: closed_Collect_le)
1.10  lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
1.11 -  by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
1.12 +  by (simp add: closed_Collect_le)
1.14  lemma closed_hyperplane: "closed {x. inner a x = b}"
1.15 -  by (intro closed_Collect_eq inner.isCont isCont_const isCont_ident)
1.16 +  by (simp add: closed_Collect_eq)
1.18  lemma closed_halfspace_component_le:
1.19    shows "closed {x::'a::euclidean_space. x\$\$i \<le> a}"
1.20 -  by (intro closed_Collect_le euclidean_component.isCont isCont_const)
1.21 +  by (simp add: closed_Collect_le)
1.23  lemma closed_halfspace_component_ge:
1.24    shows "closed {x::'a::euclidean_space. x\$\$i \<ge> a}"
1.25 -  by (intro closed_Collect_le euclidean_component.isCont isCont_const)
1.26 +  by (simp add: closed_Collect_le)
1.28  text {* Openness of halfspaces. *}
1.30  lemma open_halfspace_lt: "open {x. inner a x < b}"
1.31 -  by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
1.32 +  by (simp add: open_Collect_less)
1.34  lemma open_halfspace_gt: "open {x. inner a x > b}"
1.35 -  by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
1.36 +  by (simp add: open_Collect_less)
1.38  lemma open_halfspace_component_lt:
1.39    shows "open {x::'a::euclidean_space. x\$\$i < a}"
1.40 -  by (intro open_Collect_less euclidean_component.isCont isCont_const)
1.41 +  by (simp add: open_Collect_less)
1.43  lemma open_halfspace_component_gt:
1.44    shows "open {x::'a::euclidean_space. x\$\$i > a}"
1.45 -  by (intro open_Collect_less euclidean_component.isCont isCont_const)
1.46 +  by (simp add: open_Collect_less)
1.48  text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
1.50 @@ -5297,15 +5297,13 @@
1.51    fixes a :: "'a\<Colon>ordered_euclidean_space"
1.52    shows "closed {.. a}"
1.53    unfolding eucl_atMost_eq_halfspaces
1.54 -  by (intro closed_INT ballI closed_Collect_le
1.55 -    euclidean_component.isCont isCont_const)
1.56 +  by (simp add: closed_INT closed_Collect_le)
1.58  lemma closed_eucl_atLeast[simp, intro]:
1.59    fixes a :: "'a\<Colon>ordered_euclidean_space"
1.60    shows "closed {a ..}"
1.61    unfolding eucl_atLeast_eq_halfspaces
1.62 -  by (intro closed_INT ballI closed_Collect_le
1.63 -    euclidean_component.isCont isCont_const)
1.64 +  by (simp add: closed_INT closed_Collect_le)
1.66  lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x \$\$ i) -` S)"
1.67    by (auto intro!: continuous_open_vimage)