src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44522 2f7e9d890efe
parent 44519 ea85d78a994e
child 44530 adb18b07b341
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 25 11:57:42 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 25 12:43:55 2011 -0700
     1.3 @@ -588,11 +588,14 @@
     1.4  lemma interior_empty [simp]: "interior {} = {}"
     1.5    using open_empty by (rule interior_open)
     1.6  
     1.7 +lemma interior_UNIV [simp]: "interior UNIV = UNIV"
     1.8 +  using open_UNIV by (rule interior_open)
     1.9 +
    1.10  lemma interior_interior [simp]: "interior (interior S) = interior S"
    1.11    using open_interior by (rule interior_open)
    1.12  
    1.13 -lemma subset_interior: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
    1.14 -  by (auto simp add: interior_def) (* TODO: rename to interior_mono *)
    1.15 +lemma interior_mono: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
    1.16 +  by (auto simp add: interior_def)
    1.17  
    1.18  lemma interior_unique:
    1.19    assumes "T \<subseteq> S" and "open T"
    1.20 @@ -601,7 +604,7 @@
    1.21    by (intro equalityI assms interior_subset open_interior interior_maximal)
    1.22  
    1.23  lemma interior_inter [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
    1.24 -  by (intro equalityI Int_mono Int_greatest subset_interior Int_lower1
    1.25 +  by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1
    1.26      Int_lower2 interior_maximal interior_subset open_Int open_interior)
    1.27  
    1.28  lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
    1.29 @@ -623,7 +626,7 @@
    1.30    shows "interior (S \<union> T) = interior S"
    1.31  proof
    1.32    show "interior S \<subseteq> interior (S \<union> T)"
    1.33 -    by (rule subset_interior, rule Un_upper1)
    1.34 +    by (rule interior_mono, rule Un_upper1)
    1.35  next
    1.36    show "interior (S \<union> T) \<subseteq> interior S"
    1.37    proof
    1.38 @@ -689,7 +692,7 @@
    1.39  lemma closure_closure [simp]: "closure (closure S) = closure S"
    1.40    unfolding closure_hull by (rule hull_hull)
    1.41  
    1.42 -lemma subset_closure: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
    1.43 +lemma closure_mono: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
    1.44    unfolding closure_hull by (rule hull_mono)
    1.45  
    1.46  lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
    1.47 @@ -704,7 +707,7 @@
    1.48  lemma closure_empty [simp]: "closure {} = {}"
    1.49    using closed_empty by (rule closure_closed)
    1.50  
    1.51 -lemma closure_univ [simp]: "closure UNIV = UNIV"
    1.52 +lemma closure_UNIV [simp]: "closure UNIV = UNIV"
    1.53    using closed_UNIV by (rule closure_closed)
    1.54  
    1.55  lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
    1.56 @@ -5990,19 +5993,4 @@
    1.57  
    1.58  declare tendsto_const [intro] (* FIXME: move *)
    1.59  
    1.60 -text {* Legacy theorem names *}
    1.61 -
    1.62 -lemmas Lim_ident_at = LIM_ident
    1.63 -lemmas Lim_const = tendsto_const
    1.64 -lemmas Lim_cmul = tendsto_scaleR [OF tendsto_const]
    1.65 -lemmas Lim_neg = tendsto_minus
    1.66 -lemmas Lim_add = tendsto_add
    1.67 -lemmas Lim_sub = tendsto_diff
    1.68 -lemmas Lim_mul = tendsto_scaleR
    1.69 -lemmas Lim_vmul = tendsto_scaleR [OF _ tendsto_const]
    1.70 -lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
    1.71 -lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
    1.72 -lemmas Lim_component = tendsto_euclidean_component
    1.73 -lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
    1.74 -
    1.75  end