:: JORDAN_A semantic presentation
begin
theorem Th1: :: JORDAN_A:1
for T being non empty TopSpace
for f being continuous RealMap of T
for A being compact Subset of T holds f .: A is compact
proof
let T be non empty TopSpace; ::_thesis: for f being continuous RealMap of T
for A being compact Subset of T holds f .: A is compact
let f be continuous RealMap of T; ::_thesis: for A being compact Subset of T holds f .: A is compact
let A be compact Subset of T; ::_thesis: f .: A is compact
reconsider g = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17;
[#] (g .: A) is compact by WEIERSTR:9, WEIERSTR:13;
hence f .: A is compact by WEIERSTR:def_1; ::_thesis: verum
end;
theorem Th2: :: JORDAN_A:2
for A being compact Subset of REAL
for B being non empty Subset of REAL st B c= A holds
lower_bound B in A
proof
let A be compact Subset of REAL; ::_thesis: for B being non empty Subset of REAL st B c= A holds
lower_bound B in A
let B be non empty Subset of REAL; ::_thesis: ( B c= A implies lower_bound B in A )
assume A1: B c= A ; ::_thesis: lower_bound B in A
A2: A is real-bounded by RCOMP_1:10;
then A3: B is bounded_below by A1, XXREAL_2:44;
A4: Cl B c= A by A1, MEASURE6:57;
Cl B is bounded_below by A1, A2, MEASURE6:57, XXREAL_2:44;
then lower_bound (Cl B) in Cl B by RCOMP_1:13;
then lower_bound (Cl B) in A by A4;
hence lower_bound B in A by A3, TOPREAL6:68; ::_thesis: verum
end;
theorem :: JORDAN_A:3
for n being Element of NAT
for A, B being non empty compact Subset of (TOP-REAL n)
for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]
for g being RealMap of (TOP-REAL n) st ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: A)
proof
let n be Element of NAT ; ::_thesis: for A, B being non empty compact Subset of (TOP-REAL n)
for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]
for g being RealMap of (TOP-REAL n) st ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: A)
let A, B be non empty compact Subset of (TOP-REAL n); ::_thesis: for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]
for g being RealMap of (TOP-REAL n) st ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: A)
let f be continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]; ::_thesis: for g being RealMap of (TOP-REAL n) st ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: A)
let g be RealMap of (TOP-REAL n); ::_thesis: ( ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) implies lower_bound (f .: [:A,B:]) = lower_bound (g .: A) )
assume A1: for p being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ; ::_thesis: lower_bound (f .: [:A,B:]) = lower_bound (g .: A)
A2: [:A,B:] is compact by BORSUK_3:23;
then A3: f .: [:A,B:] is compact by Th1;
A4: f .: [:A,B:] is real-bounded by A2, Th1, RCOMP_1:10;
A5: g .: A c= f .: [:A,B:]
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in g .: A or u in f .: [:A,B:] )
assume u in g .: A ; ::_thesis: u in f .: [:A,B:]
then consider p being Point of (TOP-REAL n) such that
A6: p in A and
A7: u = g . p by FUNCT_2:65;
consider q being Point of (TOP-REAL n) such that
A8: q in B by SUBSET_1:4;
consider G being Subset of REAL such that
A9: G = { (f . (p,q1)) where q1 is Point of (TOP-REAL n) : q1 in B } and
A10: u = lower_bound G by A1, A7;
A11: f . (p,q) in G by A8, A9;
G c= f .: [:A,B:]
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in G or u in f .: [:A,B:] )
assume u in G ; ::_thesis: u in f .: [:A,B:]
then consider q1 being Point of (TOP-REAL n) such that
A12: u = f . (p,q1) and
A13: q1 in B by A9;
[p,q1] in [:A,B:] by A6, A13, ZFMISC_1:87;
hence u in f .: [:A,B:] by A12, FUNCT_2:35; ::_thesis: verum
end;
hence u in f .: [:A,B:] by A3, A10, A11, Th2; ::_thesis: verum
end;
then A14: g .: A is bounded_below by A4, XXREAL_2:44;
A15: for r being real number st r in f .: [:A,B:] holds
lower_bound (g .: A) <= r
proof
let r be real number ; ::_thesis: ( r in f .: [:A,B:] implies lower_bound (g .: A) <= r )
assume r in f .: [:A,B:] ; ::_thesis: lower_bound (g .: A) <= r
then consider pq being Point of [:(TOP-REAL n),(TOP-REAL n):] such that
A16: pq in [:A,B:] and
A17: r = f . pq by FUNCT_2:65;
pq in the carrier of [:(TOP-REAL n),(TOP-REAL n):] ;
then pq in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] by BORSUK_1:def_2;
then consider p, q being set such that
A18: p in the carrier of (TOP-REAL n) and
A19: q in the carrier of (TOP-REAL n) and
A20: pq = [p,q] by ZFMISC_1:84;
A21: q in B by A16, A20, ZFMISC_1:87;
reconsider p = p, q = q as Point of (TOP-REAL n) by A18, A19;
consider G being Subset of REAL such that
A22: G = { (f . (p,q1)) where q1 is Point of (TOP-REAL n) : q1 in B } and
A23: g . p = lower_bound G by A1;
A24: p in A by A16, A20, ZFMISC_1:87;
G c= f .: [:A,B:]
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in G or u in f .: [:A,B:] )
assume u in G ; ::_thesis: u in f .: [:A,B:]
then consider q1 being Point of (TOP-REAL n) such that
A25: u = f . (p,q1) and
A26: q1 in B by A22;
[p,q1] in [:A,B:] by A24, A26, ZFMISC_1:87;
hence u in f .: [:A,B:] by A25, FUNCT_2:35; ::_thesis: verum
end;
then A27: G is bounded_below by A4, XXREAL_2:44;
r = f . (p,q) by A17, A20;
then r in G by A21, A22;
then A28: g . p <= r by A23, A27, SEQ_4:def_2;
g . p in g .: A by A24, FUNCT_2:35;
then lower_bound (g .: A) <= g . p by A14, SEQ_4:def_2;
hence lower_bound (g .: A) <= r by A28, XXREAL_0:2; ::_thesis: verum
end;
for s being real number st 0 < s holds
ex r being real number st
( r in f .: [:A,B:] & r < (lower_bound (g .: A)) + s )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in f .: [:A,B:] & r < (lower_bound (g .: A)) + s ) )
assume 0 < s ; ::_thesis: ex r being real number st
( r in f .: [:A,B:] & r < (lower_bound (g .: A)) + s )
then consider r being real number such that
A29: r in g .: A and
A30: r < (lower_bound (g .: A)) + s by A14, SEQ_4:def_2;
take r ; ::_thesis: ( r in f .: [:A,B:] & r < (lower_bound (g .: A)) + s )
thus r in f .: [:A,B:] by A5, A29; ::_thesis: r < (lower_bound (g .: A)) + s
thus r < (lower_bound (g .: A)) + s by A30; ::_thesis: verum
end;
hence lower_bound (f .: [:A,B:]) = lower_bound (g .: A) by A4, A15, SEQ_4:def_2; ::_thesis: verum
end;
theorem :: JORDAN_A:4
for n being Element of NAT
for A, B being non empty compact Subset of (TOP-REAL n)
for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]
for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: B)
proof
let n be Element of NAT ; ::_thesis: for A, B being non empty compact Subset of (TOP-REAL n)
for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]
for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: B)
let A, B be non empty compact Subset of (TOP-REAL n); ::_thesis: for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]
for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: B)
let f be continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]; ::_thesis: for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: B)
let g be RealMap of (TOP-REAL n); ::_thesis: ( ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) implies lower_bound (f .: [:A,B:]) = lower_bound (g .: B) )
assume A1: for q being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ; ::_thesis: lower_bound (f .: [:A,B:]) = lower_bound (g .: B)
A2: [:A,B:] is compact by BORSUK_3:23;
then A3: f .: [:A,B:] is compact by Th1;
A4: f .: [:A,B:] is real-bounded by A2, Th1, RCOMP_1:10;
A5: g .: B c= f .: [:A,B:]
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in g .: B or u in f .: [:A,B:] )
assume u in g .: B ; ::_thesis: u in f .: [:A,B:]
then consider q being Point of (TOP-REAL n) such that
A6: q in B and
A7: u = g . q by FUNCT_2:65;
consider p being Point of (TOP-REAL n) such that
A8: p in A by SUBSET_1:4;
consider G being Subset of REAL such that
A9: G = { (f . (p1,q)) where p1 is Point of (TOP-REAL n) : p1 in A } and
A10: u = lower_bound G by A1, A7;
A11: f . (p,q) in G by A8, A9;
G c= f .: [:A,B:]
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in G or u in f .: [:A,B:] )
assume u in G ; ::_thesis: u in f .: [:A,B:]
then consider p1 being Point of (TOP-REAL n) such that
A12: u = f . (p1,q) and
A13: p1 in A by A9;
[p1,q] in [:A,B:] by A6, A13, ZFMISC_1:87;
hence u in f .: [:A,B:] by A12, FUNCT_2:35; ::_thesis: verum
end;
hence u in f .: [:A,B:] by A3, A10, A11, Th2; ::_thesis: verum
end;
then A14: g .: B is bounded_below by A4, XXREAL_2:44;
A15: for r being real number st r in f .: [:A,B:] holds
lower_bound (g .: B) <= r
proof
let r be real number ; ::_thesis: ( r in f .: [:A,B:] implies lower_bound (g .: B) <= r )
assume r in f .: [:A,B:] ; ::_thesis: lower_bound (g .: B) <= r
then consider pq being Point of [:(TOP-REAL n),(TOP-REAL n):] such that
A16: pq in [:A,B:] and
A17: r = f . pq by FUNCT_2:65;
pq in the carrier of [:(TOP-REAL n),(TOP-REAL n):] ;
then pq in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] by BORSUK_1:def_2;
then consider p, q being set such that
A18: p in the carrier of (TOP-REAL n) and
A19: q in the carrier of (TOP-REAL n) and
A20: pq = [p,q] by ZFMISC_1:84;
A21: p in A by A16, A20, ZFMISC_1:87;
reconsider p = p, q = q as Point of (TOP-REAL n) by A18, A19;
consider G being Subset of REAL such that
A22: G = { (f . (p1,q)) where p1 is Point of (TOP-REAL n) : p1 in A } and
A23: g . q = lower_bound G by A1;
A24: q in B by A16, A20, ZFMISC_1:87;
G c= f .: [:A,B:]
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in G or u in f .: [:A,B:] )
assume u in G ; ::_thesis: u in f .: [:A,B:]
then consider p1 being Point of (TOP-REAL n) such that
A25: u = f . (p1,q) and
A26: p1 in A by A22;
[p1,q] in [:A,B:] by A24, A26, ZFMISC_1:87;
hence u in f .: [:A,B:] by A25, FUNCT_2:35; ::_thesis: verum
end;
then A27: G is bounded_below by A4, XXREAL_2:44;
r = f . (p,q) by A17, A20;
then r in G by A21, A22;
then A28: g . q <= r by A23, A27, SEQ_4:def_2;
g . q in g .: B by A24, FUNCT_2:35;
then lower_bound (g .: B) <= g . q by A14, SEQ_4:def_2;
hence lower_bound (g .: B) <= r by A28, XXREAL_0:2; ::_thesis: verum
end;
for s being real number st 0 < s holds
ex r being real number st
( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s ) )
assume 0 < s ; ::_thesis: ex r being real number st
( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )
then consider r being real number such that
A29: r in g .: B and
A30: r < (lower_bound (g .: B)) + s by A14, SEQ_4:def_2;
take r ; ::_thesis: ( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )
thus r in f .: [:A,B:] by A5, A29; ::_thesis: r < (lower_bound (g .: B)) + s
thus r < (lower_bound (g .: B)) + s by A30; ::_thesis: verum
end;
hence lower_bound (f .: [:A,B:]) = lower_bound (g .: B) by A4, A15, SEQ_4:def_2; ::_thesis: verum
end;
theorem Th5: :: JORDAN_A:5
for C being Simple_closed_curve
for q being Point of (TOP-REAL 2) st q in Lower_Arc C & q <> W-min C holds
LE E-max C,q,C
proof
let C be Simple_closed_curve; ::_thesis: for q being Point of (TOP-REAL 2) st q in Lower_Arc C & q <> W-min C holds
LE E-max C,q,C
let q be Point of (TOP-REAL 2); ::_thesis: ( q in Lower_Arc C & q <> W-min C implies LE E-max C,q,C )
E-max C in Upper_Arc C by JORDAN7:1;
hence ( q in Lower_Arc C & q <> W-min C implies LE E-max C,q,C ) by JORDAN6:def_10; ::_thesis: verum
end;
theorem Th6: :: JORDAN_A:6
for C being Simple_closed_curve
for q being Point of (TOP-REAL 2) st q in Upper_Arc C holds
LE q, E-max C,C
proof
let C be Simple_closed_curve; ::_thesis: for q being Point of (TOP-REAL 2) st q in Upper_Arc C holds
LE q, E-max C,C
let q be Point of (TOP-REAL 2); ::_thesis: ( q in Upper_Arc C implies LE q, E-max C,C )
A1: E-max C in Lower_Arc C by JORDAN7:1;
E-max C <> W-min C by TOPREAL5:19;
hence ( q in Upper_Arc C implies LE q, E-max C,C ) by A1, JORDAN6:def_10; ::_thesis: verum
end;
begin
definition
let n be Element of NAT ;
A1: [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] = the carrier of [:(TOP-REAL n),(TOP-REAL n):] by BORSUK_1:def_2;
func Eucl_dist n -> RealMap of [:(TOP-REAL n),(TOP-REAL n):] means :Def1: :: JORDAN_A:def 1
for p, q being Point of (TOP-REAL n) holds it . (p,q) = |.(p - q).|;
existence
ex b1 being RealMap of [:(TOP-REAL n),(TOP-REAL n):] st
for p, q being Point of (TOP-REAL n) holds b1 . (p,q) = |.(p - q).|
proof
deffunc H1( Point of (TOP-REAL n), Point of (TOP-REAL n)) -> Element of REAL = |.($1 - $2).|;
A2: for p, q being Point of (TOP-REAL n) holds H1(p,q) in REAL ;
consider f being Function of [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):],REAL such that
A3: for p, q being Point of (TOP-REAL n) holds f . (p,q) = H1(p,q) from FUNCT_7:sch_1(A2);
reconsider f = f as RealMap of [:(TOP-REAL n),(TOP-REAL n):] by A1;
take f ; ::_thesis: for p, q being Point of (TOP-REAL n) holds f . (p,q) = |.(p - q).|
let p, q be Point of (TOP-REAL n); ::_thesis: f . (p,q) = |.(p - q).|
thus f . (p,q) = |.(p - q).| by A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL n),(TOP-REAL n):] st ( for p, q being Point of (TOP-REAL n) holds b1 . (p,q) = |.(p - q).| ) & ( for p, q being Point of (TOP-REAL n) holds b2 . (p,q) = |.(p - q).| ) holds
b1 = b2
proof
let IT1, IT2 be RealMap of [:(TOP-REAL n),(TOP-REAL n):]; ::_thesis: ( ( for p, q being Point of (TOP-REAL n) holds IT1 . (p,q) = |.(p - q).| ) & ( for p, q being Point of (TOP-REAL n) holds IT2 . (p,q) = |.(p - q).| ) implies IT1 = IT2 )
assume that
A4: for p, q being Point of (TOP-REAL n) holds IT1 . (p,q) = |.(p - q).| and
A5: for p, q being Point of (TOP-REAL n) holds IT2 . (p,q) = |.(p - q).| ; ::_thesis: IT1 = IT2
now__::_thesis:_for_p,_q_being_Point_of_(TOP-REAL_n)_holds_IT1_._(p,q)_=_IT2_._(p,q)
let p, q be Point of (TOP-REAL n); ::_thesis: IT1 . (p,q) = IT2 . (p,q)
thus IT1 . (p,q) = |.(p - q).| by A4
.= IT2 . (p,q) by A5 ; ::_thesis: verum
end;
hence IT1 = IT2 by A1, BINOP_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines Eucl_dist JORDAN_A:def_1_:_
for n being Element of NAT
for b2 being RealMap of [:(TOP-REAL n),(TOP-REAL n):] holds
( b2 = Eucl_dist n iff for p, q being Point of (TOP-REAL n) holds b2 . (p,q) = |.(p - q).| );
definition
let T be non empty TopSpace;
let f be RealMap of T;
redefine attr f is continuous means :: JORDAN_A:def 2
for p being Point of T
for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N;
compatibility
( f is continuous iff for p being Point of T
for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N )
proof
thus ( f is continuous implies for p being Point of T
for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N ) ::_thesis: ( ( for p being Point of T
for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N ) implies f is continuous )
proof
assume A1: f is continuous ; ::_thesis: for p being Point of T
for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N
let p be Point of T; ::_thesis: for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N
let N be Neighbourhood of f . p; ::_thesis: ex V being a_neighborhood of p st f .: V c= N
A2: f " (N `) = (f " N) ` by FUNCT_2:100;
N ` is closed by RCOMP_1:def_5;
then f " (N `) is closed by A1, PSCOMP_1:def_3;
then A3: f " N is open by A2, TOPS_1:4;
f . p in N by RCOMP_1:16;
then p in f " N by FUNCT_2:38;
then reconsider V = f " N as a_neighborhood of p by A3, CONNSP_2:3;
take V ; ::_thesis: f .: V c= N
thus f .: V c= N by FUNCT_1:75; ::_thesis: verum
end;
assume A4: for p being Point of T
for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N ; ::_thesis: f is continuous
let Y be Subset of REAL; :: according to PSCOMP_1:def_3 ::_thesis: ( not Y is closed or f " Y is closed )
assume Y is closed ; ::_thesis: f " Y is closed
then (Y `) ` is closed ;
then A5: Y ` is open by RCOMP_1:def_5;
for p being Point of T st p in (f " Y) ` holds
ex A being Subset of T st
( A is a_neighborhood of p & A c= (f " Y) ` )
proof
let p be Point of T; ::_thesis: ( p in (f " Y) ` implies ex A being Subset of T st
( A is a_neighborhood of p & A c= (f " Y) ` ) )
assume p in (f " Y) ` ; ::_thesis: ex A being Subset of T st
( A is a_neighborhood of p & A c= (f " Y) ` )
then p in f " (Y `) by FUNCT_2:100;
then f . p in Y ` by FUNCT_2:38;
then consider N being Neighbourhood of f . p such that
A6: N c= Y ` by A5, RCOMP_1:18;
consider V being a_neighborhood of p such that
A7: f .: V c= N by A4;
take V ; ::_thesis: ( V is a_neighborhood of p & V c= (f " Y) ` )
thus V is a_neighborhood of p ; ::_thesis: V c= (f " Y) `
f .: V c= Y ` by A6, A7, XBOOLE_1:1;
then A8: f " (f .: V) c= f " (Y `) by RELAT_1:143;
V c= f " (f .: V) by FUNCT_2:42;
then V c= f " (Y `) by A8, XBOOLE_1:1;
hence V c= (f " Y) ` by FUNCT_2:100; ::_thesis: verum
end;
then (f " Y) ` is open by CONNSP_2:7;
then ((f " Y) `) ` is closed by TOPS_1:4;
hence f " Y is closed ; ::_thesis: verum
end;
end;
:: deftheorem defines continuous JORDAN_A:def_2_:_
for T being non empty TopSpace
for f being RealMap of T holds
( f is continuous iff for p being Point of T
for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N );
Lm1: for X, Y being TopSpace holds TopStruct(# the carrier of [:X,Y:], the topology of [:X,Y:] #) = [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):]
proof
let X, Y be TopSpace; ::_thesis: TopStruct(# the carrier of [:X,Y:], the topology of [:X,Y:] #) = [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):]
set T = [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):];
A1: the carrier of [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] = [: the carrier of TopStruct(# the carrier of X, the topology of X #), the carrier of TopStruct(# the carrier of Y, the topology of Y #):] by BORSUK_1:def_2
.= the carrier of [:X,Y:] by BORSUK_1:def_2 ;
set tau1 = { (union A) where A is Subset-Family of [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] : A c= { [:X1,Y1:] where X1 is Subset of TopStruct(# the carrier of X, the topology of X #), Y1 is Subset of TopStruct(# the carrier of Y, the topology of Y #) : ( X1 in the topology of TopStruct(# the carrier of X, the topology of X #) & Y1 in the topology of TopStruct(# the carrier of Y, the topology of Y #) ) } } ;
set tau2 = { (union A) where A is Subset-Family of [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } ;
the topology of [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] = { (union A) where A is Subset-Family of [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] : A c= { [:X1,Y1:] where X1 is Subset of TopStruct(# the carrier of X, the topology of X #), Y1 is Subset of TopStruct(# the carrier of Y, the topology of Y #) : ( X1 in the topology of TopStruct(# the carrier of X, the topology of X #) & Y1 in the topology of TopStruct(# the carrier of Y, the topology of Y #) ) } } by BORSUK_1:def_2
.= { (union A) where A is Subset-Family of [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } }
.= the topology of [:X,Y:] by A1, BORSUK_1:def_2 ;
hence TopStruct(# the carrier of [:X,Y:], the topology of [:X,Y:] #) = [:TopStruct(# the carrier of X, the topology of X #),TopStruct(# the carrier of Y, the topology of Y #):] by A1; ::_thesis: verum
end;
registration
let n be Element of NAT ;
cluster Eucl_dist n -> continuous ;
coherence
Eucl_dist n is continuous
proof
set f = Eucl_dist n;
let p be Point of [:(TOP-REAL n),(TOP-REAL n):]; :: according to JORDAN_A:def_2 ::_thesis: for N being Neighbourhood of (Eucl_dist n) . p ex V being a_neighborhood of p st (Eucl_dist n) .: V c= N
let N be Neighbourhood of (Eucl_dist n) . p; ::_thesis: ex V being a_neighborhood of p st (Eucl_dist n) .: V c= N
consider r being real number such that
A1: 0 < r and
A2: N = ].(((Eucl_dist n) . p) - r),(((Eucl_dist n) . p) + r).[ by RCOMP_1:def_6;
p in the carrier of [:(TOP-REAL n),(TOP-REAL n):] ;
then p in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] by BORSUK_1:def_2;
then consider p1, p2 being set such that
A3: p1 in the carrier of (TOP-REAL n) and
A4: p2 in the carrier of (TOP-REAL n) and
A5: p = [p1,p2] by ZFMISC_1:84;
reconsider p1 = p1, p2 = p2 as Point of (TOP-REAL n) by A3, A4;
reconsider p19 = p1, p29 = p2 as Element of (Euclid n) by TOPREAL3:8;
A6: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider q1 = p1, q2 = p2 as Point of (TopSpaceMetr (Euclid n)) ;
reconsider U = Ball (p19,(r / 2)) as a_neighborhood of q1 by A1, GOBOARD6:91, XREAL_1:215;
reconsider W = Ball (p29,(r / 2)) as a_neighborhood of q2 by A1, GOBOARD6:91, XREAL_1:215;
reconsider V = [:U,W:] as a_neighborhood of p by A5, A6, Lm1;
take V ; ::_thesis: (Eucl_dist n) .: V c= N
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in (Eucl_dist n) .: V or s in N )
assume A7: s in (Eucl_dist n) .: V ; ::_thesis: s in N
then reconsider s = s as Real ;
consider q being Point of [:(TOP-REAL n),(TOP-REAL n):] such that
A8: q in V and
A9: (Eucl_dist n) . q = s by A7, FUNCT_2:65;
q in the carrier of [:(TOP-REAL n),(TOP-REAL n):] ;
then q in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] by BORSUK_1:def_2;
then consider q1, q2 being set such that
A10: q1 in the carrier of (TOP-REAL n) and
A11: q2 in the carrier of (TOP-REAL n) and
A12: q = [q1,q2] by ZFMISC_1:84;
reconsider q1 = q1, q2 = q2 as Point of (TOP-REAL n) by A10, A11;
reconsider q19 = q1, q29 = q2 as Element of (Euclid n) by TOPREAL3:8;
reconsider q199 = q19, q299 = q29, p199 = p19, p299 = p29 as Element of REAL n ;
A13: q19 in Ball (p19,(r / 2)) by A8, A12, ZFMISC_1:87;
A14: q29 in Ball (p29,(r / 2)) by A8, A12, ZFMISC_1:87;
A15: dist (q19,p19) < r / 2 by A13, METRIC_1:11;
A16: dist (q29,p29) < r / 2 by A14, METRIC_1:11;
A17: |.(q1 - p1).| < r / 2 by A15, SPPOL_1:5;
|.(q2 - p2).| < r / 2 by A16, SPPOL_1:5;
then A18: |.(q1 - p1).| + |.(q2 - p2).| < (r / 2) + (r / 2) by A17, XREAL_1:8;
A19: for p, q being Point of (TOP-REAL n) holds (Eucl_dist n) . [p,q] = |.(p - q).|
proof
let p, q be Point of (TOP-REAL n); ::_thesis: (Eucl_dist n) . [p,q] = |.(p - q).|
thus (Eucl_dist n) . [p,q] = (Eucl_dist n) . (p,q)
.= |.(p - q).| by Def1 ; ::_thesis: verum
end;
then A20: (Eucl_dist n) . p = |.(p1 - p2).| by A5;
A21: s = |.(q1 - q2).| by A9, A12, A19;
A22: (q1 - q2) - (p1 - p2) = ((q1 - q2) - p1) + p2 by EUCLID:47
.= (q1 - (q2 + p1)) + p2 by EUCLID:46
.= ((q1 - p1) - q2) + p2 by EUCLID:46
.= (q1 - p1) - (q2 - p2) by EUCLID:47 ;
A23: |.((q1 - p1) - (q2 - p2)).| <= |.(q1 - p1).| + |.(q2 - p2).| by TOPRNS_1:30;
A24: s - ((Eucl_dist n) . p) <= |.((q1 - q2) - (p1 - p2)).| by A20, A21, TOPRNS_1:32;
((Eucl_dist n) . p) - s <= |.((p1 - p2) - (q1 - q2)).| by A20, A21, TOPRNS_1:32;
then ((Eucl_dist n) . p) - s <= |.((q1 - q2) - (p1 - p2)).| by TOPRNS_1:27;
then ((Eucl_dist n) . p) - s <= |.(q1 - p1).| + |.(q2 - p2).| by A22, A23, XXREAL_0:2;
then ((Eucl_dist n) . p) - s < r by A18, XXREAL_0:2;
then A25: ((Eucl_dist n) . p) - r < s by XREAL_1:11;
s - ((Eucl_dist n) . p) <= |.(q1 - p1).| + |.(q2 - p2).| by A22, A23, A24, XXREAL_0:2;
then s - ((Eucl_dist n) . p) < r by A18, XXREAL_0:2;
then s < ((Eucl_dist n) . p) + r by XREAL_1:19;
hence s in N by A2, A25, XXREAL_1:4; ::_thesis: verum
end;
end;
begin
theorem Th7: :: JORDAN_A:7
for n being Element of NAT
for A, B being non empty compact Subset of (TOP-REAL n) st A misses B holds
dist_min (A,B) > 0
proof
let n be Element of NAT ; ::_thesis: for A, B being non empty compact Subset of (TOP-REAL n) st A misses B holds
dist_min (A,B) > 0
let A, B be non empty compact Subset of (TOP-REAL n); ::_thesis: ( A misses B implies dist_min (A,B) > 0 )
assume A1: A misses B ; ::_thesis: dist_min (A,B) > 0
A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
consider A9, B9 being Subset of (TopSpaceMetr (Euclid n)) such that
A3: A = A9 and
A4: B = B9 and
A5: dist_min (A,B) = min_dist_min (A9,B9) by JORDAN1K:def_1;
A6: A9 is compact by A2, A3, COMPTS_1:23;
B9 is compact by A2, A4, COMPTS_1:23;
hence dist_min (A,B) > 0 by A1, A3, A4, A5, A6, JGRAPH_1:38; ::_thesis: verum
end;
begin
theorem Th8: :: JORDAN_A:8
for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE q, E-max C,C & p <> q holds
Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q)
proof
let C be Simple_closed_curve; ::_thesis: for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE q, E-max C,C & p <> q holds
Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q)
let p, q be Point of (TOP-REAL 2); ::_thesis: ( LE p,q,C & LE q, E-max C,C & p <> q implies Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q) )
assume that
A1: LE p,q,C and
A2: LE q, E-max C,C and
A3: p <> q ; ::_thesis: Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q)
A4: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
A5: LE p, E-max C,C by A1, A2, JORDAN6:58;
A6: p in Upper_Arc C by A1, A2, JORDAN17:3, JORDAN6:58;
A7: q in Upper_Arc C by A2, JORDAN17:3;
A8: Upper_Arc C c= C by JORDAN6:61;
A9: now__::_thesis:_not_q_=_W-min_C
assume q = W-min C ; ::_thesis: contradiction
then LE q,p,C by A6, A8, JORDAN7:3;
hence contradiction by A1, A3, JORDAN6:57; ::_thesis: verum
end;
defpred S1[ Point of (TOP-REAL 2)] means ( LE p,$1,C & LE $1,q,C );
defpred S2[ Point of (TOP-REAL 2)] means ( LE p,$1, Upper_Arc C, W-min C, E-max C & LE $1,q, Upper_Arc C, W-min C, E-max C );
A10: for p1 being Point of (TOP-REAL 2) holds
( S1[p1] iff S2[p1] )
proof
let p1 be Point of (TOP-REAL 2); ::_thesis: ( S1[p1] iff S2[p1] )
hereby ::_thesis: ( S2[p1] implies S1[p1] )
assume that
A11: LE p,p1,C and
A12: LE p1,q,C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C & LE p1,q, Upper_Arc C, W-min C, E-max C )
hereby ::_thesis: LE p1,q, Upper_Arc C, W-min C, E-max C
percases ( p1 = E-max C or p1 = W-min C or ( p1 <> E-max C & p1 <> W-min C ) ) ;
suppose p1 = E-max C ; ::_thesis: LE p,p1, Upper_Arc C, W-min C, E-max C
hence LE p,p1, Upper_Arc C, W-min C, E-max C by A4, A6, JORDAN5C:10; ::_thesis: verum
end;
suppose p1 = W-min C ; ::_thesis: LE p,p1, Upper_Arc C, W-min C, E-max C
then LE p1,p,C by A6, A8, JORDAN7:3;
then p = p1 by A11, JORDAN6:57;
hence LE p,p1, Upper_Arc C, W-min C, E-max C by A5, JORDAN17:3, JORDAN5C:9; ::_thesis: verum
end;
supposethat A13: p1 <> E-max C and
A14: p1 <> W-min C ; ::_thesis: LE p,p1, Upper_Arc C, W-min C, E-max C
now__::_thesis:_not_p1_in_Lower_Arc_C
assume A15: p1 in Lower_Arc C ; ::_thesis: contradiction
p1 in Upper_Arc C by A2, A12, JORDAN17:3, JORDAN6:58;
then p1 in (Upper_Arc C) /\ (Lower_Arc C) by A15, XBOOLE_0:def_4;
then p1 in {(W-min C),(E-max C)} by JORDAN6:50;
hence contradiction by A13, A14, TARSKI:def_2; ::_thesis: verum
end;
hence LE p,p1, Upper_Arc C, W-min C, E-max C by A11, JORDAN6:def_10; ::_thesis: verum
end;
end;
end;
percases ( q = E-max C or q <> E-max C ) ;
supposeA16: q = E-max C ; ::_thesis: LE p1,q, Upper_Arc C, W-min C, E-max C
then p1 in Upper_Arc C by A12, JORDAN17:3;
hence LE p1,q, Upper_Arc C, W-min C, E-max C by A4, A16, JORDAN5C:10; ::_thesis: verum
end;
supposeA17: q <> E-max C ; ::_thesis: LE p1,q, Upper_Arc C, W-min C, E-max C
now__::_thesis:_not_q_in_Lower_Arc_C
assume q in Lower_Arc C ; ::_thesis: contradiction
then q in (Upper_Arc C) /\ (Lower_Arc C) by A7, XBOOLE_0:def_4;
then q in {(W-min C),(E-max C)} by JORDAN6:50;
hence contradiction by A9, A17, TARSKI:def_2; ::_thesis: verum
end;
hence LE p1,q, Upper_Arc C, W-min C, E-max C by A12, JORDAN6:def_10; ::_thesis: verum
end;
end;
end;
assume that
A18: LE p,p1, Upper_Arc C, W-min C, E-max C and
A19: LE p1,q, Upper_Arc C, W-min C, E-max C ; ::_thesis: S1[p1]
A20: p1 in Upper_Arc C by A18, JORDAN5C:def_3;
hence LE p,p1,C by A6, A18, JORDAN6:def_10; ::_thesis: LE p1,q,C
thus LE p1,q,C by A7, A19, A20, JORDAN6:def_10; ::_thesis: verum
end;
deffunc H1( set ) -> set = $1;
set X = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } ;
set Y = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } ;
A21: { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } from FRAENKEL:sch_3(A10);
Segment (p,q,C) = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } by A9, JORDAN7:def_1;
hence Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q) by A21, JORDAN6:26; ::_thesis: verum
end;
theorem Th9: :: JORDAN_A:9
for C being Simple_closed_curve
for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds
Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q)
proof
let C be Simple_closed_curve; ::_thesis: for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds
Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q)
let q be Point of (TOP-REAL 2); ::_thesis: ( LE E-max C,q,C implies Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q) )
set p = E-max C;
assume A1: LE E-max C,q,C ; ::_thesis: Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q)
A2: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
A3: E-max C in Lower_Arc C by JORDAN7:1;
A4: q in Lower_Arc C by A1, JORDAN17:4;
A5: Lower_Arc C c= C by JORDAN6:61;
A6: now__::_thesis:_not_q_=_W-min_C
assume A7: q = W-min C ; ::_thesis: contradiction
then E-max C = q by A1, JORDAN7:2;
hence contradiction by A7, TOPREAL5:19; ::_thesis: verum
end;
defpred S1[ Point of (TOP-REAL 2)] means ( LE E-max C,$1,C & LE $1,q,C );
defpred S2[ Point of (TOP-REAL 2)] means ( LE E-max C,$1, Lower_Arc C, E-max C, W-min C & LE $1,q, Lower_Arc C, E-max C, W-min C );
A8: for p1 being Point of (TOP-REAL 2) holds
( S1[p1] iff S2[p1] )
proof
let p1 be Point of (TOP-REAL 2); ::_thesis: ( S1[p1] iff S2[p1] )
hereby ::_thesis: ( S2[p1] implies S1[p1] )
assume that
A9: LE E-max C,p1,C and
A10: LE p1,q,C ; ::_thesis: ( LE E-max C,p1, Lower_Arc C, E-max C, W-min C & LE p1,q, Lower_Arc C, E-max C, W-min C )
A11: p1 in Lower_Arc C by A9, JORDAN17:4;
hence LE E-max C,p1, Lower_Arc C, E-max C, W-min C by A2, JORDAN5C:10; ::_thesis: LE p1,q, Lower_Arc C, E-max C, W-min C
percases ( p1 = E-max C or p1 <> E-max C ) ;
supposeA12: p1 = E-max C ; ::_thesis: LE p1,q, Lower_Arc C, E-max C, W-min C
then q in Lower_Arc C by A10, JORDAN17:4;
hence LE p1,q, Lower_Arc C, E-max C, W-min C by A2, A12, JORDAN5C:10; ::_thesis: verum
end;
supposeA13: p1 <> E-max C ; ::_thesis: LE p1,q, Lower_Arc C, E-max C, W-min C
A14: now__::_thesis:_not_p1_=_W-min_C
assume A15: p1 = W-min C ; ::_thesis: contradiction
then LE p1, E-max C,C by A3, A5, JORDAN7:3;
hence contradiction by A9, A15, JORDAN6:57, TOPREAL5:19; ::_thesis: verum
end;
now__::_thesis:_not_p1_in_Upper_Arc_C
assume p1 in Upper_Arc C ; ::_thesis: contradiction
then p1 in (Upper_Arc C) /\ (Lower_Arc C) by A11, XBOOLE_0:def_4;
then p1 in {(W-min C),(E-max C)} by JORDAN6:50;
hence contradiction by A13, A14, TARSKI:def_2; ::_thesis: verum
end;
hence LE p1,q, Lower_Arc C, E-max C, W-min C by A10, JORDAN6:def_10; ::_thesis: verum
end;
end;
end;
assume that
A16: LE E-max C,p1, Lower_Arc C, E-max C, W-min C and
A17: LE p1,q, Lower_Arc C, E-max C, W-min C ; ::_thesis: S1[p1]
A18: p1 in Lower_Arc C by A16, JORDAN5C:def_3;
p1 <> W-min C by A2, A6, A17, JORDAN6:55;
hence LE E-max C,p1,C by A3, A16, A18, JORDAN6:def_10; ::_thesis: LE p1,q,C
thus LE p1,q,C by A4, A6, A17, A18, JORDAN6:def_10; ::_thesis: verum
end;
deffunc H1( set ) -> set = $1;
set X = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } ;
set Y = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } ;
A19: { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } from FRAENKEL:sch_3(A8);
Segment ((E-max C),q,C) = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } by A6, JORDAN7:def_1;
hence Segment ((E-max C),q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q) by A19, JORDAN6:26; ::_thesis: verum
end;
theorem Th10: :: JORDAN_A:10
for C being Simple_closed_curve
for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds
Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C))
proof
let C be Simple_closed_curve; ::_thesis: for q being Point of (TOP-REAL 2) st LE E-max C,q,C holds
Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C))
let q be Point of (TOP-REAL 2); ::_thesis: ( LE E-max C,q,C implies Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C)) )
set p = W-min C;
assume A1: LE E-max C,q,C ; ::_thesis: Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C))
A2: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
A3: W-min C in Lower_Arc C by JORDAN7:1;
A4: q in Lower_Arc C by A1, JORDAN17:4;
A5: Lower_Arc C c= C by JORDAN6:61;
defpred S1[ Point of (TOP-REAL 2)] means ( LE q,$1,C or ( q in C & $1 = W-min C ) );
defpred S2[ Point of (TOP-REAL 2)] means ( LE q,$1, Lower_Arc C, E-max C, W-min C & LE $1, W-min C, Lower_Arc C, E-max C, W-min C );
A6: for p1 being Point of (TOP-REAL 2) holds
( S1[p1] iff S2[p1] )
proof
let p1 be Point of (TOP-REAL 2); ::_thesis: ( S1[p1] iff S2[p1] )
hereby ::_thesis: ( S2[p1] implies S1[p1] )
assume A7: ( LE q,p1,C or ( q in C & p1 = W-min C ) ) ; ::_thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )
percases ( ( q = E-max C & LE q,p1,C ) or ( q <> E-max C & LE q,p1,C ) or ( q in C & p1 = W-min C ) ) by A7;
supposethat A8: q = E-max C and
A9: LE q,p1,C ; ::_thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )
A10: p1 in Lower_Arc C by A8, A9, JORDAN17:4;
hence LE q,p1, Lower_Arc C, E-max C, W-min C by A2, A8, JORDAN5C:10; ::_thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min C
thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by A2, A10, JORDAN5C:10; ::_thesis: verum
end;
supposethat A11: q <> E-max C and
A12: LE q,p1,C ; ::_thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )
A13: p1 in Lower_Arc C by A1, A12, JORDAN17:4, JORDAN6:58;
A14: now__::_thesis:_not_q_=_W-min_C
assume A15: q = W-min C ; ::_thesis: contradiction
then LE q, E-max C,C by JORDAN7:3, SPRECT_1:14;
hence contradiction by A1, A15, JORDAN6:57, TOPREAL5:19; ::_thesis: verum
end;
now__::_thesis:_not_q_in_Upper_Arc_C
assume q in Upper_Arc C ; ::_thesis: contradiction
then q in (Upper_Arc C) /\ (Lower_Arc C) by A4, XBOOLE_0:def_4;
then q in {(E-max C),(W-min C)} by JORDAN6:def_9;
hence contradiction by A11, A14, TARSKI:def_2; ::_thesis: verum
end;
hence LE q,p1, Lower_Arc C, E-max C, W-min C by A12, JORDAN6:def_10; ::_thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min C
thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by A2, A13, JORDAN5C:10; ::_thesis: verum
end;
supposethat q in C and
A16: p1 = W-min C ; ::_thesis: ( LE q,p1, Lower_Arc C, E-max C, W-min C & LE p1, W-min C, Lower_Arc C, E-max C, W-min C )
thus LE q,p1, Lower_Arc C, E-max C, W-min C by A2, A4, A16, JORDAN5C:10; ::_thesis: LE p1, W-min C, Lower_Arc C, E-max C, W-min C
thus LE p1, W-min C, Lower_Arc C, E-max C, W-min C by A3, A16, JORDAN5C:9; ::_thesis: verum
end;
end;
end;
assume that
A17: LE q,p1, Lower_Arc C, E-max C, W-min C and
LE p1, W-min C, Lower_Arc C, E-max C, W-min C ; ::_thesis: S1[p1]
A18: p1 in Lower_Arc C by A17, JORDAN5C:def_3;
A19: q in Lower_Arc C by A17, JORDAN5C:def_3;
percases ( p1 <> W-min C or p1 = W-min C ) ;
suppose p1 <> W-min C ; ::_thesis: S1[p1]
hence S1[p1] by A17, A18, A19, JORDAN6:def_10; ::_thesis: verum
end;
suppose p1 = W-min C ; ::_thesis: S1[p1]
hence S1[p1] by A4, A5; ::_thesis: verum
end;
end;
end;
deffunc H1( set ) -> set = $1;
set X = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } ;
set Y = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } ;
A20: { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } from FRAENKEL:sch_3(A6);
Segment (q,(W-min C),C) = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } by JORDAN7:def_1;
hence Segment (q,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),q,(W-min C)) by A20, JORDAN6:26; ::_thesis: verum
end;
theorem Th11: :: JORDAN_A:11
for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE E-max C,p,C holds
Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q)
proof
let C be Simple_closed_curve; ::_thesis: for p, q being Point of (TOP-REAL 2) st LE p,q,C & LE E-max C,p,C holds
Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q)
let p, q be Point of (TOP-REAL 2); ::_thesis: ( LE p,q,C & LE E-max C,p,C implies Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) )
assume that
A1: LE p,q,C and
A2: LE E-max C,p,C ; ::_thesis: Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q)
percases ( p = E-max C or p <> E-max C ) ;
suppose p = E-max C ; ::_thesis: Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q)
hence Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) by A1, Th9; ::_thesis: verum
end;
supposeA3: p <> E-max C ; ::_thesis: Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q)
A4: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
A5: q in Lower_Arc C by A1, A2, JORDAN17:4, JORDAN6:58;
A6: p in Lower_Arc C by A2, JORDAN17:4;
A7: Lower_Arc C c= C by JORDAN6:61;
A8: now__::_thesis:_not_p_=_W-min_C
assume A9: p = W-min C ; ::_thesis: contradiction
then LE p, E-max C,C by JORDAN17:2;
hence contradiction by A2, A9, JORDAN6:57, TOPREAL5:19; ::_thesis: verum
end;
A10: now__::_thesis:_not_q_=_W-min_C
assume A11: q = W-min C ; ::_thesis: contradiction
then LE q,p,C by A6, A7, JORDAN7:3;
hence contradiction by A1, A8, A11, JORDAN6:57; ::_thesis: verum
end;
defpred S1[ Point of (TOP-REAL 2)] means ( LE p,$1,C & LE $1,q,C );
defpred S2[ Point of (TOP-REAL 2)] means ( LE p,$1, Lower_Arc C, E-max C, W-min C & LE $1,q, Lower_Arc C, E-max C, W-min C );
A12: for p1 being Point of (TOP-REAL 2) holds
( S1[p1] iff S2[p1] )
proof
let p1 be Point of (TOP-REAL 2); ::_thesis: ( S1[p1] iff S2[p1] )
hereby ::_thesis: ( S2[p1] implies S1[p1] )
assume that
A13: LE p,p1,C and
A14: LE p1,q,C ; ::_thesis: ( LE p,p1, Lower_Arc C, E-max C, W-min C & LE p1,q, Lower_Arc C, E-max C, W-min C )
A15: now__::_thesis:_not_p1_=_W-min_C
assume A16: p1 = W-min C ; ::_thesis: contradiction
then LE p1,p,C by A6, A7, JORDAN7:3;
hence contradiction by A8, A13, A16, JORDAN6:57; ::_thesis: verum
end;
A17: now__::_thesis:_not_p_in_Upper_Arc_C
assume A18: p in Upper_Arc C ; ::_thesis: contradiction
p in Lower_Arc C by A2, JORDAN17:4;
then p in (Lower_Arc C) /\ (Upper_Arc C) by A18, XBOOLE_0:def_4;
then p in {(W-min C),(E-max C)} by JORDAN6:50;
hence contradiction by A3, A8, TARSKI:def_2; ::_thesis: verum
end;
hence LE p,p1, Lower_Arc C, E-max C, W-min C by A13, JORDAN6:def_10; ::_thesis: LE p1,q, Lower_Arc C, E-max C, W-min C
A19: p1 in Lower_Arc C by A13, A17, JORDAN6:def_10;
percases ( q = E-max C or p1 = E-max C or p1 <> E-max C ) ;
suppose q = E-max C ; ::_thesis: LE p1,q, Lower_Arc C, E-max C, W-min C
hence LE p1,q, Lower_Arc C, E-max C, W-min C by A1, A2, A3, JORDAN6:57; ::_thesis: verum
end;
suppose p1 = E-max C ; ::_thesis: LE p1,q, Lower_Arc C, E-max C, W-min C
hence LE p1,q, Lower_Arc C, E-max C, W-min C by A4, A5, JORDAN5C:10; ::_thesis: verum
end;
supposeA20: p1 <> E-max C ; ::_thesis: LE p1,q, Lower_Arc C, E-max C, W-min C
now__::_thesis:_not_p1_in_Upper_Arc_C
assume p1 in Upper_Arc C ; ::_thesis: contradiction
then p1 in (Lower_Arc C) /\ (Upper_Arc C) by A19, XBOOLE_0:def_4;
then p1 in {(W-min C),(E-max C)} by JORDAN6:50;
hence contradiction by A15, A20, TARSKI:def_2; ::_thesis: verum
end;
hence LE p1,q, Lower_Arc C, E-max C, W-min C by A14, JORDAN6:def_10; ::_thesis: verum
end;
end;
end;
assume that
A21: LE p,p1, Lower_Arc C, E-max C, W-min C and
A22: LE p1,q, Lower_Arc C, E-max C, W-min C ; ::_thesis: S1[p1]
A23: p1 <> W-min C by A4, A10, A22, JORDAN6:55;
A24: p1 in Lower_Arc C by A21, JORDAN5C:def_3;
hence LE p,p1,C by A6, A21, A23, JORDAN6:def_10; ::_thesis: LE p1,q,C
thus LE p1,q,C by A5, A10, A22, A24, JORDAN6:def_10; ::_thesis: verum
end;
deffunc H1( set ) -> set = $1;
set X = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } ;
set Y = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } ;
A25: { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } = { H1(p1) where p1 is Point of (TOP-REAL 2) : S2[p1] } from FRAENKEL:sch_3(A12);
Segment (p,q,C) = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } by A10, JORDAN7:def_1;
hence Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) by A25, JORDAN6:26; ::_thesis: verum
end;
end;
end;
theorem Th12: :: JORDAN_A:12
for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st LE p, E-max C,C & LE E-max C,q,C holds
Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q))
proof
let C be Simple_closed_curve; ::_thesis: for p, q being Point of (TOP-REAL 2) st LE p, E-max C,C & LE E-max C,q,C holds
Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q))
let p, q be Point of (TOP-REAL 2); ::_thesis: ( LE p, E-max C,C & LE E-max C,q,C implies Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) )
assume that
A1: LE p, E-max C,C and
A2: LE E-max C,q,C ; ::_thesis: Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q))
A3: p in Upper_Arc C by A1, JORDAN17:3;
A4: q in Lower_Arc C by A2, JORDAN17:4;
A5: now__::_thesis:_not_q_=_W-min_C
assume q = W-min C ; ::_thesis: contradiction
then W-min C = E-max C by A2, JORDAN7:2;
hence contradiction by TOPREAL5:19; ::_thesis: verum
end;
A6: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
defpred S1[ Point of (TOP-REAL 2)] means ( LE p,$1,C & LE $1,q,C );
defpred S2[ Point of (TOP-REAL 2)] means LE p,$1, Upper_Arc C, W-min C, E-max C;
defpred S3[ Point of (TOP-REAL 2)] means LE $1,q, Lower_Arc C, E-max C, W-min C;
defpred S4[ Point of (TOP-REAL 2)] means ( S2[$1] or S3[$1] );
A7: for p1 being Point of (TOP-REAL 2) holds
( S1[p1] iff S4[p1] )
proof
let p1 be Point of (TOP-REAL 2); ::_thesis: ( S1[p1] iff S4[p1] )
thus ( LE p,p1,C & LE p1,q,C & not LE p,p1, Upper_Arc C, W-min C, E-max C implies LE p1,q, Lower_Arc C, E-max C, W-min C ) ::_thesis: ( S4[p1] implies S1[p1] )
proof
assume that
A8: LE p,p1,C and
A9: LE p1,q,C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C )
A10: now__::_thesis:_(_p1_in_Lower_Arc_C_&_p1_in_Upper_Arc_C_&_not_p1_=_W-min_C_implies_p1_=_E-max_C_)
assume that
A11: p1 in Lower_Arc C and
A12: p1 in Upper_Arc C ; ::_thesis: ( p1 = W-min C or p1 = E-max C )
p1 in (Lower_Arc C) /\ (Upper_Arc C) by A11, A12, XBOOLE_0:def_4;
then p1 in {(W-min C),(E-max C)} by JORDAN6:def_9;
hence ( p1 = W-min C or p1 = E-max C ) by TARSKI:def_2; ::_thesis: verum
end;
percases ( p1 = W-min C or p1 = E-max C or not p1 in Lower_Arc C or not p1 in Upper_Arc C ) by A10;
supposeA13: p1 = W-min C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C )
then p = W-min C by A8, JORDAN7:2;
hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) by A1, A13, JORDAN17:3, JORDAN5C:9; ::_thesis: verum
end;
suppose p1 = E-max C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C )
hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) by A4, A6, JORDAN5C:10; ::_thesis: verum
end;
suppose not p1 in Lower_Arc C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C )
hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) by A8, JORDAN6:def_10; ::_thesis: verum
end;
suppose not p1 in Upper_Arc C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C )
hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) by A9, JORDAN6:def_10; ::_thesis: verum
end;
end;
end;
assume A14: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1,q, Lower_Arc C, E-max C, W-min C ) ; ::_thesis: S1[p1]
percases ( LE p,p1, Upper_Arc C, W-min C, E-max C or ( LE p1,q, Lower_Arc C, E-max C, W-min C & p1 <> W-min C ) or ( LE p1,q, Lower_Arc C, E-max C, W-min C & p1 = W-min C ) ) by A14;
supposeA15: LE p,p1, Upper_Arc C, W-min C, E-max C ; ::_thesis: S1[p1]
then A16: p1 in Upper_Arc C by JORDAN5C:def_3;
hence LE p,p1,C by A3, A15, JORDAN6:def_10; ::_thesis: LE p1,q,C
thus LE p1,q,C by A4, A5, A16, JORDAN6:def_10; ::_thesis: verum
end;
supposethat A17: LE p1,q, Lower_Arc C, E-max C, W-min C and
A18: p1 <> W-min C ; ::_thesis: S1[p1]
A19: p1 in Lower_Arc C by A17, JORDAN5C:def_3;
hence LE p,p1,C by A3, A18, JORDAN6:def_10; ::_thesis: LE p1,q,C
thus LE p1,q,C by A4, A5, A17, A19, JORDAN6:def_10; ::_thesis: verum
end;
suppose ( LE p1,q, Lower_Arc C, E-max C, W-min C & p1 = W-min C ) ; ::_thesis: S1[p1]
hence S1[p1] by A5, A6, JORDAN6:55; ::_thesis: verum
end;
end;
end;
set Y1 = { p1 where p1 is Point of (TOP-REAL 2) : S2[p1] } ;
set Y2 = { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] } ;
deffunc H1( set ) -> set = $1;
set X = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } ;
set Y = { H1(p1) where p1 is Point of (TOP-REAL 2) : S4[p1] } ;
set Y9 = { p1 where p1 is Point of (TOP-REAL 2) : ( S2[p1] or S3[p1] ) } ;
A20: { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } = { H1(p1) where p1 is Point of (TOP-REAL 2) : S4[p1] } from FRAENKEL:sch_3(A7);
A21: Segment (p,q,C) = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } by A5, JORDAN7:def_1;
A22: L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) = { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] } by JORDAN6:def_3;
{ p1 where p1 is Point of (TOP-REAL 2) : ( S2[p1] or S3[p1] ) } = { p1 where p1 is Point of (TOP-REAL 2) : S2[p1] } \/ { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] } from TOPREAL1:sch_1();
hence Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) by A20, A21, A22, JORDAN6:def_4; ::_thesis: verum
end;
theorem Th13: :: JORDAN_A:13
for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st LE p, E-max C,C holds
Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)))
proof
let C be Simple_closed_curve; ::_thesis: for p being Point of (TOP-REAL 2) st LE p, E-max C,C holds
Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)))
let p be Point of (TOP-REAL 2); ::_thesis: ( LE p, E-max C,C implies Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) )
set q = W-min C;
assume LE p, E-max C,C ; ::_thesis: Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)))
then A1: p in Upper_Arc C by JORDAN17:3;
A2: W-min C in Lower_Arc C by JORDAN7:1;
A3: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
defpred S1[ Point of (TOP-REAL 2)] means ( LE p,$1,C or ( p in C & $1 = W-min C ) );
defpred S2[ Point of (TOP-REAL 2)] means LE p,$1, Upper_Arc C, W-min C, E-max C;
defpred S3[ Point of (TOP-REAL 2)] means LE $1, W-min C, Lower_Arc C, E-max C, W-min C;
defpred S4[ Point of (TOP-REAL 2)] means ( S2[$1] or S3[$1] );
A4: for p1 being Point of (TOP-REAL 2) holds
( S1[p1] iff S4[p1] )
proof
let p1 be Point of (TOP-REAL 2); ::_thesis: ( S1[p1] iff S4[p1] )
thus ( ( not LE p,p1,C & not ( p in C & p1 = W-min C ) ) or LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) ::_thesis: ( S4[p1] implies S1[p1] )
proof
assume A5: ( LE p,p1,C or ( p in C & p1 = W-min C ) ) ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C )
A6: now__::_thesis:_(_p1_in_Lower_Arc_C_&_p1_in_Upper_Arc_C_&_not_p1_=_W-min_C_implies_p1_=_E-max_C_)
assume that
A7: p1 in Lower_Arc C and
A8: p1 in Upper_Arc C ; ::_thesis: ( p1 = W-min C or p1 = E-max C )
p1 in (Lower_Arc C) /\ (Upper_Arc C) by A7, A8, XBOOLE_0:def_4;
then p1 in {(W-min C),(E-max C)} by JORDAN6:def_9;
hence ( p1 = W-min C or p1 = E-max C ) by TARSKI:def_2; ::_thesis: verum
end;
percases ( p1 = W-min C or p1 = E-max C or ( not p1 in Lower_Arc C & p1 <> W-min C ) or ( not p1 in Upper_Arc C & p1 <> W-min C ) ) by A6;
suppose p1 = W-min C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C )
hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) by A2, JORDAN5C:9; ::_thesis: verum
end;
suppose p1 = E-max C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C )
hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) by A2, A3, JORDAN5C:10; ::_thesis: verum
end;
suppose ( not p1 in Lower_Arc C & p1 <> W-min C ) ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C )
hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) by A5, JORDAN6:def_10; ::_thesis: verum
end;
supposethat A9: not p1 in Upper_Arc C and
A10: p1 <> W-min C ; ::_thesis: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C )
A11: p1 in C by A5, A10, JORDAN7:5;
C = (Lower_Arc C) \/ (Upper_Arc C) by JORDAN6:def_9;
then p1 in Lower_Arc C by A9, A11, XBOOLE_0:def_3;
hence ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) by A3, JORDAN5C:10; ::_thesis: verum
end;
end;
end;
assume A12: ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) ; ::_thesis: S1[p1]
A13: Upper_Arc C c= C by JORDAN6:61;
percases ( LE p,p1, Upper_Arc C, W-min C, E-max C or LE p1, W-min C, Lower_Arc C, E-max C, W-min C ) by A12;
supposeA14: LE p,p1, Upper_Arc C, W-min C, E-max C ; ::_thesis: S1[p1]
then p1 in Upper_Arc C by JORDAN5C:def_3;
hence S1[p1] by A1, A14, JORDAN6:def_10; ::_thesis: verum
end;
suppose LE p1, W-min C, Lower_Arc C, E-max C, W-min C ; ::_thesis: S1[p1]
then A15: p1 in Lower_Arc C by JORDAN5C:def_3;
now__::_thesis:_S1[p1]
percases ( p1 = W-min C or p1 <> W-min C ) ;
suppose p1 = W-min C ; ::_thesis: S1[p1]
hence S1[p1] by A1, A13; ::_thesis: verum
end;
suppose p1 <> W-min C ; ::_thesis: S1[p1]
hence S1[p1] by A1, A15, JORDAN6:def_10; ::_thesis: verum
end;
end;
end;
hence S1[p1] ; ::_thesis: verum
end;
end;
end;
set Y1 = { p1 where p1 is Point of (TOP-REAL 2) : S2[p1] } ;
set Y2 = { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] } ;
deffunc H1( set ) -> set = $1;
set X = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } ;
set Y = { H1(p1) where p1 is Point of (TOP-REAL 2) : S4[p1] } ;
set Y9 = { p1 where p1 is Point of (TOP-REAL 2) : ( S2[p1] or S3[p1] ) } ;
A16: { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } = { H1(p1) where p1 is Point of (TOP-REAL 2) : S4[p1] } from FRAENKEL:sch_3(A4);
A17: Segment (p,(W-min C),C) = { H1(p1) where p1 is Point of (TOP-REAL 2) : S1[p1] } by JORDAN7:def_1;
A18: L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) = { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] } by JORDAN6:def_3;
{ p1 where p1 is Point of (TOP-REAL 2) : ( S2[p1] or S3[p1] ) } = { p1 where p1 is Point of (TOP-REAL 2) : S2[p1] } \/ { p1 where p1 is Point of (TOP-REAL 2) : S3[p1] } from TOPREAL1:sch_1();
hence Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) by A16, A17, A18, JORDAN6:def_4; ::_thesis: verum
end;
theorem Th14: :: JORDAN_A:14
for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) holds R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C))
proof
let C be Simple_closed_curve; ::_thesis: for p being Point of (TOP-REAL 2) holds R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C))
let p be Point of (TOP-REAL 2); ::_thesis: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C))
Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
then L_Segment ((Upper_Arc C),(W-min C),(E-max C),(E-max C)) = Upper_Arc C by JORDAN6:22;
hence Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C)) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (Upper_Arc C) by JORDAN6:def_5
.= R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by JORDAN6:20, XBOOLE_1:28 ;
::_thesis: verum
end;
theorem Th15: :: JORDAN_A:15
for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) holds L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p)
proof
let C be Simple_closed_curve; ::_thesis: for p being Point of (TOP-REAL 2) holds L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p)
let p be Point of (TOP-REAL 2); ::_thesis: L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p)
Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
then R_Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C)) = Lower_Arc C by JORDAN6:24;
hence Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),p) = (Lower_Arc C) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),p)) by JORDAN6:def_5
.= L_Segment ((Lower_Arc C),(E-max C),(W-min C),p) by JORDAN6:19, XBOOLE_1:28 ;
::_thesis: verum
end;
theorem Th16: :: JORDAN_A:16
for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st p in C & p <> W-min C holds
Segment (p,(W-min C),C) is_an_arc_of p, W-min C
proof
let C be Simple_closed_curve; ::_thesis: for p being Point of (TOP-REAL 2) st p in C & p <> W-min C holds
Segment (p,(W-min C),C) is_an_arc_of p, W-min C
set q = W-min C;
let p be Point of (TOP-REAL 2); ::_thesis: ( p in C & p <> W-min C implies Segment (p,(W-min C),C) is_an_arc_of p, W-min C )
assume that
A1: p in C and
A2: p <> W-min C ; ::_thesis: Segment (p,(W-min C),C) is_an_arc_of p, W-min C
A3: E-max C in C by SPRECT_1:14;
A4: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
A5: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
A6: W-min C <> E-max C by TOPREAL5:19;
percases ( ( p <> E-max C & LE p, E-max C,C ) or p = E-max C or ( p <> E-max C & LE E-max C,p,C ) ) by A1, A3, JORDAN16:7;
supposethat A7: p <> E-max C and
A8: LE p, E-max C,C ; ::_thesis: Segment (p,(W-min C),C) is_an_arc_of p, W-min C
A9: now__::_thesis:_not_W-min_C_in_(R_Segment_((Upper_Arc_C),(W-min_C),(E-max_C),p))_/\_(L_Segment_((Lower_Arc_C),(E-max_C),(W-min_C),(W-min_C)))
assume W-min C in (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) ; ::_thesis: contradiction
then W-min C in R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by XBOOLE_0:def_4;
hence contradiction by A2, A4, JORDAN6:60; ::_thesis: verum
end;
p in Upper_Arc C by A8, JORDAN17:3;
then A10: LE p, E-max C, Upper_Arc C, W-min C, E-max C by A4, JORDAN5C:10;
A11: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C)) by Th14;
then A12: E-max C in R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by A10, JORDAN16:5;
W-min C in Lower_Arc C by JORDAN7:1;
then A13: LE E-max C, W-min C, Lower_Arc C, E-max C, W-min C by A5, JORDAN5C:10;
A14: L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),(W-min C)) by Th15;
then E-max C in L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) by A13, JORDAN16:5;
then A15: E-max C in (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) by A12, XBOOLE_0:def_4;
A16: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) c= Upper_Arc C by JORDAN6:20;
A17: L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) c= Lower_Arc C by JORDAN6:19;
(Upper_Arc C) /\ (Lower_Arc C) = {(W-min C),(E-max C)} by JORDAN6:def_9;
then A18: (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) = {(E-max C)} by A9, A15, A16, A17, TOPREAL8:1, XBOOLE_1:27;
A19: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) is_an_arc_of p, E-max C by A4, A7, A10, A11, JORDAN16:21;
A20: L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C)) is_an_arc_of E-max C, W-min C by A5, A6, A13, A14, JORDAN16:21;
Segment (p,(W-min C),C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),(W-min C))) by A8, Th13;
hence Segment (p,(W-min C),C) is_an_arc_of p, W-min C by A18, A19, A20, TOPREAL1:2; ::_thesis: verum
end;
supposeA21: p = E-max C ; ::_thesis: Segment (p,(W-min C),C) is_an_arc_of p, W-min C
then Segment (p,(W-min C),C) = Lower_Arc C by JORDAN7:4;
hence Segment (p,(W-min C),C) is_an_arc_of p, W-min C by A21, JORDAN6:50; ::_thesis: verum
end;
supposethat p <> E-max C and
A22: LE E-max C,p,C ; ::_thesis: Segment (p,(W-min C),C) is_an_arc_of p, W-min C
A23: Segment (p,(W-min C),C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,(W-min C)) by A22, Th10;
p in Lower_Arc C by A22, JORDAN17:4;
then LE p, W-min C, Lower_Arc C, E-max C, W-min C by A5, JORDAN5C:10;
hence Segment (p,(W-min C),C) is_an_arc_of p, W-min C by A2, A5, A23, JORDAN16:21; ::_thesis: verum
end;
end;
end;
theorem Th17: :: JORDAN_A:17
for C being Simple_closed_curve
for p, q being Point of (TOP-REAL 2) st p <> q & LE p,q,C holds
Segment (p,q,C) is_an_arc_of p,q
proof
let C be Simple_closed_curve; ::_thesis: for p, q being Point of (TOP-REAL 2) st p <> q & LE p,q,C holds
Segment (p,q,C) is_an_arc_of p,q
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q & LE p,q,C implies Segment (p,q,C) is_an_arc_of p,q )
assume that
A1: p <> q and
A2: LE p,q,C ; ::_thesis: Segment (p,q,C) is_an_arc_of p,q
A3: E-max C in C by SPRECT_1:14;
A4: p in C by A2, JORDAN7:5;
A5: q in C by A2, JORDAN7:5;
A6: Upper_Arc C is_an_arc_of W-min C, E-max C by JORDAN6:50;
A7: Lower_Arc C is_an_arc_of E-max C, W-min C by JORDAN6:50;
percases ( q = W-min C or ( LE q, E-max C,C & not LE E-max C,q,C & q <> W-min C ) or ( p <> E-max C & LE p, E-max C,C & LE E-max C,q,C & q <> E-max C ) or ( q = E-max C & LE p, E-max C,C & LE E-max C,q,C ) or ( p = E-max C & LE p, E-max C,C & LE E-max C,q,C ) or ( LE E-max C,p,C & not LE p, E-max C,C ) ) by A3, A4, A5, JORDAN16:7;
suppose q = W-min C ; ::_thesis: Segment (p,q,C) is_an_arc_of p,q
hence Segment (p,q,C) is_an_arc_of p,q by A1, A4, Th16; ::_thesis: verum
end;
supposethat A8: LE q, E-max C,C and
A9: not LE E-max C,q,C and
A10: q <> W-min C ; ::_thesis: Segment (p,q,C) is_an_arc_of p,q
A11: Segment (p,q,C) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,q) by A1, A2, A8, Th8;
not q in Lower_Arc C by A9, A10, Th5;
then LE p,q, Upper_Arc C, W-min C, E-max C by A2, JORDAN6:def_10;
hence Segment (p,q,C) is_an_arc_of p,q by A1, A6, A11, JORDAN16:21; ::_thesis: verum
end;
supposethat A12: p <> E-max C and
A13: LE p, E-max C,C and
A14: LE E-max C,q,C and
A15: q <> E-max C ; ::_thesis: Segment (p,q,C) is_an_arc_of p,q
A16: now__::_thesis:_not_W-min_C_in_(R_Segment_((Upper_Arc_C),(W-min_C),(E-max_C),p))_/\_(L_Segment_((Lower_Arc_C),(E-max_C),(W-min_C),q))
assume A17: W-min C in (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) ; ::_thesis: contradiction
then W-min C in R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by XBOOLE_0:def_4;
then A18: p = W-min C by A6, JORDAN6:60;
W-min C in L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) by A17, XBOOLE_0:def_4;
hence contradiction by A1, A7, A18, JORDAN6:59; ::_thesis: verum
end;
p in Upper_Arc C by A13, JORDAN17:3;
then A19: LE p, E-max C, Upper_Arc C, W-min C, E-max C by A6, JORDAN5C:10;
A20: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C)) by Th14;
then A21: E-max C in R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by A19, JORDAN16:5;
q in Lower_Arc C by A14, JORDAN17:4;
then A22: LE E-max C,q, Lower_Arc C, E-max C, W-min C by A7, JORDAN5C:10;
A23: L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q) by Th15;
then E-max C in L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) by A22, JORDAN16:5;
then A24: E-max C in (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) by A21, XBOOLE_0:def_4;
A25: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) c= Upper_Arc C by JORDAN6:20;
A26: L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) c= Lower_Arc C by JORDAN6:19;
(Upper_Arc C) /\ (Lower_Arc C) = {(W-min C),(E-max C)} by JORDAN6:def_9;
then A27: (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) /\ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) = {(E-max C)} by A16, A24, A25, A26, TOPREAL8:1, XBOOLE_1:27;
A28: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) is_an_arc_of p, E-max C by A6, A12, A19, A20, JORDAN16:21;
A29: L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) is_an_arc_of E-max C,q by A7, A15, A22, A23, JORDAN16:21;
Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) by A13, A14, Th12;
hence Segment (p,q,C) is_an_arc_of p,q by A27, A28, A29, TOPREAL1:2; ::_thesis: verum
end;
supposethat A30: q = E-max C and
A31: LE p, E-max C,C and
A32: LE E-max C,q,C ; ::_thesis: Segment (p,q,C) is_an_arc_of p,q
p in Upper_Arc C by A31, JORDAN17:3;
then A33: LE p, E-max C, Upper_Arc C, W-min C, E-max C by A6, JORDAN5C:10;
A34: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = Segment ((Upper_Arc C),(W-min C),(E-max C),p,(E-max C)) by Th14;
then A35: E-max C in R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by A33, JORDAN16:5;
A36: L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) = {(E-max C)} by A7, A30, JORDAN6:21;
Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) by A31, A32, Th12
.= R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) by A35, A36, ZFMISC_1:40 ;
hence Segment (p,q,C) is_an_arc_of p,q by A1, A6, A30, A33, A34, JORDAN16:21; ::_thesis: verum
end;
supposethat A37: p = E-max C and
A38: LE p, E-max C,C and
A39: LE E-max C,q,C ; ::_thesis: Segment (p,q,C) is_an_arc_of p,q
q in Lower_Arc C by A39, JORDAN17:4;
then A40: LE E-max C,q, Lower_Arc C, E-max C, W-min C by A7, JORDAN5C:10;
A41: L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) = Segment ((Lower_Arc C),(E-max C),(W-min C),(E-max C),q) by Th15;
then A42: E-max C in L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) by A40, JORDAN16:5;
A43: R_Segment ((Upper_Arc C),(W-min C),(E-max C),p) = {(E-max C)} by A6, A37, JORDAN6:23;
Segment (p,q,C) = (R_Segment ((Upper_Arc C),(W-min C),(E-max C),p)) \/ (L_Segment ((Lower_Arc C),(E-max C),(W-min C),q)) by A38, A39, Th12
.= L_Segment ((Lower_Arc C),(E-max C),(W-min C),q) by A42, A43, ZFMISC_1:40 ;
hence Segment (p,q,C) is_an_arc_of p,q by A1, A7, A37, A40, A41, JORDAN16:21; ::_thesis: verum
end;
supposethat A44: LE E-max C,p,C and
A45: not LE p, E-max C,C ; ::_thesis: Segment (p,q,C) is_an_arc_of p,q
A46: Segment (p,q,C) = Segment ((Lower_Arc C),(E-max C),(W-min C),p,q) by A2, A44, Th11;
not p in Upper_Arc C by A45, Th6;
then LE p,q, Lower_Arc C, E-max C, W-min C by A2, JORDAN6:def_10;
hence Segment (p,q,C) is_an_arc_of p,q by A1, A7, A46, JORDAN16:21; ::_thesis: verum
end;
end;
end;
theorem Th18: :: JORDAN_A:18
for C being Simple_closed_curve holds C = Segment ((W-min C),(W-min C),C)
proof
let C be Simple_closed_curve; ::_thesis: C = Segment ((W-min C),(W-min C),C)
set X = { p where p is Point of (TOP-REAL 2) : ( LE W-min C,p,C or ( W-min C in C & p = W-min C ) ) } ;
A1: Segment ((W-min C),(W-min C),C) = { p where p is Point of (TOP-REAL 2) : ( LE W-min C,p,C or ( W-min C in C & p = W-min C ) ) } by JORDAN7:def_1;
thus C c= Segment ((W-min C),(W-min C),C) :: according to XBOOLE_0:def_10 ::_thesis: Segment ((W-min C),(W-min C),C) c= C
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in C or e in Segment ((W-min C),(W-min C),C) )
assume A2: e in C ; ::_thesis: e in Segment ((W-min C),(W-min C),C)
then reconsider p = e as Point of (TOP-REAL 2) ;
LE W-min C,p,C by A2, JORDAN7:3;
hence e in Segment ((W-min C),(W-min C),C) by A1; ::_thesis: verum
end;
thus Segment ((W-min C),(W-min C),C) c= C by JORDAN16:6; ::_thesis: verum
end;
theorem Th19: :: JORDAN_A:19
for C being Simple_closed_curve
for q being Point of (TOP-REAL 2) st q in C holds
Segment (q,(W-min C),C) is compact
proof
let C be Simple_closed_curve; ::_thesis: for q being Point of (TOP-REAL 2) st q in C holds
Segment (q,(W-min C),C) is compact
let q be Point of (TOP-REAL 2); ::_thesis: ( q in C implies Segment (q,(W-min C),C) is compact )
assume A1: q in C ; ::_thesis: Segment (q,(W-min C),C) is compact
percases ( q = W-min C or q <> W-min C ) ;
suppose q = W-min C ; ::_thesis: Segment (q,(W-min C),C) is compact
hence Segment (q,(W-min C),C) is compact by Th18; ::_thesis: verum
end;
suppose q <> W-min C ; ::_thesis: Segment (q,(W-min C),C) is compact
hence Segment (q,(W-min C),C) is compact by A1, Th16, JORDAN5A:1; ::_thesis: verum
end;
end;
end;
theorem Th20: :: JORDAN_A:20
for C being Simple_closed_curve
for q1, q2 being Point of (TOP-REAL 2) st LE q1,q2,C holds
Segment (q1,q2,C) is compact
proof
let C be Simple_closed_curve; ::_thesis: for q1, q2 being Point of (TOP-REAL 2) st LE q1,q2,C holds
Segment (q1,q2,C) is compact
let q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( LE q1,q2,C implies Segment (q1,q2,C) is compact )
assume A1: LE q1,q2,C ; ::_thesis: Segment (q1,q2,C) is compact
A2: q1 in C by A1, JORDAN7:5;
percases ( q2 = W-min C or ( q1 = q2 & q2 <> W-min C ) or ( q1 <> q2 & q2 <> W-min C ) ) ;
suppose q2 = W-min C ; ::_thesis: Segment (q1,q2,C) is compact
hence Segment (q1,q2,C) is compact by A2, Th19; ::_thesis: verum
end;
suppose ( q1 = q2 & q2 <> W-min C ) ; ::_thesis: Segment (q1,q2,C) is compact
then Segment (q1,q2,C) = {q1} by A2, JORDAN7:8;
hence Segment (q1,q2,C) is compact ; ::_thesis: verum
end;
suppose ( q1 <> q2 & q2 <> W-min C ) ; ::_thesis: Segment (q1,q2,C) is compact
hence Segment (q1,q2,C) is compact by A1, Th17, JORDAN5A:1; ::_thesis: verum
end;
end;
end;
begin
definition
let C be Simple_closed_curve;
mode Segmentation of C -> FinSequence of (TOP-REAL 2) means :Def3: :: JORDAN_A:def 3
( it /. 1 = W-min C & it is one-to-one & 8 <= len it & rng it c= C & ( for i being Element of NAT st 1 <= i & i < len it holds
LE it /. i,it /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len it holds
(Segment ((it /. i),(it /. (i + 1)),C)) /\ (Segment ((it /. (i + 1)),(it /. (i + 2)),C)) = {(it /. (i + 1))} ) & (Segment ((it /. (len it)),(it /. 1),C)) /\ (Segment ((it /. 1),(it /. 2),C)) = {(it /. 1)} & (Segment ((it /. ((len it) -' 1)),(it /. (len it)),C)) /\ (Segment ((it /. (len it)),(it /. 1),C)) = {(it /. (len it))} & Segment ((it /. ((len it) -' 1)),(it /. (len it)),C) misses Segment ((it /. 1),(it /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len it & not i,j are_adjacent1 holds
Segment ((it /. i),(it /. (i + 1)),C) misses Segment ((it /. j),(it /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len it holds
Segment ((it /. (len it)),(it /. 1),C) misses Segment ((it /. i),(it /. (i + 1)),C) ) );
existence
ex b1 being FinSequence of (TOP-REAL 2) st
( b1 /. 1 = W-min C & b1 is one-to-one & 8 <= len b1 & rng b1 c= C & ( for i being Element of NAT st 1 <= i & i < len b1 holds
LE b1 /. i,b1 /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len b1 holds
(Segment ((b1 /. i),(b1 /. (i + 1)),C)) /\ (Segment ((b1 /. (i + 1)),(b1 /. (i + 2)),C)) = {(b1 /. (i + 1))} ) & (Segment ((b1 /. (len b1)),(b1 /. 1),C)) /\ (Segment ((b1 /. 1),(b1 /. 2),C)) = {(b1 /. 1)} & (Segment ((b1 /. ((len b1) -' 1)),(b1 /. (len b1)),C)) /\ (Segment ((b1 /. (len b1)),(b1 /. 1),C)) = {(b1 /. (len b1))} & Segment ((b1 /. ((len b1) -' 1)),(b1 /. (len b1)),C) misses Segment ((b1 /. 1),(b1 /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len b1 & not i,j are_adjacent1 holds
Segment ((b1 /. i),(b1 /. (i + 1)),C) misses Segment ((b1 /. j),(b1 /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len b1 holds
Segment ((b1 /. (len b1)),(b1 /. 1),C) misses Segment ((b1 /. i),(b1 /. (i + 1)),C) ) )
proof
consider h being FinSequence of the carrier of (TOP-REAL 2) such that
A1: h . 1 = W-min C and
A2: h is one-to-one and
A3: 8 <= len h and
A4: rng h c= C and
A5: for i being Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C and
for i being Element of NAT
for W being Subset of (Euclid 2) st 1 <= i & i < len h & W = Segment ((h /. i),(h /. (i + 1)),C) holds
diameter W < 1 and
for W being Subset of (Euclid 2) st W = Segment ((h /. (len h)),(h /. 1),C) holds
diameter W < 1 and
A6: for i being Element of NAT st 1 <= i & i + 1 < len h holds
(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} and
A7: (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} and
A8: (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} and
A9: Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) and
A10: for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) and
A11: for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) by JORDAN7:20;
reconsider h = h as non empty FinSequence of the carrier of (TOP-REAL 2) by A3, CARD_1:27;
take h ; ::_thesis: ( h /. 1 = W-min C & h is one-to-one & 8 <= len h & rng h c= C & ( for i being Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len h holds
(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )
1 in dom h by FINSEQ_5:6;
hence h /. 1 = W-min C by A1, PARTFUN1:def_6; ::_thesis: ( h is one-to-one & 8 <= len h & rng h c= C & ( for i being Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len h holds
(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )
thus h is one-to-one by A2; ::_thesis: ( 8 <= len h & rng h c= C & ( for i being Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len h holds
(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )
thus 8 <= len h by A3; ::_thesis: ( rng h c= C & ( for i being Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len h holds
(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )
thus rng h c= C by A4; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len h holds
(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )
thus for i being Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C by A5; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i + 1 < len h holds
(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} ) & (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )
thus for i being Element of NAT st 1 <= i & i + 1 < len h holds
(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} by A6; ::_thesis: ( (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} & (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )
thus (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} by A7; ::_thesis: ( (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} & Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )
thus (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} by A8; ::_thesis: ( Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )
thus Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) by A9; ::_thesis: ( ( for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) ) )
thus for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) by A10; ::_thesis: for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C)
thus for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) by A11; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Segmentation JORDAN_A:def_3_:_
for C being Simple_closed_curve
for b2 being FinSequence of (TOP-REAL 2) holds
( b2 is Segmentation of C iff ( b2 /. 1 = W-min C & b2 is one-to-one & 8 <= len b2 & rng b2 c= C & ( for i being Element of NAT st 1 <= i & i < len b2 holds
LE b2 /. i,b2 /. (i + 1),C ) & ( for i being Element of NAT st 1 <= i & i + 1 < len b2 holds
(Segment ((b2 /. i),(b2 /. (i + 1)),C)) /\ (Segment ((b2 /. (i + 1)),(b2 /. (i + 2)),C)) = {(b2 /. (i + 1))} ) & (Segment ((b2 /. (len b2)),(b2 /. 1),C)) /\ (Segment ((b2 /. 1),(b2 /. 2),C)) = {(b2 /. 1)} & (Segment ((b2 /. ((len b2) -' 1)),(b2 /. (len b2)),C)) /\ (Segment ((b2 /. (len b2)),(b2 /. 1),C)) = {(b2 /. (len b2))} & Segment ((b2 /. ((len b2) -' 1)),(b2 /. (len b2)),C) misses Segment ((b2 /. 1),(b2 /. 2),C) & ( for i, j being Element of NAT st 1 <= i & i < j & j < len b2 & not i,j are_adjacent1 holds
Segment ((b2 /. i),(b2 /. (i + 1)),C) misses Segment ((b2 /. j),(b2 /. (j + 1)),C) ) & ( for i being Element of NAT st 1 < i & i + 1 < len b2 holds
Segment ((b2 /. (len b2)),(b2 /. 1),C) misses Segment ((b2 /. i),(b2 /. (i + 1)),C) ) ) );
registration
let C be Simple_closed_curve;
cluster -> non trivial for Segmentation of C;
coherence
for b1 being Segmentation of C holds not b1 is trivial
proof
let S be Segmentation of C; ::_thesis: not S is trivial
len S >= 8 by Def3;
then len S >= 2 by XXREAL_0:2;
hence not S is trivial by NAT_D:60; ::_thesis: verum
end;
end;
theorem Th21: :: JORDAN_A:21
for C being Simple_closed_curve
for S being Segmentation of C
for i being Element of NAT st 1 <= i & i <= len S holds
S /. i in C
proof
let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C
for i being Element of NAT st 1 <= i & i <= len S holds
S /. i in C
let S be Segmentation of C; ::_thesis: for i being Element of NAT st 1 <= i & i <= len S holds
S /. i in C
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len S implies S /. i in C )
assume that
A1: 1 <= i and
A2: i <= len S ; ::_thesis: S /. i in C
i in dom S by A1, A2, FINSEQ_3:25;
then A3: S /. i in rng S by PARTFUN2:2;
rng S c= C by Def3;
hence S /. i in C by A3; ::_thesis: verum
end;
begin
definition
let C be Simple_closed_curve;
let i be Nat;
let S be Segmentation of C;
func Segm (S,i) -> Subset of (TOP-REAL 2) equals :Def4: :: JORDAN_A:def 4
Segment ((S /. i),(S /. (i + 1)),C) if ( 1 <= i & i < len S )
otherwise Segment ((S /. (len S)),(S /. 1),C);
correctness
coherence
( ( 1 <= i & i < len S implies Segment ((S /. i),(S /. (i + 1)),C) is Subset of (TOP-REAL 2) ) & ( ( not 1 <= i or not i < len S ) implies Segment ((S /. (len S)),(S /. 1),C) is Subset of (TOP-REAL 2) ) );
consistency
for b1 being Subset of (TOP-REAL 2) holds verum;
;
end;
:: deftheorem Def4 defines Segm JORDAN_A:def_4_:_
for C being Simple_closed_curve
for i being Nat
for S being Segmentation of C holds
( ( 1 <= i & i < len S implies Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) ) & ( ( not 1 <= i or not i < len S ) implies Segm (S,i) = Segment ((S /. (len S)),(S /. 1),C) ) );
theorem :: JORDAN_A:22
for C being Simple_closed_curve
for i being Element of NAT
for S being Segmentation of C st i in dom S holds
Segm (S,i) c= C
proof
let C be Simple_closed_curve; ::_thesis: for i being Element of NAT
for S being Segmentation of C st i in dom S holds
Segm (S,i) c= C
let i be Element of NAT ; ::_thesis: for S being Segmentation of C st i in dom S holds
Segm (S,i) c= C
let S be Segmentation of C; ::_thesis: ( i in dom S implies Segm (S,i) c= C )
assume i in dom S ; ::_thesis: Segm (S,i) c= C
then A1: 1 <= i by FINSEQ_3:25;
( i < len S or i >= len S ) ;
then ( Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) or Segm (S,i) = Segment ((S /. (len S)),(S /. 1),C) ) by A1, Def4;
hence Segm (S,i) c= C by JORDAN16:6; ::_thesis: verum
end;
registration
let C be Simple_closed_curve;
let S be Segmentation of C;
let i be Element of NAT ;
cluster Segm (S,i) -> non empty compact ;
coherence
( not Segm (S,i) is empty & Segm (S,i) is compact )
proof
percases ( ( 1 <= i & i < len S ) or not 1 <= i or not i < len S ) ;
supposeA1: ( 1 <= i & i < len S ) ; ::_thesis: ( not Segm (S,i) is empty & Segm (S,i) is compact )
then A2: Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) by Def4;
LE S /. i,S /. (i + 1),C by A1, Def3;
hence ( not Segm (S,i) is empty & Segm (S,i) is compact ) by A2, Th20, JORDAN7:6; ::_thesis: verum
end;
suppose ( not 1 <= i or not i < len S ) ; ::_thesis: ( not Segm (S,i) is empty & Segm (S,i) is compact )
then A3: Segm (S,i) = Segment ((S /. (len S)),(S /. 1),C) by Def4;
8 <= len S by Def3;
then 1 <= len S by XXREAL_0:2;
then A4: S /. (len S) in C by Th21;
S /. 1 = W-min C by Def3;
hence ( not Segm (S,i) is empty & Segm (S,i) is compact ) by A3, A4, Th19, JORDAN16:19; ::_thesis: verum
end;
end;
end;
end;
theorem :: JORDAN_A:23
for C being Simple_closed_curve
for S being Segmentation of C
for p being Point of (TOP-REAL 2) st p in C holds
ex i being Nat st
( i in dom S & p in Segm (S,i) )
proof
let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C
for p being Point of (TOP-REAL 2) st p in C holds
ex i being Nat st
( i in dom S & p in Segm (S,i) )
let S be Segmentation of C; ::_thesis: for p being Point of (TOP-REAL 2) st p in C holds
ex i being Nat st
( i in dom S & p in Segm (S,i) )
let p be Point of (TOP-REAL 2); ::_thesis: ( p in C implies ex i being Nat st
( i in dom S & p in Segm (S,i) ) )
assume A1: p in C ; ::_thesis: ex i being Nat st
( i in dom S & p in Segm (S,i) )
set X = { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } ;
A2: { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } c= dom S
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } or e in dom S )
assume e in { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } ; ::_thesis: e in dom S
then ex i being Element of NAT st
( e = i & i in dom S & LE S /. i,p,C ) ;
hence e in dom S ; ::_thesis: verum
end;
A3: 1 in dom S by FINSEQ_5:6;
A4: W-min C = S /. 1 by Def3;
then LE S /. 1,p,C by A1, JORDAN7:3;
then 1 in { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } by A3;
then reconsider X = { i where i is Element of NAT : ( i in dom S & LE S /. i,p,C ) } as non empty finite Subset of NAT by A2, XBOOLE_1:1;
take max X ; ::_thesis: ( max X in dom S & p in Segm (S,(max X)) )
A5: max X in X by XXREAL_2:def_8;
hence max X in dom S by A2; ::_thesis: p in Segm (S,(max X))
A6: 1 <= max X by A2, A5, FINSEQ_3:25;
A7: max X <= len S by A2, A5, FINSEQ_3:25;
A8: ex i being Element of NAT st
( max X = i & i in dom S & LE S /. i,p,C ) by A5;
reconsider mX = max X as Element of NAT by ORDINAL1:def_12;
percases ( max X < len S or max X = len S ) by A7, XXREAL_0:1;
supposeA9: max X < len S ; ::_thesis: p in Segm (S,(max X))
A10: 1 <= (max X) + 1 by NAT_1:11;
(max X) + 1 <= len S by A9, NAT_1:13;
then A11: mX + 1 in dom S by A10, FINSEQ_3:25;
A12: S is one-to-one by Def3;
(max X) + 1 >= 1 + 1 by A6, XREAL_1:6;
then (max X) + 1 <> 1 ;
then A13: S /. ((max X) + 1) <> S /. 1 by A3, A11, A12, PARTFUN2:10;
A14: S /. ((max X) + 1) in rng S by A11, PARTFUN2:2;
A15: rng S c= C by Def3;
now__::_thesis:_not_LE_S_/._((max_X)_+_1),p,C
assume LE S /. ((max X) + 1),p,C ; ::_thesis: contradiction
then (max X) + 1 in X by A11;
then (max X) + 1 <= max X by XXREAL_2:def_8;
hence contradiction by XREAL_1:29; ::_thesis: verum
end;
then LE p,S /. ((max X) + 1),C by A1, A14, A15, JORDAN16:7;
then p in { p1 where p1 is Point of (TOP-REAL 2) : ( LE S /. (max X),p1,C & LE p1,S /. ((max X) + 1),C ) } by A8;
then p in Segment ((S /. (max X)),(S /. ((max X) + 1)),C) by A4, A13, JORDAN7:def_1;
hence p in Segm (S,(max X)) by A6, A9, Def4; ::_thesis: verum
end;
supposeA16: max X = len S ; ::_thesis: p in Segm (S,(max X))
now__::_thesis:_(_(_p_<>_W-min_C_&_LE_S_/._(len_S),p,C_)_or_(_p_=_W-min_C_&_S_/._(len_S)_in_C_)_)
percases ( p <> W-min C or p = W-min C ) ;
case p <> W-min C ; ::_thesis: LE S /. (len S),p,C
thus LE S /. (len S),p,C by A8, A16; ::_thesis: verum
end;
case p = W-min C ; ::_thesis: S /. (len S) in C
A17: S /. (len S) in rng S by REVROT_1:3;
rng S c= C by Def3;
hence S /. (len S) in C by A17; ::_thesis: verum
end;
end;
end;
then p in { p1 where p1 is Point of (TOP-REAL 2) : ( LE S /. (len S),p1,C or ( S /. (len S) in C & p1 = W-min C ) ) } ;
then p in Segment ((S /. (len S)),(S /. 1),C) by A4, JORDAN7:def_1;
hence p in Segm (S,(max X)) by A16, Def4; ::_thesis: verum
end;
end;
end;
theorem Th24: :: JORDAN_A:24
for C being Simple_closed_curve
for S being Segmentation of C
for i, j being Element of NAT st 1 <= i & i < j & j < len S & not i,j are_adjacent1 holds
Segm (S,i) misses Segm (S,j)
proof
let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C
for i, j being Element of NAT st 1 <= i & i < j & j < len S & not i,j are_adjacent1 holds
Segm (S,i) misses Segm (S,j)
let S be Segmentation of C; ::_thesis: for i, j being Element of NAT st 1 <= i & i < j & j < len S & not i,j are_adjacent1 holds
Segm (S,i) misses Segm (S,j)
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 implies Segm (S,i) misses Segm (S,j) )
assume that
A1: 1 <= i and
A2: i < j and
A3: j < len S and
A4: not i,j are_adjacent1 ; ::_thesis: Segm (S,i) misses Segm (S,j)
i < len S by A2, A3, XXREAL_0:2;
then A5: Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) by A1, Def4;
1 < j by A1, A2, XXREAL_0:2;
then Segm (S,j) = Segment ((S /. j),(S /. (j + 1)),C) by A3, Def4;
hence Segm (S,i) misses Segm (S,j) by A1, A2, A3, A4, A5, Def3; ::_thesis: verum
end;
theorem Th25: :: JORDAN_A:25
for C being Simple_closed_curve
for S being Segmentation of C
for j being Element of NAT st 1 < j & j < (len S) -' 1 holds
Segm (S,(len S)) misses Segm (S,j)
proof
let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C
for j being Element of NAT st 1 < j & j < (len S) -' 1 holds
Segm (S,(len S)) misses Segm (S,j)
let S be Segmentation of C; ::_thesis: for j being Element of NAT st 1 < j & j < (len S) -' 1 holds
Segm (S,(len S)) misses Segm (S,j)
let j be Element of NAT ; ::_thesis: ( 1 < j & j < (len S) -' 1 implies Segm (S,(len S)) misses Segm (S,j) )
assume that
A1: 1 < j and
A2: j < (len S) -' 1 ; ::_thesis: Segm (S,(len S)) misses Segm (S,j)
A3: Segm (S,(len S)) = Segment ((S /. (len S)),(S /. 1),C) by Def4;
A4: j + 1 < len S by A2, NAT_D:53;
j < len S by A2, NAT_D:44;
then Segm (S,j) = Segment ((S /. j),(S /. (j + 1)),C) by A1, Def4;
hence Segm (S,(len S)) misses Segm (S,j) by A1, A3, A4, Def3; ::_thesis: verum
end;
theorem Th26: :: JORDAN_A:26
for C being Simple_closed_curve
for S being Segmentation of C
for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds
(Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))}
proof
let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C
for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds
(Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))}
let S be Segmentation of C; ::_thesis: for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds
(Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))}
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i < j & j < len S & i,j are_adjacent1 implies (Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))} )
assume that
A1: 1 <= i and
A2: i < j and
A3: j < len S and
A4: i,j are_adjacent1 ; ::_thesis: (Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))}
i < len S by A2, A3, XXREAL_0:2;
then A5: Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) by A1, Def4;
1 < j by A1, A2, XXREAL_0:2;
then A6: Segm (S,j) = Segment ((S /. j),(S /. (j + 1)),C) by A3, Def4;
j + 1 > i by A2, NAT_1:13;
then j = i + 1 by A4, GOBRD10:def_1;
then j + 1 = i + (1 + 1) ;
hence (Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))} by A1, A3, A5, A6, Def3; ::_thesis: verum
end;
theorem Th27: :: JORDAN_A:27
for C being Simple_closed_curve
for S being Segmentation of C
for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds
Segm (S,i) meets Segm (S,j)
proof
let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C
for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds
Segm (S,i) meets Segm (S,j)
let S be Segmentation of C; ::_thesis: for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds
Segm (S,i) meets Segm (S,j)
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & i < j & j < len S & i,j are_adjacent1 implies Segm (S,i) meets Segm (S,j) )
assume that
A1: 1 <= i and
A2: i < j and
A3: j < len S and
A4: i,j are_adjacent1 ; ::_thesis: Segm (S,i) meets Segm (S,j)
(Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))} by A1, A2, A3, A4, Th26;
hence Segm (S,i) meets Segm (S,j) by XBOOLE_0:def_7; ::_thesis: verum
end;
theorem Th28: :: JORDAN_A:28
for C being Simple_closed_curve
for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)}
proof
let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)}
let S be Segmentation of C; ::_thesis: (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)}
A1: Segm (S,(len S)) = Segment ((S /. (len S)),(S /. 1),C) by Def4;
len S >= 8 by Def3;
then 1 < len S by XXREAL_0:2;
then Segm (S,1) = Segment ((S /. 1),(S /. (1 + 1)),C) by Def4;
hence (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)} by A1, Def3; ::_thesis: verum
end;
theorem Th29: :: JORDAN_A:29
for C being Simple_closed_curve
for S being Segmentation of C holds Segm (S,(len S)) meets Segm (S,1)
proof
let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C holds Segm (S,(len S)) meets Segm (S,1)
let S be Segmentation of C; ::_thesis: Segm (S,(len S)) meets Segm (S,1)
(Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)} by Th28;
hence Segm (S,(len S)) meets Segm (S,1) by XBOOLE_0:def_7; ::_thesis: verum
end;
theorem Th30: :: JORDAN_A:30
for C being Simple_closed_curve
for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,((len S) -' 1))) = {(S /. (len S))}
proof
let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,((len S) -' 1))) = {(S /. (len S))}
let S be Segmentation of C; ::_thesis: (Segm (S,(len S))) /\ (Segm (S,((len S) -' 1))) = {(S /. (len S))}
A1: Segm (S,(len S)) = Segment ((S /. (len S)),(S /. 1),C) by Def4;
A2: len S >= 8 by Def3;
then len S >= 1 + 1 by XXREAL_0:2;
then A3: 1 <= (len S) -' 1 by NAT_D:55;
A4: ((len S) -' 1) + 1 = len S by A2, XREAL_1:235, XXREAL_0:2;
then (len S) -' 1 < len S by NAT_1:13;
then Segm (S,((len S) -' 1)) = Segment ((S /. ((len S) -' 1)),(S /. (len S)),C) by A3, A4, Def4;
hence (Segm (S,(len S))) /\ (Segm (S,((len S) -' 1))) = {(S /. (len S))} by A1, Def3; ::_thesis: verum
end;
theorem Th31: :: JORDAN_A:31
for C being Simple_closed_curve
for S being Segmentation of C holds Segm (S,(len S)) meets Segm (S,((len S) -' 1))
proof
let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C holds Segm (S,(len S)) meets Segm (S,((len S) -' 1))
let S be Segmentation of C; ::_thesis: Segm (S,(len S)) meets Segm (S,((len S) -' 1))
(Segm (S,(len S))) /\ (Segm (S,((len S) -' 1))) = {(S /. (len S))} by Th30;
hence Segm (S,(len S)) meets Segm (S,((len S) -' 1)) by XBOOLE_0:def_7; ::_thesis: verum
end;
begin
definition
let n be Element of NAT ;
let C be Subset of (TOP-REAL n);
func diameter C -> Real means :Def5: :: JORDAN_A:def 5
ex W being Subset of (Euclid n) st
( W = C & it = diameter W );
existence
ex b1 being Real ex W being Subset of (Euclid n) st
( W = C & b1 = diameter W )
proof
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8
.= TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) by PCOMPS_1:def_5 ;
then reconsider W = C as Subset of (Euclid n) ;
take diameter W ; ::_thesis: ex W being Subset of (Euclid n) st
( W = C & diameter W = diameter W )
take W ; ::_thesis: ( W = C & diameter W = diameter W )
thus ( W = C & diameter W = diameter W ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Real st ex W being Subset of (Euclid n) st
( W = C & b1 = diameter W ) & ex W being Subset of (Euclid n) st
( W = C & b2 = diameter W ) holds
b1 = b2;
;
end;
:: deftheorem Def5 defines diameter JORDAN_A:def_5_:_
for n being Element of NAT
for C being Subset of (TOP-REAL n)
for b3 being Real holds
( b3 = diameter C iff ex W being Subset of (Euclid n) st
( W = C & b3 = diameter W ) );
definition
let C be Simple_closed_curve;
let S be Segmentation of C;
func diameter S -> Real means :Def6: :: JORDAN_A:def 6
ex S1 being non empty finite Subset of REAL st
( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & it = max S1 );
existence
ex b1 being Real ex S1 being non empty finite Subset of REAL st
( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b1 = max S1 )
proof
deffunc H1( Element of NAT ) -> Real = diameter (Segm (S,$1));
defpred S1[ set ] means $1 in dom S;
set S1 = { H1(i) where i is Element of NAT : S1[i] } ;
set S2 = { H1(i) where i is Element of NAT : i in dom S } ;
A1: dom S is finite ;
A2: { H1(i) where i is Element of NAT : i in dom S } is finite from FRAENKEL:sch_21(A1);
A3: { H1(i) where i is Element of NAT : S1[i] } is Subset of REAL from DOMAIN_1:sch_8();
1 in dom S by FINSEQ_5:6;
then diameter (Segm (S,1)) in { H1(i) where i is Element of NAT : S1[i] } ;
then reconsider S1 = { H1(i) where i is Element of NAT : S1[i] } as non empty finite Subset of REAL by A2, A3;
reconsider mS1 = max S1 as Element of REAL by XREAL_0:def_1;
take mS1 ; ::_thesis: ex S1 being non empty finite Subset of REAL st
( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & mS1 = max S1 )
take S1 ; ::_thesis: ( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & mS1 = max S1 )
thus ( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & mS1 = max S1 ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Real st ex S1 being non empty finite Subset of REAL st
( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b1 = max S1 ) & ex S1 being non empty finite Subset of REAL st
( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b2 = max S1 ) holds
b1 = b2;
;
end;
:: deftheorem Def6 defines diameter JORDAN_A:def_6_:_
for C being Simple_closed_curve
for S being Segmentation of C
for b3 being Real holds
( b3 = diameter S iff ex S1 being non empty finite Subset of REAL st
( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & b3 = max S1 ) );
theorem :: JORDAN_A:32
for C being Simple_closed_curve
for S being Segmentation of C
for i being Element of NAT holds diameter (Segm (S,i)) <= diameter S
proof
let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C
for i being Element of NAT holds diameter (Segm (S,i)) <= diameter S
let S be Segmentation of C; ::_thesis: for i being Element of NAT holds diameter (Segm (S,i)) <= diameter S
let i be Element of NAT ; ::_thesis: diameter (Segm (S,i)) <= diameter S
consider S1 being non empty finite Subset of REAL such that
A1: S1 = { (diameter (Segm (S,j))) where j is Element of NAT : j in dom S } and
A2: diameter S = max S1 by Def6;
percases ( ( 1 <= i & i < len S ) or not 1 <= i or not i < len S ) ;
suppose ( 1 <= i & i < len S ) ; ::_thesis: diameter (Segm (S,i)) <= diameter S
then i in dom S by FINSEQ_3:25;
then diameter (Segm (S,i)) in S1 by A1;
hence diameter (Segm (S,i)) <= diameter S by A2, XXREAL_2:def_8; ::_thesis: verum
end;
supposeA3: ( not 1 <= i or not i < len S ) ; ::_thesis: diameter (Segm (S,i)) <= diameter S
A4: Segm (S,(len S)) = Segment ((S /. (len S)),(S /. 1),C) by Def4
.= Segm (S,i) by A3, Def4 ;
len S in dom S by FINSEQ_5:6;
then diameter (Segm (S,i)) in S1 by A1, A4;
hence diameter (Segm (S,i)) <= diameter S by A2, XXREAL_2:def_8; ::_thesis: verum
end;
end;
end;
theorem Th33: :: JORDAN_A:33
for C being Simple_closed_curve
for S being Segmentation of C
for e being Real st ( for i being Element of NAT holds diameter (Segm (S,i)) < e ) holds
diameter S < e
proof
let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C
for e being Real st ( for i being Element of NAT holds diameter (Segm (S,i)) < e ) holds
diameter S < e
let S be Segmentation of C; ::_thesis: for e being Real st ( for i being Element of NAT holds diameter (Segm (S,i)) < e ) holds
diameter S < e
let e be Real; ::_thesis: ( ( for i being Element of NAT holds diameter (Segm (S,i)) < e ) implies diameter S < e )
assume A1: for i being Element of NAT holds diameter (Segm (S,i)) < e ; ::_thesis: diameter S < e
consider S1 being non empty finite Subset of REAL such that
A2: S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } and
A3: diameter S = max S1 by Def6;
diameter S in S1 by A3, XXREAL_2:def_8;
then ex i being Element of NAT st
( diameter S = diameter (Segm (S,i)) & i in dom S ) by A2;
hence diameter S < e by A1; ::_thesis: verum
end;
theorem :: JORDAN_A:34
for C being Simple_closed_curve
for e being Real st e > 0 holds
ex S being Segmentation of C st diameter S < e
proof
let C be Simple_closed_curve; ::_thesis: for e being Real st e > 0 holds
ex S being Segmentation of C st diameter S < e
let e be Real; ::_thesis: ( e > 0 implies ex S being Segmentation of C st diameter S < e )
assume e > 0 ; ::_thesis: ex S being Segmentation of C st diameter S < e
then consider h being FinSequence of the carrier of (TOP-REAL 2) such that
A1: h . 1 = W-min C and
A2: h is one-to-one and
A3: 8 <= len h and
A4: rng h c= C and
A5: for i being Element of NAT st 1 <= i & i < len h holds
LE h /. i,h /. (i + 1),C and
A6: for i being Element of NAT
for W being Subset of (Euclid 2) st 1 <= i & i < len h & W = Segment ((h /. i),(h /. (i + 1)),C) holds
diameter W < e and
A7: for W being Subset of (Euclid 2) st W = Segment ((h /. (len h)),(h /. 1),C) holds
diameter W < e and
A8: for i being Element of NAT st 1 <= i & i + 1 < len h holds
(Segment ((h /. i),(h /. (i + 1)),C)) /\ (Segment ((h /. (i + 1)),(h /. (i + 2)),C)) = {(h /. (i + 1))} and
A9: (Segment ((h /. (len h)),(h /. 1),C)) /\ (Segment ((h /. 1),(h /. 2),C)) = {(h /. 1)} and
A10: (Segment ((h /. ((len h) -' 1)),(h /. (len h)),C)) /\ (Segment ((h /. (len h)),(h /. 1),C)) = {(h /. (len h))} and
A11: Segment ((h /. ((len h) -' 1)),(h /. (len h)),C) misses Segment ((h /. 1),(h /. 2),C) and
A12: for i, j being Element of NAT st 1 <= i & i < j & j < len h & not i,j are_adjacent1 holds
Segment ((h /. i),(h /. (i + 1)),C) misses Segment ((h /. j),(h /. (j + 1)),C) and
A13: for i being Element of NAT st 1 < i & i + 1 < len h holds
Segment ((h /. (len h)),(h /. 1),C) misses Segment ((h /. i),(h /. (i + 1)),C) by JORDAN7:20;
h <> {} by A3, CARD_1:27;
then 1 in dom h by FINSEQ_5:6;
then h /. 1 = W-min C by A1, PARTFUN1:def_6;
then reconsider h = h as Segmentation of C by A2, A3, A4, A5, A8, A9, A10, A11, A12, A13, Def3;
take h ; ::_thesis: diameter h < e
for i being Element of NAT holds diameter (Segm (h,i)) < e
proof
let i be Element of NAT ; ::_thesis: diameter (Segm (h,i)) < e
A14: ex W being Subset of (Euclid 2) st
( W = Segm (h,i) & diameter (Segm (h,i)) = diameter W ) by Def5;
percases ( ( 1 <= i & i < len h ) or not 1 <= i or not i < len h ) ;
supposeA15: ( 1 <= i & i < len h ) ; ::_thesis: diameter (Segm (h,i)) < e
then Segm (h,i) = Segment ((h /. i),(h /. (i + 1)),C) by Def4;
hence diameter (Segm (h,i)) < e by A6, A14, A15; ::_thesis: verum
end;
suppose ( not 1 <= i or not i < len h ) ; ::_thesis: diameter (Segm (h,i)) < e
then Segm (h,i) = Segment ((h /. (len h)),(h /. 1),C) by Def4;
hence diameter (Segm (h,i)) < e by A7, A14; ::_thesis: verum
end;
end;
end;
hence diameter h < e by Th33; ::_thesis: verum
end;
begin
definition
let C be Simple_closed_curve;
let S be Segmentation of C;
func S-Gap S -> Real means :Def7: :: JORDAN_A:def 7
ex S1, S2 being non empty finite Subset of REAL st
( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & it = min ((min S1),(min S2)) );
existence
ex b1 being Real ex S1, S2 being non empty finite Subset of REAL st
( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b1 = min ((min S1),(min S2)) )
proof
deffunc H1( Element of NAT ) -> Element of REAL = dist_min ((Segm (S,(len S))),(Segm (S,$1)));
deffunc H2( Element of NAT , Element of NAT ) -> Element of REAL = dist_min ((Segm (S,$1)),(Segm (S,$2)));
defpred S1[ Element of NAT ] means ( 1 < $1 & $1 < (len S) -' 1 );
defpred S2[ Element of NAT ] means $1 in dom S;
defpred S3[ Element of NAT , Element of NAT ] means ( 1 <= $1 & $1 < $2 & $2 < len S & not $1,$2 are_adjacent1 );
defpred S4[ Element of NAT , Element of NAT ] means ( S2[$1] & S2[$2] );
set S1 = { H2(i,j) where i, j is Element of NAT : S3[i,j] } ;
set S2 = { H1(j) where j is Element of NAT : S1[j] } ;
set B = { H2(i,j) where i, j is Element of NAT : S4[i,j] } ;
set B9 = { H2(i,j) where i, j is Element of NAT : ( i in dom S & j in dom S ) } ;
set A = { H1(j) where j is Element of NAT : S2[j] } ;
set A9 = { H1(j) where j is Element of NAT : j in dom S } ;
A1: for j being Element of NAT st S1[j] holds
S2[j]
proof
let j be Element of NAT ; ::_thesis: ( S1[j] implies S2[j] )
assume A2: 1 < j ; ::_thesis: ( not j < (len S) -' 1 or S2[j] )
A3: (len S) -' 1 <= len S by NAT_D:35;
assume j < (len S) -' 1 ; ::_thesis: S2[j]
then j < len S by A3, XXREAL_0:2;
hence S2[j] by A2, FINSEQ_3:25; ::_thesis: verum
end;
A4: { H1(j) where j is Element of NAT : S1[j] } c= { H1(j) where j is Element of NAT : S2[j] } from FRAENKEL:sch_1(A1);
A5: for i, j being Element of NAT st S3[i,j] holds
S4[i,j]
proof
let i, j be Element of NAT ; ::_thesis: ( S3[i,j] implies S4[i,j] )
assume that
A6: 1 <= i and
A7: i < j and
A8: j < len S and
not i,j are_adjacent1 ; ::_thesis: S4[i,j]
i < len S by A7, A8, XXREAL_0:2;
hence i in dom S by A6, FINSEQ_3:25; ::_thesis: S2[j]
1 < j by A6, A7, XXREAL_0:2;
hence S2[j] by A8, FINSEQ_3:25; ::_thesis: verum
end;
A9: { H2(i,j) where i, j is Element of NAT : S3[i,j] } c= { H2(i,j) where i, j is Element of NAT : S4[i,j] } from FRAENKEL:sch_2(A5);
A10: { H2(i,j) where i, j is Element of NAT : S3[i,j] } c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H2(i,j) where i, j is Element of NAT : S3[i,j] } or x in REAL )
assume x in { H2(i,j) where i, j is Element of NAT : S3[i,j] } ; ::_thesis: x in REAL
then ex i, j being Element of NAT st
( x = dist_min ((Segm (S,i)),(Segm (S,j))) & 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) ;
hence x in REAL ; ::_thesis: verum
end;
A11: { H1(j) where j is Element of NAT : S1[j] } c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H1(j) where j is Element of NAT : S1[j] } or x in REAL )
assume x in { H1(j) where j is Element of NAT : S1[j] } ; ::_thesis: x in REAL
then ex j being Element of NAT st
( x = dist_min ((Segm (S,(len S))),(Segm (S,j))) & 1 < j & j < (len S) -' 1 ) ;
hence x in REAL ; ::_thesis: verum
end;
A12: dom S is finite ;
A13: { H1(j) where j is Element of NAT : j in dom S } is finite from FRAENKEL:sch_21(A12);
A14: { H2(i,j) where i, j is Element of NAT : ( i in dom S & j in dom S ) } is finite from FRAENKEL:sch_22(A12, A12);
A15: 3 <> 1 + 1 ;
1 <> 3 + 1 ;
then A16: not 1,3 are_adjacent1 by A15, GOBRD10:def_1;
A17: len S >= 7 + 1 by Def3;
then 3 < len S by XXREAL_0:2;
then A18: dist_min ((Segm (S,1)),(Segm (S,3))) in { H2(i,j) where i, j is Element of NAT : S3[i,j] } by A16;
2 + 1 < len S by A17, XXREAL_0:2;
then 2 < (len S) -' 1 by NAT_D:52;
then dist_min ((Segm (S,(len S))),(Segm (S,2))) in { H1(j) where j is Element of NAT : S1[j] } ;
then reconsider S1 = { H2(i,j) where i, j is Element of NAT : S3[i,j] } , S2 = { H1(j) where j is Element of NAT : S1[j] } as non empty finite Subset of REAL by A4, A9, A10, A11, A13, A14, A18;
reconsider mm = min ((min S1),(min S2)) as Element of REAL by XREAL_0:def_1;
take mm ; ::_thesis: ex S1, S2 being non empty finite Subset of REAL st
( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & mm = min ((min S1),(min S2)) )
take S1 ; ::_thesis: ex S2 being non empty finite Subset of REAL st
( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & mm = min ((min S1),(min S2)) )
take S2 ; ::_thesis: ( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & mm = min ((min S1),(min S2)) )
thus ( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & mm = min ((min S1),(min S2)) ) ; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Real st ex S1, S2 being non empty finite Subset of REAL st
( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b1 = min ((min S1),(min S2)) ) & ex S1, S2 being non empty finite Subset of REAL st
( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b2 = min ((min S1),(min S2)) ) holds
b1 = b2;
;
end;
:: deftheorem Def7 defines S-Gap JORDAN_A:def_7_:_
for C being Simple_closed_curve
for S being Segmentation of C
for b3 being Real holds
( b3 = S-Gap S iff ex S1, S2 being non empty finite Subset of REAL st
( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & b3 = min ((min S1),(min S2)) ) );
theorem Th35: :: JORDAN_A:35
for C being Simple_closed_curve
for S being Segmentation of C ex F being non empty finite Subset of REAL st
( F = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } & S-Gap S = min F )
proof
let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C ex F being non empty finite Subset of REAL st
( F = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } & S-Gap S = min F )
let S be Segmentation of C; ::_thesis: ex F being non empty finite Subset of REAL st
( F = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } & S-Gap S = min F )
consider S1, S2 being non empty finite Subset of REAL such that
A1: S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 ) } and
A2: S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } and
A3: S-Gap S = min ((min S1),(min S2)) by Def7;
take F = S1 \/ S2; ::_thesis: ( F = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } & S-Gap S = min F )
set X = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } ;
thus F c= { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } :: according to XBOOLE_0:def_10 ::_thesis: ( { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } c= F & S-Gap S = min F )
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in F or e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } )
assume A4: e in F ; ::_thesis: e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) }
percases ( e in S1 or e in S2 ) by A4, XBOOLE_0:def_3;
suppose e in S1 ; ::_thesis: e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) }
then consider i, j being Element of NAT such that
A5: e = dist_min ((Segm (S,i)),(Segm (S,j))) and
A6: 1 <= i and
A7: i < j and
A8: j < len S and
A9: not i,j are_adjacent1 by A1;
Segm (S,i) misses Segm (S,j) by A6, A7, A8, A9, Th24;
hence e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } by A5, A6, A7, A8; ::_thesis: verum
end;
suppose e in S2 ; ::_thesis: e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) }
then consider j being Element of NAT such that
A10: e = dist_min ((Segm (S,(len S))),(Segm (S,j))) and
A11: 1 < j and
A12: j < (len S) -' 1 by A2;
A13: j < len S by A12, NAT_D:44;
Segm (S,(len S)) misses Segm (S,j) by A11, A12, Th25;
hence e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } by A10, A11, A13; ::_thesis: verum
end;
end;
end;
thus { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } c= F ::_thesis: S-Gap S = min F
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } or e in F )
assume e in { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } ; ::_thesis: e in F
then consider i, j being Element of NAT such that
A14: e = dist_min ((Segm (S,i)),(Segm (S,j))) and
A15: 1 <= i and
A16: i < j and
A17: j <= len S and
A18: Segm (S,i) misses Segm (S,j) ;
A19: i < len S by A16, A17, XXREAL_0:2;
percases ( j < len S or j = len S ) by A17, XXREAL_0:1;
supposeA20: j < len S ; ::_thesis: e in F
not i,j are_adjacent1 by A15, A16, A18, A20, Th27;
then e in S1 by A1, A14, A15, A16, A20;
hence e in F by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA21: j = len S ; ::_thesis: e in F
then 1 <> i by A18, Th29;
then A22: 1 < i by A15, XXREAL_0:1;
A23: i <= (len S) -' 1 by A19, NAT_D:49;
i <> (len S) -' 1 by A18, A21, Th31;
then i < (len S) -' 1 by A23, XXREAL_0:1;
then e in S2 by A2, A14, A21, A22;
hence e in F by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
thus S-Gap S = min F by A3, XXREAL_2:9; ::_thesis: verum
end;
theorem :: JORDAN_A:36
for C being Simple_closed_curve
for S being Segmentation of C holds S-Gap S > 0
proof
let C be Simple_closed_curve; ::_thesis: for S being Segmentation of C holds S-Gap S > 0
let S be Segmentation of C; ::_thesis: S-Gap S > 0
consider F being non empty finite Subset of REAL such that
A1: F = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) } and
A2: S-Gap S = min F by Th35;
S-Gap S in F by A2, XXREAL_2:def_7;
then ex i, j being Element of NAT st
( S-Gap S = dist_min ((Segm (S,i)),(Segm (S,j))) & 1 <= i & i < j & j <= len S & Segm (S,i) misses Segm (S,j) ) by A1;
hence S-Gap S > 0 by Th7; ::_thesis: verum
end;