| changeset 27193 | 740159cfbf0e |
| parent 23393 | 31781b2de73d |
| child 35317 | d57da4abb47d |
| 27192:005d4b953fdc | 27193:740159cfbf0e |
|---|---|
5 |
5 |
6 header {* Bounds *} |
6 header {* Bounds *} |
7 |
7 |
8 theory Bounds imports Orders begin |
8 theory Bounds imports Orders begin |
9 |
9 |
10 hide const inf sup |
10 hide (open) const inf sup |
11 |
11 |
12 subsection {* Infimum and supremum *} |
12 subsection {* Infimum and supremum *} |
13 |
13 |
14 text {* |
14 text {* |
15 Given a partial order, we define infimum (greatest lower bound) and |
15 Given a partial order, we define infimum (greatest lower bound) and |