:: Hahn Banach Theorem
::  by Bogdan Nowak and Andrzej Trybulec
::
:: Received July 8, 1993
:: Copyright (c) 1993-2021 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, 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.||;