:: BHSP_2 semantic presentation
deffunc H1( RealUnitarySpace) -> Element of the carrier of a1 = 0. a1;
:: deftheorem Def1 defines convergent BHSP_2:def 1 :
theorem Th1: :: BHSP_2:1
theorem Th2: :: BHSP_2:2
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that E4:
c
2 is
convergent
and E5:
ex b
1 being
Nat st
for b
2 being
Nat holds
( b
1 <= b
2 implies c
3 . b
2 = c
2 . b
2 )
;
consider c
4 being
Point of c
1 such that E6:
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
4 < b
1 ) ) )
by E4, Def1;
consider c
5 being
Nat such that E7:
for b
1 being
Nat holds
( b
1 >= c
5 implies c
3 . b
1 = c
2 . b
1 )
by E5;
take c
6 = c
4;
:: according to BHSP_2:def 1
let c
7 be
Real;
assume
c
7 > 0
;
then consider c
8 being
Nat such that E8:
for b
1 being
Nat holds
not ( b
1 >= c
8 & not
dist (c2 . b1),c
6 < c
7 )
by E6;
hence
ex b
1 being
Nat st
for b
2 being
Nat holds
not ( b
2 >= b
1 & not
dist (c3 . b2),c
6 < c
7 )
by E9;
end;
theorem Th3: :: BHSP_2:3
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that E5:
c
2 is
convergent
and E6:
c
3 is
convergent
;
consider c
4 being
Point of c
1 such that E7:
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
4 < b
1 ) ) )
by E5, Def1;
consider c
5 being
Point of c
1 such that E8:
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 (c3 . b3),c
5 < b
1 ) ) )
by E6, Def1;
take c
6 = c
4 + c
5;
:: according to BHSP_2:def 1
let c
7 be
Real;
assume
c
7 > 0
;
then E9:
c
7 / 2
> 0
by SEQ_2:3;
then consider c
8 being
Nat such that E10:
for b
1 being
Nat holds
not ( b
1 >= c
8 & not
dist (c2 . b1),c
4 < c
7 / 2 )
by E7;
consider c
9 being
Nat such that E11:
for b
1 being
Nat holds
not ( b
1 >= c
9 & not
dist (c3 . b1),c
5 < c
7 / 2 )
by E8, E9;
take c
10 = c
8 + c
9;
let c
11 be
Nat;
assume E12:
c
11 >= c
10
;
c
8 + c
9 >= c
8
by NAT_1:37;
then
c
11 >= c
8
by E12, XXREAL_0:2;
then E13:
dist (c2 . c11),c
4 < c
7 / 2
by E10;
c
10 >= c
9
by NAT_1:37;
then
c
11 >= c
9
by E12, XXREAL_0:2;
then
dist (c3 . c11),c
5 < c
7 / 2
by E11;
then E14:
(dist (c2 . c11),c4) + (dist (c3 . c11),c5) < (c7 / 2) + (c7 / 2)
by E13, XREAL_1:10;
dist ((c2 + c3) . c11),c
6 = dist ((c2 . c11) + (c3 . c11)),
(c4 + c5)
by NORMSP_1:def 5;
then
dist ((c2 + c3) . c11),c
6 <= (dist (c2 . c11),c4) + (dist (c3 . c11),c5)
by BHSP_1:47;
hence
dist ((c2 + c3) . c11),c
6 < c
7
by E14, XXREAL_0:2;
end;
theorem Th4: :: BHSP_2:4
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that E6:
c
2 is
convergent
and E7:
c
3 is
convergent
;
consider c
4 being
Point of c
1 such that E8:
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
4 < b
1 ) ) )
by E6, Def1;
consider c
5 being
Point of c
1 such that E9:
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 (c3 . b3),c
5 < b
1 ) ) )
by E7, Def1;
take c
6 = c
4 - c
5;
:: according to BHSP_2:def 1
let c
7 be
Real;
assume
c
7 > 0
;
then E10:
c
7 / 2
> 0
by SEQ_2:3;
then consider c
8 being
Nat such that E11:
for b
1 being
Nat holds
not ( b
1 >= c
8 & not
dist (c2 . b1),c
4 < c
7 / 2 )
by E8;
consider c
9 being
Nat such that E12:
for b
1 being
Nat holds
not ( b
1 >= c
9 & not
dist (c3 . b1),c
5 < c
7 / 2 )
by E9, E10;
take c
10 = c
8 + c
9;
let c
11 be
Nat;
assume E13:
c
11 >= c
10
;
c
8 + c
9 >= c
8
by NAT_1:37;
then
c
11 >= c
8
by E13, XXREAL_0:2;
then E14:
dist (c2 . c11),c
4 < c
7 / 2
by E11;
c
10 >= c
9
by NAT_1:37;
then
c
11 >= c
9
by E13, XXREAL_0:2;
then
dist (c3 . c11),c
5 < c
7 / 2
by E12;
then E15:
(dist (c2 . c11),c4) + (dist (c3 . c11),c5) < (c7 / 2) + (c7 / 2)
by E14, XREAL_1:10;
dist ((c2 - c3) . c11),c
6 = dist ((c2 . c11) - (c3 . c11)),
(c4 - c5)
by NORMSP_1:def 6;
then
dist ((c2 - c3) . c11),c
6 <= (dist (c2 . c11),c4) + (dist (c3 . c11),c5)
by BHSP_1:48;
hence
dist ((c2 - c3) . c11),c
6 < c
7
by E15, XXREAL_0:2;
end;
theorem Th5: :: BHSP_2:5
proof
let c
1 be
RealUnitarySpace;
let c
2 be
Real;
let c
3 be
sequence of c
1;
assume
c
3 is
convergent
;
then consider c
4 being
Point of c
1 such that E7:
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 (c3 . b3),c
4 < b
1 ) ) )
by Def1;
take c
5 = c
2 * c
4;
:: according to BHSP_2:def 1
now
assume E9:
c
2 <> 0
;
then E10:
abs c
2 > 0
by COMPLEX1:133;
let c
6 be
Real;
assume E11:
c
6 > 0
;
E12:
abs c
2 <> 0
by E9, COMPLEX1:133;
0
/ (abs c2) = 0
;
then
c
6 / (abs c2) > 0
by E10, E11, REAL_1:73;
then consider c
7 being
Nat such that E13:
for b
1 being
Nat holds
not ( b
1 >= c
7 & not
dist (c3 . b1),c
4 < c
6 / (abs c2) )
by E7;
take c
8 = c
7;
let c
9 be
Nat;
assume
c
9 >= c
8
;
then E14:
dist (c3 . c9),c
4 < c
6 / (abs c2)
by E13;
E15:
dist (c2 * (c3 . c9)),
(c2 * c4) =
||.((c2 * (c3 . c9)) - (c2 * c4)).||
by BHSP_1:def 5
.=
||.(c2 * ((c3 . c9) - c4)).||
by RLVECT_1:48
.=
(abs c2) * ||.((c3 . c9) - c4).||
by BHSP_1:33
.=
(abs c2) * (dist (c3 . c9),c4)
by BHSP_1:def 5
;
(abs c2) * (c6 / (abs c2)) =
(abs c2) * (((abs c2) " ) * c6)
by XCMPLX_0:def 9
.=
((abs c2) * ((abs c2) " )) * c
6
.=
1
* c
6
by E12, XCMPLX_0:def 7
.=
c
6
;
then
dist (c2 * (c3 . c9)),c
5 < c
6
by E10, E14, E15, XREAL_1:70;
hence
dist ((c2 * c3) . c9),c
5 < c
6
by NORMSP_1:def 8;
end;
hence
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 * c3) . b3),c
5 < b
1 ) ) )
by E8;
end;
theorem Th6: :: BHSP_2:6
theorem Th7: :: BHSP_2:7
proof
let c
1 be
RealUnitarySpace;
let c
2 be
Point of c
1;
let c
3 be
sequence of c
1;
assume
c
3 is
convergent
;
then consider c
4 being
Point of c
1 such that E9:
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 (c3 . b3),c
4 < b
1 ) ) )
by Def1;
take
c
4 + c
2
;
:: according to BHSP_2:def 1
let c
5 be
Real;
assume
c
5 > 0
;
then consider c
6 being
Nat such that E10:
for b
1 being
Nat holds
not ( b
1 >= c
6 & not
dist (c3 . b1),c
4 < c
5 )
by E9;
take c
7 = c
6;
let c
8 be
Nat;
assume
c
8 >= c
7
;
then E11:
dist (c3 . c8),c
4 < c
5
by E10;
dist ((c3 . c8) + c2),
(c4 + c2) <= (dist (c3 . c8),c4) + (dist c2,c2)
by BHSP_1:47;
then
dist ((c3 . c8) + c2),
(c4 + c2) <= (dist (c3 . c8),c4) + 0
by BHSP_1:41;
then
dist ((c3 . c8) + c2),
(c4 + c2) < c
5
by E11, XXREAL_0:2;
hence
dist ((c3 + c2) . c8),
(c4 + c2) < c
5
by BHSP_1:def 12;
end;
theorem Th8: :: BHSP_2:8
theorem Th9: :: BHSP_2:9
definition
let c
1 be
RealUnitarySpace;
let c
2 be
sequence of c
1;
assume E11:
c
2 is
convergent
;
func lim c
2 -> Point of a
1 means :
Def2:
:: BHSP_2:def 2
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 (a2 . b3),a
3 < b
1 ) ) );
existence
ex b1 being Point of c1 st
for b2 being Real holds
not ( b2 > 0 & ( for b3 being Nat holds
ex b4 being Nat st
( b4 >= b3 & not dist (c2 . b4),b1 < b2 ) ) )
by E11, Def1;
uniqueness
for b1, b2 being Point of c1 holds
( ( for b3 being Real holds
not ( b3 > 0 & ( for b4 being Nat holds
ex b5 being Nat st
( b5 >= b4 & not dist (c2 . b5),b1 < b3 ) ) ) ) & ( for b3 being Real holds
not ( b3 > 0 & ( for b4 being Nat holds
ex b5 being Nat st
( b5 >= b4 & not dist (c2 . b5),b2 < b3 ) ) ) ) implies b1 = b2 )
proof
for b
1, b
2 being
Point of c
1 holds
( ( for b
3 being
Real holds
not ( b
3 > 0 & ( for b
4 being
Nat holds
ex b
5 being
Nat st
( b
5 >= b
4 & not
dist (c2 . b5),b
1 < b
3 ) ) ) ) & ( for b
3 being
Real holds
not ( b
3 > 0 & ( for b
4 being
Nat holds
ex b
5 being
Nat st
( b
5 >= b
4 & not
dist (c2 . b5),b
2 < b
3 ) ) ) ) implies b
1 = b
2 )
proof
given c
3, c
4 being
Point of c
1 such that E12:
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 ) ) )
and E13:
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
4 < b
1 ) ) )
and E14:
c
3 <> c
4
;
E15:
dist c
3,c
4 > 0
by E14, BHSP_1:45;
then E16:
(dist c3,c4) / 4
> 0
/ 4
by REAL_1:73;
then consider c
5 being
Nat such that E17:
for b
1 being
Nat holds
not ( b
1 >= c
5 & not
dist (c2 . b1),c
3 < (dist c3,c4) / 4 )
by E12;
consider c
6 being
Nat such that E18:
for b
1 being
Nat holds
not ( b
1 >= c
6 & not
dist (c2 . b1),c
4 < (dist c3,c4) / 4 )
by E13, E16;
E19:
now
assume
c
5 <= c
6
;
then E20:
dist (c2 . c6),c
3 < (dist c3,c4) / 4
by E17;
dist (c2 . c6),c
4 < (dist c3,c4) / 4
by E18;
then E21:
(dist (c2 . c6),c3) + (dist (c2 . c6),c4) < ((dist c3,c4) / 4) + ((dist c3,c4) / 4)
by E20, XREAL_1:10;
dist c
3,c
4 = dist (c3 - (c2 . c6)),
(c4 - (c2 . c6))
by BHSP_1:49;
then
dist c
3,c
4 <= (dist (c2 . c6),c3) + (dist (c2 . c6),c4)
by BHSP_1:50;
then
dist c
3,c
4 <= (dist c3,c4) / 2
by E21, XXREAL_0:2;
hence
not verum
by E15, XREAL_1:218;
end;
now
assume
c
5 >= c
6
;
then E20:
dist (c2 . c5),c
4 < (dist c3,c4) / 4
by E18;
dist (c2 . c5),c
3 < (dist c3,c4) / 4
by E17;
then E21:
(dist (c2 . c5),c3) + (dist (c2 . c5),c4) < ((dist c3,c4) / 4) + ((dist c3,c4) / 4)
by E20, XREAL_1:10;
dist c
3,c
4 = dist (c3 - (c2 . c5)),
(c4 - (c2 . c5))
by BHSP_1:49;
then
dist c
3,c
4 <= (dist (c2 . c5),c3) + (dist (c2 . c5),c4)
by BHSP_1:50;
then
dist c
3,c
4 <= (dist c3,c4) / 2
by E21, XXREAL_0:2;
hence
not verum
by E15, XREAL_1:218;
end;
hence
not verum
by E19;
end;
hence
for b
1, b
2 being
Point of c
1 holds
( ( for b
3 being
Real holds
not ( b
3 > 0 & ( for b
4 being
Nat holds
ex b
5 being
Nat st
( b
5 >= b
4 & not
dist (c2 . b5),b
1 < b
3 ) ) ) ) & ( for b
3 being
Real holds
not ( b
3 > 0 & ( for b
4 being
Nat holds
ex b
5 being
Nat st
( b
5 >= b
4 & not
dist (c2 . b5),b
2 < b
3 ) ) ) ) implies b
1 = b
2 )
;
end;
end;
:: deftheorem Def2 defines lim BHSP_2:def 2 :
theorem Th10: :: BHSP_2:10
theorem Th11: :: BHSP_2:11
theorem Th12: :: BHSP_2:12
theorem Th13: :: BHSP_2:13
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that E14:
c
2 is
convergent
and E15:
c
3 is
convergent
;
E16:
c
2 + c
3 is
convergent
by E14, E15, Th3;
set c
4 =
lim c
2;
set c
5 =
lim c
3;
set c
6 =
(lim c2) + (lim c3);
now
let c
7 be
Real;
assume
c
7 > 0
;
then E17:
c
7 / 2
> 0
by SEQ_2:3;
then consider c
8 being
Nat such that E18:
for b
1 being
Nat holds
not ( b
1 >= c
8 & not
dist (c2 . b1),
(lim c2) < c
7 / 2 )
by E14, Def2;
consider c
9 being
Nat such that E19:
for b
1 being
Nat holds
not ( b
1 >= c
9 & not
dist (c3 . b1),
(lim c3) < c
7 / 2 )
by E15, E17, Def2;
take c
10 = c
8 + c
9;
let c
11 be
Nat;
assume E20:
c
11 >= c
10
;
c
8 + c
9 >= c
8
by NAT_1:37;
then
c
11 >= c
8
by E20, XXREAL_0:2;
then E21:
dist (c2 . c11),
(lim c2) < c
7 / 2
by E18;
c
10 >= c
9
by NAT_1:37;
then
c
11 >= c
9
by E20, XXREAL_0:2;
then
dist (c3 . c11),
(lim c3) < c
7 / 2
by E19;
then E22:
(dist (c2 . c11),(lim c2)) + (dist (c3 . c11),(lim c3)) < (c7 / 2) + (c7 / 2)
by E21, XREAL_1:10;
dist ((c2 + c3) . c11),
((lim c2) + (lim c3)) = dist ((c2 . c11) + (c3 . c11)),
((lim c2) + (lim c3))
by NORMSP_1:def 5;
then
dist ((c2 + c3) . c11),
((lim c2) + (lim c3)) <= (dist (c2 . c11),(lim c2)) + (dist (c3 . c11),(lim c3))
by BHSP_1:47;
hence
dist ((c2 + c3) . c11),
((lim c2) + (lim c3)) < c
7
by E22, XXREAL_0:2;
end;
hence
lim (c2 + c3) = (lim c2) + (lim c3)
by E16, Def2;
end;
theorem Th14: :: BHSP_2:14
proof
let c
1 be
RealUnitarySpace;
let c
2, c
3 be
sequence of c
1;
assume that E15:
c
2 is
convergent
and E16:
c
3 is
convergent
;
E17:
c
2 - c
3 is
convergent
by E15, E16, Th4;
set c
4 =
lim c
2;
set c
5 =
lim c
3;
set c
6 =
(lim c2) - (lim c3);
now
let c
7 be
Real;
assume
c
7 > 0
;
then E18:
c
7 / 2
> 0
by SEQ_2:3;
then consider c
8 being
Nat such that E19:
for b
1 being
Nat holds
not ( b
1 >= c
8 & not
dist (c2 . b1),
(lim c2) < c
7 / 2 )
by E15, Def2;
consider c
9 being
Nat such that E20:
for b
1 being
Nat holds
not ( b
1 >= c
9 & not
dist (c3 . b1),
(lim c3) < c
7 / 2 )
by E16, E18, Def2;
take c
10 = c
8 + c
9;
let c
11 be
Nat;
assume E21:
c
11 >= c
10
;
c
8 + c
9 >= c
8
by NAT_1:37;
then
c
11 >= c
8
by E21, XXREAL_0:2;
then E22:
dist (c2 . c11),
(lim c2) < c
7 / 2
by E19;
c
10 >= c
9
by NAT_1:37;
then
c
11 >= c
9
by E21, XXREAL_0:2;
then
dist (c3 . c11),
(lim c3) < c
7 / 2
by E20;
then E23:
(dist (c2 . c11),(lim c2)) + (dist (c3 . c11),(lim c3)) < (c7 / 2) + (c7 / 2)
by E22, XREAL_1:10;
dist ((c2 - c3) . c11),
((lim c2) - (lim c3)) = dist ((c2 . c11) - (c3 . c11)),
((lim c2) - (lim c3))
by NORMSP_1:def 6;
then
dist ((c2 - c3) . c11),
((lim c2) - (lim c3)) <= (dist (c2 . c11),(lim c2)) + (dist (c3 . c11),(lim c3))
by BHSP_1:48;
hence
dist ((c2 - c3) . c11),
((lim c2) - (lim c3)) < c
7
by E23, XXREAL_0:2;
end;
hence