:: by Andrzej Trybulec

::

:: Received August 28, 2000

:: Copyright (c) 2000-2021 Association of Mizar Users

scheme :: JCT_MISC:sch 2

DoubleChoice{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , P_{1}[ object , object , object ] } :

DoubleChoice{ F

ex a being Function of F_{1}(),F_{2}() ex b being Function of F_{1}(),F_{3}() st

for i being Element of F_{1}() holds P_{1}[i,a . i,b . i]

providedfor i being Element of F

A1:
for i being Element of F_{1}() ex ai being Element of F_{2}() ex bi being Element of F_{3}() st P_{1}[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

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 :: 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

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;

ex b_{1} being Real ex X being Subset of REAL st

( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & b_{1} = lower_bound X )

for b_{1}, b_{2} being Real st ex X being Subset of REAL st

( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & b_{1} = lower_bound X ) & ex X being Subset of REAL st

( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & b_{2} = lower_bound X ) holds

b_{1} = b_{2}
;

commutativity

for b_{1} 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 ) } & b_{1} = 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 ) } & b_{1} = lower_bound X )

end;
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 X being Subset of REAL st

( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & it = lower_bound X );

ex b

( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & b

proof end;

uniqueness for b

( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & b

( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & b

b

commutativity

for b

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 ) } & b

ex X being Subset of REAL st

( X = { |.(r - s).| where r, s is Real : ( r in B & s in A ) } & b

proof end;

:: deftheorem Def1 defines dist JCT_MISC:def 1 :

for A, B being Subset of REAL

for b_{3} being Real holds

( b_{3} = 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 ) } & b_{3} = lower_bound X ) );

for A, B being Subset of REAL

for b

( b

( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & b

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)

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)

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).| )

( r in A & s in B & dist (A,B) = |.(r - s).| )

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 ) ) )

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