equal
deleted
inserted
replaced
3 Author: Gertrud Bauer, TU Munich |
3 Author: Gertrud Bauer, TU Munich |
4 *) |
4 *) |
5 |
5 |
6 header {* Normed vector spaces *} |
6 header {* Normed vector spaces *} |
7 |
7 |
8 theory NormedSpace = Subspace: |
8 theory NormedSpace imports Subspace begin |
9 |
9 |
10 subsection {* Quasinorms *} |
10 subsection {* Quasinorms *} |
11 |
11 |
12 text {* |
12 text {* |
13 A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space |
13 A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space |