:: Several Properties of the $\sigma$-additive Measure :: by J\'ozef Bia{\l}as :: :: Received July 3, 1991 :: Copyright (c) 1991-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies PROB_1, MEASURE1, FUNCT_1, NUMBERS, RELAT_1, SUPINF_2, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, CARD_1, ARYTM_3, XXREAL_0, NAT_1, ZFMISC_1, VALUED_0, ORDINAL2, MEASURE2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_1, SETFAM_1, PROB_1, SUPINF_2, MEASURE1; constructors PARTFUN1, NAT_1, PROB_2, MEASURE1, SUPINF_1, XREAL_0, RELSET_1; registrations XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0, MEASURE1, MEMBERED, RELSET_1; requirements NUMERALS, SUBSET, BOOLE; begin :: :: Some useful theorems about measures and functions :: reserve X for set; theorem :: MEASURE2:1 for S being SigmaField of X, M being sigma_Measure of S, F being sequence of S holds M*F is nonnegative; definition let X be set; let S be SigmaField of X; mode N_Measure_fam of S -> N_Sub_set_fam of X means :: MEASURE2:def 1 it c= S; end; theorem :: MEASURE2:2 for S being SigmaField of X, T being N_Measure_fam of S holds meet T in S & union T in S; definition let X be set, S be SigmaField of X, T be N_Measure_fam of S; redefine func meet T -> Element of S; redefine func union T -> Element of S; end; theorem :: MEASURE2:3 for S being SigmaField of X, N being sequence of S holds ex F being sequence of S st F.0 = N.0 & for n being Nat holds F.(n+1) = N.(n+1) \ N.n; theorem :: MEASURE2:4 for S being SigmaField of X, N being sequence of S holds ex F being sequence of S st F.0 = N.0 & for n being Nat holds F.(n+1) = N.(n+1) \/ F.n; theorem :: MEASURE2:5 for S being non empty Subset-Family of X, N,F being sequence of S holds F.0 = N.0 & (for n being Nat holds F.(n+1) = N.(n+1) \/ F.n) implies for r being set for n being Nat holds (r in F.n iff ex k being Nat st k <= n & r in N.k); theorem :: MEASURE2:6 for S being non empty Subset-Family of X, N,F being sequence of S holds (F.0 = N.0 & (for n being Nat holds F.(n+1) = N.(n+1) \/ F.n) implies for n,m being Nat st n < m holds F.n c= F.m); theorem :: MEASURE2:7 for S being non empty Subset-Family of X, N, G, F being sequence of S holds G.0 = N.0 & (for n being Nat holds G.(n+1) = N.(n+1) \/ G.n) & F.0 = N.0 & (for n being Nat holds F.(n+1) = N.(n+1) \ G.n ) implies for n,m being Nat st n <= m holds F.n c= G.m; theorem :: MEASURE2:8 for S being SigmaField of X holds for N, G being sequence of S holds ex F being sequence of S st F.0 = N.0 & for n being Nat holds F.(n+1) = N.(n+1) \ G.n; theorem :: MEASURE2:9 for S being SigmaField of X holds for N being sequence of S holds ex F being sequence of S st F.0 = {} & for n being Nat holds F.( n+1) = N.0 \ N.n; theorem :: MEASURE2:10 for S being SigmaField of X holds for N, G, F being sequence of S holds G.0 = N.0 & (for n being Nat holds G.(n+1) = N.(n+1) \/ G.n) & F.0 = N.0 & (for n being Nat holds F.(n+1) = N.(n+1) \ G.n) implies for n,m being Nat st n < m holds F.n misses F.m; theorem :: MEASURE2:11 for S being SigmaField of X, M being sigma_Measure of S, T being N_Measure_fam of S, F being sequence of S st T = rng F holds M.(union T) <= SUM(M*F); theorem :: MEASURE2:12 for S being SigmaField of X, T being N_Measure_fam of S holds ex F being sequence of S st T = rng F; theorem :: MEASURE2:13 for N, F being Function st (F.0 = {} & for n being Nat holds F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n ) for n being Nat holds F.n c= F.(n+1); theorem :: MEASURE2:14 for S being SigmaField of X, M being sigma_Measure of S, T being N_Measure_fam of S st (for A being set st A in T holds A is measure_zero of M) holds union T is measure_zero of M; theorem :: MEASURE2:15 for S being SigmaField of X, M being sigma_Measure of S, T being N_Measure_fam of S st (ex A being set st A in T & A is measure_zero of M) holds meet T is measure_zero of M; theorem :: MEASURE2:16 for S being SigmaField of X, M being sigma_Measure of S, T being N_Measure_fam of S st (for A being set st A in T holds A is measure_zero of M) holds meet T is measure_zero of M; definition let X be set; let S be SigmaField of X; let IT be N_Measure_fam of S; attr IT is non-decreasing means :: MEASURE2:def 2 ex F being sequence of S st IT = rng F & for n being Nat holds F.n c= F.(n+1); end; registration let X be set; let S be SigmaField of X; cluster non-decreasing for N_Measure_fam of S; end; definition let X be set; let S be SigmaField of X; let IT be N_Measure_fam of S; attr IT is non-increasing means :: MEASURE2:def 3 ex F being sequence of S st IT = rng F & for n being Element of NAT holds F.(n+1) c= F.n; end; registration let X be set; let S be SigmaField of X; cluster non-increasing for N_Measure_fam of S; end; theorem :: MEASURE2:17 for S being SigmaField of X, N,F being sequence of S holds (F.0 = {} & for n being Nat holds F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n ) implies rng F is non-decreasing N_Measure_fam of S; theorem :: MEASURE2:18 for N being Function st (for n being Nat holds N.n c= N.(n+1)) holds for m,n being Nat st n <= m holds N.n c= N.m; theorem :: MEASURE2:19 for N,F being Function st (F.0 = N.0 & for n being Nat holds F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1)) for n,m being Nat st n < m holds F.n misses F.m; theorem :: MEASURE2:20 for S being SigmaField of X, N,F being sequence of S holds ( F.0 = N.0 & for n being Nat holds F.(n+1) = N.(n+1) \ N.n & N.n c= N .(n+1) ) implies union rng F = union rng N; theorem :: MEASURE2:21 for S being SigmaField of X, N,F being sequence of S holds ( F.0 = N.0 & for n being Nat holds F.(n+1) = N.(n+1) \ N.n & N.n c= N .(n+1) ) implies F is Sep_Sequence of S; theorem :: MEASURE2:22 for S being SigmaField of X, N,F being sequence of S holds (F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1) ) implies (N.0 = F.0 & for n being Element of NAT holds N.(n+1) = F.(n+1) \/ N. n); theorem :: MEASURE2:23 for S being SigmaField of X, M being sigma_Measure of S, F being sequence of S st (for n being Nat holds F.n c= F.(n+1)) holds M. (union rng F) = sup(rng (M*F));