:: The $\sigma$-additive Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received October 15, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
begin
theorem
Th1
:
:: MEASURE1:1
for
X
,
Y
being
set
holds
union
{
X
,
Y
,
{}
}
=
union
{
X
,
Y
}
proof
end;
theorem
:: MEASURE1:2
for
X
being
set
for
A
,
B
being
Subset
of
X
holds
{
A
,
B
}
is
Subset-Family
of
X
proof
end;
theorem
:: MEASURE1:3
for
X
being
set
for
A
,
B
,
C
being
Subset
of
X
holds
{
A
,
B
,
C
}
is
Subset-Family
of
X
proof
end;
scheme
:: MEASURE1:sch 1
DomsetFamEx
{
F
1
()
->
set
,
P
1
[
set
] } :
ex
F
being non
empty
Subset-Family
of
F
1
() st
for
B
being
set
holds
(
B
in
F
iff (
B
c=
F
1
() &
P
1
[
B
] ) )
provided
A1
: ex
B
being
set
st
(
B
c=
F
1
() &
P
1
[
B
] )
proof
end;
notation
let
X
be
set
;
let
S
be non
empty
Subset-Family
of
X
;
synonym
X
\
S
for
COMPLEMENT
S
;
end;
registration
let
X
be
set
;
let
S
be non
empty
Subset-Family
of
X
;
cluster
X
\
S
->
non
empty
;
coherence
not
X
\
S
is
empty
proof
end;
end;
theorem
Th4
:
:: MEASURE1:4
for
X
being
set
for
S
being non
empty
Subset-Family
of
X
holds
(
meet
S
=
X
\
(
union
(
X
\
S
)
)
&
union
S
=
X
\
(
meet
(
X
\
S
)
)
)
proof
end;
::
:: Field Subset of X and nonnegative measure
::
definition
let
X
be
set
;
let
IT
be
Subset-Family
of
X
;
redefine
attr
IT
is
compl-closed
means
:
Def1
:
:: MEASURE1:def 1
for
A
being
set
st
A
in
IT
holds
X
\
A
in
IT
;
compatibility
(
IT
is
compl-closed
iff for
A
being
set
st
A
in
IT
holds
X
\
A
in
IT
)
proof
end;
end;
::
deftheorem
Def1
defines
compl-closed
MEASURE1:def 1 :
for
X
being
set
for
IT
being
Subset-Family
of
X
holds
(
IT
is
compl-closed
iff for
A
being
set
st
A
in
IT
holds
X
\
A
in
IT
);
registration
let
X
be
set
;
cluster
cup-closed
compl-closed
->
cap-closed
for
Element
of
bool
(
bool
X
)
;
coherence
for
b
1
being
Subset-Family
of
X
st
b
1
is
cup-closed
&
b
1
is
compl-closed
holds
b
1
is
cap-closed
proof
end;
cluster
cap-closed
compl-closed
->
cup-closed
for
Element
of
bool
(
bool
X
)
;
coherence
for
b
1
being
Subset-Family
of
X
st
b
1
is
cap-closed
&
b
1
is
compl-closed
holds
b
1
is
cup-closed
proof
end;
end;
theorem
:: MEASURE1:5
for
X
being
set
for
S
being
Field_Subset
of
X
holds
S
=
X
\
S
proof
end;
registration
let
X
be
set
;
cluster
cap-closed
compl-closed
->
diff-closed
for
Element
of
bool
(
bool
X
)
;
coherence
for
b
1
being
Subset-Family
of
X
st
b
1
is
compl-closed
&
b
1
is
cap-closed
holds
b
1
is
diff-closed
proof
end;
end;
theorem
:: MEASURE1:6
for
X
being
set
for
S
being
Field_Subset
of
X
for
A
,
B
being
set
st
A
in
S
&
B
in
S
holds
A
\
B
in
S
by
FINSUB_1:def 3
;
theorem
:: MEASURE1:7
for
X
being
set
for
S
being
Field_Subset
of
X
holds
(
{}
in
S
&
X
in
S
)
by
PROB_1:4
,
PROB_1:5
;
definition
let
X
be non
empty
set
;
let
F
be
Function
of
X
,
ExtREAL
;
:: original:
nonnegative
redefine
attr
F
is
nonnegative
means
:
Def2
:
:: MEASURE1:def 2
for
A
being
Element
of
X
holds
0.
<=
F
.
A
;
compatibility
(
F
is
nonnegative
iff for
A
being
Element
of
X
holds
0.
<=
F
.
A
)
by
SUPINF_2:39
;
end;
::
deftheorem
Def2
defines
nonnegative
MEASURE1:def 2 :
for
X
being non
empty
set
for
F
being
Function
of
X
,
ExtREAL
holds
(
F
is
nonnegative
iff for
A
being
Element
of
X
holds
0.
<=
F
.
A
);
definition
let
X
be
set
;
let
S
be
Field_Subset
of
X
;
let
F
be
Function
of
S
,
ExtREAL
;
attr
F
is
additive
means
:
Def3
:
:: MEASURE1:def 3
for
A
,
B
being
Element
of
S
st
A
misses
B
holds
F
.
(
A
\/
B
)
=
(
F
.
A
)
+
(
F
.
B
)
;
end;
::
deftheorem
Def3
defines
additive
MEASURE1:def 3 :
for
X
being
set
for
S
being
Field_Subset
of
X
for
F
being
Function
of
S
,
ExtREAL
holds
(
F
is
additive
iff for
A
,
B
being
Element
of
S
st
A
misses
B
holds
F
.
(
A
\/
B
)
=
(
F
.
A
)
+
(
F
.
B
)
);
registration
let
X
be
set
;
let
S
be
Field_Subset
of
X
;
cluster
Relation-like
S
-defined
ExtREAL
-valued
Function-like
non
empty
V14
(
S
)
V18
(
S
,
ExtREAL
)
ext-real-valued
zeroed
V89
()
additive
for
Element
of
bool
[:
S
,
ExtREAL
:]
;
existence
ex
b
1
being
Function
of
S
,
ExtREAL
st
(
b
1
is
V89
() &
b
1
is
additive
&
b
1
is
zeroed
)
proof
end;
end;
definition
let
X
be
set
;
let
S
be
Field_Subset
of
X
;
mode
Measure of
S
is
zeroed
V89
()
additive
Function
of
S
,
ExtREAL
;
end;
theorem
Th8
:
:: MEASURE1:8
for
X
being
set
for
S
being
Field_Subset
of
X
for
M
being
Measure
of
S
for
A
,
B
being
Element
of
S
st
A
c=
B
holds
M
.
A
<=
M
.
B
proof
end;
theorem
Th9
:
:: MEASURE1:9
for
X
being
set
for
S
being
Field_Subset
of
X
for
M
being
Measure
of
S
for
A
,
B
being
Element
of
S
st
A
c=
B
&
M
.
A
<
+infty
holds
M
.
(
B
\
A
)
=
(
M
.
B
)
-
(
M
.
A
)
proof
end;
registration
let
X
be
set
;
cluster
non
empty
cap-closed
compl-closed
for
Element
of
bool
(
bool
X
)
;
existence
ex
b
1
being
Subset-Family
of
X
st
( not
b
1
is
empty
&
b
1
is
compl-closed
&
b
1
is
cap-closed
)
proof
end;
end;
definition
let
X
be
set
;
let
S
be non
empty
cup-closed
Subset-Family
of
X
;
let
A
,
B
be
Element
of
S
;
:: original:
\/
redefine
func
A
\/
B
->
Element
of
S
;
coherence
A
\/
B
is
Element
of
S
by
FINSUB_1:def 1
;
end;
definition
let
X
be
set
;
let
S
be
Field_Subset
of
X
;
let
A
,
B
be
Element
of
S
;
:: original:
/\
redefine
func
A
/\
B
->
Element
of
S
;
coherence
A
/\
B
is
Element
of
S
by
FINSUB_1:def 2
;
:: original:
\
redefine
func
A
\
B
->
Element
of
S
;
coherence
A
\
B
is
Element
of
S
by
FINSUB_1:def 3
;
end;
theorem
Th10
:
:: MEASURE1:10
for
X
being
set
for
S
being
Field_Subset
of
X
for
M
being
Measure
of
S
for
A
,
B
being
Element
of
S
holds
M
.
(
A
\/
B
)
<=
(
M
.
A
)
+
(
M
.
B
)
proof
end;
theorem
:: MEASURE1:11
for
X
being
set
for
S
being
Field_Subset
of
X
for
M
being
Measure
of
S
holds
(
{}
in
S
&
X
in
S
& ( for
A
,
B
being
set
st
A
in
S
&
B
in
S
holds
(
X
\
A
in
S
&
A
\/
B
in
S
&
A
/\
B
in
S
) ) )
by
Def1
,
FINSUB_1:def 1
,
FINSUB_1:def 2
,
PROB_1:4
,
PROB_1:5
;
definition
let
X
be
set
;
let
S
be
Field_Subset
of
X
;
let
M
be
Measure
of
S
;
mode
measure_zero
of
M
->
Element
of
S
means
:
Def4
:
:: MEASURE1:def 4
M
.
it
=
0.
;
existence
ex
b
1
being
Element
of
S
st
M
.
b
1
=
0.
proof
end;
end;
::
deftheorem
Def4
defines
measure_zero
MEASURE1:def 4 :
for
X
being
set
for
S
being
Field_Subset
of
X
for
M
being
Measure
of
S
for
b
4
being
Element
of
S
holds
(
b
4
is
measure_zero
of
M
iff
M
.
b
4
=
0.
);
theorem
:: MEASURE1:12
for
X
being
set
for
S
being
Field_Subset
of
X
for
M
being
Measure
of
S
for
A
being
Element
of
S
for
B
being
measure_zero
of
M
st
A
c=
B
holds
A
is
measure_zero
of
M
proof
end;
theorem
:: MEASURE1:13
for
X
being
set
for
S
being
Field_Subset
of
X
for
M
being
Measure
of
S
for
A
,
B
being
measure_zero
of
M
holds
(
A
\/
B
is
measure_zero
of
M
&
A
/\
B
is
measure_zero
of
M
&
A
\
B
is
measure_zero
of
M
)
proof
end;
theorem
:: MEASURE1:14
for
X
being
set
for
S
being
Field_Subset
of
X
for
M
being
Measure
of
S
for
A
being
Element
of
S
for
B
being
measure_zero
of
M
holds
(
M
.
(
A
\/
B
)
=
M
.
A
&
M
.
(
A
/\
B
)
=
0.
&
M
.
(
A
\
B
)
=
M
.
A
)
proof
end;
::
:: sigma_Field Subset of X and sigma_additive nonnegative measure
::
theorem
Th15
:
:: MEASURE1:15
for
X
being
set
for
A
being
Subset
of
X
ex
F
being
Function
of
NAT
,
(
bool
X
)
st
rng
F
=
{
A
}
proof
end;
theorem
Th16
:
:: MEASURE1:16
for
A
being
set
ex
F
being
Function
of
NAT
,
{
A
}
st
for
n
being
Element
of
NAT
holds
F
.
n
=
A
proof
end;
registration
let
X
be
set
;
cluster
non
empty
V53
() for
Element
of
bool
(
bool
X
)
;
existence
ex
b
1
being
Subset-Family
of
X
st
( not
b
1
is
empty
&
b
1
is
V53
() )
proof
end;
end;
definition
let
X
be
set
;
mode
N_Sub_set_fam of
X
is
non
empty
V53
()
Subset-Family
of
X
;
end;
theorem
Th17
:
:: MEASURE1:17
for
X
being
set
for
A
,
B
,
C
being
Subset
of
X
ex
F
being
Function
of
NAT
,
(
bool
X
)
st
(
rng
F
=
{
A
,
B
,
C
}
&
F
.
0
=
A
&
F
.
1
=
B
& ( for
n
being
Element
of
NAT
st 1
<
n
holds
F
.
n
=
C
) )
proof
end;
theorem
:: MEASURE1:18
for
X
being
set
for
A
,
B
being
Subset
of
X
holds
{
A
,
B
,
{}
}
is
N_Sub_set_fam
of
X
proof
end;
theorem
Th19
:
:: MEASURE1:19
for
X
being
set
for
A
,
B
being
Subset
of
X
ex
F
being
Function
of
NAT
,
(
bool
X
)
st
(
rng
F
=
{
A
,
B
}
&
F
.
0
=
A
& ( for
n
being
Element
of
NAT
st
0
<
n
holds
F
.
n
=
B
) )
proof
end;
theorem
:: MEASURE1:20
for
X
being
set
for
A
,
B
being
Subset
of
X
holds
{
A
,
B
}
is
N_Sub_set_fam
of
X
proof
end;
theorem
Th21
:
:: MEASURE1:21
for
X
being
set
for
S
being
N_Sub_set_fam
of
X
holds
X
\
S
is
N_Sub_set_fam
of
X
proof
end;
definition
let
X
be
set
;
let
IT
be
Subset-Family
of
X
;
attr
IT
is
sigma-additive
means
:
Def5
:
:: MEASURE1:def 5
for
M
being
N_Sub_set_fam
of
X
st
M
c=
IT
holds
union
M
in
IT
;
end;
::
deftheorem
Def5
defines
sigma-additive
MEASURE1:def 5 :
for
X
being
set
for
IT
being
Subset-Family
of
X
holds
(
IT
is
sigma-additive
iff for
M
being
N_Sub_set_fam
of
X
st
M
c=
IT
holds
union
M
in
IT
);
registration
let
X
be
set
;
cluster
non
empty
compl-closed
sigma-additive
for
Element
of
bool
(
bool
X
)
;
existence
ex
b
1
being
Subset-Family
of
X
st
( not
b
1
is
empty
&
b
1
is
compl-closed
&
b
1
is
sigma-additive
)
proof
end;
end;
registration
let
X
be
set
;
cluster
compl-closed
sigma-multiplicative
->
sigma-additive
for
Element
of
bool
(
bool
X
)
;
coherence
for
b
1
being
Subset-Family
of
X
st
b
1
is
compl-closed
&
b
1
is
sigma-multiplicative
holds
b
1
is
sigma-additive
proof
end;
cluster
compl-closed
sigma-additive
->
sigma-multiplicative
for
Element
of
bool
(
bool
X
)
;
coherence
for
b
1
being
Subset-Family
of
X
st
b
1
is
compl-closed
&
b
1
is
sigma-additive
holds
b
1
is
sigma-multiplicative
proof
end;
end;
registration
let
X
be
set
;
cluster
non
empty
compl-closed
sigma-multiplicative
->
for
Element
of
bool
(
bool
X
)
;
coherence
for
b
1
being
SigmaField
of
X
holds not
b
1
is
empty
;
end;
theorem
Th22
:
:: MEASURE1:22
for
X
being
set
for
S
being non
empty
Subset-Family
of
X
holds
( ( ( for
A
being
set
st
A
in
S
holds
X
\
A
in
S
) & ( for
M
being
N_Sub_set_fam
of
X
st
M
c=
S
holds
meet
M
in
S
) ) iff
S
is
SigmaField
of
X
)
proof
end;
registration
let
X
be
set
;
let
S
be
SigmaField
of
X
;
cluster
Relation-like
NAT
-defined
S
-valued
Function-like
non
empty
V14
(
NAT
)
V18
(
NAT
,
S
)
disjoint_valued
for
Element
of
bool
[:
NAT
,
S
:]
;
existence
ex
b
1
being
Function
of
NAT
,
S
st
b
1
is
disjoint_valued
proof
end;
end;
definition
let
X
be
set
;
let
S
be
SigmaField
of
X
;
mode
Sep_Sequence of
S
is
disjoint_valued
Function
of
NAT
,
S
;
end;
definition
let
X
be
set
;
let
S
be
SigmaField
of
X
;
let
F
be
Function
of
NAT
,
S
;
:: original:
rng
redefine
func
rng
F
->
non
empty
Subset-Family
of
X
;
coherence
rng
F
is non
empty
Subset-Family
of
X
proof
end;
end;
theorem
Th23
:
:: MEASURE1:23
for
X
being
set
for
S
being
SigmaField
of
X
for
F
being
Function
of
NAT
,
S
holds
rng
F
is
N_Sub_set_fam
of
X
proof
end;
theorem
Th24
:
:: MEASURE1:24
for
X
being
set
for
S
being
SigmaField
of
X
for
F
being
Function
of
NAT
,
S
holds
union
(
rng
F
)
is
Element
of
S
proof
end;
theorem
Th25
:
:: MEASURE1:25
for
Y
,
S
being non
empty
set
for
F
being
Function
of
Y
,
S
for
M
being
Function
of
S
,
ExtREAL
st
M
is
V89
() holds
M
*
F
is
V89
()
proof
end;
theorem
Th26
:
:: MEASURE1:26
for
X
being
set
for
S
being
SigmaField
of
X
for
a
,
b
being
R_eal
ex
M
being
Function
of
S
,
ExtREAL
st
for
A
being
Element
of
S
holds
( (
A
=
{}
implies
M
.
A
=
a
) & (
A
<>
{}
implies
M
.
A
=
b
) )
proof
end;
theorem
:: MEASURE1:27
for
X
being
set
for
S
being
SigmaField
of
X
ex
M
being
Function
of
S
,
ExtREAL
st
for
A
being
Element
of
S
holds
( (
A
=
{}
implies
M
.
A
=
0.
) & (
A
<>
{}
implies
M
.
A
=
+infty
) )
by
Th26
;
theorem
Th28
:
:: MEASURE1:28
for
X
being
set
for
S
being
SigmaField
of
X
ex
M
being
Function
of
S
,
ExtREAL
st
for
A
being
Element
of
S
holds
M
.
A
=
0.
proof
end;
definition
let
X
be
set
;
let
S
be
SigmaField
of
X
;
let
F
be
Function
of
S
,
ExtREAL
;
attr
F
is
sigma-additive
means
:
Def6
:
:: MEASURE1:def 6
for
s
being
Sep_Sequence
of
S
holds
SUM
(
F
*
s
)
=
F
.
(
union
(
rng
s
)
)
;
end;
::
deftheorem
Def6
defines
sigma-additive
MEASURE1:def 6 :
for
X
being
set
for
S
being
SigmaField
of
X
for
F
being
Function
of
S
,
ExtREAL
holds
(
F
is
sigma-additive
iff for
s
being
Sep_Sequence
of
S
holds
SUM
(
F
*
s
)
=
F
.
(
union
(
rng
s
)
)
);
registration
let
X
be
set
;
let
S
be
SigmaField
of
X
;
cluster
Relation-like
S
-defined
ExtREAL
-valued
Function-like
non
empty
V14
(
S
)
V18
(
S
,
ExtREAL
)
ext-real-valued
zeroed
V89
()
sigma-additive
for
Element
of
bool
[:
S
,
ExtREAL
:]
;
existence
ex
b
1
being
Function
of
S
,
ExtREAL
st
(
b
1
is
V89
() &
b
1
is
sigma-additive
&
b
1
is
zeroed
)
proof
end;
end;
definition
let
X
be
set
;
let
S
be
SigmaField
of
X
;
mode
sigma_Measure of
S
is
zeroed
V89
()
sigma-additive
Function
of
S
,
ExtREAL
;
end;
registration
let
X
be
set
;
cluster
non
empty
compl-closed
sigma-additive
->
non
empty
cup-closed
for
Element
of
bool
(
bool
X
)
;
coherence
for
b
1
being non
empty
Subset-Family
of
X
st
b
1
is
sigma-additive
&
b
1
is
compl-closed
holds
b
1
is
cup-closed
;
end;
theorem
Th29
:
:: MEASURE1:29
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
holds
M
is
Measure
of
S
proof
end;
theorem
:: MEASURE1:30
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
A
,
B
being
Element
of
S
st
A
misses
B
holds
M
.
(
A
\/
B
)
=
(
M
.
A
)
+
(
M
.
B
)
proof
end;
theorem
Th31
:
:: MEASURE1:31
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
A
,
B
being
Element
of
S
st
A
c=
B
holds
M
.
A
<=
M
.
B
proof
end;
theorem
:: MEASURE1:32
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
A
,
B
being
Element
of
S
st
A
c=
B
&
M
.
A
<
+infty
holds
M
.
(
B
\
A
)
=
(
M
.
B
)
-
(
M
.
A
)
proof
end;
theorem
Th33
:
:: MEASURE1:33
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
A
,
B
being
Element
of
S
holds
M
.
(
A
\/
B
)
<=
(
M
.
A
)
+
(
M
.
B
)
proof
end;
theorem
:: MEASURE1:34
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
holds
(
{}
in
S
&
X
in
S
& ( for
A
,
B
being
set
st
A
in
S
&
B
in
S
holds
(
X
\
A
in
S
&
A
\/
B
in
S
&
A
/\
B
in
S
) ) )
by
Def1
,
FINSUB_1:def 1
,
FINSUB_1:def 2
,
PROB_1:4
,
PROB_1:5
;
theorem
:: MEASURE1:35
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
T
being
N_Sub_set_fam
of
X
st ( for
A
being
set
st
A
in
T
holds
A
in
S
) holds
(
union
T
in
S
&
meet
T
in
S
)
proof
end;
definition
let
X
be
set
;
let
S
be
SigmaField
of
X
;
let
M
be
sigma_Measure
of
S
;
mode
measure_zero
of
M
->
Element
of
S
means
:
Def7
:
:: MEASURE1:def 7
M
.
it
=
0.
;
existence
ex
b
1
being
Element
of
S
st
M
.
b
1
=
0.
proof
end;
end;
::
deftheorem
Def7
defines
measure_zero
MEASURE1:def 7 :
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
b
4
being
Element
of
S
holds
(
b
4
is
measure_zero
of
M
iff
M
.
b
4
=
0.
);
theorem
:: MEASURE1:36
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
A
being
Element
of
S
for
B
being
measure_zero
of
M
st
A
c=
B
holds
A
is
measure_zero
of
M
proof
end;
theorem
:: MEASURE1:37
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
A
,
B
being
measure_zero
of
M
holds
(
A
\/
B
is
measure_zero
of
M
&
A
/\
B
is
measure_zero
of
M
&
A
\
B
is
measure_zero
of
M
)
proof
end;
theorem
:: MEASURE1:38
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
A
being
Element
of
S
for
B
being
measure_zero
of
M
holds
(
M
.
(
A
\/
B
)
=
M
.
A
&
M
.
(
A
/\
B
)
=
0.
&
M
.
(
A
\
B
)
=
M
.
A
)
proof
end;
:: Field Subset of X and nonnegative measure
::