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.5  
     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.9  
    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.13  
    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.17  
    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.22  
    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.27  
    1.28  text {* Openness of halfspaces. *}
    1.29  
    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.33  
    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.37  
    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.42  
    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.47  
    1.48  text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
    1.49  
    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.57  
    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.65  
    1.66  lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)"
    1.67    by (auto intro!: continuous_open_vimage)