equal
deleted
inserted
replaced
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 seminorm 
21 Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a seminorm 
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 normpreserving, i.e. \<open>h\<close> is also bounded 
24 form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is normpreserving, 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 normpreserving extensions of \<open>f\<close> to subspaces 
30 \<^enum> Define \<open>M\<close> as the set of normpreserving 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. 