begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem
theorem
definition
let A be non
empty set ;
let G be
Function of
[:A,A:],
REAL ;
canceled;canceled;canceled;func bounded_metric A,
G -> Function of
[:A,A:],
REAL means :
Def4:
for
a,
b being
Element of
A holds
it . a,
b = (G . a,b) / (1 + (G . a,b));
existence
ex b1 being Function of [:A,A:],REAL st
for a, b being Element of A holds b1 . a,b = (G . a,b) / (1 + (G . a,b))
uniqueness
for b1, b2 being Function of [:A,A:],REAL st ( for a, b being Element of A holds b1 . a,b = (G . a,b) / (1 + (G . a,b)) ) & ( for a, b being Element of A holds b2 . a,b = (G . a,b) / (1 + (G . a,b)) ) holds
b1 = b2
end;
:: deftheorem METRIC_6:def 1 :
canceled;
:: deftheorem METRIC_6:def 2 :
canceled;
:: deftheorem METRIC_6:def 3 :
canceled;
:: deftheorem Def4 defines bounded_metric METRIC_6:def 4 :
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th10:
:: deftheorem METRIC_6:def 5 :
canceled;
:: deftheorem METRIC_6:def 6 :
canceled;
:: deftheorem METRIC_6:def 7 :
canceled;
:: deftheorem Def8 defines is_convergent_in_metrspace_to METRIC_6:def 8 :
:: deftheorem METRIC_6:def 9 :
canceled;
:: deftheorem defines bounded METRIC_6:def 10 :
:: deftheorem Def11 defines bounded METRIC_6:def 11 :
:: deftheorem Def12 defines contains_almost_all_sequence METRIC_6:def 12 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th20:
theorem Th21:
theorem Th22:
:: deftheorem METRIC_6:def 13 :
canceled;
:: deftheorem Def14 defines dist_to_point METRIC_6:def 14 :
:: deftheorem Def15 defines sequence_of_dist METRIC_6:def 15 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem
theorem
theorem Th36:
theorem
theorem Th38:
theorem
theorem
theorem
canceled;
theorem
theorem
theorem Th44: