:: JORDAN18 semantic presentation

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

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

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

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

theorem Th1: :: JORDAN18:1

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

proof end;

theorem Th2: :: JORDAN18:2

for b₁, b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₂ st b₃ is_homeomorphism & b₄ is connected holds
b₃ " b₄ is connected

proof end;

theorem Th3: :: JORDAN18:3

for b₁, b₂ being non empty TopStruct
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₂ st b₃ is_homeomorphism & b₄ is compact holds
b₃ " b₄ is compact

proof end;

theorem Th4: :: JORDAN18:4

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

proof end;

theorem Th5: :: JORDAN18:5

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

proof end;

theorem Th6: :: JORDAN18:6

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

proof end;

theorem Th7: :: JORDAN18:7

for b₁ being Point of (TOP-REAL 2) holds proj1 .: (east_halfline b₁) is bounded_below

proof end;

registration

let c₁ be Point of (TOP-REAL 2);
cluster proj2 .: (north_halfline a₁) -> non empty ;
coherence by Lemma4, RELAT_1:152;
cluster proj2 .: (south_halfline a₁) -> non empty ;
coherence by Lemma4, RELAT_1:152;
cluster proj1 .: (west_halfline a₁) -> non empty ;
coherence by Lemma3, RELAT_1:152;
cluster proj1 .: (east_halfline a₁) -> non empty ;
coherence by Lemma3, RELAT_1:152;

end;

theorem Th8: :: JORDAN18:8

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

proof end;

theorem Th9: :: JORDAN18:9

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

proof end;

theorem Th10: :: JORDAN18:10

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

proof end;

theorem Th11: :: JORDAN18:11

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

proof end;

registration

let c₁ 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 b₁ being Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in BDD b₁ holds
not north_halfline b₂ c= UBD b₁

proof end;

theorem Th13: :: JORDAN18:13

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in BDD b₁ holds
not south_halfline b₂ c= UBD b₁

proof end;

theorem Th14: :: JORDAN18:14

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in BDD b₁ holds
not east_halfline b₂ c= UBD b₁

proof end;

theorem Th15: :: JORDAN18:15

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in BDD b₁ holds
not west_halfline b₂ c= UBD b₁

proof end;

theorem Th16: :: JORDAN18:16

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃ & b₄ <> b₃ holds
not b₃ in L_Segment b₁,b₂,b₃,b₄

proof end;

theorem Th17: :: JORDAN18:17

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃ & b₄ <> b₂ holds
not b₂ in R_Segment b₁,b₂,b₃,b₄

proof end;

theorem Th18: :: JORDAN18:18

for b₁ being Simple_closed_curve
for b₂ being Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₂ is_an_arc_of b₃,b₄ & b₂ c= b₁ holds
ex b₅ being non empty Subset of (TOP-REAL 2) st
( b₅ is_an_arc_of b₃,b₄ & b₂ \/ b₅ = b₁ & b₂ /\ b₅ = {b₃,b₄} )

proof end;

theorem Th19: :: JORDAN18:19

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₁ is_an_arc_of b₂,b₃ & b₄ in b₁ & b₅ in b₁ & b₄ <> b₂ & b₄ <> b₃ & b₅ <> b₂ & b₅ <> b₃ & b₄ <> b₅ holds
ex b₆ being non empty Subset of (TOP-REAL 2) st
( b₆ is_an_arc_of b₄,b₅ & b₆ c= b₁ & b₆ misses {b₂,b₃} )

proof end;

definition

let c₁ be Point of (TOP-REAL 2);
let c₂ be Subset of (TOP-REAL 2);
func North-Bound c₁,c₂ -> Point of (TOP-REAL 2) equals :: JORDAN18:def 1
|[(a₁ `1 ),(inf (proj2 .: (a₂ /\ (north_halfline a₁))))]|;
correctness ;
func South-Bound c₁,c₂ -> Point of (TOP-REAL 2) equals :: JORDAN18:def 2
|[(a₁ `1 ),(sup (proj2 .: (a₂ /\ (south_halfline a₁))))]|;
correctness ;

end;

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

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

theorem Th20: :: JORDAN18:20

for b₁ being Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) holds
( (North-Bound b₂,b₁) `1 = b₂ `1 & (South-Bound b₂,b₁) `1 = b₂ `1 ) by EUCLID:56;

theorem Th21: :: JORDAN18:21

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

theorem Th22: :: JORDAN18:22

for b₁ being Point of (TOP-REAL 2)
for b₂ being compact Subset of (TOP-REAL 2) st b₁ in BDD b₂ holds
( North-Bound b₁,b₂ in b₂ & North-Bound b₁,b₂ in north_halfline b₁ & South-Bound b₁,b₂ in b₂ & South-Bound b₁,b₂ in south_halfline b₁ )

proof end;

theorem Th23: :: JORDAN18:23

for b₁ being Point of (TOP-REAL 2)
for b₂ being compact Subset of (TOP-REAL 2) st b₁ in BDD b₂ holds
( (South-Bound b₁,b₂) `2 < b₁ `2 & b₁ `2 < (North-Bound b₁,b₂) `2 )

proof end;

theorem Th24: :: JORDAN18:24

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

proof end;

theorem Th25: :: JORDAN18:25

for b₁ being Point of (TOP-REAL 2)
for b₂ being compact Subset of (TOP-REAL 2) st b₁ in BDD b₂ holds
South-Bound b₁,b₂ <> North-Bound b₁,b₂

proof end;

theorem Th26: :: JORDAN18:26

for b₁ being Point of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2) holds LSeg (North-Bound b₁,b₂),(South-Bound b₁,b₂) is vertical

proof end;

theorem Th27: :: JORDAN18:27

for b₁ being Point of (TOP-REAL 2)
for b₂ being compact Subset of (TOP-REAL 2) st b₁ in BDD b₂ holds
(LSeg (North-Bound b₁,b₂),(South-Bound b₁,b₂)) /\ b₂ = {(North-Bound b₁,b₂),(South-Bound b₁,b₂)}

proof end;

theorem Th28: :: JORDAN18:28

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being compact Subset of (TOP-REAL 2) st b₁ in BDD b₃ & b₂ in BDD b₃ & b₁ `1 <> b₂ `1 holds
North-Bound b₁,b₃, South-Bound b₂,b₃, North-Bound b₂,b₃, South-Bound b₁,b₃ are_mutually_different

proof end;

definition

let c₁ be Element of NAT ;
let c₂ be Subset of (TOP-REAL c₁);
let c₃, c₄, c₅, c₆ be Point of (TOP-REAL c₁);
pred c₃,c₄,c₂ -separate c₅,c₆ means :Def3: :: JORDAN18:def 3
for b₁ being Subset of (TOP-REAL a₁) st b₁ is_an_arc_of a₃,a₄ & b₁ c= a₂ holds
b₁ meets {a₅,a₆};

end;

:: deftheorem Def3 defines -separate JORDAN18:def 3 :

notation

let c₁ be Element of NAT ;
let c₂ be Subset of (TOP-REAL c₁);
let c₃, c₄, c₅, c₆ be Point of (TOP-REAL c₁);
antonym c₃,c₄ are_neighbours_wrt c₅,c₆,c₂ for c₃,c₄,c₂ -separate c₅,c₆;

end;

theorem Th29: :: JORDAN18:29

for b₁ being Element of NAT
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄, b₅ being Point of (TOP-REAL b₁) holds b₃,b₃,b₂ -separate b₄,b₅

proof end;

theorem Th30: :: JORDAN18:30

for b₁ being Element of NAT
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄, b₅, b₆ being Point of (TOP-REAL b₁) st b₃,b₄,b₂ -separate b₅,b₆ holds
b₄,b₃,b₂ -separate b₅,b₆

proof end;

theorem Th31: :: JORDAN18:31

for b₁ being Element of NAT
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄, b₅, b₆ being Point of (TOP-REAL b₁) st b₃,b₄,b₂ -separate b₅,b₆ holds
b₃,b₄,b₂ -separate b₆,b₅

proof end;

theorem Th32: :: JORDAN18:32

for b₁ being Element of NAT
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄, b₅ being Point of (TOP-REAL b₁) holds b₃,b₄,b₂ -separate b₃,b₅

proof end;

theorem Th33: :: JORDAN18:33

for b₁ being Element of NAT
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄, b₅ being Point of (TOP-REAL b₁) holds b₃,b₄,b₂ -separate b₅,b₄

proof end;

theorem Th34: :: JORDAN18:34

for b₁ being Element of NAT
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄, b₅ being Point of (TOP-REAL b₁) holds b₃,b₄,b₂ -separate b₄,b₅

proof end;

theorem Th35: :: JORDAN18:35

for b₁ being Element of NAT
for b₂ being Subset of (TOP-REAL b₁)
for b₃, b₄, b₅ being Point of (TOP-REAL b₁) holds b₃,b₄,b₂ -separate b₅,b₃

proof end;

theorem Th36: :: JORDAN18:36

for b₁ being Simple_closed_curve
for b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₄ in b₁ & b₂ in b₁ & b₃ in b₁ & b₂ <> b₃ & b₂ <> b₄ & b₃ <> b₄ holds
b₂,b₃ are_neighbours_wrt b₄,b₄,b₁

proof end;

theorem Th37: :: JORDAN18:37

for b₁ being Simple_closed_curve
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₂ <> b₃ & b₂ in b₁ & b₃ in b₁ & b₂,b₃,b₁ -separate b₄,b₅ holds
b₄,b₅,b₁ -separate b₂,b₃

proof end;

theorem Th38: :: JORDAN18:38

for b₁ being Simple_closed_curve
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₂ in b₁ & b₃ in b₁ & b₄ in b₁ & b₂ <> b₃ & b₄ <> b₂ & b₄ <> b₃ & b₅ <> b₂ & b₅ <> b₃ & not b₂,b₃ are_neighbours_wrt b₄,b₅,b₁ holds
b₂,b₄ are_neighbours_wrt b₃,b₅,b₁

proof end;