environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, BORSUK_1, PCOMPS_1, TOPMETR, CARD_1, FINSEQ_1, XXREAL_0, ORDINAL4, FUNCT_1, ARYTM_3, RELAT_1, PARTFUN1, ORDINAL2, ARYTM_1, JGRAPH_6, CONVEX1, MCART_1, RLTOPSP1, REAL_1, TOPREALA, TARSKI, STRUCT_0, XXREAL_1, MEASURE5, XBOOLE_0, FCONT_2, METRIC_1, NAT_1, INT_1, COMPLEX1, XXREAL_2, RELAT_2, RCOMP_1, CONNSP_1, GRAPH_1, WEIERSTR, PSCOMP_1, GOBOARD1, GOBOARD4, TOPREAL1, BORSUK_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, NAT_1, NAT_D, SEQM_3, STRUCT_0, TOPREAL1, PRE_TOPC, GOBOARD1, GOBOARD4, TOPMETR, PCOMPS_1, COMPTS_1, WEIERSTR, METRIC_1, TBSP_1, RCOMP_1, UNIFORM1, INT_1, CONNSP_1, PSCOMP_1, RLVECT_1, RLTOPSP1, EUCLID, BORSUK_1, BORSUK_2, JGRAPH_6, TOPREALA, TOPALG_2;
definitions TARSKI, XBOOLE_0, JORDAN1, TOPALG_2;
theorems TARSKI, FUNCT_1, FINSEQ_1, NAT_1, FINSEQ_4, RELAT_1, FINSEQ_3, TOPREAL1, GOBOARD4, TOPREAL3, EUCLID, UNIFORM1, WEIERSTR, PRE_TOPC, TBSP_1, HEINE, COMPTS_1, TOPMETR, PSCOMP_1, BORSUK_1, RCOMP_1, FUNCT_2, XBOOLE_0, XBOOLE_1, TOPRNS_1, XCMPLX_1, JGRAPH_1, INT_1, XREAL_0, CONNSP_1, XREAL_1, BORSUK_2, TSEP_1, JGRAPH_6, JORDAN5B, FINSEQ_2, XXREAL_0, TOPS_2, PARTFUN1, XXREAL_1, XXREAL_2, SEQM_3, RLTOPSP1, RELSET_1, ORDINAL1;
schemes FINSEQ_1, NAT_1;
registrations RELAT_1, XREAL_0, INT_1, FINSEQ_1, STRUCT_0, PRE_TOPC, BORSUK_1, EUCLID, TOPREAL1, BORSUK_2, JORDAN5A, TOPALG_2, MEMBERED, VALUED_0, FUNCT_2, XXREAL_2, RELSET_1, SPPOL_1, TOPMETR, FUNCT_1, NAT_1, ORDINAL1;
constructors HIDDEN, REAL_1, RCOMP_1, CONNSP_1, COMPTS_1, TBSP_1, TOPREAL1, GOBOARD1, GOBOARD4, PSCOMP_1, WEIERSTR, UNIFORM1, JGRAPH_6, TOPALG_2, TOPREALA, BORSUK_2, NAT_D, XXREAL_2, FUNCSDOM, CONVEX1, BINOP_2, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, RLTOPSP1, EUCLID, TOPREALA, STRUCT_0;
expansions TARSKI, XBOOLE_0, TOPALG_2;
Lm1:
I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1))
by TOPMETR:20, TOPMETR:def 7;
Lm2:
for x being set
for f being FinSequence st 1 <= len f holds
( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) )
Lm3:
for f being FinSequence of REAL st ( for k being Nat st 1 <= k & k < len f holds
f /. k < f /. (k + 1) ) holds
f is increasing
theorem
for
a,
b,
c,
d being
Real for
ar,
br,
cr,
dr being
Point of
(Trectangle (a,b,c,d)) for
h being
Path of
ar,
br for
v being
Path of
dr,
cr for
Ar,
Br,
Cr,
Dr being
Point of
(TOP-REAL 2) st
Ar `1 = a &
Br `1 = b &
Cr `2 = c &
Dr `2 = d &
ar = Ar &
br = Br &
cr = Cr &
dr = Dr holds
ex
s,
t being
Point of
I[01] st
h . s = v . t