src/HOL/Topological_Spaces.thy
changeset 51775 408d937c9486
parent 51774 916271d52466
child 52265 bb907eba5902
     1.1 --- a/src/HOL/Topological_Spaces.thy	Thu Apr 25 10:35:56 2013 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Apr 25 11:59:21 2013 +0200
     1.3 @@ -2079,7 +2079,7 @@
     1.4  
     1.5  section {* Connectedness *}
     1.6  
     1.7 -class connected_linorder_topology = linorder_topology + conditionally_complete_linorder + inner_dense_linorder
     1.8 +class linear_continuum_topology = linorder_topology + linear_continuum
     1.9  begin
    1.10  
    1.11  lemma Inf_notin_open:
    1.12 @@ -2110,8 +2110,17 @@
    1.13  
    1.14  end
    1.15  
    1.16 +instance linear_continuum_topology \<subseteq> perfect_space
    1.17 +proof
    1.18 +  fix x :: 'a
    1.19 +  from ex_gt_or_lt [of x] guess y ..
    1.20 +  with Inf_notin_open[of "{x}" y] Sup_notin_open[of "{x}" y]
    1.21 +  show "\<not> open {x}"
    1.22 +    by auto
    1.23 +qed
    1.24 +
    1.25  lemma connectedI_interval:
    1.26 -  fixes U :: "'a :: connected_linorder_topology set"
    1.27 +  fixes U :: "'a :: linear_continuum_topology set"
    1.28    assumes *: "\<And>x y z. x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> U"
    1.29    shows "connected U"
    1.30  proof (rule connectedI)
    1.31 @@ -2154,35 +2163,35 @@
    1.32  qed
    1.33  
    1.34  lemma connected_iff_interval:
    1.35 -  fixes U :: "'a :: connected_linorder_topology set"
    1.36 +  fixes U :: "'a :: linear_continuum_topology set"
    1.37    shows "connected U \<longleftrightarrow> (\<forall>x\<in>U. \<forall>y\<in>U. \<forall>z. x \<le> z \<longrightarrow> z \<le> y \<longrightarrow> z \<in> U)"
    1.38    by (auto intro: connectedI_interval dest: connectedD_interval)
    1.39  
    1.40 -lemma connected_UNIV[simp]: "connected (UNIV::'a::connected_linorder_topology set)"
    1.41 +lemma connected_UNIV[simp]: "connected (UNIV::'a::linear_continuum_topology set)"
    1.42    unfolding connected_iff_interval by auto
    1.43  
    1.44 -lemma connected_Ioi[simp]: "connected {a::'a::connected_linorder_topology <..}"
    1.45 +lemma connected_Ioi[simp]: "connected {a::'a::linear_continuum_topology <..}"
    1.46    unfolding connected_iff_interval by auto
    1.47  
    1.48 -lemma connected_Ici[simp]: "connected {a::'a::connected_linorder_topology ..}"
    1.49 +lemma connected_Ici[simp]: "connected {a::'a::linear_continuum_topology ..}"
    1.50    unfolding connected_iff_interval by auto
    1.51  
    1.52 -lemma connected_Iio[simp]: "connected {..< a::'a::connected_linorder_topology}"
    1.53 +lemma connected_Iio[simp]: "connected {..< a::'a::linear_continuum_topology}"
    1.54    unfolding connected_iff_interval by auto
    1.55  
    1.56 -lemma connected_Iic[simp]: "connected {.. a::'a::connected_linorder_topology}"
    1.57 +lemma connected_Iic[simp]: "connected {.. a::'a::linear_continuum_topology}"
    1.58    unfolding connected_iff_interval by auto
    1.59  
    1.60 -lemma connected_Ioo[simp]: "connected {a <..< b::'a::connected_linorder_topology}"
    1.61 +lemma connected_Ioo[simp]: "connected {a <..< b::'a::linear_continuum_topology}"
    1.62    unfolding connected_iff_interval by auto
    1.63  
    1.64 -lemma connected_Ioc[simp]: "connected {a <.. b::'a::connected_linorder_topology}"
    1.65 +lemma connected_Ioc[simp]: "connected {a <.. b::'a::linear_continuum_topology}"
    1.66    unfolding connected_iff_interval by auto
    1.67  
    1.68 -lemma connected_Ico[simp]: "connected {a ..< b::'a::connected_linorder_topology}"
    1.69 +lemma connected_Ico[simp]: "connected {a ..< b::'a::linear_continuum_topology}"
    1.70    unfolding connected_iff_interval by auto
    1.71  
    1.72 -lemma connected_Icc[simp]: "connected {a .. b::'a::connected_linorder_topology}"
    1.73 +lemma connected_Icc[simp]: "connected {a .. b::'a::linear_continuum_topology}"
    1.74    unfolding connected_iff_interval by auto
    1.75  
    1.76  lemma connected_contains_Ioo: 
    1.77 @@ -2193,7 +2202,7 @@
    1.78  subsection {* Intermediate Value Theorem *}
    1.79  
    1.80  lemma IVT':
    1.81 -  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
    1.82 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
    1.83    assumes y: "f a \<le> y" "y \<le> f b" "a \<le> b"
    1.84    assumes *: "continuous_on {a .. b} f"
    1.85    shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
    1.86 @@ -2206,7 +2215,7 @@
    1.87  qed
    1.88  
    1.89  lemma IVT2':
    1.90 -  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
    1.91 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
    1.92    assumes y: "f b \<le> y" "y \<le> f a" "a \<le> b"
    1.93    assumes *: "continuous_on {a .. b} f"
    1.94    shows "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
    1.95 @@ -2219,17 +2228,17 @@
    1.96  qed
    1.97  
    1.98  lemma IVT:
    1.99 -  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
   1.100 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   1.101    shows "f a \<le> y \<Longrightarrow> y \<le> f b \<Longrightarrow> a \<le> b \<Longrightarrow> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x) \<Longrightarrow> \<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
   1.102    by (rule IVT') (auto intro: continuous_at_imp_continuous_on)
   1.103  
   1.104  lemma IVT2:
   1.105 -  fixes f :: "'a :: connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
   1.106 +  fixes f :: "'a :: linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   1.107    shows "f b \<le> y \<Longrightarrow> y \<le> f a \<Longrightarrow> a \<le> b \<Longrightarrow> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x) \<Longrightarrow> \<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
   1.108    by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
   1.109  
   1.110  lemma continuous_inj_imp_mono:
   1.111 -  fixes f :: "'a::connected_linorder_topology \<Rightarrow> 'b :: linorder_topology"
   1.112 +  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
   1.113    assumes x: "a < x" "x < b"
   1.114    assumes cont: "continuous_on {a..b} f"
   1.115    assumes inj: "inj_on f {a..b}"