:: 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 b₁ being Subset of X st
( b₁ is open & b₁ 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 b₁ being Subset of X st b₁ = P /\ Q holds
b₁ is closed ;

proof end;

cluster P \/ Q -> closed for Subset of X;

correctness
coherence
for b₁ being Subset of X st b₁ = P \/ Q holds
b₁ 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 b₁ being Subset of X st b₁ = P /\ Q holds
b₁ is open ;

proof end;

cluster P \/ Q -> open for Subset of X;

correctness
coherence
for b₁ being Subset of X st b₁ = P \/ Q holds
b₁ 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 b₁ being Subset of X ex Z being Subset of (LinearTopSpaceNorm X) st
( Z = Y & b₁ = Cl Z );
uniqueness
for b₁, b₂ being Subset of X st ex Z being Subset of (LinearTopSpaceNorm X) st
( Z = Y & b₁ = Cl Z ) & ex Z being Subset of (LinearTopSpaceNorm X) st
( Z = Y & b₂ = Cl Z ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem defcl defines Cl NORMSP_3:def 1 :
for X being RealNormSpace
for Y, b₃ being Subset of X holds
( b₃ = Cl Y iff ex Z being Subset of (LinearTopSpaceNorm X) st
( Z = Y & b₃ = 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 b₁ being Subset of X st
( b₁ is open & b₁ is closed & b₁ 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 b₁ being LinearOperator of X,Y st b₁ is isomorphism holds
( b₁ is one-to-one & b₁ 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 b₁ being LinearOperator of X,Y st b₁ is one-to-one & b₁ is onto holds
b₁ 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 b₁ being LinearOperator of X,Y st b₁ is isomorphism holds
( b₁ is one-to-one & b₁ 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 b₁ being LinearOperator of V,(VectQuot (V,W)) st
( b₁ is onto & ( for v being VECTOR of V holds b₁ . v = v + W ) ) by LMQ20;
uniqueness
for b₁, b₂ being LinearOperator of V,(VectQuot (V,W)) st b₁ is onto & ( for v being VECTOR of V holds b₁ . v = v + W ) & b₂ is onto & ( for v being VECTOR of V holds b₂ . v = v + W ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defDQuot defines InducedSur NORMSP_3:def 15 :
for V being RealLinearSpace
for W being Subspace of V
for b₃ being LinearOperator of V,(VectQuot (V,W)) holds
( b₃ = InducedSur (V,W) iff ( b₃ is onto & ( for v being VECTOR of V holds b₃ . 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 b₁ being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st
( b₁ is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
b₁ . z = L . v ) ) by LMQ21;
uniqueness
for b₁, b₂ being LinearOperator of (VectQuot (V,(Ker L))),(Im L) st b₁ is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
b₁ . z = L . v ) & b₂ is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
b₂ . z = L . v ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defQuotR defines InducedBi NORMSP_3:def 16 :
for V, W being RealLinearSpace
for L being LinearOperator of V,W
for b₄ being LinearOperator of (VectQuot (V,(Ker L))),(Im L) holds
( b₄ = InducedBi (V,W,L) iff ( b₄ is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
b₄ . 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 b₁ 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₁ . A = lower_bound (NormVSets (V,W,v))

proof end;

uniqueness
for b₁, b₂ 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₁ . 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₂ . A = lower_bound (NormVSets (V,W,v)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DeNorm defines NormCoset NORMSP_3:def 18 :
for V being RealNormSpace
for W being Subspace of V
for b₃ being Function of (CosetSet (V,W)),REAL holds
( b₃ = NormCoset (V,W) iff for A being Element of CosetSet (V,W)
for v being VECTOR of V st A = v + W holds
b₃ . 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 b₁ being strict RealNormSpace st
( RLSStruct(# the carrier of b₁, the ZeroF of b₁, the addF of b₁, the Mult of b₁ #) = VectQuot (X,Y) & the normF of b₁ = NormCoset (X,Y) )

proof end;

uniqueness
for b₁, b₂ being strict RealNormSpace st RLSStruct(# the carrier of b₁, the ZeroF of b₁, the addF of b₁, the Mult of b₁ #) = VectQuot (X,Y) & the normF of b₁ = NormCoset (X,Y) & RLSStruct(# the carrier of b₂, the ZeroF of b₂, the addF of b₂, the Mult of b₂ #) = VectQuot (X,Y) & the normF of b₂ = NormCoset (X,Y) holds
b₁ = b₂ ;

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 b₃ being strict RealNormSpace holds
( b₃ = NVectQuot (X,Y) iff ( RLSStruct(# the carrier of b₃, the ZeroF of b₃, the addF of b₃, the Mult of b₃ #) = VectQuot (X,Y) & the normF of b₃ = 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 b₁ being non empty NORMSTR ex Z being Subset of X st
( Z = the carrier of (Lin Y) & b₁ = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) );
uniqueness
for b₁, b₂ being non empty NORMSTR st ex Z being Subset of X st
( Z = the carrier of (Lin Y) & b₁ = 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₂ = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem defClN defines ClNLin NORMSP_3:def 20 :
for X being RealNormSpace
for Y being Subset of X
for b₃ being non empty NORMSTR holds
( b₃ = ClNLin Y iff ex Z being Subset of X st
( Z = the carrier of (Lin Y) & b₃ = 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;