let X be RealHilbertSpace; for M being Subspace of X
for x being Point of X st the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) holds
ex m0 being Point of X st
( m0 in M & ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) )
let M be Subspace of X; for x being Point of X st the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) holds
ex m0 being Point of X st
( m0 in M & ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) )
let x be Point of X; ( the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) implies ex m0 being Point of X st
( m0 in M & ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) ) )
assume A1:
the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X))
; ex m0 being Point of X st
( m0 in M & ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) )
per cases
( x in M or not x in M )
;
suppose
not
x in M
;
ex m0 being Point of X st
( m0 in M & ( for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| ) )set B =
{ ||.(x - m).|| where m is Point of X : m in M } ;
0. X in M
by RUSUB_1:11;
then A4:
||.(x - (0. X)).|| in { ||.(x - m).|| where m is Point of X : m in M }
;
{ ||.(x - m).|| where m is Point of X : m in M } c= REAL
then reconsider B =
{ ||.(x - m).|| where m is Point of X : m in M } as
real-membered set ;
reconsider r0 =
0 as
Real ;
A6:
B is
bounded_below
set delta =
lower_bound B;
reconsider B =
B as non
empty real-membered bounded_below set by A6, A4;
A7:
lower_bound B = inf B
;
r0 is
LowerBound of
B
by A5, XXREAL_2:def 2;
then A8:
r0 <= lower_bound B
by A7, XXREAL_2:def 4;
defpred S1[
Nat,
Real]
means ( $2
in B &
|.($2 - (lower_bound B)).| < 1
/ ($1 + 1) );
A9:
for
n being
Element of
NAT ex
y being
Element of
REAL st
S1[
n,
y]
consider seq being
Function of
NAT,
REAL such that A12:
for
n being
Element of
NAT holds
S1[
n,
seq . n]
from FUNCT_2:sch 3(A9);
reconsider seq =
seq as
Real_Sequence ;
A13:
for
p being
Real st
0 < p holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.((seq . m) - (lower_bound B)).| < p
then A18:
seq is
convergent
;
then
lim seq = lower_bound B
by SEQ_2:def 7, A13;
then A20:
(
seq (#) seq is
convergent &
lim (seq (#) seq) = (lower_bound B) * (lower_bound B) )
by SEQ_2:15, A18;
defpred S2[
Nat,
Point of
X]
means ( $2
in M &
seq . $1
= ||.($2 - x).|| );
A21:
for
n being
Element of
NAT ex
y being
Element of the
carrier of
X st
S2[
n,
y]
consider xseq being
Function of
NAT, the
carrier of
X such that A23:
for
n being
Element of
NAT holds
S2[
n,
xseq . n]
from FUNCT_2:sch 3(A21);
reconsider xseq =
xseq as
sequence of
X ;
for
n being
Element of
NAT holds
seq . n = ||.(xseq - x).|| . n
then A24:
seq = ||.(xseq - x).||
by FUNCT_2:63;
A26:
rng xseq c= the
carrier of
M
for
r being
Real st
r > 0 holds
ex
k being
Nat st
for
n,
m being
Nat st
n >= k &
m >= k holds
||.((xseq . n) - (xseq . m)).|| < r
proof
let r be
Real;
( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < r )
assume A35:
r > 0
;
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < r
set r1 =
r / 2;
A36:
(
0 < r / 2 &
r / 2
< r )
by A35, XREAL_1:216;
set r2 =
(r / 2) / 2;
consider k being
Nat such that A38:
for
i being
Nat st
k <= i holds
|.(((seq (#) seq) . i) - ((lower_bound B) ^2)).| < ((r / 2) / 2) ^2
by SEQ_2:def 7, A20, A35;
take
k
;
for n, m being Nat st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < r
let i,
j be
Nat;
( i >= k & j >= k implies ||.((xseq . i) - (xseq . j)).|| < r )
assume A39:
(
i >= k &
j >= k )
;
||.((xseq . i) - (xseq . j)).|| < r
A40:
||.((xseq . i) - (xseq . j)).|| ^2 <= ((2 * ((seq (#) seq) . i)) + (2 * ((seq (#) seq) . j))) - (4 * ((lower_bound B) ^2))
by A27;
|.(((seq (#) seq) . i) - ((lower_bound B) ^2)).| < ((r / 2) / 2) ^2
by A38, A39;
then
(seq (#) seq) . i in ].(((lower_bound B) ^2) - (((r / 2) / 2) ^2)),(((lower_bound B) ^2) + (((r / 2) / 2) ^2)).[
by RCOMP_1:1;
then
(seq (#) seq) . i in { r where r is Real : ( ((lower_bound B) ^2) - (((r / 2) / 2) ^2) < r & r < ((lower_bound B) ^2) + (((r / 2) / 2) ^2) ) }
by RCOMP_1:def 2;
then
ex
r being
Real st
(
r = (seq (#) seq) . i &
((lower_bound B) ^2) - (((r / 2) / 2) ^2) < r &
r < ((lower_bound B) ^2) + (((r / 2) / 2) ^2) )
;
then A41:
2
* ((seq (#) seq) . i) < 2
* (((lower_bound B) ^2) + (((r / 2) / 2) ^2))
by XREAL_1:68;
|.(((seq (#) seq) . j) - ((lower_bound B) ^2)).| < ((r / 2) / 2) ^2
by A38, A39;
then
(seq (#) seq) . j in ].(((lower_bound B) ^2) - (((r / 2) / 2) ^2)),(((lower_bound B) ^2) + (((r / 2) / 2) ^2)).[
by RCOMP_1:1;
then
(seq (#) seq) . j in { r where r is Real : ( ((lower_bound B) ^2) - (((r / 2) / 2) ^2) < r & r < ((lower_bound B) ^2) + (((r / 2) / 2) ^2) ) }
by RCOMP_1:def 2;
then
ex
r being
Real st
(
r = (seq (#) seq) . j &
((lower_bound B) ^2) - (((r / 2) / 2) ^2) < r &
r < ((lower_bound B) ^2) + (((r / 2) / 2) ^2) )
;
then
2
* ((seq (#) seq) . j) < 2
* (((lower_bound B) ^2) + (((r / 2) / 2) ^2))
by XREAL_1:68;
then
(2 * ((seq (#) seq) . i)) + (2 * ((seq (#) seq) . j)) < ((2 * ((lower_bound B) ^2)) + (2 * (((r / 2) / 2) ^2))) + ((2 * ((lower_bound B) ^2)) + (2 * (((r / 2) / 2) ^2)))
by A41, XREAL_1:8;
then
((2 * ((seq (#) seq) . i)) + (2 * ((seq (#) seq) . j))) - (4 * ((lower_bound B) ^2)) < ((((2 * ((lower_bound B) ^2)) + (2 * (((r / 2) / 2) ^2))) + (2 * ((lower_bound B) ^2))) + (2 * (((r / 2) / 2) ^2))) - (4 * ((lower_bound B) ^2))
by XREAL_1:14;
then A42:
||.((xseq . i) - (xseq . j)).|| ^2 < (2 * ((r / 2) / 2)) ^2
by A40, XXREAL_0:2;
||.((xseq . i) - (xseq . j)).|| <= 2
* ((r / 2) / 2)
by A42, SQUARE_1:16, A35;
hence
||.((xseq . i) - (xseq . j)).|| < r
by A36, XXREAL_0:2;
verum
end; then A43:
xseq is
convergent
by BHSP_3:def 4, BHSP_3:2;
A46:
||.(x - (lim xseq)).|| =
||.(- ((lim xseq) - x)).||
by RLVECT_1:33
.=
||.((lim xseq) - x).||
by BHSP_1:31
.=
lim seq
by A24, A43, BHSP_2:34
.=
lower_bound B
by A18, SEQ_2:def 7, A13
;
take
lim xseq
;
( lim xseq in M & ( for m being Point of X st m in M holds
||.(x - (lim xseq)).|| <= ||.(x - m).|| ) )thus
lim xseq in M
by A43, A26, STRUCT_0:def 5, A1, Th12;
for m being Point of X st m in M holds
||.(x - (lim xseq)).|| <= ||.(x - m).||let m be
Point of
X;
( m in M implies ||.(x - (lim xseq)).|| <= ||.(x - m).|| )assume
m in M
;
||.(x - (lim xseq)).|| <= ||.(x - m).||then
||.(x - m).|| in B
;
hence
||.(x - (lim xseq)).|| <= ||.(x - m).||
by A46, SEQ_4:def 2;
verum end;