:: Topological Properties of Real Normed Space
:: by Kazuhisa Nakasho , Yuichi Futa and Yasunari Shidama
::
:: Received September 15, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users


registration
let X be RealNormSpace;
cluster closed open for Element of bool the carrier of X;
correctness
existence
ex b1 being Subset of X st
( b1 is open & b1 is closed );
proof end;
end;

theorem :: NORMSP_3:1
for X being RealNormSpace
for R being Subset of X holds
( R is closed iff R ` is open ) ;

registration
let X be RealNormSpace;
let R be closed Subset of X;
cluster R ` -> open ;
correctness
coherence
R ` is open ;
;
end;

theorem Th0: :: NORMSP_3:2
for X being RealNormSpace
for R being Subset of X holds
( R is open iff R ` is closed ) ;

registration
let X be RealNormSpace;
let R be open Subset of X;
cluster R ` -> closed ;
correctness
coherence
R ` is closed ;
by Th0;
end;

registration
let X be RealNormSpace;
cluster [#] X -> closed ;
correctness
coherence
[#] X is closed ;
;
cluster {} X -> closed ;
correctness
coherence
{} X is closed ;
;
cluster [#] X -> open ;
correctness
coherence
[#] X is open ;
proof end;
cluster {} X -> open ;
correctness
coherence
{} X is open ;
proof end;
end;

registration
let X be RealNormSpace;
let P, Q be closed Subset of X;
cluster P /\ Q -> closed for Subset of X;
correctness
coherence
for b1 being Subset of X st b1 = P /\ Q holds
b1 is closed ;
proof end;
cluster P \/ Q -> closed for Subset of X;
correctness
coherence
for b1 being Subset of X st b1 = P \/ Q holds
b1 is closed ;
proof end;
end;

registration
let X be RealNormSpace;
let P, Q be open Subset of X;
cluster P /\ Q -> open for Subset of X;
correctness
coherence
for b1 being Subset of X st b1 = P /\ Q holds
b1 is open ;
proof end;
cluster P \/ Q -> open for Subset of X;
correctness
coherence
for b1 being Subset of X st b1 = P \/ Q holds
b1 is open ;
proof end;
end;

definition
let X be RealNormSpace;
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
existence
ex b1 being Subset of X ex Z being Subset of (LinearTopSpaceNorm X) st
( Z = Y & b1 = Cl Z );
uniqueness
for b1, b2 being Subset of X st ex Z being Subset of (LinearTopSpaceNorm X) st
( Z = Y & b1 = Cl Z ) & ex Z being Subset of (LinearTopSpaceNorm X) st
( Z = Y & b2 = Cl Z ) holds
b1 = b2;
proof end;
end;

:: deftheorem defcl defines Cl NORMSP_3:def 1 :
for X being RealNormSpace
for Y, b3 being Subset of X holds
( b3 = Cl Y iff ex Z being Subset of (LinearTopSpaceNorm X) st
( Z = Y & b3 = Cl Z ) );

registration
let X be RealNormSpace;
let Y be Subset of X;
cluster Cl Y -> closed ;
correctness
coherence
Cl Y is closed ;
proof end;
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
proof end;

theorem PRETOPC18: :: NORMSP_3:4
for X being RealNormSpace
for Z being Subset of X holds Z c= 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 )
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 ) )
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 )
proof end;

theorem :: NORMSP_3:8
for X being RealNormSpace
for A, B being Subset of X st A c= B holds
Cl A c= Cl B
proof end;

theorem :: NORMSP_3:9
for X being RealNormSpace
for A, B being Subset of X holds Cl (A \/ B) = (Cl A) \/ (Cl B)
proof end;

theorem :: NORMSP_3:10
for X being RealNormSpace
for A, B being Subset of X holds Cl (A /\ B) c= (Cl A) /\ (Cl B)
proof end;

theorem :: NORMSP_3:11
for X being RealNormSpace
for A being Subset of X holds
( A is closed iff Cl A = A )
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 )
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
proof end;

definition
let X be RealNormSpace;
let A be Subset of X;
attr A is dense means :: NORMSP_3:def 2
 Cl A = [#] X;
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 );

registration
let X be RealNormSpace;
cluster [#] X -> dense ;
correctness
coherence
[#] X is dense ;
proof end;
end;

registration
let X be RealNormSpace;
cluster closed open dense for Element of bool the carrier of X;
correctness
existence
ex b1 being Subset of X st
( b1 is open & b1 is closed & b1 is dense );
proof end;
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 ) )
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 )
proof end;

theorem :: NORMSP_3:16
for X being RealNormSpace
for R, S being Subset of X st R is dense & R c= S holds
S 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 )
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)
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
proof end;

theorem NONEMP: :: NORMSP_3:20
for X being RealNormSpace
for A being Subset of X st A is dense holds
not A is empty
proof end;

definition
let X be RealNormSpace;
attr X is separable means :: NORMSP_3:def 3
 LinearTopSpaceNorm X is separable ;
end;

:: deftheorem defines separable NORMSP_3:def 3 :
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 )
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
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 )
proof end;

theorem :: NORMSP_3:24
for X being RealNormSpace
for x being Point of X holds {x} is closed
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
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 #)
proof end;

theorem :: NORMSP_3:27
for V being RealNormSpace
for W being SubRealNormSpace of V holds W is Subspace 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 )
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
proof end;

definition
let X be RealNormSpace;
let X1 be set ;
assume A1: X1 c= the carrier of X ;
func Norm_ (X1,X) -> Function of X1,REAL equals :DefNorm: :: NORMSP_3:def 4
 the normF of X | X1;
correctness
coherence
the normF of X | X1 is Function of X1,REAL;
proof end;
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;

definition
let V be RealNormSpace;
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
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;

:: 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)) #);

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;

theorem ThSubSpace: :: NORMSP_3:30
for V being RealNormSpace
for V1 being Subset of V holds NLin V1 is SubRealNormSpace of V
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;

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
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 #)
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
proof end;

registration
let X, Y be RealLinearSpace;
let f be LinearOperator of X,Y;
cluster f " {(0. Y)} -> non empty ;
correctness
coherence
not f " {(0. Y)} is empty ;
by KERX1;
end;

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
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
proof end;

definition
let X, Y be RealLinearSpace;
let f be LinearOperator of X,Y;
func Ker f -> Subspace of X equals :: NORMSP_3:def 6
 Lin (f " {(0. Y)});
coherence
Lin (f " {(0. Y)}) is Subspace of X ;
end;

:: 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)});

definition
let X, Y be RealNormSpace;
let f be LinearOperator of X,Y;
func NKer f -> SubRealNormSpace of X equals :: NORMSP_3:def 7
 NLin (f " {(0. Y)});
coherence
NLin (f " {(0. Y)}) is SubRealNormSpace of X ;
end;

:: 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)});

definition
let X, Y be RealLinearSpace;
let f be LinearOperator of X,Y;
func Im f -> Subspace of Y equals :: NORMSP_3:def 8
 Lin (rng f);
coherence
Lin (rng f) is Subspace of Y ;
end;

:: 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);

definition
let X, Y be RealNormSpace;
let f be LinearOperator of X,Y;
func Im f -> SubRealNormSpace of Y equals :: NORMSP_3:def 9
 NLin (rng f);
coherence
NLin (rng f) is SubRealNormSpace of Y ;
end;

:: 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);

definition
let X, Y be RealLinearSpace;
let L be LinearOperator of X,Y;
attr L is isomorphism means :: NORMSP_3:def 10
( L is one-to-one & L is onto );
end;

:: 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 ) );

registration
let X, Y be RealLinearSpace;
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 b1 being LinearOperator of X,Y st b1 is isomorphism holds
( b1 is one-to-one & b1 is onto ) ;
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 b1 being LinearOperator of X,Y st b1 is one-to-one & b1 is onto holds
b1 is isomorphism ;
end;

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 )
proof end;

definition
let X, Y be RealNormSpace;
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).|| ) );
end;

:: 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).|| ) ) );

registration
let X, Y be RealNormSpace;
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 b1 being LinearOperator of X,Y st b1 is isomorphism holds
( b1 is one-to-one & b1 is onto ) ;
end;

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 )
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) )
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
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;

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 )
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
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 )
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 )
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 )
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 #)
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
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
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
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;
proof end;
end;

definition
let X be RealLinearSpace;
let Y be Subspace of X;
func VectQuot (X,Y) -> RealLinearSpace equals :: NORMSP_3:def 12
 RVSp2RLSp (VectQuot ((RLSp2RVSp X),(RLSp2RVSp Y)));
correctness
coherence
RVSp2RLSp (VectQuot ((RLSp2RVSp X),(RLSp2RVSp Y))) is RealLinearSpace;
;
end;

:: 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)));

theorem :: NORMSP_3:50
for X being RealLinearSpace
for v being Element of X
for a being Real
for v1 being Element of (RLSp2RVSp X)
for a1 being Element of F_Real st v = v1 & a = a1 holds
a * v = a1 * v1 ;

theorem :: NORMSP_3:51
for X being VectSp of F_Real
for v being Element of X
for a being Element of F_Real
for v1 being Element of (RVSp2RLSp X)
for a1 being Real st v = v1 & a = a1 holds
a * v = a1 * v1 ;

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)
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 )
proof end;

definition
let X be RealLinearSpace;
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
coherence
{ A where A is Coset of Y : verum } is non empty Subset-Family of X;
proof end;
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 } ;

definition
let V be RealLinearSpace;
let W be Subspace of V;
func zeroCoset (V,W) -> Element of CosetSet (V,W) equals :: NORMSP_3:def 14
 the carrier of W;
coherence
the carrier of W is Element of CosetSet (V,W)
proof end;
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;

theorem LMQ05: :: NORMSP_3:54
for X being RealLinearSpace
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)
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 )
proof end;

theorem LMQ08: :: NORMSP_3:57
for V being RealLinearSpace
for W being Subspace of V holds 0. (VectQuot (V,W)) = zeroCoset (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
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
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
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
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 )
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 ) )
proof end;

definition
let V be RealLinearSpace;
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
ex b1 being LinearOperator of V,(VectQuot (V,W)) st
( b1 is onto & ( for v being VECTOR of V holds b1 . v = v + W ) ) by LMQ20;
uniqueness
for b1, b2 being LinearOperator of V,(VectQuot (V,W)) st b1 is onto & ( for v being VECTOR of V holds b1 . v = v + W ) & b2 is onto & ( for v being VECTOR of V holds b2 . v = v + W ) holds
b1 = b2
proof end;
end;

:: deftheorem defDQuot defines InducedSur NORMSP_3:def 15 :
for V being RealLinearSpace
for W being Subspace of V
for b3 being LinearOperator of V,(VectQuot (V,W)) holds
( b3 = InducedSur (V,W) iff ( b3 is onto & ( for v being VECTOR of V holds b3 . v = v + W ) ) );

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 ) )
proof end;

definition
let V, W be RealLinearSpace;
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
ex b1 being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st
( b1 is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
b1 . z = L . v ) ) by LMQ21;
uniqueness
for b1, b2 being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st b1 is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
b1 . z = L . v ) & b2 is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
b2 . z = L . v ) holds
b1 = b2
proof end;
end;

:: deftheorem defQuotR defines InducedBi NORMSP_3:def 16 :
for V, W being RealLinearSpace
for L being LinearOperator of V,W
for b4 being LinearOperator of (VectQuot (V,(Ker L))),(Im L) holds
( b4 = InducedBi (V,W,L) iff ( b4 is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
b4 . z = L . v ) ) );

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)))
proof end;

definition
let V be RealNormSpace;
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
coherence
{ ||.x.|| where x is VECTOR of V : x in v + W } is non empty Subset of REAL;
proof end;
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 } ;

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;
cluster NormVSets (V,W,v) -> non empty bounded_below ;
correctness
coherence
( not NormVSets (V,W,v) is empty & NormVSets (V,W,v) is bounded_below );
by LMQ231;
end;

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.|| )
proof end;

definition
let V be RealNormSpace;
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
ex b1 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
b1 . A = lower_bound (NormVSets (V,W,v))
proof end;
uniqueness
for b1, b2 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
b1 . 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
b2 . A = lower_bound (NormVSets (V,W,v)) ) holds
b1 = b2
proof end;
end;

:: deftheorem DeNorm defines NormCoset NORMSP_3:def 18 :
for V being RealNormSpace
for W being Subspace of V
for b3 being Function of (CosetSet (V,W)),REAL holds
( b3 = NormCoset (V,W) iff for A being Element of CosetSet (V,W)
for v being VECTOR of V st A = v + W holds
b3 . A = lower_bound (NormVSets (V,W,v)) );

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 ) ;
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
ex b1 being strict RealNormSpace st
( RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = VectQuot (X,Y) & the normF of b1 = NormCoset (X,Y) )
proof end;
uniqueness
for b1, b2 being strict RealNormSpace st RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = VectQuot (X,Y) & the normF of b1 = NormCoset (X,Y) & RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = VectQuot (X,Y) & the normF of b2 = NormCoset (X,Y) holds
b1 = b2 ;
end;

:: 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 b3 being strict RealNormSpace holds
( b3 = NVectQuot (X,Y) iff ( RLSStruct(# the carrier of b3, the ZeroF of b3, the addF of b3, the Mult of b3 #) = VectQuot (X,Y) & the normF of b3 = NormCoset (X,Y) ) );

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 ) )
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;
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
existence
ex b1 being non empty NORMSTR ex Z being Subset of X st
( Z = the carrier of (Lin Y) & b1 = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) );
uniqueness
for b1, b2 being non empty NORMSTR st ex Z being Subset of X st
( Z = the carrier of (Lin Y) & b1 = 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) & b2 = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) holds
b1 = b2;
proof end;
end;

:: deftheorem defClN defines ClNLin NORMSP_3:def 20 :
for X being RealNormSpace
for Y being Subset of X
for b3 being non empty NORMSTR holds
( b3 = ClNLin Y iff ex Z being Subset of X st
( Z = the carrier of (Lin Y) & b3 = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) );

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
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.|| )
proof end;

registration
let X be RealNormSpace;
let Y be Subset of X;
cluster ClNLin Y -> non empty discerning reflexive RealNormSpace-like ;
correctness
coherence
( ClNLin Y is reflexive & ClNLin Y is discerning & ClNLin Y is RealNormSpace-like );
by CLTh37;
end;

theorem CLTh39: :: NORMSP_3:70
for V being RealNormSpace
for V1 being Subset of V holds ClNLin V1 is RealNormSpace
proof end;

registration
let X be RealNormSpace;
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;
end;

theorem CLTh40: :: NORMSP_3:71
for V being RealNormSpace
for V1 being Subset of V holds ClNLin V1 is SubRealNormSpace of V
proof end;

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;