environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, TOPREAL2, PROB_1, STRUCT_0, EUCLID, FUNCT_1, JORDAN6, TOPREAL1, JORDAN9, KURATO_2, GOBOARD1, XXREAL_0, TREES_1, CARD_1, ARYTM_3, FINSEQ_1, INT_1, JORDAN1A, MATRIX_1, XBOOLE_0, PSCOMP_1, JORDAN8, RELAT_1, MCART_1, ARYTM_1, NEWTON, RCOMP_1, SPPOL_1, RLTOPSP1, TARSKI, RELAT_2, JORDAN1E, JORDAN3, ORDINAL4, PARTFUN1, FINSEQ_5, PRE_TOPC, GROUP_2, SPPOL_2, SPRECT_2, METRIC_1, GOBOARD5, FINSEQ_4, GRAPH_2, FINSEQ_6, ZFMISC_1, GOBOARD9, GOBOARD2, NAT_1, CONNSP_1, JORDAN2C, SEQ_4, REAL_1, CONNSP_2, POWER, COMPLEX1, JORDAN19, XXREAL_2;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, INT_1, NAT_1, NAT_D, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, MATRIX_0, FINSEQ_6, POWER, METRIC_1, CONNSP_2, GRAPH_2, SEQ_4, STRUCT_0, PRE_TOPC, TOPREAL2, NEWTON, PROB_1, CONNSP_1, COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, PSCOMP_1, SPRECT_2, SPPOL_2, KURATO_2, GOBOARD1, TOPREAL6, TOPREAL1, GOBOARD2, GOBOARD5, GOBOARD9, GOBRD13, SPPOL_1, JORDAN3, JORDAN6, JORDAN8, JORDAN9, JORDAN2C, JORDAN1A, JORDAN1E;
definitions TARSKI, XBOOLE_0, FUNCT_2;
theorems NAT_1, FINSEQ_1, GOBOARD1, FINSEQ_4, EUCLID, FINSEQ_3, SPPOL_2, TARSKI, JORDAN3, PSCOMP_1, FINSEQ_5, FINSEQ_6, GOBOARD7, TOPREAL1, JORDAN5B, GOBOARD5, SPRECT_2, SPPOL_1, ABSVALUE, GOBOARD9, FINSEQ_2, SUBSET_1, GOBRD11, JORDAN4, GOBOARD2, SPRECT_3, TOPREAL3, JORDAN8, PARTFUN2, SPRECT_1, XBOOLE_0, XBOOLE_1, ZFMISC_1, GOBRD14, JORDAN2C, TOPREAL5, PRE_TOPC, JORDAN6, JORDAN9, JORDAN1H, JORDAN1A, JORDAN1E, JORDAN10, JGRAPH_1, REVROT_1, COMPTS_1, ENUMSET1, JORDAN1B, JORDAN1F, JORDAN1G, JORDAN1I, JORDAN1J, GOBOARD3, TOPREAL8, GRAPH_2, SPRECT_5, JORDAN1D, METRIC_1, POWER, PRE_FF, JORDAN15, PCOMPS_1, TOPRNS_1, BOOLMARK, JORDAN5D, XCMPLX_1, XREAL_0, KURATO_2, INT_1, XREAL_1, NEWTON, XXREAL_0, GOBOARD6, PREPOWER, TOPREAL6, PARTFUN1, MATRIX_0, NAT_D, RLTOPSP1, ORDINAL1;
schemes FUNCT_2;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, FINSEQ_5, FINSEQ_6, STRUCT_0, COMPTS_1, METRIC_1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD2, JORDAN1, SPPOL_2, PSCOMP_1, GOBRD11, TOPREAL5, SPRECT_1, SPRECT_2, JORDAN6, REVROT_1, TOPREAL6, JORDAN8, JORDAN1E, JORDAN1J, CARD_1, FUNCT_1, RLTOPSP1, JORDAN2C, VALUED_0, NEWTON;
constructors HIDDEN, REAL_1, NAT_D, FINSEQ_4, NEWTON, POWER, CONNSP_1, REALSET2, CONNSP_2, MATRIX_1, GOBOARD2, PSCOMP_1, GRAPH_2, GOBOARD9, JORDAN3, JORDAN5C, JORDAN6, JORDAN2C, TOPREAL6, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, KURATO_2, SEQ_4, RELSET_1, CONVEX1;
requirements HIDDEN, NUMERALS, ARITHM, BOOLE, SUBSET, REAL;
equalities PSCOMP_1, EUCLID, XCMPLX_0;
expansions TARSKI, XBOOLE_0;
Lm2:
now for D being non empty Subset of (TOP-REAL 2)
for n, i being Nat st [i,(width (Gauge (D,n)))] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2))
let D be non
empty Subset of
(TOP-REAL 2);
for n, i being Nat st [i,(width (Gauge (D,n)))] in Indices (Gauge (D,n)) holds
((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2))let n,
i be
Nat;
( [i,(width (Gauge (D,n)))] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2)) )set a =
N-bound D;
set s =
S-bound D;
set w =
W-bound D;
set e =
E-bound D;
set G =
Gauge (
D,
n);
assume
[i,(width (Gauge (D,n)))] in Indices (Gauge (D,n))
;
((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 = (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2))hence ((Gauge (D,n)) * (i,(width (Gauge (D,n))))) `2 =
|[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2)))]| `2
by JORDAN8:def 1
.=
(S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((width (Gauge (D,n))) - 2))
by EUCLID:52
;
verum
end;
theorem Th1:
for
n,
m being
Nat st
n <= m &
n <> 0 holds
(n + 1) / n >= (m + 1) / m
theorem Th2:
for
n being
Nat for
E being
compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
m,
j being
Nat st 1
<= m &
m <= n & 1
<= j &
j <= width (Gauge (E,n)) holds
LSeg (
((Gauge (E,n)) * ((Center (Gauge (E,n))),(width (Gauge (E,n))))),
((Gauge (E,n)) * ((Center (Gauge (E,n))),j)))
c= LSeg (
((Gauge (E,m)) * ((Center (Gauge (E,m))),(width (Gauge (E,m))))),
((Gauge (E,n)) * ((Center (Gauge (E,n))),j)))
theorem Th3:
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
i,
j being
Nat st 1
<= i &
i <= len (Gauge (C,n)) & 1
<= j &
j <= width (Gauge (C,n)) &
(Gauge (C,n)) * (
i,
j)
in L~ (Cage (C,n)) holds
LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
((Gauge (C,n)) * (i,j)))
meets L~ (Upper_Seq (C,n))
theorem Th4:
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat st
n > 0 holds
for
i,
j being
Nat st 1
<= i &
i <= len (Gauge (C,n)) & 1
<= j &
j <= width (Gauge (C,n)) &
(Gauge (C,n)) * (
i,
j)
in L~ (Cage (C,n)) holds
LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
((Gauge (C,n)) * (i,j)))
meets Upper_Arc (L~ (Cage (C,n)))
theorem
for
n being
Nat for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
j being
Nat st
(Gauge (C,(n + 1))) * (
(Center (Gauge (C,(n + 1)))),
j)
in Lower_Arc (L~ (Cage (C,(n + 1)))) & 1
<= j &
j <= width (Gauge (C,(n + 1))) holds
LSeg (
((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))),
((Gauge (C,(n + 1))) * ((Center (Gauge (C,(n + 1)))),j)))
meets Upper_Arc (L~ (Cage (C,(n + 1))))
theorem Th12:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
Nat st 1
< i &
i < len (Gauge (C,n)) & 1
<= k &
k <= j &
j <= width (Gauge (C,n)) &
(LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} &
(LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds
LSeg (
((Gauge (C,n)) * (i,k)),
((Gauge (C,n)) * (i,j)))
meets Upper_Arc C
theorem Th13:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
Nat st 1
< i &
i < len (Gauge (C,n)) & 1
<= k &
k <= j &
j <= width (Gauge (C,n)) &
(LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i,k))} &
(LSeg (((Gauge (C,n)) * (i,k)),((Gauge (C,n)) * (i,j)))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i,j))} holds
LSeg (
((Gauge (C,n)) * (i,k)),
((Gauge (C,n)) * (i,j)))
meets Lower_Arc C
theorem
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
Nat st 1
< i &
i < len (Gauge (C,n)) & 1
<= j &
j <= k &
k <= width (Gauge (C,n)) &
n > 0 &
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} &
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds
LSeg (
((Gauge (C,n)) * (i,j)),
((Gauge (C,n)) * (i,k)))
meets Upper_Arc C
theorem
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
Nat st 1
< i &
i < len (Gauge (C,n)) & 1
<= j &
j <= k &
k <= width (Gauge (C,n)) &
n > 0 &
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Lower_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,k))} &
(LSeg (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,k)))) /\ (Upper_Arc (L~ (Cage (C,n)))) = {((Gauge (C,n)) * (i,j))} holds
LSeg (
((Gauge (C,n)) * (i,j)),
((Gauge (C,n)) * (i,k)))
meets Lower_Arc C
theorem Th16:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
Nat st 1
< i &
i < len (Gauge (C,n)) & 1
<= j &
j <= k &
k <= width (Gauge (C,n)) &
(Gauge (C,n)) * (
i,
k)
in L~ (Lower_Seq (C,n)) &
(Gauge (C,n)) * (
i,
j)
in L~ (Upper_Seq (C,n)) holds
LSeg (
((Gauge (C,n)) * (i,j)),
((Gauge (C,n)) * (i,k)))
meets Upper_Arc C
theorem Th17:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
Nat st 1
< i &
i < len (Gauge (C,n)) & 1
<= j &
j <= k &
k <= width (Gauge (C,n)) &
(Gauge (C,n)) * (
i,
k)
in L~ (Lower_Seq (C,n)) &
(Gauge (C,n)) * (
i,
j)
in L~ (Upper_Seq (C,n)) holds
LSeg (
((Gauge (C,n)) * (i,j)),
((Gauge (C,n)) * (i,k)))
meets Lower_Arc C
theorem Th18:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
Nat st 1
< i &
i < len (Gauge (C,n)) & 1
<= j &
j <= k &
k <= width (Gauge (C,n)) &
n > 0 &
(Gauge (C,n)) * (
i,
k)
in Lower_Arc (L~ (Cage (C,n))) &
(Gauge (C,n)) * (
i,
j)
in Upper_Arc (L~ (Cage (C,n))) holds
LSeg (
((Gauge (C,n)) * (i,j)),
((Gauge (C,n)) * (i,k)))
meets Upper_Arc C
theorem Th19:
for
n being
Nat for
C being
Simple_closed_curve for
i,
j,
k being
Nat st 1
< i &
i < len (Gauge (C,n)) & 1
<= j &
j <= k &
k <= width (Gauge (C,n)) &
n > 0 &
(Gauge (C,n)) * (
i,
k)
in Lower_Arc (L~ (Cage (C,n))) &
(Gauge (C,n)) * (
i,
j)
in Upper_Arc (L~ (Cage (C,n))) holds
LSeg (
((Gauge (C,n)) * (i,j)),
((Gauge (C,n)) * (i,k)))
meets Lower_Arc C
theorem Th20:
for
n being
Nat for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Nat st 1
< i1 &
i1 <= i2 &
i2 < len (Gauge (C,n)) & 1
<= j &
j <= k &
k <= width (Gauge (C,n)) &
((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} &
((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds
(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Upper_Arc C
theorem Th21:
for
n being
Nat for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Nat st 1
< i1 &
i1 <= i2 &
i2 < len (Gauge (C,n)) & 1
<= j &
j <= k &
k <= width (Gauge (C,n)) &
((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} &
((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds
(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Lower_Arc C
theorem Th22:
for
n being
Nat for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Nat st 1
< i2 &
i2 <= i1 &
i1 < len (Gauge (C,n)) & 1
<= j &
j <= k &
k <= width (Gauge (C,n)) &
((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} &
((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds
(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Upper_Arc C
theorem Th23:
for
n being
Nat for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Nat st 1
< i2 &
i2 <= i1 &
i1 < len (Gauge (C,n)) & 1
<= j &
j <= k &
k <= width (Gauge (C,n)) &
((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Upper_Seq (C,n))) = {((Gauge (C,n)) * (i1,j))} &
((LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k))))) /\ (L~ (Lower_Seq (C,n))) = {((Gauge (C,n)) * (i2,k))} holds
(LSeg (((Gauge (C,n)) * (i1,j)),((Gauge (C,n)) * (i1,k)))) \/ (LSeg (((Gauge (C,n)) * (i1,k)),((Gauge (C,n)) * (i2,k)))) meets Lower_Arc C
theorem Th24:
for
n being
Nat for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Nat st 1
< i1 &
i1 < len (Gauge (C,(n + 1))) & 1
< i2 &
i2 < len (Gauge (C,(n + 1))) & 1
<= j &
j <= k &
k <= width (Gauge (C,(n + 1))) &
(Gauge (C,(n + 1))) * (
i1,
k)
in Lower_Arc (L~ (Cage (C,(n + 1)))) &
(Gauge (C,(n + 1))) * (
i2,
j)
in Upper_Arc (L~ (Cage (C,(n + 1)))) holds
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Lower_Arc C
theorem Th25:
for
n being
Nat for
C being
Simple_closed_curve for
i1,
i2,
j,
k being
Nat st 1
< i1 &
i1 < len (Gauge (C,(n + 1))) & 1
< i2 &
i2 < len (Gauge (C,(n + 1))) & 1
<= j &
j <= k &
k <= width (Gauge (C,(n + 1))) &
(Gauge (C,(n + 1))) * (
i1,
k)
in Lower_Arc (L~ (Cage (C,(n + 1)))) &
(Gauge (C,(n + 1))) * (
i2,
j)
in Upper_Arc (L~ (Cage (C,(n + 1)))) holds
(LSeg (((Gauge (C,(n + 1))) * (i2,j)),((Gauge (C,(n + 1))) * (i2,k)))) \/ (LSeg (((Gauge (C,(n + 1))) * (i2,k)),((Gauge (C,(n + 1))) * (i1,k)))) meets Upper_Arc C