equal
deleted
inserted
replaced
3 Author: Gertrud Bauer, TU Munich |
3 Author: Gertrud Bauer, TU Munich |
4 *) |
4 *) |
5 |
5 |
6 header {* An order on functions *} |
6 header {* An order on functions *} |
7 |
7 |
8 theory FunctionOrder = Subspace + Linearform: |
8 theory FunctionOrder imports Subspace Linearform begin |
9 |
9 |
10 subsection {* The graph of a function *} |
10 subsection {* The graph of a function *} |
11 |
11 |
12 text {* |
12 text {* |
13 We define the \emph{graph} of a (real) function @{text f} with |
13 We define the \emph{graph} of a (real) function @{text f} with |