:: JORDAN_A semantic presentation

theorem Th1: :: JORDAN_A:1

for b₁, b₂ being non empty finite Subset of REAL holds min (b₁ \/ b₂) = min (min b₁),(min b₂)

proof end;

registration

let c₁ be non empty TopSpace;
cluster non empty compact Element of bool the carrier of a₁;
existence

proof end;

end;

theorem Th2: :: JORDAN_A:2

for b₁ being non empty TopSpace
for b₂ being continuous RealMap of b₁
for b₃ being compact Subset of b₁ holds b₂ .: b₃ is compact

proof end;

theorem Th3: :: JORDAN_A:3

for b₁ being compact Subset of REAL
for b₂ being non empty Subset of REAL st b₂ c= b₁ holds
inf b₂ in b₁

proof end;

theorem Th4: :: JORDAN_A:4

for b₁ being Nat
for b₂, b₃ being non empty compact Subset of (TOP-REAL b₁)
for b₄ being continuous RealMap of [:(TOP-REAL b₁),(TOP-REAL b₁):]
for b₅ being RealMap of (TOP-REAL b₁) st ( for b₆ being Point of (TOP-REAL b₁) ex b₇ being Subset of REAL st
( b₇ = { (b₄ . b₆,b₈) where B is Point of (TOP-REAL b₁) : b₈ in b₃ } & b₅ . b₆ = inf b₇ ) ) holds
inf (b₄ .: [:b₂,b₃:]) = inf (b₅ .: b₂)

proof end;

theorem Th5: :: JORDAN_A:5

for b₁ being Nat
for b₂, b₃ being non empty compact Subset of (TOP-REAL b₁)
for b₄ being continuous RealMap of [:(TOP-REAL b₁),(TOP-REAL b₁):]
for b₅ being RealMap of (TOP-REAL b₁) st ( for b₆ being Point of (TOP-REAL b₁) ex b₇ being Subset of REAL st
( b₇ = { (b₄ . b₈,b₆) where B is Point of (TOP-REAL b₁) : b₈ in b₂ } & b₅ . b₆ = inf b₇ ) ) holds
inf (b₄ .: [:b₂,b₃:]) = inf (b₅ .: b₃)

proof end;

theorem Th6: :: JORDAN_A:6

for b₁ being Simple_closed_curve
for b₂ being Point of (TOP-REAL 2) st b₂ in Lower_Arc b₁ & b₂ <> W-min b₁ holds
LE E-max b₁,b₂,b₁

proof end;

theorem Th7: :: JORDAN_A:7

for b₁ being Simple_closed_curve
for b₂ being Point of (TOP-REAL 2) st b₂ in Upper_Arc b₁ holds
LE b₂, E-max b₁,b₁

proof end;

definition

let c₁ be Nat;
E6: [:the carrier of (TOP-REAL c₁),the carrier of (TOP-REAL c₁):] = the carrier of [:(TOP-REAL c₁),(TOP-REAL c₁):] by BORSUK_1:def 5;
func Eucl_dist c₁ -> RealMap of [:(TOP-REAL a₁),(TOP-REAL a₁):] means :Def1: :: JORDAN_A:def 1
for b₁, b₂ being Point of (TOP-REAL a₁) holds a₂ . b₁,b₂ = |.(b₁ - b₂).|;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Eucl_dist JORDAN_A:def 1 :

definition

let c₁ be non empty TopSpace;
let c₂ be RealMap of c₁;
redefine attr a₂ is continuous means :: JORDAN_A:def 2
for b₁ being Point of a₁
for b₂ being Neighbourhood of a₂ . b₁ ex b₃ being a_neighborhood of b₁ st a₂ .: b₃ c= b₂;
compatibility

proof end;

end;

:: deftheorem Def2 defines continuous JORDAN_A:def 2 :

registration

let c₁ be Nat;
cluster Eucl_dist a₁ -> continuous ;
coherence

proof end;

end;

theorem Th8: :: JORDAN_A:8

for b₁ being Nat
for b₂, b₃ being non empty compact Subset of (TOP-REAL b₁) st b₂ misses b₃ holds
dist_min b₂,b₃ > 0

proof end;

theorem Th9: :: JORDAN_A:9

for b₁ being Simple_closed_curve
for b₂, b₃ being Point of (TOP-REAL 2) st LE b₂,b₃,b₁ & LE b₃, E-max b₁,b₁ & b₂ <> b₃ holds
Segment b₂,b₃,b₁ = Segment (Upper_Arc b₁),(W-min b₁),(E-max b₁),b₂,b₃

proof end;

theorem Th10: :: JORDAN_A:10

for b₁ being Simple_closed_curve
for b₂ being Point of (TOP-REAL 2) st LE E-max b₁,b₂,b₁ holds
Segment (E-max b₁),b₂,b₁ = Segment (Lower_Arc b₁),(E-max b₁),(W-min b₁),(E-max b₁),b₂

proof end;

theorem Th11: :: JORDAN_A:11

for b₁ being Simple_closed_curve
for b₂ being Point of (TOP-REAL 2) st LE E-max b₁,b₂,b₁ holds
Segment b₂,(W-min b₁),b₁ = Segment (Lower_Arc b₁),(E-max b₁),(W-min b₁),b₂,(W-min b₁)

proof end;

theorem Th12: :: JORDAN_A:12

for b₁ being Simple_closed_curve
for b₂, b₃ being Point of (TOP-REAL 2) st LE b₂,b₃,b₁ & LE E-max b₁,b₂,b₁ holds
Segment b₂,b₃,b₁ = Segment (Lower_Arc b₁),(E-max b₁),(W-min b₁),b₂,b₃

proof end;

theorem Th13: :: JORDAN_A:13

for b₁ being Simple_closed_curve
for b₂, b₃ being Point of (TOP-REAL 2) st LE b₂, E-max b₁,b₁ & LE E-max b₁,b₃,b₁ holds
Segment b₂,b₃,b₁ = (R_Segment (Upper_Arc b₁),(W-min b₁),(E-max b₁),b₂) \/ (L_Segment (Lower_Arc b₁),(E-max b₁),(W-min b₁),b₃)

proof end;

theorem Th14: :: JORDAN_A:14

for b₁ being Simple_closed_curve
for b₂ being Point of (TOP-REAL 2) st LE b₂, E-max b₁,b₁ holds
Segment b₂,(W-min b₁),b₁ = (R_Segment (Upper_Arc b₁),(W-min b₁),(E-max b₁),b₂) \/ (L_Segment (Lower_Arc b₁),(E-max b₁),(W-min b₁),(W-min b₁))

proof end;

theorem Th15: :: JORDAN_A:15

for b₁ being Simple_closed_curve
for b₂ being Point of (TOP-REAL 2) holds R_Segment (Upper_Arc b₁),(W-min b₁),(E-max b₁),b₂ = Segment (Upper_Arc b₁),(W-min b₁),(E-max b₁),b₂,(E-max b₁)

proof end;

theorem Th16: :: JORDAN_A:16

for b₁ being Simple_closed_curve
for b₂ being Point of (TOP-REAL 2) holds L_Segment (Lower_Arc b₁),(E-max b₁),(W-min b₁),b₂ = Segment (Lower_Arc b₁),(E-max b₁),(W-min b₁),(E-max b₁),b₂

proof end;

theorem Th17: :: JORDAN_A:17

for b₁ being Simple_closed_curve
for b₂ being Point of (TOP-REAL 2) st b₂ in b₁ & b₂ <> W-min b₁ holds
Segment b₂,(W-min b₁),b₁ is_an_arc_of b₂, W-min b₁

proof end;

theorem Th18: :: JORDAN_A:18

for b₁ being Simple_closed_curve
for b₂, b₃ being Point of (TOP-REAL 2) st b₂ <> b₃ & LE b₂,b₃,b₁ holds
Segment b₂,b₃,b₁ is_an_arc_of b₂,b₃

proof end;

theorem Th19: :: JORDAN_A:19

for b₁ being Simple_closed_curve holds b₁ = Segment (W-min b₁),(W-min b₁),b₁

proof end;

theorem Th20: :: JORDAN_A:20

for b₁ being Simple_closed_curve
for b₂ being Point of (TOP-REAL 2) st b₂ in b₁ holds
Segment b₂,(W-min b₁),b₁ is compact

proof end;

theorem Th21: :: JORDAN_A:21

for b₁ being Simple_closed_curve
for b₂, b₃ being Point of (TOP-REAL 2) st LE b₂,b₃,b₁ holds
Segment b₂,b₃,b₁ is compact

proof end;

definition

let c₁ be Simple_closed_curve;
mode Segmentation of c₁ -> FinSequence of (TOP-REAL 2) means :Def3: :: JORDAN_A:def 3
( a₂ /. 1 = W-min a₁ & a₂ is one-to-one & 8 <= len a₂ & rng a₂ c= a₁ & ( for b₁ being Nat st 1 <= b₁ & b₁ < len a₂ holds
LE a₂ /. b₁,a₂ /. (b₁ + 1),a₁ ) & ( for b₁ being Nat st 1 <= b₁ & b₁ + 1 < len a₂ holds
(Segment (a₂ /. b₁),(a₂ /. (b₁ + 1)),a₁) /\ (Segment (a₂ /. (b₁ + 1)),(a₂ /. (b₁ + 2)),a₁) = {(a₂ /. (b₁ + 1))} ) & (Segment (a₂ /. (len a₂)),(a₂ /. 1),a₁) /\ (Segment (a₂ /. 1),(a₂ /. 2),a₁) = {(a₂ /. 1)} & (Segment (a₂ /. ((len a₂) -' 1)),(a₂ /. (len a₂)),a₁) /\ (Segment (a₂ /. (len a₂)),(a₂ /. 1),a₁) = {(a₂ /. (len a₂))} & Segment (a₂ /. ((len a₂) -' 1)),(a₂ /. (len a₂)),a₁ misses Segment (a₂ /. 1),(a₂ /. 2),a₁ & ( for b₁, b₂ being Nat st 1 <= b₁ & b₁ < b₂ & b₂ < len a₂ & not b₁,b₂ are_adjacent1 holds
Segment (a₂ /. b₁),(a₂ /. (b₁ + 1)),a₁ misses Segment (a₂ /. b₂),(a₂ /. (b₂ + 1)),a₁ ) & ( for b₁ being Nat st 1 < b₁ & b₁ + 1 < len a₂ holds
Segment (a₂ /. (len a₂)),(a₂ /. 1),a₁ misses Segment (a₂ /. b₁),(a₂ /. (b₁ + 1)),a₁ ) );
existence

proof end;

end;

:: deftheorem Def3 defines Segmentation JORDAN_A:def 3 :

registration

let c₁ be Simple_closed_curve;
cluster -> non trivial Segmentation of a₁;
coherence

proof end;

end;

theorem Th22: :: JORDAN_A:22

for b₁ being Simple_closed_curve
for b₂ being Segmentation of b₁
for b₃ being Nat st 1 <= b₃ & b₃ <= len b₂ holds
b₂ /. b₃ in b₁

proof end;

definition

let c₁ be Simple_closed_curve;
let c₂ be natural number ;
let c₃ be Segmentation of c₁;
func Segm c₃,c₂ -> Subset of (TOP-REAL 2) equals :Def4: :: JORDAN_A:def 4
Segment (a₃ /. a₂),(a₃ /. (a₂ + 1)),a₁ if ( 1 <= a₂ & a₂ < len a₃ )
otherwise Segment (a₃ /. (len a₃)),(a₃ /. 1),a₁;
correctness ;

end;

:: deftheorem Def4 defines Segm JORDAN_A:def 4 :

theorem Th23: :: JORDAN_A:23

for b₁ being Simple_closed_curve
for b₂ being Nat
for b₃ being Segmentation of b₁ st b₂ in dom b₃ holds
Segm b₃,b₂ c= b₁

proof end;

registration

let c₁ be Simple_closed_curve;
let c₂ be Segmentation of c₁;
let c₃ be Nat;
cluster Segm a₂,a₃ -> non empty compact ;
coherence

proof end;

end;

theorem Th24: :: JORDAN_A:24

for b₁ being Simple_closed_curve
for b₂ being Segmentation of b₁
for b₃ being Point of (TOP-REAL 2) st b₃ in b₁ holds
ex b₄ being natural number st
( b₄ in dom b₂ & b₃ in Segm b₂,b₄ )

proof end;

theorem Th25: :: JORDAN_A:25

for b₁ being Simple_closed_curve
for b₂ being Segmentation of b₁
for b₃, b₄ being Nat st 1 <= b₃ & b₃ < b₄ & b₄ < len b₂ & not b₃,b₄ are_adjacent1 holds
Segm b₂,b₃ misses Segm b₂,b₄

proof end;

theorem Th26: :: JORDAN_A:26

for b₁ being Simple_closed_curve
for b₂ being Segmentation of b₁
for b₃ being Nat st 1 < b₃ & b₃ < (len b₂) -' 1 holds
Segm b₂,(len b₂) misses Segm b₂,b₃

proof end;

theorem Th27: :: JORDAN_A:27

for b₁ being Simple_closed_curve
for b₂ being Segmentation of b₁
for b₃, b₄ being Nat st 1 <= b₃ & b₃ < b₄ & b₄ < len b₂ & b₃,b₄ are_adjacent1 holds
(Segm b₂,b₃) /\ (Segm b₂,b₄) = {(b₂ /. (b₃ + 1))}

proof end;

theorem Th28: :: JORDAN_A:28

for b₁ being Simple_closed_curve
for b₂ being Segmentation of b₁
for b₃, b₄ being Nat st 1 <= b₃ & b₃ < b₄ & b₄ < len b₂ & b₃,b₄ are_adjacent1 holds
Segm b₂,b₃ meets Segm b₂,b₄

proof end;

theorem Th29: :: JORDAN_A:29

for b₁ being Simple_closed_curve
for b₂ being Segmentation of b₁ holds (Segm b₂,(len b₂)) /\ (Segm b₂,1) = {(b₂ /. 1)}

proof end;

theorem Th30: :: JORDAN_A:30

for b₁ being Simple_closed_curve
for b₂ being Segmentation of b₁ holds Segm b₂,(len b₂) meets Segm b₂,1

proof end;

theorem Th31: :: JORDAN_A:31

for b₁ being Simple_closed_curve
for b₂ being Segmentation of b₁ holds (Segm b₂,(len b₂)) /\ (Segm b₂,((len b₂) -' 1)) = {(b₂ /. (len b₂))}

proof end;

theorem Th32: :: JORDAN_A:32

for b₁ being Simple_closed_curve
for b₂ being Segmentation of b₁ holds Segm b₂,(len b₂) meets Segm b₂,((len b₂) -' 1)

proof end;

definition

let c₁ be Nat;
let c₂ be Subset of (TOP-REAL c₁);
func diameter c₂ -> Real means :Def5: :: JORDAN_A:def 5
ex b₁ being Subset of (Euclid a₁) st
( b₁ = a₂ & a₃ = diameter b₁ );
existence

proof end;

correctness ;

end;

:: deftheorem Def5 defines diameter JORDAN_A:def 5 :

definition

let c₁ be Simple_closed_curve;
let c₂ be Segmentation of c₁;
func diameter c₂ -> Real means :Def6: :: JORDAN_A:def 6
ex b₁ being non empty finite Subset of REAL st
( b₁ = { (diameter (Segm a₂,b₂)) where B is Nat : b₂ in dom a₂ } & a₃ = max b₁ );
existence

proof end;

correctness ;

end;

:: deftheorem Def6 defines diameter JORDAN_A:def 6 :

theorem Th33: :: JORDAN_A:33

for b₁ being Simple_closed_curve
for b₂ being Segmentation of b₁
for b₃ being Nat holds diameter (Segm b₂,b₃) <= diameter b₂

proof end;

theorem Th34: :: JORDAN_A:34

for b₁ being Simple_closed_curve
for b₂ being Segmentation of b₁
for b₃ being Real st ( for b₄ being Nat holds diameter (Segm b₂,b₄) < b₃ ) holds
diameter b₂ < b₃

proof end;

theorem Th35: :: JORDAN_A:35

for b₁ being Simple_closed_curve
for b₂ being Real st b₂ > 0 holds
ex b₃ being Segmentation of b₁ st diameter b₃ < b₂

proof end;

definition

let c₁ be Simple_closed_curve;
let c₂ be Segmentation of c₁;
func S-Gap c₂ -> Real means :Def7: :: JORDAN_A:def 7
ex b₁, b₂ being non empty finite Subset of REAL st
( b₁ = { (dist_min (Segm a₂,b₃),(Segm a₂,b₄)) where B is Nat, B is Nat : ( 1 <= b₃ & b₃ < b₄ & b₄ < len a₂ & not b₃,b₄ are_adjacent1 ) } & b₂ = { (dist_min (Segm a₂,(len a₂)),(Segm a₂,b₃)) where B is Nat : ( 1 < b₃ & b₃ < (len a₂) -' 1 ) } & a₃ = min (min b₁),(min b₂) );
existence

proof end;

correctness ;

end;

:: deftheorem Def7 defines S-Gap JORDAN_A:def 7 :

theorem Th36: :: JORDAN_A:36

for b₁ being Simple_closed_curve
for b₂ being Segmentation of b₁ ex b₃ being non empty finite Subset of REAL st
( b₃ = { (dist_min (Segm b₂,b₄),(Segm b₂,b₅)) where B is Nat, B is Nat : ( 1 <= b₄ & b₄ < b₅ & b₅ <= len b₂ & Segm b₂,b₄ misses Segm b₂,b₅ ) } & S-Gap b₂ = min b₃ )

proof end;

theorem Th37: :: JORDAN_A:37

for b₁ being Simple_closed_curve
for b₂ being Segmentation of b₁ holds S-Gap b₂ > 0

proof end;