environ
vocabularies HIDDEN, NUMBERS, PROB_1, MEASURE1, SUBSET_1, MESFUNC5, ORDINAL1, SUPINF_2, SERIES_1, FUNCT_1, NAT_1, ARYTM_3, CARD_1, CARD_3, VALUED_0, SEQ_2, ORDINAL2, XXREAL_0, RELAT_1, PROB_2, XBOOLE_0, TARSKI, FINSEQ_1, ZFMISC_1, FUNCOP_1, FUNCT_2, MEASURE7, SUPINF_1, NAGATA_2, MCART_1, FUNCT_7, XXREAL_2, REAL_1, MEASURE4, PROB_3, SETLIM_2, ARYTM_1, SETLIM_1, EQREL_1, LATTICE5, MEASURE2, MEASURE8;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XXREAL_0, XXREAL_2, XREAL_0, VALUED_0, RELAT_1, FUNCOP_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NUMBERS, FINSEQ_1, SETFAM_1, RINFSUP2, MEASURE1, MEASURE2, MEASURE4, MESFUNC5, SUPINF_2, XXREAL_3, NAT_1, MESFUNC9, SUPINF_1, RECDEF_1, PROB_1, PROB_2, PROB_3, SETLIM_1, SETLIM_2, NAGATA_2, FUNCT_7;
definitions TARSKI, PROB_2;
theorems ZFMISC_1, TARSKI, XBOOLE_0, PROB_1, MEASURE1, FUNCT_2, FUNCT_1, XBOOLE_1, PROB_3, FINSEQ_1, RELAT_1, MEASURE4, ORDINAL1, NAT_1, FUNCOP_1, SUPINF_2, XXREAL_2, PROB_4, MEASURE7, XXREAL_0, MEASURE6, FINSUB_1, CARD_3, RINFSUP2, MESFUNC9, VALUED_0, MESFUNC5, MONOID_1, MEASURE2, SETLIM_1, SETLIM_2, ABCMIZ_1, PROB_2, NAGATA_2, FUNCTOR1, FUNCT_7, XXREAL_3, XREAL_0, PARTFUN1, XTUPLE_0;
schemes FUNCT_2, NAT_1, BINOP_2, XBOOLE_0, SUBSET_1;
registrations MEMBERED, ORDINAL1, MEASURE1, XBOOLE_0, NUMBERS, XXREAL_0, VALUED_0, FUNCT_1, FUNCT_2, SUBSET_1, RELSET_1, MEASURE4, NAT_1, XXREAL_3, XREAL_0, PROB_3;
constructors HIDDEN, KURATO_0, MESFUNC5, RINFSUP2, MESFUNC9, SUPINF_1, PROB_3, MEASURE7, RECDEF_1, SETLIM_2, SETLIM_1, NAGATA_2, FUNCT_7;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET;
equalities SUPINF_2, RINFSUP2, MESFUNC9;
expansions SUPINF_2, TARSKI, MESFUNC9;
Lm1:
for X being set
for F being Field_Subset of X holds NAT --> X is Set_Sequence of F
Lm2:
for X being set
for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds
(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)