:: JCT_MISC semantic presentation

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

not { F₂(a) where a is Element of F₁() : verum } is empty

proof end;

theorem :: JCT_MISC:1

canceled;

theorem :: JCT_MISC:2

canceled;

theorem Th3: :: JCT_MISC:3

for A, B being set
for f being Function st A c= dom f & f .: A c= B holds
A c= f " B

proof end;

theorem Th4: :: JCT_MISC:4

for f being Function
for A, B being set st A misses B holds
f " A misses f " B

proof end;

theorem Th5: :: JCT_MISC:5

for S, X being set
for f being Function of S,X
for A being Subset of X st ( X = {} implies S = {} ) holds
(f " A) ` = f " (A ` )

proof end;

theorem :: JCT_MISC:6

for S being 1-sorted
for X being non empty set
for f being Function of the carrier of S,X
for A being Subset of X holds (f " A) ` = f " (A ` ) by Th5;

theorem :: JCT_MISC:7

for m, n being Nat st m <= n holds
n -' (n -' m) = m

proof end;

theorem :: JCT_MISC:8

canceled;

theorem Th9: :: JCT_MISC:9

for r, s, a, b being real number st r in [.a,b.] & s in [.a,b.] holds
(r + s) / 2 in [.a,b.]

proof end;

Lm1: for Nseq being increasing Seq_of_Nat
for i, j being Nat st i <= j holds
Nseq . i <= Nseq . j
by SEQM_3:12;

theorem :: JCT_MISC:10

canceled;

theorem Th11: :: JCT_MISC:11

for r0, s0, r, s being real number holds abs ((abs (r0 - s0)) - (abs (r - s))) <= (abs (r0 - r)) + (abs (s0 - s))

proof end;

theorem :: JCT_MISC:12

for t, r, s being real number st t in ].r,s.[ holds
abs t < max (abs r),(abs s)

proof end;

definition

let A, B, C be non empty set ;
let f be Function of A,[:B,C:];
:: original: pr1
redefine func pr1 f -> Function of A,B means :Def1: :: JCT_MISC:def 1
for x being Element of A holds it . x = (f . x) `1 ;
coherence

proof end;

compatibility

proof end;

:: original: pr2
redefine func pr2 f -> Function of A,C means :Def2: :: JCT_MISC:def 2
for x being Element of A holds it . x = (f . x) `2 ;
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def1 defines pr1 JCT_MISC:def 1 :

:: deftheorem Def2 defines pr2 JCT_MISC:def 2 :

scheme :: JCT_MISC:sch 2
DoubleChoice{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , P₁[ set , set , set ] } :

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 Th13: :: JCT_MISC:13

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 Th14: :: JCT_MISC:14

for A, B being compact Subset of REAL holds A /\ B is compact

proof end;

definition

let A be Subset of REAL ;
attr A is connected means :Def3: :: JCT_MISC:def 3
for r, s being real number st r in A & s in A holds
[.r,s.] c= A;

end;

:: deftheorem Def3 defines connected JCT_MISC:def 3 :

theorem :: JCT_MISC:15

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 connected

proof end;

definition

let A, B be Subset of REAL ;
func dist A,B -> real number means :Def4: :: JCT_MISC:def 4
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

proof end;

uniqueness ;
commutativity

proof end;

end;

:: deftheorem Def4 defines dist JCT_MISC:def 4 :

theorem Th16: :: JCT_MISC:16

for A, B being Subset of REAL
for r, s being real number st r in A & s in B holds
abs (r - s) >= dist A,B

proof end;

theorem Th17: :: JCT_MISC:17

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 Th18: :: JCT_MISC:18

for A, B being non empty compact Subset of REAL ex r, s being real number st
( r in A & s in B & dist A,B = abs (r - s) )

proof end;

theorem Th19: :: JCT_MISC:19

for A, B being non empty compact Subset of REAL holds dist A,B >= 0

proof end;

theorem Th20: :: JCT_MISC:20

for A, B being non empty compact Subset of REAL st A misses B holds
dist A,B > 0

proof end;

theorem :: JCT_MISC:21

for e, f being real number
for A, B being compact Subset of REAL st A misses B & A c= [.e,f.] & B c= [.e,f.] holds
for S being Function of NAT , bool REAL st ( for i being Nat holds
( S . i is connected & S . i meets A & S . i meets B ) ) holds
ex r being real number 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;