begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th9:
theorem
canceled;
theorem Th11:
theorem Th12:
theorem Th13:
begin
theorem Th14:
theorem
definition
canceled;let A,
B be
Subset of
REAL;
func dist (
A,
B)
-> real number means :
Def2:
ex
X being
Subset of
REAL st
(
X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } &
it = lower_bound X );
existence
ex b1 being real number ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b1 = lower_bound X )
uniqueness
for b1, b2 being real number st ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b1 = lower_bound X ) & ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b2 = lower_bound X ) holds
b1 = b2
;
commutativity
for b1 being real number
for A, B being Subset of REAL st ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b1 = lower_bound X ) holds
ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in B & s in A ) } & b1 = lower_bound X )
end;
:: deftheorem JCT_MISC:def 1 :
canceled;
:: deftheorem Def2 defines dist JCT_MISC:def 2 :
for A, B being Subset of REAL
for b3 being real number holds
( b3 = dist (A,B) iff ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & b3 = lower_bound X ) );
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem