:: JCT_MISC semantic presentation

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

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

proof end;

theorem Th1: :: JCT_MISC:1

canceled;

theorem Th2: :: JCT_MISC:2

canceled;

theorem Th3: :: JCT_MISC:3

for b₁, b₂ being set
for b₃ being Function st b₁ c= dom b₃ & b₃ .: b₁ c= b₂ holds
b₁ c= b₃ " b₂

proof end;

theorem Th4: :: JCT_MISC:4

for b₁ being Function
for b₂, b₃ being set st b₂ misses b₃ holds
b₁ " b₂ misses b₁ " b₃

proof end;

theorem Th5: :: JCT_MISC:5

for b₁, b₂ being set
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₂ st ( b₂ = {} implies b₁ = {} ) holds
(b₃ " b₄) ` = b₃ " (b₄ ` )

proof end;

theorem Th6: :: JCT_MISC:6

for b₁ being 1-sorted
for b₂ being non empty set
for b₃ being Function of the carrier of b₁,b₂
for b₄ being Subset of b₂ holds (b₃ " b₄) ` = b₃ " (b₄ ` ) by Th5;

theorem Th7: :: JCT_MISC:7

for b₁, b₂ being Nat st b₁ <= b₂ holds
b₂ -' (b₂ -' b₁) = b₁

proof end;

theorem Th8: :: JCT_MISC:8

canceled;

theorem Th9: :: JCT_MISC:9

for b₁, b₂, b₃, b₄ being real number st b₁ in [.b₃,b₄.] & b₂ in [.b₃,b₄.] holds
(b₁ + b₂) / 2 in [.b₃,b₄.]

proof end;

Lemma5: for b₁ being increasing Seq_of_Nat
for b₂, b₃ being Nat st b₂ <= b₃ holds
b₁ . b₂ <= b₁ . b₃
by SEQM_3:12;

theorem Th10: :: JCT_MISC:10

canceled;

theorem Th11: :: JCT_MISC:11

for b₁, b₂, b₃, b₄ being real number holds abs ((abs (b₁ - b₂)) - (abs (b₃ - b₄))) <= (abs (b₁ - b₃)) + (abs (b₂ - b₄))

proof end;

theorem Th12: :: JCT_MISC:12

for b₁, b₂, b₃ being real number st b₁ in ].b₂,b₃.[ holds
abs b₁ < max (abs b₂),(abs b₃)

proof end;

definition

let c₁, c₂, c₃ be non empty set ;
let c₄ be Function of c₁,[:c₂,c₃:];
redefine func pr1 as pr1 c₄ -> Function of a₁,a₂ means :Def1: :: JCT_MISC:def 1
for b₁ being Element of a₁ holds a₅ . b₁ = (a₄ . b₁) `1 ;
coherence

proof end;

compatibility

proof end;

redefine func pr2 as pr2 c₄ -> Function of a₁,a₃ means :Def2: :: JCT_MISC:def 2
for b₁ being Element of a₁ holds a₅ . b₁ = (a₄ . b₁) `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
s2{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , P₁[ set , set , set ] } :

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

provided

E9: for b₁ being Element of F₁() ex b₂ being Element of F₂()ex b₃ being Element of F₃() st P₁[b₁,b₂,b₃]

proof end;

theorem Th13: :: JCT_MISC:13

for b₁, b₂ being non empty TopSpace
for b₃ being Subset of [:b₁,b₂:] st ( for b₄ being Point of [:b₁,b₂:] st b₄ in b₃ holds
ex b₅ being Subset of b₁ex b₆ being Subset of b₂ st
( b₅ is open & b₆ is open & b₄ in [:b₅,b₆:] & [:b₅,b₆:] c= b₃ ) ) holds
b₃ is open

proof end;

theorem Th14: :: JCT_MISC:14

for b₁, b₂ being compact Subset of REAL holds b₁ /\ b₂ is compact

proof end;

definition

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

end;

:: deftheorem Def3 defines connected JCT_MISC:def 3 :

theorem Th15: :: JCT_MISC:15

for b₁ being non empty TopSpace
for b₂ being continuous RealMap of b₁
for b₃ being Subset of b₁ st b₃ is connected holds
b₂ .: b₃ is connected

proof end;

definition

let c₁, c₂ be Subset of REAL ;
func dist c₁,c₂ -> real number means :Def4: :: JCT_MISC:def 4
ex b₁ being Subset of REAL st
( b₁ = { (abs (b₂ - b₃)) where B is Element of REAL , B is Element of REAL : ( b₂ in a₁ & b₃ in a₂ ) } & a₃ = lower_bound b₁ );
existence

proof end;

uniqueness ;
commutativity

proof end;

end;

:: deftheorem Def4 defines dist JCT_MISC:def 4 :

theorem Th16: :: JCT_MISC:16

for b₁, b₂ being Subset of REAL
for b₃, b₄ being real number st b₃ in b₁ & b₄ in b₂ holds
abs (b₃ - b₄) >= dist b₁,b₂

proof end;

theorem Th17: :: JCT_MISC:17

for b₁, b₂ being Subset of REAL
for b₃, b₄ being non empty Subset of REAL st b₃ c= b₁ & b₄ c= b₂ holds
dist b₁,b₂ <= dist b₃,b₄

proof end;

theorem Th18: :: JCT_MISC:18

for b₁, b₂ being non empty compact Subset of REAL ex b₃, b₄ being real number st
( b₃ in b₁ & b₄ in b₂ & dist b₁,b₂ = abs (b₃ - b₄) )

proof end;

theorem Th19: :: JCT_MISC:19

for b₁, b₂ being non empty compact Subset of REAL holds dist b₁,b₂ >= 0

proof end;

theorem Th20: :: JCT_MISC:20

for b₁, b₂ being non empty compact Subset of REAL st b₁ misses b₂ holds
dist b₁,b₂ > 0

proof end;

theorem Th21: :: JCT_MISC:21

for b₁, b₂ being real number
for b₃, b₄ being compact Subset of REAL st b₃ misses b₄ & b₃ c= [.b₁,b₂.] & b₄ c= [.b₁,b₂.] holds
for b₅ being Function of NAT , bool REAL st ( for b₆ being Nat holds
( b₅ . b₆ is connected & b₅ . b₆ meets b₃ & b₅ . b₆ meets b₄ ) ) holds
ex b₆ being real number st
( b₆ in [.b₁,b₂.] & not b₆ in b₃ \/ b₄ & ( for b₇ being Nat ex b₈ being Nat st
( b₇ <= b₈ & b₆ in b₅ . b₈ ) ) )

proof end;