| changeset 36176 | 3fe7e97ccca8 |
| parent 35317 | d57da4abb47d |
| child 58879 | 143c85e3cdb5 |
| 36175:5cec4ca719d1 | 36176:3fe7e97ccca8 |
|---|---|
4 |
4 |
5 header {* Bounds *} |
5 header {* Bounds *} |
6 |
6 |
7 theory Bounds imports Orders begin |
7 theory Bounds imports Orders begin |
8 |
8 |
9 hide (open) const inf sup |
9 hide_const (open) inf sup |
10 |
10 |
11 subsection {* Infimum and supremum *} |
11 subsection {* Infimum and supremum *} |
12 |
12 |
13 text {* |
13 text {* |
14 Given a partial order, we define infimum (greatest lower bound) and |
14 Given a partial order, we define infimum (greatest lower bound) and |