environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD1, RLTOPSP1, RELAT_1, XBOOLE_0, TOPREAL1, MATRIX_1, XXREAL_0, MCART_1, RCOMP_1, PSCOMP_1, PRE_TOPC, TREES_1, TARSKI, ARYTM_3, PARTFUN1, COMPLEX1, ARYTM_1, CARD_1, SPPOL_1, JORDAN1E, JORDAN9, FINSEQ_6, FINSEQ_5, FINSEQ_4, JORDAN6, TOPREAL2, RELAT_2, JORDAN8, ORDINAL4, FUNCT_1, NAT_1, RFINSEQ, JORDAN1A, SEQ_4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, FINSEQ_6, MATRIX_0, SEQ_4, STRUCT_0, PRE_TOPC, COMPTS_1, CONNSP_1, RFINSEQ, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD1, SPPOL_1, PSCOMP_1, JORDAN6, JORDAN8, JORDAN9, JORDAN1A, JORDAN1E;
definitions TARSKI;
theorems JORDAN8, NAT_1, GOBOARD7, GOBOARD5, SPRECT_3, ABSVALUE, GOBOARD1, JORDAN6, PSCOMP_1, TARSKI, TOPREAL3, SPRECT_2, FINSEQ_6, RELAT_1, FINSEQ_5, TOPREAL1, PRE_TOPC, JORDAN5B, FINSEQ_1, JORDAN1E, JORDAN1A, REVROT_1, JORDAN9, JORDAN1B, FINSEQ_3, UNIFORM1, FINSEQ_4, JORDAN1D, SPRECT_5, RFINSEQ, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, EUCLID, PARTFUN1, MATRIX_0, XREAL_0;
schemes ;
registrations XBOOLE_0, RELSET_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_6, STRUCT_0, SPPOL_2, SPRECT_1, SPRECT_2, TOPREAL6, JORDAN8, JORDAN1A, JORDAN1E, FUNCT_1, EUCLID, PSCOMP_1, ORDINAL1;
constructors HIDDEN, REAL_1, FINSEQ_4, NEWTON, RFINSEQ, FINSEQ_5, CONNSP_1, JORDAN5C, JORDAN6, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D, SEQ_4, RELSET_1, PSCOMP_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities STRUCT_0, PSCOMP_1;
expansions ;
theorem Th1:
for
i,
j,
k being
Nat for
f being
FinSequence of the
carrier of
(TOP-REAL 2) for
G being
Go-board st
f is_sequence_on G &
LSeg (
(G * (i,j)),
(G * (i,k)))
meets L~ f &
[i,j] in Indices G &
[i,k] in Indices G &
j <= k holds
ex
n being
Nat st
(
j <= n &
n <= k &
(G * (i,n)) `2 = lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) )
theorem
for
i,
j,
k being
Nat for
f being
FinSequence of the
carrier of
(TOP-REAL 2) for
G being
Go-board st
f is_sequence_on G &
LSeg (
(G * (i,j)),
(G * (i,k)))
meets L~ f &
[i,j] in Indices G &
[i,k] in Indices G &
j <= k holds
ex
n being
Nat st
(
j <= n &
n <= k &
(G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) )
theorem
for
i,
j,
k being
Nat for
f being
FinSequence of the
carrier of
(TOP-REAL 2) for
G being
Go-board st
f is_sequence_on G &
LSeg (
(G * (j,i)),
(G * (k,i)))
meets L~ f &
[j,i] in Indices G &
[k,i] in Indices G &
j <= k holds
ex
n being
Nat st
(
j <= n &
n <= k &
(G * (n,i)) `1 = lower_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )
theorem
for
i,
j,
k being
Nat for
f being
FinSequence of the
carrier of
(TOP-REAL 2) for
G being
Go-board st
f is_sequence_on G &
LSeg (
(G * (j,i)),
(G * (k,i)))
meets L~ f &
[j,i] in Indices G &
[k,i] in Indices G &
j <= k holds
ex
n being
Nat st
(
j <= n &
n <= k &
(G * (n,i)) `1 = upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )
theorem Th11:
for
G being
Go-board for
p being
Point of
(TOP-REAL 2) for
f being
FinSequence of
(TOP-REAL 2) st
f is_sequence_on G & ex
i,
j being
Nat st
(
[i,j] in Indices G &
p = G * (
i,
j) ) & ( for
i1,
j1,
i2,
j2 being
Nat st
[i1,j1] in Indices G &
[i2,j2] in Indices G &
p = G * (
i1,
j1) &
f /. 1
= G * (
i2,
j2) holds
|.(i2 - i1).| + |.(j2 - j1).| = 1 ) holds
<*p*> ^ f is_sequence_on G
theorem
for
i being
Nat for
C being non
empty being_simple_closed_curve compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
p being
Point of
(TOP-REAL 2) st
p `1 = ((W-bound C) + (E-bound C)) / 2 &
p `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) holds
ex
j being
Nat st
( 1
<= j &
j <= width (Gauge (C,(i + 1))) &
p = (Gauge (C,(i + 1))) * (
(Center (Gauge (C,(i + 1)))),
j) )