environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, CARD_3, FUNCT_1, RELAT_1, FINSEQ_1, XBOOLE_0, ARYTM_3, XXREAL_0, CARD_1, TARSKI, NAT_1, ZFMISC_1, ORDINAL4, PROB_1, FINSUB_1, SETFAM_1, PROB_2, MEASURE9, MSSUBFAM, FUNCOP_1, SUPINF_2, VALUED_0, FUNCT_2, PARTFUN1, MEASURE1, ORDINAL2, SERIES_1, MESFUNC5, SUPINF_1, SEQ_2, MEASURE6, SEQFUNC, REAL_1, XCMPLX_0, PBOOLE, MESFUNC9, VALUED_1, SIMPLEX0, SRINGS_3, MEASURE3, MEASURE5, XXREAL_1, MEASUR10, SRINGS_1, SRINGS_4, MESFUNC8, MESFUNC1, FUNCT_3, INTEGRA5, RFUNCT_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSUB_1, CARD_1, CARD_3, NUMBERS, FUNCT_3, XXREAL_1, XXREAL_3, BINOP_1, XTUPLE_0, PROB_1, XCMPLX_0, XREAL_0, XXREAL_0, SIMPLEX0, NAT_1, VALUED_0, SUPINF_1, FINSEQ_1, FINSEQOP, SUPINF_2, PROB_2, SEQFUNC, MEASURE1, MEASURE3, MEASURE5, MESFUNC1, MESFUNC2, MESFUNC5, MESFUNC8, MESFUNC9, RINFSUP2, EXTREAL1, SRINGS_3, MEASURE9, SRINGS_1, SRINGS_4, MESFUNC6;
definitions ;
theorems TARSKI, XBOOLE_0, XREAL_0, FINSEQ_1, NAT_1, FUNCT_1, CARD_3, XXREAL_0, ZFMISC_1, FINSEQ_3, XBOOLE_1, PROB_2, XREAL_1, PROB_1, FINSUB_1, SETFAM_1, FUNCOP_1, XXREAL_3, MEASURE1, VALUED_0, FUNCT_2, RELAT_1, MESFUNC5, EXTREAL1, MESFUNC9, FINSEQ_2, PARTFUN1, ORDINAL1, ABCMIZ_1, RINFSUP2, MEASURE8, MESFUNC1, SUPINF_2, XTUPLE_0, SRINGS_3, MEASURE3, CARD_1, MEASURE9, MEASURE5, SRINGS_2, XXREAL_1, FINANCE1, FINANCE2, SRINGS_4, FUNCT_5, MESFUNC8, FUNCT_3, MESFUNC2, MESFUNC6, MESFUNC7, RELSET_1;
schemes FINSEQ_1, NAT_1, FUNCT_2, FUNCT_1, SEQFUNC;
registrations XREAL_0, MEMBERED, FUNCT_1, XBOOLE_0, FINSEQ_1, RELAT_1, SUBSET_1, XXREAL_0, ROUGHS_1, NUMBERS, VALUED_0, FUNCT_2, ORDINAL1, MESFUNC9, RELSET_1, PROB_1, MEASURE1, MESFUNC5, NAT_1, PARTFUN1, XXREAL_3, CARD_1, XXREAL_2, SIMPLEX0, SRINGS_3, DBLSEQ_3, MEASURE3, MEASURE9, SRINGS_2, SRINGS_1, SRINGS_4;
constructors HIDDEN, TOPMETR, PROB_2, MESFUNC5, EXTREAL1, SUPINF_1, MESFUNC1, MESFUNC9, RINFSUP2, FINSEQOP, SEQFUNC, MEASURE3, INTEGRA1, SRINGS_1, MEASURE9, SEQ_4, SRINGS_4, MESFUNC2, MESFUNC8, MESFUNC6;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities FINSEQ_1, BINOP_1;
expansions TARSKI, XBOOLE_0;
theorem Th23:
for
A,
A1,
A2,
B,
B1,
B2 being non
empty set holds
( (
[:A1,B1:] misses [:A2,B2:] &
[:A,B:] = [:A1,B1:] \/ [:A2,B2:] ) iff ( (
A1 misses A2 &
A = A1 \/ A2 &
B = B1 &
B = B2 ) or (
B1 misses B2 &
B = B1 \/ B2 &
A = A1 &
A = A2 ) ) )
theorem Th26:
for
X,
Y,
A,
B being
set for
x,
y being
object st
x in X &
y in Y holds
((chi (A,X)) . x) * ((chi (B,Y)) . y) = (chi ([:A,B:],[:X,Y:])) . (
x,
y)
Lm01:
for I being Subset of REAL st I is open_interval holds
I in Borel_Sets
Lm02:
for I being Subset of REAL st I is closed_interval holds
I in Borel_Sets
Lm03:
for I being Subset of REAL st I is right_open_interval holds
I in Borel_Sets
Lm04:
for I being Subset of REAL st I is left_open_interval holds
I in Borel_Sets
Lm05:
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being SemialgebraFamily of X holds S is cap-closed-yielding SemiringFamily of X
Lm06:
for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being FieldFamily of X holds S is SemialgebraFamily of X
definition
let X1,
X2 be
set ;
let S1 be
Field_Subset of
X1;
let S2 be
Field_Subset of
X2;
let m1 be
Measure of
S1;
let m2 be
Measure of
S2;
existence
ex b1 being zeroed V161() Function of (measurable_rectangles (S1,S2)),ExtREAL st
for C being Element of measurable_rectangles (S1,S2) ex A being Element of S1 ex B being Element of S2 st
( C = [:A,B:] & b1 . C = (m1 . A) * (m2 . B) )
uniqueness
for b1, b2 being zeroed V161() Function of (measurable_rectangles (S1,S2)),ExtREAL st ( for C being Element of measurable_rectangles (S1,S2) ex A being Element of S1 ex B being Element of S2 st
( C = [:A,B:] & b1 . C = (m1 . A) * (m2 . B) ) ) & ( for C being Element of measurable_rectangles (S1,S2) ex A being Element of S1 ex B being Element of S2 st
( C = [:A,B:] & b2 . C = (m1 . A) * (m2 . B) ) ) holds
b1 = b2
end;
Lm08:
for X being non empty set
for S being SigmaField of X
for A being Element of S
for r being Real st r > 0 holds
great_eq_dom ((Xchi (A,X)),r) = A
Lm09:
for X being non empty set
for S being SigmaField of X
for A being Element of S
for r being Real st r <= 0 holds
great_eq_dom ((Xchi (A,X)),r) = X