:: by Kazuhisa Nakasho , Yuichi Futa and Yasunari Shidama

::

:: Received September 15, 2014

:: Copyright (c) 2014-2017 Association of Mizar Users

registration

let X be RealNormSpace;

correctness

existence

ex b_{1} being Subset of X st

( b_{1} is open & b_{1} is closed );

end;
correctness

existence

ex b

( b

proof end;

theorem :: NORMSP_3:1

registration
end;

registration
end;

registration

let X be RealNormSpace;

correctness

coherence

[#] X is closed ;

;

correctness

coherence

{} X is closed ;

;

correctness

coherence

[#] X is open ;

coherence

{} X is open ;

end;
correctness

coherence

[#] X is closed ;

;

correctness

coherence

{} X is closed ;

;

correctness

coherence

[#] X is open ;

proof end;

correctness coherence

{} X is open ;

proof end;

registration

let X be RealNormSpace;

let P, Q be closed Subset of X;

correctness

coherence

for b_{1} being Subset of X st b_{1} = P /\ Q holds

b_{1} is closed ;

coherence

for b_{1} being Subset of X st b_{1} = P \/ Q holds

b_{1} is closed ;

end;
let P, Q be closed Subset of X;

correctness

coherence

for b

b

proof end;

correctness coherence

for b

b

proof end;

registration

let X be RealNormSpace;

let P, Q be open Subset of X;

correctness

coherence

for b_{1} being Subset of X st b_{1} = P /\ Q holds

b_{1} is open ;

coherence

for b_{1} being Subset of X st b_{1} = P \/ Q holds

b_{1} is open ;

end;
let P, Q be open Subset of X;

correctness

coherence

for b

b

proof end;

correctness coherence

for b

b

proof end;

definition

let X be RealNormSpace;

let Y be Subset of X;

existence

ex b_{1} being Subset of X ex Z being Subset of (LinearTopSpaceNorm X) st

( Z = Y & b_{1} = Cl Z );

uniqueness

for b_{1}, b_{2} being Subset of X st ex Z being Subset of (LinearTopSpaceNorm X) st

( Z = Y & b_{1} = Cl Z ) & ex Z being Subset of (LinearTopSpaceNorm X) st

( Z = Y & b_{2} = Cl Z ) holds

b_{1} = b_{2};

end;
let Y be Subset of X;

func Cl Y -> Subset of X means :defcl: :: NORMSP_3:def 1

ex Z being Subset of (LinearTopSpaceNorm X) st

( Z = Y & it = Cl Z );

correctness ex Z being Subset of (LinearTopSpaceNorm X) st

( Z = Y & it = Cl Z );

existence

ex b

( Z = Y & b

uniqueness

for b

( Z = Y & b

( Z = Y & b

b

proof end;

:: deftheorem defcl defines Cl NORMSP_3:def 1 :

for X being RealNormSpace

for Y, b_{3} being Subset of X holds

( b_{3} = Cl Y iff ex Z being Subset of (LinearTopSpaceNorm X) st

( Z = Y & b_{3} = Cl Z ) );

for X being RealNormSpace

for Y, b

( b

( Z = Y & b

registration
end;

theorem EQCL1: :: NORMSP_3:3

for X being RealNormSpace

for Y being Subset of X

for Z being Subset of (LinearTopSpaceNorm X) st Y = Z holds

Cl Y = Cl Z

for Y being Subset of X

for Z being Subset of (LinearTopSpaceNorm X) st Y = Z holds

Cl Y = Cl Z

proof end;

theorem :: NORMSP_3:5

for X being RealNormSpace

for Y being Subset of X

for v being object st v in the carrier of X holds

( v in Cl Y iff for G being Subset of X st G is open & v in G holds

G meets Y )

for Y being Subset of X

for v being object st v in the carrier of X holds

( v in Cl Y iff for G being Subset of X st G is open & v in G holds

G meets Y )

proof end;

theorem EQCL3: :: NORMSP_3:6

for X being RealNormSpace

for Y being Subset of X

for v being object holds

( v in Cl Y iff ex seq being sequence of X st

( rng seq c= Y & seq is convergent & lim seq = v ) )

for Y being Subset of X

for v being object holds

( v in Cl Y iff ex seq being sequence of X st

( rng seq c= Y & seq is convergent & lim seq = v ) )

proof end;

theorem :: NORMSP_3:7

for X being RealNormSpace

for A being Subset of X ex F being Subset-Family of X st

( ( for C being Subset of X holds

( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )

for A being Subset of X ex F being Subset-Family of X st

( ( for C being Subset of X holds

( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )

proof end;

theorem :: NORMSP_3:12

for X being RealNormSpace

for A being Subset of X holds

( A is open iff Cl (([#] X) \ A) = ([#] X) \ A )

for A being Subset of X holds

( A is open iff Cl (([#] X) \ A) = ([#] X) \ A )

proof end;

theorem Cl01: :: NORMSP_3:13

for X being RealNormSpace

for Y being Subspace of X

for CY being Subset of X st CY = the carrier of Y holds

Cl CY is linearly-closed

for Y being Subspace of X

for CY being Subset of X st CY = the carrier of Y holds

Cl CY is linearly-closed

proof end;

definition
end;

:: deftheorem defines dense NORMSP_3:def 2 :

for X being RealNormSpace

for A being Subset of X holds

( A is dense iff Cl A = [#] X );

for X being RealNormSpace

for A being Subset of X holds

( A is dense iff Cl A = [#] X );

registration
end;

registration

let X be RealNormSpace;

correctness

existence

ex b_{1} being Subset of X st

( b_{1} is open & b_{1} is closed & b_{1} is dense );

end;
correctness

existence

ex b

( b

proof end;

theorem :: NORMSP_3:14

for X being RealNormSpace

for A being Subset of X holds

( A is dense iff for x being Point of X ex seq being sequence of X st

( rng seq c= A & seq is convergent & lim seq = x ) )

for A being Subset of X holds

( A is dense iff for x being Point of X ex seq being sequence of X st

( rng seq c= A & seq is convergent & lim seq = x ) )

proof end;

theorem EQCL2: :: NORMSP_3:15

for X being RealNormSpace

for Y being Subset of X

for Z being Subset of (LinearTopSpaceNorm X) st Y = Z holds

( Y is dense iff Z is dense )

for Y being Subset of X

for Z being Subset of (LinearTopSpaceNorm X) st Y = Z holds

( Y is dense iff Z is dense )

proof end;

theorem TOPS145: :: NORMSP_3:17

for X being RealNormSpace

for R being Subset of X holds

( R is dense iff for S being Subset of X st S <> {} & S is open holds

R meets S )

for R being Subset of X holds

( R is dense iff for S being Subset of X st S <> {} & S is open holds

R meets S )

proof end;

theorem :: NORMSP_3:18

for X being RealNormSpace

for R, S being Subset of X st R is dense & S is open holds

Cl S = Cl (S /\ R)

for R, S being Subset of X st R is dense & S is open holds

Cl S = Cl (S /\ R)

proof end;

theorem :: NORMSP_3:19

for X being RealNormSpace

for R, S being Subset of X st R is dense & S is dense & S is open holds

R /\ S is dense

for R, S being Subset of X st R is dense & S is dense & S is open holds

R /\ S is dense

proof end;

:: deftheorem defines separable NORMSP_3:def 3 :

for X being RealNormSpace holds

( X is separable iff LinearTopSpaceNorm X is separable );

for X being RealNormSpace holds

( X is separable iff LinearTopSpaceNorm X is separable );

theorem :: NORMSP_3:21

for X being RealNormSpace holds

( X is separable iff ex seq being sequence of X st rng seq is dense )

( X is separable iff ex seq being sequence of X st rng seq is dense )

proof end;

theorem LMINEQ: :: NORMSP_3:22

for x, y, z being Real st 0 <= y & ( for e being Real st 0 < e holds

x <= z + (y * e) ) holds

x <= z

x <= z + (y * e) ) holds

x <= z

proof end;

theorem CLOSE01: :: NORMSP_3:23

for X being RealNormSpace

for x being Point of X

for seq being sequence of X st ( for n being Nat holds seq . n = x ) holds

( seq is convergent & lim seq = x )

for x being Point of X

for seq being sequence of X st ( for n being Nat holds seq . n = x ) holds

( seq is convergent & lim seq = x )

proof end;

theorem CLOSE1: :: NORMSP_3:25

for X being RealNormSpace

for Y being Subset of X

for v being VECTOR of X st Y is closed & ( for e being Real st 0 < e holds

ex w being VECTOR of X st

( w in Y & ||.(v - w).|| <= e ) ) holds

v in Y

for Y being Subset of X

for v being VECTOR of X st Y is closed & ( for e being Real st 0 < e holds

ex w being VECTOR of X st

( w in Y & ||.(v - w).|| <= e ) ) holds

v in Y

proof end;

theorem NSUBA: :: NORMSP_3:26

for V being RealNormSpace

for W being SubRealNormSpace of V st the carrier of W = the carrier of V holds

NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the normF of W #) = NORMSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the normF of V #)

for W being SubRealNormSpace of V st the carrier of W = the carrier of V holds

NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the normF of W #) = NORMSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the normF of V #)

proof end;

theorem SUBTH0: :: NORMSP_3:28

for V being RealNormSpace

for V1 being SubRealNormSpace of V

for x, y being Point of V

for x1, y1 being Point of V1

for a being Real st x = x1 & y = y1 holds

( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )

for V1 being SubRealNormSpace of V

for x, y being Point of V

for x1, y1 being Point of V1

for a being Real st x = x1 & y = y1 holds

( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )

proof end;

theorem RLSUB134: :: NORMSP_3:29

for V being RealNormSpace

for V1 being SubRealNormSpace of V

for S being Subset of V st S = the carrier of V1 holds

S is linearly-closed

for V1 being SubRealNormSpace of V

for S being Subset of V st S = the carrier of V1 holds

S is linearly-closed

proof end;

definition

let X be RealNormSpace;

let X1 be set ;

assume A1: X1 c= the carrier of X ;

correctness

coherence

the normF of X | X1 is Function of X1,REAL;

end;
let X1 be set ;

assume A1: X1 c= the carrier of X ;

correctness

coherence

the normF of X | X1 is Function of X1,REAL;

proof end;

:: deftheorem DefNorm defines Norm_ NORMSP_3:def 4 :

for X being RealNormSpace

for X1 being set st X1 c= the carrier of X holds

Norm_ (X1,X) = the normF of X | X1;

for X being RealNormSpace

for X1 being set st X1 c= the carrier of X holds

Norm_ (X1,X) = the normF of X | X1;

definition

let V be RealNormSpace;

let V1 be Subset of V;

coherence

NORMSTR(# the carrier of (Lin V1),(0. (Lin V1)), the addF of (Lin V1), the Mult of (Lin V1),(Norm_ ( the carrier of (Lin V1),V)) #) is non empty NORMSTR ;

;

end;
let V1 be Subset of V;

func NLin V1 -> non empty NORMSTR equals :: NORMSP_3:def 5

NORMSTR(# the carrier of (Lin V1),(0. (Lin V1)), the addF of (Lin V1), the Mult of (Lin V1),(Norm_ ( the carrier of (Lin V1),V)) #);

correctness NORMSTR(# the carrier of (Lin V1),(0. (Lin V1)), the addF of (Lin V1), the Mult of (Lin V1),(Norm_ ( the carrier of (Lin V1),V)) #);

coherence

NORMSTR(# the carrier of (Lin V1),(0. (Lin V1)), the addF of (Lin V1), the Mult of (Lin V1),(Norm_ ( the carrier of (Lin V1),V)) #) is non empty NORMSTR ;

;

:: deftheorem defines NLin NORMSP_3:def 5 :

for V being RealNormSpace

for V1 being Subset of V holds NLin V1 = NORMSTR(# the carrier of (Lin V1),(0. (Lin V1)), the addF of (Lin V1), the Mult of (Lin V1),(Norm_ ( the carrier of (Lin V1),V)) #);

for V being RealNormSpace

for V1 being Subset of V holds NLin V1 = NORMSTR(# the carrier of (Lin V1),(0. (Lin V1)), the addF of (Lin V1), the Mult of (Lin V1),(Norm_ ( the carrier of (Lin V1),V)) #);

SUBTH: for V being RealNormSpace

for V1 being Subset of V

for x, y being Point of V

for x1, y1 being Point of (NLin V1)

for a being Real st x = x1 & y = y1 holds

( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )

proof end;

XTh7: for V being RealNormSpace

for V1 being Subset of V

for x, y being Point of (NLin V1)

for a being Real holds

( ( ||.x.|| = 0 implies x = 0. (NLin V1) ) & ( x = 0. (NLin V1) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )

proof end;

definition

let V be RealNormSpace;

let V1 be Subset of V;

:: original: NLin

redefine func NLin V1 -> SubRealNormSpace of V;

coherence

NLin V1 is SubRealNormSpace of V by ThSubSpace;

end;
let V1 be Subset of V;

:: original: NLin

redefine func NLin V1 -> SubRealNormSpace of V;

coherence

NLin V1 is SubRealNormSpace of V by ThSubSpace;

theorem LCL1: :: NORMSP_3:31

for V being RealLinearSpace

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

the carrier of (Lin V1) = V1

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

the carrier of (Lin V1) = V1

proof end;

theorem :: NORMSP_3:32

for V being RealNormSpace

for W being SubRealNormSpace of V

for V1 being Subset of V st the carrier of W = V1 holds

NLin V1 = NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the normF of W #)

for W being SubRealNormSpace of V

for V1 being Subset of V st the carrier of W = V1 holds

NLin V1 = NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the normF of W #)

proof end;

theorem KERX1: :: NORMSP_3:33

for X, Y being RealLinearSpace

for f being Function of X,Y st f is homogeneous holds

not f " {(0. Y)} is empty

for f being Function of X,Y st f is homogeneous holds

not f " {(0. Y)} is empty

proof end;

registration

let X, Y be RealLinearSpace;

let f be LinearOperator of X,Y;

correctness

coherence

not f " {(0. Y)} is empty ;

by KERX1;

end;
let f be LinearOperator of X,Y;

correctness

coherence

not f " {(0. Y)} is empty ;

by KERX1;

theorem KLXY1: :: NORMSP_3:34

for X, Y being RealLinearSpace

for f being Function of X,Y st f is additive & f is homogeneous holds

f " {(0. Y)} is linearly-closed

for f being Function of X,Y st f is additive & f is homogeneous holds

f " {(0. Y)} is linearly-closed

proof end;

theorem IMX2: :: NORMSP_3:35

for X, Y being RealLinearSpace

for f being Function of X,Y st f is additive & f is homogeneous holds

rng f is linearly-closed

for f being Function of X,Y st f is additive & f is homogeneous holds

rng f is linearly-closed

proof end;

definition

let X, Y be RealLinearSpace;

let f be LinearOperator of X,Y;

coherence

Lin (f " {(0. Y)}) is Subspace of X ;

end;
let f be LinearOperator of X,Y;

coherence

Lin (f " {(0. Y)}) is Subspace of X ;

:: deftheorem defines Ker NORMSP_3:def 6 :

for X, Y being RealLinearSpace

for f being LinearOperator of X,Y holds Ker f = Lin (f " {(0. Y)});

for X, Y being RealLinearSpace

for f being LinearOperator of X,Y holds Ker f = Lin (f " {(0. Y)});

definition

let X, Y be RealNormSpace;

let f be LinearOperator of X,Y;

coherence

NLin (f " {(0. Y)}) is SubRealNormSpace of X ;

end;
let f be LinearOperator of X,Y;

coherence

NLin (f " {(0. Y)}) is SubRealNormSpace of X ;

:: deftheorem defines NKer NORMSP_3:def 7 :

for X, Y being RealNormSpace

for f being LinearOperator of X,Y holds NKer f = NLin (f " {(0. Y)});

for X, Y being RealNormSpace

for f being LinearOperator of X,Y holds NKer f = NLin (f " {(0. Y)});

definition

let X, Y be RealLinearSpace;

let f be LinearOperator of X,Y;

coherence

Lin (rng f) is Subspace of Y ;

end;
let f be LinearOperator of X,Y;

coherence

Lin (rng f) is Subspace of Y ;

:: deftheorem defines Im NORMSP_3:def 8 :

for X, Y being RealLinearSpace

for f being LinearOperator of X,Y holds Im f = Lin (rng f);

for X, Y being RealLinearSpace

for f being LinearOperator of X,Y holds Im f = Lin (rng f);

definition

let X, Y be RealNormSpace;

let f be LinearOperator of X,Y;

coherence

NLin (rng f) is SubRealNormSpace of Y ;

end;
let f be LinearOperator of X,Y;

coherence

NLin (rng f) is SubRealNormSpace of Y ;

:: deftheorem defines Im NORMSP_3:def 9 :

for X, Y being RealNormSpace

for f being LinearOperator of X,Y holds Im f = NLin (rng f);

for X, Y being RealNormSpace

for f being LinearOperator of X,Y holds Im f = NLin (rng f);

:: deftheorem defines isomorphism NORMSP_3:def 10 :

for X, Y being RealLinearSpace

for L being LinearOperator of X,Y holds

( L is isomorphism iff ( L is one-to-one & L is onto ) );

for X, Y being RealLinearSpace

for L being LinearOperator of X,Y holds

( L is isomorphism iff ( L is one-to-one & L is onto ) );

registration

let X, Y be RealLinearSpace;

for b_{1} being LinearOperator of X,Y st b_{1} is isomorphism holds

( b_{1} is one-to-one & b_{1} is onto )
;

for b_{1} being LinearOperator of X,Y st b_{1} is one-to-one & b_{1} is onto holds

b_{1} is isomorphism
;

end;
cluster Function-like quasi_total additive homogeneous isomorphism -> one-to-one onto for Element of bool [: the carrier of X, the carrier of Y:];

coherence for b

( b

cluster Function-like one-to-one quasi_total onto additive homogeneous -> isomorphism for Element of bool [: the carrier of X, the carrier of Y:];

coherence for b

b

theorem :: NORMSP_3:36

for X, Y being RealLinearSpace

for L being LinearOperator of X,Y st L is isomorphism holds

ex K being LinearOperator of Y,X st

( K = L " & K is isomorphism )

for L being LinearOperator of X,Y st L is isomorphism holds

ex K being LinearOperator of Y,X st

( K = L " & K is isomorphism )

proof end;

definition

let X, Y be RealNormSpace;

let L be LinearOperator of X,Y;

end;
let L be LinearOperator of X,Y;

attr L is isomorphism means :: NORMSP_3:def 11

( L is one-to-one & L is onto & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) );

( L is one-to-one & L is onto & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) );

:: deftheorem defines isomorphism NORMSP_3:def 11 :

for X, Y being RealNormSpace

for L being LinearOperator of X,Y holds

( L is isomorphism iff ( L is one-to-one & L is onto & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) ) );

for X, Y being RealNormSpace

for L being LinearOperator of X,Y holds

( L is isomorphism iff ( L is one-to-one & L is onto & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) ) );

registration

let X, Y be RealNormSpace;

for b_{1} being LinearOperator of X,Y st b_{1} is isomorphism holds

( b_{1} is one-to-one & b_{1} is onto )
;

end;
cluster Function-like quasi_total additive homogeneous isomorphism -> one-to-one onto for Element of bool [: the carrier of X, the carrier of Y:];

coherence for b

( b

theorem NISOM01: :: NORMSP_3:37

for X, Y being RealNormSpace

for L being LinearOperator of X,Y st L is isomorphism holds

ex K being Lipschitzian LinearOperator of Y,X st

( K = L " & K is isomorphism )

for L being LinearOperator of X,Y st L is isomorphism holds

ex K being Lipschitzian LinearOperator of Y,X st

( K = L " & K is isomorphism )

proof end;

theorem NISOM02: :: NORMSP_3:38

for X, Y being RealNormSpace

for L being Lipschitzian LinearOperator of X,Y

for seq being sequence of X st seq is convergent holds

( L * seq is convergent & lim (L * seq) = L . (lim seq) )

for L being Lipschitzian LinearOperator of X,Y

for seq being sequence of X st seq is convergent holds

( L * seq is convergent & lim (L * seq) = L . (lim seq) )

proof end;

theorem KERCL01: :: NORMSP_3:39

for X, Y being RealNormSpace

for L being Function of X,Y

for w being Point of Y st L is_continuous_on the carrier of X holds

L " {w} is closed

for L being Function of X,Y

for w being Point of Y st L is_continuous_on the carrier of X holds

L " {w} is closed

proof end;

theorem :: NORMSP_3:40

for X, Y being RealNormSpace

for L being Lipschitzian LinearOperator of X,Y holds

( the carrier of (Ker L) = L " {(0. Y)} & L " {(0. Y)} is closed ) by LCL1, KLXY1, KERCL01, LOPBAN_7:6;

for L being Lipschitzian LinearOperator of X,Y holds

( the carrier of (Ker L) = L " {(0. Y)} & L " {(0. Y)} is closed ) by LCL1, KLXY1, KERCL01, LOPBAN_7:6;

theorem NISOM03: :: NORMSP_3:41

for X, Y being RealNormSpace

for L being Lipschitzian LinearOperator of X,Y

for seq being sequence of X st L is isomorphism holds

( seq is convergent iff L * seq is convergent )

for L being Lipschitzian LinearOperator of X,Y

for seq being sequence of X st L is isomorphism holds

( seq is convergent iff L * seq is convergent )

proof end;

theorem NISOM04: :: NORMSP_3:42

for X, Y being RealNormSpace

for L being Lipschitzian LinearOperator of X,Y

for seq being sequence of X st L is isomorphism & seq is Cauchy_sequence_by_Norm holds

L * seq is Cauchy_sequence_by_Norm

for L being Lipschitzian LinearOperator of X,Y

for seq being sequence of X st L is isomorphism & seq is Cauchy_sequence_by_Norm holds

L * seq is Cauchy_sequence_by_Norm

proof end;

theorem NISOM05: :: NORMSP_3:43

for X, Y being RealNormSpace

for L being Lipschitzian LinearOperator of X,Y

for seq being sequence of X st L is isomorphism holds

( seq is Cauchy_sequence_by_Norm iff L * seq is Cauchy_sequence_by_Norm )

for L being Lipschitzian LinearOperator of X,Y

for seq being sequence of X st L is isomorphism holds

( seq is Cauchy_sequence_by_Norm iff L * seq is Cauchy_sequence_by_Norm )

proof end;

theorem :: NORMSP_3:44

for X, Y being RealNormSpace st ex L being Lipschitzian LinearOperator of X,Y st L is isomorphism holds

( X is complete iff Y is complete )

( X is complete iff Y is complete )

proof end;

NISOM06: for X, Y being RealNormSpace

for L being Lipschitzian LinearOperator of X,Y

for V being Subset of X

for W being Subset of Y st L is isomorphism & W = L .: V & W is closed holds

V is closed

proof end;

theorem :: NORMSP_3:45

for X, Y being RealNormSpace

for L being Lipschitzian LinearOperator of X,Y

for V being Subset of X

for W being Subset of Y st L is isomorphism & W = L .: V holds

( V is closed iff W is closed )

for L being Lipschitzian LinearOperator of X,Y

for V being Subset of X

for W being Subset of Y st L is isomorphism & W = L .: V holds

( V is closed iff W is closed )

proof end;

theorem :: NORMSP_3:46

for X, Y being RealNormSpace

for L being LinearOperator of X,Y st L is onto holds

Im L = NORMSTR(# the carrier of Y, the ZeroF of Y, the addF of Y, the Mult of Y, the normF of Y #)

for L being LinearOperator of X,Y st L is onto holds

Im L = NORMSTR(# the carrier of Y, the ZeroF of Y, the addF of Y, the Mult of Y, the normF of Y #)

proof end;

theorem LM76A: :: NORMSP_3:47

for V being RealBanachSpace

for V1 being SubRealNormSpace of V st ex CV1 being Subset of V st

( CV1 = the carrier of V1 & CV1 is closed ) holds

V1 is RealBanachSpace

for V1 being SubRealNormSpace of V st ex CV1 being Subset of V st

( CV1 = the carrier of V1 & CV1 is closed ) holds

V1 is RealBanachSpace

proof end;

theorem :: NORMSP_3:48

for V being RealNormSpace

for V1 being SubRealNormSpace of V

for CV1 being Subset of V st V1 is complete & CV1 = the carrier of V1 holds

CV1 is closed

for V1 being SubRealNormSpace of V

for CV1 being Subset of V st V1 is complete & CV1 = the carrier of V1 holds

CV1 is closed

proof end;

theorem :: NORMSP_3:49

for X being RealBanachSpace

for M being non empty Subset of X st M is linearly-closed & M is closed holds

NLin M is RealBanachSpace

for M being non empty Subset of X st M is linearly-closed & M is closed holds

NLin M is RealBanachSpace

proof end;

definition

let X be RealLinearSpace;

let Y be Subspace of X;

:: original: RLSp2RVSp

redefine func RLSp2RVSp Y -> Subspace of RLSp2RVSp X;

correctness

coherence

RLSp2RVSp Y is Subspace of RLSp2RVSp X;

end;
let Y be Subspace of X;

:: original: RLSp2RVSp

redefine func RLSp2RVSp Y -> Subspace of RLSp2RVSp X;

correctness

coherence

RLSp2RVSp Y is Subspace of RLSp2RVSp X;

proof end;

definition

let X be RealLinearSpace;

let Y be Subspace of X;

coherence

RVSp2RLSp (VectQuot ((RLSp2RVSp X),(RLSp2RVSp Y))) is RealLinearSpace;

;

end;
let Y be Subspace of X;

func VectQuot (X,Y) -> RealLinearSpace equals :: NORMSP_3:def 12

RVSp2RLSp (VectQuot ((RLSp2RVSp X),(RLSp2RVSp Y)));

correctness RVSp2RLSp (VectQuot ((RLSp2RVSp X),(RLSp2RVSp Y)));

coherence

RVSp2RLSp (VectQuot ((RLSp2RVSp X),(RLSp2RVSp Y))) is RealLinearSpace;

;

:: deftheorem defines VectQuot NORMSP_3:def 12 :

for X being RealLinearSpace

for Y being Subspace of X holds VectQuot (X,Y) = RVSp2RLSp (VectQuot ((RLSp2RVSp X),(RLSp2RVSp Y)));

for X being RealLinearSpace

for Y being Subspace of X holds VectQuot (X,Y) = RVSp2RLSp (VectQuot ((RLSp2RVSp X),(RLSp2RVSp Y)));

theorem :: NORMSP_3:50

theorem :: NORMSP_3:51

theorem LMQ03: :: NORMSP_3:52

for X being RealLinearSpace

for Y being Subspace of X

for v being Element of X

for v1 being Element of (RLSp2RVSp X) st v = v1 holds

v + Y = v1 + (RLSp2RVSp Y)

for Y being Subspace of X

for v being Element of X

for v1 being Element of (RLSp2RVSp X) st v = v1 holds

v + Y = v1 + (RLSp2RVSp Y)

proof end;

theorem LMQ04: :: NORMSP_3:53

for X being RealLinearSpace

for Y being Subspace of X

for x being object holds

( x is Coset of Y iff x is Coset of RLSp2RVSp Y )

for Y being Subspace of X

for x being object holds

( x is Coset of Y iff x is Coset of RLSp2RVSp Y )

proof end;

definition

let X be RealLinearSpace;

let Y be Subspace of X;

coherence

{ A where A is Coset of Y : verum } is non empty Subset-Family of X;

end;
let Y be Subspace of X;

func CosetSet (X,Y) -> non empty Subset-Family of X equals :: NORMSP_3:def 13

{ A where A is Coset of Y : verum } ;

correctness { A where A is Coset of Y : verum } ;

coherence

{ A where A is Coset of Y : verum } is non empty Subset-Family of X;

proof end;

:: deftheorem defines CosetSet NORMSP_3:def 13 :

for X being RealLinearSpace

for Y being Subspace of X holds CosetSet (X,Y) = { A where A is Coset of Y : verum } ;

for X being RealLinearSpace

for Y being Subspace of X holds CosetSet (X,Y) = { A where A is Coset of Y : verum } ;

definition

let V be RealLinearSpace;

let W be Subspace of V;

coherence

the carrier of W is Element of CosetSet (V,W)

end;
let W be Subspace of V;

coherence

the carrier of W is Element of CosetSet (V,W)

proof end;

:: deftheorem defines zeroCoset NORMSP_3:def 14 :

for V being RealLinearSpace

for W being Subspace of V holds zeroCoset (V,W) = the carrier of W;

for V being RealLinearSpace

for W being Subspace of V holds zeroCoset (V,W) = the carrier of W;

theorem LMQ05: :: NORMSP_3:54

for X being RealLinearSpace

for Y being Subspace of X holds CosetSet (X,Y) = CosetSet ((RLSp2RVSp X),(RLSp2RVSp Y))

for Y being Subspace of X holds CosetSet (X,Y) = CosetSet ((RLSp2RVSp X),(RLSp2RVSp Y))

proof end;

theorem LMQ06: :: NORMSP_3:55

for V being RealLinearSpace

for W being Subspace of V holds the carrier of (VectQuot (V,W)) = CosetSet (V,W)

for W being Subspace of V holds the carrier of (VectQuot (V,W)) = CosetSet (V,W)

proof end;

theorem LMQ07: :: NORMSP_3:56

for V being RealLinearSpace

for W being Subspace of V

for x being object holds

( x is Point of (VectQuot (V,W)) iff ex v being Point of V st x = v + W )

for W being Subspace of V

for x being object holds

( x is Point of (VectQuot (V,W)) iff ex v being Point of V st x = v + W )

proof end;

theorem LMQ09: :: NORMSP_3:58

for V being RealLinearSpace

for W being Subspace of V

for A being VECTOR of (VectQuot (V,W))

for v being VECTOR of V

for a being Real st A = v + W holds

a * A = (a * v) + W

for W being Subspace of V

for A being VECTOR of (VectQuot (V,W))

for v being VECTOR of V

for a being Real st A = v + W holds

a * A = (a * v) + W

proof end;

theorem LMQ10: :: NORMSP_3:59

for V being RealLinearSpace

for W being Subspace of V

for A being VECTOR of (VectQuot (V,W))

for v being VECTOR of V

for a being Real st A = v + W holds

- A = (- v) + W

for W being Subspace of V

for A being VECTOR of (VectQuot (V,W))

for v being VECTOR of V

for a being Real st A = v + W holds

- A = (- v) + W

proof end;

theorem LMQ11: :: NORMSP_3:60

for V being RealLinearSpace

for W being Subspace of V

for A1, A2 being VECTOR of (VectQuot (V,W))

for v1, v2 being VECTOR of V st A1 = v1 + W & A2 = v2 + W holds

A1 + A2 = (v1 + v2) + W

for W being Subspace of V

for A1, A2 being VECTOR of (VectQuot (V,W))

for v1, v2 being VECTOR of V st A1 = v1 + W & A2 = v2 + W holds

A1 + A2 = (v1 + v2) + W

proof end;

theorem :: NORMSP_3:61

for V being RealLinearSpace

for W being Subspace of V

for A1, A2 being VECTOR of (VectQuot (V,W))

for v1, v2 being VECTOR of V st A1 = v1 + W & A2 = v2 + W holds

A1 - A2 = (v1 - v2) + W

for W being Subspace of V

for A1, A2 being VECTOR of (VectQuot (V,W))

for v1, v2 being VECTOR of V st A1 = v1 + W & A2 = v2 + W holds

A1 - A2 = (v1 - v2) + W

proof end;

theorem LMQ13: :: NORMSP_3:62

for V being RealLinearSpace

for W being Subspace of V holds

( 0. (VectQuot (V,W)) = the carrier of W & 0. (VectQuot (V,W)) = (0. V) + W )

for W being Subspace of V holds

( 0. (VectQuot (V,W)) = the carrier of W & 0. (VectQuot (V,W)) = (0. V) + W )

proof end;

theorem LMQ20: :: NORMSP_3:63

for V being RealLinearSpace

for W being Subspace of V ex QL being LinearOperator of V,(VectQuot (V,W)) st

( QL is onto & ( for v being VECTOR of V holds QL . v = v + W ) )

for W being Subspace of V ex QL being LinearOperator of V,(VectQuot (V,W)) st

( QL is onto & ( for v being VECTOR of V holds QL . v = v + W ) )

proof end;

definition

let V be RealLinearSpace;

let W be Subspace of V;

ex b_{1} being LinearOperator of V,(VectQuot (V,W)) st

( b_{1} is onto & ( for v being VECTOR of V holds b_{1} . v = v + W ) )
by LMQ20;

uniqueness

for b_{1}, b_{2} being LinearOperator of V,(VectQuot (V,W)) st b_{1} is onto & ( for v being VECTOR of V holds b_{1} . v = v + W ) & b_{2} is onto & ( for v being VECTOR of V holds b_{2} . v = v + W ) holds

b_{1} = b_{2}

end;
let W be Subspace of V;

func InducedSur (V,W) -> LinearOperator of V,(VectQuot (V,W)) means :defDQuot: :: NORMSP_3:def 15

( it is onto & ( for v being VECTOR of V holds it . v = v + W ) );

existence ( it is onto & ( for v being VECTOR of V holds it . v = v + W ) );

ex b

( b

uniqueness

for b

b

proof end;

:: deftheorem defDQuot defines InducedSur NORMSP_3:def 15 :

for V being RealLinearSpace

for W being Subspace of V

for b_{3} being LinearOperator of V,(VectQuot (V,W)) holds

( b_{3} = InducedSur (V,W) iff ( b_{3} is onto & ( for v being VECTOR of V holds b_{3} . v = v + W ) ) );

for V being RealLinearSpace

for W being Subspace of V

for b

( b

theorem LMQ21: :: NORMSP_3:64

for V, W being RealLinearSpace

for L being LinearOperator of V,W ex QL being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st

( QL is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

for L being LinearOperator of V,W ex QL being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st

( QL is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

proof end;

definition

let V, W be RealLinearSpace;

let L be LinearOperator of V,W;

ex b_{1} being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st

( b_{1} is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

b_{1} . z = L . v ) )
by LMQ21;

uniqueness

for b_{1}, b_{2} being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st b_{1} is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

b_{1} . z = L . v ) & b_{2} is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

b_{2} . z = L . v ) holds

b_{1} = b_{2}

end;
let L be LinearOperator of V,W;

func InducedBi (V,W,L) -> LinearOperator of (VectQuot (V,(Ker L))),(Im L) means :defQuotR: :: NORMSP_3:def 16

( it is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

it . z = L . v ) );

existence ( it is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

it . z = L . v ) );

ex b

( b

for v being VECTOR of V st z = v + (Ker L) holds

b

uniqueness

for b

for v being VECTOR of V st z = v + (Ker L) holds

b

for v being VECTOR of V st z = v + (Ker L) holds

b

b

proof end;

:: deftheorem defQuotR defines InducedBi NORMSP_3:def 16 :

for V, W being RealLinearSpace

for L being LinearOperator of V,W

for b_{4} being LinearOperator of (VectQuot (V,(Ker L))),(Im L) holds

( b_{4} = InducedBi (V,W,L) iff ( b_{4} is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

b_{4} . z = L . v ) ) );

for V, W being RealLinearSpace

for L being LinearOperator of V,W

for b

( b

for v being VECTOR of V st z = v + (Ker L) holds

b

theorem :: NORMSP_3:65

for V, W being RealLinearSpace

for L being LinearOperator of V,W holds L = (InducedBi (V,W,L)) * (InducedSur (V,(Ker L)))

for L being LinearOperator of V,W holds L = (InducedBi (V,W,L)) * (InducedSur (V,(Ker L)))

proof end;

definition

let V be RealNormSpace;

let W be Subspace of V;

let v be VECTOR of V;

coherence

{ ||.x.|| where x is VECTOR of V : x in v + W } is non empty Subset of REAL;

end;
let W be Subspace of V;

let v be VECTOR of V;

func NormVSets (V,W,v) -> non empty Subset of REAL equals :: NORMSP_3:def 17

{ ||.x.|| where x is VECTOR of V : x in v + W } ;

correctness { ||.x.|| where x is VECTOR of V : x in v + W } ;

coherence

{ ||.x.|| where x is VECTOR of V : x in v + W } is non empty Subset of REAL;

proof end;

:: deftheorem defines NormVSets NORMSP_3:def 17 :

for V being RealNormSpace

for W being Subspace of V

for v being VECTOR of V holds NormVSets (V,W,v) = { ||.x.|| where x is VECTOR of V : x in v + W } ;

for V being RealNormSpace

for W being Subspace of V

for v being VECTOR of V holds NormVSets (V,W,v) = { ||.x.|| where x is VECTOR of V : x in v + W } ;

LMQ231: for V being RealNormSpace

for W being Subspace of V

for v being VECTOR of V holds NormVSets (V,W,v) is bounded_below

proof end;

registration

let V be RealNormSpace;

let W be Subspace of V;

let v be VECTOR of V;

correctness

coherence

( not NormVSets (V,W,v) is empty & NormVSets (V,W,v) is bounded_below );

by LMQ231;

end;
let W be Subspace of V;

let v be VECTOR of V;

correctness

coherence

( not NormVSets (V,W,v) is empty & NormVSets (V,W,v) is bounded_below );

by LMQ231;

theorem LMQ23: :: NORMSP_3:66

for V being RealNormSpace

for W being Subspace of V

for v being VECTOR of V holds

( 0 <= lower_bound (NormVSets (V,W,v)) & lower_bound (NormVSets (V,W,v)) <= ||.v.|| )

for W being Subspace of V

for v being VECTOR of V holds

( 0 <= lower_bound (NormVSets (V,W,v)) & lower_bound (NormVSets (V,W,v)) <= ||.v.|| )

proof end;

definition

let V be RealNormSpace;

let W be Subspace of V;

ex b_{1} being Function of (CosetSet (V,W)),REAL st

for A being Element of CosetSet (V,W)

for v being VECTOR of V st A = v + W holds

b_{1} . A = lower_bound (NormVSets (V,W,v))

for b_{1}, b_{2} being Function of (CosetSet (V,W)),REAL st ( for A being Element of CosetSet (V,W)

for v being VECTOR of V st A = v + W holds

b_{1} . A = lower_bound (NormVSets (V,W,v)) ) & ( for A being Element of CosetSet (V,W)

for v being VECTOR of V st A = v + W holds

b_{2} . A = lower_bound (NormVSets (V,W,v)) ) holds

b_{1} = b_{2}

end;
let W be Subspace of V;

func NormCoset (V,W) -> Function of (CosetSet (V,W)),REAL means :DeNorm: :: NORMSP_3:def 18

for A being Element of CosetSet (V,W)

for v being VECTOR of V st A = v + W holds

it . A = lower_bound (NormVSets (V,W,v));

existence for A being Element of CosetSet (V,W)

for v being VECTOR of V st A = v + W holds

it . A = lower_bound (NormVSets (V,W,v));

ex b

for A being Element of CosetSet (V,W)

for v being VECTOR of V st A = v + W holds

b

proof end;

uniqueness for b

for v being VECTOR of V st A = v + W holds

b

for v being VECTOR of V st A = v + W holds

b

b

proof end;

:: deftheorem DeNorm defines NormCoset NORMSP_3:def 18 :

for V being RealNormSpace

for W being Subspace of V

for b_{3} being Function of (CosetSet (V,W)),REAL holds

( b_{3} = NormCoset (V,W) iff for A being Element of CosetSet (V,W)

for v being VECTOR of V st A = v + W holds

b_{3} . A = lower_bound (NormVSets (V,W,v)) );

for V being RealNormSpace

for W being Subspace of V

for b

( b

for v being VECTOR of V st A = v + W holds

b

definition

let X be RealNormSpace;

let Y be Subspace of X;

assume A1: ex CY being Subset of X st

( CY = the carrier of Y & CY is closed ) ;

ex b_{1} being strict RealNormSpace st

( RLSStruct(# the carrier of b_{1}, the ZeroF of b_{1}, the addF of b_{1}, the Mult of b_{1} #) = VectQuot (X,Y) & the normF of b_{1} = NormCoset (X,Y) )

for b_{1}, b_{2} being strict RealNormSpace st RLSStruct(# the carrier of b_{1}, the ZeroF of b_{1}, the addF of b_{1}, the Mult of b_{1} #) = VectQuot (X,Y) & the normF of b_{1} = NormCoset (X,Y) & RLSStruct(# the carrier of b_{2}, the ZeroF of b_{2}, the addF of b_{2}, the Mult of b_{2} #) = VectQuot (X,Y) & the normF of b_{2} = NormCoset (X,Y) holds

b_{1} = b_{2}
;

end;
let Y be Subspace of X;

assume A1: ex CY being Subset of X st

( CY = the carrier of Y & CY is closed ) ;

func NVectQuot (X,Y) -> strict RealNormSpace means :defQuotN: :: NORMSP_3:def 19

( RLSStruct(# the carrier of it, the ZeroF of it, the addF of it, the Mult of it #) = VectQuot (X,Y) & the normF of it = NormCoset (X,Y) );

existence ( RLSStruct(# the carrier of it, the ZeroF of it, the addF of it, the Mult of it #) = VectQuot (X,Y) & the normF of it = NormCoset (X,Y) );

ex b

( RLSStruct(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem defQuotN defines NVectQuot NORMSP_3:def 19 :

for X being RealNormSpace

for Y being Subspace of X st ex CY being Subset of X st

( CY = the carrier of Y & CY is closed ) holds

for b_{3} being strict RealNormSpace holds

( b_{3} = NVectQuot (X,Y) iff ( RLSStruct(# the carrier of b_{3}, the ZeroF of b_{3}, the addF of b_{3}, the Mult of b_{3} #) = VectQuot (X,Y) & the normF of b_{3} = NormCoset (X,Y) ) );

for X being RealNormSpace

for Y being Subspace of X st ex CY being Subset of X st

( CY = the carrier of Y & CY is closed ) holds

for b

( b

theorem :: NORMSP_3:67

for V, W being RealNormSpace

for L being Lipschitzian LinearOperator of V,W ex QL being Lipschitzian LinearOperator of (NVectQuot (V,(Ker L))),(Im L) ex PQL being Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) ex PL being Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) st

( QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & ( for z being Point of (NVectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

for L being Lipschitzian LinearOperator of V,W ex QL being Lipschitzian LinearOperator of (NVectQuot (V,(Ker L))),(Im L) ex PQL being Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) ex PL being Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) st

( QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & ( for z being Point of (NVectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

proof end;

LMCL1: for X being RealNormSpace

for Y, Z being Subset of X st Z = the carrier of (Lin Y) holds

not Cl Z is empty

proof end;

definition

let X be RealNormSpace;

let Y be Subset of X;

existence

ex b_{1} being non empty NORMSTR ex Z being Subset of X st

( Z = the carrier of (Lin Y) & b_{1} = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) );

uniqueness

for b_{1}, b_{2} being non empty NORMSTR st ex Z being Subset of X st

( Z = the carrier of (Lin Y) & b_{1} = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) & ex Z being Subset of X st

( Z = the carrier of (Lin Y) & b_{2} = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) holds

b_{1} = b_{2};

end;
let Y be Subset of X;

func ClNLin Y -> non empty NORMSTR means :defClN: :: NORMSP_3:def 20

ex Z being Subset of X st

( Z = the carrier of (Lin Y) & it = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) );

correctness ex Z being Subset of X st

( Z = the carrier of (Lin Y) & it = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) );

existence

ex b

( Z = the carrier of (Lin Y) & b

uniqueness

for b

( Z = the carrier of (Lin Y) & b

( Z = the carrier of (Lin Y) & b

b

proof end;

:: deftheorem defClN defines ClNLin NORMSP_3:def 20 :

for X being RealNormSpace

for Y being Subset of X

for b_{3} being non empty NORMSTR holds

( b_{3} = ClNLin Y iff ex Z being Subset of X st

( Z = the carrier of (Lin Y) & b_{3} = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) );

for X being RealNormSpace

for Y being Subset of X

for b

( b

( Z = the carrier of (Lin Y) & b

theorem RSSPACE11: :: NORMSP_3:68

for X being RealNormSpace

for V1, CL being Subset of X st CL = the carrier of (ClNLin V1) holds

RLSStruct(# CL,(Zero_ (CL,X)),(Add_ (CL,X)),(Mult_ (CL,X)) #) is Subspace of X

for V1, CL being Subset of X st CL = the carrier of (ClNLin V1) holds

RLSStruct(# CL,(Zero_ (CL,X)),(Add_ (CL,X)),(Mult_ (CL,X)) #) is Subspace of X

proof end;

SUBTHCL: for V being RealNormSpace

for V1 being Subset of V

for x, y being Point of V

for x1, y1 being Point of (ClNLin V1)

for a being Real st x = x1 & y = y1 holds

( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )

proof end;

theorem CLTh37: :: NORMSP_3:69

for X being RealNormSpace

for Y being Subset of X

for f, g being Point of (ClNLin Y)

for a being Real holds

( ( ||.f.|| = 0 implies f = 0. (ClNLin Y) ) & ( f = 0. (ClNLin Y) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

for Y being Subset of X

for f, g being Point of (ClNLin Y)

for a being Real holds

( ( ||.f.|| = 0 implies f = 0. (ClNLin Y) ) & ( f = 0. (ClNLin Y) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

proof end;

registration

let X be RealNormSpace;

let Y be Subset of X;

correctness

coherence

( ClNLin Y is reflexive & ClNLin Y is discerning & ClNLin Y is RealNormSpace-like );

by CLTh37;

end;
let Y be Subset of X;

correctness

coherence

( ClNLin Y is reflexive & ClNLin Y is discerning & ClNLin Y is RealNormSpace-like );

by CLTh37;

registration

let X be RealNormSpace;

let Y be Subset of X;

( ClNLin Y is reflexive & ClNLin Y is discerning & ClNLin Y is RealNormSpace-like & ClNLin Y is vector-distributive & ClNLin Y is scalar-distributive & ClNLin Y is scalar-associative & ClNLin Y is scalar-unital & ClNLin Y is Abelian & ClNLin Y is add-associative & ClNLin Y is right_zeroed & ClNLin Y is right_complementable ) by CLTh39;

end;
let Y be Subset of X;

cluster ClNLin Y -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;

coherence ( ClNLin Y is reflexive & ClNLin Y is discerning & ClNLin Y is RealNormSpace-like & ClNLin Y is vector-distributive & ClNLin Y is scalar-distributive & ClNLin Y is scalar-associative & ClNLin Y is scalar-unital & ClNLin Y is Abelian & ClNLin Y is add-associative & ClNLin Y is right_zeroed & ClNLin Y is right_complementable ) by CLTh39;

definition

let V be RealNormSpace;

let V1 be Subset of V;

:: original: ClNLin

redefine func ClNLin V1 -> SubRealNormSpace of V;

coherence

ClNLin V1 is SubRealNormSpace of V by CLTh40;

end;
let V1 be Subset of V;

:: original: ClNLin

redefine func ClNLin V1 -> SubRealNormSpace of V;

coherence

ClNLin V1 is SubRealNormSpace of V by CLTh40;