Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

### The abstract of the Mizar article:

### Completeness of the $\sigma$-Additive Measure. Measure Theory

**by****Jozef Bialas**- Received February 22, 1992
- MML identifier: MEASURE3

- [ Mizar article, MML identifier index ]

environ vocabulary SUPINF_1, FUNCT_1, SUPINF_2, ARYTM_3, ORDINAL2, RELAT_1, MEASURE1, MEASURE2, SETFAM_1, BOOLE, TARSKI, ARYTM_1, RLVECT_1, PROB_1, MEASURE3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2, REAL_1, NAT_1, SETFAM_1, SUPINF_1, SUPINF_2, MEASURE1, MEASURE2; constructors NAT_1, REAL_1, SUPINF_2, MEASURE2, PROB_2, MEMBERED, XBOOLE_0; clusters SUBSET_1, SUPINF_1, MEASURE1, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2; requirements NUMERALS, SUBSET, BOOLE, ARITHM; begin :: :: Some additional properties about R_eal numbers :: reserve X for set; theorem :: MEASURE3:1 for x being R_eal holds (-infty <'x & x <'+infty) implies x is Real; theorem :: MEASURE3:2 for x being R_eal holds ((not x = -infty) & (not x = +infty)) implies x is Real; theorem :: MEASURE3:3 for F1,F2 being Function of NAT,ExtREAL st (for n being Nat holds Ser(F1).n <=' Ser(F2).n) holds (SUM(F1) <=' SUM(F2)); theorem :: MEASURE3:4 for F1,F2 being Function of NAT,ExtREAL holds ((for n being Nat holds Ser(F1).n = Ser(F2).n) implies (SUM(F1) = SUM(F2))); :: :: Some additional theorems about measures and functions :: definition let X be set; let S be sigma_Field_Subset of X; redefine mode N_Measure_fam of S; synonym N_Sub_fam of S; end; definition let X be set; let S be sigma_Field_Subset of X; let F be Function of NAT,S; redefine func rng F -> N_Measure_fam of S; end; theorem :: MEASURE3:5 for S being sigma_Field_Subset of X, M being sigma_Measure of S, F being Function of NAT,S, A being Element of S holds (meet rng F c= A & (for n being Element of NAT holds A c= F.n)) implies M.A = M.(meet rng F); theorem :: MEASURE3:6 for S being sigma_Field_Subset of X holds for G,F being Function of NAT,S holds (G.0 = {} & for n being Element of NAT holds (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n)) implies union rng G = F.0 \ meet rng F; theorem :: MEASURE3:7 for S being sigma_Field_Subset of X holds for G,F being Function of NAT,S holds (G.0 = {} & for n being Element of NAT holds (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n)) implies meet rng F = F.0 \ union rng G; theorem :: MEASURE3:8 for S being sigma_Field_Subset of X holds for M being sigma_Measure of S holds for G,F being Function of NAT,S holds (M.(F.0) <'+infty & G.0 = {} & for n being Element of NAT holds (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n)) implies M.(meet rng F) = M.(F.0) - M.(union rng G); theorem :: MEASURE3:9 for S being sigma_Field_Subset of X holds for M being sigma_Measure of S holds for G,F being Function of NAT,S holds (M.(F.0) <'+infty & G.0 = {} & for n being Element of NAT holds (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n)) implies M.(union rng G) = M.(F.0) - M.(meet rng F); theorem :: MEASURE3:10 for S being sigma_Field_Subset of X holds for M being sigma_Measure of S holds for G,F being Function of NAT,S holds (M.(F.0) <'+infty & G.0 = {} & for n being Element of NAT holds (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n)) implies M.(meet rng F) = M.(F.0) - sup(rng (M*G)); theorem :: MEASURE3:11 for S being sigma_Field_Subset of X holds for M being sigma_Measure of S holds for G,F being Function of NAT,S holds (M.(F.0) <'+infty & G.0 = {} & for n being Element of NAT holds (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n)) implies sup(rng (M*G)) is Real & M.(F.0) is Real & inf(rng (M*F)) is Real; theorem :: MEASURE3:12 for S being sigma_Field_Subset of X holds for M being sigma_Measure of S holds for G,F being Function of NAT,S holds (M.(F.0) <'+infty & G.0 = {} & for n being Element of NAT holds (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n)) implies sup(rng (M*G)) = M.(F.0) - inf(rng (M*F)); theorem :: MEASURE3:13 for S being sigma_Field_Subset of X holds for M being sigma_Measure of S holds for G,F being Function of NAT,S holds (M.(F.0) <'+infty & G.0 = {} & for n being Element of NAT holds (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n)) implies inf(rng (M*F)) = M.(F.0) - sup(rng (M*G)); theorem :: MEASURE3:14 for S being sigma_Field_Subset of X holds for M being sigma_Measure of S holds for F being Function of NAT,S holds ((for n being Element of NAT holds F.(n+1) c= F.n) & M.(F.0) <'+infty) implies (M.(meet rng F) = inf(rng (M*F))); theorem :: MEASURE3:15 for S being sigma_Field_Subset of X holds for M being Measure of S holds for T being N_Measure_fam of S holds for F being Sep_Sequence of S holds T = rng F implies SUM(M*F) <=' M.(union T); theorem :: MEASURE3:16 for S being sigma_Field_Subset of X holds for M being Measure of S holds for F being Sep_Sequence of S holds SUM(M*F) <=' M.(union rng F); theorem :: MEASURE3:17 for S being sigma_Field_Subset of X holds for M being Measure of S st (for F being Sep_Sequence of S holds M.(union rng F) <=' SUM(M*F)) holds M is sigma_Measure of S; :: :: Completeness of sigma_additive Measure :: definition let X be set; let S be sigma_Field_Subset of X; let M be sigma_Measure of S; canceled; pred M is_complete S means :: MEASURE3:def 2 for A being Subset of X for B being set st B in S holds (A c= B & M.B = 0.) implies A in S; end; definition let X be set; let S be sigma_Field_Subset of X; let M be sigma_Measure of S; mode thin of M -> Subset of X means :: MEASURE3:def 3 ex B being set st B in S & it c= B & M.B = 0.; end; definition let X be set; let S be sigma_Field_Subset of X; let M be sigma_Measure of S; func COM(S,M) -> non empty Subset-Family of X means :: MEASURE3:def 4 for A being set holds (A in it iff (ex B being set st B in S & ex C being thin of M st A = B \/ C)); end; definition let X be set; let S be sigma_Field_Subset of X; let M be sigma_Measure of S; let A be Element of COM(S,M); func MeasPart(A) -> non empty Subset-Family of X means :: MEASURE3:def 5 for B being set holds (B in it iff (B in S & B c= A & A \ B is thin of M)); end; theorem :: MEASURE3:18 for S being sigma_Field_Subset of X holds for M being sigma_Measure of S holds for F being Function of NAT,COM(S,M) holds ex G being Function of NAT,S st for n being Element of NAT holds G.n in MeasPart(F.n); theorem :: MEASURE3:19 for S being sigma_Field_Subset of X holds for M being sigma_Measure of S holds for F being Function of NAT,COM(S,M) holds for G being Function of NAT,S holds (ex H being Function of NAT,bool X st for n being Element of NAT holds H.n = F.n \ G.n); theorem :: MEASURE3:20 for S being sigma_Field_Subset of X holds for M being sigma_Measure of S holds for F being Function of NAT,bool X st (for n being Element of NAT holds F.n is thin of M) holds ex G being Function of NAT,S st (for n being Element of NAT holds F.n c= G.n & M.(G.n) = 0.); theorem :: MEASURE3:21 for S being sigma_Field_Subset of X holds for M being sigma_Measure of S holds for D being non empty Subset-Family of X holds (for A being set holds (A in D iff ex B being set st B in S & ex C being thin of M st A = B \/ C)) implies D is sigma_Field_Subset of X; definition let X be set; let S be sigma_Field_Subset of X; let M be sigma_Measure of S; cluster COM(S,M) -> sigma_Field_Subset-like compl-closed non empty; end; theorem :: MEASURE3:22 for S being sigma_Field_Subset of X, M being sigma_Measure of S, B1,B2 being set st B1 in S & B2 in S holds for C1,C2 being thin of M holds B1 \/ C1 = B2 \/ C2 implies M.B1 = M.B2; definition let X be set; let S be sigma_Field_Subset of X; let M be sigma_Measure of S; func COM(M) -> sigma_Measure of COM(S,M) means :: MEASURE3:def 6 for B being set st B in S for C being thin of M holds it.(B \/ C) = M.B; end; theorem :: MEASURE3:23 for S being sigma_Field_Subset of X holds for M being sigma_Measure of S holds COM(M) is_complete COM(S,M);

Back to top