environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, ZFMISC_1, FINSEQ_1, XBOOLE_0, RELAT_1, FINSEQ_5, MATRIX_1, GOBOARD1, FINSEQ_4, ARYTM_3, RFINSEQ, RCOMP_1, RELAT_2, SPPOL_1, EUCLID, JORDAN1E, JORDAN8, JORDAN9, FINSEQ_6, PSCOMP_1, TOPREAL1, GOBOARD5, MCART_1, XXREAL_0, TREES_1, PARTFUN1, FUNCT_1, ARYTM_1, RLTOPSP1, TARSKI, CARD_1, PRE_TOPC, ORDINAL4, NEWTON, NAT_1, JORDAN1A, SPPOL_2, JORDAN3, SPRECT_2, GROUP_2, JORDAN5C, JORDAN6, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_0, MATRIX_1, FINSEQ_6, STRUCT_0, PRE_TOPC, NEWTON, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD5, SPPOL_1, SPPOL_2, JORDAN3, JORDAN8, JORDAN5C, JORDAN6, JORDAN9, JORDAN1A, JORDAN1E, NAT_1;
definitions TARSKI, XBOOLE_0;
theorems EUCLID, JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, GOBOARD5, FINSEQ_1, FINSEQ_2, JORDAN4, JORDAN6, SPRECT_2, FINSEQ_4, FINSEQ_5, FINSEQ_6, GOBOARD7, SPPOL_1, SPPOL_2, REVROT_1, TOPREAL1, SPRECT_3, BOOLMARK, JORDAN5B, JORDAN3, JORDAN9, ZFMISC_1, GOBOARD1, SPRECT_1, TARSKI, TOPREAL3, FINSEQ_3, RELAT_1, FUNCT_1, TOPREAL5, JORDAN10, GOBOARD2, CARD_1, CARD_2, ENUMSET1, SPRECT_4, JORDAN1B, SPRECT_5, JORDAN5D, JORDAN1E, PARTFUN2, JORDAN1F, JORDAN5C, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, MATRIX_0, XREAL_0, NAT_D, RLTOPSP1;
schemes NAT_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, FINSEQ_5, FINSEQ_6, STRUCT_0, PRE_TOPC, GOBOARD1, SPPOL_2, SPRECT_1, SPRECT_2, SPRECT_3, REVROT_1, TOPREAL6, JORDAN8, JORDAN1A, JORDAN1E, CARD_1, EUCLID, SPPOL_1, NEWTON, ORDINAL1, SUBSET_1;
constructors HIDDEN, REAL_1, FINSEQ_4, NEWTON, RFINSEQ, FINSEQ_5, CONNSP_1, TOPS_2, MATRIX_1, TOPMETR, PSCOMP_1, JORDAN3, JORDAN5C, JORDAN6, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities PSCOMP_1, CARD_1, ORDINAL1;
expansions TARSKI, XBOOLE_0;
theorem Th46:
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,1)),
((Gauge (C,n)) * (i,j)))
meets L~ (Lower_Seq (C,n))
theorem Th50:
for
f being
S-Sequence_in_R2 for
Q being
closed Subset of
(TOP-REAL 2) st
L~ f meets Q & not
f /. 1
in Q &
First_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
in rng f holds
(L~ (mid (f,1,((First_Point ((L~ f),(f /. 1),(f /. (len f)),Q)) .. f)))) /\ Q = {(First_Point ((L~ f),(f /. 1),(f /. (len f)),Q))}
theorem Th51:
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat st
n > 0 holds
for
k being
Nat st 1
<= k &
k < (First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n)) holds
((Upper_Seq (C,n)) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
theorem Th52:
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat st
n > 0 holds
for
k being
Nat st 1
<= k &
k < (First_Point ((L~ (Rev (Lower_Seq (C,n)))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Rev (Lower_Seq (C,n))) holds
((Rev (Lower_Seq (C,n))) /. k) `1 < ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
theorem Th53:
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat st
n > 0 holds
for
q being
Point of
(TOP-REAL 2) st
q in rng (mid ((Upper_Seq (C,n)),2,((First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) .. (Upper_Seq (C,n))))) holds
q `1 <= ((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2
theorem Th54:
for
C being
connected compact non
horizontal non
vertical Subset of
(TOP-REAL 2) for
n being
Nat st
n > 0 holds
(First_Point ((L~ (Upper_Seq (C,n))),(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `2 > (Last_Point ((L~ (Lower_Seq (C,n))),(E-max (L~ (Cage (C,n)))),(W-min (L~ (Cage (C,n)))),(Vertical_Line (((W-bound (L~ (Cage (C,n)))) + (E-bound (L~ (Cage (C,n))))) / 2)))) `2
theorem
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,1)),
((Gauge (C,n)) * (i,j)))
meets Lower_Arc (L~ (Cage (C,n)))