:: METRIC_6 semantic presentation

theorem Th1: :: METRIC_6:1

for b₁ being MetrSpace
for b₂, b₃, b₄ being Element of b₁ holds abs ((dist b₂,b₃) - (dist b₄,b₃)) <= dist b₂,b₄

proof end;

theorem Th2: :: METRIC_6:2

for b₁ being non empty set
for b₂ being Function of [:b₁,b₁:], REAL st b₂ is_metric_of b₁ holds
for b₃, b₄ being Element of b₁ holds 0 <= b₂ . b₃,b₄

proof end;

theorem Th3: :: METRIC_6:3

for b₁ being non empty set
for b₂ being Function of [:b₁,b₁:], REAL holds
( b₂ is_metric_of b₁ iff ( b₂ is Reflexive & b₂ is discerning & b₂ is symmetric & b₂ is triangle ) )

proof end;

theorem Th4: :: METRIC_6:4

for b₁ being non empty strict MetrSpace holds
( the distance of b₁ is Reflexive & the distance of b₁ is discerning & the distance of b₁ is symmetric & the distance of b₁ is triangle )

proof end;

theorem Th5: :: METRIC_6:5

for b₁ being non empty set
for b₂ being Function of [:b₁,b₁:], REAL holds
( b₂ is_metric_of b₁ iff ( b₂ is Reflexive & b₂ is discerning & ( for b₃, b₄, b₅ being Element of b₁ holds b₂ . b₄,b₅ <= (b₂ . b₃,b₄) + (b₂ . b₃,b₅) ) ) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be Function of [:c₁,c₁:], REAL ;
canceled;
canceled;
canceled;
func bounded_metric c₁,c₂ -> Function of [:a₁,a₁:], REAL means :Def4: :: METRIC_6:def 4
for b₁, b₂ being Element of a₁ holds a₃ . b₁,b₂ = (a₂ . b₁,b₂) / (1 + (a₂ . b₁,b₂));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 METRIC_6:def 1 :

:: deftheorem Def2 METRIC_6:def 2 :

:: deftheorem Def3 METRIC_6:def 3 :

:: deftheorem Def4 defines bounded_metric METRIC_6:def 4 :

theorem Th6: :: METRIC_6:6

for b₁ being non empty set
for b₂ being Function of [:b₁,b₁:], REAL st b₂ is_metric_of b₁ holds
bounded_metric b₁,b₂ is_metric_of b₁

proof end;

theorem Th7: :: METRIC_6:7

canceled;

theorem Th8: :: METRIC_6:8

canceled;

theorem Th9: :: METRIC_6:9

canceled;

theorem Th10: :: METRIC_6:10

for b₁ being non empty MetrSpace
for b₂ being Element of b₁ ex b₃ being sequence of b₁ st rng b₃ = {b₂}

proof end;

definition

let c₁ be non empty MetrStruct ;
let c₂ be sequence of c₁;
let c₃ be Element of c₁;
canceled;
canceled;
canceled;
pred c₂ is_convergent_in_metrspace_to c₃ means :Def8: :: METRIC_6:def 8
for b₁ being Real st 0 < b₁ holds
ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
dist (a₂ . b₃),a₃ < b₁;

end;

:: deftheorem Def5 METRIC_6:def 5 :

:: deftheorem Def6 METRIC_6:def 6 :

:: deftheorem Def7 METRIC_6:def 7 :

:: deftheorem Def8 defines is_convergent_in_metrspace_to METRIC_6:def 8 :

definition

let c₁ be non empty symmetric triangle MetrStruct ;
let c₂ be Subset of c₁;
canceled;
redefine attr a₂ is bounded means :: METRIC_6:def 10
ex b₁ being Realex b₂ being Element of a₁ st
( 0 < b₁ & a₂ c= Ball b₂,b₁ );
compatibility

proof end;

end;

:: deftheorem Def9 METRIC_6:def 9 :

:: deftheorem Def10 defines bounded METRIC_6:def 10 :

definition

let c₁ be non empty MetrStruct ;
let c₂ be sequence of c₁;
attr a₂ is bounded means :Def11: :: METRIC_6:def 11
ex b₁ being Realex b₂ being Element of a₁ st
( 0 < b₁ & rng a₂ c= Ball b₂,b₁ );

end;

:: deftheorem Def11 defines bounded METRIC_6:def 11 :

definition

let c₁ be non empty MetrSpace;
let c₂ be Subset of c₁;
let c₃ be sequence of c₁;
pred c₂ contains_almost_all_sequence c₃ means :Def12: :: METRIC_6:def 12
ex b₁ being Nat st
for b₂ being Nat st b₁ <= b₂ holds
a₃ . b₂ in a₂;

end;

:: deftheorem Def12 defines contains_almost_all_sequence METRIC_6:def 12 :

theorem Th11: :: METRIC_6:11

canceled;

theorem Th12: :: METRIC_6:12

canceled;

theorem Th13: :: METRIC_6:13

canceled;

theorem Th14: :: METRIC_6:14

canceled;

theorem Th15: :: METRIC_6:15

canceled;

theorem Th16: :: METRIC_6:16

canceled;

theorem Th17: :: METRIC_6:17

canceled;

theorem Th18: :: METRIC_6:18

canceled;

theorem Th19: :: METRIC_6:19

canceled;

theorem Th20: :: METRIC_6:20

for b₁ being non empty MetrSpace
for b₂ being sequence of b₁ holds
( b₂ is bounded iff ex b₃ being Realex b₄ being Element of b₁ st
( 0 < b₃ & ( for b₅ being Nat holds b₂ . b₅ in Ball b₄,b₃ ) ) )

proof end;

theorem Th21: :: METRIC_6:21

for b₁ being non empty MetrSpace
for b₂ being Element of b₁
for b₃ being sequence of b₁ st b₃ is_convergent_in_metrspace_to b₂ holds
b₃ is convergent

proof end;

theorem Th22: :: METRIC_6:22

for b₁ being non empty MetrSpace
for b₂ being sequence of b₁ st b₂ is convergent holds
ex b₃ being Element of b₁ st b₂ is_convergent_in_metrspace_to b₃

proof end;

definition

let c₁ be non empty MetrSpace;
let c₂ be sequence of c₁;
let c₃ be Element of c₁;
canceled;
func dist_to_point c₂,c₃ -> Real_Sequence means :Def14: :: METRIC_6:def 14
for b₁ being Nat holds a₄ . b₁ = dist (a₂ . b₁),a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 METRIC_6:def 13 :

:: deftheorem Def14 defines dist_to_point METRIC_6:def 14 :

definition

let c₁ be non empty MetrSpace;
let c₂, c₃ be sequence of c₁;
func sequence_of_dist c₂,c₃ -> Real_Sequence means :Def15: :: METRIC_6:def 15
for b₁ being Nat holds a₄ . b₁ = dist (a₂ . b₁),(a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines sequence_of_dist METRIC_6:def 15 :

theorem Th23: :: METRIC_6:23

canceled;

theorem Th24: :: METRIC_6:24

canceled;

theorem Th25: :: METRIC_6:25

canceled;

theorem Th26: :: METRIC_6:26

for b₁ being non empty MetrSpace
for b₂ being Element of b₁
for b₃ being sequence of b₁ st b₃ is_convergent_in_metrspace_to b₂ holds
lim b₃ = b₂

proof end;

theorem Th27: :: METRIC_6:27

for b₁ being non empty MetrSpace
for b₂ being Element of b₁
for b₃ being sequence of b₁ holds
( b₃ is_convergent_in_metrspace_to b₂ iff ( b₃ is convergent & lim b₃ = b₂ ) )

proof end;

theorem Th28: :: METRIC_6:28

for b₁ being non empty MetrSpace
for b₂ being sequence of b₁ st b₂ is convergent holds
ex b₃ being Element of b₁ st
( b₂ is_convergent_in_metrspace_to b₃ & lim b₂ = b₃ )

proof end;

theorem Th29: :: METRIC_6:29

for b₁ being non empty MetrSpace
for b₂ being Element of b₁
for b₃ being sequence of b₁ holds
( b₃ is_convergent_in_metrspace_to b₂ iff ( dist_to_point b₃,b₂ is convergent & lim (dist_to_point b₃,b₂) = 0 ) )

proof end;

theorem Th30: :: METRIC_6:30

for b₁ being non empty MetrSpace
for b₂ being Element of b₁
for b₃ being sequence of b₁ st b₃ is_convergent_in_metrspace_to b₂ holds
for b₄ being Real st 0 < b₄ holds
Ball b₂,b₄ contains_almost_all_sequence b₃

proof end;

theorem Th31: :: METRIC_6:31

for b₁ being non empty MetrSpace
for b₂ being Element of b₁
for b₃ being sequence of b₁ st ( for b₄ being Real st 0 < b₄ holds
Ball b₂,b₄ contains_almost_all_sequence b₃ ) holds
for b₄ being Subset of b₁ st b₂ in b₄ & b₄ in Family_open_set b₁ holds
b₄ contains_almost_all_sequence b₃

proof end;

theorem Th32: :: METRIC_6:32

for b₁ being non empty MetrSpace
for b₂ being Element of b₁
for b₃ being sequence of b₁ st ( for b₄ being Subset of b₁ st b₂ in b₄ & b₄ in Family_open_set b₁ holds
b₄ contains_almost_all_sequence b₃ ) holds
b₃ is_convergent_in_metrspace_to b₂

proof end;

theorem Th33: :: METRIC_6:33

for b₁ being non empty MetrSpace
for b₂ being Element of b₁
for b₃ being sequence of b₁ holds
( b₃ is_convergent_in_metrspace_to b₂ iff for b₄ being Real st 0 < b₄ holds
Ball b₂,b₄ contains_almost_all_sequence b₃ )

proof end;

theorem Th34: :: METRIC_6:34

for b₁ being non empty MetrSpace
for b₂ being Element of b₁
for b₃ being sequence of b₁ holds
( b₃ is_convergent_in_metrspace_to b₂ iff for b₄ being Subset of b₁ st b₂ in b₄ & b₄ in Family_open_set b₁ holds
b₄ contains_almost_all_sequence b₃ )

proof end;

theorem Th35: :: METRIC_6:35

for b₁ being non empty MetrSpace
for b₂ being Element of b₁
for b₃ being sequence of b₁ holds
( ( for b₄ being Real st 0 < b₄ holds
Ball b₂,b₄ contains_almost_all_sequence b₃ ) iff for b₄ being Subset of b₁ st b₂ in b₄ & b₄ in Family_open_set b₁ holds
b₄ contains_almost_all_sequence b₃ )

proof end;

theorem Th36: :: METRIC_6:36

for b₁ being non empty MetrSpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
dist (lim b₂),(lim b₃) = lim (sequence_of_dist b₂,b₃)

proof end;

theorem Th37: :: METRIC_6:37

for b₁ being non empty MetrSpace
for b₂, b₃ being Element of b₁
for b₄ being sequence of b₁ st b₄ is_convergent_in_metrspace_to b₂ & b₄ is_convergent_in_metrspace_to b₃ holds
b₂ = b₃

proof end;

theorem Th38: :: METRIC_6:38

for b₁ being non empty MetrSpace
for b₂ being sequence of b₁ st b₂ is constant holds
b₂ is convergent

proof end;

theorem Th39: :: METRIC_6:39

for b₁ being non empty MetrSpace
for b₂ being Element of b₁
for b₃, b₄ being sequence of b₁ st b₃ is_convergent_in_metrspace_to b₂ & b₄ is subsequence of b₃ holds
b₄ is_convergent_in_metrspace_to b₂

proof end;

theorem Th40: :: METRIC_6:40

for b₁ being non empty MetrSpace
for b₂, b₃ being sequence of b₁ st b₂ is Cauchy & b₃ is subsequence of b₂ holds
b₃ is Cauchy

proof end;

theorem Th41: :: METRIC_6:41

canceled;

theorem Th42: :: METRIC_6:42

for b₁ being non empty MetrSpace
for b₂ being sequence of b₁ st b₂ is constant holds
b₂ is Cauchy

proof end;

theorem Th43: :: METRIC_6:43

for b₁ being non empty MetrSpace
for b₂ being sequence of b₁ st b₂ is convergent holds
b₂ is bounded

proof end;

theorem Th44: :: METRIC_6:44

for b₁ being non empty MetrSpace
for b₂ being sequence of b₁ st b₂ is Cauchy holds
b₂ is bounded

proof end;

registration

let c₁ be non empty MetrSpace;
cluster V80 -> convergent M5( NAT ,the carrier of a₁);
coherence by Th38;
cluster Cauchy -> bounded M5( NAT ,the carrier of a₁);
coherence by Th44;

end;

registration

let c₁ be non empty MetrSpace;
cluster convergent Cauchy V80 bounded M5( NAT ,the carrier of a₁);
existence

proof end;

end;