environ
vocabularies HIDDEN, NUMBERS, ZFMISC_1, TOPREAL2, PRE_TOPC, EUCLID, XBOOLE_0, SUBSET_1, TARSKI, STRUCT_0, FUNCT_1, RELAT_1, FUNCT_4, PARTFUN1, TOPREAL1, XXREAL_0, ARYTM_3, CARD_1, ARYTM_1, BORSUK_1, XXREAL_1, TOPMETR, CONNSP_1, REAL_1, RELAT_2, RCOMP_1, XXREAL_2, ORDINAL2, SEQ_4, T_0TOPSP, TOPS_2, RLTOPSP1, TREAL_1, VALUED_1, BORSUK_4, FUNCT_2, MEASURE5;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_2, XREAL_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, RCOMP_1, FUNCT_4, XXREAL_0, STRUCT_0, MEASURE6, PRE_TOPC, COMPTS_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, SEQ_4, TREAL_1, CONNSP_1, BORSUK_1, BORSUK_3, TSEP_1, TOPMETR, MEASURE5, TOPS_2;
definitions TARSKI, CONNSP_1, PARTFUN1, STRUCT_0;
theorems TOPS_2, T_0TOPSP, BORSUK_1, PRE_TOPC, COMPTS_1, TARSKI, TOPMETR, TOPREAL1, RCOMP_1, CONNSP_1, ZFMISC_1, JORDAN5A, TOPREAL6, MEASURE6, TREAL_1, XBOOLE_0, XBOOLE_1, JORDAN6, SEQ_4, INTEGRA1, INTEGRA2, TSEP_1, TOPREAL2, JORDAN5B, FUNCT_2, FUNCT_1, GOBOARD9, RELAT_1, RFUNCT_2, BORSUK_3, FUNCT_4, JGRAPH_2, TOPMETR2, XREAL_1, FRECHET, ENUMSET1, XXREAL_0, XXREAL_1, XXREAL_2, SUBSET_1, MEASURE5, RLTOPSP1;
schemes ;
registrations XBOOLE_0, RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, BORSUK_1, EUCLID, TOPREAL1, TOPREAL2, BORSUK_2, REVROT_1, TOPREAL6, XXREAL_2, TOPMETR, SUBSET_1, MEASURE5, JORDAN2C, ORDINAL1;
constructors HIDDEN, FUNCT_4, CONNSP_1, TOPS_2, COMPTS_1, TSEP_1, TOPREAL1, TOPREAL2, TREAL_1, MEASURE6, BORSUK_3, INTEGRA1, SEQ_4, BINOP_2;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities SUBSET_1, STRUCT_0, RELAT_1;
expansions TARSKI, PARTFUN1, SUBSET_1;
theorem
for
s1,
s3,
s4,
l being
Real st
s1 <= s3 &
s1 < s4 &
0 <= l &
l <= 1 holds
s1 <= ((1 - l) * s3) + (l * s4)
Lm1:
I[01] is closed SubSpace of R^1
by TOPMETR:20, TREAL_1:2;