src/HOL/Topological_Spaces.thy
changeset 56020 f92479477c52
parent 55945 e96383acecf9
child 56166 9a241bc276cd
     1.1 --- a/src/HOL/Topological_Spaces.thy	Mon Mar 10 17:14:57 2014 +0100
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Mar 10 20:04:40 2014 +0100
     1.3 @@ -1193,26 +1193,25 @@
     1.4          The use of disjunction here complicates proofs considerably.
     1.5          One alternative is to add a Boolean argument to indicate the direction.
     1.6          Another is to develop the notions of increasing and decreasing first.*}
     1.7 -  "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
     1.8 -
     1.9 -definition
    1.10 -  incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
    1.11 -    --{*Increasing sequence*}
    1.12 -  "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X m \<le> X n)"
    1.13 -
    1.14 -definition
    1.15 -  decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
    1.16 -    --{*Decreasing sequence*}
    1.17 -  "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
    1.18 +  "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) \<or> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
    1.19 +
    1.20 +abbreviation incseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
    1.21 +  "incseq X \<equiv> mono X"
    1.22 +
    1.23 +lemma incseq_def: "incseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<ge> X m)"
    1.24 +  unfolding mono_def ..
    1.25 +
    1.26 +abbreviation decseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
    1.27 +  "decseq X \<equiv> antimono X"
    1.28 +
    1.29 +lemma decseq_def: "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
    1.30 +  unfolding antimono_def ..
    1.31  
    1.32  definition
    1.33    subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" where
    1.34      --{*Definition of subsequence*}
    1.35    "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
    1.36  
    1.37 -lemma incseq_mono: "mono f \<longleftrightarrow> incseq f"
    1.38 -  unfolding mono_def incseq_def by auto
    1.39 -
    1.40  lemma incseq_SucI:
    1.41    "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
    1.42    using lift_Suc_mono_le[of X]