src/HOL/Complete_Lattice.thy
 changeset 43740 3316e6831801 parent 43739 4529a3c56609 child 43741 fac11b64713c
```     1.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 10 14:14:19 2011 +0200
1.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 14:26:07 2011 +0200
1.3 @@ -349,14 +349,24 @@
1.4    by (unfold Inter_eq) blast
1.5
1.6  lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
1.7 -  by blast
1.8 +  by (fact Inf_lower)
1.9 +
1.10 +lemma (in complete_lattice) Inf_less_eq:
1.11 +  assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
1.12 +    and "A \<noteq> {}"
1.13 +  shows "\<Sqinter>A \<le> u"
1.14 +proof -
1.15 +  from `A \<noteq> {}` obtain v where "v \<in> A" by blast
1.16 +  moreover with assms have "v \<sqsubseteq> u" by blast
1.17 +  ultimately show ?thesis by (rule Inf_lower2)
1.18 +qed
1.19
1.20  lemma Inter_subset:
1.21    "[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
1.22 -  by blast
1.23 +  by (fact Inf_less_eq)
1.24
1.25  lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
1.26 -  by (iprover intro: InterI subsetI dest: subsetD)
1.27 +  by (fact Inf_greatest)
1.28
1.29  lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
1.30    by (fact Inf_binary [symmetric])
```