equal
deleted
inserted
replaced
7 begin |
7 begin |
8 |
8 |
9 instantiation real :: Sup |
9 instantiation real :: Sup |
10 begin |
10 begin |
11 definition |
11 definition |
12 Sup_real_def [code del]: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)" |
12 Sup_real_def: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)" |
13 |
13 |
14 instance .. |
14 instance .. |
15 end |
15 end |
16 |
16 |
17 instantiation real :: Inf |
17 instantiation real :: Inf |
18 begin |
18 begin |
19 definition |
19 definition |
20 Inf_real_def [code del]: "Inf (X::real set) == - (Sup (uminus ` X))" |
20 Inf_real_def: "Inf (X::real set) == - (Sup (uminus ` X))" |
21 |
21 |
22 instance .. |
22 instance .. |
23 end |
23 end |
24 |
24 |
25 subsection{*Supremum of a set of reals*} |
25 subsection{*Supremum of a set of reals*} |