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


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

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

theorem Th2: :: JCT_MISC:2
for r, s, r0, s0 being Real holds |.(|.(r0 - s0).| - |.(r - s).|).| <= |.(r0 - r).| + |.(s0 - s).|
proof end;

theorem Th3: :: JCT_MISC:3
for r, s, t being Real st t in ].r,s.[ holds
|.t.| < max (|.r.|,|.s.|)
proof end;

scheme :: JCT_MISC:sch 2
DoubleChoice{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , P1[ object , object , object ] } :
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]
proof end;

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 & GT is open & x in [:GS,GT:] & [:GS,GT:] c= G ) ) holds
G is open
proof end;

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

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
proof end;

definition
let A, B be Subset of REAL;
func dist (A,B) -> Real means :Def1: :: JCT_MISC:def 1
 ex X being Subset of REAL st
( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & it = lower_bound X );
existence
ex b1 being Real ex X being Subset of REAL st
( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & b1 = lower_bound X )
proof end;
uniqueness
for b1, b2 being Real st ex X being Subset of REAL st
( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & b1 = lower_bound X ) & ex X being Subset of REAL st
( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & b2 = lower_bound X ) holds
b1 = b2 ;
commutativity
for b1 being Real
for A, B being Subset of REAL st ex X being Subset of REAL st
( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & b1 = lower_bound X ) holds
ex X being Subset of REAL st
( X = { |.(r - s).| where r, s is Real : ( r in B & s in A ) } & b1 = lower_bound X )
proof end;
end;

:: deftheorem Def1 defines dist JCT_MISC:def 1 :
for A, B being Subset of REAL
for b3 being Real holds
( b3 = dist (A,B) iff ex X being Subset of REAL st
( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & b3 = lower_bound X ) );

theorem Th7: :: JCT_MISC:7
for A, B being Subset of REAL
for r, s being Real st r in A & s in B holds
|.(r - s).| >= dist (A,B)
proof end;

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 & D c= B holds
dist (A,B) <= dist (C,D)
proof end;

theorem Th9: :: JCT_MISC:9
for A, B being non empty compact Subset of REAL ex r, s being Real st
( r in A & s in B & dist (A,B) = |.(r - s).| )
proof end;

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

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

theorem :: JCT_MISC:12
for e, f being Real
for A, B being compact Subset of REAL st A misses B & A c= [.e,f.] & B c= [.e,f.] holds
for S being sequence of (bool REAL) st ( for i being Nat holds
( S . i is interval & S . i meets A & S . i meets B ) ) holds
ex r being Real st
( r in [.e,f.] & not r in A \/ B & ( for i being Nat ex k being Nat st
( i <= k & r in S . k ) ) )
proof end;

:: 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
proof end;

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

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