:: JORDAN16 semantic presentation

for S1 being non empty finite Subset of REAL
for e being Real st ( for r being Real st r in S1 holds
r < e ) holds
max S1 < e

proof end;

registration

let n be Nat;
cluster trivial Element of K40(the carrier of (TOP-REAL n));
existence

proof end;

end;

theorem :: JORDAN16:2

for a, b, c, X being set st a in X & b in X & c in X holds
{a,b,c} c= X

proof end;

theorem :: JORDAN16:3

for n being Nat holds {} (TOP-REAL n) is Bounded

proof end;

theorem :: JORDAN16:4

for C being Simple_closed_curve holds Lower_Arc C <> Upper_Arc C

proof end;

theorem Th5: :: JORDAN16:5

for A being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment A,p1,p2,q1,q2 c= A

proof end;

theorem Th6: :: JORDAN16:6

for T being non empty TopSpace
for A, B being Subset of T st A c= B holds
T | A is SubSpace of T | B

proof end;

theorem Th7: :: JORDAN16:7

for A being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & q in A holds
q in L_Segment A,p1,p2,q

proof end;

theorem Th8: :: JORDAN16:8

for A being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & q in A holds
q in R_Segment A,p1,p2,q

proof end;

theorem Th9: :: JORDAN16:9

for A being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 holds
( q1 in Segment A,p1,p2,q1,q2 & q2 in Segment A,p1,p2,q1,q2 )

proof end;

theorem :: JORDAN16:10

for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) holds Segment p,q,C c= C

proof end;

theorem :: JORDAN16:11

for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st p in C & q in C & not LE p,q,C holds
LE q,p,C

proof end;

theorem Th12: :: JORDAN16:12

for X, Y being non empty TopSpace
for Y0 being non empty SubSpace of Y
for f being Function of X,Y
for g being Function of X,Y0 st f = g & f is continuous holds
g is continuous

proof end;

theorem Th13: :: JORDAN16:13

for S, T being non empty TopSpace
for S0 being non empty SubSpace of S
for T0 being non empty SubSpace of T
for f being Function of S,T st f is_homeomorphism holds
for g being Function of S0,T0 st g = f | S0 & g is onto holds
g is_homeomorphism

proof end;

theorem Th14: :: JORDAN16:14

for P1, P2, P3 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P3 is_an_arc_of p1,p2 & P2 /\ P3 = {p1,p2} & P1 c= P2 \/ P3 & not P1 = P2 holds
P1 = P3

proof end;

theorem Th15: :: JORDAN16:15

for C being Simple_closed_curve
for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 <> A2 holds
( A1 \/ A2 = C & A1 /\ A2 = {p1,p2} )

proof end;

theorem Th16: :: JORDAN16:16

for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A1 /\ A2 = {q1,q2} holds
A1 <> A2

proof end;

theorem :: JORDAN16:17

for C being Simple_closed_curve
for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 & A1 c= C & A2 c= C & A1 /\ A2 = {p1,p2} holds
A1 \/ A2 = C

proof end;

theorem :: JORDAN16:18

for C being Simple_closed_curve
for A1, A2 being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st A1 c= C & A2 c= C & A1 <> A2 & A1 is_an_arc_of p1,p2 & A2 is_an_arc_of p1,p2 holds
for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C & not A = A1 holds
A = A2

proof end;

theorem Th19: :: JORDAN16:19

for C being Simple_closed_curve
for A being non empty Subset of (TOP-REAL 2) st A is_an_arc_of W-min C, E-max C & A c= C & not A = Lower_Arc C holds
A = Upper_Arc C

proof end;

theorem Th20: :: JORDAN16:20

for A being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 holds
ex g being Function of I[01] ,((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 <= s2 & s2 <= 1 )

proof end;

theorem Th21: :: JORDAN16:21

for A being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 & q1 <> q2 holds
ex g being Function of I[01] ,((TOP-REAL 2) | A) ex s1, s2 being Real st
( g is_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & g . s2 = q2 & 0 <= s1 & s1 < s2 & s2 <= 1 )

proof end;

theorem :: JORDAN16:22

for A being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 holds
not Segment A,p1,p2,q1,q2 is empty

proof end;

theorem :: JORDAN16:23

for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st p in C holds
( p in Segment p,(W-min C),C & W-min C in Segment p,(W-min C),C )

proof end;

definition

let f be PartFunc of REAL , REAL ;
attr f is continuous means :Def1: :: JORDAN16:def 1
f is_continuous_on dom f;

end;

:: deftheorem Def1 defines continuous JORDAN16:def 1 :

definition

let f be Function of REAL , REAL ;
redefine attr f is continuous means :: JORDAN16:def 2
f is_continuous_on REAL ;
compatibility

proof end;

end;

:: deftheorem defines continuous JORDAN16:def 2 :

definition

let a, b be real number ;
func AffineMap a,b -> Function of REAL , REAL means :Def3: :: JORDAN16:def 3
for x being real number holds it . x = (a * x) + b;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines AffineMap JORDAN16:def 3 :

registration

let a, b be real number ;
cluster AffineMap a,b -> continuous ;
coherence

proof end;

end;

registration

cluster continuous M5( REAL , REAL );
existence

proof end;

end;

theorem :: JORDAN16:24

for f, g being continuous PartFunc of REAL , REAL holds g * f is continuous PartFunc of REAL , REAL

proof end;

theorem Th25: :: JORDAN16:25

for a, b being real number holds (AffineMap a,b) . 0 = b

proof end;

theorem Th26: :: JORDAN16:26

for a, b being real number holds (AffineMap a,b) . 1 = a + b

proof end;

theorem Th27: :: JORDAN16:27

for a, b being real number st a <> 0 holds
AffineMap a,b is one-to-one

proof end;

theorem :: JORDAN16:28

for a, b, x, y being real number st a > 0 & x < y holds
(AffineMap a,b) . x < (AffineMap a,b) . y

proof end;

theorem :: JORDAN16:29

for a, b, x, y being real number st a < 0 & x < y holds
(AffineMap a,b) . x > (AffineMap a,b) . y

proof end;

theorem Th30: :: JORDAN16:30

for a, b, x, y being real number st a >= 0 & x <= y holds
(AffineMap a,b) . x <= (AffineMap a,b) . y

proof end;

theorem :: JORDAN16:31

for a, b, x, y being real number st a <= 0 & x <= y holds
(AffineMap a,b) . x >= (AffineMap a,b) . y

proof end;

theorem Th32: :: JORDAN16:32

for a, b being real number st a <> 0 holds
rng (AffineMap a,b) = REAL

proof end;

theorem Th33: :: JORDAN16:33

for a, b being real number st a <> 0 holds
(AffineMap a,b) " = AffineMap (a " ),(- (b / a))

proof end;

theorem Th34: :: JORDAN16:34

for a, b being real number st a > 0 holds
(AffineMap a,b) .: [.0,1.] = [.b,(a + b).]

proof end;

theorem Th35: :: JORDAN16:35

for f being Function of R^1 ,R^1
for a, b being Real st a <> 0 & f = AffineMap a,b holds
f is_homeomorphism

proof end;

theorem Th36: :: JORDAN16:36

for A being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 & q1 <> q2 holds
Segment A,p1,p2,q1,q2 is_an_arc_of q1,q2

proof end;

theorem :: JORDAN16:37

for C being Simple_closed_curve
for p1, p2 being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st P c= C & P is_an_arc_of p1,p2 & W-min C in P & E-max C in P & not Upper_Arc C c= P holds
Lower_Arc C c= P

proof end;