:: BHSP_3 semantic presentation
deffunc H1( RealUnitarySpace) -> M3(the carrier of a1) = 0. a1;
:: deftheorem E1 defines Cauchy BHSP_3:def 1 :
theorem :: BHSP_3:1
theorem :: BHSP_3:2
theorem :: BHSP_3:3
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that E2:
c
2 is_Cauchy_sequence
and E3:
c
3 is_Cauchy_sequence
;
let c
4 be
Real;
:: according to BHSP_3:def 1
assume
c
4 > 0
;
then E4:
c
4 / 2
> 0
by SEQ_2:3;
then consider c
5 being
Nat such that E5:
for b
1, b
2 being
Nat holds
not ( b
1 >= c
5 & b
2 >= c
5 & not
dist (c2 . b1),
(c2 . b2) < c
4 / 2 )
by E2, E1;
consider c
6 being
Nat such that E6:
for b
1, b
2 being
Nat holds
not ( b
1 >= c
6 & b
2 >= c
6 & not
dist (c3 . b1),
(c3 . b2) < c
4 / 2 )
by E3, E4, E1;
take c
7 = c
5 + c
6;
let c
8, c
9 be
Nat;
assume E7:
( c
8 >= c
7 & c
9 >= c
7 )
;
c
5 + c
6 >= c
5
by NAT_1:37;
then
( c
8 >= c
5 & c
9 >= c
5 )
by E7, XXREAL_0:2;
then E8:
dist (c2 . c8),
(c2 . c9) < c
4 / 2
by E5;
c
7 >= c
6
by NAT_1:37;
then
( c
8 >= c
6 & c
9 >= c
6 )
by E7, XXREAL_0:2;
then
dist (c3 . c8),
(c3 . c9) < c
4 / 2
by E6;
then E9:
(dist (c2 . c8),(c2 . c9)) + (dist (c3 . c8),(c3 . c9)) < (c4 / 2) + (c4 / 2)
by E8, XREAL_1:10;
dist ((c2 + c3) . c8),
((c2 + c3) . c9) =
dist ((c2 . c8) + (c3 . c8)),
((c2 + c3) . c9)
by NORMSP_1:def 5
.=
dist ((c2 . c8) + (c3 . c8)),
((c2 . c9) + (c3 . c9))
by NORMSP_1:def 5
;
then
dist ((c2 + c3) . c8),
((c2 + c3) . c9) <= (dist (c2 . c8),(c2 . c9)) + (dist (c3 . c8),(c3 . c9))
by BHSP_1:47;
hence
dist ((c2 + c3) . c8),
((c2 + c3) . c9) < c
4
by E9, XXREAL_0:2;
end;
theorem :: BHSP_3:4
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that E2:
c
2 is_Cauchy_sequence
and E3:
c
3 is_Cauchy_sequence
;
let c
4 be
Real;
:: according to BHSP_3:def 1
assume
c
4 > 0
;
then E4:
c
4 / 2
> 0
by SEQ_2:3;
then consider c
5 being
Nat such that E5:
for b
1, b
2 being
Nat holds
not ( b
1 >= c
5 & b
2 >= c
5 & not
dist (c2 . b1),
(c2 . b2) < c
4 / 2 )
by E2, E1;
consider c
6 being
Nat such that E6:
for b
1, b
2 being
Nat holds
not ( b
1 >= c
6 & b
2 >= c
6 & not
dist (c3 . b1),
(c3 . b2) < c
4 / 2 )
by E3, E4, E1;
take c
7 = c
5 + c
6;
let c
8, c
9 be
Nat;
assume E7:
( c
8 >= c
7 & c
9 >= c
7 )
;
c
5 + c
6 >= c
5
by NAT_1:37;
then
( c
8 >= c
5 & c
9 >= c
5 )
by E7, XXREAL_0:2;
then E8:
dist (c2 . c8),
(c2 . c9) < c
4 / 2
by E5;
c
7 >= c
6
by NAT_1:37;
then
( c
8 >= c
6 & c
9 >= c
6 )
by E7, XXREAL_0:2;
then
dist (c3 . c8),
(c3 . c9) < c
4 / 2
by E6;
then E9:
(dist (c2 . c8),(c2 . c9)) + (dist (c3 . c8),(c3 . c9)) < (c4 / 2) + (c4 / 2)
by E8, XREAL_1:10;
dist ((c2 - c3) . c8),
((c2 - c3) . c9) =
dist ((c2 . c8) - (c3 . c8)),
((c2 - c3) . c9)
by NORMSP_1:def 6
.=
dist ((c2 . c8) - (c3 . c8)),
((c2 . c9) - (c3 . c9))
by NORMSP_1:def 6
;
then
dist ((c2 - c3) . c8),
((c2 - c3) . c9) <= (dist (c2 . c8),(c2 . c9)) + (dist (c3 . c8),(c3 . c9))
by BHSP_1:48;
hence
dist ((c2 - c3) . c8),
((c2 - c3) . c9) < c
4
by E9, XXREAL_0:2;
end;
theorem E2: :: BHSP_3:5
proof
let c
1 be
RealUnitarySpace;
let c
2 be
Real;
let c
3 be
sequence of c
1;
assume E3:
c
3 is_Cauchy_sequence
;
E4:
now
assume E5:
c
2 = 0
;
let c
4 be
Real;
assume
c
4 > 0
;
then consider c
5 being
Nat such that E6:
for b
1, b
2 being
Nat holds
not ( b
1 >= c
5 & b
2 >= c
5 & not
dist (c3 . b1),
(c3 . b2) < c
4 )
by E3, E1;
take c
6 = c
5;
let c
7, c
8 be
Nat;
assume
( c
7 >= c
6 & c
8 >= c
6 )
;
then E7:
dist (c3 . c7),
(c3 . c8) < c
4
by E6;
dist (c2 * (c3 . c7)),
(c2 * (c3 . c8)) =
dist H
1(c
1),
(0 * (c3 . c8))
by E5, RLVECT_1:23
.=
dist H
1(c
1),H
1(c
1)
by RLVECT_1:23
.=
0
by BHSP_1:41
;
then
dist (c2 * (c3 . c7)),
(c2 * (c3 . c8)) < c
4
by E7, BHSP_1:44;
then
dist ((c2 * c3) . c7),
(c2 * (c3 . c8)) < c
4
by NORMSP_1:def 8;
hence
dist ((c2 * c3) . c7),
((c2 * c3) . c8) < c
4
by NORMSP_1:def 8;
end;
now
assume E5:
c
2 <> 0
;
then E6:
abs c
2 > 0
by COMPLEX1:133;
let c
4 be
Real;
assume E7:
c
4 > 0
;
E8:
abs c
2 <> 0
by E5, COMPLEX1:133;
0
/ (abs c2) = 0
;
then
c
4 / (abs c2) > 0
by E6, E7, REAL_1:73;
then consider c
5 being
Nat such that E9:
for b
1, b
2 being
Nat holds
not ( b
1 >= c
5 & b
2 >= c
5 & not
dist (c3 . b1),
(c3 . b2) < c
4 / (abs c2) )
by E3, E1;
take c
6 = c
5;
let c
7, c
8 be
Nat;
assume
( c
7 >= c
6 & c
8 >= c
6 )
;
then E10:
dist (c3 . c7),
(c3 . c8) < c
4 / (abs c2)
by E9;
E11:
dist (c2 * (c3 . c7)),
(c2 * (c3 . c8)) =
||.((c2 * (c3 . c7)) - (c2 * (c3 . c8))).||
by BHSP_1:def 5
.=
||.(c2 * ((c3 . c7) - (c3 . c8))).||
by RLVECT_1:48
.=
(abs c2) * ||.((c3 . c7) - (c3 . c8)).||
by BHSP_1:33
.=
(abs c2) * (dist (c3 . c7),(c3 . c8))
by BHSP_1:def 5
;
(abs c2) * (c4 / (abs c2)) =
(abs c2) * (((abs c2) " ) * c4)
by XCMPLX_0:def 9
.=
((abs c2) * ((abs c2) " )) * c
4
.=
1
* c
4
by E8, XCMPLX_0:def 7
.=
c
4
;
then
dist (c2 * (c3 . c7)),
(c2 * (c3 . c8)) < c
4
by E6, E10, E11, XREAL_1:70;
then
dist ((c2 * c3) . c7),
(c2 * (c3 . c8)) < c
4
by NORMSP_1:def 8;
hence
dist ((c2 * c3) . c7),
((c2 * c3) . c8) < c
4
by NORMSP_1:def 8;
end;
hence
c
2 * c
3 is_Cauchy_sequence
by E4, E1;
end;
theorem :: BHSP_3:6
theorem E3: :: BHSP_3:7
proof
let c
1 be
RealUnitarySpace;
let c
2 be
Point of c
1;
let c
3 be
sequence of c
1;
assume E4:
c
3 is_Cauchy_sequence
;
let c
4 be
Real;
:: according to BHSP_3:def 1
assume
c
4 > 0
;
then consider c
5 being
Nat such that E5:
for b
1, b
2 being
Nat holds
not ( b
1 >= c
5 & b
2 >= c
5 & not
dist (c3 . b1),
(c3 . b2) < c
4 )
by E4, E1;
take c
6 = c
5;
let c
7, c
8 be
Nat;
assume
( c
7 >= c
6 & c
8 >= c
6 )
;
then E6:
dist (c3 . c7),
(c3 . c8) < c
4
by E5;
dist ((c3 . c7) + c2),
((c3 . c8) + c2) <= (dist (c3 . c7),(c3 . c8)) + (dist c2,c2)
by BHSP_1:47;
then
dist ((c3 . c7) + c2),
((c3 . c8) + c2) <= (dist (c3 . c7),(c3 . c8)) + 0
by BHSP_1:41;
then
dist ((c3 . c7) + c2),
((c3 . c8) + c2) < c
4
by E6, XXREAL_0:2;
then
dist ((c3 + c2) . c7),
((c3 . c8) + c2) < c
4
by BHSP_1:def 12;
hence
dist ((c3 + c2) . c7),
((c3 + c2) . c8) < c
4
by BHSP_1:def 12;
end;
theorem :: BHSP_3:8
theorem :: BHSP_3:9
proof
let c
1 be
RealUnitarySpace;
let c
2 be
sequence of c
1;
assume
c
2 is
convergent
;
then consider c
3 being
Point of c
1 such that E4:
for b
1 being
Real holds
not ( b
1 > 0 & ( for b
2 being
Nat holds
ex b
3 being
Nat st
( b
3 >= b
2 & not
dist (c2 . b3),c
3 < b
1 ) ) )
by BHSP_2:def 1;
let c
4 be
Real;
:: according to BHSP_3:def 1
assume
c
4 > 0
;
then
c
4 / 2
> 0
by SEQ_2:3;
then consider c
5 being
Nat such that E5:
for b
1 being
Nat holds
not ( b
1 >= c
5 & not
dist (c2 . b1),c
3 < c
4 / 2 )
by E4;
take c
6 = c
5;
let c
7, c
8 be
Nat;
assume E6:
( c
7 >= c
6 & c
8 >= c
6 )
;
then E7:
dist (c2 . c7),c
3 < c
4 / 2
by E5;
E8:
dist (c2 . c8),c
3 < c
4 / 2
by E5, E6;
E9:
dist (c2 . c7),
(c2 . c8) <= (dist (c2 . c7),c3) + (dist c3,(c2 . c8))
by BHSP_1:42;
(dist (c2 . c7),c3) + (dist c3,(c2 . c8)) < (c4 / 2) + (c4 / 2)
by E7, E8, XREAL_1:10;
hence
dist (c2 . c7),
(c2 . c8) < c
4
by E9, XXREAL_0:2;
end;
:: deftheorem E4 defines is_compared_to BHSP_3:def 2 :
theorem E5: :: BHSP_3:10
theorem E6: :: BHSP_3:11
theorem :: BHSP_3:12
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3, c
4 be
sequence of c
1;
assume that E7:
c
2 is_compared_to c
3
and E8:
c
3 is_compared_to c
4
;
let c
5 be
Real;
:: according to BHSP_3:def 2
assume
c
5 > 0
;
then E9:
c
5 / 2
> 0
by SEQ_2:3;
then consider c
6 being
Nat such that E10:
for b
1 being
Nat holds
not ( b
1 >= c
6 & not
dist (c2 . b1),
(c3 . b1) < c
5 / 2 )
by E7, E4;
consider c
7 being
Nat such that E11:
for b
1 being
Nat holds
not ( b
1 >= c
7 & not
dist (c3 . b1),
(c4 . b1) < c
5 / 2 )
by E8, E9, E4;
take c
8 = c
6 + c
7;
let c
9 be
Nat;
assume E12:
c
9 >= c
8
;
c
6 + c
7 >= c
6
by NAT_1:37;
then
c
9 >= c
6
by E12, XXREAL_0:2;
then E13:
dist (c2 . c9),
(c3 . c9) < c
5 / 2
by E10;
c
8 >= c
7
by NAT_1:37;
then
c
9 >= c
7
by E12, XXREAL_0:2;
then
dist (c3 . c9),
(c4 . c9) < c
5 / 2
by E11;
then E14:
(dist (c2 . c9),(c3 . c9)) + (dist (c3 . c9),(c4 . c9)) < (c5 / 2) + (c5 / 2)
by E13, XREAL_1:10;
dist (c2 . c9),
(c4 . c9) <= (dist (c2 . c9),(c3 . c9)) + (dist (c3 . c9),(c4 . c9))
by BHSP_1:42;
hence
dist (c2 . c9),
(c4 . c9) < c
5
by E14, XXREAL_0:2;
end;
theorem :: BHSP_3:13
theorem :: BHSP_3:14
theorem :: BHSP_3:15
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that E7:
c
2 is_Cauchy_sequence
and E8:
c
2 is_compared_to c
3
;
let c
4 be
Real;
:: according to BHSP_3:def 1
assume
c
4 > 0
;
then E9:
c
4 / 3
> 0
by XREAL_1:224;
then consider c
5 being
Nat such that E10:
for b
1, b
2 being
Nat holds
not ( b
1 >= c
5 & b
2 >= c
5 & not
dist (c2 . b1),
(c2 . b2) < c
4 / 3 )
by E7, E1;
consider c
6 being
Nat such that E11:
for b
1 being
Nat holds
not ( b
1 >= c
6 & not
dist (c2 . b1),
(c3 . b1) < c
4 / 3 )
by E8, E9, E4;
take c
7 = c
5 + c
6;
let c
8, c
9 be
Nat;
assume E12:
( c
8 >= c
7 & c
9 >= c
7 )
;
c
5 + c
6 >= c
5
by NAT_1:37;
then
( c
8 >= c
5 & c
9 >= c
5 )
by E12, XXREAL_0:2;
then E13:
dist (c2 . c8),
(c2 . c9) < c
4 / 3
by E10;
E14:
c
7 >= c
6
by NAT_1:37;
then
c
8 >= c
6
by E12, XXREAL_0:2;
then E15:
dist (c2 . c8),
(c3 . c8) < c
4 / 3
by E11;
c
9 >= c
6
by E12, E14, XXREAL_0:2;
then E16:
dist (c2 . c9),
(c3 . c9) < c
4 / 3
by E11;
E17:
(dist (c3 . c8),(c2 . c8)) + (dist (c2 . c8),(c2 . c9)) < (c4 / 3) + (c4 / 3)
by E13, E15, XREAL_1:10;
dist (c3 . c8),
(c2 . c9) <= (dist (c3 . c8),(c2 . c8)) + (dist (c2 . c8),(c2 . c9))
by BHSP_1:42;
then
dist (c3 . c8),
(c2 . c9) < (c4 / 3) + (c4 / 3)
by E17, XXREAL_0:2;
then E18:
(dist (c3 . c8),(c2 . c9)) + (dist (c2 . c9),(c3 . c9)) < ((c4 / 3) + (c4 / 3)) + (c4 / 3)
by E16, XREAL_1:10;
dist (c3 . c8),
(c3 . c9) <= (dist (c3 . c8),(c2 . c9)) + (dist (c2 . c9),(c3 . c9))
by BHSP_1:42;
hence
dist (c3 . c8),
(c3 . c9) < c
4
by E18, XXREAL_0:2;
end;
theorem :: BHSP_3:16
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that E7:
c
2 is
convergent
and E8:
c
2 is_compared_to c
3
;
now
let c
4 be
Real;
assume
c
4 > 0
;
then E9:
c
4 / 2
> 0
by SEQ_2:3;
then consider c
5 being
Nat such that E10:
for b
1 being
Nat holds
not ( b
1 >= c
5 & not
dist (c2 . b1),
(lim c2) < c
4 / 2 )
by E7, BHSP_2:def 2;
consider c
6 being
Nat such that E11:
for b
1 being
Nat holds
not ( b
1 >= c
6 & not
dist (c2 . b1),
(c3 . b1) < c
4 / 2 )
by E8, E9, E4;
take c
7 = c
5 + c
6;
let c
8 be
Nat;
assume E12:
c
8 >= c
7
;
c
5 + c
6 >= c
5
by NAT_1:37;
then
c
8 >= c
5
by E12, XXREAL_0:2;
then E13:
dist (c2 . c8),
(lim c2) < c
4 / 2
by E10;
c
7 >= c
6
by NAT_1:37;
then
c
8 >= c
6
by E12, XXREAL_0:2;
then
dist (c2 . c8),
(c3 . c8) < c
4 / 2
by E11;
then E14:
(dist (c3 . c8),(c2 . c8)) + (dist (c2 . c8),(lim c2)) < (c4 / 2) + (c4 / 2)
by E13, XREAL_1:10;
dist (c3 . c8),
(lim c2) <= (dist (c3 . c8),(c2 . c8)) + (dist (c2 . c8),(lim c2))
by BHSP_1:42;
hence
dist (c3 . c8),
(lim c2) < c
4
by E14, XXREAL_0:2;
end;
hence
c
3 is
convergent
by BHSP_2:def 1;
end;
theorem :: BHSP_3:17
proof
let c
1 be
RealUnitarySpace;
let c
2 be
Point of c
1;
let c
3, c
4 be
sequence of c
1;
assume that E7:
c
3 is
convergent
and E8:
lim c
3 = c
2
and E9:
c
3 is_compared_to c
4
;
E10:
now
let c
5 be
Real;
assume
c
5 > 0
;
then E11:
c
5 / 2
> 0
by SEQ_2:3;
then consider c
6 being
Nat such that E12:
for b
1 being
Nat holds
not ( b
1 >= c
6 & not
dist (c3 . b1),c
2 < c
5 / 2 )
by E7, E8, BHSP_2:def 2;
consider c
7 being
Nat such that E13:
for b
1 being
Nat holds
not ( b
1 >= c
7 & not
dist (c3 . b1),
(c4 . b1) < c
5 / 2 )
by E9, E11, E4;
take c
8 = c
6 + c
7;
let c
9 be
Nat;
assume E14:
c
9 >= c
8
;
c
6 + c
7 >= c
6
by NAT_1:37;
then
c
9 >= c
6
by E14, XXREAL_0:2;
then E15:
dist (c3 . c9),c
2 < c
5 / 2
by E12;
c
8 >= c
7
by NAT_1:37;
then
c
9 >= c
7
by E14, XXREAL_0:2;
then
dist (c3 . c9),
(c4 . c9) < c
5 / 2
by E13;
then E16:
(dist (c4 . c9),(c3 . c9)) + (dist (c3 . c9),c2) < (c5 / 2) + (c5 / 2)
by E15, XREAL_1:10;
dist (c4 . c9),c
2 <= (dist (c4 . c9),(c3 . c9)) + (dist (c3 . c9),c2)
by BHSP_1:42;
hence
dist (c4 . c9),c
2 < c
5
by E16, XXREAL_0:2;
end;
then
c
4 is
convergent
by BHSP_2:def 1;
hence
( c
4 is
convergent &
lim c
4 = c
2 )
by E10, BHSP_2:def 2;
end;
:: deftheorem E7 defines bounded BHSP_3:def 3 :
theorem E8: :: BHSP_3:18