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:67;
A1:
for r being Real st r > 0 holds
ex k being Nat st
for m being Nat st m > k holds
(Upper_Appr C) . m meets Ball (w,r)
proof
let r be
Real;
( r > 0 implies ex k being Nat st
for m being Nat st m > k holds
(Upper_Appr C) . m meets Ball (w,r) )
assume
r > 0
;
ex k being Nat st
for m being Nat st m > k holds
(Upper_Appr C) . m meets Ball (w,r)
then
r / 2
> 0
;
then consider k being
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:11;
reconsider k =
k as
Nat ;
take
k
;
for m being Nat st m > k holds
(Upper_Appr C) . m meets Ball (w,r)
let m be
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:34, 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:31;
reconsider p =
W-min (L~ (Cage (C,m))) as
Point of
(Euclid 2) by EUCLID:67;
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:43;
then A11:
W-min (L~ (Cage (C,m))) = (Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))) /. 1
by FINSEQ_6:92;
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
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:21;
A16:
1
<= j
by A12, MATRIX_0:32;
i < len (Gauge (C,m))
by A7, A10, A12, A13, A14, A15, JORDAN1I:14;
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_0:32;
then A19:
[(i + 1),j] in Indices (Gauge (C,m))
by A16, A18, A17, MATRIX_0:30;
[(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:10;
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:10;
then A20:
(((Gauge (C,m)) * ((i + 1),j)) `1) - (((Gauge (C,m)) * (i,j)) `1) < r / 2
by A12, A19, A6, GOBRD14:5;
[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:9;
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:9;
then
(((Gauge (C,m)) * (i,(j + 1))) `2) - (((Gauge (C,m)) * (i,j)) `2) < r / 2
by A12, A13, A5, GOBRD14:6;
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:8;
A22:
1
<= i
by A12, MATRIX_0:32;
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:23
.=
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:44
;
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:22;
A24:
j + 1
<= width (Gauge (C,m))
by A13, MATRIX_0:32;
(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:21;
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:17;
A27:
W-min C in right_cell (
(Rotate ((Cage (C,m)),(W-min (L~ (Cage (C,m)))))),1)
by JORDAN1I:6;
then A28:
(W-min C) `1 <= ((Gauge (C,m)) * ((i + 1),j)) `1
by A23, A22, A16, A24, A17, JORDAN9:17;
A29:
((Gauge (C,m)) * (i,j)) `2 <= (W-min (L~ (Cage (C,m)))) `2
by A25, A23, A22, A16, A24, A17, JORDAN9:17;
A30:
(W-min (L~ (Cage (C,m)))) `1 <= ((Gauge (C,m)) * ((i + 1),j)) `1
by A25, A23, A22, A16, A24, A17, JORDAN9:17;
A31:
(W-min (L~ (Cage (C,m)))) `2 <= ((Gauge (C,m)) * (i,(j + 1))) `2
by A25, A23, A22, A16, A24, A17, JORDAN9:17;
A32:
(W-min C) `2 <= ((Gauge (C,m)) * (i,(j + 1))) `2
by A27, A23, A22, A16, A24, A17, JORDAN9:17;
A33:
((Gauge (C,m)) * (i,j)) `2 <= (W-min C) `2
by A27, A23, A22, A16, A24, A17, JORDAN9:17;
((Gauge (C,m)) * (i,j)) `1 <= (W-min C) `1
by A27, A23, A22, A16, A24, A17, JORDAN9:17;
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:95;
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:11;
(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:14; verum