:: Completeness of the $\sigma$-Additive Measure. Measure Theory :: by J\'ozef Bia{\l}as :: :: Received February 22, 1992 :: Copyright (c) 1992-2012 Association of Mizar Users
uniqueness
for b1, b2 being non emptySubset-Family of X st ( for A being set holds ( A in b1 iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) ) & ( for A being set holds ( A in b2 iff ex B being set st ( B in S & ex C being thin of M st A = B \/ C ) ) ) holds b1= b2
uniqueness
for b1, b2 being non emptySubset-Family of X st ( for B being set holds ( B in b1 iff ( B in S & B c= A & A \ B is thin of M ) ) ) & ( for B being set holds ( B in b2 iff ( B in S & B c= A & A \ B is thin of M ) ) ) holds b1= b2
for X being set for S being SigmaField of X for M being sigma_Measure of S for B1, B2 being set st B1 in S & B2 in S holds for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds M . B1 = M . B2
uniqueness
for b1, b2 being sigma_Measure of (COM (S,M)) st ( for B being set st B in S holds for C being thin of M holds b1.(B \/ C)= M . B ) & ( for B being set st B in S holds for C being thin of M holds b2.(B \/ C)= M . B ) holds b1= b2
:: Completeness of sigma_additive Measure
::