author hoelzl Tue, 05 Mar 2013 15:43:13 +0100 changeset 51342 763c6872bd10 parent 51341 8c10293e7ea7 child 51343 b61b32f62c78
generalized isGlb_unique
```--- a/src/HOL/Library/Glbs.thy	Tue Mar 05 15:43:12 2013 +0100
+++ b/src/HOL/Library/Glbs.thy	Tue Mar 05 15:43:13 2013 +0100
@@ -70,4 +70,10 @@
lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
unfolding lbs_def isGlb_def by (rule greatestPD2)

+lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
+  apply (frule isGlb_isLb)
+  apply (frule_tac x = y in isGlb_isLb)
+  apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
+  done
+
end```
```--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:12 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:13 2013 +0100
@@ -28,12 +28,7 @@
lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s o r) ----> l"
by (rule LIMSEQ_subseq_LIMSEQ)

-(* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
-lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
-  apply (frule isGlb_isLb)
-  apply (frule_tac x = y in isGlb_isLb)
-  apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
-  done
+lemmas real_isGlb_unique = isGlb_unique[where 'a=real]

lemma countable_PiE:
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"```