src/HOL/Lattices_Big.thy
changeset 59000 6eb0725503fc
parent 58889 5b7a9633cfa8
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Lattices_Big.thy	Thu Nov 13 14:40:06 2014 +0100
     1.2 +++ b/src/HOL/Lattices_Big.thy	Thu Nov 13 17:19:52 2014 +0100
     1.3 @@ -764,6 +764,18 @@
     1.4    } from this [of "{a. P a}"] assms show ?thesis by simp
     1.5  qed
     1.6  
     1.7 +lemma infinite_growing:
     1.8 +  assumes "X \<noteq> {}"
     1.9 +  assumes *: "\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>X. y > x"
    1.10 +  shows "\<not> finite X"
    1.11 +proof
    1.12 +  assume "finite X"
    1.13 +  with `X \<noteq> {}` have "Max X \<in> X" "\<forall>x\<in>X. x \<le> Max X"
    1.14 +    by auto
    1.15 +  with *[of "Max X"] show False
    1.16 +    by auto
    1.17 +qed
    1.18 +
    1.19  end
    1.20  
    1.21  context linordered_ab_semigroup_add