:: Hahn Banach Theorem
:: by Bogdan Nowak and Andrzej Trybulec
::
:: Received July 8, 1993
:: Copyright (c) 1993-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, PARTFUN1, FUNCT_1, TARSKI, RELAT_1,
SUPINF_1, XXREAL_0, ORDINAL1, ARYTM_3, ORDINAL2, XXREAL_2, RLVECT_1,
RLSUB_1, STRUCT_0, SUPINF_2, RLSUB_2, FINSEQ_4, MCART_1, RLVECT_3,
REAL_1, CARD_1, MSSUBFAM, UNIALG_1, COMPLEX1, FUNCOP_1, ARYTM_1,
ALGSTR_0, REALSET1, ZFMISC_1, NORMSP_1, HAHNBAN, NORMSP_0, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, COMPLEX1, STRUCT_0, ALGSTR_0, REAL_1, RELAT_1,
REALSET1, FUNCT_1, FUNCT_2, RLVECT_1, RLSUB_1, RLSUB_2, NORMSP_0,
NORMSP_1, SUPINF_1, PARTFUN1, FUNCOP_1, RLVECT_3, DOMAIN_1, XXREAL_2;
constructors BINOP_1, REAL_1, COMPLEX1, SUPINF_1, REALSET1, RFUNCT_3, RLSUB_2,
RLVECT_2, RLVECT_3, NORMSP_1, XXREAL_2, RELSET_1, XXREAL_1;
registrations SUBSET_1, RELSET_1, PARTFUN1, NUMBERS, XXREAL_0, XREAL_0,
MEMBERED, STRUCT_0, RLVECT_1, RLSUB_1, ALGSTR_0, FUNCT_2, FUNCT_1,
RELAT_1, ORDINAL1, XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Some Facts on Real Vector Spaces
reserve V for RealLinearSpace;
theorem :: HAHNBAN:1
for W1,W2 being Subspace of V holds the carrier of W1 c= the
carrier of W1 + W2;
theorem :: HAHNBAN:2
for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v,v1,v2 being VECTOR of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds v |--
(W1,W2) = [v1,v2];
theorem :: HAHNBAN:3
for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v,v1,v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds v = v1 + v2;
theorem :: HAHNBAN:4
for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v,v1,v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds v1 in W1 & v2 in
W2;
theorem :: HAHNBAN:5
for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v,v1,v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds v |-- (W2,W1) =
[v2,v1];
theorem :: HAHNBAN:6
for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v being VECTOR of V st v in W1 holds v |-- (W1,W2) = [v,0.V];
theorem :: HAHNBAN:7
for W1,W2 being Subspace of V st V is_the_direct_sum_of W1,W2
for v being VECTOR of V st v in W2 holds v |-- (W1,W2) = [0.V,v];
theorem :: HAHNBAN:8
for V1 being Subspace of V, W1 being Subspace of V1, v being
VECTOR of V st v in W1 holds v is VECTOR of V1;
theorem :: HAHNBAN:9
for V1,V2,W being Subspace of V, W1,W2 being Subspace of W st W1
= V1 & W2 = V2 holds W1 + W2 = V1 + V2;
theorem :: HAHNBAN:10
for W being Subspace of V for v being VECTOR of V, w being
VECTOR of W st v = w holds Lin{w} = Lin{v};
theorem :: HAHNBAN:11
for v being VECTOR of V, X being Subspace of V st not v in X for
y being VECTOR of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & W = X
holds X + Lin{v} is_the_direct_sum_of W,Lin{y};
theorem :: HAHNBAN:12
for v being VECTOR of V, X being Subspace of V, y being VECTOR
of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X
holds y |-- (W,Lin{y}) = [0.W,y];
theorem :: HAHNBAN:13
for v being VECTOR of V, X being Subspace of V, y being VECTOR
of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X for
w being VECTOR of X + Lin{v} st w in X holds w |-- (W,Lin{y}) = [w,0.V];
theorem :: HAHNBAN:14
for v being VECTOR of V, W1,W2 being Subspace of V ex v1,v2
being VECTOR of V st v |-- (W1,W2) = [v1,v2];
theorem :: HAHNBAN:15
for v being VECTOR of V, X being Subspace of V, y being VECTOR
of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X for
w being VECTOR of X + Lin{v} ex x being VECTOR of X, r being Real
st w |-- (W,
Lin{y}) = [x,r*v];
theorem :: HAHNBAN:16
for v being VECTOR of V, X being Subspace of V, y being VECTOR
of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X for
w1,w2 being VECTOR of X + Lin{v}, x1,x2 being VECTOR of X,
r1,r2 being Real st
w1 |-- (W,Lin{y}) = [x1,r1*v] & w2 |-- (W,Lin{y}) = [x2,r2*v] holds w1 + w2 |--
(W,Lin{y}) = [x1 + x2, (r1+r2)*v];
theorem :: HAHNBAN:17
for v being VECTOR of V, X being Subspace of V, y being VECTOR
of X + Lin{v}, W being Subspace of X + Lin{v} st v = y & X = W & not v in X for
w being VECTOR of X + Lin{v}, x being VECTOR of X,
t,r being Real st w |-- (W,
Lin{y}) = [x,r*v] holds t*w |-- (W,Lin{y}) = [t*x, t*r*v];
begin :: Functionals in Real Linear Space
definition
let V be RLSStruct;
mode Functional of V is Function of the carrier of V,REAL;
end;
definition
let V;
let IT be Functional of V;
attr IT is subadditive means
:: HAHNBAN:def 1
for x,y being VECTOR of V holds IT.(x+y) <= IT.x+IT.y;
attr IT is additive means
:: HAHNBAN:def 2
for x,y being VECTOR of V holds IT.(x+y) = IT.x+IT.y;
attr IT is homogeneous means
:: HAHNBAN:def 3
for x being VECTOR of V, r being Real holds IT.(r*x) = r*IT.x;
attr IT is positively_homogeneous means
:: HAHNBAN:def 4
for x being VECTOR of V, r being Real st r > 0
holds IT.(r*x) = r*IT.x;
attr IT is semi-homogeneous means
:: HAHNBAN:def 5
for x being VECTOR of V, r being Real st r >= 0
holds IT.(r*x) = r*IT.x;
attr IT is absolutely_homogeneous means
:: HAHNBAN:def 6
for x being VECTOR of V, r being Real holds IT.(r*x) = |.r.|*IT.x;
attr IT is 0-preserving means
:: HAHNBAN:def 7
IT.(0.V) = 0;
end;
registration
let V;
cluster additive -> subadditive for Functional of V;
cluster homogeneous -> positively_homogeneous for Functional of V;
cluster semi-homogeneous -> positively_homogeneous for Functional of V;
cluster semi-homogeneous -> 0-preserving for Functional of V;
cluster absolutely_homogeneous -> semi-homogeneous for Functional of V;
cluster 0-preserving positively_homogeneous -> semi-homogeneous for
Functional
of V;
end;
registration
let V;
cluster additive absolutely_homogeneous homogeneous for Functional of V;
end;
definition
let V;
mode Banach-Functional of V is subadditive positively_homogeneous Functional
of V;
mode linear-Functional of V is additive homogeneous Functional of V;
end;
theorem :: HAHNBAN:18
for L being homogeneous Functional of V, v being VECTOR of V
holds L.(-v) = - L.v;
theorem :: HAHNBAN:19
for L being linear-Functional of V, v1,v2 being VECTOR of V
holds L.(v1 - v2) = L.v1 - L.v2;
theorem :: HAHNBAN:20
for L being additive Functional of V holds L.(0.V) = 0;
theorem :: HAHNBAN:21
for X being Subspace of V, fi being linear-Functional of X, v
being VECTOR of V, y being VECTOR of X + Lin{v} st v = y & not v in X for r
being Real ex psi being linear-Functional of X + Lin{v} st psi|the carrier of X
=fi & psi.y = r;
begin
theorem :: HAHNBAN:22
for V being RealLinearSpace, X being Subspace of V, q being
Banach-Functional of V, fi being linear-Functional of X st for x being VECTOR
of X, v being VECTOR of V st x=v holds fi.x <= q.v ex psi being
linear-Functional of V st psi|the carrier of X=fi & for x being VECTOR of V
holds psi.x <= q.x;
theorem :: HAHNBAN:23
for V being RealNormSpace holds the normF of V is
absolutely_homogeneous subadditive Functional of V;
::$N Hahn-Banach Theorem (real spaces)
theorem :: HAHNBAN:24
for V being RealNormSpace, X being Subspace of V, fi being
linear-Functional of X st for x being VECTOR of X, v being VECTOR of V st x=v
holds fi.x <= ||.v.|| ex psi being linear-Functional of V st psi|the carrier of
X=fi & for x being VECTOR of V holds psi.x <= ||.x.||;