src/HOL/Complete_Lattice.thy
 changeset 43756 15ea1a07a8cf parent 43755 5e4a595e63fc child 43801 097732301fc0
```     1.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 10 22:17:33 2011 +0200
1.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 22:42:53 2011 +0200
1.3 @@ -386,18 +386,25 @@
1.4  lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
1.5    by (fact Inf_inter_less)
1.6
1.7 -(*lemma (in complete_lattice) Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"*)
1.8 +lemma (in complete_lattice) Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
1.9 +  by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
1.10
1.11  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
1.12 -  by blast
1.13 +  by (fact Inf_union_distrib)
1.14 +
1.15 +(*lemma (in complete_lattice) Inf_top_conv [no_atp]:
1.16 +  "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"*)
1.17
1.18  lemma Inter_UNIV_conv [simp,no_atp]:
1.19    "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
1.20    "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
1.21    by blast+
1.22
1.23 +lemma (in complete_lattice) Inf_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
1.24 +  by (auto intro: Inf_greatest Inf_lower)
1.25 +
1.26  lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B"
1.27 -  by blast
1.28 +  by (fact Inf_anti_mono)
1.29
1.30
1.31  subsection {* Intersections of families *}
```