:: The Ordering of Points on a Curve, Part {IV}
:: by Artur Korni{\l}owicz
::
:: Received September 16, 2002
:: Copyright (c) 2002-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, EUCLID, PRE_TOPC, TOPREAL2, RELAT_1, STRUCT_0, ARYTM_1, SQUARE_1, XBOOLE_0, FUNCT_1, TOPS_2, RCOMP_1, ORDINAL2, TOPREAL1, XXREAL_2, MCART_1, XXREAL_0, CARD_1, ARYTM_3, PCOMPS_1, METRIC_1, TARSKI, COMPLEX1, JORDAN2C, RLTOPSP1, SPPOL_1, ZFMISC_1, JORDAN6, JORDAN3, JORDAN18, SEQ_4, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, XXREAL_2, SEQ_4, STRUCT_0, PCOMPS_1, COMPLEX1, PRE_TOPC, TOPS_2, RCOMP_1, COMPTS_1, METRIC_1, SPPOL_1, RLTOPSP1, EUCLID, TOPREAL1, PSCOMP_1, TOPREAL2, JORDAN5C, JORDAN2C, TOPREAL6, JORDAN6;
definitions TARSKI, XBOOLE_0, ZFMISC_1, XXREAL_2;
theorems JORDAN5B, TARSKI, TOPREAL1, XBOOLE_0, EUCLID, JORDAN6, TOPS_2, XBOOLE_1, SEQ_4, RELAT_1, PSCOMP_1, FUNCT_2, TOPREAL3, JORDAN1A, COMPTS_1, ZFMISC_1, JORDAN5C, TOPREAL2, JORDAN2C, SQUARE_1, RCOMP_1, TOPMETR, METRIC_1, JORDAN16, SPPOL_1, COMPLEX1, XREAL_1, TOPREAL6, XXREAL_0, JCT_MISC, PRE_TOPC, RLTOPSP1;
schemes ;
registrations RELSET_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, MEMBERED, COMPTS_1, EUCLID, TOPREAL1, STRUCT_0, TOPS_1, JORDAN2C, ORDINAL1;
constructors HIDDEN, REAL_1, SQUARE_1, COMPLEX1, RCOMP_1, TOPS_2, COMPTS_1, TOPREAL1, SPPOL_1, PSCOMP_1, JORDAN5C, JORDAN6, JORDAN2C, TOPREAL6, SEQ_4, RELSET_1, FUNCSDOM, BINOP_2, PCOMPS_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, SQUARE_1, SUBSET_1;
expansions TARSKI, XBOOLE_0, XXREAL_2;


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 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 end;

theorem Th3: :: JORDAN18:3
for a being Point of (TOP-REAL 2) holds proj2 .: (north_halfline a) is bounded_below
proof end;

theorem Th4: :: JORDAN18:4
for a being Point of (TOP-REAL 2) holds proj2 .: (south_halfline a) is bounded_above
proof end;

theorem Th5: :: JORDAN18:5
for a being Point of (TOP-REAL 2) holds proj1 .: (west_halfline a) is bounded_above
proof end;

theorem Th6: :: JORDAN18:6
for a being Point of (TOP-REAL 2) holds proj1 .: (east_halfline a) is bounded_below
proof end;

registration
let a be Point of (TOP-REAL 2);
cluster proj2 .: (north_halfline a) -> non empty ;
coherence
not proj2 .: (north_halfline a) is empty by Lm2, RELAT_1:119;
cluster proj2 .: (south_halfline a) -> non empty ;
coherence
not proj2 .: (south_halfline a) is empty by Lm2, RELAT_1:119;
cluster proj1 .: (west_halfline a) -> non empty ;
coherence
not proj1 .: (west_halfline a) is empty by Lm1, RELAT_1:119;
cluster proj1 .: (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 end;

theorem Th8: :: JORDAN18:8
for a being Point of (TOP-REAL 2) holds upper_bound (proj2 .: (south_halfline a)) = a `2
proof end;

theorem :: JORDAN18:9
for a being Point of (TOP-REAL 2) holds upper_bound (proj1 .: (west_halfline a)) = a `1
proof end;

theorem :: JORDAN18:10
for a being Point of (TOP-REAL 2) holds lower_bound (proj1 .: (east_halfline a)) = a `1
proof 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 end;
cluster south_halfline a -> closed ;
coherence
south_halfline a is closed
proof end;
cluster east_halfline a -> closed ;
coherence
east_halfline a is closed
proof end;
cluster west_halfline a -> closed ;
coherence
west_halfline a is closed
proof 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 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 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 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 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 end;

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 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 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 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 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 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 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_distinct
proof end;

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);
pred s1,s2,V -separate t1,t2 means :: 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 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 s1, s2, t being Point of (TOP-REAL n) holds t,t,V -separate s1,s2 by JORDAN6:37;

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 by JORDAN5B:14;

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 ;

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 end;

theorem Th28: :: JORDAN18:28
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 t1,s,V -separate t2,s
proof end;

theorem Th29: :: JORDAN18:29
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 t1,s,V -separate s,t2
proof 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 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 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 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 end;