src/HOL/Hahn_Banach/Hahn_Banach.thy
 changeset 61543 de44d4fa5ef0 parent 61540 f92bf6674699 child 61583 c2b7033fa0ba
equal inserted replaced
61542:b3eb789616c3 61543:de44d4fa5ef0
`    20 text \<open>`
`    20 text \<open>`
`    21   Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm`
`    21   Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm`
`    22   on \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded`
`    22   on \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded`
`    23   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`
`    23   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`
`    24   form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded`
`    24   form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded`
`    25   by \<open>p\<close>. \<close>`
`    25   by \<open>p\<close>.`
`       `
`    26 \<close>`
`    26 `
`    27 `
`    27 paragraph \<open>Proof Sketch.\<close>`
`    28 paragraph \<open>Proof Sketch.\<close>`
`    28 text \<open>`
`    29 text \<open>`
`    29   \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces`
`    30   \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces`
`    30   of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.`
`    31   of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.`