environ
vocabularies HIDDEN, NUMBERS, CARD_1, XXREAL_0, ARYTM_3, RELAT_1, ARYTM_1, XBOOLE_0, SUBSET_1, FUNCT_1, MCART_1, ZFMISC_1, NORMSP_1, PRE_TOPC, METRIC_1, SUPINF_2, TARSKI, REAL_1, COMPLEX1, LOPBAN_1, STRUCT_0, NORMSP_2, RCOMP_1, CONVEX1, XCMPLX_0, PREPOWER, SERIES_1, NEWTON, NAT_1, CARD_3, ORDINAL2, SEQ_2, RSSPACE3, FUNCT_2, PARTFUN1, FCONT_1, PROB_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, FUNCT_1, RELSET_1, FUNCT_2, XTUPLE_0, MCART_1, PRE_TOPC, DOMAIN_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, STRUCT_0, XXREAL_0, SEQ_2, NEWTON, PREPOWER, SERIES_1, RLVECT_1, CONVEX1, RUSUB_4, NORMSP_0, NORMSP_1, NORMSP_2, RSSPACE3, LOPBAN_1, NFCONT_1, LOPBAN_5, KURATO_2, T_0TOPSP;
definitions TARSKI, T_0TOPSP, XBOOLE_0;
theorems TARSKI, SEQ_2, RLVECT_1, RELAT_1, RUSUB_4, RLTOPSP1, SERIES_1, PREPOWER, ZFMISC_1, FUNCT_2, XBOOLE_0, XREAL_1, XCMPLX_1, NORMSP_1, PRE_TOPC, NFCONT_1, XXREAL_0, FUNCT_1, NEWTON, MESFUNC1, NORMSP_2, RINFSUP1, ABSVALUE, XCMPLX_0, LOPBAN_3, ORDINAL1, RSSPACE2, LOPBAN_1, NAT_1, PROB_1, LOPBAN_5, CONVEX1, VECTSP_1, NORMSP_0;
schemes FUNCT_2, RECDEF_1, NAT_1;
registrations XREAL_0, XXREAL_0, ORDINAL1, RELSET_1, STRUCT_0, TOPS_1, SUBSET_1, NAT_1, NORMSP_1, NORMSP_2, FUNCT_2, LOPBAN_1, NORMSP_0, NEWTON, XTUPLE_0;
constructors HIDDEN, REAL_1, DOMAIN_1, SEQ_2, PCOMPS_1, RUSUB_4, CONVEX1, NFCONT_1, NEWTON, PREPOWER, SERIES_1, NORMSP_2, RSSPACE3, LOPBAN_5, T_0TOPSP, RELSET_1, COMSEQ_2, XTUPLE_0, BINOP_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities RLVECT_1, PCOMPS_1, CONVEX1, RUSUB_4, ALGSTR_0, NORMSP_2, XBOOLE_0, LOPBAN_5;
expansions TARSKI, CONVEX1, XBOOLE_0;
theorem Th1:
for
x,
y being
Real st
0 <= x &
x < y holds
ex
s0 being
Real st
(
0 < s0 &
x < y / (1 + s0) &
y / (1 + s0) < y )
scheme
RecExD3{
F1()
-> non
empty set ,
F2()
-> Element of
F1(),
F3()
-> Element of
F1(),
P1[
object ,
object ,
object ,
object ] } :
ex
f being
sequence of
F1() st
(
f . 0 = F2() &
f . 1
= F3() & ( for
n being
Nat holds
P1[
n,
f . n,
f . (n + 1),
f . (n + 2)] ) )
provided
A1:
for
n being
Nat for
x,
y being
Element of
F1() ex
z being
Element of
F1() st
P1[
n,
x,
y,
z]