:: JORDAN7 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: 2 -' 1 = 2 - 1 by BINARITH:50
.= 1 ;

Lm2: for i, j, k being Nat st i -' k <= j holds
i <= j + k
proof end;

Lm3: for i, j, k being Nat st j + k <= i holds
k <= i -' j
proof end;

theorem Th1: :: JORDAN7:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2) st P is_simple_closed_curve holds
( W-min P in Lower_Arc P & E-max P in Lower_Arc P & W-min P in Upper_Arc P & E-max P in Upper_Arc P )
proof end;

theorem Th2: :: JORDAN7:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st P is_simple_closed_curve & LE q, W-min P,P holds
q = W-min P
proof end;

theorem Th3: :: JORDAN7:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st P is_simple_closed_curve & q in P holds
LE W-min P,q,P
proof end;

definition
let P be non empty compact Subset of (TOP-REAL 2);
let q1, q2 be Point of (TOP-REAL 2);
func Segment q1,q2,P -> Subset of (TOP-REAL 2) equals :Def1: :: JORDAN7:def 1
{ p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } if q2 <> W-min P
otherwise { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ;
correctness
coherence
( ( q2 <> W-min P implies { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } is Subset of (TOP-REAL 2) ) & ( not q2 <> W-min P implies { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } is Subset of (TOP-REAL 2) ) )
;
consistency
for b1 being Subset of (TOP-REAL 2) holds verum
;
proof end;
end;

:: deftheorem Def1 defines Segment JORDAN7:def 1 :
for P being non empty compact Subset of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2) holds
( ( q2 <> W-min P implies Segment q1,q2,P = { p where p is Point of (TOP-REAL 2) : ( LE q1,p,P & LE p,q2,P ) } ) & ( not q2 <> W-min P implies Segment q1,q2,P = { p1 where p1 is Point of (TOP-REAL 2) : ( LE q1,p1,P or ( q1 in P & p1 = W-min P ) ) } ) );

theorem :: JORDAN7:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2) st P is_simple_closed_curve holds
( Segment (W-min P),(E-max P),P = Upper_Arc P & Segment (E-max P),(W-min P),P = Lower_Arc P )
proof end;

theorem Th5: :: JORDAN7:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2) st P is_simple_closed_curve & LE q1,q2,P holds
( q1 in P & q2 in P )
proof end;

theorem Th6: :: JORDAN7:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2) st P is_simple_closed_curve & LE q1,q2,P holds
( q1 in Segment q1,q2,P & q2 in Segment q1,q2,P )
proof end;

theorem Th7: :: JORDAN7:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2)
for q1 being Point of (TOP-REAL 2) st q1 in P & P is_simple_closed_curve holds
q1 in Segment q1,(W-min P),P
proof end;

theorem :: JORDAN7:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st P is_simple_closed_curve & q in P & q <> W-min P holds
Segment q,q,P = {q}
proof end;

theorem :: JORDAN7:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2) st P is_simple_closed_curve & q1 <> W-min P & q2 <> W-min P holds
not W-min P in Segment q1,q2,P
proof end;

theorem Th10: :: JORDAN7:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2)
for q1, q2, q3 being Point of (TOP-REAL 2) st P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & ( not q1 = q2 or not q1 = W-min P ) & q1 <> q3 & ( not q2 = q3 or not q2 = W-min P ) holds
(Segment q1,q2,P) /\ (Segment q2,q3,P) = {q2}
proof end;

theorem Th11: :: JORDAN7:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2) st P is_simple_closed_curve & LE q1,q2,P & q1 <> W-min P & q2 <> W-min P holds
(Segment q1,q2,P) /\ (Segment q2,(W-min P),P) = {q2}
proof end;

theorem Th12: :: JORDAN7:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2) st P is_simple_closed_curve & LE q1,q2,P & q1 <> q2 & q1 <> W-min P holds
(Segment q2,(W-min P),P) /\ (Segment (W-min P),q1,P) = {(W-min P)}
proof end;

theorem Th13: :: JORDAN7:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2)
for q1, q2, q3, q4 being Point of (TOP-REAL 2) st P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P & q1 <> q2 & q2 <> q3 holds
Segment q1,q2,P misses Segment q3,q4,P
proof end;

theorem Th14: :: JORDAN7:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2)
for q1, q2, q3 being Point of (TOP-REAL 2) st P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & q1 <> W-min P & q1 <> q2 & q2 <> q3 holds
Segment q1,q2,P misses Segment q3,(W-min P),P
proof end;

theorem Th15: :: JORDAN7:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for P being non empty Subset of (TOP-REAL n)
for f being Function of I[01] ,((TOP-REAL n) | P) st P <> {} & f is_homeomorphism holds
ex g being Function of I[01] ,(TOP-REAL n) st
( f = g & g is continuous & g is one-to-one )
proof end;

theorem Th16: :: JORDAN7:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for P being non empty Subset of (TOP-REAL n)
for g being Function of I[01] ,(TOP-REAL n) st g is continuous & g is one-to-one & rng g = P holds
ex f being Function of I[01] ,((TOP-REAL n) | P) st
( f = g & f is_homeomorphism )
proof end;

registration
cluster increasing -> one-to-one FinSequence of REAL ;
coherence
for b1 being FinSequence of REAL st b1 is increasing holds
b1 is one-to-one
proof end;
end;

theorem Th17: :: JORDAN7:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of REAL st f is increasing holds
f is one-to-one
proof end;

Lm4: now
let h2 be Nat; :: thesis: (h2 - 1) - 1 < h2
h2 < h2 + 1 by NAT_1:38;
then h2 - 1 < (h2 + 1) - 1 by XREAL_1:11;
then ( (h2 - 1) - 1 < h2 - 1 & h2 - 1 < h2 ) by XREAL_1:11;
hence (h2 - 1) - 1 < h2 by XREAL_1:2; :: thesis: verum
end;

Lm5: ( 0 in [.0,1.] & 1 in [.0,1.] )
by RCOMP_1:15;

theorem Th18: :: JORDAN7:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 holds
ex g being Function of I[01] ,(TOP-REAL 2) st
( g is continuous & g is one-to-one & rng g = A & g . 0 = p1 & g . 1 = p2 )
proof end;

theorem Th19: :: JORDAN7:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2)
for g being Function of I[01] ,(TOP-REAL 2)
for s1, s2 being Real st P is_an_arc_of p1,p2 & g is continuous & g is one-to-one & rng g = P & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 holds
LE q1,q2,P,p1,p2
proof end;

theorem Th20: :: JORDAN7:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2)
for g being Function of I[01] ,(TOP-REAL 2)
for s1, s2 being Real st g is continuous & g is one-to-one & rng g = P & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & LE q1,q2,P,p1,p2 holds
s1 <= s2
proof end;

theorem :: JORDAN7:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being non empty compact Subset of (TOP-REAL 2)
for e being Real st P is_simple_closed_curve & e > 0 holds
ex h being FinSequence of the carrier of (TOP-REAL 2) st
( h . 1 = W-min P & h is one-to-one & 8 <= len h & rng h c= P & ( for i being Nat st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),P ) & ( for i being Nat
for W being Subset of (Euclid 2) st 1 <= i & i < len h & W = Segment (h /. i),(h /. (i + 1)),P holds
diameter W < e ) & ( for W being Subset of (Euclid 2) st W = Segment (h /. (len h)),(h /. 1),P holds
diameter W < e ) & ( for i being Nat st 1 <= i & i + 1 < len h holds
(Segment (h /. i),(h /. (i + 1)),P) /\ (Segment (h /. (i + 1)),(h /. (i + 2)),P) = {(h /. (i + 1))} ) & (Segment (h /. (len h)),(h /. 1),P) /\ (Segment (h /. 1),(h /. 2),P) = {(h /. 1)} & (Segment (h /. ((len h) -' 1)),(h /. (len h)),P) /\ (Segment (h /. (len h)),(h /. 1),P) = {(h /. (len h))} & Segment (h /. ((len h) -' 1)),(h /. (len h)),P misses Segment (h /. 1),(h /. 2),P & ( for i, j being Nat st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment (h /. i),(h /. (i + 1)),P misses Segment (h /. j),(h /. (j + 1)),P ) & ( for i being Nat st 1 < i & i + 1 < len h holds
Segment (h /. (len h)),(h /. 1),P misses Segment (h /. i),(h /. (i + 1)),P ) )
proof end;