summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Hahn_Banach/Hahn_Banach.thy

changeset 61543 | de44d4fa5ef0 |

parent 61540 | f92bf6674699 |

child 61583 | c2b7033fa0ba |

--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy Mon Nov 02 14:09:14 2015 +0100 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy Mon Nov 02 16:02:32 2015 +0100 @@ -22,7 +22,8 @@ on \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded by \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded - by \<open>p\<close>. \<close> + by \<open>p\<close>. +\<close> paragraph \<open>Proof Sketch.\<close> text \<open>