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: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;
reconsider p =
E-max (L~ (Cage (C,m))) as
Point of
(Euclid 2) by EUCLID:67;
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:34, 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:31;
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:46;
then A11:
E-max (L~ (Cage (C,m))) = (Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))) /. 1
by FINSEQ_6:92;
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
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:23;
A16:
i <= len (Gauge (C,m))
by A12, MATRIX_0:32;
i > 1
by A8, A10, A12, A13, A14, A15, JORDAN1I:16;
then A17:
i - 1
> 1
- 1
by XREAL_1:14;
then A18:
i -' 1
= i - 1
by XREAL_0:def 2;
then A19:
i -' 1
<= len (Gauge (C,m))
by A16, XREAL_1:146, XXREAL_0:2;
i - 1
in NAT
by A17, INT_1:3;
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:23
.=
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:44
;
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:28;
A23:
j + 1
<= width (Gauge (C,m))
by A12, MATRIX_0:32;
1
<= j + 1
by NAT_1:11;
then A24:
[(i -' 1),(j + 1)] in Indices (Gauge (C,m))
by A23, A20, A18, A19, MATRIX_0:30;
A25:
1
<= j
by A13, MATRIX_0:32;
j <= width (Gauge (C,m))
by A13, MATRIX_0:32;
then A26:
[(i -' 1),j] in Indices (Gauge (C,m))
by A25, A20, A18, A19, MATRIX_0:30;
[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 -' 1),j)),
((Gauge (C,m)) * ((i -' 1),(j + 1))))
by A26, A24, GOBRD14:9;
then A27:
(((Gauge (C,m)) * ((i -' 1),(j + 1))) `2) - (((Gauge (C,m)) * ((i -' 1),j)) `2) < r / 2
by A26, A24, A5, GOBRD14:6;
[(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 -' 1),j)),
((Gauge (C,m)) * (((i -' 1) + 1),j)))
by A13, A21, A26, GOBRD14:10;
then
(((Gauge (C,m)) * (((i -' 1) + 1),j)) `1) - (((Gauge (C,m)) * ((i -' 1),j)) `1) < r / 2
by A13, A21, A26, A6, GOBRD14:5;
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:8;
A29:
E-max C in right_cell (
(Rotate ((Cage (C,m)),(E-max (L~ (Cage (C,m)))))),1)
by JORDAN1I:7;
then A30:
(E-max C) `1 <= ((Gauge (C,m)) * (((i -' 1) + 1),j)) `1
by A22, A25, A23, A20, A21, A16, JORDAN9:17;
(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:21;
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:17;
A33:
((Gauge (C,m)) * ((i -' 1),j)) `2 <= (E-max (L~ (Cage (C,m)))) `2
by A31, A22, A25, A23, A20, A21, A16, JORDAN9:17;
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:17;
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:17;
A36:
(E-max C) `2 <= ((Gauge (C,m)) * ((i -' 1),(j + 1))) `2
by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17;
A37:
((Gauge (C,m)) * ((i -' 1),j)) `2 <= (E-max C) `2
by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17;
((Gauge (C,m)) * ((i -' 1),j)) `1 <= (E-max C) `1
by A29, A22, A25, A23, A20, A21, A16, JORDAN9:17;
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:95;
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: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 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:14; verum