equal
deleted
inserted
replaced
8 imports Hahn_Banach_Lemmas |
8 imports Hahn_Banach_Lemmas |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text {* |
12 We present the proof of two different versions of the Hahn-Banach |
12 We present the proof of two different versions of the Hahn-Banach |
13 Theorem, closely following \cite[\S36]{Heuser:1986}. |
13 Theorem, closely following @{cite \<open>\S36\<close> "Heuser:1986"}. |
14 *} |
14 *} |
15 |
15 |
16 subsection {* The Hahn-Banach Theorem for vector spaces *} |
16 subsection {* The Hahn-Banach Theorem for vector spaces *} |
17 |
17 |
18 text {* |
18 text {* |