:: JORDAN5C semantic presentation
begin
theorem Th1: :: JORDAN5C:1
for P, Q being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2)
for f being Function of I[01],((TOP-REAL 2) | P)
for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 0 <= t & t < s1 holds
not f . t in Q ) holds
for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
proof
let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL 2)
for f being Function of I[01],((TOP-REAL 2) | P)
for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 0 <= t & t < s1 holds
not f . t in Q ) holds
for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: for f being Function of I[01],((TOP-REAL 2) | P)
for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 0 <= t & t < s1 holds
not f . t in Q ) holds
for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
let f be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 0 <= t & t < s1 holds
not f . t in Q ) holds
for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
let s1 be Real; ::_thesis: ( q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 0 <= t & t < s1 holds
not f . t in Q ) implies for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q )
assume that
A1: q1 in P and
A2: f . s1 = q1 and
A3: f is being_homeomorphism and
A4: f . 0 = p1 and
A5: f . 1 = p2 and
A6: ( 0 <= s1 & s1 <= 1 ) and
A7: for t being Real st 0 <= t & t < s1 holds
not f . t in Q ; ::_thesis: for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1;
let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds
not g . t in Q )
assume that
A8: g is being_homeomorphism and
A9: g . 0 = p1 and
A10: g . 1 = p2 and
A11: g . s2 = q1 and
A12: 0 <= s2 and
A13: s2 <= 1 ; ::_thesis: for t being Real st 0 <= t & t < s2 holds
not g . t in Q
reconsider f = f, g = g as Function of I[01],((TOP-REAL 2) | P9) ;
A14: f is one-to-one by A3, TOPS_2:def_5;
A15: dom f = [#] I[01] by A3, TOPS_2:def_5;
then A16: 1 in dom f by BORSUK_1:43;
A17: rng f = [#] ((TOP-REAL 2) | P) by A3, TOPS_2:def_5;
then f is onto by FUNCT_2:def_3;
then A18: f " = f " by A14, TOPS_2:def_4;
A19: (f ") . p2 = 1 by A5, A16, A14, A18, FUNCT_1:32;
A20: 0 in dom f by A15, BORSUK_1:43;
A21: (f ") . p1 = 0 by A4, A20, A14, A18, FUNCT_1:32;
set fg = (f ") * g;
A22: f " is being_homeomorphism by A3, TOPS_2:56;
then (f ") * g is being_homeomorphism by A8, TOPS_2:57;
then A23: ( (f ") * g is continuous & (f ") * g is one-to-one ) by TOPS_2:def_5;
let t be Real; ::_thesis: ( 0 <= t & t < s2 implies not g . t in Q )
assume that
A24: 0 <= t and
A25: t < s2 ; ::_thesis: not g . t in Q
A26: t <= 1 by A13, A25, XXREAL_0:2;
then reconsider t1 = t, s29 = s2 as Point of I[01] by A12, A13, A24, BORSUK_1:43;
A27: t in the carrier of I[01] by A24, A26, BORSUK_1:43;
then ((f ") * g) . t in the carrier of I[01] by FUNCT_2:5;
then reconsider Ft = ((f ") * g) . t1 as Real by BORSUK_1:40;
A28: rng g = [#] ((TOP-REAL 2) | P) by A8, TOPS_2:def_5;
A29: dom g = [#] I[01] by A8, TOPS_2:def_5;
then 1 in dom g by BORSUK_1:43;
then A30: ((f ") * g) . 1 = 1 by A10, A19, FUNCT_1:13;
A31: s1 in dom f by A6, A15, BORSUK_1:43;
dom (f ") = [#] ((TOP-REAL 2) | P) by A22, TOPS_2:def_5;
then A32: dom ((f ") * g) = dom g by A28, RELAT_1:27;
0 in dom g by A29, BORSUK_1:43;
then A33: ((f ") * g) . 0 = 0 by A9, A21, FUNCT_1:13;
A34: 0 <= Ft
proof
percases ( 0 < t or 0 = t ) by A24;
suppose 0 < t ; ::_thesis: 0 <= Ft
hence 0 <= Ft by A23, A33, A30, BORSUK_1:def_14, JORDAN5A:15, TOPMETR:20; ::_thesis: verum
end;
suppose 0 = t ; ::_thesis: 0 <= Ft
hence 0 <= Ft by A9, A21, A29, FUNCT_1:13; ::_thesis: verum
end;
end;
end;
f * ((f ") * g) = g * (f * (f ")) by RELAT_1:36
.= g * (id (rng f)) by A17, A14, TOPS_2:52
.= (id (rng g)) * g by A8, A17, TOPS_2:def_5
.= g by RELAT_1:54 ;
then A35: f . (((f ") * g) . t) = g . t by A29, A27, A32, FUNCT_1:13;
s2 in dom g by A12, A13, A29, BORSUK_1:43;
then ((f ") * g) . s2 = (f ") . q1 by A11, FUNCT_1:13
.= s1 by A2, A14, A31, A18, FUNCT_1:32 ;
then ((f ") * g) . s29 = s1 ;
then Ft < s1 by A25, A23, A33, A30, JORDAN5A:15, TOPMETR:20;
hence not g . t in Q by A7, A34, A35; ::_thesis: verum
end;
definition
let P, Q be Subset of (TOP-REAL 2);
let p1, p2 be Point of (TOP-REAL 2);
assume that
A1: ( P meets Q & P /\ Q is closed ) and
A2: P is_an_arc_of p1,p2 ;
func First_Point (P,p1,p2,Q) -> Point of (TOP-REAL 2) means :Def1: :: JORDAN5C:def 1
( it in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = it & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) );
existence
ex b1 being Point of (TOP-REAL 2) st
( b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) )
proof
consider EX being Point of (TOP-REAL 2) such that
A3: EX in P /\ Q and
A4: ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) by A1, A2, JORDAN5A:21;
EX in P by A3, XBOOLE_0:def_4;
then for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q by A4, Th1;
hence ex b1 being Point of (TOP-REAL 2) st
( b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) by A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Point of (TOP-REAL 2) st b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) & b2 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b2 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) holds
b1 = b2
proof
let IT1, IT2 be Point of (TOP-REAL 2); ::_thesis: ( IT1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) & IT2 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT2 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) implies IT1 = IT2 )
A5: P /\ Q c= Q by XBOOLE_1:17;
A6: P /\ Q c= P by XBOOLE_1:17;
assume that
A7: IT1 in P /\ Q and
A8: for g1 being Function of I[01],((TOP-REAL 2) | P)
for s1 being Real st g1 is being_homeomorphism & g1 . 0 = p1 & g1 . 1 = p2 & g1 . s1 = IT1 & 0 <= s1 & s1 <= 1 holds
for t being Real st 0 <= t & t < s1 holds
not g1 . t in Q ; ::_thesis: ( not IT2 in P /\ Q or ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT2 & 0 <= s2 & s2 <= 1 & ex t being Real st
( 0 <= t & t < s2 & g . t in Q ) ) or IT1 = IT2 )
assume that
A9: IT2 in P /\ Q and
A10: for g2 being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g2 is being_homeomorphism & g2 . 0 = p1 & g2 . 1 = p2 & g2 . s2 = IT2 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g2 . t in Q ; ::_thesis: IT1 = IT2
consider g being Function of I[01],((TOP-REAL 2) | P) such that
A11: g is being_homeomorphism and
A12: ( g . 0 = p1 & g . 1 = p2 ) by A2, TOPREAL1:def_1;
A13: rng g = [#] ((TOP-REAL 2) | P) by A11, TOPS_2:def_5
.= P by PRE_TOPC:def_5 ;
then consider ss1 being set such that
A14: ss1 in dom g and
A15: g . ss1 = IT1 by A6, A7, FUNCT_1:def_3;
A16: dom g = [#] I[01] by A11, TOPS_2:def_5
.= the carrier of I[01] ;
then reconsider ss1 = ss1 as Real by A14, BORSUK_1:40;
A17: 0 <= ss1 by A14, BORSUK_1:43;
consider ss2 being set such that
A18: ss2 in dom g and
A19: g . ss2 = IT2 by A6, A9, A13, FUNCT_1:def_3;
reconsider ss2 = ss2 as Real by A16, A18, BORSUK_1:40;
A20: 0 <= ss2 by A18, BORSUK_1:43;
A21: ss1 <= 1 by A14, BORSUK_1:43;
A22: ss2 <= 1 by A18, BORSUK_1:43;
percases ( ss1 < ss2 or ss1 = ss2 or ss1 > ss2 ) by XXREAL_0:1;
suppose ss1 < ss2 ; ::_thesis: IT1 = IT2
hence IT1 = IT2 by A5, A7, A10, A11, A12, A15, A19, A17, A22; ::_thesis: verum
end;
suppose ss1 = ss2 ; ::_thesis: IT1 = IT2
hence IT1 = IT2 by A15, A19; ::_thesis: verum
end;
suppose ss1 > ss2 ; ::_thesis: IT1 = IT2
hence IT1 = IT2 by A5, A8, A9, A11, A12, A15, A19, A21, A20; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def1 defines First_Point JORDAN5C:def_1_:_
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
for b5 being Point of (TOP-REAL 2) holds
( b5 = First_Point (P,p1,p2,Q) iff ( b5 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b5 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q ) ) );
theorem :: JORDAN5C:2
for P, Q being Subset of (TOP-REAL 2)
for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds
First_Point (P,p1,p2,Q) = p
proof
let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds
First_Point (P,p1,p2,Q) = p
let p, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p in P & P is_an_arc_of p1,p2 & Q = {p} implies First_Point (P,p1,p2,Q) = p )
assume that
A1: p in P and
A2: P is_an_arc_of p1,p2 and
A3: Q = {p} ; ::_thesis: First_Point (P,p1,p2,Q) = p
A4: P /\ {p} = {p} by A1, ZFMISC_1:46;
A5: for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in {p}
proof
let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in {p}
let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds
not g . t in {p} )
assume that
A6: g is being_homeomorphism and
g . 0 = p1 and
g . 1 = p2 and
A7: g . s2 = p and
A8: 0 <= s2 and
A9: s2 <= 1 ; ::_thesis: for t being Real st 0 <= t & t < s2 holds
not g . t in {p}
A10: g is one-to-one by A6, TOPS_2:def_5;
let t be Real; ::_thesis: ( 0 <= t & t < s2 implies not g . t in {p} )
assume that
A11: 0 <= t and
A12: t < s2 ; ::_thesis: not g . t in {p}
A13: dom g = the carrier of I[01] by A1, FUNCT_2:def_1;
t <= 1 by A9, A12, XXREAL_0:2;
then A14: t in dom g by A13, A11, BORSUK_1:43;
s2 in dom g by A8, A9, A13, BORSUK_1:43;
then g . t <> g . s2 by A10, A12, A14, FUNCT_1:def_4;
hence not g . t in {p} by A7, TARSKI:def_1; ::_thesis: verum
end;
A15: P /\ Q is closed by A3, A4, PCOMPS_1:7;
A16: p in P /\ {p} by A4, TARSKI:def_1;
then P meets {p} by A1, A4, XBOOLE_0:3;
hence First_Point (P,p1,p2,Q) = p by A2, A3, A16, A15, A5, Def1; ::_thesis: verum
end;
theorem Th3: :: JORDAN5C:3
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st p1 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
First_Point (P,p1,p2,Q) = p1
proof
let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
First_Point (P,p1,p2,Q) = p1
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 implies First_Point (P,p1,p2,Q) = p1 )
assume that
A1: p1 in Q and
A2: P /\ Q is closed and
A3: P is_an_arc_of p1,p2 ; ::_thesis: First_Point (P,p1,p2,Q) = p1
A4: for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
proof
let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p1 & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds
not g . t in Q )
assume that
A5: g is being_homeomorphism and
A6: g . 0 = p1 and
g . 1 = p2 and
A7: g . s2 = p1 and
A8: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: for t being Real st 0 <= t & t < s2 holds
not g . t in Q
A9: g is one-to-one by A5, TOPS_2:def_5;
let t be Real; ::_thesis: ( 0 <= t & t < s2 implies not g . t in Q )
assume A10: ( 0 <= t & t < s2 ) ; ::_thesis: not g . t in Q
A11: dom g = [#] I[01] by A5, TOPS_2:def_5
.= the carrier of I[01] ;
then A12: 0 in dom g by BORSUK_1:43;
s2 in dom g by A8, A11, BORSUK_1:43;
hence not g . t in Q by A6, A7, A12, A9, A10, FUNCT_1:def_4; ::_thesis: verum
end;
p1 in P by A3, TOPREAL1:1;
then ( p1 in P /\ Q & P meets Q ) by A1, XBOOLE_0:3, XBOOLE_0:def_4;
hence First_Point (P,p1,p2,Q) = p1 by A2, A3, A4, Def1; ::_thesis: verum
end;
theorem Th4: :: JORDAN5C:4
for P, Q being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2)
for f being Function of I[01],((TOP-REAL 2) | P)
for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds
not f . t in Q ) holds
for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q
proof
let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL 2)
for f being Function of I[01],((TOP-REAL 2) | P)
for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds
not f . t in Q ) holds
for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q
let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: for f being Function of I[01],((TOP-REAL 2) | P)
for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds
not f . t in Q ) holds
for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q
let f be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1 being Real st q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds
not f . t in Q ) holds
for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q
let s1 be Real; ::_thesis: ( q1 in P & f . s1 = q1 & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & 0 <= s1 & s1 <= 1 & ( for t being Real st 1 >= t & t > s1 holds
not f . t in Q ) implies for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q )
assume that
A1: q1 in P and
A2: f . s1 = q1 and
A3: f is being_homeomorphism and
A4: f . 0 = p1 and
A5: f . 1 = p2 and
A6: ( 0 <= s1 & s1 <= 1 ) and
A7: for t being Real st 1 >= t & t > s1 holds
not f . t in Q ; ::_thesis: for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q
reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1;
let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q
let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = q1 & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds
not g . t in Q )
assume that
A8: g is being_homeomorphism and
A9: g . 0 = p1 and
A10: g . 1 = p2 and
A11: g . s2 = q1 and
A12: 0 <= s2 and
A13: s2 <= 1 ; ::_thesis: for t being Real st 1 >= t & t > s2 holds
not g . t in Q
reconsider f = f, g = g as Function of I[01],((TOP-REAL 2) | P9) ;
A14: f is one-to-one by A3, TOPS_2:def_5;
set fg = (f ") * g;
let t be Real; ::_thesis: ( 1 >= t & t > s2 implies not g . t in Q )
assume that
A15: 1 >= t and
A16: t > s2 ; ::_thesis: not g . t in Q
reconsider t1 = t, s29 = s2 as Point of I[01] by A12, A13, A15, A16, BORSUK_1:43;
A17: t in the carrier of I[01] by A12, A15, A16, BORSUK_1:43;
then ((f ") * g) . t in the carrier of I[01] by FUNCT_2:5;
then reconsider Ft = ((f ") * g) . t1 as Real by BORSUK_1:40;
A18: rng g = [#] ((TOP-REAL 2) | P) by A8, TOPS_2:def_5;
A19: f " is being_homeomorphism by A3, TOPS_2:56;
then (f ") * g is being_homeomorphism by A8, TOPS_2:57;
then A20: ( (f ") * g is continuous & (f ") * g is one-to-one ) by TOPS_2:def_5;
A21: dom f = [#] I[01] by A3, TOPS_2:def_5;
then A22: 0 in dom f by BORSUK_1:43;
A23: rng f = [#] ((TOP-REAL 2) | P) by A3, TOPS_2:def_5;
then f is onto by FUNCT_2:def_3;
then A24: f " = f " by A14, TOPS_2:def_4;
then A25: (f ") . p1 = 0 by A4, A22, A14, FUNCT_1:32;
A26: 1 in dom f by A21, BORSUK_1:43;
A27: (f ") . p2 = 1 by A24, A5, A26, A14, FUNCT_1:32;
A28: dom g = [#] I[01] by A8, TOPS_2:def_5;
then 0 in dom g by BORSUK_1:43;
then A29: ((f ") * g) . 0 = 0 by A9, A25, FUNCT_1:13;
1 in dom g by A28, BORSUK_1:43;
then A30: ((f ") * g) . 1 = 1 by A10, A27, FUNCT_1:13;
A31: Ft <= 1
proof
percases ( t < 1 or t = 1 ) by A15, XXREAL_0:1;
suppose t < 1 ; ::_thesis: Ft <= 1
hence Ft <= 1 by A20, A29, A30, BORSUK_1:def_15, JORDAN5A:15, TOPMETR:20; ::_thesis: verum
end;
suppose t = 1 ; ::_thesis: Ft <= 1
hence Ft <= 1 by A10, A27, A28, FUNCT_1:13; ::_thesis: verum
end;
end;
end;
dom (f ") = [#] ((TOP-REAL 2) | P) by A19, TOPS_2:def_5;
then A32: t in dom ((f ") * g) by A28, A18, A17, RELAT_1:27;
f * ((f ") * g) = g * (f * (f ")) by RELAT_1:36
.= g * (id (rng f)) by A23, A14, TOPS_2:52
.= (id (rng g)) * g by A8, A23, TOPS_2:def_5
.= g by RELAT_1:54 ;
then A33: f . (((f ") * g) . t) = g . t by A32, FUNCT_1:13;
A34: s1 in dom f by A6, A21, BORSUK_1:43;
s2 in dom g by A12, A13, A28, BORSUK_1:43;
then ((f ") * g) . s2 = (f ") . q1 by A11, FUNCT_1:13
.= s1 by A2, A14, A34, A24, FUNCT_1:32 ;
then ((f ") * g) . s29 = s1 ;
then s1 < Ft by A16, A20, A29, A30, JORDAN5A:15, TOPMETR:20;
hence not g . t in Q by A7, A31, A33; ::_thesis: verum
end;
definition
let P, Q be Subset of (TOP-REAL 2);
let p1, p2 be Point of (TOP-REAL 2);
assume that
A1: ( P meets Q & P /\ Q is closed ) and
A2: P is_an_arc_of p1,p2 ;
func Last_Point (P,p1,p2,Q) -> Point of (TOP-REAL 2) means :Def2: :: JORDAN5C:def 2
( it in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = it & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) );
existence
ex b1 being Point of (TOP-REAL 2) st
( b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) )
proof
consider EX being Point of (TOP-REAL 2) such that
A3: EX in P /\ Q and
A4: ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 & ( for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) ) by A1, A2, JORDAN5A:22;
EX in P by A3, XBOOLE_0:def_4;
then for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = EX & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q by A4, Th4;
hence ex b1 being Point of (TOP-REAL 2) st
( b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) ) by A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Point of (TOP-REAL 2) st b1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) & b2 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b2 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) holds
b1 = b2
proof
let IT1, IT2 be Point of (TOP-REAL 2); ::_thesis: ( IT1 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT1 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) & IT2 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT2 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) implies IT1 = IT2 )
A5: P /\ Q c= P by XBOOLE_1:17;
assume that
A6: IT1 in P /\ Q and
A7: for g1 being Function of I[01],((TOP-REAL 2) | P)
for s1 being Real st g1 is being_homeomorphism & g1 . 0 = p1 & g1 . 1 = p2 & g1 . s1 = IT1 & 0 <= s1 & s1 <= 1 holds
for t being Real st 1 >= t & t > s1 holds
not g1 . t in Q ; ::_thesis: ( not IT2 in P /\ Q or ex g being Function of I[01],((TOP-REAL 2) | P) ex s2 being Real st
( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = IT2 & 0 <= s2 & s2 <= 1 & ex t being Real st
( 1 >= t & t > s2 & g . t in Q ) ) or IT1 = IT2 )
assume that
A8: IT2 in P /\ Q and
A9: for g2 being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g2 is being_homeomorphism & g2 . 0 = p1 & g2 . 1 = p2 & g2 . s2 = IT2 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g2 . t in Q ; ::_thesis: IT1 = IT2
consider g being Function of I[01],((TOP-REAL 2) | P) such that
A10: g is being_homeomorphism and
A11: ( g . 0 = p1 & g . 1 = p2 ) by A2, TOPREAL1:def_1;
A12: rng g = [#] ((TOP-REAL 2) | P) by A10, TOPS_2:def_5
.= P by PRE_TOPC:def_5 ;
then consider ss1 being set such that
A13: ss1 in dom g and
A14: g . ss1 = IT1 by A5, A6, FUNCT_1:def_3;
A15: dom g = [#] I[01] by A10, TOPS_2:def_5
.= the carrier of I[01] ;
then reconsider ss1 = ss1 as Real by A13, BORSUK_1:40;
A16: 0 <= ss1 by A13, BORSUK_1:43;
A17: ( P /\ Q c= Q & ss1 <= 1 ) by A13, BORSUK_1:43, XBOOLE_1:17;
consider ss2 being set such that
A18: ss2 in dom g and
A19: g . ss2 = IT2 by A5, A8, A12, FUNCT_1:def_3;
reconsider ss2 = ss2 as Real by A15, A18, BORSUK_1:40;
A20: 0 <= ss2 by A18, BORSUK_1:43;
A21: ss2 <= 1 by A18, BORSUK_1:43;
percases ( ss1 < ss2 or ss1 = ss2 or ss1 > ss2 ) by XXREAL_0:1;
suppose ss1 < ss2 ; ::_thesis: IT1 = IT2
hence IT1 = IT2 by A7, A8, A10, A11, A14, A19, A16, A17, A21; ::_thesis: verum
end;
suppose ss1 = ss2 ; ::_thesis: IT1 = IT2
hence IT1 = IT2 by A14, A19; ::_thesis: verum
end;
suppose ss1 > ss2 ; ::_thesis: IT1 = IT2
hence IT1 = IT2 by A6, A9, A10, A11, A14, A19, A17, A20, A21; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def2 defines Last_Point JORDAN5C:def_2_:_
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P meets Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
for b5 being Point of (TOP-REAL 2) holds
( b5 = Last_Point (P,p1,p2,Q) iff ( b5 in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = b5 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q ) ) );
theorem :: JORDAN5C:5
for P, Q being Subset of (TOP-REAL 2)
for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds
Last_Point (P,p1,p2,Q) = p
proof
let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p, p1, p2 being Point of (TOP-REAL 2) st p in P & P is_an_arc_of p1,p2 & Q = {p} holds
Last_Point (P,p1,p2,Q) = p
let p, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p in P & P is_an_arc_of p1,p2 & Q = {p} implies Last_Point (P,p1,p2,Q) = p )
assume that
A1: p in P and
A2: P is_an_arc_of p1,p2 and
A3: Q = {p} ; ::_thesis: Last_Point (P,p1,p2,Q) = p
A4: P /\ {p} = {p} by A1, ZFMISC_1:46;
A5: for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in {p}
proof
let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in {p}
let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds
not g . t in {p} )
assume that
A6: g is being_homeomorphism and
g . 0 = p1 and
g . 1 = p2 and
A7: g . s2 = p and
A8: 0 <= s2 and
A9: s2 <= 1 ; ::_thesis: for t being Real st 1 >= t & t > s2 holds
not g . t in {p}
A10: g is one-to-one by A6, TOPS_2:def_5;
A11: dom g = the carrier of I[01] by A1, FUNCT_2:def_1;
then A12: s2 in dom g by A8, A9, BORSUK_1:43;
let t be Real; ::_thesis: ( 1 >= t & t > s2 implies not g . t in {p} )
assume that
A13: 1 >= t and
A14: t > s2 ; ::_thesis: not g . t in {p}
t in dom g by A8, A11, A13, A14, BORSUK_1:43;
then g . t <> g . s2 by A10, A14, A12, FUNCT_1:def_4;
hence not g . t in {p} by A7, TARSKI:def_1; ::_thesis: verum
end;
A15: P /\ Q is closed by A3, A4, PCOMPS_1:7;
A16: p in P /\ {p} by A4, TARSKI:def_1;
then P meets {p} by A1, A4, XBOOLE_0:3;
hence Last_Point (P,p1,p2,Q) = p by A2, A3, A16, A15, A5, Def2; ::_thesis: verum
end;
theorem Th6: :: JORDAN5C:6
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st p2 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
Last_Point (P,p1,p2,Q) = p2
proof
let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st p2 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 holds
Last_Point (P,p1,p2,Q) = p2
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p2 in Q & P /\ Q is closed & P is_an_arc_of p1,p2 implies Last_Point (P,p1,p2,Q) = p2 )
assume that
A1: p2 in Q and
A2: P /\ Q is closed and
A3: P is_an_arc_of p1,p2 ; ::_thesis: Last_Point (P,p1,p2,Q) = p2
A4: for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q
proof
let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q
let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds
not g . t in Q )
assume that
A5: g is being_homeomorphism and
g . 0 = p1 and
A6: ( g . 1 = p2 & g . s2 = p2 ) and
A7: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: for t being Real st 1 >= t & t > s2 holds
not g . t in Q
A8: g is one-to-one by A5, TOPS_2:def_5;
let t be Real; ::_thesis: ( 1 >= t & t > s2 implies not g . t in Q )
assume A9: ( 1 >= t & t > s2 ) ; ::_thesis: not g . t in Q
A10: dom g = [#] I[01] by A5, TOPS_2:def_5
.= the carrier of I[01] ;
then A11: 1 in dom g by BORSUK_1:43;
s2 in dom g by A7, A10, BORSUK_1:43;
hence not g . t in Q by A6, A11, A8, A9, FUNCT_1:def_4; ::_thesis: verum
end;
p2 in P by A3, TOPREAL1:1;
then ( p2 in P /\ Q & P meets Q ) by A1, XBOOLE_0:3, XBOOLE_0:def_4;
hence Last_Point (P,p1,p2,Q) = p2 by A2, A3, A4, Def2; ::_thesis: verum
end;
theorem Th7: :: JORDAN5C:7
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P c= Q & P is closed & P is_an_arc_of p1,p2 holds
( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 )
proof
let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P c= Q & P is closed & P is_an_arc_of p1,p2 holds
( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P c= Q & P is closed & P is_an_arc_of p1,p2 implies ( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 ) )
assume that
A1: P c= Q and
A2: P is closed and
A3: P is_an_arc_of p1,p2 ; ::_thesis: ( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 )
A4: p2 in P by A3, TOPREAL1:1;
( P /\ Q = P & p1 in P ) by A1, A3, TOPREAL1:1, XBOOLE_1:28;
hence ( First_Point (P,p1,p2,Q) = p1 & Last_Point (P,p1,p2,Q) = p2 ) by A1, A2, A3, A4, Th3, Th6; ::_thesis: verum
end;
begin
definition
let P be Subset of (TOP-REAL 2);
let p1, p2, q1, q2 be Point of (TOP-REAL 2);
pred LE q1,q2,P,p1,p2 means :Def3: :: JORDAN5C:def 3
( q1 in P & q2 in P & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) );
end;
:: deftheorem Def3 defines LE JORDAN5C:def_3_:_
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds
( LE q1,q2,P,p1,p2 iff ( q1 in P & q2 in P & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) ) );
theorem Th8: :: JORDAN5C:8
for P being 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) | P)
for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & 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
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2)
for g being Function of I[01],((TOP-REAL 2) | P)
for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & 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
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: for g being Function of I[01],((TOP-REAL 2) | P)
for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & 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
let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st P is_an_arc_of p1,p2 & g is being_homeomorphism & 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
let s1, s2 be Real; ::_thesis: ( P is_an_arc_of p1,p2 & g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2 implies LE q1,q2,P,p1,p2 )
assume that
A1: P is_an_arc_of p1,p2 and
A2: g is being_homeomorphism and
A3: g . 0 = p1 and
A4: g . 1 = p2 and
A5: g . s1 = q1 and
A6: ( 0 <= s1 & s1 <= 1 ) and
A7: g . s2 = q2 and
A8: ( 0 <= s2 & s2 <= 1 ) and
A9: s1 <= s2 ; ::_thesis: LE q1,q2,P,p1,p2
reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;
A10: s1 in the carrier of I[01] by A6, BORSUK_1:43;
then A11: q1 in [#] ((TOP-REAL 2) | P9) by A5, FUNCT_2:5;
reconsider g = g as Function of I[01],((TOP-REAL 2) | P9) ;
A12: s2 in the carrier of I[01] by A8, BORSUK_1:43;
then g . s2 in the carrier of ((TOP-REAL 2) | P9) by FUNCT_2:5;
then A13: q2 in P by A7, A11, PRE_TOPC:def_5;
A14: now__::_thesis:_for_h_being_Function_of_I[01],((TOP-REAL_2)_|_P9)
for_t1,_t2_being_Real_st_h_is_being_homeomorphism_&_h_._0_=_p1_&_h_._1_=_p2_&_h_._t1_=_q1_&_0_<=_t1_&_t1_<=_1_&_h_._t2_=_q2_&_0_<=_t2_&_t2_<=_1_holds_
t1_<=_t2
reconsider s19 = s1, s29 = s2 as Point of I[01] by A6, A8, BORSUK_1:43;
let h be Function of I[01],((TOP-REAL 2) | P9); ::_thesis: for t1, t2 being Real st h is being_homeomorphism & h . 0 = p1 & h . 1 = p2 & h . t1 = q1 & 0 <= t1 & t1 <= 1 & h . t2 = q2 & 0 <= t2 & t2 <= 1 holds
b4 <= b5
let t1, t2 be Real; ::_thesis: ( h is being_homeomorphism & h . 0 = p1 & h . 1 = p2 & h . t1 = q1 & 0 <= t1 & t1 <= 1 & h . t2 = q2 & 0 <= t2 & t2 <= 1 implies b2 <= b3 )
assume that
A15: h is being_homeomorphism and
A16: h . 0 = p1 and
A17: h . 1 = p2 and
A18: h . t1 = q1 and
A19: ( 0 <= t1 & t1 <= 1 ) and
A20: h . t2 = q2 and
A21: ( 0 <= t2 & t2 <= 1 ) ; ::_thesis: b2 <= b3
A22: h is one-to-one by A15, TOPS_2:def_5;
set hg = (h ") * g;
h " is being_homeomorphism by A15, TOPS_2:56;
then (h ") * g is being_homeomorphism by A2, TOPS_2:57;
then A23: ( (h ") * g is continuous & (h ") * g is one-to-one ) by TOPS_2:def_5;
( ((h ") * g) . s1 in the carrier of I[01] & ((h ") * g) . s2 in the carrier of I[01] ) by A10, A12, FUNCT_2:5;
then reconsider hg1 = ((h ") * g) . s19, hg2 = ((h ") * g) . s29 as Real by BORSUK_1:40;
A24: dom g = [#] I[01] by A2, TOPS_2:def_5;
then A25: 0 in dom g by BORSUK_1:43;
A26: dom h = [#] I[01] by A15, TOPS_2:def_5;
then A27: t1 in dom h by A19, BORSUK_1:43;
A28: 0 in dom h by A26, BORSUK_1:43;
rng h = [#] ((TOP-REAL 2) | P) by A15, TOPS_2:def_5;
then h is onto by FUNCT_2:def_3;
then A29: h " = h " by A22, TOPS_2:def_4;
then (h ") . p1 = 0 by A16, A28, A22, FUNCT_1:32;
then A30: ((h ") * g) . 0 = 0 by A3, A25, FUNCT_1:13;
s1 in dom g by A6, A24, BORSUK_1:43;
then A31: ((h ") * g) . s1 = (h ") . q1 by A5, FUNCT_1:13
.= t1 by A18, A22, A27, A29, FUNCT_1:32 ;
A32: t2 in dom h by A21, A26, BORSUK_1:43;
s2 in dom g by A8, A24, BORSUK_1:43;
then A33: ((h ") * g) . s2 = (h ") . q2 by A7, FUNCT_1:13
.= t2 by A20, A22, A32, A29, FUNCT_1:32 ;
A34: 1 in dom g by A24, BORSUK_1:43;
A35: 1 in dom h by A26, BORSUK_1:43;
(h ") . p2 = 1 by A17, A35, A22, A29, FUNCT_1:32;
then A36: ((h ") * g) . 1 = 1 by A4, A34, FUNCT_1:13;
percases ( s1 < s2 or s1 = s2 ) by A9, XXREAL_0:1;
suppose s1 < s2 ; ::_thesis: b2 <= b3
then hg1 < hg2 by A23, A30, A36, JORDAN5A:16;
hence t1 <= t2 by A31, A33; ::_thesis: verum
end;
suppose s1 = s2 ; ::_thesis: b2 <= b3
hence t1 <= t2 by A31, A33; ::_thesis: verum
end;
end;
end;
q1 in P by A11, PRE_TOPC:def_5;
hence LE q1,q2,P,p1,p2 by A13, A14, Def3; ::_thesis: verum
end;
theorem Th9: :: JORDAN5C:9
for P being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) st q1 in P holds
LE q1,q1,P,p1,p2
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL 2) st q1 in P holds
LE q1,q1,P,p1,p2
let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: ( q1 in P implies LE q1,q1,P,p1,p2 )
assume A1: q1 in P ; ::_thesis: LE q1,q1,P,p1,p2
then reconsider P = P as non empty Subset of (TOP-REAL 2) ;
now__::_thesis:_for_g_being_Function_of_I[01],((TOP-REAL_2)_|_P)
for_s1,_s2_being_Real_st_g_is_being_homeomorphism_&_g_._0_=_p1_&_g_._1_=_p2_&_g_._s1_=_q1_&_0_<=_s1_&_s1_<=_1_&_g_._s2_=_q1_&_0_<=_s2_&_s2_<=_1_holds_
s1_<=_s2
let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
s1 <= s2
let s1, s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q1 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume that
A2: g is being_homeomorphism and
g . 0 = p1 and
g . 1 = p2 and
A3: g . s1 = q1 and
A4: ( 0 <= s1 & s1 <= 1 ) and
A5: g . s2 = q1 and
A6: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: s1 <= s2
A7: g is one-to-one by A2, TOPS_2:def_5;
( s1 in the carrier of I[01] & s2 in the carrier of I[01] ) by A4, A6, BORSUK_1:43;
hence s1 <= s2 by A3, A5, A7, FUNCT_2:19; ::_thesis: verum
end;
hence LE q1,q1,P,p1,p2 by A1, Def3; ::_thesis: verum
end;
theorem Th10: :: JORDAN5C:10
for P being Subset of (TOP-REAL 2)
for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P holds
( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P holds
( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 )
let p1, p2, q1 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & q1 in P implies ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 ) )
assume that
A1: P is_an_arc_of p1,p2 and
A2: q1 in P ; ::_thesis: ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 )
reconsider P = P as non empty Subset of (TOP-REAL 2) by A2;
A3: now__::_thesis:_for_g_being_Function_of_I[01],((TOP-REAL_2)_|_P)
for_s1,_s2_being_Real_st_g_is_being_homeomorphism_&_g_._0_=_p1_&_g_._1_=_p2_&_g_._s1_=_p1_&_0_<=_s1_&_s1_<=_1_&_g_._s2_=_q1_&_0_<=_s2_&_s2_<=_1_holds_
s1_<=_s2
A4: 0 in the carrier of I[01] by BORSUK_1:43;
let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = q1 & 0 <= s2 & s2 <= 1 holds
s1 <= s2
let s1, s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = q1 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume that
A5: g is being_homeomorphism and
A6: g . 0 = p1 and
g . 1 = p2 and
A7: g . s1 = p1 and
A8: ( 0 <= s1 & s1 <= 1 ) and
g . s2 = q1 and
A9: 0 <= s2 and
s2 <= 1 ; ::_thesis: s1 <= s2
( s1 in the carrier of I[01] & g is one-to-one ) by A5, A8, BORSUK_1:43, TOPS_2:def_5;
hence s1 <= s2 by A6, A7, A9, A4, FUNCT_2:19; ::_thesis: verum
end;
A10: now__::_thesis:_for_g_being_Function_of_I[01],((TOP-REAL_2)_|_P)
for_s1,_s2_being_Real_st_g_is_being_homeomorphism_&_g_._0_=_p1_&_g_._1_=_p2_&_g_._s1_=_q1_&_0_<=_s1_&_s1_<=_1_&_g_._s2_=_p2_&_0_<=_s2_&_s2_<=_1_holds_
s1_<=_s2
A11: 1 in the carrier of I[01] by BORSUK_1:43;
let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2
let s1, s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume that
A12: g is being_homeomorphism and
g . 0 = p1 and
A13: g . 1 = p2 and
g . s1 = q1 and
0 <= s1 and
A14: ( s1 <= 1 & g . s2 = p2 ) and
A15: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: s1 <= s2
( s2 in the carrier of I[01] & g is one-to-one ) by A12, A15, BORSUK_1:43, TOPS_2:def_5;
hence s1 <= s2 by A13, A14, A11, FUNCT_2:19; ::_thesis: verum
end;
( p1 in P & p2 in P ) by A1, TOPREAL1:1;
hence ( LE p1,q1,P,p1,p2 & LE q1,p2,P,p1,p2 ) by A2, A3, A10, Def3; ::_thesis: verum
end;
theorem :: JORDAN5C:11
for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
LE p1,p2,P,p1,p2
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds
LE p1,p2,P,p1,p2
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 implies LE p1,p2,P,p1,p2 )
assume A1: P is_an_arc_of p1,p2 ; ::_thesis: LE p1,p2,P,p1,p2
then p2 in P by TOPREAL1:1;
hence LE p1,p2,P,p1,p2 by A1, Th10; ::_thesis: verum
end;
theorem Th12: :: JORDAN5C:12
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 holds
q1 = q2
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 holds
q1 = q2
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 implies q1 = q2 )
assume that
A1: P is_an_arc_of p1,p2 and
A2: LE q1,q2,P,p1,p2 and
A3: LE q2,q1,P,p1,p2 ; ::_thesis: q1 = q2
consider f being Function of I[01],((TOP-REAL 2) | P) such that
A4: f is being_homeomorphism and
A5: ( f . 0 = p1 & f . 1 = p2 ) by A1, TOPREAL1:def_1;
A6: dom f = [#] I[01] by A4, TOPS_2:def_5
.= the carrier of I[01] ;
A7: rng f = [#] ((TOP-REAL 2) | P) by A4, TOPS_2:def_5
.= P by PRE_TOPC:def_5 ;
then q2 in rng f by A2, Def3;
then consider x being set such that
A8: x in dom f and
A9: q2 = f . x by FUNCT_1:def_3;
q1 in rng f by A2, A7, Def3;
then consider y being set such that
A10: y in dom f and
A11: q1 = f . y by FUNCT_1:def_3;
[.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def_1;
then consider s3 being Real such that
A12: s3 = x and
A13: ( 0 <= s3 & s3 <= 1 ) by A6, A8, BORSUK_1:40;
[.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def_1;
then consider s4 being Real such that
A14: s4 = y and
A15: ( 0 <= s4 & s4 <= 1 ) by A6, A10, BORSUK_1:40;
( s3 <= s4 & s4 <= s3 ) by A2, A3, A4, A5, A9, A12, A13, A11, A14, A15, Def3;
hence q1 = q2 by A9, A12, A11, A14, XXREAL_0:1; ::_thesis: verum
end;
theorem Th13: :: JORDAN5C:13
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2, q3 being Point of (TOP-REAL 2) st LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 holds
LE q1,q3,P,p1,p2
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2, q3 being Point of (TOP-REAL 2) st LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 holds
LE q1,q3,P,p1,p2
let p1, p2, q1, q2, q3 be Point of (TOP-REAL 2); ::_thesis: ( LE q1,q2,P,p1,p2 & LE q2,q3,P,p1,p2 implies LE q1,q3,P,p1,p2 )
assume that
A1: LE q1,q2,P,p1,p2 and
A2: LE q2,q3,P,p1,p2 ; ::_thesis: LE q1,q3,P,p1,p2
A3: q2 in P by A1, Def3;
A4: now__::_thesis:_for_g_being_Function_of_I[01],((TOP-REAL_2)_|_P)
for_s1,_s2_being_Real_st_g_is_being_homeomorphism_&_g_._0_=_p1_&_g_._1_=_p2_&_g_._s1_=_q1_&_0_<=_s1_&_s1_<=_1_&_g_._s2_=_q3_&_0_<=_s2_&_s2_<=_1_holds_
s1_<=_s2
A5: [.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def_1;
let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q3 & 0 <= s2 & s2 <= 1 holds
s1 <= s2
let s1, s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q3 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume that
A6: g is being_homeomorphism and
A7: ( g . 0 = p1 & g . 1 = p2 & g . s1 = q1 ) and
0 <= s1 and
A8: ( s1 <= 1 & g . s2 = q3 & 0 <= s2 & s2 <= 1 ) ; ::_thesis: s1 <= s2
rng g = [#] ((TOP-REAL 2) | P) by A6, TOPS_2:def_5
.= P by PRE_TOPC:def_5 ;
then consider x being set such that
A9: x in dom g and
A10: q2 = g . x by A3, FUNCT_1:def_3;
dom g = [#] I[01] by A6, TOPS_2:def_5
.= the carrier of I[01] ;
then consider s3 being Real such that
A11: ( s3 = x & 0 <= s3 & s3 <= 1 ) by A9, A5, BORSUK_1:40;
( s1 <= s3 & s3 <= s2 ) by A1, A2, A6, A7, A8, A10, A11, Def3;
hence s1 <= s2 by XXREAL_0:2; ::_thesis: verum
end;
( q1 in P & q3 in P ) by A1, A2, Def3;
hence LE q1,q3,P,p1,p2 by A4, Def3; ::_thesis: verum
end;
theorem :: JORDAN5C:14
for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> q2 & not ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) holds
( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 )
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> q2 & not ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) holds
( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 )
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> q2 & not ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) implies ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) )
assume that
A1: P is_an_arc_of p1,p2 and
A2: q1 in P and
A3: q2 in P and
A4: q1 <> q2 ; ::_thesis: ( ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) or ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) )
reconsider P = P as non empty Subset of (TOP-REAL 2) by A2;
( ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) or ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) )
proof
consider f being Function of I[01],((TOP-REAL 2) | P) such that
A5: f is being_homeomorphism and
A6: ( f . 0 = p1 & f . 1 = p2 ) by A1, TOPREAL1:def_1;
A7: rng f = [#] ((TOP-REAL 2) | P) by A5, TOPS_2:def_5
.= P by PRE_TOPC:def_5 ;
then consider x being set such that
A8: x in dom f and
A9: q1 = f . x by A2, FUNCT_1:def_3;
consider y being set such that
A10: y in dom f and
A11: q2 = f . y by A3, A7, FUNCT_1:def_3;
dom f = [#] I[01] by A5, TOPS_2:def_5
.= [.0,1.] by BORSUK_1:40 ;
then reconsider s1 = x, s2 = y as Real by A8, A10;
A12: 0 <= s1 by A8, BORSUK_1:43;
A13: s2 <= 1 by A10, BORSUK_1:43;
A14: 0 <= s2 by A10, BORSUK_1:43;
A15: s1 <= 1 by A8, BORSUK_1:43;
assume A16: ( LE q1,q2,P,p1,p2 iff LE q2,q1,P,p1,p2 ) ; ::_thesis: contradiction
percases ( s1 < s2 or s1 = s2 or s1 > s2 ) by XXREAL_0:1;
suppose s1 < s2 ; ::_thesis: contradiction
hence contradiction by A1, A4, A16, A5, A6, A9, A11, A12, A15, A13, Th8, Th12; ::_thesis: verum
end;
suppose s1 = s2 ; ::_thesis: contradiction
hence contradiction by A4, A9, A11; ::_thesis: verum
end;
suppose s1 > s2 ; ::_thesis: contradiction
hence contradiction by A1, A4, A16, A5, A6, A9, A11, A15, A14, A13, Th8, Th12; ::_thesis: verum
end;
end;
end;
hence ( ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) or ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) ) ; ::_thesis: verum
end;
begin
theorem Th15: :: JORDAN5C:15
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds
LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds
LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f)
let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds
LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f)
let q be Point of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) )
assume that
A1: f is being_S-Seq and
A2: (L~ f) /\ Q is closed and
A3: q in L~ f and
A4: q in Q ; ::_thesis: LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f)
set P = L~ f;
A5: (L~ f) /\ Q c= L~ f by XBOOLE_1:17;
set q1 = First_Point ((L~ f),(f /. 1),(f /. (len f)),Q);
( L~ f meets Q & L~ f is_an_arc_of f /. 1,f /. (len f) ) by A1, A3, A4, TOPREAL1:25, XBOOLE_0:3;
then ( First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | (L~ f))
for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) & 0 <= s1 & s1 <= 1 & g . s2 = q & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) ) by A2, A4, Def1;
hence LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q, L~ f,f /. 1,f /. (len f) by A3, A5, Def3; ::_thesis: verum
end;
theorem Th16: :: JORDAN5C:16
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds
LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds
LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f)
let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) st f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q holds
LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f)
let q be Point of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq & (L~ f) /\ Q is closed & q in L~ f & q in Q implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) )
set P = L~ f;
assume that
A1: f is being_S-Seq and
A2: (L~ f) /\ Q is closed and
A3: q in L~ f and
A4: q in Q ; ::_thesis: LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f)
set q1 = Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q);
A5: (L~ f) /\ Q c= L~ f by XBOOLE_1:17;
( L~ f meets Q & L~ f is_an_arc_of f /. 1,f /. (len f) ) by A1, A3, A4, TOPREAL1:25, XBOOLE_0:3;
then ( Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | (L~ f))
for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q & 0 <= s1 & s1 <= 1 & g . s2 = Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) ) by A2, A4, Def2;
hence LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q), L~ f,f /. 1,f /. (len f) by A3, A5, Def3; ::_thesis: verum
end;
theorem Th17: :: JORDAN5C:17
for q1, q2, p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & LE q1,q2, LSeg (p1,p2),p1,p2 holds
LE q1,q2,p1,p2
proof
let q1, q2, p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 <> p2 & LE q1,q2, LSeg (p1,p2),p1,p2 implies LE q1,q2,p1,p2 )
set P = LSeg (p1,p2);
assume p1 <> p2 ; ::_thesis: ( not LE q1,q2, LSeg (p1,p2),p1,p2 or LE q1,q2,p1,p2 )
then consider f being Function of I[01],((TOP-REAL 2) | (LSeg (p1,p2))) such that
A1: for x being Real st x in [.0,1.] holds
f . x = ((1 - x) * p1) + (x * p2) and
A2: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by JORDAN5A:3;
assume A3: LE q1,q2, LSeg (p1,p2),p1,p2 ; ::_thesis: LE q1,q2,p1,p2
hence ( q1 in LSeg (p1,p2) & q2 in LSeg (p1,p2) ) by Def3; :: according to JORDAN3:def_5 ::_thesis: for b1, b2 being Element of REAL holds
( not 0 <= b1 or not b1 <= 1 or not q1 = ((1 - b1) * p1) + (b1 * p2) or not 0 <= b2 or not b2 <= 1 or not q2 = ((1 - b2) * p1) + (b2 * p2) or b1 <= b2 )
let r1, r2 be Real; ::_thesis: ( not 0 <= r1 or not r1 <= 1 or not q1 = ((1 - r1) * p1) + (r1 * p2) or not 0 <= r2 or not r2 <= 1 or not q2 = ((1 - r2) * p1) + (r2 * p2) or r1 <= r2 )
assume that
A4: 0 <= r1 and
A5: r1 <= 1 and
A6: q1 = ((1 - r1) * p1) + (r1 * p2) and
A7: ( 0 <= r2 & r2 <= 1 ) and
A8: q2 = ((1 - r2) * p1) + (r2 * p2) ; ::_thesis: r1 <= r2
r2 in [.0,1.] by A7, BORSUK_1:40, BORSUK_1:43;
then A9: q2 = f . r2 by A8, A1;
r1 in [.0,1.] by A4, A5, BORSUK_1:40, BORSUK_1:43;
then q1 = f . r1 by A6, A1;
hence r1 <= r2 by A3, A5, A7, A2, A9, Def3; ::_thesis: verum
end;
theorem :: JORDAN5C:18
for P, Q being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P meets Q & P /\ Q is closed holds
( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) )
proof
let P, Q be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P meets Q & P /\ Q is closed holds
( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & P meets Q & P /\ Q is closed implies ( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) ) )
assume that
A1: P is_an_arc_of p1,p2 and
A2: P /\ Q <> {} and
A3: P /\ Q is closed ; :: according to XBOOLE_0:def_7 ::_thesis: ( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) )
reconsider P = P as non empty Subset of (TOP-REAL 2) by A2;
A4: P meets Q by A2, XBOOLE_0:def_7;
A5: P is_an_arc_of p2,p1 by A1, JORDAN5B:14;
A6: for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = Last_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
proof
set Ex = L[01] (((0,1) (#)),((#) (0,1)));
let f be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = Last_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not f . t in Q
let s2 be Real; ::_thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = Last_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds
not f . t in Q )
assume that
A7: f is being_homeomorphism and
A8: f . 0 = p1 and
A9: f . 1 = p2 and
A10: f . s2 = Last_Point (P,p2,p1,Q) and
A11: 0 <= s2 and
A12: s2 <= 1 ; ::_thesis: for t being Real st 0 <= t & t < s2 holds
not f . t in Q
set s21 = 1 - s2;
set g = f * (L[01] (((0,1) (#)),((#) (0,1))));
A13: L[01] (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18;
dom f = [#] I[01] by A7, TOPS_2:def_5;
then rng (L[01] (((0,1) (#)),((#) (0,1)))) = dom f by A13, TOPMETR:20, TOPS_2:def_5;
then dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = dom (L[01] (((0,1) (#)),((#) (0,1)))) by RELAT_1:27;
then A14: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = [#] I[01] by A13, TOPMETR:20, TOPS_2:def_5;
reconsider g = f * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],((TOP-REAL 2) | P) by TOPMETR:20;
A15: ( 1 - 1 <= 1 - s2 & 1 - s2 <= 1 - 0 ) by A11, A12, XREAL_1:13;
then A16: 1 - s2 in dom g by A14, BORSUK_1:43;
(L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by BORSUK_1:def_15, TREAL_1:5, TREAL_1:9;
then A17: g . 0 = p2 by A9, A14, BORSUK_1:def_14, FUNCT_1:12, TREAL_1:5;
(L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by BORSUK_1:def_14, TREAL_1:5, TREAL_1:9;
then A18: g . 1 = p1 by A8, A14, BORSUK_1:def_15, FUNCT_1:12, TREAL_1:5;
let t be Real; ::_thesis: ( 0 <= t & t < s2 implies not f . t in Q )
assume that
A19: 0 <= t and
A20: t < s2 ; ::_thesis: not f . t in Q
A21: 1 - t <= 1 - 0 by A19, XREAL_1:13;
t <= 1 by A12, A20, XXREAL_0:2;
then A22: 1 - 1 <= 1 - t by XREAL_1:13;
then reconsider r2 = 1 - s2, t9 = 1 - t as Point of (Closed-Interval-TSpace (0,1)) by A15, A21, BORSUK_1:43, TOPMETR:20;
A23: 1 - t in dom g by A14, A22, A21, BORSUK_1:43;
(L[01] (((0,1) (#)),((#) (0,1)))) . r2 = ((1 - (1 - s2)) * 1) + ((1 - s2) * 0) by BORSUK_1:def_14, BORSUK_1:def_15, TREAL_1:5, TREAL_1:def_3
.= s2 ;
then A24: g . (1 - s2) = f . s2 by A16, FUNCT_1:12;
(L[01] (((0,1) (#)),((#) (0,1)))) . t9 = ((1 - (1 - t)) * 1) + ((1 - t) * 0) by BORSUK_1:def_14, BORSUK_1:def_15, TREAL_1:5, TREAL_1:def_3
.= t ;
then A25: g . t9 = f . t by A23, FUNCT_1:12;
A26: 1 - s2 < 1 - t by A20, XREAL_1:15;
g is being_homeomorphism by A7, A13, TOPMETR:20, TOPS_2:57;
hence not f . t in Q by A3, A5, A4, A10, A17, A18, A15, A21, A24, A25, A26, Def2; ::_thesis: verum
end;
A27: for g being Function of I[01],((TOP-REAL 2) | P)
for s2 being Real st g is being_homeomorphism & g . 0 = p1 & g . 1 = p2 & g . s2 = First_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q
proof
set Ex = L[01] (((0,1) (#)),((#) (0,1)));
let f be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s2 being Real st f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = First_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not f . t in Q
let s2 be Real; ::_thesis: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 & f . s2 = First_Point (P,p2,p1,Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds
not f . t in Q )
assume that
A28: f is being_homeomorphism and
A29: f . 0 = p1 and
A30: f . 1 = p2 and
A31: f . s2 = First_Point (P,p2,p1,Q) and
A32: 0 <= s2 and
A33: s2 <= 1 ; ::_thesis: for t being Real st 1 >= t & t > s2 holds
not f . t in Q
set g = f * (L[01] (((0,1) (#)),((#) (0,1))));
A34: L[01] (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18;
dom f = [#] I[01] by A28, TOPS_2:def_5;
then rng (L[01] (((0,1) (#)),((#) (0,1)))) = dom f by A34, TOPMETR:20, TOPS_2:def_5;
then dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = dom (L[01] (((0,1) (#)),((#) (0,1)))) by RELAT_1:27;
then A35: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = [#] I[01] by A34, TOPMETR:20, TOPS_2:def_5;
let t be Real; ::_thesis: ( 1 >= t & t > s2 implies not f . t in Q )
assume that
A36: 1 >= t and
A37: t > s2 ; ::_thesis: not f . t in Q
A38: 1 - s2 > 1 - t by A37, XREAL_1:15;
set s21 = 1 - s2;
A39: 1 - s2 <= 1 - 0 by A32, XREAL_1:13;
reconsider g = f * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],((TOP-REAL 2) | P) by TOPMETR:20;
A40: 1 - 1 <= 1 - t by A36, XREAL_1:13;
A41: 1 - t <= 1 - 0 by A32, A37, XREAL_1:13;
then A42: 1 - t in dom g by A35, A40, BORSUK_1:43;
A43: 1 - 1 <= 1 - s2 by A33, XREAL_1:13;
then A44: 1 - s2 in dom g by A35, A39, BORSUK_1:43;
reconsider r2 = 1 - s2, t9 = 1 - t as Point of (Closed-Interval-TSpace (0,1)) by A43, A39, A40, A41, BORSUK_1:43, TOPMETR:20;
(L[01] (((0,1) (#)),((#) (0,1)))) . r2 = ((1 - (1 - s2)) * 1) + ((1 - s2) * 0) by BORSUK_1:def_14, BORSUK_1:def_15, TREAL_1:5, TREAL_1:def_3
.= s2 ;
then A45: g . (1 - s2) = f . s2 by A44, FUNCT_1:12;
(L[01] (((0,1) (#)),((#) (0,1)))) . t9 = ((1 - (1 - t)) * 1) + ((1 - t) * 0) by BORSUK_1:def_14, BORSUK_1:def_15, TREAL_1:5, TREAL_1:def_3
.= t ;
then A46: g . t9 = f . t by A42, FUNCT_1:12;
(L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by BORSUK_1:def_15, TREAL_1:5, TREAL_1:9;
then A47: g . 0 = p2 by A30, A35, BORSUK_1:def_14, FUNCT_1:12, TREAL_1:5;
(L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by BORSUK_1:def_14, TREAL_1:5, TREAL_1:9;
then A48: g . 1 = p1 by A29, A35, BORSUK_1:def_15, FUNCT_1:12, TREAL_1:5;
g is being_homeomorphism by A28, A34, TOPMETR:20, TOPS_2:57;
hence not f . t in Q by A3, A5, A4, A31, A47, A48, A39, A40, A45, A46, A38, Def1; ::_thesis: verum
end;
( Last_Point (P,p2,p1,Q) in P /\ Q & First_Point (P,p2,p1,Q) in P /\ Q ) by A3, A5, A4, Def1, Def2;
hence ( First_Point (P,p1,p2,Q) = Last_Point (P,p2,p1,Q) & Last_Point (P,p1,p2,Q) = First_Point (P,p2,p1,Q) ) by A1, A3, A4, A6, A27, Def1, Def2; ::_thesis: verum
end;
theorem Th19: :: JORDAN5C:19
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds
First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2)
for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds
First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)
let Q be Subset of (TOP-REAL 2); ::_thesis: for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds
First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)
let i be Element of NAT ; ::_thesis: ( L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) implies First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) )
assume that
A1: L~ f meets Q and
A2: Q is closed and
A3: f is being_S-Seq and
A4: ( 1 <= i & i + 1 <= len f ) and
A5: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) ; ::_thesis: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)
len f >= 2 by A3, TOPREAL1:def_8;
then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of the carrier of (TOP-REAL 2) by A5, TOPREAL1:23;
A6: P is_an_arc_of f /. 1,f /. (len f) by A3, TOPREAL1:25;
set FPO = First_Point (R,(f /. i),(f /. (i + 1)),Q);
set FPG = First_Point (P,(f /. 1),(f /. (len f)),Q);
A7: (L~ f) /\ Q is closed by A2, TOPS_1:8;
then First_Point (P,(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A6, Def1;
then A8: First_Point (P,(f /. 1),(f /. (len f)),Q) in Q by XBOOLE_0:def_4;
A9: i + 1 in dom f by A4, SEQ_4:134;
A10: ( f is one-to-one & i in dom f ) by A3, A4, SEQ_4:134, TOPREAL1:def_8;
A11: f /. i <> f /. (i + 1)
proof
assume f /. i = f /. (i + 1) ; ::_thesis: contradiction
then i = i + 1 by A10, A9, PARTFUN2:10;
hence contradiction ; ::_thesis: verum
end;
First_Point (P,(f /. 1),(f /. (len f)),Q) = First_Point (R,(f /. i),(f /. (i + 1)),Q)
proof
First_Point (P,(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A7, A6, Def1;
then A12: First_Point (P,(f /. 1),(f /. (len f)),Q) in L~ f by XBOOLE_0:def_4;
consider F being Function of I[01],((TOP-REAL 2) | P) such that
A13: F is being_homeomorphism and
A14: ( F . 0 = f /. 1 & F . 1 = f /. (len f) ) by A6, TOPREAL1:def_1;
rng F = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def_5
.= L~ f by PRE_TOPC:def_5 ;
then consider s21 being set such that
A15: s21 in dom F and
A16: F . s21 = First_Point (P,(f /. 1),(f /. (len f)),Q) by A12, FUNCT_1:def_3;
A17: dom F = [#] I[01] by A13, TOPS_2:def_5
.= [.0,1.] by BORSUK_1:40 ;
then reconsider s21 = s21 as Real by A15;
A18: s21 <= 1 by A15, BORSUK_1:43;
A19: for g being Function of I[01],((TOP-REAL 2) | R)
for s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = First_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
proof
consider ppi, pi1 being Real such that
A20: ppi < pi1 and
A21: 0 <= ppi and
ppi <= 1 and
0 <= pi1 and
A22: pi1 <= 1 and
A23: LSeg (f,i) = F .: [.ppi,pi1.] and
A24: F . ppi = f /. i and
A25: F . pi1 = f /. (i + 1) by A3, A4, A13, A14, JORDAN5B:7;
A26: ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A20;
then reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01] by A21, A22, BORSUK_1:40, RCOMP_1:def_1, XXREAL_1:34;
consider hh being Function of (I[01] | Poz),((TOP-REAL 2) | R) such that
A27: hh = F | Poz and
A28: hh is being_homeomorphism by A3, A4, A13, A14, A23, JORDAN5B:8;
A29: hh = F * (id Poz) by A27, RELAT_1:65;
A30: [.ppi,pi1.] c= [.0,1.] by A21, A22, XXREAL_1:34;
reconsider A = Closed-Interval-TSpace (ppi,pi1) as strict SubSpace of I[01] by A20, A21, A22, TOPMETR:20, TREAL_1:3;
Poz = [#] A by A20, TOPMETR:18;
then A31: I[01] | Poz = A by PRE_TOPC:def_5;
hh " is being_homeomorphism by A28, TOPS_2:56;
then A32: ( hh " is continuous & hh " is one-to-one ) by TOPS_2:def_5;
pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A20;
then pi1 in [.ppi,pi1.] by RCOMP_1:def_1;
then pi1 in (dom F) /\ Poz by A17, A30, XBOOLE_0:def_4;
then A33: pi1 in dom hh by A27, RELAT_1:61;
then A34: hh . pi1 = f /. (i + 1) by A25, A27, FUNCT_1:47;
the carrier of ((TOP-REAL 2) | P) = [#] ((TOP-REAL 2) | P)
.= P by PRE_TOPC:def_5 ;
then reconsider SEG = LSeg (f,i) as non empty Subset of the carrier of ((TOP-REAL 2) | P) by A5, TOPREAL3:19;
A35: the carrier of (((TOP-REAL 2) | P) | SEG) = [#] (((TOP-REAL 2) | P) | SEG)
.= SEG by PRE_TOPC:def_5 ;
reconsider SE = SEG as non empty Subset of (TOP-REAL 2) ;
let g be Function of I[01],((TOP-REAL 2) | R); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = First_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds
for t being Real st 0 <= t & t < s2 holds
not g . t in Q
let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = First_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 0 <= t & t < s2 holds
not g . t in Q )
assume that
A36: g is being_homeomorphism and
A37: g . 0 = f /. i and
A38: g . 1 = f /. (i + 1) and
A39: g . s2 = First_Point (P,(f /. 1),(f /. (len f)),Q) and
A40: 0 <= s2 and
A41: s2 <= 1 ; ::_thesis: for t being Real st 0 <= t & t < s2 holds
not g . t in Q
A42: ( g is continuous & g is one-to-one ) by A36, TOPS_2:def_5;
reconsider SEG = SEG as non empty Subset of ((TOP-REAL 2) | P) ;
A43: ((TOP-REAL 2) | P) | SEG = (TOP-REAL 2) | SE by GOBOARD9:2;
ppi in [.ppi,pi1.] by A26, RCOMP_1:def_1;
then ppi in (dom F) /\ Poz by A17, A30, XBOOLE_0:def_4;
then A44: ppi in dom hh by A27, RELAT_1:61;
then A45: hh . ppi = f /. i by A24, A27, FUNCT_1:47;
A46: dom hh = [#] (I[01] | Poz) by A28, TOPS_2:def_5;
then A47: dom hh = Poz by PRE_TOPC:def_5;
A48: rng hh = hh .: (dom hh) by A46, RELSET_1:22
.= [#] (((TOP-REAL 2) | P) | SEG) by A23, A35, A27, A47, RELAT_1:129 ;
let t be Real; ::_thesis: ( 0 <= t & t < s2 implies not g . t in Q )
assume that
A49: 0 <= t and
A50: t < s2 ; ::_thesis: not g . t in Q
A51: t < 1 by A41, A50, XXREAL_0:2;
then reconsider w1 = s2, w2 = t as Point of (Closed-Interval-TSpace (0,1)) by A40, A41, A49, BORSUK_1:43, TOPMETR:20;
A52: ( F is one-to-one & rng F = [#] ((TOP-REAL 2) | P) ) by A13, TOPS_2:def_5;
set H = (hh ") * g;
A53: rng g = [#] ((TOP-REAL 2) | SE) by A36, TOPS_2:def_5;
set ss = ((hh ") * g) . t;
A54: hh is one-to-one by A28, TOPS_2:def_5;
A55: hh is one-to-one by A28, TOPS_2:def_5;
then A56: dom (hh ") = [#] (((TOP-REAL 2) | P) | SEG) by A43, A48, TOPS_2:49;
then A57: rng ((hh ") * g) = rng (hh ") by A53, RELAT_1:28;
A58: rng (hh ") = [#] (I[01] | Poz) by A43, A55, A48, TOPS_2:49
.= Poz by PRE_TOPC:def_5 ;
then rng ((hh ") * g) = Poz by A53, A56, RELAT_1:28;
then A59: rng ((hh ") * g) c= the carrier of (Closed-Interval-TSpace (ppi,pi1)) by A20, TOPMETR:18;
hh is onto by A43, A48, FUNCT_2:def_3;
then A60: hh " = hh " by A55, TOPS_2:def_4;
A61: dom g = [#] I[01] by A36, TOPS_2:def_5
.= the carrier of I[01] ;
then A62: dom ((hh ") * g) = the carrier of (Closed-Interval-TSpace (0,1)) by A43, A53, A56, RELAT_1:27, TOPMETR:20;
A63: t in dom g by A61, A49, A51, BORSUK_1:43;
then g . t in [#] ((TOP-REAL 2) | SE) by A53, FUNCT_1:def_3;
then A64: g . t in SEG by PRE_TOPC:def_5;
then consider x being set such that
A65: x in dom F and
A66: x in Poz and
A67: g . t = F . x by A23, FUNCT_1:def_6;
A68: F is one-to-one by A52;
then A69: (F ") . (g . t) in Poz by A65, A66, A67, FUNCT_1:32;
F is onto by A52, FUNCT_2:def_3;
then A70: F " = F " by A52, TOPS_2:def_4;
x = (F ") . (g . t) by A68, A65, A67, FUNCT_1:32;
then (F ") . (g . t) in Poz by A66, A70;
then A71: (F ") . (g . t) in dom (id Poz) by FUNCT_1:17;
g . t in the carrier of ((TOP-REAL 2) | P) by A64;
then A72: g . t in dom (F ") by A52, TOPS_2:49;
t in dom ((hh ") * g) by A43, A53, A63, A56, RELAT_1:27;
then A73: F . (((hh ") * g) . t) = (((hh ") * g) * F) . t by FUNCT_1:13
.= (g * ((hh ") * F)) . t by RELAT_1:36
.= (F * (hh ")) . (g . t) by A63, FUNCT_1:13
.= (F * ((F ") * ((id Poz) "))) . (g . t) by A68, A29, A60, FUNCT_1:44
.= (((F ") * ((id Poz) ")) * F) . (g . t) by A70
.= ((F ") * (((id Poz) ") * F)) . (g . t) by RELAT_1:36
.= ((F ") * (F * (id Poz))) . (g . t) by FUNCT_1:45
.= (F * (id Poz)) . ((F ") . (g . t)) by A72, FUNCT_1:13
.= F . ((id Poz) . ((F ") . (g . t))) by A71, FUNCT_1:13
.= F . ((F ") . (g . t)) by A69, A70, FUNCT_1:17
.= g . t by A52, A64, FUNCT_1:35 ;
1 in dom g by A61, BORSUK_1:43;
then A74: ((hh ") * g) . 1 = (hh ") . (f /. (i + 1)) by A38, FUNCT_1:13
.= pi1 by A54, A33, A34, A60, FUNCT_1:32 ;
0 in dom g by A61, BORSUK_1:43;
then A75: ((hh ") * g) . 0 = (hh ") . (f /. i) by A37, FUNCT_1:13
.= ppi by A54, A44, A45, A60, FUNCT_1:32 ;
dom ((hh ") * g) = dom g by A43, A53, A56, RELAT_1:27;
then ((hh ") * g) . t in Poz by A58, A63, A57, FUNCT_1:def_3;
then ((hh ") * g) . t in { l where l is Real : ( ppi <= l & l <= pi1 ) } by RCOMP_1:def_1;
then consider ss9 being Real such that
A76: ss9 = ((hh ") * g) . t and
A77: ppi <= ss9 and
ss9 <= pi1 ;
reconsider H = (hh ") * g as Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (ppi,pi1)) by A62, A59, FUNCT_2:2;
A78: ss9 = H . w2 by A76;
ex z being set st
( z in dom F & z in Poz & F . s21 = F . z ) by A5, A16, A23, FUNCT_1:def_6;
then A79: s21 in Poz by A15, A68, FUNCT_1:def_4;
then hh . s21 = g . s2 by A16, A39, A27, FUNCT_1:49;
then s21 = (hh ") . (g . s2) by A55, A47, A79, FUNCT_1:32;
then A80: s21 = (hh ") . (g . s2) by A60;
s2 in dom g by A40, A41, A61, BORSUK_1:43;
then s21 = H . w1 by A80, FUNCT_1:13;
then ss9 < s21 by A20, A50, A75, A74, A42, A32, A31, A78, JORDAN5A:15, TOPMETR:20;
hence not g . t in Q by A1, A7, A6, A13, A14, A16, A18, A21, A76, A77, A73, Def1; ::_thesis: verum
end;
A81: (LSeg (f,i)) /\ Q is closed by A2, TOPS_1:8;
(LSeg (f,i)) /\ Q <> {} by A5, A8, XBOOLE_0:def_4;
then A82: LSeg (f,i) meets Q by XBOOLE_0:def_7;
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, TOPREAL1:def_3;
then A83: R is_an_arc_of f /. i,f /. (i + 1) by A11, TOPREAL1:9;
First_Point (P,(f /. 1),(f /. (len f)),Q) in (LSeg (f,i)) /\ Q by A5, A8, XBOOLE_0:def_4;
hence First_Point (P,(f /. 1),(f /. (len f)),Q) = First_Point (R,(f /. i),(f /. (i + 1)),Q) by A82, A81, A83, A19, Def1; ::_thesis: verum
end;
hence First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) ; ::_thesis: verum
end;
theorem Th20: :: JORDAN5C:20
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2)
for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)
let Q be Subset of (TOP-REAL 2); ::_thesis: for i being Element of NAT st L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) holds
Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)
let i be Element of NAT ; ::_thesis: ( L~ f meets Q & Q is closed & f is being_S-Seq & 1 <= i & i + 1 <= len f & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) implies Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) )
assume that
A1: L~ f meets Q and
A2: Q is closed and
A3: f is being_S-Seq and
A4: ( 1 <= i & i + 1 <= len f ) and
A5: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) ; ::_thesis: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q)
len f >= 2 by A3, TOPREAL1:def_8;
then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A5, TOPREAL1:23;
A6: P is_an_arc_of f /. 1,f /. (len f) by A3, TOPREAL1:25;
set FPO = Last_Point (R,(f /. i),(f /. (i + 1)),Q);
set FPG = Last_Point (P,(f /. 1),(f /. (len f)),Q);
A7: (L~ f) /\ Q is closed by A2, TOPS_1:8;
then Last_Point (P,(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A6, Def2;
then A8: Last_Point (P,(f /. 1),(f /. (len f)),Q) in Q by XBOOLE_0:def_4;
A9: i + 1 in dom f by A4, SEQ_4:134;
A10: ( f is one-to-one & i in dom f ) by A3, A4, SEQ_4:134, TOPREAL1:def_8;
A11: f /. i <> f /. (i + 1)
proof
assume f /. i = f /. (i + 1) ; ::_thesis: contradiction
then i = i + 1 by A10, A9, PARTFUN2:10;
hence contradiction ; ::_thesis: verum
end;
Last_Point (P,(f /. 1),(f /. (len f)),Q) = Last_Point (R,(f /. i),(f /. (i + 1)),Q)
proof
Last_Point (P,(f /. 1),(f /. (len f)),Q) in (L~ f) /\ Q by A1, A7, A6, Def2;
then A12: Last_Point (P,(f /. 1),(f /. (len f)),Q) in L~ f by XBOOLE_0:def_4;
consider F being Function of I[01],((TOP-REAL 2) | P) such that
A13: F is being_homeomorphism and
A14: ( F . 0 = f /. 1 & F . 1 = f /. (len f) ) by A6, TOPREAL1:def_1;
rng F = [#] ((TOP-REAL 2) | P) by A13, TOPS_2:def_5
.= L~ f by PRE_TOPC:def_5 ;
then consider s21 being set such that
A15: s21 in dom F and
A16: F . s21 = Last_Point (P,(f /. 1),(f /. (len f)),Q) by A12, FUNCT_1:def_3;
A17: dom F = [#] I[01] by A13, TOPS_2:def_5
.= [.0,1.] by BORSUK_1:40 ;
then reconsider s21 = s21 as Real by A15;
A18: ( 0 <= s21 & s21 <= 1 ) by A15, BORSUK_1:43;
A19: for g being Function of I[01],((TOP-REAL 2) | R)
for s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = Last_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q
proof
consider ppi, pi1 being Real such that
A20: ppi < pi1 and
A21: 0 <= ppi and
ppi <= 1 and
0 <= pi1 and
A22: pi1 <= 1 and
A23: LSeg (f,i) = F .: [.ppi,pi1.] and
A24: F . ppi = f /. i and
A25: F . pi1 = f /. (i + 1) by A3, A4, A13, A14, JORDAN5B:7;
A26: ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A20;
then reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01] by A21, A22, BORSUK_1:40, RCOMP_1:def_1, XXREAL_1:34;
A27: [.ppi,pi1.] c= [.0,1.] by A21, A22, XXREAL_1:34;
reconsider A = Closed-Interval-TSpace (ppi,pi1) as strict SubSpace of I[01] by A20, A21, A22, TOPMETR:20, TREAL_1:3;
A28: Poz = [#] A by A20, TOPMETR:18;
then A29: I[01] | Poz = A by PRE_TOPC:def_5;
Closed-Interval-TSpace (ppi,pi1) is compact by A20, HEINE:4;
then [#] (Closed-Interval-TSpace (ppi,pi1)) is compact by COMPTS_1:1;
then for P being Subset of A st P = Poz holds
P is compact by A20, TOPMETR:18;
then Poz is compact by A28, COMPTS_1:2;
then A30: I[01] | Poz is compact by COMPTS_1:3;
reconsider Lf = L~ f as non empty Subset of (TOP-REAL 2) by A6;
let g be Function of I[01],((TOP-REAL 2) | R); ::_thesis: for s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = Last_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 holds
for t being Real st 1 >= t & t > s2 holds
not g . t in Q
let s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s2 = Last_Point (P,(f /. 1),(f /. (len f)),Q) & 0 <= s2 & s2 <= 1 implies for t being Real st 1 >= t & t > s2 holds
not g . t in Q )
assume that
A31: g is being_homeomorphism and
A32: g . 0 = f /. i and
A33: g . 1 = f /. (i + 1) and
A34: g . s2 = Last_Point (P,(f /. 1),(f /. (len f)),Q) and
A35: 0 <= s2 and
A36: s2 <= 1 ; ::_thesis: for t being Real st 1 >= t & t > s2 holds
not g . t in Q
the carrier of ((TOP-REAL 2) | Lf) = [#] ((TOP-REAL 2) | Lf)
.= Lf by PRE_TOPC:def_5 ;
then reconsider SEG = LSeg (f,i) as non empty Subset of ((TOP-REAL 2) | Lf) by A5, TOPREAL3:19;
reconsider SE = SEG as non empty Subset of (TOP-REAL 2) ;
A37: rng g = [#] ((TOP-REAL 2) | SE) by A31, TOPS_2:def_5;
set gg = F | Poz;
A38: the carrier of (I[01] | Poz) = [#] (I[01] | Poz)
.= Poz by PRE_TOPC:def_5 ;
then reconsider gg = F | Poz as Function of (I[01] | Poz),((TOP-REAL 2) | P) by FUNCT_2:32;
let t be Real; ::_thesis: ( 1 >= t & t > s2 implies not g . t in Q )
assume that
A39: 1 >= t and
A40: t > s2 ; ::_thesis: not g . t in Q
A41: rng gg c= SEG
proof
let ii be set ; :: according to TARSKI:def_3 ::_thesis: ( not ii in rng gg or ii in SEG )
assume ii in rng gg ; ::_thesis: ii in SEG
then consider j being set such that
A42: j in dom gg and
A43: ii = gg . j by FUNCT_1:def_3;
j in (dom F) /\ Poz by A42, RELAT_1:61;
then j in dom F by XBOOLE_0:def_4;
then F . j in LSeg (f,i) by A23, A38, A42, FUNCT_1:def_6;
hence ii in SEG by A38, A42, A43, FUNCT_1:49; ::_thesis: verum
end;
A44: the carrier of (((TOP-REAL 2) | Lf) | SEG) = [#] (((TOP-REAL 2) | Lf) | SEG)
.= SEG by PRE_TOPC:def_5 ;
reconsider SEG = SEG as non empty Subset of ((TOP-REAL 2) | Lf) ;
reconsider hh9 = gg as Function of (I[01] | Poz),(((TOP-REAL 2) | Lf) | SEG) by A44, A41, FUNCT_2:6;
reconsider hh = hh9 as Function of (I[01] | Poz),((TOP-REAL 2) | SE) by GOBOARD9:2;
A45: dom hh = [#] (I[01] | Poz) by FUNCT_2:def_1;
then A46: dom hh = Poz by PRE_TOPC:def_5;
A47: rng hh = hh .: (dom hh) by A45, RELSET_1:22
.= [#] (((TOP-REAL 2) | Lf) | SEG) by A23, A44, A46, RELAT_1:129 ;
A48: F is one-to-one by A13, TOPS_2:def_5;
then A49: hh is one-to-one by FUNCT_1:52;
set H = (hh ") * g;
A50: ((TOP-REAL 2) | Lf) | SEG = (TOP-REAL 2) | SE by GOBOARD9:2;
A51: hh9 is one-to-one by A48, FUNCT_1:52;
then A52: dom (hh ") = [#] (((TOP-REAL 2) | Lf) | SEG) by A50, A47, TOPS_2:49;
then A53: rng ((hh ") * g) = rng (hh ") by A37, RELAT_1:28;
A54: dom g = [#] I[01] by A31, TOPS_2:def_5
.= the carrier of I[01] ;
then A55: dom ((hh ") * g) = the carrier of (Closed-Interval-TSpace (0,1)) by A50, A37, A52, RELAT_1:27, TOPMETR:20;
A56: t in dom g by A35, A54, A39, A40, BORSUK_1:43;
then g . t in [#] ((TOP-REAL 2) | SE) by A37, FUNCT_1:def_3;
then A57: g . t in SEG by PRE_TOPC:def_5;
then consider x being set such that
A58: x in dom F and
A59: x in Poz and
A60: g . t = F . x by A23, FUNCT_1:def_6;
hh is onto by A50, A47, FUNCT_2:def_3;
then A61: hh " = hh " by A51, TOPS_2:def_4;
A62: (F ") . (g . t) in Poz by A48, A58, A59, A60, FUNCT_1:32;
ex z being set st
( z in dom F & z in Poz & F . s21 = F . z ) by A5, A16, A23, FUNCT_1:def_6;
then A63: s21 in Poz by A15, A48, FUNCT_1:def_4;
then hh . s21 = g . s2 by A16, A34, FUNCT_1:49;
then s21 = (hh ") . (g . s2) by A51, A46, A63, FUNCT_1:32;
then A64: s21 = (hh ") . (g . s2) by A61;
A65: ( g is continuous & g is one-to-one ) by A31, TOPS_2:def_5;
A66: (TOP-REAL 2) | SE is T_2 by TOPMETR:2;
reconsider w1 = s2, w2 = t as Point of (Closed-Interval-TSpace (0,1)) by A35, A36, A39, A40, BORSUK_1:43, TOPMETR:20;
A67: hh = F * (id Poz) by RELAT_1:65;
set ss = ((hh ") * g) . t;
A68: ( F is one-to-one & rng F = [#] ((TOP-REAL 2) | P) ) by A13, TOPS_2:def_5;
A69: rng (hh ") = [#] (I[01] | Poz) by A50, A51, A47, TOPS_2:49
.= Poz by PRE_TOPC:def_5 ;
then rng ((hh ") * g) = Poz by A37, A52, RELAT_1:28;
then A70: rng ((hh ") * g) c= the carrier of (Closed-Interval-TSpace (ppi,pi1)) by A20, TOPMETR:18;
dom ((hh ") * g) = dom g by A50, A37, A52, RELAT_1:27;
then ((hh ") * g) . t in Poz by A69, A56, A53, FUNCT_1:def_3;
then ((hh ") * g) . t in { l where l is Real : ( ppi <= l & l <= pi1 ) } by RCOMP_1:def_1;
then consider ss9 being Real such that
A71: ss9 = ((hh ") * g) . t and
ppi <= ss9 and
A72: ss9 <= pi1 ;
F is onto by A68, FUNCT_2:def_3;
then A73: F " = F " by A68, TOPS_2:def_4;
A74: 1 >= ss9 by A22, A72, XXREAL_0:2;
x = (F ") . (g . t) by A48, A58, A60, FUNCT_1:32;
then (F ") . (g . t) in Poz by A59, A73;
then A75: (F ") . (g . t) in dom (id Poz) by FUNCT_1:17;
g . t in the carrier of ((TOP-REAL 2) | Lf) by A57;
then A76: g . t in dom (F ") by A68, TOPS_2:49;
t in dom ((hh ") * g) by A50, A37, A56, A52, RELAT_1:27;
then A77: F . (((hh ") * g) . t) = (((hh ") * g) * F) . t by FUNCT_1:13
.= (g * ((hh ") * F)) . t by RELAT_1:36
.= (F * (hh ")) . (g . t) by A56, FUNCT_1:13
.= (F * (hh ")) . (g . t) by A61
.= (F * ((F ") * ((id Poz) "))) . (g . t) by A48, A67, FUNCT_1:44
.= (((F ") * ((id Poz) ")) * F) . (g . t) by A73
.= ((F ") * (((id Poz) ") * F)) . (g . t) by RELAT_1:36
.= ((F ") * (F * (id Poz))) . (g . t) by FUNCT_1:45
.= (F * (id Poz)) . ((F ") . (g . t)) by A76, FUNCT_1:13
.= F . ((id Poz) . ((F ") . (g . t))) by A75, FUNCT_1:13
.= F . ((id Poz) . ((F ") . (g . t))) by A73
.= F . ((F ") . (g . t)) by A62, FUNCT_1:17
.= g . t by A68, A57, FUNCT_1:35 ;
pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A20;
then pi1 in [.ppi,pi1.] by RCOMP_1:def_1;
then pi1 in (dom F) /\ Poz by A17, A27, XBOOLE_0:def_4;
then A78: pi1 in dom hh by RELAT_1:61;
then A79: hh . pi1 = f /. (i + 1) by A25, FUNCT_1:47;
F is continuous by A13, TOPS_2:def_5;
then gg is continuous by TOPMETR:7;
then hh is being_homeomorphism by A50, A51, A45, A47, A30, A66, COMPTS_1:17, TOPMETR:6;
then hh " is being_homeomorphism by TOPS_2:56;
then A80: ( hh " is continuous & hh " is one-to-one ) by TOPS_2:def_5;
ppi in [.ppi,pi1.] by A26, RCOMP_1:def_1;
then ppi in (dom F) /\ Poz by A17, A27, XBOOLE_0:def_4;
then A81: ppi in dom hh by RELAT_1:61;
then A82: hh . ppi = f /. i by A24, FUNCT_1:47;
1 in dom g by A54, BORSUK_1:43;
then A83: ((hh ") * g) . 1 = (hh ") . (f /. (i + 1)) by A33, FUNCT_1:13
.= pi1 by A49, A78, A79, A61, FUNCT_1:32 ;
0 in dom g by A54, BORSUK_1:43;
then A84: ((hh ") * g) . 0 = (hh ") . (f /. i) by A32, FUNCT_1:13
.= ppi by A49, A81, A82, A61, FUNCT_1:32 ;
reconsider H = (hh ") * g as Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (ppi,pi1)) by A55, A70, FUNCT_2:2;
s2 in dom g by A35, A36, A54, BORSUK_1:43;
then A85: s21 = H . w1 by A64, FUNCT_1:13;
ss9 = H . w2 by A71;
then ss9 > s21 by A20, A40, A84, A83, A65, A80, A29, A85, JORDAN5A:15, TOPMETR:20;
hence not g . t in Q by A1, A7, A6, A13, A14, A16, A18, A71, A74, A77, Def2; ::_thesis: verum
end;
A86: (LSeg (f,i)) /\ Q is closed by A2, TOPS_1:8;
(LSeg (f,i)) /\ Q <> {} by A5, A8, XBOOLE_0:def_4;
then A87: LSeg (f,i) meets Q by XBOOLE_0:def_7;
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, TOPREAL1:def_3;
then A88: R is_an_arc_of f /. i,f /. (i + 1) by A11, TOPREAL1:9;
Last_Point (P,(f /. 1),(f /. (len f)),Q) in (LSeg (f,i)) /\ Q by A5, A8, XBOOLE_0:def_4;
hence Last_Point (P,(f /. 1),(f /. (len f)),Q) = Last_Point (R,(f /. i),(f /. (i + 1)),Q) by A87, A86, A88, A19, Def2; ::_thesis: verum
end;
hence Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q) ; ::_thesis: verum
end;
theorem :: JORDAN5C:21
for f being FinSequence of (TOP-REAL 2)
for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) holds
First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) holds
First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i
let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len f & f is being_S-Seq & First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) implies First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i )
assume that
A1: ( 1 <= i & i + 1 <= len f ) and
A2: f is being_S-Seq and
A3: First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) ; ::_thesis: First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i
reconsider Q = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A3;
Q = LSeg ((f /. i),(f /. (i + 1))) by A1, TOPREAL1:def_3;
then Q c= L~ f by A1, SPPOL_2:16;
then L~ f meets Q by A3, XBOOLE_0:3;
then A4: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point (Q,(f /. i),(f /. (i + 1)),Q) by A1, A2, A3, Th19;
( Q is closed & Q is_an_arc_of f /. i,f /. (i + 1) ) by A1, A2, JORDAN5B:15;
hence First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i by A4, Th7; ::_thesis: verum
end;
theorem :: JORDAN5C:22
for f being FinSequence of (TOP-REAL 2)
for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) holds
Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st 1 <= i & i + 1 <= len f & f is being_S-Seq & Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) holds
Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1)
let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len f & f is being_S-Seq & Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) implies Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1) )
assume that
A1: ( 1 <= i & i + 1 <= len f ) and
A2: f is being_S-Seq and
A3: Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) ; ::_thesis: Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1)
reconsider Q = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A3;
Q = LSeg ((f /. i),(f /. (i + 1))) by A1, TOPREAL1:def_3;
then Q c= L~ f by A1, SPPOL_2:16;
then L~ f meets Q by A3, XBOOLE_0:3;
then A4: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point (Q,(f /. i),(f /. (i + 1)),Q) by A1, A2, A3, Th20;
( Q is closed & Q is_an_arc_of f /. i,f /. (i + 1) ) by A1, A2, JORDAN5B:15;
hence Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1) by A4, Th7; ::_thesis: verum
end;
theorem Th23: :: JORDAN5C:23
for f being FinSequence of (TOP-REAL 2)
for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f holds
LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f holds
LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f)
let i be Element of NAT ; ::_thesis: ( f is being_S-Seq & 1 <= i & i + 1 <= len f implies LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f) )
assume that
A1: f is being_S-Seq and
A2: ( 1 <= i & i + 1 <= len f ) ; ::_thesis: LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f)
set p1 = f /. 1;
set p2 = f /. (len f);
set q1 = f /. i;
set q2 = f /. (i + 1);
A3: len f >= 2 by A1, TOPREAL1:def_8;
then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by TOPREAL1:23;
i + 1 in dom f by A2, SEQ_4:134;
then A4: f /. (i + 1) in P by A3, GOBOARD1:1;
A5: for g being Function of I[01],((TOP-REAL 2) | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 holds
s1 <= s2
proof
let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 holds
s1 <= s2
let s1, s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume that
A6: g is being_homeomorphism and
A7: ( g . 0 = f /. 1 & g . 1 = f /. (len f) ) and
A8: g . s1 = f /. i and
A9: ( 0 <= s1 & s1 <= 1 ) and
A10: g . s2 = f /. (i + 1) and
A11: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: s1 <= s2
A12: dom g = [#] I[01] by A6, TOPS_2:def_5
.= the carrier of I[01] ;
then A13: s1 in dom g by A9, BORSUK_1:43;
A14: s2 in dom g by A11, A12, BORSUK_1:43;
A15: g is one-to-one by A6, TOPS_2:def_5;
consider r1, r2 being Real such that
A16: r1 < r2 and
A17: 0 <= r1 and
A18: r1 <= 1 and
0 <= r2 and
A19: r2 <= 1 and
LSeg (f,i) = g .: [.r1,r2.] and
A20: g . r1 = f /. i and
A21: g . r2 = f /. (i + 1) by A1, A2, A6, A7, JORDAN5B:7;
A22: r2 in dom g by A16, A17, A19, A12, BORSUK_1:43;
r1 in dom g by A17, A18, A12, BORSUK_1:43;
then s1 = r1 by A8, A20, A13, A15, FUNCT_1:def_4;
hence s1 <= s2 by A10, A16, A21, A22, A14, A15, FUNCT_1:def_4; ::_thesis: verum
end;
i in dom f by A2, SEQ_4:134;
then f /. i in P by A3, GOBOARD1:1;
hence LE f /. i,f /. (i + 1), L~ f,f /. 1,f /. (len f) by A4, A5, Def3; ::_thesis: verum
end;
theorem Th24: :: JORDAN5C:24
for f being FinSequence of (TOP-REAL 2)
for i, j being Element of NAT st f is being_S-Seq & 1 <= i & i <= j & j <= len f holds
LE f /. i,f /. j, L~ f,f /. 1,f /. (len f)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT st f is being_S-Seq & 1 <= i & i <= j & j <= len f holds
LE f /. i,f /. j, L~ f,f /. 1,f /. (len f)
let i, j be Element of NAT ; ::_thesis: ( f is being_S-Seq & 1 <= i & i <= j & j <= len f implies LE f /. i,f /. j, L~ f,f /. 1,f /. (len f) )
assume that
A1: f is being_S-Seq and
A2: 1 <= i and
A3: i <= j and
A4: j <= len f ; ::_thesis: LE f /. i,f /. j, L~ f,f /. 1,f /. (len f)
consider k being Nat such that
A5: i + k = j by A3, NAT_1:10;
A6: len f >= 2 by A1, TOPREAL1:def_8;
then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by TOPREAL1:23;
defpred S1[ Element of NAT ] means ( 1 <= i & i + $1 <= len f implies LE f /. i,f /. (i + $1),P,f /. 1,f /. (len f) );
A7: for l being Element of NAT st S1[l] holds
S1[l + 1]
proof
let l be Element of NAT ; ::_thesis: ( S1[l] implies S1[l + 1] )
assume A8: S1[l] ; ::_thesis: S1[l + 1]
A9: i + l <= (i + l) + 1 by NAT_1:11;
assume that
A10: 1 <= i and
A11: i + (l + 1) <= len f ; ::_thesis: LE f /. i,f /. (i + (l + 1)),P,f /. 1,f /. (len f)
A12: (i + l) + 1 <= len f by A11;
i <= i + l by NAT_1:11;
then 1 <= i + l by A10, XXREAL_0:2;
then LE f /. (i + l),f /. (i + (l + 1)),P,f /. 1,f /. (len f) by A1, A12, Th23;
hence LE f /. i,f /. (i + (l + 1)),P,f /. 1,f /. (len f) by A8, A10, A11, A9, Th13, XXREAL_0:2; ::_thesis: verum
end;
A13: S1[ 0 ]
proof
assume ( 1 <= i & i + 0 <= len f ) ; ::_thesis: LE f /. i,f /. (i + 0),P,f /. 1,f /. (len f)
then i in dom f by FINSEQ_3:25;
hence LE f /. i,f /. (i + 0),P,f /. 1,f /. (len f) by A6, Th9, GOBOARD1:1; ::_thesis: verum
end;
A14: for l being Element of NAT holds S1[l] from NAT_1:sch_1(A13, A7);
k in NAT by ORDINAL1:def_12;
hence LE f /. i,f /. j, L~ f,f /. 1,f /. (len f) by A2, A4, A5, A14; ::_thesis: verum
end;
Lm1: for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)
let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2)
for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)
let q be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)
let i be Element of NAT ; ::_thesis: ( LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q implies LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1) )
assume that
A1: LSeg (f,i) meets Q and
A2: f is being_S-Seq and
A3: Q is closed and
A4: ( 1 <= i & i + 1 <= len f ) and
A5: q in LSeg (f,i) and
A6: q in Q ; ::_thesis: LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1)
reconsider P = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A5;
set q1 = First_Point (P,(f /. i),(f /. (i + 1)),Q);
set p1 = f /. i;
set p2 = f /. (i + 1);
A7: P /\ Q c= P by XBOOLE_1:17;
A8: i + 1 in dom f by A4, SEQ_4:134;
A9: ( f is one-to-one & i in dom f ) by A2, A4, SEQ_4:134, TOPREAL1:def_8;
A10: f /. i <> f /. (i + 1)
proof
assume f /. i = f /. (i + 1) ; ::_thesis: contradiction
then i = i + 1 by A9, A8, PARTFUN2:10;
hence contradiction ; ::_thesis: verum
end;
A11: P /\ Q is closed by A3, TOPS_1:8;
P is_an_arc_of f /. i,f /. (i + 1) by A2, A4, JORDAN5B:15;
then ( First_Point (P,(f /. i),(f /. (i + 1)),Q) in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s1 = First_Point (P,(f /. i),(f /. (i + 1)),Q) & 0 <= s1 & s1 <= 1 & g . s2 = q & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) ) by A1, A6, A11, Def1;
then A12: LE First_Point (P,(f /. i),(f /. (i + 1)),Q),q,P,f /. i,f /. (i + 1) by A5, A7, Def3;
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, TOPREAL1:def_3;
hence LE First_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),q,f /. i,f /. (i + 1) by A10, A12, Th17; ::_thesis: verum
end;
Lm2: for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1)
let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2)
for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1)
let q be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1)
let i be Element of NAT ; ::_thesis: ( L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) )
assume that
A1: L~ f meets Q and
A2: f is being_S-Seq and
A3: Q is closed and
A4: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) and
A5: ( 1 <= i & i + 1 <= len f ) and
A6: ( q in LSeg (f,i) & q in Q ) ; ::_thesis: LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1)
len f >= 2 by A2, TOPREAL1:def_8;
then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A4, TOPREAL1:23;
(LSeg (f,i)) /\ Q <> {} by A6, XBOOLE_0:def_4;
then A7: LSeg (f,i) meets Q by XBOOLE_0:def_7;
First_Point (P,(f /. 1),(f /. (len f)),Q) = First_Point (R,(f /. i),(f /. (i + 1)),Q) by A1, A2, A3, A4, A5, Th19;
hence LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) by A2, A3, A5, A6, A7, Lm1; ::_thesis: verum
end;
Lm3: for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1)
let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2)
for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1)
let q be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1)
let i be Element of NAT ; ::_thesis: ( LSeg (f,i) meets Q & f is being_S-Seq & Q is closed & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q implies LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1) )
assume that
A1: LSeg (f,i) meets Q and
A2: f is being_S-Seq and
A3: Q is closed and
A4: ( 1 <= i & i + 1 <= len f ) and
A5: q in LSeg (f,i) and
A6: q in Q ; ::_thesis: LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1)
reconsider P = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A5;
set q1 = Last_Point (P,(f /. i),(f /. (i + 1)),Q);
set p1 = f /. i;
set p2 = f /. (i + 1);
A7: P /\ Q c= P by XBOOLE_1:17;
A8: i + 1 in dom f by A4, SEQ_4:134;
A9: ( f is one-to-one & i in dom f ) by A2, A4, SEQ_4:134, TOPREAL1:def_8;
A10: f /. i <> f /. (i + 1)
proof
assume f /. i = f /. (i + 1) ; ::_thesis: contradiction
then i = i + 1 by A9, A8, PARTFUN2:10;
hence contradiction ; ::_thesis: verum
end;
A11: P /\ Q is closed by A3, TOPS_1:8;
P is_an_arc_of f /. i,f /. (i + 1) by A2, A4, JORDAN5B:15;
then ( Last_Point (P,(f /. i),(f /. (i + 1)),Q) in P /\ Q & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. i & g . 1 = f /. (i + 1) & g . s1 = q & 0 <= s1 & s1 <= 1 & g . s2 = Last_Point (P,(f /. i),(f /. (i + 1)),Q) & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) ) by A1, A6, A11, Def2;
then A12: LE q, Last_Point (P,(f /. i),(f /. (i + 1)),Q),P,f /. i,f /. (i + 1) by A5, A7, Def3;
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A4, TOPREAL1:def_3;
hence LE q, Last_Point ((LSeg (f,i)),(f /. i),(f /. (i + 1)),Q),f /. i,f /. (i + 1) by A10, A12, Th17; ::_thesis: verum
end;
Lm4: for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)
let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2)
for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)
let q be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q holds
LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)
let i be Element of NAT ; ::_thesis: ( L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,i) & q in Q implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) )
assume that
A1: L~ f meets Q and
A2: f is being_S-Seq and
A3: Q is closed and
A4: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) and
A5: ( 1 <= i & i + 1 <= len f ) and
A6: ( q in LSeg (f,i) & q in Q ) ; ::_thesis: LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)
len f >= 2 by A2, TOPREAL1:def_8;
then reconsider P = L~ f, R = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A4, TOPREAL1:23;
(LSeg (f,i)) /\ Q <> {} by A6, XBOOLE_0:def_4;
then A7: LSeg (f,i) meets Q by XBOOLE_0:def_7;
Last_Point (P,(f /. 1),(f /. (len f)),Q) = Last_Point (R,(f /. i),(f /. (i + 1)),Q) by A1, A2, A3, A4, A5, Th20;
hence LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) by A2, A3, A5, A6, A7, Lm3; ::_thesis: verum
end;
theorem Th25: :: JORDAN5C:25
for f being FinSequence of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds
LE f /. i,q, L~ f,f /. 1,f /. (len f)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2)
for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds
LE f /. i,q, L~ f,f /. 1,f /. (len f)
let q be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds
LE f /. i,q, L~ f,f /. 1,f /. (len f)
let i be Element of NAT ; ::_thesis: ( f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) implies LE f /. i,q, L~ f,f /. 1,f /. (len f) )
assume that
A1: f is being_S-Seq and
A2: ( 1 <= i & i + 1 <= len f ) and
A3: q in LSeg (f,i) ; ::_thesis: LE f /. i,q, L~ f,f /. 1,f /. (len f)
set p1 = f /. 1;
set p2 = f /. (len f);
set q1 = f /. i;
A4: 2 <= len f by A1, TOPREAL1:def_8;
then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by TOPREAL1:23;
i in dom f by A2, SEQ_4:134;
then A5: f /. i in P by A4, GOBOARD1:1;
A6: for g being Function of I[01],((TOP-REAL 2) | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = q & 0 <= s2 & s2 <= 1 holds
s1 <= s2
proof
let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = q & 0 <= s2 & s2 <= 1 holds
s1 <= s2
let s1, s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = f /. i & 0 <= s1 & s1 <= 1 & g . s2 = q & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume that
A7: g is being_homeomorphism and
A8: ( g . 0 = f /. 1 & g . 1 = f /. (len f) ) and
A9: g . s1 = f /. i and
A10: ( 0 <= s1 & s1 <= 1 ) and
A11: g . s2 = q and
A12: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: s1 <= s2
A13: dom g = [#] I[01] by A7, TOPS_2:def_5
.= the carrier of I[01] ;
then A14: s1 in dom g by A10, BORSUK_1:43;
consider r1, r2 being Real such that
r1 < r2 and
A15: ( 0 <= r1 & r1 <= 1 ) and
0 <= r2 and
r2 <= 1 and
A16: LSeg (f,i) = g .: [.r1,r2.] and
A17: g . r1 = f /. i and
g . r2 = f /. (i + 1) by A1, A2, A7, A8, JORDAN5B:7;
consider r39 being set such that
A18: r39 in dom g and
A19: r39 in [.r1,r2.] and
A20: g . r39 = q by A3, A16, FUNCT_1:def_6;
r39 in { l where l is Real : ( r1 <= l & l <= r2 ) } by A19, RCOMP_1:def_1;
then consider r3 being Real such that
A21: r3 = r39 and
A22: r1 <= r3 and
r3 <= r2 ;
A23: g is one-to-one by A7, TOPS_2:def_5;
A24: r1 in dom g by A15, A13, BORSUK_1:43;
s2 in dom g by A12, A13, BORSUK_1:43;
then s2 = r3 by A11, A18, A20, A21, A23, FUNCT_1:def_4;
hence s1 <= s2 by A9, A17, A22, A24, A14, A23, FUNCT_1:def_4; ::_thesis: verum
end;
q in P by A3, SPPOL_2:17;
hence LE f /. i,q, L~ f,f /. 1,f /. (len f) by A5, A6, Def3; ::_thesis: verum
end;
theorem Th26: :: JORDAN5C:26
for f being FinSequence of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds
LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2)
for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds
LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f)
let q be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) holds
LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f)
let i be Element of NAT ; ::_thesis: ( f is being_S-Seq & 1 <= i & i + 1 <= len f & q in LSeg (f,i) implies LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f) )
assume that
A1: f is being_S-Seq and
A2: ( 1 <= i & i + 1 <= len f ) and
A3: q in LSeg (f,i) ; ::_thesis: LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f)
len f >= 2 by A1, TOPREAL1:def_8;
then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by TOPREAL1:23;
set p1 = f /. 1;
set p2 = f /. (len f);
set q1 = f /. (i + 1);
f /. (i + 1) in LSeg (f,i) by A2, TOPREAL1:21;
then A4: f /. (i + 1) in P by SPPOL_2:17;
A5: for g being Function of I[01],((TOP-REAL 2) | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 holds
s1 <= s2
proof
let g be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 holds
s1 <= s2
let s1, s2 be Real; ::_thesis: ( g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q & 0 <= s1 & s1 <= 1 & g . s2 = f /. (i + 1) & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume that
A6: g is being_homeomorphism and
A7: ( g . 0 = f /. 1 & g . 1 = f /. (len f) ) and
A8: g . s1 = q and
A9: ( 0 <= s1 & s1 <= 1 ) and
A10: g . s2 = f /. (i + 1) and
A11: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: s1 <= s2
A12: dom g = [#] I[01] by A6, TOPS_2:def_5
.= the carrier of I[01] ;
then A13: s2 in dom g by A11, BORSUK_1:43;
consider r1, r2 being Real such that
A14: ( r1 < r2 & 0 <= r1 ) and
r1 <= 1 and
0 <= r2 and
A15: r2 <= 1 and
A16: LSeg (f,i) = g .: [.r1,r2.] and
g . r1 = f /. i and
A17: g . r2 = f /. (i + 1) by A1, A2, A6, A7, JORDAN5B:7;
A18: r2 in dom g by A14, A15, A12, BORSUK_1:43;
consider r39 being set such that
A19: r39 in dom g and
A20: r39 in [.r1,r2.] and
A21: g . r39 = q by A3, A16, FUNCT_1:def_6;
r39 in { l where l is Real : ( r1 <= l & l <= r2 ) } by A20, RCOMP_1:def_1;
then consider r3 being Real such that
A22: r3 = r39 and
r1 <= r3 and
A23: r3 <= r2 ;
A24: g is one-to-one by A6, TOPS_2:def_5;
s1 in dom g by A9, A12, BORSUK_1:43;
then s1 = r3 by A8, A19, A21, A22, A24, FUNCT_1:def_4;
hence s1 <= s2 by A10, A17, A23, A18, A13, A24, FUNCT_1:def_4; ::_thesis: verum
end;
q in P by A3, SPPOL_2:17;
hence LE q,f /. (i + 1), L~ f,f /. 1,f /. (len f) by A4, A5, Def3; ::_thesis: verum
end;
theorem :: JORDAN5C:27
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds
( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) )
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds
( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) )
let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2)
for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds
( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) )
let q be Point of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds
( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) )
let i, j be Element of NAT ; ::_thesis: ( L~ f meets Q & f is being_S-Seq & Q is closed & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q implies ( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) ) )
assume that
A1: L~ f meets Q and
A2: f is being_S-Seq and
A3: Q is closed and
A4: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) and
A5: 1 <= i and
A6: i + 1 <= len f and
A7: q in LSeg (f,j) and
A8: ( 1 <= j & j + 1 <= len f ) and
A9: q in Q and
A10: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q ; ::_thesis: ( i <= j & ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) ) )
reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by A4, SPPOL_2:17;
set q1 = First_Point (P,(f /. 1),(f /. (len f)),Q);
set p1 = f /. i;
A11: q in L~ f by A7, SPPOL_2:17;
thus i <= j ::_thesis: ( i = j implies LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) )
proof
(L~ f) /\ Q is closed by A3, TOPS_1:8;
then A12: LE First_Point (P,(f /. 1),(f /. (len f)),Q),q,P,f /. 1,f /. (len f) by A2, A9, A11, Th15;
A13: LE q,f /. (j + 1),P,f /. 1,f /. (len f) by A2, A7, A8, Th26;
i <= i + 1 by NAT_1:11;
then A14: i <= len f by A6, XXREAL_0:2;
assume j < i ; ::_thesis: contradiction
then A15: j + 1 <= i by NAT_1:13;
1 <= j + 1 by NAT_1:11;
then LE f /. (j + 1),f /. i,P,f /. 1,f /. (len f) by A2, A15, A14, Th24;
then A16: LE q,f /. i,P,f /. 1,f /. (len f) by A13, Th13;
LE f /. i, First_Point (P,(f /. 1),(f /. (len f)),Q),P,f /. 1,f /. (len f) by A2, A4, A5, A6, Th25;
then LE q, First_Point (P,(f /. 1),(f /. (len f)),Q),P,f /. 1,f /. (len f) by A16, Th13;
hence contradiction by A2, A10, A12, Th12, TOPREAL1:25; ::_thesis: verum
end;
assume i = j ; ::_thesis: LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1)
hence LE First_Point ((L~ f),(f /. 1),(f /. (len f)),Q),q,f /. i,f /. (i + 1) by A1, A2, A3, A4, A5, A6, A7, A9, Lm2; ::_thesis: verum
end;
theorem :: JORDAN5C:28
for f being FinSequence of (TOP-REAL 2)
for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds
( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) )
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2)
for q being Point of (TOP-REAL 2)
for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds
( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) )
let Q be Subset of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2)
for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds
( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) )
let q be Point of (TOP-REAL 2); ::_thesis: for i, j being Element of NAT st L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q holds
( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) )
let i, j be Element of NAT ; ::_thesis: ( L~ f meets Q & f is being_S-Seq & Q is closed & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) & 1 <= i & i + 1 <= len f & q in LSeg (f,j) & 1 <= j & j + 1 <= len f & q in Q & Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q implies ( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) ) )
assume that
A1: L~ f meets Q and
A2: f is being_S-Seq and
A3: Q is closed and
A4: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) in LSeg (f,i) and
A5: ( 1 <= i & i + 1 <= len f ) and
A6: q in LSeg (f,j) and
A7: 1 <= j and
A8: j + 1 <= len f and
A9: q in Q and
A10: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) <> q ; ::_thesis: ( i >= j & ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) ) )
reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by A4, SPPOL_2:17;
set q1 = Last_Point (P,(f /. 1),(f /. (len f)),Q);
set p2 = f /. (i + 1);
A11: q in L~ f by A6, SPPOL_2:17;
thus i >= j ::_thesis: ( i = j implies LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) )
proof
assume j > i ; ::_thesis: contradiction
then A12: i + 1 <= j by NAT_1:13;
j <= j + 1 by NAT_1:11;
then ( 1 <= i + 1 & j <= len f ) by A8, NAT_1:11, XXREAL_0:2;
then A13: LE f /. (i + 1),f /. j,P,f /. 1,f /. (len f) by A2, A12, Th24;
LE f /. j,q,P,f /. 1,f /. (len f) by A2, A6, A7, A8, Th25;
then A14: LE f /. (i + 1),q,P,f /. 1,f /. (len f) by A13, Th13;
(L~ f) /\ Q is closed by A3, TOPS_1:8;
then A15: LE q, Last_Point (P,(f /. 1),(f /. (len f)),Q),P,f /. 1,f /. (len f) by A2, A9, A11, Th16;
LE Last_Point (P,(f /. 1),(f /. (len f)),Q),f /. (i + 1),P,f /. 1,f /. (len f) by A2, A4, A5, Th26;
then LE Last_Point (P,(f /. 1),(f /. (len f)),Q),q,P,f /. 1,f /. (len f) by A14, Th13;
hence contradiction by A2, A10, A15, Th12, TOPREAL1:25; ::_thesis: verum
end;
assume i = j ; ::_thesis: LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1)
hence LE q, Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q),f /. i,f /. (i + 1) by A1, A2, A3, A4, A5, A6, A9, Lm4; ::_thesis: verum
end;
theorem Th29: :: JORDAN5C:29
for f being FinSequence of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2)
for i being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) holds
LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for q1, q2 being Point of (TOP-REAL 2)
for i being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) holds
LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)
let q1, q2 be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) holds
LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)
let i be Element of NAT ; ::_thesis: ( q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) implies LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) )
assume that
A1: q1 in LSeg (f,i) and
A2: q2 in LSeg (f,i) and
A3: f is being_S-Seq and
A4: ( 1 <= i & i + 1 <= len f ) ; ::_thesis: ( not LE q1,q2, L~ f,f /. 1,f /. (len f) or LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) )
len f >= 2 by A3, TOPREAL1:def_8;
then reconsider P = L~ f, Q = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:23;
L~ f is_an_arc_of f /. 1,f /. (len f) by A3, TOPREAL1:25;
then consider F being Function of I[01],((TOP-REAL 2) | P) such that
A5: ( F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) ) by TOPREAL1:def_1;
consider ppi, pi1 being Real such that
A6: ppi < pi1 and
A7: 0 <= ppi and
ppi <= 1 and
0 <= pi1 and
A8: pi1 <= 1 and
A9: LSeg (f,i) = F .: [.ppi,pi1.] and
A10: F . ppi = f /. i and
A11: F . pi1 = f /. (i + 1) by A3, A4, A5, JORDAN5B:7;
set Ex = L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)));
A12: L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))) is being_homeomorphism by A6, TREAL_1:17;
then A13: rng (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) = [#] (Closed-Interval-TSpace (ppi,pi1)) by TOPS_2:def_5;
A14: ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A6;
then reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01] by A7, A8, BORSUK_1:40, RCOMP_1:def_1, XXREAL_1:34;
consider G being Function of (I[01] | Poz),((TOP-REAL 2) | Q) such that
A15: G = F | Poz and
A16: G is being_homeomorphism by A3, A4, A5, A9, JORDAN5B:8;
A17: ppi in [.ppi,pi1.] by A14, RCOMP_1:def_1;
set H = G * (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))));
A18: dom G = [#] (I[01] | Poz) by A16, TOPS_2:def_5
.= Poz by PRE_TOPC:def_5
.= [#] (Closed-Interval-TSpace (ppi,pi1)) by A6, TOPMETR:18 ;
then A19: rng (G * (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))))) = rng G by A13, RELAT_1:28
.= [#] ((TOP-REAL 2) | (LSeg (f,i))) by A16, TOPS_2:def_5 ;
pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A6;
then A20: pi1 in [.ppi,pi1.] by RCOMP_1:def_1;
A21: (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . 1 = (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . ((0,1) (#)) by TREAL_1:def_2
.= (ppi,pi1) (#) by A6, TREAL_1:9
.= pi1 by A6, TREAL_1:def_2 ;
A22: dom (G * (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))))) = dom (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) by A13, A18, RELAT_1:27
.= [#] I[01] by A12, TOPMETR:20, TOPS_2:def_5
.= the carrier of I[01] ;
then reconsider H = G * (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) as Function of I[01],((TOP-REAL 2) | Q) by A19, FUNCT_2:2;
q1 in rng H by A1, A19, PRE_TOPC:def_5;
then consider x19 being set such that
A23: x19 in dom H and
A24: q1 = H . x19 by FUNCT_1:def_3;
x19 in { l where l is Real : ( 0 <= l & l <= 1 ) } by A22, A23, BORSUK_1:40, RCOMP_1:def_1;
then consider x1 being Real such that
A25: x1 = x19 and
A26: ( 0 <= x1 & x1 <= 1 ) ;
assume A27: LE q1,q2, L~ f,f /. 1,f /. (len f) ; ::_thesis: LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)
x1 in the carrier of I[01] by A26, BORSUK_1:43;
then x1 in dom (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) by A13, A18, A22, RELAT_1:27;
then (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x1 in the carrier of (Closed-Interval-TSpace (ppi,pi1)) by A13, FUNCT_1:def_3;
then A28: (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x1 in Poz by A6, TOPMETR:18;
1 in dom H by A22, BORSUK_1:43;
then A29: H . 1 = G . pi1 by A21, FUNCT_1:12
.= f /. (i + 1) by A11, A20, A15, FUNCT_1:49 ;
A30: (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . 0 = (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . ((#) (0,1)) by TREAL_1:def_1
.= (#) (ppi,pi1) by A6, TREAL_1:9
.= ppi by A6, TREAL_1:def_1 ;
q2 in rng H by A2, A19, PRE_TOPC:def_5;
then consider x29 being set such that
A31: x29 in dom H and
A32: q2 = H . x29 by FUNCT_1:def_3;
x29 in { l where l is Real : ( 0 <= l & l <= 1 ) } by A22, A31, BORSUK_1:40, RCOMP_1:def_1;
then consider x2 being Real such that
A33: x2 = x29 and
A34: 0 <= x2 and
A35: x2 <= 1 ;
reconsider X1 = x1, X2 = x2 as Point of (Closed-Interval-TSpace (0,1)) by A26, A34, A35, BORSUK_1:43, TOPMETR:20;
x2 in the carrier of I[01] by A34, A35, BORSUK_1:43;
then x2 in dom (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) by A13, A18, A22, RELAT_1:27;
then (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2 in the carrier of (Closed-Interval-TSpace (ppi,pi1)) by A13, FUNCT_1:def_3;
then A36: (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2 in Poz by A6, TOPMETR:18;
then reconsider E1 = (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . X1, E2 = (L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . X2 as Real by A28;
A37: q2 = G . ((L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2) by A31, A32, A33, FUNCT_1:12
.= F . ((L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2) by A15, A36, FUNCT_1:49 ;
reconsider K1 = Closed-Interval-TSpace (ppi,pi1), K2 = I[01] | Poz as SubSpace of I[01] by A6, A7, A8, TOPMETR:20, TREAL_1:3;
A38: ( L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))) is one-to-one & L[01] (((#) (ppi,pi1)),((ppi,pi1) (#))) is continuous ) by A12, TOPS_2:def_5;
the carrier of K1 = [.ppi,pi1.] by A6, TOPMETR:18
.= [#] (I[01] | Poz) by PRE_TOPC:def_5
.= the carrier of K2 ;
then I[01] | Poz = Closed-Interval-TSpace (ppi,pi1) by TSEP_1:5;
then A39: H is being_homeomorphism by A16, A12, TOPMETR:20, TOPS_2:57;
A40: q1 = G . ((L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x1) by A23, A24, A25, FUNCT_1:12
.= F . ((L[01] (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x1) by A15, A28, FUNCT_1:49 ;
A41: ( 0 <= E2 & E2 <= 1 ) by A36, BORSUK_1:43;
0 in dom H by A22, BORSUK_1:43;
then A42: H . 0 = G . ppi by A30, FUNCT_1:12
.= f /. i by A10, A17, A15, FUNCT_1:49 ;
E1 <= 1 by A28, BORSUK_1:43;
then E1 <= E2 by A27, A5, A40, A37, A41, Def3;
then x1 <= x2 by A6, A30, A21, A38, JORDAN5A:15;
hence LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) by A3, A4, A39, A42, A29, A24, A32, A25, A26, A33, A35, Th8, JORDAN5B:15; ::_thesis: verum
end;
theorem :: JORDAN5C:30
for f being FinSequence of (TOP-REAL 2)
for q1, q2 being Point of (TOP-REAL 2) st q1 in L~ f & q2 in L~ f & f is being_S-Seq & q1 <> q2 holds
( LE q1,q2, L~ f,f /. 1,f /. (len f) iff for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) )
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for q1, q2 being Point of (TOP-REAL 2) st q1 in L~ f & q2 in L~ f & f is being_S-Seq & q1 <> q2 holds
( LE q1,q2, L~ f,f /. 1,f /. (len f) iff for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) )
let q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( q1 in L~ f & q2 in L~ f & f is being_S-Seq & q1 <> q2 implies ( LE q1,q2, L~ f,f /. 1,f /. (len f) iff for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ) )
set p3 = f /. 1;
set p4 = f /. (len f);
assume that
A1: q1 in L~ f and
A2: q2 in L~ f and
A3: f is being_S-Seq and
A4: q1 <> q2 ; ::_thesis: ( LE q1,q2, L~ f,f /. 1,f /. (len f) iff for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) )
reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by A1;
hereby ::_thesis: ( ( for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ) implies LE q1,q2, L~ f,f /. 1,f /. (len f) )
assume A5: LE q1,q2, L~ f,f /. 1,f /. (len f) ; ::_thesis: for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) )
thus for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ::_thesis: verum
proof
let i, j be Element of NAT ; ::_thesis: ( q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f implies ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) )
assume that
A6: q1 in LSeg (f,i) and
A7: q2 in LSeg (f,j) and
A8: 1 <= i and
A9: i + 1 <= len f and
A10: ( 1 <= j & j + 1 <= len f ) ; ::_thesis: ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) )
thus i <= j ::_thesis: ( i = j implies LE q1,q2,f /. i,f /. (i + 1) )
proof
assume j < i ; ::_thesis: contradiction
then j + 1 <= i by NAT_1:13;
then consider m being Nat such that
A11: (j + 1) + m = i by NAT_1:10;
A12: LE q2,f /. (j + 1),P,f /. 1,f /. (len f) by A3, A7, A10, Th26;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
A13: ( 1 <= j + 1 & j + 1 <= (j + 1) + m ) by NAT_1:11;
i <= i + 1 by NAT_1:11;
then (j + 1) + m <= len f by A9, A11, XXREAL_0:2;
then LE f /. (j + 1),f /. ((j + 1) + m),P,f /. 1,f /. (len f) by A3, A13, Th24;
then A14: LE q2,f /. ((j + 1) + m),P,f /. 1,f /. (len f) by A12, Th13;
LE f /. ((j + 1) + m),q1,P,f /. 1,f /. (len f) by A3, A6, A8, A9, A11, Th25;
then LE q2,q1,P,f /. 1,f /. (len f) by A14, Th13;
hence contradiction by A3, A4, A5, Th12, TOPREAL1:25; ::_thesis: verum
end;
assume A15: i = j ; ::_thesis: LE q1,q2,f /. i,f /. (i + 1)
A16: f is one-to-one by A3, TOPREAL1:def_8;
set p1 = f /. i;
set p2 = f /. (i + 1);
A17: ( i in dom f & i + 1 in dom f ) by A8, A9, SEQ_4:134;
A18: f /. i <> f /. (i + 1)
proof
assume f /. i = f /. (i + 1) ; ::_thesis: contradiction
then i = i + 1 by A17, A16, PARTFUN2:10;
hence contradiction ; ::_thesis: verum
end;
LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A8, A9, TOPREAL1:def_3;
hence LE q1,q2,f /. i,f /. (i + 1) by A3, A5, A6, A7, A8, A9, A15, A18, Th17, Th29; ::_thesis: verum
end;
end;
consider i being Element of NAT such that
A19: ( 1 <= i & i + 1 <= len f ) and
A20: q1 in LSeg (f,i) by A1, SPPOL_2:13;
consider j being Element of NAT such that
A21: 1 <= j and
A22: j + 1 <= len f and
A23: q2 in LSeg (f,j) by A2, SPPOL_2:13;
assume A24: for i, j being Element of NAT st q1 in LSeg (f,i) & q2 in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ; ::_thesis: LE q1,q2, L~ f,f /. 1,f /. (len f)
then A25: i <= j by A19, A20, A21, A22, A23;
percases ( i < j or i = j ) by A25, XXREAL_0:1;
suppose i < j ; ::_thesis: LE q1,q2, L~ f,f /. 1,f /. (len f)
then i + 1 <= j by NAT_1:13;
then consider m being Nat such that
A26: j = (i + 1) + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
A27: ( 1 <= i + 1 & i + 1 <= (i + 1) + m ) by NAT_1:11;
A28: LE q1,f /. (i + 1),P,f /. 1,f /. (len f) by A3, A19, A20, Th26;
j <= j + 1 by NAT_1:11;
then (i + 1) + m <= len f by A22, A26, XXREAL_0:2;
then LE f /. (i + 1),f /. ((i + 1) + m),P,f /. 1,f /. (len f) by A3, A27, Th24;
then A29: LE q1,f /. ((i + 1) + m),P,f /. 1,f /. (len f) by A28, Th13;
LE f /. ((i + 1) + m),q2,P,f /. 1,f /. (len f) by A3, A21, A22, A23, A26, Th25;
hence LE q1,q2, L~ f,f /. 1,f /. (len f) by A29, Th13; ::_thesis: verum
end;
supposeA30: i = j ; ::_thesis: LE q1,q2, L~ f,f /. 1,f /. (len f)
reconsider Q = LSeg (f,i) as non empty Subset of (TOP-REAL 2) by A20;
set p1 = f /. i;
set p2 = f /. (i + 1);
A31: f is one-to-one by A3, TOPREAL1:def_8;
A32: ( i in dom f & i + 1 in dom f ) by A19, SEQ_4:134;
f /. i <> f /. (i + 1)
proof
assume f /. i = f /. (i + 1) ; ::_thesis: contradiction
then i = i + 1 by A32, A31, PARTFUN2:10;
hence contradiction ; ::_thesis: verum
end;
then consider H being Function of I[01],((TOP-REAL 2) | (LSeg ((f /. i),(f /. (i + 1))))) such that
A33: for x being Real st x in [.0,1.] holds
H . x = ((1 - x) * (f /. i)) + (x * (f /. (i + 1))) and
A34: H is being_homeomorphism and
H . 0 = f /. i and
H . 1 = f /. (i + 1) by JORDAN5A:3;
A35: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A19, TOPREAL1:def_3;
then reconsider H = H as Function of I[01],((TOP-REAL 2) | Q) ;
A36: LE q1,q2,f /. i,f /. (i + 1) by A24, A19, A20, A23, A30;
( q1 in P & q2 in P & ( for g being Function of I[01],((TOP-REAL 2) | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) )
proof
A37: rng H = [#] ((TOP-REAL 2) | (LSeg (f,i))) by A34, A35, TOPS_2:def_5
.= LSeg (f,i) by PRE_TOPC:def_5 ;
then consider x19 being set such that
A38: x19 in dom H and
A39: H . x19 = q1 by A20, FUNCT_1:def_3;
A40: dom H = [#] I[01] by A34, TOPS_2:def_5
.= [.0,1.] by BORSUK_1:40 ;
then x19 in { l where l is Real : ( 0 <= l & l <= 1 ) } by A38, RCOMP_1:def_1;
then consider x1 being Real such that
A41: x1 = x19 and
0 <= x1 and
A42: x1 <= 1 ;
consider x29 being set such that
A43: x29 in dom H and
A44: H . x29 = q2 by A23, A30, A37, FUNCT_1:def_3;
x29 in { l where l is Real : ( 0 <= l & l <= 1 ) } by A40, A43, RCOMP_1:def_1;
then consider x2 being Real such that
A45: x2 = x29 and
A46: ( 0 <= x2 & x2 <= 1 ) ;
A47: q2 = ((1 - x2) * (f /. i)) + (x2 * (f /. (i + 1))) by A33, A40, A43, A44, A45;
q1 = ((1 - x1) * (f /. i)) + (x1 * (f /. (i + 1))) by A33, A40, A38, A39, A41;
then A48: x1 <= x2 by A36, A42, A46, A47, JORDAN3:def_5;
0 in { l where l is Real : ( 0 <= l & l <= 1 ) } ;
then A49: 0 in [.0,1.] by RCOMP_1:def_1;
then A50: H . 0 = ((1 - 0) * (f /. i)) + (0 * (f /. (i + 1))) by A33
.= (f /. i) + (0 * (f /. (i + 1))) by EUCLID:29
.= (f /. i) + (0. (TOP-REAL 2)) by EUCLID:29
.= f /. i by EUCLID:27 ;
thus ( q1 in P & q2 in P ) by A1, A2; ::_thesis: for g being Function of I[01],((TOP-REAL 2) | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2
let F be Function of I[01],((TOP-REAL 2) | P); ::_thesis: for s1, s2 being Real st F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & F . s1 = q1 & 0 <= s1 & s1 <= 1 & F . s2 = q2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2
let s1, s2 be Real; ::_thesis: ( F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & F . s1 = q1 & 0 <= s1 & s1 <= 1 & F . s2 = q2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume that
A51: F is being_homeomorphism and
A52: ( F . 0 = f /. 1 & F . 1 = f /. (len f) ) and
A53: F . s1 = q1 and
A54: ( 0 <= s1 & s1 <= 1 ) and
A55: F . s2 = q2 and
A56: ( 0 <= s2 & s2 <= 1 ) ; ::_thesis: s1 <= s2
consider ppi, pi1 being Real such that
A57: ppi < pi1 and
A58: 0 <= ppi and
ppi <= 1 and
0 <= pi1 and
A59: pi1 <= 1 and
A60: LSeg (f,i) = F .: [.ppi,pi1.] and
A61: F . ppi = f /. i and
A62: F . pi1 = f /. (i + 1) by A3, A19, A51, A52, JORDAN5B:7;
A63: ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A57;
then reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01] by A58, A59, BORSUK_1:40, RCOMP_1:def_1, XXREAL_1:34;
consider G being Function of (I[01] | Poz),((TOP-REAL 2) | Q) such that
A64: G = F | Poz and
A65: G is being_homeomorphism by A3, A19, A51, A52, A60, JORDAN5B:8;
A66: dom F = [#] I[01] by A51, TOPS_2:def_5
.= the carrier of I[01] ;
reconsider K1 = Closed-Interval-TSpace (ppi,pi1), K2 = I[01] | Poz as SubSpace of I[01] by A57, A58, A59, TOPMETR:20, TREAL_1:3;
A67: the carrier of K1 = [.ppi,pi1.] by A57, TOPMETR:18
.= [#] (I[01] | Poz) by PRE_TOPC:def_5
.= the carrier of K2 ;
then reconsider E = (G ") * H as Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (ppi,pi1)) by TOPMETR:20;
A68: G is one-to-one by A65, TOPS_2:def_5;
reconsider X1 = x1, X2 = x2 as Point of (Closed-Interval-TSpace (0,1)) by A40, A38, A41, A43, A45, TOPMETR:18;
A69: G " is being_homeomorphism by A65, TOPS_2:56;
A70: s2 in the carrier of I[01] by A56, BORSUK_1:43;
A71: F is one-to-one by A51, TOPS_2:def_5;
rng G = [#] ((TOP-REAL 2) | (LSeg (f,i))) by A65, TOPS_2:def_5;
then G is onto by FUNCT_2:def_3;
then A72: G " = G " by A68, TOPS_2:def_4;
A73: ex x9 being set st
( x9 in dom F & x9 in [.ppi,pi1.] & q2 = F . x9 ) by A23, A30, A60, FUNCT_1:def_6;
then s2 in Poz by A55, A70, A66, A71, FUNCT_1:def_4;
then A74: G . s2 = q2 by A55, A64, FUNCT_1:49;
dom G = [#] (I[01] | Poz) by A65, TOPS_2:def_5;
then A75: dom G = Poz by PRE_TOPC:def_5;
then s2 in dom G by A55, A70, A66, A71, A73, FUNCT_1:def_4;
then A76: s2 = (G ") . (H . x2) by A44, A45, A68, A72, A74, FUNCT_1:32
.= E . x2 by A43, A45, FUNCT_1:13 ;
then A77: s2 = E . X2 ;
consider x being set such that
A78: x in dom F and
A79: x in [.ppi,pi1.] and
A80: q1 = F . x by A20, A60, FUNCT_1:def_6;
A81: s1 in the carrier of I[01] by A54, BORSUK_1:43;
then x = s1 by A53, A66, A71, A78, A80, FUNCT_1:def_4;
then A82: G . s1 = q1 by A64, A79, A80, FUNCT_1:49;
Closed-Interval-TSpace (ppi,pi1) = I[01] | Poz by A67, TSEP_1:5;
then E is being_homeomorphism by A34, A35, A69, TOPMETR:20, TOPS_2:57;
then A83: ( E is continuous & E is one-to-one ) by TOPS_2:def_5;
1 in { l where l is Real : ( 0 <= l & l <= 1 ) } ;
then A84: 1 in [.0,1.] by RCOMP_1:def_1;
then A85: H . 1 = ((1 - 1) * (f /. i)) + (1 * (f /. (i + 1))) by A33
.= (0. (TOP-REAL 2)) + (1 * (f /. (i + 1))) by EUCLID:29
.= (0. (TOP-REAL 2)) + (f /. (i + 1)) by EUCLID:29
.= f /. (i + 1) by EUCLID:27 ;
s1 in dom G by A53, A81, A66, A71, A75, A79, A80, FUNCT_1:def_4;
then A86: s1 = (G ") . (H . x1) by A39, A41, A68, A72, A82, FUNCT_1:32
.= E . x1 by A38, A41, FUNCT_1:13 ;
then A87: s1 = E . X1 ;
pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A57;
then A88: pi1 in [.ppi,pi1.] by RCOMP_1:def_1;
then G . pi1 = f /. (i + 1) by A62, A64, FUNCT_1:49;
then A89: pi1 = (G ") . (H . 1) by A88, A68, A75, A72, A85, FUNCT_1:32
.= E . 1 by A40, A84, FUNCT_1:13 ;
A90: ppi in [.ppi,pi1.] by A63, RCOMP_1:def_1;
then G . ppi = f /. i by A61, A64, FUNCT_1:49;
then A91: ppi = (G ") . (H . 0) by A90, A68, A75, A72, A50, FUNCT_1:32
.= E . 0 by A40, A49, FUNCT_1:13 ;
percases ( x1 = x2 or x1 < x2 ) by A48, XXREAL_0:1;
suppose x1 = x2 ; ::_thesis: s1 <= s2
hence s1 <= s2 by A86, A76; ::_thesis: verum
end;
suppose x1 < x2 ; ::_thesis: s1 <= s2
hence s1 <= s2 by A57, A83, A91, A89, A87, A77, JORDAN5A:15; ::_thesis: verum
end;
end;
end;
hence LE q1,q2, L~ f,f /. 1,f /. (len f) by Def3; ::_thesis: verum
end;
end;
end;