src/HOL/Conditionally_Complete_Lattices.thy
changeset 51775 408d937c9486
parent 51773 9328c6681f3c
child 52265 bb907eba5902
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Thu Apr 25 10:35:56 2013 +0200
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Thu Apr 25 11:59:21 2013 +0200
     1.3 @@ -246,6 +246,15 @@
     1.4  
     1.5  end
     1.6  
     1.7 +class linear_continuum = conditionally_complete_linorder + inner_dense_linorder +
     1.8 +  assumes UNIV_not_singleton: "\<exists>a b::'a. a \<noteq> b"
     1.9 +begin
    1.10 +
    1.11 +lemma ex_gt_or_lt: "\<exists>b. a < b \<or> b < a"
    1.12 +  by (metis UNIV_not_singleton neq_iff)
    1.13 +
    1.14 +end
    1.15 +
    1.16  lemma cSup_bounds:
    1.17    fixes S :: "'a :: conditionally_complete_lattice set"
    1.18    assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"