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"
```