:: by Keiko Narita , Noboru Endou and Yasunari Shidama

::

:: Received July 1, 2015

:: Copyright (c) 2015-2016 Association of Mizar Users

definition

let X be RealUnitarySpace;

ex b_{1} being Function of the carrier of X,REAL st

for x being Point of X holds b_{1} . x = ||.x.||

for b_{1}, b_{2} being Function of the carrier of X,REAL st ( for x being Point of X holds b_{1} . x = ||.x.|| ) & ( for x being Point of X holds b_{2} . x = ||.x.|| ) holds

b_{1} = b_{2}

end;
func normRU X -> Function of the carrier of X,REAL means :Def1: :: DUALSP04:def 1

for x being Point of X holds it . x = ||.x.||;

existence for x being Point of X holds it . x = ||.x.||;

ex b

for x being Point of X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines normRU DUALSP04:def 1 :

for X being RealUnitarySpace

for b_{2} being Function of the carrier of X,REAL holds

( b_{2} = normRU X iff for x being Point of X holds b_{2} . x = ||.x.|| );

for X being RealUnitarySpace

for b

( b

Lm01: for X being RealUnitarySpace holds NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #) is RealNormSpace

proof end;

definition

let X be RealUnitarySpace;

coherence

NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #) is RealNormSpace;

by Lm01;

end;
func RUSp2RNSp X -> RealNormSpace equals :: DUALSP04:def 2

NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #);

correctness NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #);

coherence

NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #) is RealNormSpace;

by Lm01;

:: deftheorem defines RUSp2RNSp DUALSP04:def 2 :

for X being RealUnitarySpace holds RUSp2RNSp X = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #);

for X being RealUnitarySpace holds RUSp2RNSp X = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #);

theorem RHS3: :: DUALSP04:1

for X being RealUnitarySpace

for x being Point of X

for x1 being Point of (RUSp2RNSp X) st x = x1 holds

- x = - x1

for x being Point of X

for x1 being Point of (RUSp2RNSp X) st x = x1 holds

- x = - x1

proof end;

theorem RHS8: :: DUALSP04:4

for X being RealUnitarySpace

for s1 being sequence of X

for s2 being sequence of (RUSp2RNSp X) st s1 = s2 holds

( s1 is convergent iff s2 is convergent )

for s1 being sequence of X

for s2 being sequence of (RUSp2RNSp X) st s1 = s2 holds

( s1 is convergent iff s2 is convergent )

proof end;

theorem RHS9: :: DUALSP04:5

for X being RealUnitarySpace

for s1 being sequence of X

for s2 being sequence of (RUSp2RNSp X) st s1 = s2 & s1 is convergent holds

lim s1 = lim s2

for s1 being sequence of X

for s2 being sequence of (RUSp2RNSp X) st s1 = s2 & s1 is convergent holds

lim s1 = lim s2

proof end;

theorem RHS11a: :: DUALSP04:6

for X being RealUnitarySpace

for s1 being sequence of X

for s2 being sequence of (RUSp2RNSp X) st s1 = s2 holds

( s2 is Cauchy_sequence_by_Norm iff s1 is Cauchy )

for s1 being sequence of X

for s2 being sequence of (RUSp2RNSp X) st s1 = s2 holds

( s2 is Cauchy_sequence_by_Norm iff s1 is Cauchy )

proof end;

registration
end;

:: deftheorem defines open DUALSP04:def 3 :

for X being RealUnitarySpace

for Y being Subset of X holds

( Y is open iff ex Z being Subset of (RUSp2RNSp X) st

( Z = Y & Z is open ) );

for X being RealUnitarySpace

for Y being Subset of X holds

( Y is open iff ex Z being Subset of (RUSp2RNSp X) st

( Z = Y & Z is open ) );

:: deftheorem defines closed DUALSP04:def 4 :

for X being RealUnitarySpace

for Y being Subset of X holds

( Y is closed iff ex Z being Subset of (RUSp2RNSp X) st

( Z = Y & Z is closed ) );

for X being RealUnitarySpace

for Y being Subset of X holds

( Y is closed iff ex Z being Subset of (RUSp2RNSp X) st

( Z = Y & Z is closed ) );

theorem LM1: :: DUALSP04:8

for X being RealUnitarySpace

for Y being Subset of X holds

( Y is closed iff for s being sequence of X st rng s c= Y & s is convergent holds

lim s in Y )

for Y being Subset of X holds

( Y is closed iff for s being sequence of X st rng s c= Y & s is convergent holds

lim s in Y )

proof end;

definition

let X be RealUnitarySpace;

let f be PartFunc of the carrier of X,REAL;

let x0 be Point of X;

end;
let f be PartFunc of the carrier of X,REAL;

let x0 be Point of X;

pred f is_continuous_in x0 means :: DUALSP04:def 5

( x0 in dom f & ( for s1 being sequence of X st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) );

( x0 in dom f & ( for s1 being sequence of X st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) );

:: deftheorem defines is_continuous_in DUALSP04:def 5 :

for X being RealUnitarySpace

for f being PartFunc of the carrier of X,REAL

for x0 being Point of X holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of X st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) );

for X being RealUnitarySpace

for f being PartFunc of the carrier of X,REAL

for x0 being Point of X holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of X st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) );

definition

let X be RealUnitarySpace;

let f be PartFunc of the carrier of X,REAL;

let Y be set ;

end;
let f be PartFunc of the carrier of X,REAL;

let Y be set ;

pred f is_continuous_on Y means :: DUALSP04:def 6

( Y c= dom f & ( for x0 being Point of X st x0 in Y holds

f | Y is_continuous_in x0 ) );

( Y c= dom f & ( for x0 being Point of X st x0 in Y holds

f | Y is_continuous_in x0 ) );

:: deftheorem defines is_continuous_on DUALSP04:def 6 :

for X being RealUnitarySpace

for f being PartFunc of the carrier of X,REAL

for Y being set holds

( f is_continuous_on Y iff ( Y c= dom f & ( for x0 being Point of X st x0 in Y holds

f | Y is_continuous_in x0 ) ) );

for X being RealUnitarySpace

for f being PartFunc of the carrier of X,REAL

for Y being set holds

( f is_continuous_on Y iff ( Y c= dom f & ( for x0 being Point of X st x0 in Y holds

f | Y is_continuous_in x0 ) ) );

theorem LM3B: :: DUALSP04:10

for X being RealUnitarySpace

for f being Function of X,REAL

for g being Function of (RUSp2RNSp X),REAL

for x0 being Point of X

for y0 being Point of (RUSp2RNSp X) st f = g & x0 = y0 holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

for f being Function of X,REAL

for g being Function of (RUSp2RNSp X),REAL

for x0 being Point of X

for y0 being Point of (RUSp2RNSp X) st f = g & x0 = y0 holds

( f is_continuous_in x0 iff g is_continuous_in y0 )

proof end;

theorem LM3C: :: DUALSP04:11

for X being RealUnitarySpace

for f being Function of X,REAL

for g being Function of (RUSp2RNSp X),REAL st f = g holds

( f is_continuous_on the carrier of X iff g is_continuous_on the carrier of (RUSp2RNSp X) )

for f being Function of X,REAL

for g being Function of (RUSp2RNSp X),REAL st f = g holds

( f is_continuous_on the carrier of X iff g is_continuous_on the carrier of (RUSp2RNSp X) )

proof end;

theorem :: DUALSP04:12

for X being RealUnitarySpace

for w being Point of X

for f being Function of X,REAL st ( for v being Point of X holds f . v = w .|. v ) holds

f is_continuous_on the carrier of X

for w being Point of X

for f being Function of X,REAL st ( for v being Point of X holds f . v = w .|. v ) holds

f is_continuous_on the carrier of X

proof end;

:: deftheorem defines is_Lipschitzian_on DUALSP04:def 7 :

for X being RealUnitarySpace

for Y being set

for f being PartFunc of the carrier of X,REAL holds

( f is_Lipschitzian_on Y iff ( Y c= dom f & ex r being Real st

( 0 < r & ( for x1, x2 being Point of X st x1 in Y & x2 in Y holds

|.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| ) ) ) );

for X being RealUnitarySpace

for Y being set

for f being PartFunc of the carrier of X,REAL holds

( f is_Lipschitzian_on Y iff ( Y c= dom f & ex r being Real st

( 0 < r & ( for x1, x2 being Point of X st x1 in Y & x2 in Y holds

|.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| ) ) ) );

theorem LM4: :: DUALSP04:13

for X being RealUnitarySpace

for f being Function of X,REAL

for g being Function of (RUSp2RNSp X),REAL st f = g holds

( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) )

for f being Function of X,REAL

for g being Function of (RUSp2RNSp X),REAL st f = g holds

( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) )

proof end;

theorem LM5: :: DUALSP04:14

for X being RealUnitarySpace

for f being Function of X,REAL st f is_Lipschitzian_on the carrier of X holds

f is_continuous_on the carrier of X

for f being Function of X,REAL st f is_Lipschitzian_on the carrier of X holds

f is_continuous_on the carrier of X

proof end;

Th16: for X being RealUnitarySpace

for f being linear-Functional of X st ( for x being VECTOR of X holds f . x = 0 ) holds

f is Lipschitzian

proof end;

theorem Th21X: :: DUALSP04:15

for X being RealUnitarySpace

for F being linear-Functional of X st F = the carrier of X --> 0 holds

F is Lipschitzian

for F being linear-Functional of X st F = the carrier of X --> 0 holds

F is Lipschitzian

proof end;

registration

let X be RealUnitarySpace;

existence

ex b_{1} being linear-Functional of X st b_{1} is Lipschitzian ;

end;
cluster V1() V4( the carrier of X) V5( REAL ) non empty Function-like total quasi_total additive homogeneous V164() V165() V166() Lipschitzian for Element of bool [: the carrier of X,REAL:];

correctness existence

ex b

proof end;

definition

let X be RealUnitarySpace;

ex b_{1} being Subset of (X *') st

for x being set holds

( x in b_{1} iff x is Lipschitzian linear-Functional of X )

for b_{1}, b_{2} being Subset of (X *') st ( for x being set holds

( x in b_{1} iff x is Lipschitzian linear-Functional of X ) ) & ( for x being set holds

( x in b_{2} iff x is Lipschitzian linear-Functional of X ) ) holds

b_{1} = b_{2}

end;
func BoundedLinearFunctionals X -> Subset of (X *') means :Def10: :: DUALSP04:def 8

for x being set holds

( x in it iff x is Lipschitzian linear-Functional of X );

existence for x being set holds

( x in it iff x is Lipschitzian linear-Functional of X );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def10 defines BoundedLinearFunctionals DUALSP04:def 8 :

for X being RealUnitarySpace

for b_{2} being Subset of (X *') holds

( b_{2} = BoundedLinearFunctionals X iff for x being set holds

( x in b_{2} iff x is Lipschitzian linear-Functional of X ) );

for X being RealUnitarySpace

for b

( b

( x in b

Th17: for X being RealUnitarySpace holds BoundedLinearFunctionals X is linearly-closed

proof end;

registration

let X be RealUnitarySpace;

coherence

( not BoundedLinearFunctionals X is empty & BoundedLinearFunctionals X is linearly-closed )

end;
coherence

( not BoundedLinearFunctionals X is empty & BoundedLinearFunctionals X is linearly-closed )

proof end;

definition

let X be RealUnitarySpace;

let f be object ;

In (f,(BoundedLinearFunctionals X)) is Lipschitzian linear-Functional of X by Def10;

end;
let f be object ;

func Bound2Lipschitz (f,X) -> Lipschitzian linear-Functional of X equals :: DUALSP04:def 9

In (f,(BoundedLinearFunctionals X));

coherence In (f,(BoundedLinearFunctionals X));

In (f,(BoundedLinearFunctionals X)) is Lipschitzian linear-Functional of X by Def10;

:: deftheorem defines Bound2Lipschitz DUALSP04:def 9 :

for X being RealUnitarySpace

for f being object holds Bound2Lipschitz (f,X) = In (f,(BoundedLinearFunctionals X));

for X being RealUnitarySpace

for f being object holds Bound2Lipschitz (f,X) = In (f,(BoundedLinearFunctionals X));

definition

let X be RealUnitarySpace;

let u be linear-Functional of X;

{ |.(u . t).| where t is VECTOR of X : ||.t.|| <= 1 } is non empty Subset of REAL

end;
let u be linear-Functional of X;

func PreNorms u -> non empty Subset of REAL equals :: DUALSP04:def 10

{ |.(u . t).| where t is VECTOR of X : ||.t.|| <= 1 } ;

coherence { |.(u . t).| where t is VECTOR of X : ||.t.|| <= 1 } ;

{ |.(u . t).| where t is VECTOR of X : ||.t.|| <= 1 } is non empty Subset of REAL

proof end;

:: deftheorem defines PreNorms DUALSP04:def 10 :

for X being RealUnitarySpace

for u being linear-Functional of X holds PreNorms u = { |.(u . t).| where t is VECTOR of X : ||.t.|| <= 1 } ;

for X being RealUnitarySpace

for u being linear-Functional of X holds PreNorms u = { |.(u . t).| where t is VECTOR of X : ||.t.|| <= 1 } ;

Th27X: for X being RealUnitarySpace

for g being Lipschitzian linear-Functional of X holds PreNorms g is bounded_above

proof end;

registration

let X be RealUnitarySpace;

let g be Lipschitzian linear-Functional of X;

coherence

PreNorms g is bounded_above by Th27X;

end;
let g be Lipschitzian linear-Functional of X;

coherence

PreNorms g is bounded_above by Th27X;

definition

let X be RealUnitarySpace;

ex b_{1} being Function of (BoundedLinearFunctionals X),REAL st

for x being object st x in BoundedLinearFunctionals X holds

b_{1} . x = upper_bound (PreNorms (Bound2Lipschitz (x,X)))

for b_{1}, b_{2} being Function of (BoundedLinearFunctionals X),REAL st ( for x being object st x in BoundedLinearFunctionals X holds

b_{1} . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) ) & ( for x being object st x in BoundedLinearFunctionals X holds

b_{2} . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) ) holds

b_{1} = b_{2}

end;
func BoundedLinearFunctionalsNorm X -> Function of (BoundedLinearFunctionals X),REAL means :Def14: :: DUALSP04:def 11

for x being object st x in BoundedLinearFunctionals X holds

it . x = upper_bound (PreNorms (Bound2Lipschitz (x,X)));

existence for x being object st x in BoundedLinearFunctionals X holds

it . x = upper_bound (PreNorms (Bound2Lipschitz (x,X)));

ex b

for x being object st x in BoundedLinearFunctionals X holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def14 defines BoundedLinearFunctionalsNorm DUALSP04:def 11 :

for X being RealUnitarySpace

for b_{2} being Function of (BoundedLinearFunctionals X),REAL holds

( b_{2} = BoundedLinearFunctionalsNorm X iff for x being object st x in BoundedLinearFunctionals X holds

b_{2} . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) );

for X being RealUnitarySpace

for b

( b

b

Th23: for X being RealUnitarySpace

for f being Lipschitzian linear-Functional of X holds Bound2Lipschitz (f,X) = f

proof end;

registration

let X be RealUnitarySpace;

let f be Lipschitzian linear-Functional of X;

reducibility

Bound2Lipschitz (f,X) = f by Th23;

end;
let f be Lipschitzian linear-Functional of X;

reducibility

Bound2Lipschitz (f,X) = f by Th23;

theorem Th24: :: DUALSP04:16

for X being RealUnitarySpace

for f being Lipschitzian linear-Functional of X holds (BoundedLinearFunctionalsNorm X) . f = upper_bound (PreNorms f)

for f being Lipschitzian linear-Functional of X holds (BoundedLinearFunctionalsNorm X) . f = upper_bound (PreNorms f)

proof end;

definition

let X be RealUnitarySpace;

NORMSTR(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))),(BoundedLinearFunctionalsNorm X) #) is non empty NORMSTR ;

end;
func DualSp X -> non empty NORMSTR equals :: DUALSP04:def 12

NORMSTR(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))),(BoundedLinearFunctionalsNorm X) #);

coherence NORMSTR(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))),(BoundedLinearFunctionalsNorm X) #);

NORMSTR(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))),(BoundedLinearFunctionalsNorm X) #) is non empty NORMSTR ;

:: deftheorem defines DualSp DUALSP04:def 12 :

for X being RealUnitarySpace holds DualSp X = NORMSTR(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))),(BoundedLinearFunctionalsNorm X) #);

for X being RealUnitarySpace holds DualSp X = NORMSTR(# (BoundedLinearFunctionals X),(Zero_ ((BoundedLinearFunctionals X),(X *'))),(Add_ ((BoundedLinearFunctionals X),(X *'))),(Mult_ ((BoundedLinearFunctionals X),(X *'))),(BoundedLinearFunctionalsNorm X) #);

theorem Th26: :: DUALSP04:17

for X being RealUnitarySpace

for f being Point of (DualSp X)

for g being Lipschitzian linear-Functional of X st g = f holds

for t being VECTOR of X holds |.(g . t).| <= ||.f.|| * ||.t.||

for f being Point of (DualSp X)

for g being Lipschitzian linear-Functional of X st g = f holds

for t being VECTOR of X holds |.(g . t).| <= ||.f.|| * ||.t.||

proof end;

theorem LM6A: :: DUALSP04:19

for X being RealUnitarySpace

for f being Function of X,REAL

for g being Function of (RUSp2RNSp X),REAL st f = g holds

( f is additive & f is homogeneous iff ( g is additive & g is homogeneous ) )

for f being Function of X,REAL

for g being Function of (RUSp2RNSp X),REAL st f = g holds

( f is additive & f is homogeneous iff ( g is additive & g is homogeneous ) )

proof end;

theorem LM6B: :: DUALSP04:20

for X being RealUnitarySpace

for f being linear-Functional of X

for g being linear-Functional of (RUSp2RNSp X) st f = g holds

( f is Lipschitzian iff g is Lipschitzian )

for f being linear-Functional of X

for g being linear-Functional of (RUSp2RNSp X) st f = g holds

( f is Lipschitzian iff g is Lipschitzian )

proof end;

theorem LM6: :: DUALSP04:21

for X being RealUnitarySpace holds BoundedLinearFunctionals X = BoundedLinearFunctionals (RUSp2RNSp X)

proof end;

theorem LM8: :: DUALSP04:22

for X being RealUnitarySpace

for u being linear-Functional of X

for v being linear-Functional of (RUSp2RNSp X) st u = v holds

PreNorms u = PreNorms v

for u being linear-Functional of X

for v being linear-Functional of (RUSp2RNSp X) st u = v holds

PreNorms u = PreNorms v

proof end;

theorem LM9: :: DUALSP04:23

for X being RealUnitarySpace holds BoundedLinearFunctionalsNorm X = BoundedLinearFunctionalsNorm (RUSp2RNSp X)

proof end;

theorem :: DUALSP04:27

for X being RealUnitarySpace

for M, N being Subspace of X st the carrier of M c= the carrier of N holds

the carrier of (Ort_Comp N) c= the carrier of (Ort_Comp M)

for M, N being Subspace of X st the carrier of M c= the carrier of N holds

the carrier of (Ort_Comp N) c= the carrier of (Ort_Comp M)

proof end;

theorem :: DUALSP04:28

for X being RealUnitarySpace

for M being Subspace of X holds the carrier of M c= the carrier of (Ort_Comp (Ort_Comp M))

for M being Subspace of X holds the carrier of M c= the carrier of (Ort_Comp (Ort_Comp M))

proof end;

theorem Lm814: :: DUALSP04:29

for X being RealUnitarySpace

for M being Subspace of X

for x being Point of X st x in the carrier of M /\ the carrier of (Ort_Comp M) holds

x = 0. X

for M being Subspace of X

for x being Point of X st x in the carrier of M /\ the carrier of (Ort_Comp M) holds

x = 0. X

proof end;

theorem :: DUALSP04:30

for X being RealUnitarySpace

for M being Subspace of X

for N being non empty Subset of X st N = the carrier of (Ort_Comp M) holds

( N is linearly-closed & N is closed )

for M being Subspace of X

for N being non empty Subset of X st N = the carrier of (Ort_Comp M) holds

( N is linearly-closed & N is closed )

proof end;

Lm88A: for X being RealUnitarySpace

for x, y being Point of X holds (||.(x + y).|| * ||.(x + y).||) + (||.(x - y).|| * ||.(x - y).||) = (2 * (||.x.|| * ||.x.||)) + (2 * (||.y.|| * ||.y.||))

proof end;

theorem Lm88: :: DUALSP04:31

for X being RealHilbertSpace

for M being Subspace of X

for N being Subset of X

for x being Point of X

for d being Real st N = the carrier of M & N is closed & ex Y being non empty Subset of REAL st

( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) holds

ex x0 being Point of X st

( d = ||.(x - x0).|| & x0 in M )

for M being Subspace of X

for N being Subset of X

for x being Point of X

for d being Real st N = the carrier of M & N is closed & ex Y being non empty Subset of REAL st

( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) holds

ex x0 being Point of X st

( d = ||.(x - x0).|| & x0 in M )

proof end;

theorem Lm87A: :: DUALSP04:32

for X being RealHilbertSpace

for M being Subspace of X

for x, x0 being Point of X

for d being Real st x0 in M & ex Y being non empty Subset of REAL st

( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) holds

( d = ||.(x - x0).|| iff for w being Point of X st w in M holds

w,x - x0 are_orthogonal )

for M being Subspace of X

for x, x0 being Point of X

for d being Real st x0 in M & ex Y being non empty Subset of REAL st

( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) holds

( d = ||.(x - x0).|| iff for w being Point of X st w in M holds

w,x - x0 are_orthogonal )

proof end;

theorem Th87A: :: DUALSP04:33

for X being RealHilbertSpace

for M being Subspace of X

for N being Subset of X

for x being Point of X st N = the carrier of M & N is closed holds

ex y, z being Point of X st

( y in M & z in Ort_Comp M & x = y + z )

for M being Subspace of X

for N being Subset of X

for x being Point of X st N = the carrier of M & N is closed holds

ex y, z being Point of X st

( y in M & z in Ort_Comp M & x = y + z )

proof end;

theorem :: DUALSP04:34

for X being RealUnitarySpace

for M being Subspace of X

for x, y1, y2, z1, z2 being Point of X st y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M & x = y1 + z1 & x = y2 + z2 holds

( y1 = y2 & z1 = z2 )

for M being Subspace of X

for x, y1, y2, z1, z2 being Point of X st y1 in M & y2 in M & z1 in Ort_Comp M & z2 in Ort_Comp M & x = y1 + z1 & x = y2 + z2 holds

( y1 = y2 & z1 = z2 )

proof end;

theorem :: DUALSP04:35

for X being RealUnitarySpace

for f being linear-Functional of X

for y being Point of X st ( for x being Point of X holds f . x = x .|. y ) holds

f is Lipschitzian

for f being linear-Functional of X

for y being Point of X st ( for x being Point of X holds f . x = x .|. y ) holds

f is Lipschitzian

proof end;

KERX1: for X being RealUnitarySpace

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

not f " {0} is empty

proof end;

registration

let X be RealUnitarySpace;

let f be linear-Functional of X;

correctness

coherence

not f " {0} is empty ;

by KERX1;

end;
let f be linear-Functional of X;

correctness

coherence

not f " {0} is empty ;

by KERX1;

theorem KLXY1: :: DUALSP04:36

for X being RealUnitarySpace

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

f " {0} is linearly-closed

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

f " {0} is linearly-closed

proof end;

definition

let X be RealUnitarySpace;

let f be linear-Functional of X;

existence

ex b_{1} being strict Subspace of X st the carrier of b_{1} = f " {0}
by KLXY1, RUSUB_1:29;

uniqueness

for b_{1}, b_{2} being strict Subspace of X st the carrier of b_{1} = f " {0} & the carrier of b_{2} = f " {0} holds

b_{1} = b_{2}
by RUSUB_1:24;

end;
let f be linear-Functional of X;

existence

ex b

uniqueness

for b

b

:: deftheorem defuker defines UKer DUALSP04:def 13 :

for X being RealUnitarySpace

for f being linear-Functional of X

for b_{3} being strict Subspace of X holds

( b_{3} = UKer f iff the carrier of b_{3} = f " {0} );

for X being RealUnitarySpace

for f being linear-Functional of X

for b

( b

theorem Lm89A: :: DUALSP04:37

for X being RealUnitarySpace

for f being linear-Functional of X st f is Lipschitzian holds

f " {0} is closed

for f being linear-Functional of X st f is Lipschitzian holds

f " {0} is closed

proof end;

theorem Lm89B: :: DUALSP04:38

for V being RealUnitarySpace

for W being Subspace of V

for v being VECTOR of V st v <> 0. V & v in Ort_Comp W holds

not v in W

for W being Subspace of V

for v being VECTOR of V st v <> 0. V & v in Ort_Comp W holds

not v in W

proof end;

theorem Th89A: :: DUALSP04:39

for X being RealHilbertSpace

for f being linear-Functional of X st f is Lipschitzian holds

ex y being Point of X st

for x being Point of X holds f . x = x .|. y

for f being linear-Functional of X st f is Lipschitzian holds

ex y being Point of X st

for x being Point of X holds f . x = x .|. y

proof end;

theorem :: DUALSP04:40

for X being RealUnitarySpace

for f being linear-Functional of X

for y1, y2 being Point of X st ( for x being Point of X holds

( f . x = x .|. y1 & f . x = x .|. y2 ) ) holds

y1 = y2

for f being linear-Functional of X

for y1, y2 being Point of X st ( for x being Point of X holds

( f . x = x .|. y1 & f . x = x .|. y2 ) ) holds

y1 = y2

proof end;

theorem :: DUALSP04:41

for X being RealHilbertSpace

for f being Point of (DualSp X)

for g being Lipschitzian linear-Functional of X st g = f holds

ex y being Point of X st

( ( for x being Point of X holds g . x = x .|. y ) & ||.f.|| = ||.y.|| )

for f being Point of (DualSp X)

for g being Lipschitzian linear-Functional of X st g = f holds

ex y being Point of X st

( ( for x being Point of X holds g . x = x .|. y ) & ||.f.|| = ||.y.|| )

proof end;