:: Properties of Caratheodory's Measure :: by J\'ozef Bia{\l}as :: :: Received June 25, 1992 :: Copyright (c) 1992-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 NUMBERS, SUPINF_1, PROB_1, XBOOLE_0, SETFAM_1, FUNCT_1, SUBSET_1, TARSKI, RELAT_1, CARD_1, ARYTM_3, NAT_1, XXREAL_0, ZFMISC_1, MEASURE1, SUPINF_2, VALUED_0, FUNCOP_1, XREAL_0, ARYTM_1, MEASURE3, MEASURE4, REWRITE1, MEASURE2; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XXREAL_0, XREAL_0, VALUED_0, XCMPLX_0, FUNCOP_1, REAL_1, NAT_1, SETFAM_1, PROB_1, SUPINF_1, SUPINF_2, MEASURE1, MEASURE2, MEASURE3; constructors ENUMSET1, PARTFUN1, REAL_1, NAT_1, PROB_2, MEASURE3, SUPINF_1, FUNCOP_1, RELSET_1, XREAL_0, MEASURE2; registrations SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEASURE1, VALUED_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Some theorems about R_eal numbers reserve A,B,X for set, S for SigmaField of X; theorem :: MEASURE4:1 for S being non empty Subset-Family of X, F, G being sequence of S, A being Element of S st for n being Element of NAT holds G.n = A /\ F.n holds union rng G = A /\ union rng F; theorem :: MEASURE4:2 for S being non empty Subset-Family of X for F, G being sequence of S st (G.0 = F.0 & for n being Nat holds G.(n+1) = F.(n+1) \/ G.n) holds for H being sequence of S st (H.0 = F.0 & for n being Nat holds H.(n+1) = F.(n+1) \ G.n) holds union rng F = union rng H; theorem :: MEASURE4:3 bool X is SigmaField of X; definition let X be set; mode C_Measure of X -> Function of bool X,ExtREAL means :: MEASURE4:def 1 it is nonnegative zeroed & for A,B being Subset of X st A c= B holds it.A <= it.B & for F being sequence of bool X holds it.(union rng F) <= SUM(it*F); end; reserve C for C_Measure of X; definition let X be set; let C be C_Measure of X; func sigma_Field(C) -> non empty Subset-Family of X means :: MEASURE4:def 2 for A being Subset of X holds (A in it iff for W,Z being Subset of X holds (W c= A & Z c= X \ A implies C.W + C.Z <= C.(W \/ Z))); end; theorem :: MEASURE4:4 for W,Z being Subset of X holds C.(W \/ Z) <= C.W + C.Z; theorem :: MEASURE4:5 for A being Subset of X holds (A in sigma_Field(C) iff for W,Z being Subset of X holds (W c= A & Z c= X \ A implies C.W + C.Z = C.(W \/ Z))) ; theorem :: MEASURE4:6 for W,Z being Subset of X holds W in sigma_Field(C) & Z misses W implies C.(W \/ Z) = C.W + C.Z; theorem :: MEASURE4:7 A in sigma_Field(C) implies X \ A in sigma_Field(C); theorem :: MEASURE4:8 A in sigma_Field(C) & B in sigma_Field(C) implies A \/ B in sigma_Field(C); theorem :: MEASURE4:9 A in sigma_Field(C) & B in sigma_Field(C) implies A /\ B in sigma_Field(C); theorem :: MEASURE4:10 A in sigma_Field(C) & B in sigma_Field(C) implies A \ B in sigma_Field(C); theorem :: MEASURE4:11 for N being sequence of S holds for A being Element of S holds ex F being sequence of S st for n being Element of NAT holds F.n = A /\ N.n; theorem :: MEASURE4:12 sigma_Field(C) is SigmaField of X; registration let X be set; let C be C_Measure of X; cluster sigma_Field(C) -> sigma-additive compl-closed non empty; end; definition let X be set; let S be SigmaField of X; let A be N_Measure_fam of S; redefine func union A -> Element of S; end; definition let X be set; let C be C_Measure of X; func sigma_Meas(C) -> Function of sigma_Field(C),ExtREAL means :: MEASURE4:def 3 for A being Subset of X st A in sigma_Field(C) holds it.A = C.A; end; theorem :: MEASURE4:13 sigma_Meas(C) is Measure of sigma_Field(C); ::$N Caratheodory's Theorem theorem :: MEASURE4:14 sigma_Meas(C) is sigma_Measure of sigma_Field(C); registration let X be set; let C be C_Measure of X; cluster sigma_Meas(C) -> nonnegative sigma-additive zeroed; end; theorem :: MEASURE4:15 for A being Subset of X holds C.A = 0. implies A in sigma_Field(C); theorem :: MEASURE4:16 sigma_Meas(C) is complete;