src/HOL/Library/Option_ord.thy
 changeset 69313 b021008c5397 parent 68980 5717fbc55521 child 69661 a03a63b81f44
```     1.1 --- a/src/HOL/Library/Option_ord.thy	Sun Nov 18 09:51:41 2018 +0100
1.2 +++ b/src/HOL/Library/Option_ord.thy	Sun Nov 18 18:07:51 2018 +0000
1.3 @@ -283,7 +283,8 @@
1.4    "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
1.5    using Some_Sup [of "f ` A"] by (simp add: comp_def)
1.6
1.7 -lemma option_Inf_Sup: "INFIMUM (A::('a::complete_distrib_lattice option) set set) Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
1.8 +lemma option_Inf_Sup: "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
1.9 +  for A :: "('a::complete_distrib_lattice option) set set"
1.10  proof (cases "{} \<in> A")
1.11    case True
1.12    then show ?thesis
1.13 @@ -438,8 +439,8 @@
1.14      also have "... = Some (\<Squnion>x\<in>{f ` {the ` (y - {None}) |y. y \<in> A} |f. \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y}. \<Sqinter>x) "