:: JORDAN18 semantic presentation

Lm1: TOP-REAL 2 = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;

Lm2: the carrier of (Euclid 2) = the carrier of (TopSpaceMetr (Euclid 2))
by TOPMETR:16;

Lm3: dom proj1 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;

Lm4: dom proj2 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;

theorem Th1: :: JORDAN18:1

for a, b being real number holds (a - b) ^2 = (b - a) ^2

proof end;

theorem :: JORDAN18:2

for S, T being non empty TopSpace
for f being Function of S,T
for A being Subset of T st f is_homeomorphism & A is connected holds
f " A is connected

proof end;

theorem :: JORDAN18:3

for S, T being non empty TopStruct
for f being Function of S,T
for A being Subset of T st f is_homeomorphism & A is compact holds
f " A is compact

proof end;

theorem Th4: :: JORDAN18:4

for a being Point of (TOP-REAL 2) holds proj2 .: (north_halfline a) is bounded_below

proof end;

theorem Th5: :: JORDAN18:5

for a being Point of (TOP-REAL 2) holds proj2 .: (south_halfline a) is bounded_above

proof end;

theorem Th6: :: JORDAN18:6

for a being Point of (TOP-REAL 2) holds proj1 .: (west_halfline a) is bounded_above

proof end;

theorem Th7: :: JORDAN18:7

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 by Lm4, RELAT_1:152;
cluster proj2 .: (south_halfline a) -> non empty ;
coherence by Lm4, RELAT_1:152;
cluster proj1 .: (west_halfline a) -> non empty ;
coherence by Lm3, RELAT_1:152;
cluster proj1 .: (east_halfline a) -> non empty ;
coherence by Lm3, RELAT_1:152;

end;

theorem Th8: :: JORDAN18:8

for a being Point of (TOP-REAL 2) holds inf (proj2 .: (north_halfline a)) = a `2

proof end;

theorem Th9: :: JORDAN18:9

for a being Point of (TOP-REAL 2) holds sup (proj2 .: (south_halfline a)) = a `2

proof end;

theorem :: JORDAN18:10

for a being Point of (TOP-REAL 2) holds sup (proj1 .: (west_halfline a)) = a `1

proof end;

theorem :: JORDAN18:11

for a being Point of (TOP-REAL 2) holds inf (proj1 .: (east_halfline a)) = a `1

proof end;

registration

let a be Point of (TOP-REAL 2);
cluster north_halfline a -> closed ;
coherence

proof end;

cluster south_halfline a -> closed ;
coherence

proof end;

cluster east_halfline a -> closed ;
coherence

proof end;

cluster west_halfline a -> closed ;
coherence

proof end;

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 north_halfline a c= UBD P

proof end;

theorem Th13: :: 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 south_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 east_halfline a c= UBD P

proof end;

theorem :: JORDAN18:15

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 :: JORDAN18:16

for P being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q <> p2 holds
not p2 in L_Segment P,p1,p2,q

proof end;

theorem :: JORDAN18:17

for P being Subset of (TOP-REAL 2)
for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q <> p1 holds
not p1 in R_Segment P,p1,p2,q

proof end;

theorem Th18: :: JORDAN18:18

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;

theorem Th19: :: JORDAN18:19

for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 & q1 <> q2 holds
ex Q being non empty Subset of (TOP-REAL 2) st
( Q is_an_arc_of q1,q2 & Q c= P & Q misses {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 ),(inf (proj2 .: (P /\ (north_halfline p))))]|;
correctness ;
func South-Bound p,P -> Point of (TOP-REAL 2) equals :: JORDAN18:def 2
|[(p `1 ),(sup (proj2 .: (P /\ (south_halfline p))))]|;
correctness ;

end;

:: deftheorem defines North-Bound JORDAN18:def 1 :

:: deftheorem defines South-Bound JORDAN18:def 2 :

theorem Th20: :: JORDAN18:20

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:56;

theorem Th21: :: JORDAN18:21

for P being Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) holds
( (North-Bound p,P) `2 = inf (proj2 .: (P /\ (north_halfline p))) & (South-Bound p,P) `2 = sup (proj2 .: (P /\ (south_halfline p))) ) by EUCLID:56;

theorem Th22: :: 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
( 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 Th23: :: JORDAN18:23

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 Th24: :: JORDAN18:24

for p being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
inf (proj2 .: (C /\ (north_halfline p))) > sup (proj2 .: (C /\ (south_halfline p)))

proof end;

theorem :: JORDAN18:25

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 Th26: :: JORDAN18:26

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:27

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:28

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 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 :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 :

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:29

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

theorem :: JORDAN18:30

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

theorem :: JORDAN18:31

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

theorem Th32: :: JORDAN18:32

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 Th33: :: JORDAN18:33

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

theorem Th34: :: JORDAN18:34

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

theorem Th35: :: JORDAN18:35

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:36

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:37

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:38

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;