:: TBSP_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: TBSP_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Real st 0 < L & L < 1 holds
for n, m being Nat st n <= m holds
L to_power m <= L to_power n
proof end;

theorem Th2: :: TBSP_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Real st 0 < L & L < 1 holds
for k being Nat holds
( L to_power k <= 1 & 0 < L to_power k )
proof end;

theorem Th3: :: TBSP_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Real st 0 < L & L < 1 holds
for s being Real st 0 < s holds
ex n being Nat st L to_power n < s
proof end;

definition
let N be non empty MetrStruct ;
attr N is totally_bounded means :Def1: :: TBSP_1:def 1
for r being Real st r > 0 holds
ex G being Subset-Family of N st
( G is finite & the carrier of N = union G & ( for C being Subset of N st C in G holds
ex w being Element of N st C = Ball w,r ) );
end;

:: deftheorem Def1 defines totally_bounded TBSP_1:def 1 :
for N being non empty MetrStruct holds
( N is totally_bounded iff for r being Real st r > 0 holds
ex G being Subset-Family of N st
( G is finite & the carrier of N = union G & ( for C being Subset of N st C in G holds
ex w being Element of N st C = Ball w,r ) ) );

Lm1: for N being non empty MetrStruct
for f being Function holds
( f is sequence of N iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of N ) ) )
proof end;

theorem :: TBSP_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TBSP_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty MetrStruct
for f being Function holds
( f is sequence of N iff ( dom f = NAT & ( for n being Nat holds f . n is Element of N ) ) )
proof end;

definition
let N be non empty MetrStruct ;
let S2 be sequence of N;
canceled;
attr S2 is convergent means :Def3: :: TBSP_1:def 3
ex x being Element of N st
for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
dist (S2 . m),x < r;
end;

:: deftheorem TBSP_1:def 2 :
canceled;

:: deftheorem Def3 defines convergent TBSP_1:def 3 :
for N being non empty MetrStruct
for S2 being sequence of N holds
( S2 is convergent iff ex x being Element of N st
for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
dist (S2 . m),x < r );

definition
let M be non empty MetrSpace;
let S1 be sequence of M;
assume A1: S1 is convergent ;
func lim S1 -> Element of M means :: TBSP_1:def 4
for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
dist (S1 . m),it < r;
existence
ex b1 being Element of M st
for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
dist (S1 . m),b1 < r
by A1, Def3;
uniqueness
for b1, b2 being Element of M st ( for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
dist (S1 . m),b1 < r ) & ( for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
dist (S1 . m),b2 < r ) holds
b1 = b2
proof end;
end;

:: deftheorem defines lim TBSP_1:def 4 :
for M being non empty MetrSpace
for S1 being sequence of M st S1 is convergent holds
for b3 being Element of M holds
( b3 = lim S1 iff for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
dist (S1 . m),b3 < r );

definition
let N be non empty MetrStruct ;
let S2 be sequence of N;
attr S2 is Cauchy means :Def5: :: TBSP_1:def 5
for r being Real st r > 0 holds
ex p being Nat st
for n, m being Nat st p <= n & p <= m holds
dist (S2 . n),(S2 . m) < r;
end;

:: deftheorem Def5 defines Cauchy TBSP_1:def 5 :
for N being non empty MetrStruct
for S2 being sequence of N holds
( S2 is Cauchy iff for r being Real st r > 0 holds
ex p being Nat st
for n, m being Nat st p <= n & p <= m holds
dist (S2 . n),(S2 . m) < r );

definition
let N be non empty MetrStruct ;
attr N is complete means :Def6: :: TBSP_1:def 6
for S2 being sequence of N st S2 is Cauchy holds
S2 is convergent;
end;

:: deftheorem Def6 defines complete TBSP_1:def 6 :
for N being non empty MetrStruct holds
( N is complete iff for S2 being sequence of N st S2 is Cauchy holds
S2 is convergent );

theorem :: TBSP_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th7: :: TBSP_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty MetrStruct
for S2 being sequence of N st N is triangle & N is symmetric & S2 is convergent holds
S2 is Cauchy
proof end;

registration
let M be non empty symmetric triangle MetrStruct ;
cluster convergent -> Cauchy M5( NAT ,the carrier of M);
coherence
for b1 being sequence of M st b1 is convergent holds
b1 is Cauchy
by Th7;
end;

theorem Th8: :: TBSP_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty MetrStruct
for S2 being sequence of N st N is symmetric holds
( S2 is Cauchy iff for r being Real st r > 0 holds
ex p being Nat st
for n, k being Nat st p <= n holds
dist (S2 . (n + k)),(S2 . n) < r )
proof end;

theorem :: TBSP_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for f being contraction of M st M is complete holds
ex c being Element of M st
( f . c = c & ( for y being Element of M st f . y = y holds
y = c ) )
proof end;

theorem :: TBSP_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty Reflexive symmetric triangle MetrStruct st TopSpaceMetr T is compact holds
T is complete
proof end;

theorem :: TBSP_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TBSP_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty MetrStruct st N is Reflexive & N is triangle & TopSpaceMetr N is compact holds
N is totally_bounded
proof end;

definition
let N be non empty MetrStruct ;
canceled;
attr N is bounded means :Def8: :: TBSP_1:def 8
ex r being Real st
( 0 < r & ( for x, y being Point of N holds dist x,y <= r ) );
let C be Subset of N;
attr C is bounded means :Def9: :: TBSP_1:def 9
ex r being Real st
( 0 < r & ( for x, y being Point of N st x in C & y in C holds
dist x,y <= r ) );
end;

:: deftheorem TBSP_1:def 7 :
canceled;

:: deftheorem Def8 defines bounded TBSP_1:def 8 :
for N being non empty MetrStruct holds
( N is bounded iff ex r being Real st
( 0 < r & ( for x, y being Point of N holds dist x,y <= r ) ) );

:: deftheorem Def9 defines bounded TBSP_1:def 9 :
for N being non empty MetrStruct
for C being Subset of N holds
( C is bounded iff ex r being Real st
( 0 < r & ( for x, y being Point of N st x in C & y in C holds
dist x,y <= r ) ) );

registration
let A be non empty set ;
cluster DiscreteSpace A -> bounded ;
coherence
DiscreteSpace A is bounded
proof end;
end;

registration
cluster non empty bounded MetrStruct ;
existence
ex b1 being non empty MetrSpace st b1 is bounded
proof end;
end;

theorem :: TBSP_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th14: :: TBSP_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty MetrStruct holds {} N is bounded
proof end;

registration
let N be non empty MetrStruct ;
cluster {} N -> bounded ;
coherence
{} N is bounded
by Th14;
end;

registration
let N be non empty MetrStruct ;
cluster bounded Element of K40(the carrier of N);
existence
ex b1 being Subset of N st b1 is bounded
proof end;
end;

theorem Th15: :: TBSP_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty MetrStruct
for C being Subset of N holds
( ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist w,z <= r ) ) ) & ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist w,z <= r ) ) implies C is bounded ) )
proof end;

theorem Th16: :: TBSP_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty MetrStruct
for w being Element of N
for r being real number st N is Reflexive & 0 < r holds
w in Ball w,r
proof end;

theorem Th17: :: TBSP_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty Reflexive symmetric triangle MetrStruct
for t1 being Element of T
for r being real number st r <= 0 holds
Ball t1,r = {}
proof end;

Lm2: for T being non empty Reflexive symmetric triangle MetrStruct
for t1 being Element of T
for r being real number st 0 < r holds
Ball t1,r is bounded
proof end;

theorem :: TBSP_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th19: :: TBSP_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty Reflexive symmetric triangle MetrStruct
for t1 being Element of T
for r being real number holds Ball t1,r is bounded
proof end;

theorem Th20: :: TBSP_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty Reflexive symmetric triangle MetrStruct
for P, Q being Subset of T st P is bounded & Q is bounded holds
P \/ Q is bounded
proof end;

theorem Th21: :: TBSP_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty MetrStruct
for C, D being Subset of N st C is bounded & D c= C holds
D is bounded
proof end;

theorem Th22: :: TBSP_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty Reflexive symmetric triangle MetrStruct
for t1 being Element of T
for P being Subset of T st P = {t1} holds
P is bounded
proof end;

theorem Th23: :: TBSP_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty Reflexive symmetric triangle MetrStruct
for P being Subset of T st P is finite holds
P is bounded
proof end;

registration
let T be non empty Reflexive symmetric triangle MetrStruct ;
cluster finite -> bounded Element of K40(the carrier of T);
coherence
for b1 being Subset of T st b1 is finite holds
b1 is bounded
by Th23;
end;

registration
let T be non empty Reflexive symmetric triangle MetrStruct ;
cluster non empty finite bounded Element of K40(the carrier of T);
existence
ex b1 being Subset of T st
( b1 is finite & not b1 is empty )
proof end;
end;

theorem Th24: :: TBSP_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty Reflexive symmetric triangle MetrStruct
for Y being Subset-Family of T st Y is finite & ( for P being Subset of T st P in Y holds
P is bounded ) holds
union Y is bounded
proof end;

theorem Th25: :: TBSP_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being non empty MetrStruct holds
( N is bounded iff [#] N is bounded )
proof end;

registration
let N be non empty bounded MetrStruct ;
cluster [#] N -> bounded ;
coherence
[#] N is bounded
by Th25;
end;

theorem :: TBSP_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty Reflexive symmetric triangle MetrStruct st T is totally_bounded holds
T is bounded
proof end;

definition
let N be non empty Reflexive MetrStruct ;
let C be Subset of N;
assume A1: C is bounded ;
func diameter C -> Real means :Def10: :: TBSP_1:def 10
( ( for x, y being Point of N st x in C & y in C holds
dist x,y <= it ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist x,y <= s ) holds
it <= s ) ) if C <> {}
otherwise it = 0;
consistency
for b1 being Real holds verum
;
existence
( ( C <> {} implies ex b1 being Real st
( ( for x, y being Point of N st x in C & y in C holds
dist x,y <= b1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist x,y <= s ) holds
b1 <= s ) ) ) & ( not C <> {} implies ex b1 being Real st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Real holds
( ( C <> {} & ( for x, y being Point of N st x in C & y in C holds
dist x,y <= b1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist x,y <= s ) holds
b1 <= s ) & ( for x, y being Point of N st x in C & y in C holds
dist x,y <= b2 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist x,y <= s ) holds
b2 <= s ) implies b1 = b2 ) & ( not C <> {} & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
end;

:: deftheorem Def10 defines diameter TBSP_1:def 10 :
for N being non empty Reflexive MetrStruct
for C being Subset of N st C is bounded holds
for b3 being Real holds
( ( C <> {} implies ( b3 = diameter C iff ( ( for x, y being Point of N st x in C & y in C holds
dist x,y <= b3 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist x,y <= s ) holds
b3 <= s ) ) ) ) & ( not C <> {} implies ( b3 = diameter C iff b3 = 0 ) ) );

theorem :: TBSP_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: TBSP_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty Reflexive symmetric triangle MetrStruct
for x being set
for P being Subset of T st P = {x} holds
diameter P = 0
proof end;

theorem Th29: :: TBSP_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty Reflexive MetrStruct
for S being Subset of R st S is bounded holds
0 <= diameter S
proof end;

theorem :: TBSP_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being non empty MetrSpace
for A being Subset of M st A <> {} & A is bounded & diameter A = 0 holds
ex g being Point of M st A = {g}
proof end;

theorem :: TBSP_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty Reflexive symmetric triangle MetrStruct
for t1 being Element of T
for r being Real st 0 < r holds
diameter (Ball t1,r) <= 2 * r
proof end;

theorem :: TBSP_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty Reflexive MetrStruct
for S, V being Subset of R st S is bounded & V c= S holds
diameter V <= diameter S
proof end;

theorem :: TBSP_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty Reflexive symmetric triangle MetrStruct
for P, Q being Subset of T st P is bounded & Q is bounded & P meets Q holds
diameter (P \/ Q) <= (diameter P) + (diameter Q)
proof end;

definition
let N be non empty MetrStruct ;
let S2 be sequence of N;
:: original: rng
redefine func rng S2 -> Subset of N;
coherence
rng S2 is Subset of N
by RELSET_1:12;
end;

theorem :: TBSP_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being non empty Reflexive symmetric triangle MetrStruct
for S1 being sequence of T st S1 is Cauchy holds
rng S1 is bounded
proof end;