:: JORDAN18 semantic presentation
begin
Lm1: dom proj1 = the carrier of (TOP-REAL 2)
by FUNCT_2:def_1;
Lm2: dom proj2 = the carrier of (TOP-REAL 2)
by FUNCT_2:def_1;
theorem :: JORDAN18:1
for a, b being real number holds (a - b) ^2 = (b - a) ^2 ;
theorem :: JORDAN18:2
for S, T being non empty TopStruct
for f being Function of S,T
for A being Subset of T st f is being_homeomorphism & A is compact holds
f " A is compact
proof
let S, T be non empty TopStruct ; ::_thesis: for f being Function of S,T
for A being Subset of T st f is being_homeomorphism & A is compact holds
f " A is compact
let f be Function of S,T; ::_thesis: for A being Subset of T st f is being_homeomorphism & A is compact holds
f " A is compact
let A be Subset of T; ::_thesis: ( f is being_homeomorphism & A is compact implies f " A is compact )
assume that
A1: f is being_homeomorphism and
A2: A is compact ; ::_thesis: f " A is compact
A3: ( rng f = [#] T & f is one-to-one ) by A1, TOPS_2:def_5;
f " is being_homeomorphism by A1, TOPS_2:56;
then A4: rng (f ") = [#] S by TOPS_2:def_5;
f " is continuous by A1, TOPS_2:def_5;
then (f ") .: A is compact by A2, A4, COMPTS_1:15;
hence f " A is compact by A3, TOPS_2:55; ::_thesis: verum
end;
theorem Th3: :: JORDAN18:3
for a being Point of (TOP-REAL 2) holds proj2 .: (north_halfline a) is bounded_below
proof
let a be Point of (TOP-REAL 2); ::_thesis: proj2 .: (north_halfline a) is bounded_below
take a `2 ; :: according to XXREAL_2:def_9 ::_thesis: a `2 is LowerBound of proj2 .: (north_halfline a)
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in proj2 .: (north_halfline a) or a `2 <= r )
assume r in proj2 .: (north_halfline a) ; ::_thesis: a `2 <= r
then consider x being set such that
A1: x in the carrier of (TOP-REAL 2) and
A2: x in north_halfline a and
A3: r = proj2 . x by FUNCT_2:64;
reconsider x = x as Point of (TOP-REAL 2) by A1;
r = x `2 by A3, PSCOMP_1:def_6;
hence a `2 <= r by A2, TOPREAL1:def_10; ::_thesis: verum
end;
theorem Th4: :: JORDAN18:4
for a being Point of (TOP-REAL 2) holds proj2 .: (south_halfline a) is bounded_above
proof
let a be Point of (TOP-REAL 2); ::_thesis: proj2 .: (south_halfline a) is bounded_above
take a `2 ; :: according to XXREAL_2:def_10 ::_thesis: a `2 is UpperBound of proj2 .: (south_halfline a)
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in proj2 .: (south_halfline a) or r <= a `2 )
assume r in proj2 .: (south_halfline a) ; ::_thesis: r <= a `2
then consider x being set such that
A1: x in the carrier of (TOP-REAL 2) and
A2: x in south_halfline a and
A3: r = proj2 . x by FUNCT_2:64;
reconsider x = x as Point of (TOP-REAL 2) by A1;
r = x `2 by A3, PSCOMP_1:def_6;
hence r <= a `2 by A2, TOPREAL1:def_12; ::_thesis: verum
end;
theorem Th5: :: JORDAN18:5
for a being Point of (TOP-REAL 2) holds proj1 .: (west_halfline a) is bounded_above
proof
let a be Point of (TOP-REAL 2); ::_thesis: proj1 .: (west_halfline a) is bounded_above
take a `1 ; :: according to XXREAL_2:def_10 ::_thesis: a `1 is UpperBound of proj1 .: (west_halfline a)
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in proj1 .: (west_halfline a) or r <= a `1 )
assume r in proj1 .: (west_halfline a) ; ::_thesis: r <= a `1
then consider x being set such that
A1: x in the carrier of (TOP-REAL 2) and
A2: x in west_halfline a and
A3: r = proj1 . x by FUNCT_2:64;
reconsider x = x as Point of (TOP-REAL 2) by A1;
r = x `1 by A3, PSCOMP_1:def_5;
hence r <= a `1 by A2, TOPREAL1:def_13; ::_thesis: verum
end;
theorem Th6: :: JORDAN18:6
for a being Point of (TOP-REAL 2) holds proj1 .: (east_halfline a) is bounded_below
proof
let a be Point of (TOP-REAL 2); ::_thesis: proj1 .: (east_halfline a) is bounded_below
take a `1 ; :: according to XXREAL_2:def_9 ::_thesis: a `1 is LowerBound of proj1 .: (east_halfline a)
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in proj1 .: (east_halfline a) or a `1 <= r )
assume r in proj1 .: (east_halfline a) ; ::_thesis: a `1 <= r
then consider x being set such that
A1: x in the carrier of (TOP-REAL 2) and
A2: x in east_halfline a and
A3: r = proj1 . x by FUNCT_2:64;
reconsider x = x as Point of (TOP-REAL 2) by A1;
r = x `1 by A3, PSCOMP_1:def_5;
hence a `1 <= r by A2, TOPREAL1:def_11; ::_thesis: verum
end;
registration
let a be Point of (TOP-REAL 2);
clusterproj2 .: (north_halfline a) -> non empty ;
coherence
not proj2 .: (north_halfline a) is empty by Lm2, RELAT_1:119;
clusterproj2 .: (south_halfline a) -> non empty ;
coherence
not proj2 .: (south_halfline a) is empty by Lm2, RELAT_1:119;
clusterproj1 .: (west_halfline a) -> non empty ;
coherence
not proj1 .: (west_halfline a) is empty by Lm1, RELAT_1:119;
clusterproj1 .: (east_halfline a) -> non empty ;
coherence
not proj1 .: (east_halfline a) is empty by Lm1, RELAT_1:119;
end;
theorem Th7: :: JORDAN18:7
for a being Point of (TOP-REAL 2) holds lower_bound (proj2 .: (north_halfline a)) = a `2
proof
let a be Point of (TOP-REAL 2); ::_thesis: lower_bound (proj2 .: (north_halfline a)) = a `2
set X = proj2 .: (north_halfline a);
A1: now__::_thesis:_for_r_being_real_number_st_r_in_proj2_.:_(north_halfline_a)_holds_
a_`2_<=_r
let r be real number ; ::_thesis: ( r in proj2 .: (north_halfline a) implies a `2 <= r )
assume r in proj2 .: (north_halfline a) ; ::_thesis: a `2 <= r
then consider x being set such that
A2: x in the carrier of (TOP-REAL 2) and
A3: x in north_halfline a and
A4: r = proj2 . x by FUNCT_2:64;
reconsider x = x as Point of (TOP-REAL 2) by A2;
r = x `2 by A4, PSCOMP_1:def_6;
hence a `2 <= r by A3, TOPREAL1:def_10; ::_thesis: verum
end;
A5: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_r_being_real_number_st_
(_r_in_proj2_.:_(north_halfline_a)_&_r_<_(a_`2)_+_s_)
reconsider r = a `2 as real number ;
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in proj2 .: (north_halfline a) & r < (a `2) + s ) )
assume 0 < s ; ::_thesis: ex r being real number st
( r in proj2 .: (north_halfline a) & r < (a `2) + s )
then A6: r + 0 < (a `2) + s by XREAL_1:8;
take r = r; ::_thesis: ( r in proj2 .: (north_halfline a) & r < (a `2) + s )
( a in north_halfline a & r = proj2 . a ) by PSCOMP_1:def_6, TOPREAL1:38;
hence r in proj2 .: (north_halfline a) by FUNCT_2:35; ::_thesis: r < (a `2) + s
thus r < (a `2) + s by A6; ::_thesis: verum
end;
proj2 .: (north_halfline a) is bounded_below by Th3;
hence lower_bound (proj2 .: (north_halfline a)) = a `2 by A1, A5, SEQ_4:def_2; ::_thesis: verum
end;
theorem Th8: :: JORDAN18:8
for a being Point of (TOP-REAL 2) holds upper_bound (proj2 .: (south_halfline a)) = a `2
proof
let a be Point of (TOP-REAL 2); ::_thesis: upper_bound (proj2 .: (south_halfline a)) = a `2
set X = proj2 .: (south_halfline a);
A1: now__::_thesis:_for_r_being_real_number_st_r_in_proj2_.:_(south_halfline_a)_holds_
r_<=_a_`2
let r be real number ; ::_thesis: ( r in proj2 .: (south_halfline a) implies r <= a `2 )
assume r in proj2 .: (south_halfline a) ; ::_thesis: r <= a `2
then consider x being set such that
A2: x in the carrier of (TOP-REAL 2) and
A3: x in south_halfline a and
A4: r = proj2 . x by FUNCT_2:64;
reconsider x = x as Point of (TOP-REAL 2) by A2;
r = x `2 by A4, PSCOMP_1:def_6;
hence r <= a `2 by A3, TOPREAL1:def_12; ::_thesis: verum
end;
A5: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_r_being_real_number_st_
(_r_in_proj2_.:_(south_halfline_a)_&_(a_`2)_-_s_<_r_)
reconsider r = a `2 as real number ;
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in proj2 .: (south_halfline a) & (a `2) - s < r ) )
assume 0 < s ; ::_thesis: ex r being real number st
( r in proj2 .: (south_halfline a) & (a `2) - s < r )
then A6: (a `2) - s < r - 0 by XREAL_1:15;
take r = r; ::_thesis: ( r in proj2 .: (south_halfline a) & (a `2) - s < r )
( a in south_halfline a & r = proj2 . a ) by PSCOMP_1:def_6, TOPREAL1:38;
hence r in proj2 .: (south_halfline a) by FUNCT_2:35; ::_thesis: (a `2) - s < r
thus (a `2) - s < r by A6; ::_thesis: verum
end;
proj2 .: (south_halfline a) is bounded_above by Th4;
hence upper_bound (proj2 .: (south_halfline a)) = a `2 by A1, A5, SEQ_4:def_1; ::_thesis: verum
end;
theorem :: JORDAN18:9
for a being Point of (TOP-REAL 2) holds upper_bound (proj1 .: (west_halfline a)) = a `1
proof
let a be Point of (TOP-REAL 2); ::_thesis: upper_bound (proj1 .: (west_halfline a)) = a `1
set X = proj1 .: (west_halfline a);
A1: now__::_thesis:_for_r_being_real_number_st_r_in_proj1_.:_(west_halfline_a)_holds_
r_<=_a_`1
let r be real number ; ::_thesis: ( r in proj1 .: (west_halfline a) implies r <= a `1 )
assume r in proj1 .: (west_halfline a) ; ::_thesis: r <= a `1
then consider x being set such that
A2: x in the carrier of (TOP-REAL 2) and
A3: x in west_halfline a and
A4: r = proj1 . x by FUNCT_2:64;
reconsider x = x as Point of (TOP-REAL 2) by A2;
r = x `1 by A4, PSCOMP_1:def_5;
hence r <= a `1 by A3, TOPREAL1:def_13; ::_thesis: verum
end;
A5: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_r_being_real_number_st_
(_r_in_proj1_.:_(west_halfline_a)_&_(a_`1)_-_s_<_r_)
reconsider r = a `1 as real number ;
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in proj1 .: (west_halfline a) & (a `1) - s < r ) )
assume 0 < s ; ::_thesis: ex r being real number st
( r in proj1 .: (west_halfline a) & (a `1) - s < r )
then A6: (a `1) - s < r - 0 by XREAL_1:15;
take r = r; ::_thesis: ( r in proj1 .: (west_halfline a) & (a `1) - s < r )
( a in west_halfline a & r = proj1 . a ) by PSCOMP_1:def_5, TOPREAL1:38;
hence r in proj1 .: (west_halfline a) by FUNCT_2:35; ::_thesis: (a `1) - s < r
thus (a `1) - s < r by A6; ::_thesis: verum
end;
proj1 .: (west_halfline a) is bounded_above by Th5;
hence upper_bound (proj1 .: (west_halfline a)) = a `1 by A1, A5, SEQ_4:def_1; ::_thesis: verum
end;
theorem :: JORDAN18:10
for a being Point of (TOP-REAL 2) holds lower_bound (proj1 .: (east_halfline a)) = a `1
proof
let a be Point of (TOP-REAL 2); ::_thesis: lower_bound (proj1 .: (east_halfline a)) = a `1
set X = proj1 .: (east_halfline a);
A1: now__::_thesis:_for_r_being_real_number_st_r_in_proj1_.:_(east_halfline_a)_holds_
a_`1_<=_r
let r be real number ; ::_thesis: ( r in proj1 .: (east_halfline a) implies a `1 <= r )
assume r in proj1 .: (east_halfline a) ; ::_thesis: a `1 <= r
then consider x being set such that
A2: x in the carrier of (TOP-REAL 2) and
A3: x in east_halfline a and
A4: r = proj1 . x by FUNCT_2:64;
reconsider x = x as Point of (TOP-REAL 2) by A2;
r = x `1 by A4, PSCOMP_1:def_5;
hence a `1 <= r by A3, TOPREAL1:def_11; ::_thesis: verum
end;
A5: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_r_being_real_number_st_
(_r_in_proj1_.:_(east_halfline_a)_&_r_<_(a_`1)_+_s_)
reconsider r = a `1 as real number ;
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in proj1 .: (east_halfline a) & r < (a `1) + s ) )
assume 0 < s ; ::_thesis: ex r being real number st
( r in proj1 .: (east_halfline a) & r < (a `1) + s )
then A6: r + 0 < (a `1) + s by XREAL_1:8;
take r = r; ::_thesis: ( r in proj1 .: (east_halfline a) & r < (a `1) + s )
( a in east_halfline a & r = proj1 . a ) by PSCOMP_1:def_5, TOPREAL1:38;
hence r in proj1 .: (east_halfline a) by FUNCT_2:35; ::_thesis: r < (a `1) + s
thus r < (a `1) + s by A6; ::_thesis: verum
end;
proj1 .: (east_halfline a) is bounded_below by Th6;
hence lower_bound (proj1 .: (east_halfline a)) = a `1 by A1, A5, SEQ_4:def_2; ::_thesis: verum
end;
Lm3: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by EUCLID:def_8;
registration
let a be Point of (TOP-REAL 2);
cluster north_halfline a -> closed ;
coherence
north_halfline a is closed
proof
set X = north_halfline a;
reconsider XX = (north_halfline a) ` as Subset of (TOP-REAL 2) ;
reconsider OO = XX as Subset of (TopSpaceMetr (Euclid 2)) by Lm3;
for p being Point of (Euclid 2) st p in (north_halfline a) ` holds
ex r being real number st
( r > 0 & Ball (p,r) c= (north_halfline a) ` )
proof
let p be Point of (Euclid 2); ::_thesis: ( p in (north_halfline a) ` implies ex r being real number st
( r > 0 & Ball (p,r) c= (north_halfline a) ` ) )
reconsider x = p as Point of (TOP-REAL 2) by EUCLID:67;
assume p in (north_halfline a) ` ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (north_halfline a) ` )
then A1: not p in north_halfline a by XBOOLE_0:def_5;
percases ( x `1 <> a `1 or x `2 < a `2 ) by A1, TOPREAL1:def_10;
supposeA2: x `1 <> a `1 ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (north_halfline a) ` )
take r = abs ((x `1) - (a `1)); ::_thesis: ( r > 0 & Ball (p,r) c= (north_halfline a) ` )
(x `1) - (a `1) <> 0 by A2;
hence r > 0 by COMPLEX1:47; ::_thesis: Ball (p,r) c= (north_halfline a) `
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (north_halfline a) ` )
assume A3: b in Ball (p,r) ; ::_thesis: b in (north_halfline a) `
then reconsider bb = b as Point of (Euclid 2) ;
reconsider c = bb as Point of (TOP-REAL 2) by EUCLID:67;
dist (p,bb) < r by A3, METRIC_1:11;
then A4: dist (x,c) < r by TOPREAL6:def_1;
now__::_thesis:_not_c_`1_=_a_`1
assume c `1 = a `1 ; ::_thesis: contradiction
then A5: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < abs ((x `1) - (c `1)) by A4, TOPREAL6:92;
A6: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63;
A7: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63;
then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A6, SQUARE_1:def_2;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < (abs ((x `1) - (c `1))) ^2 by A5, SQUARE_1:16;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `1) - (c `1)) ^2 by COMPLEX1:75;
then (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < (((x `1) - (c `1)) ^2) + 0 by A6, SQUARE_1:def_2;
hence contradiction by A7, XREAL_1:7; ::_thesis: verum
end;
then not c in north_halfline a by TOPREAL1:def_10;
hence b in (north_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum
end;
supposeA8: x `2 < a `2 ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (north_halfline a) ` )
take r = (a `2) - (x `2); ::_thesis: ( r > 0 & Ball (p,r) c= (north_halfline a) ` )
thus r > 0 by A8, XREAL_1:50; ::_thesis: Ball (p,r) c= (north_halfline a) `
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (north_halfline a) ` )
assume A9: b in Ball (p,r) ; ::_thesis: b in (north_halfline a) `
then reconsider b = b as Point of (Euclid 2) ;
reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67;
dist (p,b) < r by A9, METRIC_1:11;
then A10: dist (x,c) < r by TOPREAL6:def_1;
now__::_thesis:_not_c_`2_>=_a_`2
assume c `2 >= a `2 ; ::_thesis: contradiction
then A11: (a `2) - (x `2) <= (c `2) - (x `2) by XREAL_1:13;
0 <= (a `2) - (x `2) by A8, XREAL_1:50;
then A12: ((a `2) - (x `2)) ^2 <= ((c `2) - (x `2)) ^2 by A11, SQUARE_1:15;
A13: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63;
A14: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < (a `2) - (x `2) by A10, TOPREAL6:92;
A15: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63;
then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A13, SQUARE_1:def_2;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((a `2) - (x `2)) ^2 by A14, SQUARE_1:16;
then A16: (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < ((a `2) - (x `2)) ^2 by A13, A15, SQUARE_1:def_2;
0 + (((x `2) - (c `2)) ^2) <= (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) by A13, XREAL_1:7;
hence contradiction by A16, A12, XXREAL_0:2; ::_thesis: verum
end;
then not c in north_halfline a by TOPREAL1:def_10;
hence b in (north_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
then OO is open by TOPMETR:15;
then XX is open by Lm3, PRE_TOPC:30;
then XX ` is closed ;
hence north_halfline a is closed ; ::_thesis: verum
end;
cluster south_halfline a -> closed ;
coherence
south_halfline a is closed
proof
set X = south_halfline a;
reconsider XX = (south_halfline a) ` as Subset of (TOP-REAL 2) ;
reconsider OO = XX as Subset of (TopSpaceMetr (Euclid 2)) by Lm3;
for p being Point of (Euclid 2) st p in (south_halfline a) ` holds
ex r being real number st
( r > 0 & Ball (p,r) c= (south_halfline a) ` )
proof
let p be Point of (Euclid 2); ::_thesis: ( p in (south_halfline a) ` implies ex r being real number st
( r > 0 & Ball (p,r) c= (south_halfline a) ` ) )
reconsider x = p as Point of (TOP-REAL 2) by EUCLID:67;
assume p in (south_halfline a) ` ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (south_halfline a) ` )
then A17: not p in south_halfline a by XBOOLE_0:def_5;
percases ( x `1 <> a `1 or x `2 > a `2 ) by A17, TOPREAL1:def_12;
supposeA18: x `1 <> a `1 ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (south_halfline a) ` )
take r = abs ((x `1) - (a `1)); ::_thesis: ( r > 0 & Ball (p,r) c= (south_halfline a) ` )
(x `1) - (a `1) <> 0 by A18;
hence r > 0 by COMPLEX1:47; ::_thesis: Ball (p,r) c= (south_halfline a) `
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (south_halfline a) ` )
assume A19: b in Ball (p,r) ; ::_thesis: b in (south_halfline a) `
then reconsider b = b as Point of (Euclid 2) ;
reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67;
dist (p,b) < r by A19, METRIC_1:11;
then A20: dist (x,c) < r by TOPREAL6:def_1;
now__::_thesis:_not_c_`1_=_a_`1
assume c `1 = a `1 ; ::_thesis: contradiction
then A21: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < abs ((x `1) - (c `1)) by A20, TOPREAL6:92;
A22: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63;
A23: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63;
then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A22, SQUARE_1:def_2;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < (abs ((x `1) - (c `1))) ^2 by A21, SQUARE_1:16;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `1) - (c `1)) ^2 by COMPLEX1:75;
then (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < (((x `1) - (c `1)) ^2) + 0 by A22, SQUARE_1:def_2;
hence contradiction by A23, XREAL_1:7; ::_thesis: verum
end;
then not c in south_halfline a by TOPREAL1:def_12;
hence b in (south_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum
end;
supposeA24: x `2 > a `2 ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (south_halfline a) ` )
take r = (x `2) - (a `2); ::_thesis: ( r > 0 & Ball (p,r) c= (south_halfline a) ` )
thus r > 0 by A24, XREAL_1:50; ::_thesis: Ball (p,r) c= (south_halfline a) `
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (south_halfline a) ` )
assume A25: b in Ball (p,r) ; ::_thesis: b in (south_halfline a) `
then reconsider b = b as Point of (Euclid 2) ;
reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67;
dist (p,b) < r by A25, METRIC_1:11;
then A26: dist (x,c) < r by TOPREAL6:def_1;
now__::_thesis:_not_c_`2_<=_a_`2
assume c `2 <= a `2 ; ::_thesis: contradiction
then A27: (x `2) - (c `2) >= (x `2) - (a `2) by XREAL_1:13;
0 <= (x `2) - (a `2) by A24, XREAL_1:50;
then A28: ((x `2) - (a `2)) ^2 <= ((x `2) - (c `2)) ^2 by A27, SQUARE_1:15;
A29: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63;
A30: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < (x `2) - (a `2) by A26, TOPREAL6:92;
A31: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63;
then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A29, SQUARE_1:def_2;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `2) - (a `2)) ^2 by A30, SQUARE_1:16;
then A32: (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < ((x `2) - (a `2)) ^2 by A29, A31, SQUARE_1:def_2;
0 + (((x `2) - (c `2)) ^2) <= (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) by A29, XREAL_1:7;
hence contradiction by A32, A28, XXREAL_0:2; ::_thesis: verum
end;
then not c in south_halfline a by TOPREAL1:def_12;
hence b in (south_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
then OO is open by TOPMETR:15;
then XX is open by Lm3, PRE_TOPC:30;
then XX ` is closed ;
hence south_halfline a is closed ; ::_thesis: verum
end;
cluster east_halfline a -> closed ;
coherence
east_halfline a is closed
proof
set X = east_halfline a;
reconsider XX = (east_halfline a) ` as Subset of (TOP-REAL 2) ;
reconsider OO = XX as Subset of (TopSpaceMetr (Euclid 2)) by Lm3;
for p being Point of (Euclid 2) st p in (east_halfline a) ` holds
ex r being real number st
( r > 0 & Ball (p,r) c= (east_halfline a) ` )
proof
let p be Point of (Euclid 2); ::_thesis: ( p in (east_halfline a) ` implies ex r being real number st
( r > 0 & Ball (p,r) c= (east_halfline a) ` ) )
reconsider x = p as Point of (TOP-REAL 2) by EUCLID:67;
assume p in (east_halfline a) ` ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (east_halfline a) ` )
then A33: not p in east_halfline a by XBOOLE_0:def_5;
percases ( x `2 <> a `2 or x `1 < a `1 ) by A33, TOPREAL1:def_11;
supposeA34: x `2 <> a `2 ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (east_halfline a) ` )
take r = abs ((x `2) - (a `2)); ::_thesis: ( r > 0 & Ball (p,r) c= (east_halfline a) ` )
(x `2) - (a `2) <> 0 by A34;
hence r > 0 by COMPLEX1:47; ::_thesis: Ball (p,r) c= (east_halfline a) `
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (east_halfline a) ` )
assume A35: b in Ball (p,r) ; ::_thesis: b in (east_halfline a) `
then reconsider b = b as Point of (Euclid 2) ;
reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67;
dist (p,b) < r by A35, METRIC_1:11;
then A36: dist (x,c) < r by TOPREAL6:def_1;
now__::_thesis:_not_c_`2_=_a_`2
assume c `2 = a `2 ; ::_thesis: contradiction
then A37: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < abs ((x `2) - (c `2)) by A36, TOPREAL6:92;
A38: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63;
A39: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63;
then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A38, SQUARE_1:def_2;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < (abs ((x `2) - (c `2))) ^2 by A37, SQUARE_1:16;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `2) - (c `2)) ^2 by COMPLEX1:75;
then (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < (((x `2) - (c `2)) ^2) + 0 by A38, SQUARE_1:def_2;
hence contradiction by A39, XREAL_1:7; ::_thesis: verum
end;
then not c in east_halfline a by TOPREAL1:def_11;
hence b in (east_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum
end;
supposeA40: x `1 < a `1 ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (east_halfline a) ` )
take r = (a `1) - (x `1); ::_thesis: ( r > 0 & Ball (p,r) c= (east_halfline a) ` )
thus r > 0 by A40, XREAL_1:50; ::_thesis: Ball (p,r) c= (east_halfline a) `
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (east_halfline a) ` )
assume A41: b in Ball (p,r) ; ::_thesis: b in (east_halfline a) `
then reconsider b = b as Point of (Euclid 2) ;
reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67;
dist (p,b) < r by A41, METRIC_1:11;
then A42: dist (x,c) < r by TOPREAL6:def_1;
now__::_thesis:_not_c_`1_>=_a_`1
assume c `1 >= a `1 ; ::_thesis: contradiction
then A43: (a `1) - (x `1) <= (c `1) - (x `1) by XREAL_1:13;
0 <= (a `1) - (x `1) by A40, XREAL_1:50;
then A44: ((a `1) - (x `1)) ^2 <= ((c `1) - (x `1)) ^2 by A43, SQUARE_1:15;
A45: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63;
A46: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < (a `1) - (x `1) by A42, TOPREAL6:92;
A47: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63;
then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A45, SQUARE_1:def_2;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((a `1) - (x `1)) ^2 by A46, SQUARE_1:16;
then A48: (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < ((a `1) - (x `1)) ^2 by A45, A47, SQUARE_1:def_2;
(((x `1) - (c `1)) ^2) + 0 <= (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) by A45, XREAL_1:7;
hence contradiction by A48, A44, XXREAL_0:2; ::_thesis: verum
end;
then not c in east_halfline a by TOPREAL1:def_11;
hence b in (east_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
then OO is open by TOPMETR:15;
then XX is open by Lm3, PRE_TOPC:30;
then XX ` is closed ;
hence east_halfline a is closed ; ::_thesis: verum
end;
cluster west_halfline a -> closed ;
coherence
west_halfline a is closed
proof
set X = west_halfline a;
reconsider XX = (west_halfline a) ` as Subset of (TOP-REAL 2) ;
reconsider OO = XX as Subset of (TopSpaceMetr (Euclid 2)) by Lm3;
for p being Point of (Euclid 2) st p in (west_halfline a) ` holds
ex r being real number st
( r > 0 & Ball (p,r) c= (west_halfline a) ` )
proof
let p be Point of (Euclid 2); ::_thesis: ( p in (west_halfline a) ` implies ex r being real number st
( r > 0 & Ball (p,r) c= (west_halfline a) ` ) )
reconsider x = p as Point of (TOP-REAL 2) by EUCLID:67;
assume p in (west_halfline a) ` ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (west_halfline a) ` )
then A49: not p in west_halfline a by XBOOLE_0:def_5;
percases ( x `2 <> a `2 or x `1 > a `1 ) by A49, TOPREAL1:def_13;
supposeA50: x `2 <> a `2 ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (west_halfline a) ` )
take r = abs ((x `2) - (a `2)); ::_thesis: ( r > 0 & Ball (p,r) c= (west_halfline a) ` )
(x `2) - (a `2) <> 0 by A50;
hence r > 0 by COMPLEX1:47; ::_thesis: Ball (p,r) c= (west_halfline a) `
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (west_halfline a) ` )
assume A51: b in Ball (p,r) ; ::_thesis: b in (west_halfline a) `
then reconsider b = b as Point of (Euclid 2) ;
reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67;
dist (p,b) < r by A51, METRIC_1:11;
then A52: dist (x,c) < r by TOPREAL6:def_1;
now__::_thesis:_not_c_`2_=_a_`2
assume c `2 = a `2 ; ::_thesis: contradiction
then A53: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < abs ((x `2) - (c `2)) by A52, TOPREAL6:92;
A54: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63;
A55: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63;
then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A54, SQUARE_1:def_2;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < (abs ((x `2) - (c `2))) ^2 by A53, SQUARE_1:16;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `2) - (c `2)) ^2 by COMPLEX1:75;
then (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < (((x `2) - (c `2)) ^2) + 0 by A54, SQUARE_1:def_2;
hence contradiction by A55, XREAL_1:7; ::_thesis: verum
end;
then not c in west_halfline a by TOPREAL1:def_13;
hence b in (west_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum
end;
supposeA56: x `1 > a `1 ; ::_thesis: ex r being real number st
( r > 0 & Ball (p,r) c= (west_halfline a) ` )
take r = (x `1) - (a `1); ::_thesis: ( r > 0 & Ball (p,r) c= (west_halfline a) ` )
thus r > 0 by A56, XREAL_1:50; ::_thesis: Ball (p,r) c= (west_halfline a) `
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Ball (p,r) or b in (west_halfline a) ` )
assume A57: b in Ball (p,r) ; ::_thesis: b in (west_halfline a) `
then reconsider b = b as Point of (Euclid 2) ;
reconsider c = b as Point of (TOP-REAL 2) by EUCLID:67;
dist (p,b) < r by A57, METRIC_1:11;
then A58: dist (x,c) < r by TOPREAL6:def_1;
now__::_thesis:_not_c_`1_<=_a_`1
assume c `1 <= a `1 ; ::_thesis: contradiction
then A59: (x `1) - (c `1) >= (x `1) - (a `1) by XREAL_1:13;
0 <= (x `1) - (a `1) by A56, XREAL_1:50;
then A60: ((x `1) - (a `1)) ^2 <= ((x `1) - (c `1)) ^2 by A59, SQUARE_1:15;
A61: 0 <= ((x `2) - (c `2)) ^2 by XREAL_1:63;
A62: sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) < (x `1) - (a `1) by A58, TOPREAL6:92;
A63: 0 <= ((x `1) - (c `1)) ^2 by XREAL_1:63;
then 0 <= sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2)) by A61, SQUARE_1:def_2;
then (sqrt ((((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2))) ^2 < ((x `1) - (a `1)) ^2 by A62, SQUARE_1:16;
then A64: (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) < ((x `1) - (a `1)) ^2 by A61, A63, SQUARE_1:def_2;
0 + (((x `1) - (c `1)) ^2) <= (((x `1) - (c `1)) ^2) + (((x `2) - (c `2)) ^2) by A61, XREAL_1:7;
hence contradiction by A64, A60, XXREAL_0:2; ::_thesis: verum
end;
then not c in west_halfline a by TOPREAL1:def_13;
hence b in (west_halfline a) ` by XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
then OO is open by TOPMETR:15;
then XX is open by Lm3, PRE_TOPC:30;
then XX ` is closed ;
hence west_halfline a is closed ; ::_thesis: verum
end;
end;
theorem Th11: :: JORDAN18:11
for P being Subset of (TOP-REAL 2)
for a being Point of (TOP-REAL 2) st a in BDD P holds
not north_halfline a c= UBD P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for a being Point of (TOP-REAL 2) st a in BDD P holds
not north_halfline a c= UBD P
let a be Point of (TOP-REAL 2); ::_thesis: ( a in BDD P implies not north_halfline a c= UBD P )
A1: ( BDD P misses UBD P & a in north_halfline a ) by JORDAN2C:24, TOPREAL1:38;
assume a in BDD P ; ::_thesis: not north_halfline a c= UBD P
hence not north_halfline a c= UBD P by A1, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th12: :: JORDAN18:12
for P being Subset of (TOP-REAL 2)
for a being Point of (TOP-REAL 2) st a in BDD P holds
not south_halfline a c= UBD P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for a being Point of (TOP-REAL 2) st a in BDD P holds
not south_halfline a c= UBD P
let a be Point of (TOP-REAL 2); ::_thesis: ( a in BDD P implies not south_halfline a c= UBD P )
A1: ( BDD P misses UBD P & a in south_halfline a ) by JORDAN2C:24, TOPREAL1:38;
assume a in BDD P ; ::_thesis: not south_halfline a c= UBD P
hence not south_halfline a c= UBD P by A1, XBOOLE_0:3; ::_thesis: verum
end;
theorem :: JORDAN18:13
for P being Subset of (TOP-REAL 2)
for a being Point of (TOP-REAL 2) st a in BDD P holds
not east_halfline a c= UBD P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for a being Point of (TOP-REAL 2) st a in BDD P holds
not east_halfline a c= UBD P
let a be Point of (TOP-REAL 2); ::_thesis: ( a in BDD P implies not east_halfline a c= UBD P )
A1: ( BDD P misses UBD P & a in east_halfline a ) by JORDAN2C:24, TOPREAL1:38;
assume a in BDD P ; ::_thesis: not east_halfline a c= UBD P
hence not east_halfline a c= UBD P by A1, XBOOLE_0:3; ::_thesis: verum
end;
theorem :: JORDAN18:14
for P being Subset of (TOP-REAL 2)
for a being Point of (TOP-REAL 2) st a in BDD P holds
not west_halfline a c= UBD P
proof
let P be Subset of (TOP-REAL 2); ::_thesis: for a being Point of (TOP-REAL 2) st a in BDD P holds
not west_halfline a c= UBD P
let a be Point of (TOP-REAL 2); ::_thesis: ( a in BDD P implies not west_halfline a c= UBD P )
A1: ( BDD P misses UBD P & a in west_halfline a ) by JORDAN2C:24, TOPREAL1:38;
assume a in BDD P ; ::_thesis: not west_halfline a c= UBD P
hence not west_halfline a c= UBD P by A1, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th15: :: JORDAN18:15
for C being Simple_closed_curve
for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P c= C holds
ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )
proof
let C be Simple_closed_curve; ::_thesis: for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P c= C holds
ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )
let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P c= C holds
ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_an_arc_of p1,p2 & P c= C implies ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} ) )
assume that
A1: P is_an_arc_of p1,p2 and
A2: P c= C ; ::_thesis: ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )
A3: p1 <> p2 by A1, JORDAN6:37;
( p1 in P & p2 in P ) by A1, TOPREAL1:1;
then consider P1, P2 being non empty Subset of (TOP-REAL 2) such that
A4: P1 is_an_arc_of p1,p2 and
A5: P2 is_an_arc_of p1,p2 and
A6: C = P1 \/ P2 and
A7: P1 /\ P2 = {p1,p2} by A2, A3, TOPREAL2:5;
reconsider P1 = P1, P2 = P2 as non empty Subset of (TOP-REAL 2) ;
A8: ( P1 c= C & P2 c= C ) by A6, XBOOLE_1:7;
A9: now__::_thesis:_not_P1_=_P2
assume A10: P1 = P2 ; ::_thesis: contradiction
ex p3 being Point of (TOP-REAL 2) st
( p3 in P1 & p3 <> p1 & p3 <> p2 ) by A4, JORDAN6:42;
hence contradiction by A7, A10, TARSKI:def_2; ::_thesis: verum
end;
percases ( P = P1 or P = P2 ) by A1, A2, A4, A5, A8, A9, JORDAN16:14;
supposeA11: P = P1 ; ::_thesis: ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )
take P2 ; ::_thesis: ( P2 is_an_arc_of p1,p2 & P \/ P2 = C & P /\ P2 = {p1,p2} )
thus ( P2 is_an_arc_of p1,p2 & P \/ P2 = C & P /\ P2 = {p1,p2} ) by A5, A6, A7, A11; ::_thesis: verum
end;
supposeA12: P = P2 ; ::_thesis: ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )
take P1 ; ::_thesis: ( P1 is_an_arc_of p1,p2 & P \/ P1 = C & P /\ P1 = {p1,p2} )
thus ( P1 is_an_arc_of p1,p2 & P \/ P1 = C & P /\ P1 = {p1,p2} ) by A4, A6, A7, A12; ::_thesis: verum
end;
end;
end;
begin
definition
let p be Point of (TOP-REAL 2);
let P be Subset of (TOP-REAL 2);
func North-Bound (p,P) -> Point of (TOP-REAL 2) equals :: JORDAN18:def 1
|[(p `1),(lower_bound (proj2 .: (P /\ (north_halfline p))))]|;
correctness
coherence
|[(p `1),(lower_bound (proj2 .: (P /\ (north_halfline p))))]| is Point of (TOP-REAL 2);
;
func South-Bound (p,P) -> Point of (TOP-REAL 2) equals :: JORDAN18:def 2
|[(p `1),(upper_bound (proj2 .: (P /\ (south_halfline p))))]|;
correctness
coherence
|[(p `1),(upper_bound (proj2 .: (P /\ (south_halfline p))))]| is Point of (TOP-REAL 2);
;
end;
:: deftheorem defines North-Bound JORDAN18:def_1_:_
for p being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) holds North-Bound (p,P) = |[(p `1),(lower_bound (proj2 .: (P /\ (north_halfline p))))]|;
:: deftheorem defines South-Bound JORDAN18:def_2_:_
for p being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) holds South-Bound (p,P) = |[(p `1),(upper_bound (proj2 .: (P /\ (south_halfline p))))]|;
theorem :: JORDAN18:16
for P being Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) holds
( (North-Bound (p,P)) `1 = p `1 & (South-Bound (p,P)) `1 = p `1 ) by EUCLID:52;
theorem Th17: :: JORDAN18:17
for p being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p & South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p )
proof
let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p & South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p )
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C implies ( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p & South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p ) )
set X = C /\ (north_halfline p);
C /\ (north_halfline p) c= C by XBOOLE_1:17;
then proj2 .: (C /\ (north_halfline p)) is real-bounded by JCT_MISC:14, RLTOPSP1:42;
then A1: proj2 .: (C /\ (north_halfline p)) is bounded_below by XXREAL_2:def_11;
assume A2: p in BDD C ; ::_thesis: ( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p & South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p )
then not north_halfline p c= UBD C by Th11;
then north_halfline p meets C by JORDAN2C:129;
then A3: not C /\ (north_halfline p) is empty by XBOOLE_0:def_7;
C /\ (north_halfline p) is bounded by RLTOPSP1:42, XBOOLE_1:17;
then proj2 .: (C /\ (north_halfline p)) is closed by JCT_MISC:13;
then lower_bound (proj2 .: (C /\ (north_halfline p))) in proj2 .: (C /\ (north_halfline p)) by A3, A1, Lm2, RCOMP_1:13, RELAT_1:119;
then consider x being set such that
A4: x in the carrier of (TOP-REAL 2) and
A5: x in C /\ (north_halfline p) and
A6: lower_bound (proj2 .: (C /\ (north_halfline p))) = proj2 . x by FUNCT_2:64;
reconsider x = x as Point of (TOP-REAL 2) by A4;
A7: x `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) by A6, PSCOMP_1:def_6
.= (North-Bound (p,C)) `2 by EUCLID:52 ;
x in north_halfline p by A5, XBOOLE_0:def_4;
then x `1 = p `1 by TOPREAL1:def_10
.= (North-Bound (p,C)) `1 by EUCLID:52 ;
then x = North-Bound (p,C) by A7, TOPREAL3:6;
hence ( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p ) by A5, XBOOLE_0:def_4; ::_thesis: ( South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p )
set X = C /\ (south_halfline p);
C /\ (south_halfline p) c= C by XBOOLE_1:17;
then proj2 .: (C /\ (south_halfline p)) is real-bounded by JCT_MISC:14, RLTOPSP1:42;
then A8: proj2 .: (C /\ (south_halfline p)) is bounded_above by XXREAL_2:def_11;
not south_halfline p c= UBD C by A2, Th12;
then south_halfline p meets C by JORDAN2C:128;
then A9: not C /\ (south_halfline p) is empty by XBOOLE_0:def_7;
C /\ (south_halfline p) is bounded by RLTOPSP1:42, XBOOLE_1:17;
then proj2 .: (C /\ (south_halfline p)) is closed by JCT_MISC:13;
then upper_bound (proj2 .: (C /\ (south_halfline p))) in proj2 .: (C /\ (south_halfline p)) by A9, A8, Lm2, RCOMP_1:12, RELAT_1:119;
then consider x being set such that
A10: x in the carrier of (TOP-REAL 2) and
A11: x in C /\ (south_halfline p) and
A12: upper_bound (proj2 .: (C /\ (south_halfline p))) = proj2 . x by FUNCT_2:64;
reconsider x = x as Point of (TOP-REAL 2) by A10;
x in south_halfline p by A11, XBOOLE_0:def_4;
then A13: x `1 = p `1 by TOPREAL1:def_12
.= (South-Bound (p,C)) `1 by EUCLID:52 ;
x `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) by A12, PSCOMP_1:def_6
.= (South-Bound (p,C)) `2 by EUCLID:52 ;
then x = South-Bound (p,C) by A13, TOPREAL3:6;
hence ( South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p ) by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th18: :: JORDAN18:18
for p being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 )
proof
let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 )
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C implies ( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 ) )
assume A1: p in BDD C ; ::_thesis: ( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 )
then ( South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p ) by Th17;
then South-Bound (p,C) in C /\ (south_halfline p) by XBOOLE_0:def_4;
then A2: not proj2 .: (C /\ (south_halfline p)) is empty by Lm2, RELAT_1:119;
A3: BDD C misses C by JORDAN1A:7;
A4: now__::_thesis:_not_(South-Bound_(p,C))_`2_=_p_`2
A5: (South-Bound (p,C)) `1 = p `1 by EUCLID:52;
assume (South-Bound (p,C)) `2 = p `2 ; ::_thesis: contradiction
then South-Bound (p,C) = p by A5, TOPREAL3:6;
then p in C by A1, Th17;
hence contradiction by A1, A3, XBOOLE_0:3; ::_thesis: verum
end;
( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p ) by A1, Th17;
then not C /\ (north_halfline p) is empty by XBOOLE_0:def_4;
then A6: not proj2 .: (C /\ (north_halfline p)) is empty by Lm2, RELAT_1:119;
( proj2 .: (south_halfline p) is bounded_above & C /\ (south_halfline p) c= south_halfline p ) by Th4, XBOOLE_1:17;
then A7: upper_bound (proj2 .: (C /\ (south_halfline p))) <= upper_bound (proj2 .: (south_halfline p)) by A2, RELAT_1:123, SEQ_4:48;
A8: now__::_thesis:_not_(North-Bound_(p,C))_`2_=_p_`2
A9: (North-Bound (p,C)) `1 = p `1 by EUCLID:52;
assume (North-Bound (p,C)) `2 = p `2 ; ::_thesis: contradiction
then North-Bound (p,C) = p by A9, TOPREAL3:6;
then p in C by A1, Th17;
hence contradiction by A1, A3, XBOOLE_0:3; ::_thesis: verum
end;
( (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) & upper_bound (proj2 .: (south_halfline p)) = p `2 ) by Th8, EUCLID:52;
hence (South-Bound (p,C)) `2 < p `2 by A7, A4, XXREAL_0:1; ::_thesis: p `2 < (North-Bound (p,C)) `2
( proj2 .: (north_halfline p) is bounded_below & C /\ (north_halfline p) c= north_halfline p ) by Th3, XBOOLE_1:17;
then A10: lower_bound (proj2 .: (C /\ (north_halfline p))) >= lower_bound (proj2 .: (north_halfline p)) by A6, RELAT_1:123, SEQ_4:47;
( lower_bound (proj2 .: (north_halfline p)) = p `2 & (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) ) by Th7, EUCLID:52;
hence p `2 < (North-Bound (p,C)) `2 by A10, A8, XXREAL_0:1; ::_thesis: verum
end;
theorem Th19: :: JORDAN18:19
for p being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p)))
proof
let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p)))
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C implies lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p))) )
assume p in BDD C ; ::_thesis: lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p)))
then A1: ( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 ) by Th18;
( (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) & (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) ) by EUCLID:52;
hence lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p))) by A1, XXREAL_0:2; ::_thesis: verum
end;
theorem :: JORDAN18:20
for p being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
South-Bound (p,C) <> North-Bound (p,C)
proof
let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
South-Bound (p,C) <> North-Bound (p,C)
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C implies South-Bound (p,C) <> North-Bound (p,C) )
assume A1: p in BDD C ; ::_thesis: South-Bound (p,C) <> North-Bound (p,C)
A2: ( (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) & (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) ) by EUCLID:52;
assume not South-Bound (p,C) <> North-Bound (p,C) ; ::_thesis: contradiction
hence contradiction by A1, A2, Th19; ::_thesis: verum
end;
theorem Th21: :: JORDAN18:21
for p being Point of (TOP-REAL 2)
for C being Subset of (TOP-REAL 2) holds LSeg ((North-Bound (p,C)),(South-Bound (p,C))) is vertical
proof
let p be Point of (TOP-REAL 2); ::_thesis: for C being Subset of (TOP-REAL 2) holds LSeg ((North-Bound (p,C)),(South-Bound (p,C))) is vertical
let C be Subset of (TOP-REAL 2); ::_thesis: LSeg ((North-Bound (p,C)),(South-Bound (p,C))) is vertical
( (North-Bound (p,C)) `1 = p `1 & (South-Bound (p,C)) `1 = p `1 ) by EUCLID:52;
hence LSeg ((North-Bound (p,C)),(South-Bound (p,C))) is vertical by SPPOL_1:16; ::_thesis: verum
end;
theorem :: JORDAN18:22
for p being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
(LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C = {(North-Bound (p,C)),(South-Bound (p,C))}
proof
let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
(LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C = {(North-Bound (p,C)),(South-Bound (p,C))}
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C implies (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C = {(North-Bound (p,C)),(South-Bound (p,C))} )
set L = LSeg ((North-Bound (p,C)),(South-Bound (p,C)));
assume A1: p in BDD C ; ::_thesis: (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C = {(North-Bound (p,C)),(South-Bound (p,C))}
then A2: ( North-Bound (p,C) in C & South-Bound (p,C) in C ) by Th17;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(North-Bound (p,C)),(South-Bound (p,C))} c= (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C
A3: (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) by EUCLID:52;
A4: (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) by EUCLID:52;
let x be set ; ::_thesis: ( x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C implies x in {(North-Bound (p,C)),(South-Bound (p,C))} )
A5: (South-Bound (p,C)) `1 = p `1 by EUCLID:52;
assume A6: x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C ; ::_thesis: x in {(North-Bound (p,C)),(South-Bound (p,C))}
then reconsider y = x as Point of (TOP-REAL 2) ;
A7: x in LSeg ((North-Bound (p,C)),(South-Bound (p,C))) by A6, XBOOLE_0:def_4;
( LSeg ((North-Bound (p,C)),(South-Bound (p,C))) is vertical & South-Bound (p,C) in LSeg ((North-Bound (p,C)),(South-Bound (p,C))) ) by Th21, RLTOPSP1:68;
then A8: y `1 = p `1 by A5, A7, SPPOL_1:def_3;
A9: x in C by A6, XBOOLE_0:def_4;
A10: (North-Bound (p,C)) `1 = p `1 by EUCLID:52;
now__::_thesis:_(_y_<>_North-Bound_(p,C)_implies_y_=_South-Bound_(p,C)_)
C /\ (north_halfline p) is bounded by TOPREAL6:89;
then proj2 .: (C /\ (north_halfline p)) is real-bounded by JCT_MISC:14;
then A11: proj2 .: (C /\ (north_halfline p)) is bounded_below by XXREAL_2:def_11;
( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 ) by A1, Th18;
then A12: (South-Bound (p,C)) `2 < (North-Bound (p,C)) `2 by XXREAL_0:2;
then A13: (South-Bound (p,C)) `2 <= y `2 by A7, TOPREAL1:4;
assume y <> North-Bound (p,C) ; ::_thesis: y = South-Bound (p,C)
then A14: y `2 <> (North-Bound (p,C)) `2 by A10, A8, TOPREAL3:6;
A15: y `2 = proj2 . y by PSCOMP_1:def_6;
y `2 <= (North-Bound (p,C)) `2 by A7, A12, TOPREAL1:4;
then A16: y `2 < (North-Bound (p,C)) `2 by A14, XXREAL_0:1;
now__::_thesis:_not_y_`2_>_p_`2
assume y `2 > p `2 ; ::_thesis: contradiction
then y in north_halfline p by A8, TOPREAL1:def_10;
then y in C /\ (north_halfline p) by A9, XBOOLE_0:def_4;
then y `2 in proj2 .: (C /\ (north_halfline p)) by A15, FUNCT_2:35;
hence contradiction by A3, A16, A11, SEQ_4:def_2; ::_thesis: verum
end;
then y in south_halfline p by A8, TOPREAL1:def_12;
then y in C /\ (south_halfline p) by A9, XBOOLE_0:def_4;
then A17: y `2 in proj2 .: (C /\ (south_halfline p)) by A15, FUNCT_2:35;
C /\ (south_halfline p) is bounded by TOPREAL6:89;
then proj2 .: (C /\ (south_halfline p)) is real-bounded by JCT_MISC:14;
then proj2 .: (C /\ (south_halfline p)) is bounded_above by XXREAL_2:def_11;
then y `2 <= (South-Bound (p,C)) `2 by A4, A17, SEQ_4:def_1;
then y `2 = (South-Bound (p,C)) `2 by A13, XXREAL_0:1;
hence y = South-Bound (p,C) by A5, A8, TOPREAL3:6; ::_thesis: verum
end;
hence x in {(North-Bound (p,C)),(South-Bound (p,C))} by TARSKI:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(North-Bound (p,C)),(South-Bound (p,C))} or x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C )
assume x in {(North-Bound (p,C)),(South-Bound (p,C))} ; ::_thesis: x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C
then A18: ( x = North-Bound (p,C) or x = South-Bound (p,C) ) by TARSKI:def_2;
then x in LSeg ((North-Bound (p,C)),(South-Bound (p,C))) by RLTOPSP1:68;
hence x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C by A18, A2, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: JORDAN18:23
for p, q being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in BDD C & q in BDD C & p `1 <> q `1 holds
North-Bound (p,C), South-Bound (q,C), North-Bound (q,C), South-Bound (p,C) are_mutually_different
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C & q in BDD C & p `1 <> q `1 holds
North-Bound (p,C), South-Bound (q,C), North-Bound (q,C), South-Bound (p,C) are_mutually_different
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C & q in BDD C & p `1 <> q `1 implies North-Bound (p,C), South-Bound (q,C), North-Bound (q,C), South-Bound (p,C) are_mutually_different )
set np = North-Bound (p,C);
set sq = South-Bound (q,C);
set nq = North-Bound (q,C);
set sp = South-Bound (p,C);
A1: ( (North-Bound (p,C)) `1 = p `1 & (South-Bound (p,C)) `1 = p `1 ) by EUCLID:52;
A2: ( (North-Bound (q,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline q))) & (South-Bound (q,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline q))) ) by EUCLID:52;
A3: ( (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) & (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) ) by EUCLID:52;
assume ( p in BDD C & q in BDD C & p `1 <> q `1 ) ; ::_thesis: North-Bound (p,C), South-Bound (q,C), North-Bound (q,C), South-Bound (p,C) are_mutually_different
hence ( North-Bound (p,C) <> South-Bound (q,C) & North-Bound (p,C) <> North-Bound (q,C) & North-Bound (p,C) <> South-Bound (p,C) & South-Bound (q,C) <> North-Bound (q,C) & South-Bound (q,C) <> South-Bound (p,C) & North-Bound (q,C) <> South-Bound (p,C) ) by A1, A2, A3, Th19, EUCLID:52; :: according to ZFMISC_1:def_6 ::_thesis: verum
end;
begin
definition
let n be Element of NAT ;
let V be Subset of (TOP-REAL n);
let s1, s2, t1, t2 be Point of (TOP-REAL n);
preds1,s2,V -separate t1,t2 means :Def3: :: JORDAN18:def 3
for A being Subset of (TOP-REAL n) st A is_an_arc_of s1,s2 & A c= V holds
A meets {t1,t2};
end;
:: deftheorem Def3 defines -separate JORDAN18:def_3_:_
for n being Element of NAT
for V being Subset of (TOP-REAL n)
for s1, s2, t1, t2 being Point of (TOP-REAL n) holds
( s1,s2,V -separate t1,t2 iff for A being Subset of (TOP-REAL n) st A is_an_arc_of s1,s2 & A c= V holds
A meets {t1,t2} );
notation
let n be Element of NAT ;
let V be Subset of (TOP-REAL n);
let s1, s2, t1, t2 be Point of (TOP-REAL n);
antonym s1,s2 are_neighbours_wrt t1,t2,V for s1,s2,V -separate t1,t2;
end;
theorem :: JORDAN18:24
for n being Element of NAT
for V being Subset of (TOP-REAL n)
for t, s1, s2 being Point of (TOP-REAL n) holds t,t,V -separate s1,s2
proof
let n be Element of NAT ; ::_thesis: for V being Subset of (TOP-REAL n)
for t, s1, s2 being Point of (TOP-REAL n) holds t,t,V -separate s1,s2
let V be Subset of (TOP-REAL n); ::_thesis: for t, s1, s2 being Point of (TOP-REAL n) holds t,t,V -separate s1,s2
let t, s1, s2 be Point of (TOP-REAL n); ::_thesis: t,t,V -separate s1,s2
assume not t,t,V -separate s1,s2 ; ::_thesis: contradiction
then ex A being Subset of (TOP-REAL n) st
( A is_an_arc_of t,t & A c= V & A misses {s1,s2} ) by Def3;
hence contradiction by JORDAN6:37; ::_thesis: verum
end;
theorem :: JORDAN18:25
for n being Element of NAT
for V being Subset of (TOP-REAL n)
for s1, s2, t1, t2 being Point of (TOP-REAL n) st s1,s2,V -separate t1,t2 holds
s2,s1,V -separate t1,t2
proof
let n be Element of NAT ; ::_thesis: for V being Subset of (TOP-REAL n)
for s1, s2, t1, t2 being Point of (TOP-REAL n) st s1,s2,V -separate t1,t2 holds
s2,s1,V -separate t1,t2
let V be Subset of (TOP-REAL n); ::_thesis: for s1, s2, t1, t2 being Point of (TOP-REAL n) st s1,s2,V -separate t1,t2 holds
s2,s1,V -separate t1,t2
let s1, s2, t1, t2 be Point of (TOP-REAL n); ::_thesis: ( s1,s2,V -separate t1,t2 implies s2,s1,V -separate t1,t2 )
assume A1: for A being Subset of (TOP-REAL n) st A is_an_arc_of s1,s2 & A c= V holds
A meets {t1,t2} ; :: according to JORDAN18:def_3 ::_thesis: s2,s1,V -separate t1,t2
let A be Subset of (TOP-REAL n); :: according to JORDAN18:def_3 ::_thesis: ( A is_an_arc_of s2,s1 & A c= V implies A meets {t1,t2} )
assume ( A is_an_arc_of s2,s1 & A c= V ) ; ::_thesis: A meets {t1,t2}
hence A meets {t1,t2} by A1, JORDAN5B:14; ::_thesis: verum
end;
theorem :: JORDAN18:26
for n being Element of NAT
for V being Subset of (TOP-REAL n)
for s1, s2, t1, t2 being Point of (TOP-REAL n) st s1,s2,V -separate t1,t2 holds
s1,s2,V -separate t2,t1
proof
let n be Element of NAT ; ::_thesis: for V being Subset of (TOP-REAL n)
for s1, s2, t1, t2 being Point of (TOP-REAL n) st s1,s2,V -separate t1,t2 holds
s1,s2,V -separate t2,t1
let V be Subset of (TOP-REAL n); ::_thesis: for s1, s2, t1, t2 being Point of (TOP-REAL n) st s1,s2,V -separate t1,t2 holds
s1,s2,V -separate t2,t1
let s1, s2, t1, t2 be Point of (TOP-REAL n); ::_thesis: ( s1,s2,V -separate t1,t2 implies s1,s2,V -separate t2,t1 )
assume A1: for A being Subset of (TOP-REAL n) st A is_an_arc_of s1,s2 & A c= V holds
A meets {t1,t2} ; :: according to JORDAN18:def_3 ::_thesis: s1,s2,V -separate t2,t1
let A be Subset of (TOP-REAL n); :: according to JORDAN18:def_3 ::_thesis: ( A is_an_arc_of s1,s2 & A c= V implies A meets {t2,t1} )
thus ( A is_an_arc_of s1,s2 & A c= V implies A meets {t2,t1} ) by A1; ::_thesis: verum
end;
theorem Th27: :: JORDAN18:27
for n being Element of NAT
for V being Subset of (TOP-REAL n)
for s, t1, t2 being Point of (TOP-REAL n) holds s,t1,V -separate s,t2
proof
let n be Element of NAT ; ::_thesis: for V being Subset of (TOP-REAL n)
for s, t1, t2 being Point of (TOP-REAL n) holds s,t1,V -separate s,t2
let V be Subset of (TOP-REAL n); ::_thesis: for s, t1, t2 being Point of (TOP-REAL n) holds s,t1,V -separate s,t2
let s, t1, t2 be Point of (TOP-REAL n); ::_thesis: s,t1,V -separate s,t2
let A be Subset of (TOP-REAL n); :: according to JORDAN18:def_3 ::_thesis: ( A is_an_arc_of s,t1 & A c= V implies A meets {s,t2} )
assume that
A1: A is_an_arc_of s,t1 and
A c= V ; ::_thesis: A meets {s,t2}
A2: s in {s,t2} by TARSKI:def_2;
s in A by A1, TOPREAL1:1;
hence A meets {s,t2} by A2, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th28: :: JORDAN18:28
for n being Element of NAT
for V being Subset of (TOP-REAL n)
for t1, s, t2 being Point of (TOP-REAL n) holds t1,s,V -separate t2,s
proof
let n be Element of NAT ; ::_thesis: for V being Subset of (TOP-REAL n)
for t1, s, t2 being Point of (TOP-REAL n) holds t1,s,V -separate t2,s
let V be Subset of (TOP-REAL n); ::_thesis: for t1, s, t2 being Point of (TOP-REAL n) holds t1,s,V -separate t2,s
let t1, s, t2 be Point of (TOP-REAL n); ::_thesis: t1,s,V -separate t2,s
let A be Subset of (TOP-REAL n); :: according to JORDAN18:def_3 ::_thesis: ( A is_an_arc_of t1,s & A c= V implies A meets {t2,s} )
assume that
A1: A is_an_arc_of t1,s and
A c= V ; ::_thesis: A meets {t2,s}
A2: s in {s,t2} by TARSKI:def_2;
s in A by A1, TOPREAL1:1;
hence A meets {t2,s} by A2, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th29: :: JORDAN18:29
for n being Element of NAT
for V being Subset of (TOP-REAL n)
for t1, s, t2 being Point of (TOP-REAL n) holds t1,s,V -separate s,t2
proof
let n be Element of NAT ; ::_thesis: for V being Subset of (TOP-REAL n)
for t1, s, t2 being Point of (TOP-REAL n) holds t1,s,V -separate s,t2
let V be Subset of (TOP-REAL n); ::_thesis: for t1, s, t2 being Point of (TOP-REAL n) holds t1,s,V -separate s,t2
let t1, s, t2 be Point of (TOP-REAL n); ::_thesis: t1,s,V -separate s,t2
let A be Subset of (TOP-REAL n); :: according to JORDAN18:def_3 ::_thesis: ( A is_an_arc_of t1,s & A c= V implies A meets {s,t2} )
assume that
A1: A is_an_arc_of t1,s and
A c= V ; ::_thesis: A meets {s,t2}
A2: s in {s,t2} by TARSKI:def_2;
s in A by A1, TOPREAL1:1;
hence A meets {s,t2} by A2, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th30: :: JORDAN18:30
for n being Element of NAT
for V being Subset of (TOP-REAL n)
for s, t1, t2 being Point of (TOP-REAL n) holds s,t1,V -separate t2,s
proof
let n be Element of NAT ; ::_thesis: for V being Subset of (TOP-REAL n)
for s, t1, t2 being Point of (TOP-REAL n) holds s,t1,V -separate t2,s
let V be Subset of (TOP-REAL n); ::_thesis: for s, t1, t2 being Point of (TOP-REAL n) holds s,t1,V -separate t2,s
let s, t1, t2 be Point of (TOP-REAL n); ::_thesis: s,t1,V -separate t2,s
let A be Subset of (TOP-REAL n); :: according to JORDAN18:def_3 ::_thesis: ( A is_an_arc_of s,t1 & A c= V implies A meets {t2,s} )
assume that
A1: A is_an_arc_of s,t1 and
A c= V ; ::_thesis: A meets {t2,s}
A2: s in {s,t2} by TARSKI:def_2;
s in A by A1, TOPREAL1:1;
hence A meets {t2,s} by A2, XBOOLE_0:3; ::_thesis: verum
end;
theorem :: JORDAN18:31
for C being Simple_closed_curve
for p1, p2, q being Point of (TOP-REAL 2) st q in C & p1 in C & p2 in C & p1 <> p2 & p1 <> q & p2 <> q holds
p1,p2 are_neighbours_wrt q,q,C
proof
let C be Simple_closed_curve; ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st q in C & p1 in C & p2 in C & p1 <> p2 & p1 <> q & p2 <> q holds
p1,p2 are_neighbours_wrt q,q,C
let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( q in C & p1 in C & p2 in C & p1 <> p2 & p1 <> q & p2 <> q implies p1,p2 are_neighbours_wrt q,q,C )
assume that
A1: q in C and
A2: ( p1 in C & p2 in C & p1 <> p2 ) and
A3: ( p1 <> q & p2 <> q ) ; ::_thesis: p1,p2 are_neighbours_wrt q,q,C
consider P1, P2 being non empty Subset of (TOP-REAL 2) such that
A4: P1 is_an_arc_of p1,p2 and
A5: P2 is_an_arc_of p1,p2 and
A6: C = P1 \/ P2 and
A7: P1 /\ P2 = {p1,p2} by A2, TOPREAL2:5;
percases ( ( q in P1 & not q in P2 ) or ( q in P2 & not q in P1 ) or ( q in P1 & q in P2 ) ) by A1, A6, XBOOLE_0:def_3;
supposeA8: ( q in P1 & not q in P2 ) ; ::_thesis: p1,p2 are_neighbours_wrt q,q,C
take P2 ; :: according to JORDAN18:def_3 ::_thesis: ( P2 is_an_arc_of p1,p2 & P2 c= C & not P2 meets {q,q} )
thus P2 is_an_arc_of p1,p2 by A5; ::_thesis: ( P2 c= C & not P2 meets {q,q} )
thus P2 c= C by A6, XBOOLE_1:7; ::_thesis: not P2 meets {q,q}
thus P2 misses {q,q} by A8, ZFMISC_1:51; ::_thesis: verum
end;
supposeA9: ( q in P2 & not q in P1 ) ; ::_thesis: p1,p2 are_neighbours_wrt q,q,C
take P1 ; :: according to JORDAN18:def_3 ::_thesis: ( P1 is_an_arc_of p1,p2 & P1 c= C & not P1 meets {q,q} )
thus P1 is_an_arc_of p1,p2 by A4; ::_thesis: ( P1 c= C & not P1 meets {q,q} )
thus P1 c= C by A6, XBOOLE_1:7; ::_thesis: not P1 meets {q,q}
thus P1 misses {q,q} by A9, ZFMISC_1:51; ::_thesis: verum
end;
suppose ( q in P1 & q in P2 ) ; ::_thesis: p1,p2 are_neighbours_wrt q,q,C
then q in P1 /\ P2 by XBOOLE_0:def_4;
hence p1,p2 are_neighbours_wrt q,q,C by A3, A7, TARSKI:def_2; ::_thesis: verum
end;
end;
end;
theorem :: JORDAN18:32
for C being Simple_closed_curve
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in C & p2 in C & p1,p2,C -separate q1,q2 holds
q1,q2,C -separate p1,p2
proof
let C be Simple_closed_curve; ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in C & p2 in C & p1,p2,C -separate q1,q2 holds
q1,q2,C -separate p1,p2
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( p1 <> p2 & p1 in C & p2 in C & p1,p2,C -separate q1,q2 implies q1,q2,C -separate p1,p2 )
assume that
A1: p1 <> p2 and
A2: p1 in C and
A3: p2 in C and
A4: p1,p2,C -separate q1,q2 ; ::_thesis: q1,q2,C -separate p1,p2
percases ( q1 = p1 or q2 = p2 or q1 = p2 or p1 = q2 or ( q1 <> p1 & q2 <> p2 & q1 <> p2 & q2 <> p1 ) ) ;
suppose q1 = p1 ; ::_thesis: q1,q2,C -separate p1,p2
hence q1,q2,C -separate p1,p2 by Th27; ::_thesis: verum
end;
suppose q2 = p2 ; ::_thesis: q1,q2,C -separate p1,p2
hence q1,q2,C -separate p1,p2 by Th28; ::_thesis: verum
end;
suppose q1 = p2 ; ::_thesis: q1,q2,C -separate p1,p2
hence q1,q2,C -separate p1,p2 by Th30; ::_thesis: verum
end;
suppose p1 = q2 ; ::_thesis: q1,q2,C -separate p1,p2
hence q1,q2,C -separate p1,p2 by Th29; ::_thesis: verum
end;
supposeA5: ( q1 <> p1 & q2 <> p2 & q1 <> p2 & q2 <> p1 ) ; ::_thesis: q1,q2,C -separate p1,p2
let A be Subset of (TOP-REAL 2); :: according to JORDAN18:def_3 ::_thesis: ( A is_an_arc_of q1,q2 & A c= C implies A meets {p1,p2} )
assume ( A is_an_arc_of q1,q2 & A c= C ) ; ::_thesis: A meets {p1,p2}
then consider B being non empty Subset of (TOP-REAL 2) such that
A6: B is_an_arc_of q1,q2 and
A7: A \/ B = C and
A /\ B = {q1,q2} by Th15;
assume A8: A misses {p1,p2} ; ::_thesis: contradiction
then not p2 in A by ZFMISC_1:49;
then A9: p2 in B by A3, A7, XBOOLE_0:def_3;
not p1 in A by A8, ZFMISC_1:49;
then p1 in B by A2, A7, XBOOLE_0:def_3;
then consider P being non empty Subset of (TOP-REAL 2) such that
A10: P is_an_arc_of p1,p2 and
A11: P c= B and
A12: P misses {q1,q2} by A1, A5, A6, A9, JORDAN16:23;
B c= C by A7, XBOOLE_1:7;
then P c= C by A11, XBOOLE_1:1;
hence contradiction by A4, A10, A12, Def3; ::_thesis: verum
end;
end;
end;
theorem :: JORDAN18:33
for C being Simple_closed_curve
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1 in C & p2 in C & q1 in C & p1 <> p2 & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & not p1,p2 are_neighbours_wrt q1,q2,C holds
p1,q1 are_neighbours_wrt p2,q2,C
proof
let C be Simple_closed_curve; ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1 in C & p2 in C & q1 in C & p1 <> p2 & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & not p1,p2 are_neighbours_wrt q1,q2,C holds
p1,q1 are_neighbours_wrt p2,q2,C
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( p1 in C & p2 in C & q1 in C & p1 <> p2 & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & not p1,p2 are_neighbours_wrt q1,q2,C implies p1,q1 are_neighbours_wrt p2,q2,C )
assume that
A1: ( p1 in C & p2 in C ) and
A2: q1 in C and
A3: p1 <> p2 and
A4: q1 <> p1 and
A5: q1 <> p2 and
A6: ( q2 <> p1 & q2 <> p2 ) ; ::_thesis: ( p1,p2 are_neighbours_wrt q1,q2,C or p1,q1 are_neighbours_wrt p2,q2,C )
consider P, P1 being non empty Subset of (TOP-REAL 2) such that
A7: P is_an_arc_of p1,p2 and
A8: P1 is_an_arc_of p1,p2 and
A9: C = P \/ P1 and
A10: P /\ P1 = {p1,p2} by A1, A3, TOPREAL2:5;
A11: P c= C by A9, XBOOLE_1:7;
assume A12: for A being Subset of (TOP-REAL 2) st A is_an_arc_of p1,p2 & A c= C holds
A meets {q1,q2} ; :: according to JORDAN18:def_3 ::_thesis: p1,q1 are_neighbours_wrt p2,q2,C
then A13: P meets {q1,q2} by A7, A9, XBOOLE_1:7;
A14: P1 c= C by A9, XBOOLE_1:7;
percases ( ( q1 in P & not q2 in P ) or ( q2 in P & not q1 in P ) or ( q1 in P & q2 in P ) ) by A13, ZFMISC_1:51;
supposethat A15: q1 in P and
A16: not q2 in P ; ::_thesis: p1,q1 are_neighbours_wrt p2,q2,C
now__::_thesis:_ex_A_being_Element_of_bool_the_carrier_of_(TOP-REAL_2)_st_
(_A_is_an_arc_of_p1,q1_&_A_c=_C_&_A_misses_{p2,q2}_)
take A = Segment (P,p1,p2,p1,q1); ::_thesis: ( A is_an_arc_of p1,q1 & A c= C & A misses {p2,q2} )
A17: now__::_thesis:_not_p2_in_A
A18: A = { q where q is Point of (TOP-REAL 2) : ( LE p1,q,P,p1,p2 & LE q,q1,P,p1,p2 ) } by JORDAN6:26;
assume p2 in A ; ::_thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( p2 = q & LE p1,q,P,p1,p2 & LE q,q1,P,p1,p2 ) by A18;
hence contradiction by A5, A7, JORDAN6:55; ::_thesis: verum
end;
LE p1,q1,P,p1,p2 by A7, A15, JORDAN5C:10;
hence A is_an_arc_of p1,q1 by A4, A7, JORDAN16:21; ::_thesis: ( A c= C & A misses {p2,q2} )
A19: A c= P by JORDAN16:2;
hence A c= C by A11, XBOOLE_1:1; ::_thesis: A misses {p2,q2}
not q2 in A by A16, A19;
hence A misses {p2,q2} by A17, ZFMISC_1:51; ::_thesis: verum
end;
hence p1,q1 are_neighbours_wrt p2,q2,C by Def3; ::_thesis: verum
end;
supposethat A20: q2 in P and
A21: not q1 in P ; ::_thesis: p1,q1 are_neighbours_wrt p2,q2,C
now__::_thesis:_ex_A_being_Element_of_bool_the_carrier_of_(TOP-REAL_2)_st_
(_A_is_an_arc_of_p1,q1_&_A_c=_C_&_A_misses_{p2,q2}_)
take A = Segment (P1,p1,p2,p1,q1); ::_thesis: ( A is_an_arc_of p1,q1 & A c= C & A misses {p2,q2} )
A22: now__::_thesis:_not_p2_in_A
A23: A = { q where q is Point of (TOP-REAL 2) : ( LE p1,q,P1,p1,p2 & LE q,q1,P1,p1,p2 ) } by JORDAN6:26;
assume p2 in A ; ::_thesis: contradiction
then ex q being Point of (TOP-REAL 2) st
( p2 = q & LE p1,q,P1,p1,p2 & LE q,q1,P1,p1,p2 ) by A23;
hence contradiction by A5, A8, JORDAN6:55; ::_thesis: verum
end;
q1 in P1 by A2, A9, A21, XBOOLE_0:def_3;
then LE p1,q1,P1,p1,p2 by A8, JORDAN5C:10;
hence A is_an_arc_of p1,q1 by A4, A8, JORDAN16:21; ::_thesis: ( A c= C & A misses {p2,q2} )
A24: A c= P1 by JORDAN16:2;
hence A c= C by A14, XBOOLE_1:1; ::_thesis: A misses {p2,q2}
now__::_thesis:_not_q2_in_A
assume q2 in A ; ::_thesis: contradiction
then q2 in {p1,p2} by A10, A20, A24, XBOOLE_0:def_4;
hence contradiction by A6, TARSKI:def_2; ::_thesis: verum
end;
hence A misses {p2,q2} by A22, ZFMISC_1:51; ::_thesis: verum
end;
hence p1,q1 are_neighbours_wrt p2,q2,C by Def3; ::_thesis: verum
end;
supposeA25: ( q1 in P & q2 in P ) ; ::_thesis: p1,q1 are_neighbours_wrt p2,q2,C
P1 meets {q1,q2} by A12, A8, A9, XBOOLE_1:7;
then ( q1 in P1 or q2 in P1 ) by ZFMISC_1:51;
then ( q1 in {p1,p2} or q2 in {p1,p2} ) by A10, A25, XBOOLE_0:def_4;
hence p1,q1 are_neighbours_wrt p2,q2,C by A4, A5, A6, TARSKI:def_2; ::_thesis: verum
end;
end;
end;