src/HOL/Library/Glbs.thy
changeset 51342 763c6872bd10
parent 46509 c4b2ec379fdd
     1.1 --- a/src/HOL/Library/Glbs.thy	Tue Mar 05 15:43:12 2013 +0100
     1.2 +++ b/src/HOL/Library/Glbs.thy	Tue Mar 05 15:43:13 2013 +0100
     1.3 @@ -70,4 +70,10 @@
     1.4  lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
     1.5    unfolding lbs_def isGlb_def by (rule greatestPD2)
     1.6  
     1.7 +lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
     1.8 +  apply (frule isGlb_isLb)
     1.9 +  apply (frule_tac x = y in isGlb_isLb)
    1.10 +  apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
    1.11 +  done
    1.12 +
    1.13  end