| changeset 29043 | 409d1ca929b5 |
| parent 27612 | d3eb431db035 |
| child 29234 | 60f7fb56f8cd |
| 29042:d5a5888b8c54 | 29043:409d1ca929b5 |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Bounds *} |
6 header {* Bounds *} |
7 |
7 |
8 theory Bounds |
8 theory Bounds |
9 imports Main Real |
9 imports Main ContNotDenum |
10 begin |
10 begin |
11 |
11 |
12 locale lub = |
12 locale lub = |
13 fixes A and x |
13 fixes A and x |
14 assumes least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<le> b) \<Longrightarrow> x \<le> b" |
14 assumes least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<le> b) \<Longrightarrow> x \<le> b" |