environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, XXREAL_0, CARD_1, COMPLEX1, ARYTM_1, ARYTM_3, FINSEQ_1, RELAT_1, FUNCT_1, ORDINAL2, PRE_TOPC, EUCLID, RVSUM_1, SQUARE_1, XBOOLE_0, RELAT_2, TARSKI, STRUCT_0, NAT_1, XXREAL_2, CONNSP_1, METRIC_1, CONVEX1, CONNSP_3, ZFMISC_1, SETFAM_1, RLTOPSP1, FINSEQ_2, SUPINF_2, BORSUK_1, XXREAL_1, BORSUK_2, GRAPH_1, TOPMETR, TREAL_1, VALUED_1, FUNCT_4, RCOMP_1, TOPREAL1, TOPS_2, PCOMPS_1, WEIERSTR, SEQ_4, PARTFUN1, FUNCOP_1, BINOP_2, ORDINAL4, JORDAN3, TBSP_1, CONNSP_2, RUSUB_4, SPPOL_1, GOBOARD2, SPRECT_1, TREES_1, PSCOMP_1, GOBOARD1, MCART_1, MATRIX_1, GOBOARD9, GOBOARD5, TOPS_1, JORDAN1, SPRECT_2, JORDAN2C;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RVSUM_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_2, COMPLEX1, SEQM_3, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, METRIC_1, BINOP_2, PCOMPS_1, CONNSP_1, CONNSP_2, TBSP_1, CONNSP_3, TOPMETR, RCOMP_1, FINSEQ_1, FINSEQ_2, DOMAIN_1, STRUCT_0, SQUARE_1, BORSUK_2, XXREAL_0, SEQ_4, FINSEQ_6, FUNCOP_1, FUNCT_3, TREAL_1, FUNCT_4, RLVECT_1, RUSUB_4, RLTOPSP1, CONVEX1, EUCLID, SPPOL_1, PSCOMP_1, SPRECT_1, SPRECT_2, TOPREAL1, MATRIX_0, GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD9, JORDAN2B, REAL_1, NAT_1, NAT_D, WEIERSTR, FINSOP_1;
definitions TARSKI, XBOOLE_0, TOPS_2, TBSP_1, RLTOPSP1, XXREAL_2;
theorems PRE_TOPC, CONNSP_1, EUCLID, TBSP_1, TOPREAL3, NAT_1, JGRAPH_1, JORDAN1, TOPS_2, FUNCT_2, BORSUK_1, TOPMETR, TOPREAL1, FINSEQ_2, ABSVALUE, RVSUM_1, SQUARE_1, BORSUK_2, TOPREAL5, WEIERSTR, TARSKI, SEQ_4, FUNCT_1, METRIC_1, SUBSET_1, FUNCOP_1, ZFMISC_1, FINSEQ_1, FINSEQ_4, RELAT_1, FUNCT_3, RCOMP_1, FUNCT_4, HEINE, TREAL_1, CONNSP_3, JORDAN6, COMPTS_1, TSEP_1, CONNSP_2, TOPS_1, JORDAN5D, JORDAN2B, GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD6, UNIFORM1, FINSEQ_6, MATRIX_0, GOBOARD9, GOBRD12, SPRECT_1, CARD_1, CARD_2, ENUMSET1, SPRECT_2, SPRECT_3, SEQ_2, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_0, TOPRNS_1, XCMPLX_0, XCMPLX_1, BINOP_2, COMPLEX1, XREAL_1, XXREAL_0, FINSOP_1, XXREAL_1, SEQM_3, NAT_D, VALUED_1, RLTOPSP1, RLVECT_1, FINSEQ_3, SPPOL_1, RUSUB_4, CONVEX1, METRIC_6, XTUPLE_0, RLVECT_4;
schemes NAT_1, CLASSES1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, BORSUK_1, TBSP_1, EUCLID, TOPMETR, GOBOARD2, JORDAN1, BORSUK_2, SPRECT_1, SPRECT_3, VALUED_0, RLTOPSP1, JORDAN2B, MONOID_0, SEQ_4, SPPOL_1, CARD_1, NAT_1, SQUARE_1, ORDINAL1;
constructors HIDDEN, REAL_1, SQUARE_1, FINSEQOP, RCOMP_1, FINSOP_1, TOPS_1, CONNSP_1, TOPS_2, COMPTS_1, TBSP_1, MONOID_0, TREAL_1, GOBOARD2, SPPOL_1, JORDAN1, PSCOMP_1, WEIERSTR, BORSUK_2, GOBOARD9, CONNSP_3, JORDAN2B, SPRECT_1, SPRECT_2, BINOP_2, GOBOARD1, NAT_D, SEQ_4, FUNCSDOM, CONVEX1, RUSUB_4, SETWISEO, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities EUCLID, BINOP_1, SQUARE_1, SUBSET_1, PSCOMP_1, FINSEQ_2, CONNSP_3, RVSUM_1, STRUCT_0, VALUED_1, ALGSTR_0, RLTOPSP1, METRIC_1, CONVEX1;
expansions TARSKI, XBOOLE_0, TOPS_2, TBSP_1, RLTOPSP1, XXREAL_2, METRIC_1;
Lm1:
for n being Nat
for r being Real st r > 0 holds
for x, y, z being Element of (Euclid n) st x = 0* n holds
for p being Element of (TOP-REAL n) st p = y & r * p = z holds
r * (dist (x,y)) = dist (x,z)
Lm2:
for n being Nat
for r, s being Real st r > 0 holds
for x being Element of (Euclid n) st x = 0* n holds
for A being Subset of (TOP-REAL n) st A = Ball (x,s) holds
r * A = Ball (x,(r * s))
Lm3:
for n being Nat
for r, s, t being Real st 0 < s & s <= t holds
for x being Element of (Euclid n) st x = 0* n holds
for BA being Subset of (TOP-REAL n) st BA = Ball (x,r) holds
s * BA c= t * BA
theorem Th27:
for
n being
Nat for
P being
Subset of
(TOP-REAL n) for
w1,
w2,
w3,
w4,
w5,
w6,
w7 being
Point of
(TOP-REAL n) st
w1 in P &
w2 in P &
w3 in P &
w4 in P &
w5 in P &
w6 in P &
w7 in P &
LSeg (
w1,
w2)
c= P &
LSeg (
w2,
w3)
c= P &
LSeg (
w3,
w4)
c= P &
LSeg (
w4,
w5)
c= P &
LSeg (
w5,
w6)
c= P &
LSeg (
w6,
w7)
c= P holds
ex
h being
Function of
I[01],
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w7 = h . 1 )
theorem Th35:
for
n being
Nat for
a being
Real for
Q being
Subset of
(TOP-REAL n) for
w1,
w7 being
Point of
(TOP-REAL n) st
n >= 2 &
Q = { q where q is Point of (TOP-REAL n) : |.q.| > a } &
w1 in Q &
w7 in Q & ex
r being
Real st
(
w1 = r * w7 or
w7 = r * w1 ) holds
ex
w2,
w3,
w4,
w5,
w6 being
Point of
(TOP-REAL n) st
(
w2 in Q &
w3 in Q &
w4 in Q &
w5 in Q &
w6 in Q &
LSeg (
w1,
w2)
c= Q &
LSeg (
w2,
w3)
c= Q &
LSeg (
w3,
w4)
c= Q &
LSeg (
w4,
w5)
c= Q &
LSeg (
w5,
w6)
c= Q &
LSeg (
w6,
w7)
c= Q )
theorem Th36:
for
n being
Nat for
a being
Real for
Q being
Subset of
(TOP-REAL n) for
w1,
w7 being
Point of
(TOP-REAL n) st
n >= 2 &
Q = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } &
w1 in Q &
w7 in Q & ex
r being
Real st
(
w1 = r * w7 or
w7 = r * w1 ) holds
ex
w2,
w3,
w4,
w5,
w6 being
Point of
(TOP-REAL n) st
(
w2 in Q &
w3 in Q &
w4 in Q &
w5 in Q &
w6 in Q &
LSeg (
w1,
w2)
c= Q &
LSeg (
w2,
w3)
c= Q &
LSeg (
w3,
w4)
c= Q &
LSeg (
w4,
w5)
c= Q &
LSeg (
w5,
w6)
c= Q &
LSeg (
w6,
w7)
c= Q )