equal
deleted
inserted
replaced
1 (* Title: HOL/Lattice/CompleteLattice.thy |
1 (* Title: HOL/Lattice/CompleteLattice.thy |
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
2 Author: Markus Wenzel, TU Muenchen |
4 *) |
3 *) |
5 |
4 |
6 header {* Complete lattices *} |
5 header {* Complete lattices *} |
7 |
6 |
14 (infinitary) infimum of any set of elements. General supremum |
13 (infinitary) infimum of any set of elements. General supremum |
15 exists as well, as a consequence of the connection of infinitary |
14 exists as well, as a consequence of the connection of infinitary |
16 bounds (see \S\ref{sec:connect-bounds}). |
15 bounds (see \S\ref{sec:connect-bounds}). |
17 *} |
16 *} |
18 |
17 |
19 axclass complete_lattice \<subseteq> partial_order |
18 class complete_lattice = |
20 ex_Inf: "\<exists>inf. is_Inf A inf" |
19 assumes ex_Inf: "\<exists>inf. is_Inf A inf" |
21 |
20 |
22 theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup" |
21 theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup" |
23 proof - |
22 proof - |
24 from ex_Inf obtain sup where "is_Inf {b. \<forall>a\<in>A. a \<sqsubseteq> b} sup" by blast |
23 from ex_Inf obtain sup where "is_Inf {b. \<forall>a\<in>A. a \<sqsubseteq> b} sup" by blast |
25 then have "is_Sup A sup" by (rule Inf_Sup) |
24 then have "is_Sup A sup" by (rule Inf_Sup) |