:: JORDAN19 semantic presentation

definition
let c1 be Simple_closed_curve;
func Upper_Appr c1 -> SetSequence of the carrier of (TOP-REAL 2) means :Def1: :: JORDAN19:def 1
for b1 being Nat holds a2 . b1 = Upper_Arc (L~ (Cage a1,b1));
existence
ex b1 being SetSequence of the carrier of (TOP-REAL 2) st
for b2 being Nat holds b1 . b2 = Upper_Arc (L~ (Cage c1,b2))
proof end;
uniqueness
for b1, b2 being SetSequence of the carrier of (TOP-REAL 2) st ( for b3 being Nat holds b1 . b3 = Upper_Arc (L~ (Cage c1,b3)) ) & ( for b3 being Nat holds b2 . b3 = Upper_Arc (L~ (Cage c1,b3)) ) holds
b1 = b2
proof end;
func Lower_Appr c1 -> SetSequence of the carrier of (TOP-REAL 2) means :Def2: :: JORDAN19:def 2
for b1 being Nat holds a2 . b1 = Lower_Arc (L~ (Cage a1,b1));
existence
ex b1 being SetSequence of the carrier of (TOP-REAL 2) st
for b2 being Nat holds b1 . b2 = Lower_Arc (L~ (Cage c1,b2))
proof end;
uniqueness
for b1, b2 being SetSequence of the carrier of (TOP-REAL 2) st ( for b3 being Nat holds b1 . b3 = Lower_Arc (L~ (Cage c1,b3)) ) & ( for b3 being Nat holds b2 . b3 = Lower_Arc (L~ (Cage c1,b3)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Upper_Appr JORDAN19:def 1 :
for b1 being Simple_closed_curve
for b2 being SetSequence of the carrier of (TOP-REAL 2) holds
( b2 = Upper_Appr b1 iff for b3 being Nat holds b2 . b3 = Upper_Arc (L~ (Cage b1,b3)) );

:: deftheorem Def2 defines Lower_Appr JORDAN19:def 2 :
for b1 being Simple_closed_curve
for b2 being SetSequence of the carrier of (TOP-REAL 2) holds
( b2 = Lower_Appr b1 iff for b3 being Nat holds b2 . b3 = Lower_Arc (L~ (Cage b1,b3)) );

definition
let c1 be Simple_closed_curve;
func North_Arc c1 -> Subset of (TOP-REAL 2) equals :: JORDAN19:def 3
 Lim_inf (Upper_Appr a1);
coherence
Lim_inf (Upper_Appr c1) is Subset of (TOP-REAL 2) ;
func South_Arc c1 -> Subset of (TOP-REAL 2) equals :: JORDAN19:def 4
 Lim_inf (Lower_Appr a1);
coherence
Lim_inf (Lower_Appr c1) is Subset of (TOP-REAL 2) ;
end;

:: deftheorem Def3 defines North_Arc JORDAN19:def 3 :
for b1 being Simple_closed_curve holds North_Arc b1 = Lim_inf (Upper_Appr b1);

:: deftheorem Def4 defines South_Arc JORDAN19:def 4 :
for b1 being Simple_closed_curve holds South_Arc b1 = Lim_inf (Lower_Appr b1);

E3: now
let c1 be Go-board;
let c2 be Nat;
assume E4: ( 1 <= c2 & c2 <= width c1 ) ;
0 + 1 <= ((len c1) div 2) + 1 by XREAL_1:8;
then E5: 0 + 1 <= Center c1 by JORDAN1A:def 1;
Center c1 <= len c1 by JORDAN1B:14;
hence [(Center c1),c2] in Indices c1 by E4, E5, GOBOARD7:10;
end;

E4: now
let c1 be non empty Subset of (TOP-REAL 2);
let c2, c3 be Nat;
set c4 = N-bound c1;
set c5 = S-bound c1;
set c6 = W-bound c1;
set c7 = E-bound c1;
set c8 = Gauge c1,c2;
assume [c3,(width (Gauge c1,c2))] in Indices (Gauge c1,c2) ;
hence ((Gauge c1,c2) * c3,(width (Gauge c1,c2))) `2 = |[((W-bound c1) + ((((E-bound c1) - (W-bound c1)) / (2 |^ c2)) * (c3 - 2))),((S-bound c1) + ((((N-bound c1) - (S-bound c1)) / (2 |^ c2)) * ((width (Gauge c1,c2)) - 2)))]| `2 by JORDAN8:def 1
.= (S-bound c1) + ((((N-bound c1) - (S-bound c1)) / (2 |^ c2)) * ((width (Gauge c1,c2)) - 2)) by EUCLID:56 ;

end;

theorem Th1: :: JORDAN19:1
for b1, b2 being Nat st b1 <= b2 & b1 <> 0 holds
(b1 + 1) / b1 >= (b2 + 1) / b2
proof end;

theorem Th2: :: JORDAN19:2
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4 being Nat st 1 <= b3 & b3 <= b1 & 1 <= b4 & b4 <= width (Gauge b2,b1) holds
LSeg ((Gauge b2,b1) * (Center (Gauge b2,b1)),(width (Gauge b2,b1))),((Gauge b2,b1) * (Center (Gauge b2,b1)),b4) c= LSeg ((Gauge b2,b3) * (Center (Gauge b2,b3)),(width (Gauge b2,b3))),((Gauge b2,b1) * (Center (Gauge b2,b1)),b4)
proof end;

theorem Th3: :: JORDAN19:3
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4 being Nat st 1 <= b3 & b3 <= len (Gauge b2,b1) & 1 <= b4 & b4 <= width (Gauge b2,b1) & (Gauge b2,b1) * b3,b4 in L~ (Cage b2,b1) holds
LSeg ((Gauge b2,b1) * b3,(width (Gauge b2,b1))),((Gauge b2,b1) * b3,b4) meets L~ (Upper_Seq b2,b1)
proof end;

theorem Th4: :: JORDAN19:4
for b1 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b2 being Nat st b2 > 0 holds
for b3, b4 being Nat st 1 <= b3 & b3 <= len (Gauge b1,b2) & 1 <= b4 & b4 <= width (Gauge b1,b2) & (Gauge b1,b2) * b3,b4 in L~ (Cage b1,b2) holds
LSeg ((Gauge b1,b2) * b3,(width (Gauge b1,b2))),((Gauge b1,b2) * b3,b4) meets Upper_Arc (L~ (Cage b1,b2))
proof end;

theorem Th5: :: JORDAN19:5
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3 being Nat st (Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3 in Lower_Arc (L~ (Cage b2,(b1 + 1))) & 1 <= b3 & b3 <= width (Gauge b2,(b1 + 1)) holds
LSeg ((Gauge b2,1) * (Center (Gauge b2,1)),(width (Gauge b2,1))),((Gauge b2,(b1 + 1)) * (Center (Gauge b2,(b1 + 1))),b3) meets Upper_Arc (L~ (Cage b2,(b1 + 1)))
proof end;

theorem Th6: :: JORDAN19:6
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3 being FinSequence of (TOP-REAL 2)
for b4 being Nat st 1 <= b4 & b4 + 1 <= len b3 & b3 is_sequence_on Gauge b2,b1 & not dist (b3 /. b4),(b3 /. (b4 + 1)) = ((N-bound b2) - (S-bound b2)) / (2 |^ b1) holds
dist (b3 /. b4),(b3 /. (b4 + 1)) = ((E-bound b2) - (W-bound b2)) / (2 |^ b1)
proof end;

theorem Th7: :: JORDAN19:7
for b1 being symmetric triangle MetrStruct
for b2 being real number
for b3, b4, b5 being Element of b1 st b3 in Ball b5,b2 & b4 in Ball b5,b2 holds
dist b3,b4 < 2 * b2
proof end;

theorem Th8: :: JORDAN19:8
for b1 being Nat
for b2 being Subset of (TOP-REAL b1)
for b3 being Point of (TOP-REAL b1)
for b4 being Point of (Euclid b1) st b3 = b4 holds
for b5 being real number st b5 > 0 holds
( b3 in Cl b2 iff for b6 being real number st 0 < b6 & b6 < b5 holds
Ball b4,b6 meets b2 )
proof end;

theorem Th9: :: JORDAN19:9
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound b2 < N-bound (L~ (Cage b2,b1))
proof end;

theorem Th10: :: JORDAN19:10
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-bound b2 < E-bound (L~ (Cage b2,b1))
proof end;

theorem Th11: :: JORDAN19:11
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds S-bound (L~ (Cage b2,b1)) < S-bound b2
proof end;

theorem Th12: :: JORDAN19:12
for b1 being Nat
for b2 being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds W-bound (L~ (Cage b2,b1)) < W-bound b2
proof end;

theorem Th13: :: JORDAN19:13
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b5 & b5 <= b4 & b4 <= width (Gauge b2,b1) & (LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b4)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b3,b5)} & (LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b4)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b3,b4)} holds
LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b4) meets Upper_Arc b2
proof end;

theorem Th14: :: JORDAN19:14
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b5 & b5 <= b4 & b4 <= width (Gauge b2,b1) & (LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b4)) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b3,b5)} & (LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b4)) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b3,b4)} holds
LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b4) meets Lower_Arc b2
proof end;

theorem Th15: :: JORDAN19:15
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & b1 > 0 & (LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5)) /\ (Lower_Arc (L~ (Cage b2,b1))) = {((Gauge b2,b1) * b3,b5)} & (LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5)) /\ (Upper_Arc (L~ (Cage b2,b1))) = {((Gauge b2,b1) * b3,b4)} holds
LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5) meets Upper_Arc b2
proof end;

theorem Th16: :: JORDAN19:16
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & b1 > 0 & (LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5)) /\ (Lower_Arc (L~ (Cage b2,b1))) = {((Gauge b2,b1) * b3,b5)} & (LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5)) /\ (Upper_Arc (L~ (Cage b2,b1))) = {((Gauge b2,b1) * b3,b4)} holds
LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5) meets Lower_Arc b2
proof end;

theorem Th17: :: JORDAN19:17
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & (Gauge b2,b1) * b3,b5 in L~ (Lower_Seq b2,b1) & (Gauge b2,b1) * b3,b4 in L~ (Upper_Seq b2,b1) holds
LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5) meets Upper_Arc b2
proof end;

theorem Th18: :: JORDAN19:18
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & (Gauge b2,b1) * b3,b5 in L~ (Lower_Seq b2,b1) & (Gauge b2,b1) * b3,b4 in L~ (Upper_Seq b2,b1) holds
LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5) meets Lower_Arc b2
proof end;

theorem Th19: :: JORDAN19:19
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & b1 > 0 & (Gauge b2,b1) * b3,b5 in Lower_Arc (L~ (Cage b2,b1)) & (Gauge b2,b1) * b3,b4 in Upper_Arc (L~ (Cage b2,b1)) holds
LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5) meets Upper_Arc b2
proof end;

theorem Th20: :: JORDAN19:20
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5 being Nat st 1 < b3 & b3 < len (Gauge b2,b1) & 1 <= b4 & b4 <= b5 & b5 <= width (Gauge b2,b1) & b1 > 0 & (Gauge b2,b1) * b3,b5 in Lower_Arc (L~ (Cage b2,b1)) & (Gauge b2,b1) * b3,b4 in Upper_Arc (L~ (Cage b2,b1)) holds
LSeg ((Gauge b2,b1) * b3,b4),((Gauge b2,b1) * b3,b5) meets Lower_Arc b2
proof end;

theorem Th21: :: JORDAN19:21
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5, b6 being Nat st 1 < b3 & b3 <= b4 & b4 < len (Gauge b2,b1) & 1 <= b5 & b5 <= b6 & b6 <= width (Gauge b2,b1) & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b3,b5)} & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b4,b6)} holds
(LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6)) meets Upper_Arc b2
proof end;

theorem Th22: :: JORDAN19:22
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5, b6 being Nat st 1 < b3 & b3 <= b4 & b4 < len (Gauge b2,b1) & 1 <= b5 & b5 <= b6 & b6 <= width (Gauge b2,b1) & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b3,b5)} & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b4,b6)} holds
(LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6)) meets Lower_Arc b2
proof end;

theorem Th23: :: JORDAN19:23
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5, b6 being Nat st 1 < b4 & b4 <= b3 & b3 < len (Gauge b2,b1) & 1 <= b5 & b5 <= b6 & b6 <= width (Gauge b2,b1) & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b3,b5)} & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b4,b6)} holds
(LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6)) meets Upper_Arc b2
proof end;

theorem Th24: :: JORDAN19:24
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5, b6 being Nat st 1 < b4 & b4 <= b3 & b3 < len (Gauge b2,b1) & 1 <= b5 & b5 <= b6 & b6 <= width (Gauge b2,b1) & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Upper_Seq b2,b1)) = {((Gauge b2,b1) * b3,b5)} & ((LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6))) /\ (L~ (Lower_Seq b2,b1)) = {((Gauge b2,b1) * b4,b6)} holds
(LSeg ((Gauge b2,b1) * b3,b5),((Gauge b2,b1) * b3,b6)) \/ (LSeg ((Gauge b2,b1) * b3,b6),((Gauge b2,b1) * b4,b6)) meets Lower_Arc b2
proof end;

theorem Th25: :: JORDAN19:25
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5, b6 being Nat st 1 < b3 & b3 < len (Gauge b2,(b1 + 1)) & 1 < b4 & b4 < len (Gauge b2,(b1 + 1)) & 1 <= b5 & b5 <= b6 & b6 <= width (Gauge b2,(b1 + 1)) & (Gauge b2,(b1 + 1)) * b3,b6 in Lower_Arc (L~ (Cage b2,(b1 + 1))) & (Gauge b2,(b1 + 1)) * b4,b5 in Upper_Arc (L~ (Cage b2,(b1 + 1))) holds
(LSeg ((Gauge b2,(b1 + 1)) * b4,b5),((Gauge b2,(b1 + 1)) * b4,b6)) \/ (LSeg ((Gauge b2,(b1 + 1)) * b4,b6),((Gauge b2,(b1 + 1)) * b3,b6)) meets Lower_Arc b2
proof end;

theorem Th26: :: JORDAN19:26
for b1 being Nat
for b2 being Simple_closed_curve
for b3, b4, b5, b6 being Nat st 1 < b3 & b3 < len (Gauge b2,(b1 + 1)) & 1 < b4 & b4 < len (Gauge b2,(b1 + 1)) & 1 <= b5 & b5 <= b6 & b6 <= width (Gauge b2,(b1 + 1)) & (Gauge b2,(b1 + 1)) * b3,b6 in Lower_Arc (L~ (Cage b2,(b1 + 1))) & (Gauge b2,(b1 + 1)) * b4,b5 in Upper_Arc (L~ (Cage b2,(b1 + 1))) holds
(LSeg ((Gauge b2,(b1 + 1)) * b4,b5),((Gauge b2,(b1 + 1)) * b4,b6)) \/ (LSeg ((Gauge b2,(b1 + 1)) * b4,b6),((Gauge b2,(b1 + 1)) * b3,b6)) meets Upper_Arc b2
proof end;

theorem Th27: :: JORDAN19:27
for b1 being Simple_closed_curve
for b2 being Point of (TOP-REAL 2) st W-bound b1 < b2 `1 & b2 `1 < E-bound b1 & b2 in North_Arc b1 holds
not b2 in South_Arc b1
proof end;

theorem Th28: :: JORDAN19:28
for b1 being Simple_closed_curve
for b2 being Point of (TOP-REAL 2) st b2 `1 = ((W-bound b1) + (E-bound b1)) / 2 & b2 in North_Arc b1 holds
not b2 in South_Arc b1
proof end;