equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 section \<open>Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\<close> |
6 section \<open>Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\<close> |
7 |
7 |
8 theory Lattices_Big |
8 theory Lattices_Big |
9 imports Option |
9 imports Groups_Big Option |
10 begin |
10 begin |
11 |
11 |
12 subsection \<open>Generic lattice operations over a set\<close> |
12 subsection \<open>Generic lattice operations over a set\<close> |
13 |
13 |
14 subsubsection \<open>Without neutral element\<close> |
14 subsubsection \<open>Without neutral element\<close> |