:: Miscellaneous { I }
:: by Andrzej Trybulec
::
:: Received August 28, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

scheme :: JCT_MISC:sch 1
NonEmpty{ F1() ->  non empty set , F2( set ) ->  set } :
 not  {  F2(a) where a is Element of F1() : verum  }  is empty
proofend;

theorem Th1: :: JCT_MISC:1
for r, s, a, b being real number st r in [.a,b.] & s in [.a,b.] holds
(r + s) / 2 in [.a,b.]
proofend;

theorem Th2: :: JCT_MISC:2
for r0, s0, r, s being real number holds abs ((abs (r0 - s0)) - (abs (r - s))) <= (abs (r0 - r)) + (abs (s0 - s))
proofend;

theorem Th3: :: JCT_MISC:3
for t, r, s being real number st t in ].r,s.[ holds
abs t < max ((abs r),(abs s))
proofend;

scheme :: JCT_MISC:sch 2
DoubleChoice{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , P1[ set , set , set ] } :
 ex a being Function of F1(),F2() ex b being Function of F1(),F3() st
for i being Element of F1() holds P1[i,a . i,b . i]
provided
A1: for i being Element of F1() ex ai being Element of F2() ex bi being Element of F3() st P1[i,ai,bi]
proofend;

theorem Th4: :: JCT_MISC:4
for S, T being non empty TopSpace
for G being Subset of [:S,T:] st ( for x being Point of [:S,T:] st x in G holds
ex GS being Subset of S ex GT being Subset of T st
( GS is open &amp; GT is open &amp; x in [:GS,GT:] &amp; [:GS,GT:] c= G ) ) holds
G is open
proofend;

begin

theorem Th5: :: JCT_MISC:5
for A, B being compact Subset of REAL holds A /\ B is compact
proofend;

theorem :: JCT_MISC:6
for T being non empty TopSpace
for f being continuous RealMap of T
for A being Subset of T st A is connected holds
f .: A is interval
proofend;

definition
let A, B be Subset of REAL;
func dist (A,B) ->  real number  means :Def1: :: JCT_MISC:def 1
 ex X being Subset of REAL st
( X =  {  (abs (r - s)) where r, s is Element of REAL : ( r in A &amp; s in B )  }  &amp; 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 &amp; s in B )  }  &amp; b1 = lower_bound X )
proofend;
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 &amp; s in B )  }  &amp; b1 = lower_bound X ) &amp; ex X being Subset of REAL st
( X =  {  (abs (r - s)) where r, s is Element of REAL : ( r in A &amp; s in B )  }  &amp; 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 &amp; s in B )  }  &amp; 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 &amp; s in A )  }  &amp; b1 = lower_bound X )
proofend;
end;

:: deftheorem Def1 defines dist JCT_MISC:def_1_:_
 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 &amp; s in B )  }  &amp; b3 = lower_bound X ) );

theorem Th7: :: JCT_MISC:7
for A, B being Subset of REAL
for r, s being real number st r in A &amp; s in B holds
abs (r - s) >= dist (A,B)
proofend;

theorem Th8: :: JCT_MISC:8
for A, B being Subset of REAL
for C, D being non empty Subset of REAL st C c= A &amp; D c= B holds
dist (A,B) <= dist (C,D)
proofend;

theorem Th9: :: JCT_MISC:9
for A, B being non empty compact Subset of REAL ex r, s being real number st
( r in A &amp; s in B &amp; dist (A,B) = abs (r - s) )
proofend;

theorem Th10: :: JCT_MISC:10
for A, B being non empty compact Subset of REAL holds dist (A,B) >= 0
proofend;

theorem Th11: :: JCT_MISC:11
for A, B being non empty compact Subset of REAL st A misses B holds
dist (A,B) > 0
proofend;

theorem :: JCT_MISC:12
for e, f being real number
for A, B being compact Subset of REAL st A misses B &amp; A c= [.e,f.] &amp; B c= [.e,f.] holds
for S being Function of NAT,(bool REAL) st ( for i being Element of NAT holds
( S . i is interval &amp; S . i meets A &amp; S . i meets B ) ) holds
ex r being real number st
( r in [.e,f.] &amp; not r in A \/ B &amp; ( for i being Element of NAT ex k being Element of NAT st
( i <= k &amp; r in S . k ) ) )
proofend;

:: Moved from JORDAN1A, AK, 23.02.2006
theorem Th13: :: JCT_MISC:13
for S being closed Subset of (TOP-REAL 2) st S is bounded holds
proj2 .: S is closed
proofend;

theorem Th14: :: JCT_MISC:14
for S being Subset of (TOP-REAL 2) st S is bounded holds
proj2 .: S is real-bounded
proofend;

theorem :: JCT_MISC:15
for S being compact Subset of (TOP-REAL 2) holds proj2 .: S is compact
proofend;