JCT_MISC: Miscellaneous { I }

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

scheme :: JCT_MISC:sch 1
NonEmpty{ F₁() -> non empty set , F₂( object ) -> set } :

not { F₂(a) where a is Element of F₁() : 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{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , P₁[ object , object , object ] } :

ex a being Function of F₁(),F₂() ex b being Function of F₁(),F₃() st
for i being Element of F₁() holds P₁[i,a . i,b . i]

provided

A1: for i being Element of F₁() ex ai being Element of F₂() ex bi being Element of F₃() st P₁[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

proof end;

uniqueness ;
commutativity

proof end;

end;

:: deftheorem Def1 defines dist JCT_MISC:def 1 :

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;