let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); N-bound (L~ (Cage (C,n))) = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))
set a = N-bound C;
set s = S-bound C;
set w = W-bound C;
set f = Cage (C,n);
set G = Gauge (C,n);
consider i being Nat such that
A1:
1 <= i
and
A2:
i + 1 <= len (Gauge (C,n))
and
A3:
(Cage (C,n)) /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n))))
and
(Cage (C,n)) /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n))))
and
N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1))
and
N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1))
by JORDAN9:def 1;
A4:
len (Gauge (C,n)) = width (Gauge (C,n))
by JORDAN8:def 1;
4 <= len (Gauge (C,n))
by JORDAN8:10;
then A5:
1 <= len (Gauge (C,n))
by XXREAL_0:2;
i + 0 <= i + 1
by XREAL_1:6;
then
i <= len (Gauge (C,n))
by A2, XXREAL_0:2;
then A6:
[i,(len (Gauge (C,n)))] in Indices (Gauge (C,n))
by A1, A4, A5, MATRIX_0:30;
A7:
2 |^ n <> 0
by NEWTON:83;
thus N-bound (L~ (Cage (C,n))) =
(N-min (L~ (Cage (C,n)))) `2
by EUCLID:52
.=
((Cage (C,n)) /. 1) `2
by JORDAN9:32
.=
|[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2)))]| `2
by A3, A4, A6, JORDAN8:def 1
.=
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((len (Gauge (C,n))) - 2))
by EUCLID:52
.=
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((2 |^ n) + 3) - 2))
by JORDAN8:def 1
.=
((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (2 |^ n))) + (((N-bound C) - (S-bound C)) / (2 |^ n))
.=
((S-bound C) + ((N-bound C) - (S-bound C))) + (((N-bound C) - (S-bound C)) / (2 |^ n))
by A7, XCMPLX_1:87
.=
(N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))
; verum