environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, FUNCT_1, FINSEQ_1, CARD_1, ORDINAL4, RELAT_1, TARSKI, ZFMISC_1, PRE_TOPC, SUBSET_1, CONNSP_1, STRUCT_0, EUCLID, RCOMP_1, TOPREAL1, RLTOPSP1, PARTFUN1, ARYTM_3, SPPOL_1, SPPOL_2, MCART_1, PSCOMP_1, XXREAL_0, REAL_1, FINSEQ_6, GOBOARD5, ORDINAL2, NAT_1, GOBOARD1, GOBOARD2, MATRIX_1, TREES_1, COMPLEX1, ARYTM_1, XXREAL_1, XXREAL_2, JORDAN1, GOBOARD9, TOPS_1, SPRECT_1, SEQ_4;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0, REAL_1, NAT_1, FUNCT_1, PARTFUN1, RELSET_1, FINSEQ_1, FINSEQ_4, FINSEQ_6, XXREAL_0, XXREAL_2, SEQM_3, SEQ_4, MATRIX_0, RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, JORDAN1, GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD9, SPPOL_1, SPPOL_2, PSCOMP_1;
definitions SPPOL_1, TOPREAL1, GOBOARD1, GOBOARD5, TARSKI, JORDAN1, XBOOLE_0, SEQM_3, XXREAL_2;
theorems FINSEQ_1, SPPOL_2, SPPOL_1, EUCLID, FUNCT_1, ZFMISC_1, PSCOMP_1, FINSEQ_3, GOBOARD1, TARSKI, GOBOARD2, ENUMSET1, MCART_1, CARD_2, TOPREAL1, NAT_1, FINSEQ_4, FINSEQ_6, TOPREAL3, GOBOARD7, JORDAN1, GOBRD12, GOBOARD9, CONNSP_1, TOPS_2, JORDAN5A, COMPTS_1, FINSEQ_2, RELAT_1, FUNCT_2, SEQ_4, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, PRE_TOPC, XXREAL_1, RLTOPSP1, MEASURE6, SEQM_3, NAT_D, RELSET_1, XTUPLE_0, MATRIX_0, XREAL_0;
schemes NAT_1;
registrations XBOOLE_0, NUMBERS, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, SEQ_2, FINSEQ_5, FINSEQ_6, STRUCT_0, PRE_TOPC, EUCLID, GOBOARD2, SPPOL_2, PSCOMP_1, WAYBEL_2, VALUED_0, XXREAL_2, COMPTS_1, FUNCT_1, RLTOPSP1, SEQ_4, SUBSET_1, RELSET_1, ORDINAL1;
constructors HIDDEN, REAL_1, COMPLEX1, RCOMP_1, FINSEQ_4, REALSET1, TOPS_1, CONNSP_1, COMPTS_1, TOPREAL4, GOBOARD2, SPPOL_1, JORDAN1, SPPOL_2, PSCOMP_1, GOBOARD9, GOBOARD1, SEQ_4, RELSET_1, CONVEX1, RVSUM_1, MEASURE6, SQUARE_1, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities TOPREAL1, PSCOMP_1, RLTOPSP1;
expansions SPPOL_1, JORDAN1, XBOOLE_0;
theorem Th51:
for
t,
r1,
r2 being
Real st
r1 <= r2 holds
(
t in [.r1,r2.] iff ex
s1 being
Real st
(
0 <= s1 &
s1 <= 1 &
t = (s1 * r1) + ((1 - s1) * r2) ) )
theorem Th87:
for
r1,
r2,
s1,
s2 being
Real st
r1 < r2 &
s1 < s2 holds
[.r1,r2,s1,s2.] is
Jordan