:: by Artur Korni{\l}owicz

::

:: Received September 16, 2002

:: Copyright (c) 2002-2021 Association of Mizar Users

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

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;

registration

let a be Point of (TOP-REAL 2);

coherence

not proj2 .: (north_halfline a) is empty by Lm2, RELAT_1:119;

coherence

not proj2 .: (south_halfline a) is empty by Lm2, RELAT_1:119;

coherence

not proj1 .: (west_halfline a) is empty by Lm1, RELAT_1:119;

coherence

not proj1 .: (east_halfline a) is empty by Lm1, RELAT_1:119;

end;
coherence

not proj2 .: (north_halfline a) is empty by Lm2, RELAT_1:119;

coherence

not proj2 .: (south_halfline a) is empty by Lm2, RELAT_1:119;

coherence

not proj1 .: (west_halfline a) is empty by Lm1, RELAT_1:119;

coherence

not proj1 .: (east_halfline a) is empty by Lm1, RELAT_1:119;

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

coherence

north_halfline a is closed

south_halfline a is closed

east_halfline a is closed

west_halfline a is closed

end;
coherence

north_halfline a is closed

proof end;

coherence south_halfline a is closed

proof end;

coherence east_halfline a is closed

proof end;

coherence west_halfline a is closed

proof 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

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

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

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

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} )

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

coherence

|[(p `1),(lower_bound (proj2 .: (P /\ (north_halfline p))))]| is Point of (TOP-REAL 2);

;

coherence

|[(p `1),(upper_bound (proj2 .: (P /\ (south_halfline p))))]| is Point of (TOP-REAL 2);

;

end;
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 |[(p `1),(lower_bound (proj2 .: (P /\ (north_halfline p))))]|;

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 |[(p `1),(upper_bound (proj2 .: (P /\ (south_halfline p))))]|;

coherence

|[(p `1),(upper_bound (proj2 .: (P /\ (south_halfline p))))]| is Point of (TOP-REAL 2);

;

:: 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))))]|;

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))))]|;

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

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 )

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 )

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

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)

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

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))}

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

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

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

for A being Subset of (TOP-REAL n) st A is_an_arc_of s1,s2 & A c= V holds

A meets {t1,t2};

:: 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} );

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

theorem :: JORDAN18:24

theorem :: JORDAN18:25

theorem :: JORDAN18:26

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

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

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

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

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

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

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

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;