let X be RealHilbertSpace; :: thesis: 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 )
let M be Subspace of X; :: thesis: 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 )
let N be Subset of X; :: thesis: 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 )
let x be Point of X; :: thesis: 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 )
let d be Real; :: thesis: ( 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 ) implies ex x0 being Point of X st
( d = ||.(x - x0).|| & x0 in M ) )
assume that
A1: ( N = the carrier of M & N is closed ) and
A2: 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 ) ; :: thesis: ex x0 being Point of X st
( d = ||.(x - x0).|| & x0 in M )
consider Y being non empty Subset of REAL such that
A3: ( Y = { ||.(x - y).|| where y is Point of X : y in M } & d = lower_bound Y & lower_bound Y >= 0 ) by A2;
reconsider r0 = 0 as Real ;
for r being ExtReal st r in Y holds
r0 <= r then r0 is LowerBound of Y by XXREAL_2:def 2;
then A4: Y is bounded_below ;
defpred S₁[ Nat, Real] means ( $2 in Y & $2 < d + (1 / ($1 + 1)) );
F1: for n being Element of NAT ex r being Element of REAL st S₁[n,r] consider S being Function of NAT,REAL such that
B3: for n being Element of NAT holds S₁[n,S . n] from FUNCT_2:sch 3(F1);
B4: for n being Nat holds |.((S . n) - d).| <= 1 / (n + 1) B5: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((S . m) - d).| < p then A5: S is convergent ;
then A6: lim S = d by SEQ_2:def 7, B5;
defpred S₂[ Nat, Point of X] means ( $2 in M & S . $1 = ||.(x - $2).|| );
F2: for n being Element of NAT ex v being Point of X st S₂[n,v] consider z being Function of NAT, the carrier of X such that
A7: for n being Element of NAT holds S₂[n,z . n] from FUNCT_2:sch 3(F2);
for n being Nat holds
( z . n in M & S . n = ||.(x - (z . n)).|| ) then consider z being sequence of X such that
A8: for n being Nat holds
( z . n in M & S . n = ||.(x - (z . n)).|| ) ;
reconsider S1 = S (#) S, S2 = S (#) S as Real_Sequence ;
reconsider SA = 2 (#) S1, SB = 2 (#) S2 as Real_Sequence ;
C3: lim S1 = d * d by A6, A5, SEQ_2:15;
C4: lim S2 = d * d by A6, A5, SEQ_2:15;
C5: lim SA = 2 * (d * d) by C3, A5, SEQ_2:8;
C6: lim SB = 2 * (d * d) by C4, A5, SEQ_2:8;
A12: for e being Real st 0 < e holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
|.(((SA . m) + (SB . n)) - (4 * (d * d))).| < e for p being Real st p > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((z . n) - (z . m)).|| < p then A13: z is convergent by BHSP_3:def 4, BHSP_3:2;
then consider x0 being Point of X such that
A14: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((z . n) - x0).|| < r by BHSP_2:9;
lim z = x0 by A13, A14, BHSP_2:19;
then A16: lim ||.(z - x).|| = ||.(x0 - x).|| by A13, BHSP_2:34
.= ||.(- (x0 - x)).|| by BHSP_1:31
.= ||.(x - x0).|| by RLVECT_1:33 ;
for y being object st y in rng z holds
y in N then rng z c= N ;
then BX: lim z in N by A1, A13, LM1;
ex k0 being Nat st
for n being Nat st k0 <= n holds
S . n = ||.(z - x).|| . n then BY: lim S = lim ||.(z - x).|| by A5, SEQ_4:19;
take x0 ; :: thesis: ( d = ||.(x - x0).|| & x0 in M )
thus ( d = ||.(x - x0).|| & x0 in M ) by BX, A1, A13, A14, BHSP_2:19, BY, SEQ_2:def 7, B5, A16, A5; :: thesis: verum