src/HOL/RealVector.thy
changeset 51481 ef949192e5d6
parent 51480 3793c3a11378
child 51518 6a56b7088a6a
     1.1 --- a/src/HOL/RealVector.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/RealVector.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -950,6 +950,8 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instance real :: linear_continuum_topology ..
     1.8 +
     1.9  lemma connectedI_interval:
    1.10    fixes U :: "'a :: linear_continuum_topology set"
    1.11    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.12 @@ -1068,6 +1070,27 @@
    1.13    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.14    by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
    1.15  
    1.16 -instance real :: linear_continuum_topology ..
    1.17 +lemma continuous_inj_imp_mono:
    1.18 +  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
    1.19 +  assumes x: "a < x" "x < b"
    1.20 +  assumes cont: "continuous_on {a..b} f"
    1.21 +  assumes inj: "inj_on f {a..b}"
    1.22 +  shows "(f a < f x \<and> f x < f b) \<or> (f b < f x \<and> f x < f a)"
    1.23 +proof -
    1.24 +  note I = inj_on_iff[OF inj]
    1.25 +  { assume "f x < f a" "f x < f b"
    1.26 +    then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f x < f s"
    1.27 +      using IVT'[of f x "min (f a) (f b)" b] IVT2'[of f x "min (f a) (f b)" a] x
    1.28 +      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
    1.29 +    with x I have False by auto }
    1.30 +  moreover
    1.31 +  { assume "f a < f x" "f b < f x"
    1.32 +    then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f s < f x"
    1.33 +      using IVT'[of f a "max (f a) (f b)" x] IVT2'[of f b "max (f a) (f b)" x] x
    1.34 +      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
    1.35 +    with x I have False by auto }
    1.36 +  ultimately show ?thesis
    1.37 +    using I[of a x] I[of x b] x less_trans[OF x] by (auto simp add: le_less less_imp_neq neq_iff)
    1.38 +qed
    1.39  
    1.40  end