:: JORDAN21 semantic presentation

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

Lm2: for r being real number
for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds
ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r )

proof end;

Lm3: now

let a, A, B, C be set ; :: thesis:
assume a in (A \/ B) \/ C ; :: thesis:
then ( a in A \/ B or a in C ) by XBOOLE_0:def 2;
hence ( a in A or a in B or a in C ) by XBOOLE_0:def 2; :: thesis:

end;

Lm4: for A, B, C, D being set st A misses D & B misses D & C misses D holds
(A \/ B) \/ C misses D

proof end;

theorem Th1: :: JORDAN21:1

for n being Nat
for p being Point of (TOP-REAL n) holds {p} is Bounded

proof end;

theorem Th2: :: JORDAN21:2

for s1, t being real number
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s is Real : s1 < s } holds
P is convex

proof end;

theorem Th3: :: JORDAN21:3

for s2, t being real number
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s is Real : s < s2 } holds
P is convex

proof end;

theorem Th4: :: JORDAN21:4

for s, t1 being real number
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where t is Real : t1 < t } holds
P is convex

proof end;

theorem Th5: :: JORDAN21:5

for s, t2 being real number
for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where t is Real : t < t2 } holds
P is convex

proof end;

theorem Th6: :: JORDAN21:6

for p being Point of (TOP-REAL 2) holds (north_halfline p) \ {p} is convex

proof end;

theorem Th7: :: JORDAN21:7

for p being Point of (TOP-REAL 2) holds (south_halfline p) \ {p} is convex

proof end;

theorem :: JORDAN21:8

for p being Point of (TOP-REAL 2) holds (west_halfline p) \ {p} is convex

proof end;

theorem :: JORDAN21:9

for p being Point of (TOP-REAL 2) holds (east_halfline p) \ {p} is convex

proof end;

theorem Th10: :: JORDAN21:10

for A being Subset of the carrier of (TOP-REAL 2) holds UBD A misses A

proof end;

theorem Th11: :: JORDAN21:11

for P being Subset of the carrier of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & p1 <> q1 & p2 <> q2 holds
( not p1 in Segment P,p1,p2,q1,q2 & not p2 in Segment P,p1,p2,q1,q2 )

proof end;

definition

let D be Subset of (TOP-REAL 2);
attr D is with_the_max_arc means :Def1: :: JORDAN21:def 1
D meets Vertical_Line (((W-bound D) + (E-bound D)) / 2);

end;

:: deftheorem Def1 defines with_the_max_arc JORDAN21:def 1 :

registration

cluster with_the_max_arc -> non empty Element of K40(the carrier of (TOP-REAL 2));
coherence

proof end;

end;

Lm5: for C being Simple_closed_curve holds Upper_Middle_Point C in C

proof end;

registration

cluster -> non empty with_the_max_arc Element of K40(the carrier of (TOP-REAL 2));
coherence

proof end;

end;

registration

cluster non empty with_the_max_arc Element of K40(the carrier of (TOP-REAL 2));
existence

proof end;

end;

theorem Th12: :: JORDAN21:12

for D being with_the_max_arc Subset of (TOP-REAL 2) holds not proj2 .: (D /\ (Vertical_Line (((W-bound D) + (E-bound D)) / 2))) is empty

proof end;

theorem Th13: :: JORDAN21:13

for C being compact Subset of (TOP-REAL 2) holds
( proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is closed & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_below & proj2 .: (C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is bounded_above )

proof end;

Lm6: for R being non empty Subset of (TOP-REAL 2)
for n being Nat holds 1 <= len (Gauge R,n)

proof end;

theorem Th14: :: JORDAN21:14

for R being non empty Subset of (TOP-REAL 2)
for n being Nat holds [1,1] in Indices (Gauge R,n)

proof end;

theorem Th15: :: JORDAN21:15

for R being non empty Subset of (TOP-REAL 2)
for n being Nat holds [1,2] in Indices (Gauge R,n)

proof end;

theorem Th16: :: JORDAN21:16

for R being non empty Subset of (TOP-REAL 2)
for n being Nat holds [2,1] in Indices (Gauge R,n)

proof end;

theorem Th17: :: JORDAN21:17

for m, k, i, j being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge C,k) & [i,(j + 1)] in Indices (Gauge C,k) holds
dist ((Gauge C,m) * i,j),((Gauge C,m) * i,(j + 1)) < dist ((Gauge C,k) * i,j),((Gauge C,k) * i,(j + 1))

proof end;

theorem Th18: :: JORDAN21:18

for m, k being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds
dist ((Gauge C,m) * 1,1),((Gauge C,m) * 1,2) < dist ((Gauge C,k) * 1,1),((Gauge C,k) * 1,2)

proof end;

theorem Th19: :: JORDAN21:19

for m, k, i, j being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge C,k) & [(i + 1),j] in Indices (Gauge C,k) holds
dist ((Gauge C,m) * i,j),((Gauge C,m) * (i + 1),j) < dist ((Gauge C,k) * i,j),((Gauge C,k) * (i + 1),j)

proof end;

theorem Th20: :: JORDAN21:20

for m, k being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k holds
dist ((Gauge C,m) * 1,1),((Gauge C,m) * 2,1) < dist ((Gauge C,k) * 1,1),((Gauge C,k) * 2,1)

proof end;

theorem :: JORDAN21:21

for C being Simple_closed_curve
for i being Nat
for r, t being real number st r > 0 & t > 0 holds
ex n being Nat st
( i < n & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r & dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < t )

proof end;

theorem Th22: :: JORDAN21:22

for C being Simple_closed_curve holds Upper_Middle_Point C in C by Lm5;

theorem Th23: :: JORDAN21:23

for C being Simple_closed_curve holds Lower_Middle_Point C in C

proof end;

theorem Th24: :: JORDAN21:24

for C being Simple_closed_curve holds (Lower_Middle_Point C) `2 <> (Upper_Middle_Point C) `2

proof end;

theorem :: JORDAN21:25

for C being Simple_closed_curve holds Lower_Middle_Point C <> Upper_Middle_Point C

proof end;

theorem Th26: :: JORDAN21:26

for C being Simple_closed_curve holds W-bound C = W-bound (Upper_Arc C)

proof end;

theorem Th27: :: JORDAN21:27

for C being Simple_closed_curve holds E-bound C = E-bound (Upper_Arc C)

proof end;

theorem Th28: :: JORDAN21:28

for C being Simple_closed_curve holds W-bound C = W-bound (Lower_Arc C)

proof end;

theorem Th29: :: JORDAN21:29

for C being Simple_closed_curve holds E-bound C = E-bound (Lower_Arc C)

proof end;

theorem Th30: :: JORDAN21:30

for C being Simple_closed_curve holds
( not (Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Upper_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty )

proof end;

theorem Th31: :: JORDAN21:31

for C being Simple_closed_curve holds
( not (Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) is empty & not proj2 .: ((Lower_Arc C) /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is empty )

proof end;

theorem :: JORDAN21:32

for C being Simple_closed_curve
for P being connected compact Subset of (TOP-REAL 2) st P c= C & W-min C in P & E-max C in P & not Upper_Arc C c= P holds
Lower_Arc C c= P

proof end;

definition

let P be Subset of the carrier of (TOP-REAL 2);
func UMP P -> Point of (TOP-REAL 2) equals :: JORDAN21:def 2
|[(((E-bound P) + (W-bound P)) / 2),(sup (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]|;
correctness ;
func LMP P -> Point of (TOP-REAL 2) equals :: JORDAN21:def 3
|[(((E-bound P) + (W-bound P)) / 2),(inf (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))))]|;
correctness ;

end;

:: deftheorem defines UMP JORDAN21:def 2 :

:: deftheorem defines LMP JORDAN21:def 3 :

theorem :: JORDAN21:33

for P being Subset of (TOP-REAL 2) holds (UMP P) `1 = ((W-bound P) + (E-bound P)) / 2 by EUCLID:56;

theorem :: JORDAN21:34

for P being Subset of (TOP-REAL 2) holds (UMP P) `2 = sup (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))) by EUCLID:56;

theorem :: JORDAN21:35

for P being Subset of (TOP-REAL 2) holds (LMP P) `1 = ((W-bound P) + (E-bound P)) / 2 by EUCLID:56;

theorem :: JORDAN21:36

for P being Subset of (TOP-REAL 2) holds (LMP P) `2 = inf (proj2 .: (P /\ (Vertical_Line (((E-bound P) + (W-bound P)) / 2)))) by EUCLID:56;

theorem Th37: :: JORDAN21:37

for C being compact non vertical Subset of (TOP-REAL 2) holds UMP C <> W-min C

proof end;

theorem Th38: :: JORDAN21:38

for C being compact non vertical Subset of (TOP-REAL 2) holds UMP C <> E-max C

proof end;

theorem Th39: :: JORDAN21:39

for C being compact non vertical Subset of (TOP-REAL 2) holds LMP C <> W-min C

proof end;

theorem Th40: :: JORDAN21:40

for C being compact non vertical Subset of (TOP-REAL 2) holds LMP C <> E-max C

proof end;

theorem Th41: :: JORDAN21:41

for p being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) holds
p `2 <= (UMP C) `2

proof end;

theorem Th42: :: JORDAN21:42

for p being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in C /\ (Vertical_Line (((W-bound C) + (E-bound C)) / 2)) holds
(LMP C) `2 <= p `2

proof end;

theorem Th43: :: JORDAN21:43

for D being compact with_the_max_arc Subset of (TOP-REAL 2) holds UMP D in D

proof end;

theorem Th44: :: JORDAN21:44

for D being compact with_the_max_arc Subset of (TOP-REAL 2) holds LMP D in D

proof end;

theorem Th45: :: JORDAN21:45

for P being Subset of (TOP-REAL 2) holds LSeg (UMP P),|[(((W-bound P) + (E-bound P)) / 2),(N-bound P)]| is vertical

proof end;

theorem Th46: :: JORDAN21:46

for P being Subset of (TOP-REAL 2) holds LSeg (LMP P),|[(((W-bound P) + (E-bound P)) / 2),(S-bound P)]| is vertical

proof end;

theorem Th47: :: JORDAN21:47

for D being compact with_the_max_arc Subset of (TOP-REAL 2) holds (LSeg (UMP D),|[(((W-bound D) + (E-bound D)) / 2),(N-bound D)]|) /\ D = {(UMP D)}

proof end;

theorem Th48: :: JORDAN21:48

for D being compact with_the_max_arc Subset of (TOP-REAL 2) holds (LSeg (LMP D),|[(((W-bound D) + (E-bound D)) / 2),(S-bound D)]|) /\ D = {(LMP D)}

proof end;

theorem Th49: :: JORDAN21:49

for C being Simple_closed_curve holds (LMP C) `2 < (UMP C) `2

proof end;

theorem Th50: :: JORDAN21:50

for C being Simple_closed_curve holds UMP C <> LMP C

proof end;

theorem Th51: :: JORDAN21:51

for C being Simple_closed_curve holds S-bound C < (UMP C) `2

proof end;

theorem Th52: :: JORDAN21:52

for C being Simple_closed_curve holds (UMP C) `2 <= N-bound C

proof end;

theorem Th53: :: JORDAN21:53

for C being Simple_closed_curve holds S-bound C <= (LMP C) `2

proof end;

theorem Th54: :: JORDAN21:54

for C being Simple_closed_curve holds (LMP C) `2 < N-bound C

proof end;

theorem Th55: :: JORDAN21:55

for C being Simple_closed_curve holds LSeg (UMP C),|[(((W-bound C) + (E-bound C)) / 2),(N-bound C)]| misses LSeg (LMP C),|[(((W-bound C) + (E-bound C)) / 2),(S-bound C)]|

proof end;

theorem Th56: :: JORDAN21:56

for A, B being Subset of (TOP-REAL 2) st A c= B & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2))) is bounded_above holds
(UMP A) `2 <= (UMP B) `2

proof end;

theorem Th57: :: JORDAN21:57

proof end;

theorem Th58: :: JORDAN21:58

for A, B being Subset of (TOP-REAL 2) st A c= B & UMP B in A & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound B) + (E-bound B)) / 2))) is bounded_above & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) holds
UMP A = UMP B

proof end;

theorem Th59: :: JORDAN21:59

for A, B being Subset of (TOP-REAL 2) st A c= B & LMP B in A & not A /\ (Vertical_Line (((W-bound A) + (E-bound A)) / 2)) is empty & proj2 .: (B /\ (Vertical_Line (((W-bound B) + (E-bound B)) / 2))) is bounded_below & (W-bound A) + (E-bound A) = (W-bound B) + (E-bound B) holds
LMP A = LMP B

proof end;

theorem :: JORDAN21:60

for C being Simple_closed_curve holds (UMP (Upper_Arc C)) `2 <= N-bound C

proof end;

theorem :: JORDAN21:61

for C being Simple_closed_curve holds S-bound C <= (LMP (Lower_Arc C)) `2

proof end;

theorem :: JORDAN21:62

for C being Simple_closed_curve holds
( not LMP C in Lower_Arc C or not UMP C in Lower_Arc C )

proof end;

theorem :: JORDAN21:63

for C being Simple_closed_curve holds
( not LMP C in Upper_Arc C or not UMP C in Upper_Arc C )

proof end;

theorem Th64: :: JORDAN21:64

for C being Simple_closed_curve
for n being Nat st 0 < n holds
sup (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))) = sup (proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2))))

proof end;

theorem Th65: :: JORDAN21:65

for C being Simple_closed_curve
for n being Nat st 0 < n holds
inf (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))) = inf (proj2 .: ((L~ (Cage C,n)) /\ (Vertical_Line (((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2))))

proof end;

theorem Th66: :: JORDAN21:66

for C being Simple_closed_curve
for n being Nat st 0 < n holds
UMP (L~ (Cage C,n)) = |[(((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2),(sup (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))))]| by Th64;

theorem Th67: :: JORDAN21:67

for C being Simple_closed_curve
for n being Nat st 0 < n holds
LMP (L~ (Cage C,n)) = |[(((E-bound (L~ (Cage C,n))) + (W-bound (L~ (Cage C,n)))) / 2),(inf (proj2 .: ((L~ (Cage C,n)) /\ (LSeg ((Gauge C,n) * (Center (Gauge C,n)),1),((Gauge C,n) * (Center (Gauge C,n)),(len (Gauge C,n)))))))]| by Th65;

theorem Th68: :: JORDAN21:68

for C being Simple_closed_curve
for n being Nat holds (UMP C) `2 < (UMP (L~ (Cage C,n))) `2

proof end;

theorem Th69: :: JORDAN21:69

for C being Simple_closed_curve
for n being Nat holds (LMP C) `2 > (LMP (L~ (Cage C,n))) `2

proof end;

registration

let C be Simple_closed_curve;
cluster Lower_Arc C -> with_the_max_arc ;
coherence

proof end;

cluster Upper_Arc C -> with_the_max_arc ;
coherence

proof end;

end;

theorem :: JORDAN21:70

for C being Simple_closed_curve
for n being Nat holds UMP (Upper_Arc (L~ (Cage C,n))) in Upper_Arc (L~ (Cage C,n)) by Th43;

theorem :: JORDAN21:71

for C being Simple_closed_curve
for n being Nat holds LMP (Lower_Arc (L~ (Cage C,n))) in Lower_Arc (L~ (Cage C,n)) by Th44;

theorem Th72: :: JORDAN21:72

for C being Simple_closed_curve
for n being Nat st 0 < n holds
ex i being Nat st
( 1 <= i & i <= len (Gauge C,n) & UMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),i )

proof end;

theorem Th73: :: JORDAN21:73

for C being Simple_closed_curve
for n being Nat st 0 < n holds
ex i being Nat st
( 1 <= i & i <= len (Gauge C,n) & LMP (L~ (Cage C,n)) = (Gauge C,n) * (Center (Gauge C,n)),i )

proof end;

theorem Th74: :: JORDAN21:74

for C being Simple_closed_curve
for n being Nat st 0 < n holds
UMP (L~ (Cage C,n)) = UMP (Upper_Arc (L~ (Cage C,n)))

proof end;

theorem Th75: :: JORDAN21:75

for C being Simple_closed_curve
for n being Nat st 0 < n holds
LMP (L~ (Cage C,n)) = LMP (Lower_Arc (L~ (Cage C,n)))

proof end;

theorem :: JORDAN21:76

for C being Simple_closed_curve
for n being Nat st 0 < n holds
(UMP C) `2 < (UMP (Upper_Arc (L~ (Cage C,n)))) `2

proof end;

theorem :: JORDAN21:77

for C being Simple_closed_curve
for n being Nat st 0 < n holds
(LMP (Lower_Arc (L~ (Cage C,n)))) `2 < (LMP C) `2

proof end;

theorem Th78: :: JORDAN21:78

for C being Simple_closed_curve
for i, j being Nat st i <= j holds
(UMP (L~ (Cage C,j))) `2 <= (UMP (L~ (Cage C,i))) `2

proof end;

theorem Th79: :: JORDAN21:79

for C being Simple_closed_curve
for i, j being Nat st i <= j holds
(LMP (L~ (Cage C,i))) `2 <= (LMP (L~ (Cage C,j))) `2

proof end;

theorem :: JORDAN21:80

for C being Simple_closed_curve
for i, j being Nat st 0 < i & i <= j holds
(UMP (Upper_Arc (L~ (Cage C,j)))) `2 <= (UMP (Upper_Arc (L~ (Cage C,i)))) `2

proof end;

theorem :: JORDAN21:81

for C being Simple_closed_curve
for i, j being Nat st 0 < i & i <= j holds
(LMP (Lower_Arc (L~ (Cage C,i)))) `2 <= (LMP (Lower_Arc (L~ (Cage C,j)))) `2

proof end;