Q00:
ex A1 being SetSequence of REAL st
for n being Nat holds A1 . n = {n}
Q0:
ex A being SetSequence of Borel_Sets st
for n being Nat holds A . n = {n}
H2:
ex A being SetSequence of REAL st
for n being Nat holds A . n = {(- n)}
definition
let p be
Nat;
let Omega,
Omega2 be non
empty set ;
let F be
SigmaField of
Omega;
let F2 be
SigmaField of
Omega2;
let X be
set ;
assume A1:
X = set_of_random_variables_on (
F,
F2)
;
let G be
sequence of
X;
Element_Ofredefine func Element_Of (
F,
F2,
G,
p)
-> random_variable of
F,
F2;
correctness
coherence
Element_Of (F,F2,G,p) is random_variable of F,F2;
end;
definition
let phi be
Real_Sequence;
let Omega be non
empty set ;
let F be
SigmaField of
Omega;
let X be non
empty set ;
let G be
sequence of
X;
let w be
Element of
Omega;
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w ) & ( for n being Nat holds b2 . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w ) holds
b1 = b2
end;
definition
let d be
Nat;
let phi be
Real_Sequence;
let Omega be non
empty set ;
let F be
SigmaField of
Omega;
let X be non
empty set ;
let G be
sequence of
X;
let w be
Element of
Omega;
correctness
coherence
PortfolioValueFutExt (d,phi,F,G,w) is Real;
compatibility
for b1 being Real holds
( b1 = PortfolioValueFutExt (d,phi,F,G,w) iff b1 = (Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . d );
end;
:: Event of the Borel-Sets