let C be Simple_closed_curve; W-min C in North_Arc C
reconsider w = W-min C as Point of (Euclid 2) by EUCLID:71;
A1:
for r being real number st r > 0 holds
ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball w,r
proof
let r be
real number ;
( r > 0 implies ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball w,r )
assume
r > 0
;
ex k being Element of NAT st
for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball w,r
then
r / 2
> 0
by XREAL_1:217;
then consider k being
Element of
NAT such that
1
< k
and A2:
dist ((Gauge C,k) * 1,1),
((Gauge C,k) * 1,2) < r / 2
and A3:
dist ((Gauge C,k) * 1,1),
((Gauge C,k) * 2,1) < r / 2
by GOBRD14:21;
take
k
;
for m being Element of NAT st m > k holds
(Upper_Appr C) . m meets Ball w,r
let m be
Element of
NAT ;
( m > k implies (Upper_Appr C) . m meets Ball w,r )
assume A4:
m > k
;
(Upper_Appr C) . m meets Ball w,r
dist ((Gauge C,m) * 1,1),
((Gauge C,m) * 1,2) < dist ((Gauge C,k) * 1,1),
((Gauge C,k) * 1,2)
by A4, Th9;
then A5:
dist ((Gauge C,m) * 1,1),
((Gauge C,m) * 1,2) < r / 2
by A2, XXREAL_0:2;
dist ((Gauge C,m) * 1,1),
((Gauge C,m) * 2,1) < dist ((Gauge C,k) * 1,1),
((Gauge C,k) * 2,1)
by A4, Th11;
then A6:
dist ((Gauge C,m) * 1,1),
((Gauge C,m) * 2,1) < r / 2
by A3, XXREAL_0:2;
A7:
1
+ 1
<= len (Rotate (Cage C,m),(W-min (L~ (Cage C,m))))
by GOBOARD7:36, XXREAL_0:2;
then A8:
(left_cell (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))),1) /\ (right_cell (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))),1) = LSeg (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))),1
by GOBOARD5:32;
reconsider p =
W-min (L~ (Cage C,m)) as
Point of
(Euclid 2) by EUCLID:71;
A9:
W-min (L~ (Cage C,m)) in Upper_Arc (L~ (Cage C,m))
by JORDAN7:1;
Cage C,
m is_sequence_on Gauge C,
m
by JORDAN9:def 1;
then A10:
Rotate (Cage C,m),
(W-min (L~ (Cage C,m))) is_sequence_on Gauge C,
m
by REVROT_1:34;
W-min (L~ (Cage C,m)) in rng (Cage C,m)
by SPRECT_2:47;
then A11:
W-min (L~ (Cage C,m)) = (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))) /. 1
by FINSEQ_6:98;
then
(Rotate (Cage C,m),(W-min (L~ (Cage C,m)))) /. 1
= W-min (L~ (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))))
by REVROT_1:33;
then consider i,
j being
Element of
NAT such that A12:
[i,j] in Indices (Gauge C,m)
and A13:
[i,(j + 1)] in Indices (Gauge C,m)
and A14:
(Rotate (Cage C,m),(W-min (L~ (Cage C,m)))) /. 1
= (Gauge C,m) * i,
j
and A15:
(Rotate (Cage C,m),(W-min (L~ (Cage C,m)))) /. (1 + 1) = (Gauge C,m) * i,
(j + 1)
by A7, A10, JORDAN1I:23;
A16:
1
<= j
by A12, MATRIX_1:39;
i < len (Gauge C,m)
by A7, A10, A12, A13, A14, A15, JORDAN1I:16;
then A17:
i + 1
<= len (Gauge C,m)
by NAT_1:13;
A18:
1
<= i + 1
by NAT_1:11;
j <= width (Gauge C,m)
by A12, MATRIX_1:39;
then A19:
[(i + 1),j] in Indices (Gauge C,m)
by A16, A18, A17, MATRIX_1:37;
[(1 + 1),1] in Indices (Gauge C,m)
by Th7;
then
dist ((Gauge C,m) * 1,1),
((Gauge C,m) * (1 + 1),1) = ((E-bound C) - (W-bound C)) / (2 |^ m)
by Th5, GOBRD14:20;
then
dist ((Gauge C,m) * 1,1),
((Gauge C,m) * (1 + 1),1) = dist ((Gauge C,m) * i,j),
((Gauge C,m) * (i + 1),j)
by A12, A19, GOBRD14:20;
then A20:
(((Gauge C,m) * (i + 1),j) `1 ) - (((Gauge C,m) * i,j) `1 ) < r / 2
by A12, A19, A6, GOBRD14:15;
[1,(1 + 1)] in Indices (Gauge C,m)
by Th6;
then
dist ((Gauge C,m) * 1,1),
((Gauge C,m) * 1,(1 + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ m)
by Th5, GOBRD14:19;
then
dist ((Gauge C,m) * 1,1),
((Gauge C,m) * 1,(1 + 1)) = dist ((Gauge C,m) * i,j),
((Gauge C,m) * i,(j + 1))
by A12, A13, GOBRD14:19;
then
(((Gauge C,m) * i,(j + 1)) `2 ) - (((Gauge C,m) * i,j) `2 ) < r / 2
by A12, A13, A5, GOBRD14:16;
then A21:
((((Gauge C,m) * (i + 1),j) `1 ) - (((Gauge C,m) * i,j) `1 )) + ((((Gauge C,m) * i,(j + 1)) `2 ) - (((Gauge C,m) * i,j) `2 )) < (r / 2) + (r / 2)
by A20, XREAL_1:10;
A22:
1
<= i
by A12, MATRIX_1:39;
right_cell (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))),1 =
right_cell (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))),1,
(GoB (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))))
by A7, JORDAN1H:29
.=
right_cell (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))),1,
(GoB (Cage C,m))
by REVROT_1:28
.=
right_cell (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))),1,
(Gauge C,m)
by JORDAN1H:52
;
then A23:
right_cell (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))),1
= cell (Gauge C,m),
i,
j
by A7, A10, A12, A13, A14, A15, GOBRD13:23;
A24:
j + 1
<= width (Gauge C,m)
by A13, MATRIX_1:39;
(Rotate (Cage C,m),(W-min (L~ (Cage C,m)))) /. 1
in LSeg (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))),1
by A7, TOPREAL1:27;
then A25:
W-min (L~ (Cage C,m)) in right_cell (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))),1
by A11, A8, XBOOLE_0:def 4;
then A26:
((Gauge C,m) * i,j) `1 <= (W-min (L~ (Cage C,m))) `1
by A23, A22, A16, A24, A17, JORDAN9:19;
A27:
W-min C in right_cell (Rotate (Cage C,m),(W-min (L~ (Cage C,m)))),1
by JORDAN1I:8;
then A28:
(W-min C) `1 <= ((Gauge C,m) * (i + 1),j) `1
by A23, A22, A16, A24, A17, JORDAN9:19;
A29:
((Gauge C,m) * i,j) `2 <= (W-min (L~ (Cage C,m))) `2
by A25, A23, A22, A16, A24, A17, JORDAN9:19;
A30:
(W-min (L~ (Cage C,m))) `1 <= ((Gauge C,m) * (i + 1),j) `1
by A25, A23, A22, A16, A24, A17, JORDAN9:19;
A31:
(W-min (L~ (Cage C,m))) `2 <= ((Gauge C,m) * i,(j + 1)) `2
by A25, A23, A22, A16, A24, A17, JORDAN9:19;
A32:
(W-min C) `2 <= ((Gauge C,m) * i,(j + 1)) `2
by A27, A23, A22, A16, A24, A17, JORDAN9:19;
A33:
((Gauge C,m) * i,j) `2 <= (W-min C) `2
by A27, A23, A22, A16, A24, A17, JORDAN9:19;
((Gauge C,m) * i,j) `1 <= (W-min C) `1
by A27, A23, A22, A16, A24, A17, JORDAN9:19;
then
dist (W-min C),
(W-min (L~ (Cage C,m))) <= ((((Gauge C,m) * (i + 1),j) `1 ) - (((Gauge C,m) * i,j) `1 )) + ((((Gauge C,m) * i,(j + 1)) `2 ) - (((Gauge C,m) * i,j) `2 ))
by A28, A33, A32, A26, A30, A29, A31, TOPREAL6:104;
then
dist (W-min C),
(W-min (L~ (Cage C,m))) < r
by A21, XXREAL_0:2;
then
dist w,
p < r
by TOPREAL6:def 1;
then A34:
p in Ball w,
r
by METRIC_1:12;
(Upper_Appr C) . m = Upper_Arc (L~ (Cage C,m))
by JORDAN19:def 1;
hence
(Upper_Appr C) . m meets Ball w,
r
by A9, A34, XBOOLE_0:3;
verum
end;
North_Arc C = Lim_inf (Upper_Appr C)
by JORDAN19:def 3;
hence
W-min C in North_Arc C
by A1, KURATO_2:48; verum