:: TBSP_1 semantic presentation

theorem Th1: :: TBSP_1:1

for b₁ being Real st 0 < b₁ & b₁ < 1 holds
for b₂, b₃ being Nat st b₂ <= b₃ holds
b₁ to_power b₃ <= b₁ to_power b₂

proof end;

theorem Th2: :: TBSP_1:2

for b₁ being Real st 0 < b₁ & b₁ < 1 holds
for b₂ being Nat holds
( b₁ to_power b₂ <= 1 & 0 < b₁ to_power b₂ )

proof end;

theorem Th3: :: TBSP_1:3

for b₁ being Real st 0 < b₁ & b₁ < 1 holds
for b₂ being Real st 0 < b₂ holds
ex b₃ being Nat st b₁ to_power b₃ < b₂

proof end;

definition

let c₁ be non empty MetrStruct ;
attr a₁ is totally_bounded means :Def1: :: TBSP_1:def 1
for b₁ being Real st b₁ > 0 holds
ex b₂ being Subset-Family of a₁ st
( b₂ is finite & the carrier of a₁ = union b₂ & ( for b₃ being Subset of a₁ st b₃ in b₂ holds
ex b₄ being Element of a₁ st b₃ = Ball b₄,b₁ ) );

end;

:: deftheorem Def1 defines totally_bounded TBSP_1:def 1 :

Lemma5: for b₁ being non empty MetrStruct
for b₂ being Function holds
( b₂ is sequence of b₁ iff ( dom b₂ = NAT & ( for b₃ being set st b₃ in NAT holds
b₂ . b₃ is Element of b₁ ) ) )

proof end;

theorem Th4: :: TBSP_1:4

canceled;

theorem Th5: :: TBSP_1:5

for b₁ being non empty MetrStruct
for b₂ being Function holds
( b₂ is sequence of b₁ iff ( dom b₂ = NAT & ( for b₃ being Nat holds b₂ . b₃ is Element of b₁ ) ) )

proof end;

definition

let c₁ be non empty MetrStruct ;
let c₂ be sequence of c₁;
canceled;
attr a₂ is convergent means :Def3: :: TBSP_1:def 3
ex b₁ being Element of a₁ st
for b₂ being Real st b₂ > 0 holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
dist (a₂ . b₄),b₁ < b₂;

end;

:: deftheorem Def2 TBSP_1:def 2 :

:: deftheorem Def3 defines convergent TBSP_1:def 3 :

definition

let c₁ be non empty MetrSpace;
let c₂ be sequence of c₁;
assume E7: c₂ is convergent ;
func lim c₂ -> Element of a₁ means :: TBSP_1:def 4
for b₁ being Real st b₁ > 0 holds
ex b₂ being Nat st
for b₃ being Nat st b₃ >= b₂ holds
dist (a₂ . b₃),a₃ < b₁;
existence by E7, Def3;
uniqueness

proof end;

end;

:: deftheorem Def4 defines lim TBSP_1:def 4 :

definition

let c₁ be non empty MetrStruct ;
let c₂ be sequence of c₁;
attr a₂ is Cauchy means :Def5: :: TBSP_1:def 5
for b₁ being Real st b₁ > 0 holds
ex b₂ being Nat st
for b₃, b₄ being Nat st b₂ <= b₃ & b₂ <= b₄ holds
dist (a₂ . b₃),(a₂ . b₄) < b₁;

end;

:: deftheorem Def5 defines Cauchy TBSP_1:def 5 :

definition

let c₁ be non empty MetrStruct ;
attr a₁ is complete means :Def6: :: TBSP_1:def 6
for b₁ being sequence of a₁ st b₁ is Cauchy holds
b₁ is convergent;

end;

:: deftheorem Def6 defines complete TBSP_1:def 6 :

theorem Th6: :: TBSP_1:6

canceled;

theorem Th7: :: TBSP_1:7

for b₁ being non empty MetrStruct
for b₂ being sequence of b₁ st b₁ is triangle & b₁ is symmetric & b₂ is convergent holds
b₂ is Cauchy

proof end;

registration

let c₁ be non empty symmetric triangle MetrStruct ;
cluster convergent -> Cauchy M5( NAT ,the carrier of a₁);
coherence by Th7;

end;

theorem Th8: :: TBSP_1:8

for b₁ being non empty MetrStruct
for b₂ being sequence of b₁ st b₁ is symmetric holds
( b₂ is Cauchy iff for b₃ being Real st b₃ > 0 holds
ex b₄ being Nat st
for b₅, b₆ being Nat st b₄ <= b₅ holds
dist (b₂ . (b₅ + b₆)),(b₂ . b₅) < b₃ )

proof end;

theorem Th9: :: TBSP_1:9

for b₁ being non empty MetrSpace
for b₂ being contraction of b₁ st b₁ is complete holds
ex b₃ being Element of b₁ st
( b₂ . b₃ = b₃ & ( for b₄ being Element of b₁ st b₂ . b₄ = b₄ holds
b₄ = b₃ ) )

proof end;

theorem Th10: :: TBSP_1:10

for b₁ being non empty Reflexive symmetric triangle MetrStruct st TopSpaceMetr b₁ is compact holds
b₁ is complete

proof end;

theorem Th11: :: TBSP_1:11

canceled;

theorem Th12: :: TBSP_1:12

for b₁ being non empty MetrStruct st b₁ is Reflexive & b₁ is triangle & TopSpaceMetr b₁ is compact holds
b₁ is totally_bounded

proof end;

definition

let c₁ be non empty MetrStruct ;
canceled;
attr a₁ is bounded means :Def8: :: TBSP_1:def 8
ex b₁ being Real st
( 0 < b₁ & ( for b₂, b₃ being Point of a₁ holds dist b₂,b₃ <= b₁ ) );
let c₂ be Subset of c₁;
attr a₂ is bounded means :Def9: :: TBSP_1:def 9
ex b₁ being Real st
( 0 < b₁ & ( for b₂, b₃ being Point of a₁ st b₂ in a₂ & b₃ in a₂ holds
dist b₂,b₃ <= b₁ ) );

end;

:: deftheorem Def7 TBSP_1:def 7 :

:: deftheorem Def8 defines bounded TBSP_1:def 8 :

:: deftheorem Def9 defines bounded TBSP_1:def 9 :

registration

let c₁ be non empty set ;
cluster DiscreteSpace a₁ -> bounded ;
coherence

proof end;

end;

registration

cluster non empty bounded MetrStruct ;
existence

proof end;

end;

theorem Th13: :: TBSP_1:13

canceled;

theorem Th14: :: TBSP_1:14

for b₁ being non empty MetrStruct holds {} b₁ is bounded

proof end;

registration

let c₁ be non empty MetrStruct ;
cluster {} a₁ -> bounded ;
coherence by Th14;

end;

registration

let c₁ be non empty MetrStruct ;
cluster bounded Element of K40(the carrier of a₁);
existence

proof end;

end;

theorem Th15: :: TBSP_1:15

for b₁ being non empty MetrStruct
for b₂ being Subset of b₁ holds
( ( b₂ <> {} & b₂ is bounded implies ex b₃ being Realex b₄ being Element of b₁ st
( 0 < b₃ & b₄ in b₂ & ( for b₅ being Point of b₁ st b₅ in b₂ holds
dist b₄,b₅ <= b₃ ) ) ) & ( b₁ is symmetric & b₁ is triangle & ex b₃ being Realex b₄ being Element of b₁ st
( 0 < b₃ & b₄ in b₂ & ( for b₅ being Point of b₁ st b₅ in b₂ holds
dist b₄,b₅ <= b₃ ) ) implies b₂ is bounded ) )

proof end;

theorem Th16: :: TBSP_1:16

for b₁ being non empty MetrStruct
for b₂ being Element of b₁
for b₃ being real number st b₁ is Reflexive & 0 < b₃ holds
b₂ in Ball b₂,b₃

proof end;

theorem Th17: :: TBSP_1:17

for b₁ being non empty Reflexive symmetric triangle MetrStruct
for b₂ being Element of b₁
for b₃ being real number st b₃ <= 0 holds
Ball b₂,b₃ = {}

proof end;

Lemma17: for b₁ being non empty Reflexive symmetric triangle MetrStruct
for b₂ being Element of b₁
for b₃ being real number st 0 < b₃ holds
Ball b₂,b₃ is bounded

proof end;

theorem Th18: :: TBSP_1:18

canceled;

theorem Th19: :: TBSP_1:19

for b₁ being non empty Reflexive symmetric triangle MetrStruct
for b₂ being Element of b₁
for b₃ being real number holds Ball b₂,b₃ is bounded

proof end;

theorem Th20: :: TBSP_1:20

for b₁ being non empty Reflexive symmetric triangle MetrStruct
for b₂, b₃ being Subset of b₁ st b₂ is bounded & b₃ is bounded holds
b₂ \/ b₃ is bounded

proof end;

theorem Th21: :: TBSP_1:21

for b₁ being non empty MetrStruct
for b₂, b₃ being Subset of b₁ st b₂ is bounded & b₃ c= b₂ holds
b₃ is bounded

proof end;

theorem Th22: :: TBSP_1:22

for b₁ being non empty Reflexive symmetric triangle MetrStruct
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₃ = {b₂} holds
b₃ is bounded

proof end;

theorem Th23: :: TBSP_1:23

for b₁ being non empty Reflexive symmetric triangle MetrStruct
for b₂ being Subset of b₁ st b₂ is finite holds
b₂ is bounded

proof end;

registration

let c₁ be non empty Reflexive symmetric triangle MetrStruct ;
cluster finite -> bounded Element of K40(the carrier of a₁);
coherence by Th23;

end;

registration

let c₁ be non empty Reflexive symmetric triangle MetrStruct ;
cluster non empty finite bounded Element of K40(the carrier of a₁);
existence

proof end;

end;

theorem Th24: :: TBSP_1:24

for b₁ being non empty Reflexive symmetric triangle MetrStruct
for b₂ being Subset-Family of b₁ st b₂ is finite & ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ is bounded ) holds
union b₂ is bounded

proof end;

theorem Th25: :: TBSP_1:25

for b₁ being non empty MetrStruct holds
( b₁ is bounded iff [#] b₁ is bounded )

proof end;

registration

let c₁ be non empty bounded MetrStruct ;
cluster [#] a₁ -> bounded ;
coherence by Th25;

end;

theorem Th26: :: TBSP_1:26

for b₁ being non empty Reflexive symmetric triangle MetrStruct st b₁ is totally_bounded holds
b₁ is bounded

proof end;

definition

let c₁ be non empty Reflexive MetrStruct ;
let c₂ be Subset of c₁;
assume E25: c₂ is bounded ;
func diameter c₂ -> Real means :Def10: :: TBSP_1:def 10
( ( for b₁, b₂ being Point of a₁ st b₁ in a₂ & b₂ in a₂ holds
dist b₁,b₂ <= a₃ ) & ( for b₁ being Real st ( for b₂, b₃ being Point of a₁ st b₂ in a₂ & b₃ in a₂ holds
dist b₂,b₃ <= b₁ ) holds
a₃ <= b₁ ) ) if a₂ <> {}
otherwise a₃ = 0;
consistency ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines diameter TBSP_1:def 10 :

theorem Th27: :: TBSP_1:27

canceled;

theorem Th28: :: TBSP_1:28

for b₁ being non empty Reflexive symmetric triangle MetrStruct
for b₂ being set
for b₃ being Subset of b₁ st b₃ = {b₂} holds
diameter b₃ = 0

proof end;

theorem Th29: :: TBSP_1:29

for b₁ being non empty Reflexive MetrStruct
for b₂ being Subset of b₁ st b₂ is bounded holds
0 <= diameter b₂

proof end;

theorem Th30: :: TBSP_1:30

for b₁ being non empty MetrSpace
for b₂ being Subset of b₁ st b₂ <> {} & b₂ is bounded & diameter b₂ = 0 holds
ex b₃ being Point of b₁ st b₂ = {b₃}

proof end;

theorem Th31: :: TBSP_1:31

for b₁ being non empty Reflexive symmetric triangle MetrStruct
for b₂ being Element of b₁
for b₃ being Real st 0 < b₃ holds
diameter (Ball b₂,b₃) <= 2 * b₃

proof end;

theorem Th32: :: TBSP_1:32

for b₁ being non empty Reflexive MetrStruct
for b₂, b₃ being Subset of b₁ st b₂ is bounded & b₃ c= b₂ holds
diameter b₃ <= diameter b₂

proof end;

theorem Th33: :: TBSP_1:33

for b₁ being non empty Reflexive symmetric triangle MetrStruct
for b₂, b₃ being Subset of b₁ st b₂ is bounded & b₃ is bounded & b₂ meets b₃ holds
diameter (b₂ \/ b₃) <= (diameter b₂) + (diameter b₃)

proof end;

definition

let c₁ be non empty MetrStruct ;
let c₂ be sequence of c₁;
redefine func rng as rng c₂ -> Subset of a₁;
coherence by RELSET_1:12;

end;

theorem Th34: :: TBSP_1:34

for b₁ being non empty Reflexive symmetric triangle MetrStruct
for b₂ being sequence of b₁ st b₂ is Cauchy holds
rng b₂ is bounded

proof end;