:: The Ordering of Points on a Curve, Part {IV} :: by Artur Korni{\l}owicz :: :: Received September 16, 2002 :: Copyright (c) 2002-2012 Association of Mizar Users 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 proofend; theorem Th3: :: JORDAN18:3 for a being Point of (TOP-REAL 2) holds proj2 .: (north_halfline a) is bounded_below proofend; theorem Th4: :: JORDAN18:4 for a being Point of (TOP-REAL 2) holds proj2 .: (south_halfline a) is bounded_above proofend; theorem Th5: :: JORDAN18:5 for a being Point of (TOP-REAL 2) holds proj1 .: (west_halfline a) is bounded_above proofend; theorem Th6: :: JORDAN18:6 for a being Point of (TOP-REAL 2) holds proj1 .: (east_halfline a) is bounded_below proofend; 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 proofend; theorem Th8: :: JORDAN18:8 for a being Point of (TOP-REAL 2) holds upper_bound (proj2 .: (south_halfline a)) = a `2 proofend; theorem :: JORDAN18:9 for a being Point of (TOP-REAL 2) holds upper_bound (proj1 .: (west_halfline a)) = a `1 proofend; theorem :: JORDAN18:10 for a being Point of (TOP-REAL 2) holds lower_bound (proj1 .: (east_halfline a)) = a `1 proofend; 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 proofend; cluster south_halfline a -> closed ; coherence south_halfline a is closed proofend; cluster east_halfline a -> closed ; coherence east_halfline a is closed proofend; cluster west_halfline a -> closed ; coherence west_halfline a is closed proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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} ) proofend; 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 ) proofend; 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 ) proofend; 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))) proofend; 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) proofend; 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 proofend; 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))} proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend;