let C be Simple_closed_curve; E-max C in North_Arc C
reconsider w = E-max 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;
reconsider p =
E-max (L~ (Cage C,m)) as
Point of
(Euclid 2) by EUCLID:71;
A7:
E-max (L~ (Cage C,m)) in Upper_Arc (L~ (Cage C,m))
by JORDAN7:1;
A8:
1
+ 1
<= len (Rotate (Cage C,m),(E-max (L~ (Cage C,m))))
by GOBOARD7:36, XXREAL_0:2;
then A9:
(left_cell (Rotate (Cage C,m),(E-max (L~ (Cage C,m)))),1) /\ (right_cell (Rotate (Cage C,m),(E-max (L~ (Cage C,m)))),1) = LSeg (Rotate (Cage C,m),(E-max (L~ (Cage C,m)))),1
by GOBOARD5:32;
Cage C,
m is_sequence_on Gauge C,
m
by JORDAN9:def 1;
then A10:
Rotate (Cage C,m),
(E-max (L~ (Cage C,m))) is_sequence_on Gauge C,
m
by REVROT_1:34;
E-max (L~ (Cage C,m)) in rng (Cage C,m)
by SPRECT_2:50;
then A11:
E-max (L~ (Cage C,m)) = (Rotate (Cage C,m),(E-max (L~ (Cage C,m)))) /. 1
by FINSEQ_6:98;
then
(Rotate (Cage C,m),(E-max (L~ (Cage C,m)))) /. 1
= E-max (L~ (Rotate (Cage C,m),(E-max (L~ (Cage C,m)))))
by REVROT_1:33;
then consider i,
j being
Element of
NAT such that A12:
[i,(j + 1)] in Indices (Gauge C,m)
and A13:
[i,j] in Indices (Gauge C,m)
and A14:
(Rotate (Cage C,m),(E-max (L~ (Cage C,m)))) /. 1
= (Gauge C,m) * i,
(j + 1)
and A15:
(Rotate (Cage C,m),(E-max (L~ (Cage C,m)))) /. (1 + 1) = (Gauge C,m) * i,
j
by A8, A10, JORDAN1I:25;
A16:
i <= len (Gauge C,m)
by A12, MATRIX_1:39;
i > 1
by A8, A10, A12, A13, A14, A15, JORDAN1I:18;
then A17:
i - 1
> 1
- 1
by XREAL_1:16;
then A18:
i -' 1
= i - 1
by XREAL_0:def 2;
then A19:
i -' 1
<= len (Gauge C,m)
by A16, XREAL_1:148, XXREAL_0:2;
i - 1 is
Element of
NAT
by A17, INT_1:16;
then A20:
i - 1
>= 0 + 1
by A17, NAT_1:13;
then A21:
(i -' 1) + 1
= i
by NAT_D:43;
right_cell (Rotate (Cage C,m),(E-max (L~ (Cage C,m)))),1 =
right_cell (Rotate (Cage C,m),(E-max (L~ (Cage C,m)))),1,
(GoB (Rotate (Cage C,m),(E-max (L~ (Cage C,m)))))
by A8, JORDAN1H:29
.=
right_cell (Rotate (Cage C,m),(E-max (L~ (Cage C,m)))),1,
(GoB (Cage C,m))
by REVROT_1:28
.=
right_cell (Rotate (Cage C,m),(E-max (L~ (Cage C,m)))),1,
(Gauge C,m)
by JORDAN1H:52
;
then A22:
right_cell (Rotate (Cage C,m),(E-max (L~ (Cage C,m)))),1
= cell (Gauge C,m),
(i -' 1),
j
by A8, A10, A12, A13, A14, A15, GOBRD13:29;
A23:
j + 1
<= width (Gauge C,m)
by A12, MATRIX_1:39;
1
<= j + 1
by NAT_1:11;
then A24:
[(i -' 1),(j + 1)] in Indices (Gauge C,m)
by A23, A20, A18, A19, MATRIX_1:37;
A25:
1
<= j
by A13, MATRIX_1:39;
j <= width (Gauge C,m)
by A13, MATRIX_1:39;
then A26:
[(i -' 1),j] in Indices (Gauge C,m)
by A25, A20, A18, A19, MATRIX_1:37;
[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 -' 1),j),
((Gauge C,m) * (i -' 1),(j + 1))
by A26, A24, GOBRD14:19;
then A27:
(((Gauge C,m) * (i -' 1),(j + 1)) `2 ) - (((Gauge C,m) * (i -' 1),j) `2 ) < r / 2
by A26, A24, A5, GOBRD14:16;
[(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 -' 1),j),
((Gauge C,m) * ((i -' 1) + 1),j)
by A13, A21, A26, GOBRD14:20;
then
(((Gauge C,m) * ((i -' 1) + 1),j) `1 ) - (((Gauge C,m) * (i -' 1),j) `1 ) < r / 2
by A13, A21, A26, A6, GOBRD14:15;
then A28:
((((Gauge C,m) * ((i -' 1) + 1),j) `1 ) - (((Gauge C,m) * (i -' 1),j) `1 )) + ((((Gauge C,m) * (i -' 1),(j + 1)) `2 ) - (((Gauge C,m) * (i -' 1),j) `2 )) < (r / 2) + (r / 2)
by A27, XREAL_1:10;
A29:
E-max C in right_cell (Rotate (Cage C,m),(E-max (L~ (Cage C,m)))),1
by JORDAN1I:9;
then A30:
(E-max C) `1 <= ((Gauge C,m) * ((i -' 1) + 1),j) `1
by A22, A25, A23, A20, A21, A16, JORDAN9:19;
(Rotate (Cage C,m),(E-max (L~ (Cage C,m)))) /. 1
in LSeg (Rotate (Cage C,m),(E-max (L~ (Cage C,m)))),1
by A8, TOPREAL1:27;
then A31:
E-max (L~ (Cage C,m)) in right_cell (Rotate (Cage C,m),(E-max (L~ (Cage C,m)))),1
by A11, A9, XBOOLE_0:def 4;
then A32:
((Gauge C,m) * (i -' 1),j) `1 <= (E-max (L~ (Cage C,m))) `1
by A22, A25, A23, A20, A21, A16, JORDAN9:19;
A33:
((Gauge C,m) * (i -' 1),j) `2 <= (E-max (L~ (Cage C,m))) `2
by A31, A22, A25, A23, A20, A21, A16, JORDAN9:19;
A34:
(E-max (L~ (Cage C,m))) `1 <= ((Gauge C,m) * ((i -' 1) + 1),j) `1
by A31, A22, A25, A23, A20, A21, A16, JORDAN9:19;
A35:
(E-max (L~ (Cage C,m))) `2 <= ((Gauge C,m) * (i -' 1),(j + 1)) `2
by A31, A22, A25, A23, A20, A21, A16, JORDAN9:19;
A36:
(E-max C) `2 <= ((Gauge C,m) * (i -' 1),(j + 1)) `2
by A29, A22, A25, A23, A20, A21, A16, JORDAN9:19;
A37:
((Gauge C,m) * (i -' 1),j) `2 <= (E-max C) `2
by A29, A22, A25, A23, A20, A21, A16, JORDAN9:19;
((Gauge C,m) * (i -' 1),j) `1 <= (E-max C) `1
by A29, A22, A25, A23, A20, A21, A16, JORDAN9:19;
then
dist (E-max C),
(E-max (L~ (Cage C,m))) <= ((((Gauge C,m) * ((i -' 1) + 1),j) `1 ) - (((Gauge C,m) * (i -' 1),j) `1 )) + ((((Gauge C,m) * (i -' 1),(j + 1)) `2 ) - (((Gauge C,m) * (i -' 1),j) `2 ))
by A30, A37, A36, A32, A34, A33, A35, TOPREAL6:104;
then
dist (E-max C),
(E-max (L~ (Cage C,m))) < r
by A28, XXREAL_0:2;
then
dist w,
p < r
by TOPREAL6:def 1;
then A38:
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 A7, A38, XBOOLE_0:3;
verum
end;
North_Arc C = Lim_inf (Upper_Appr C)
by JORDAN19:def 3;
hence
E-max C in North_Arc C
by A1, KURATO_2:48; verum