let M be non empty Reflexive triangle MetrStruct ; for a being Point of M
for X being non empty set st WellSpace (a,X) is complete holds
M is complete
let a be Point of M; for X being non empty set st WellSpace (a,X) is complete holds
M is complete
let X be non empty set ; ( WellSpace (a,X) is complete implies M is complete )
consider x0 being object such that
A1:
x0 in X
by XBOOLE_0:def 1;
set W = WellSpace (a,X);
assume A2:
WellSpace (a,X) is complete
; M is complete
let S be sequence of M; TBSP_1:def 5 ( not S is Cauchy or S is convergent )
assume A3:
S is Cauchy
; S is convergent
defpred S1[ object , object ] means ( ( S . $1 <> a implies $2 = [x0,(S . $1)] ) & ( S . $1 = a implies $2 = [X,(S . $1)] ) );
A4:
for x being object st x in NAT holds
ex y being object st
( y in the carrier of (WellSpace (a,X)) & S1[x,y] )
proof
let x be
object ;
( x in NAT implies ex y being object st
( y in the carrier of (WellSpace (a,X)) & S1[x,y] ) )
assume
x in NAT
;
ex y being object st
( y in the carrier of (WellSpace (a,X)) & S1[x,y] )
then reconsider i =
x as
Nat ;
per cases
( S . i <> a or S . x = a )
;
suppose A5:
S . i <> a
;
ex y being object st
( y in the carrier of (WellSpace (a,X)) & S1[x,y] )take
[x0,(S . i)]
;
( [x0,(S . i)] in the carrier of (WellSpace (a,X)) & S1[x,[x0,(S . i)]] )thus
(
[x0,(S . i)] in the
carrier of
(WellSpace (a,X)) &
S1[
x,
[x0,(S . i)]] )
by A1, A5, Th37;
verum end; suppose A6:
S . x = a
;
ex y being object st
( y in the carrier of (WellSpace (a,X)) & S1[x,y] )take
[X,a]
;
( [X,a] in the carrier of (WellSpace (a,X)) & S1[x,[X,a]] )thus
(
[X,a] in the
carrier of
(WellSpace (a,X)) &
S1[
x,
[X,a]] )
by A6, Th37;
verum end; end;
end;
consider S9 being sequence of (WellSpace (a,X)) such that
A7:
for x being object st x in NAT holds
S1[x,S9 . x]
from FUNCT_2:sch 1(A4);
S9 is Cauchy
proof
let r be
Real;
TBSP_1:def 4 ( r <= 0 or ex b1 being set st
for b2, b3 being set holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((S9 . b2),(S9 . b3)) ) )
assume
r > 0
;
ex b1 being set st
for b2, b3 being set holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((S9 . b2),(S9 . b3)) )
then consider p being
Nat such that A8:
for
n,
m being
Nat st
p <= n &
p <= m holds
dist (
(S . n),
(S . m))
< r
by A3;
take
p
;
for b1, b2 being set holds
( not p <= b1 or not p <= b2 or not r <= dist ((S9 . b1),(S9 . b2)) )
let n,
m be
Nat;
( not p <= n or not p <= m or not r <= dist ((S9 . n),(S9 . m)) )
assume that A9:
p <= n
and A10:
p <= m
;
not r <= dist ((S9 . n),(S9 . m))
A11:
(
n in NAT &
m in NAT )
by ORDINAL1:def 12;
per cases
( ( S . n = a & S . m = a ) or ( S . n <> a & S . m = a ) or ( S . n = a & S . m <> a ) or ( S . n <> a & S . m <> a ) )
;
suppose A12:
(
S . n = a &
S . m = a )
;
not r <= dist ((S9 . n),(S9 . m))then A13:
[X,(S . m)] = S9 . m
by A7, A11;
[X,(S . n)] = S9 . n
by A7, A12, A11;
then
dist (
(S9 . n),
(S9 . m))
= dist (
(S . n),
(S . m))
by A13, Def10;
hence
not
r <= dist (
(S9 . n),
(S9 . m))
by A8, A9, A10;
verum end; suppose A14:
(
S . n <> a &
S . m = a )
;
not r <= dist ((S9 . n),(S9 . m))then A15:
[X,(S . m)] = S9 . m
by A7, A11;
A16:
dist (
(S . m),
(S . m))
= 0
by METRIC_1:1;
reconsider xx =
x0 as
set by TARSKI:1;
not
xx in xx
;
then A17:
X <> x0
by A1;
[x0,(S . n)] = S9 . n
by A7, A14, A11;
then
dist (
(S9 . n),
(S9 . m))
= (dist ((S . n),(S . m))) + (dist ((S . m),(S . m)))
by A14, A15, A17, Def10;
hence
not
r <= dist (
(S9 . n),
(S9 . m))
by A8, A9, A10, A16;
verum end; suppose A18:
(
S . n = a &
S . m <> a )
;
not r <= dist ((S9 . n),(S9 . m))then A19:
[x0,(S . m)] = S9 . m
by A7, A11;
A20:
dist (
(S . n),
(S . n))
= 0
by METRIC_1:1;
reconsider xx =
x0 as
set by TARSKI:1;
not
xx in xx
;
then A21:
X <> x0
by A1;
[X,(S . n)] = S9 . n
by A7, A18, A11;
then
dist (
(S9 . n),
(S9 . m))
= (dist ((S . n),(S . n))) + (dist ((S . n),(S . m)))
by A18, A19, A21, Def10;
hence
not
r <= dist (
(S9 . n),
(S9 . m))
by A8, A9, A10, A20;
verum end; suppose A22:
(
S . n <> a &
S . m <> a )
;
not r <= dist ((S9 . n),(S9 . m))then A23:
[x0,(S . m)] = S9 . m
by A7, A11;
[x0,(S . n)] = S9 . n
by A7, A22, A11;
then
dist (
(S9 . n),
(S9 . m))
= dist (
(S . n),
(S . m))
by A23, Def10;
hence
not
r <= dist (
(S9 . n),
(S9 . m))
by A8, A9, A10;
verum end; end;
end;
then
S9 is convergent
by A2;
then consider L being Element of (WellSpace (a,X)) such that
A24:
for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S9 . m),L) < r
;
consider L1 being set , L2 being Point of M such that
A25:
L = [L1,L2]
and
( ( L1 in X & L2 <> a ) or ( L1 = X & L2 = a ) )
by Th37;
take
L2
; TBSP_1:def 2 for b1 being object holds
( b1 <= 0 or ex b2 being set st
for b3 being set holds
( not b2 <= b3 or not b1 <= dist ((S . b3),L2) ) )
let r be Real; ( r <= 0 or ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not r <= dist ((S . b2),L2) ) )
assume
r > 0
; ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not r <= dist ((S . b2),L2) )
then consider n being Nat such that
A26:
for m being Nat st n <= m holds
dist ((S9 . m),L) < r
by A24;
take
n
; for b1 being set holds
( not n <= b1 or not r <= dist ((S . b1),L2) )
let m be Nat; ( not n <= m or not r <= dist ((S . m),L2) )
assume A27:
n <= m
; not r <= dist ((S . m),L2)
A28:
( n in NAT & m in NAT )
by ORDINAL1:def 12;
per cases
( ( S . m = a & L1 = X ) or ( S . m = a & L1 <> X ) or ( S . m <> a & L1 = x0 ) or ( S . m <> a & L1 <> x0 ) )
;
suppose A30:
(
S . m = a &
L1 <> X )
;
not r <= dist ((S . m),L2)then
S9 . m = [X,a]
by A7, A28;
then A31:
dist (
(S9 . m),
L)
= (dist ((S . m),(S . m))) + (dist ((S . m),L2))
by A25, A30, Def10;
dist (
(S . m),
(S . m))
= 0
by METRIC_1:1;
hence
not
r <= dist (
(S . m),
L2)
by A26, A27, A31;
verum end; suppose A33:
(
S . m <> a &
L1 <> x0 )
;
not r <= dist ((S . m),L2)then
S9 . m = [x0,(S . m)]
by A7, A28;
then A34:
dist (
(S9 . m),
L)
= (dist ((S . m),a)) + (dist (a,L2))
by A25, A33, Def10;
A35:
(dist ((S . m),a)) + (dist (a,L2)) >= dist (
(S . m),
L2)
by METRIC_1:4;
dist (
(S9 . m),
L)
< r
by A26, A27;
hence
not
r <= dist (
(S . m),
L2)
by A34, A35, XXREAL_0:2;
verum end; end;