:: Miscellaneous { I }
:: by Andrzej Trybulec
::
:: Received August 28, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem :: JCT_MISC:1
canceled;
theorem :: JCT_MISC:2
canceled;
theorem :: JCT_MISC:3
canceled;
theorem :: JCT_MISC:4
canceled;
theorem :: JCT_MISC:5
canceled;
theorem :: JCT_MISC:6
canceled;
theorem :: JCT_MISC:7
canceled;
theorem :: JCT_MISC:8
canceled;
theorem Th9: :: JCT_MISC:9
theorem :: JCT_MISC:10
canceled;
theorem Th11: :: JCT_MISC:11
theorem Th12: :: JCT_MISC:12
theorem Th13: :: JCT_MISC:13
theorem Th14: :: JCT_MISC:14
:: deftheorem Def1 defines connected JCT_MISC:def 1 :
theorem :: JCT_MISC:15
definition
let A,
B be
Subset of
REAL ;
func dist A,
B -> real number means :
Def2:
:: JCT_MISC:def 2
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 Def2 defines dist JCT_MISC:def 2 :
theorem Th16: :: JCT_MISC:16
theorem Th17: :: JCT_MISC:17
theorem Th18: :: JCT_MISC:18
theorem Th19: :: JCT_MISC:19
theorem Th20: :: JCT_MISC:20
theorem :: JCT_MISC:21
theorem Th22: :: JCT_MISC:22
theorem Th23: :: JCT_MISC:23
theorem :: JCT_MISC:24