generalized isGlb_unique
authorhoelzl
Tue Mar 05 15:43:13 2013 +0100 (2013-03-05)
changeset 51342763c6872bd10
parent 51341 8c10293e7ea7
child 51343 b61b32f62c78
generalized isGlb_unique
src/HOL/Library/Glbs.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     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
     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:12 2013 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:13 2013 +0100
     2.3 @@ -28,12 +28,7 @@
     2.4  lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s o r) ----> l"
     2.5    by (rule LIMSEQ_subseq_LIMSEQ)
     2.6  
     2.7 -(* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
     2.8 -lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
     2.9 -  apply (frule isGlb_isLb)
    2.10 -  apply (frule_tac x = y in isGlb_isLb)
    2.11 -  apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
    2.12 -  done
    2.13 +lemmas real_isGlb_unique = isGlb_unique[where 'a=real]
    2.14  
    2.15  lemma countable_PiE: 
    2.16    "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"