src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44207 ea99698c2070
parent 44170 510ac30f44c0
child 44210 eba74571833b
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 14 10:47:47 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Aug 14 11:44:12 2011 -0700
     1.3 @@ -432,9 +432,8 @@
     1.4  
     1.5  subsection{* Limit points *}
     1.6  
     1.7 -definition
     1.8 -  islimpt:: "'a::topological_space \<Rightarrow> 'a set \<Rightarrow> bool"
     1.9 -    (infixr "islimpt" 60) where
    1.10 +definition (in topological_space)
    1.11 +  islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) where
    1.12    "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
    1.13  
    1.14  lemma islimptI:
    1.15 @@ -469,8 +468,8 @@
    1.16    using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
    1.17    by metis 
    1.18  
    1.19 -class perfect_space =
    1.20 -  assumes islimpt_UNIV [simp, intro]: "(x::'a::topological_space) islimpt UNIV"
    1.21 +class perfect_space = topological_space +
    1.22 +  assumes islimpt_UNIV [simp, intro]: "x islimpt UNIV"
    1.23  
    1.24  lemma perfect_choose_dist:
    1.25    fixes x :: "'a::{perfect_space, metric_space}"
    1.26 @@ -1881,8 +1880,8 @@
    1.27  subsection{* Boundedness. *}
    1.28  
    1.29    (* FIXME: This has to be unified with BSEQ!! *)
    1.30 -definition
    1.31 -  bounded :: "'a::metric_space set \<Rightarrow> bool" where
    1.32 +definition (in metric_space)
    1.33 +  bounded :: "'a set \<Rightarrow> bool" where
    1.34    "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
    1.35  
    1.36  lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
    1.37 @@ -2110,7 +2109,7 @@
    1.38    Heine-Borel property if every closed and bounded subset is compact.
    1.39  *}
    1.40  
    1.41 -class heine_borel =
    1.42 +class heine_borel = metric_space +
    1.43    assumes bounded_imp_convergent_subsequence:
    1.44      "bounded s \<Longrightarrow> \<forall>n. f n \<in> s
    1.45        \<Longrightarrow> \<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"