changeset 22426 | 1c38ca2496c4 |
parent 21404 | eb85850d3eb7 |
child 22457 | 1ed5b9c3ae67 |
22425:c252770ae2d0 | 22426:1c38ca2496c4 |
---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Bounds *} |
6 header {* Bounds *} |
7 |
7 |
8 theory Bounds imports Orders begin |
8 theory Bounds imports Orders begin |
9 |
|
10 hide const inf sup |
|
11 hide const inf sup |
|
9 |
12 |
10 subsection {* Infimum and supremum *} |
13 subsection {* Infimum and supremum *} |
11 |
14 |
12 text {* |
15 text {* |
13 Given a partial order, we define infimum (greatest lower bound) and |
16 Given a partial order, we define infimum (greatest lower bound) and |