| changeset 16417 | 9bc16273c2d4 |
| parent 11265 | 4f2e6c87a57f |
| child 19736 | d8d0f8f51d69 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Bounds *} |
6 header {* Bounds *} |
7 |
7 |
8 theory Bounds = Orders: |
8 theory Bounds imports Orders begin |
9 |
9 |
10 subsection {* Infimum and supremum *} |
10 subsection {* Infimum and supremum *} |
11 |
11 |
12 text {* |
12 text {* |
13 Given a partial order, we define infimum (greatest lower bound) and |
13 Given a partial order, we define infimum (greatest lower bound) and |