:: Several Properties of the $\sigma$-additive Measure
:: by J\'ozef Bia{\l}as
::
:: Received July 3, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users
begin
theorem
:: MEASURE2:1
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
F
being
Function
of
NAT
,
S
holds
M
*
F
is
V86
()
by
MEASURE1:25
;
definition
let
X
be
set
;
let
S
be
SigmaField
of
X
;
mode
N_Measure_fam
of
S
->
N_Sub_set_fam
of
X
means
:
Def1
:
:: MEASURE2:def 1
it
c=
S
;
existence
ex
b
1
being
N_Sub_set_fam
of
X
st
b
1
c=
S
proof
end;
end;
::
deftheorem
Def1
defines
N_Measure_fam
MEASURE2:def 1 :
for
X
being
set
for
S
being
SigmaField
of
X
for
b
3
being
N_Sub_set_fam
of
X
holds
(
b
3
is
N_Measure_fam
of
S
iff
b
3
c=
S
);
theorem
Th2
:
:: MEASURE2:2
for
X
being
set
for
S
being
SigmaField
of
X
for
T
being
N_Measure_fam
of
S
holds
(
meet
T
in
S
&
union
T
in
S
)
proof
end;
definition
let
X
be
set
;
let
S
be
SigmaField
of
X
;
let
T
be
N_Measure_fam
of
S
;
:: original:
meet
redefine
func
meet
T
->
Element
of
S
;
coherence
meet
T
is
Element
of
S
by
Th2
;
:: original:
union
redefine
func
union
T
->
Element
of
S
;
coherence
union
T
is
Element
of
S
by
Th2
;
end;
theorem
Th3
:
:: MEASURE2:3
for
X
being
set
for
S
being
SigmaField
of
X
for
N
being
Function
of
NAT
,
S
ex
F
being
Function
of
NAT
,
S
st
(
F
.
0
=
N
.
0
& ( for
n
being
Element
of
NAT
holds
F
.
(
n
+
1
)
=
(
N
.
(
n
+
1
)
)
\
(
N
.
n
)
) )
proof
end;
theorem
Th4
:
:: MEASURE2:4
for
X
being
set
for
S
being
SigmaField
of
X
for
N
being
Function
of
NAT
,
S
ex
F
being
Function
of
NAT
,
S
st
(
F
.
0
=
N
.
0
& ( for
n
being
Element
of
NAT
holds
F
.
(
n
+
1
)
=
(
N
.
(
n
+
1
)
)
\/
(
F
.
n
)
) )
proof
end;
theorem
Th5
:
:: MEASURE2:5
for
X
being
set
for
S
being non
empty
Subset-Family
of
X
for
N
,
F
being
Function
of
NAT
,
S
st
F
.
0
=
N
.
0
& ( for
n
being
Element
of
NAT
holds
F
.
(
n
+
1
)
=
(
N
.
(
n
+
1
)
)
\/
(
F
.
n
)
) holds
for
r
being
set
for
n
being
Element
of
NAT
holds
(
r
in
F
.
n
iff ex
k
being
Element
of
NAT
st
(
k
<=
n
&
r
in
N
.
k
) )
proof
end;
theorem
Th6
:
:: MEASURE2:6
for
X
being
set
for
S
being non
empty
Subset-Family
of
X
for
N
,
F
being
Function
of
NAT
,
S
st
F
.
0
=
N
.
0
& ( for
n
being
Element
of
NAT
holds
F
.
(
n
+
1
)
=
(
N
.
(
n
+
1
)
)
\/
(
F
.
n
)
) holds
for
n
,
m
being
Element
of
NAT
st
n
<
m
holds
F
.
n
c=
F
.
m
proof
end;
theorem
Th7
:
:: MEASURE2:7
for
X
being
set
for
S
being non
empty
Subset-Family
of
X
for
N
,
G
,
F
being
Function
of
NAT
,
S
st
G
.
0
=
N
.
0
& ( for
n
being
Element
of
NAT
holds
G
.
(
n
+
1
)
=
(
N
.
(
n
+
1
)
)
\/
(
G
.
n
)
) &
F
.
0
=
N
.
0
& ( for
n
being
Element
of
NAT
holds
F
.
(
n
+
1
)
=
(
N
.
(
n
+
1
)
)
\
(
G
.
n
)
) holds
for
n
,
m
being
Element
of
NAT
st
n
<=
m
holds
F
.
n
c=
G
.
m
proof
end;
theorem
Th8
:
:: MEASURE2:8
for
X
being
set
for
S
being
SigmaField
of
X
for
N
,
G
being
Function
of
NAT
,
S
ex
F
being
Function
of
NAT
,
S
st
(
F
.
0
=
N
.
0
& ( for
n
being
Element
of
NAT
holds
F
.
(
n
+
1
)
=
(
N
.
(
n
+
1
)
)
\
(
G
.
n
)
) )
proof
end;
theorem
:: MEASURE2:9
for
X
being
set
for
S
being
SigmaField
of
X
for
N
being
Function
of
NAT
,
S
ex
F
being
Function
of
NAT
,
S
st
(
F
.
0
=
{}
& ( for
n
being
Element
of
NAT
holds
F
.
(
n
+
1
)
=
(
N
.
0
)
\
(
N
.
n
)
) )
proof
end;
theorem
Th10
:
:: MEASURE2:10
for
X
being
set
for
S
being
SigmaField
of
X
for
N
,
G
,
F
being
Function
of
NAT
,
S
st
G
.
0
=
N
.
0
& ( for
n
being
Element
of
NAT
holds
G
.
(
n
+
1
)
=
(
N
.
(
n
+
1
)
)
\/
(
G
.
n
)
) &
F
.
0
=
N
.
0
& ( for
n
being
Element
of
NAT
holds
F
.
(
n
+
1
)
=
(
N
.
(
n
+
1
)
)
\
(
G
.
n
)
) holds
for
n
,
m
being
Element
of
NAT
st
n
<
m
holds
F
.
n
misses
F
.
m
proof
end;
theorem
Th11
:
:: MEASURE2:11
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
T
being
N_Measure_fam
of
S
for
F
being
Function
of
NAT
,
S
st
T
=
rng
F
holds
M
.
(
union
T
)
<=
SUM
(
M
*
F
)
proof
end;
theorem
Th12
:
:: MEASURE2:12
for
X
being
set
for
S
being
SigmaField
of
X
for
T
being
N_Measure_fam
of
S
ex
F
being
Function
of
NAT
,
S
st
T
=
rng
F
proof
end;
theorem
Th13
:
:: MEASURE2:13
for
N
,
F
being
Function
st
F
.
0
=
{}
& ( for
n
being
Element
of
NAT
holds
(
F
.
(
n
+
1
)
=
(
N
.
0
)
\
(
N
.
n
)
&
N
.
(
n
+
1
)
c=
N
.
n
) ) holds
for
n
being
Element
of
NAT
holds
F
.
n
c=
F
.
(
n
+
1
)
proof
end;
theorem
:: MEASURE2:14
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
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
proof
end;
theorem
:: MEASURE2:15
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
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
by
MEASURE1:36
,
SETFAM_1:3
;
theorem
:: MEASURE2:16
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
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
proof
end;
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
:
Def2
:
:: MEASURE2:def 2
ex
F
being
Function
of
NAT
,
S
st
(
IT
=
rng
F
& ( for
n
being
Element
of
NAT
holds
F
.
n
c=
F
.
(
n
+
1
)
) );
end;
::
deftheorem
Def2
defines
non-decreasing
MEASURE2:def 2 :
for
X
being
set
for
S
being
SigmaField
of
X
for
IT
being
N_Measure_fam
of
S
holds
(
IT
is
non-decreasing
iff ex
F
being
Function
of
NAT
,
S
st
(
IT
=
rng
F
& ( for
n
being
Element
of
NAT
holds
F
.
n
c=
F
.
(
n
+
1
)
) ) );
registration
let
X
be
set
;
let
S
be
SigmaField
of
X
;
cluster
non
empty
V46
()
non-decreasing
for
N_Measure_fam
of
S
;
existence
ex
b
1
being
N_Measure_fam
of
S
st
b
1
is
non-decreasing
proof
end;
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
Function
of
NAT
,
S
st
(
IT
=
rng
F
& ( for
n
being
Element
of
NAT
holds
F
.
(
n
+
1
)
c=
F
.
n
) );
end;
::
deftheorem
defines
non-increasing
MEASURE2:def 3 :
for
X
being
set
for
S
being
SigmaField
of
X
for
IT
being
N_Measure_fam
of
S
holds
(
IT
is
non-increasing
iff ex
F
being
Function
of
NAT
,
S
st
(
IT
=
rng
F
& ( for
n
being
Element
of
NAT
holds
F
.
(
n
+
1
)
c=
F
.
n
) ) );
registration
let
X
be
set
;
let
S
be
SigmaField
of
X
;
cluster
non
empty
V46
()
non-increasing
for
N_Measure_fam
of
S
;
existence
ex
b
1
being
N_Measure_fam
of
S
st
b
1
is
non-increasing
proof
end;
end;
theorem
:: MEASURE2:17
for
X
being
set
for
S
being
SigmaField
of
X
for
N
,
F
being
Function
of
NAT
,
S
st
F
.
0
=
{}
& ( for
n
being
Element
of
NAT
holds
(
F
.
(
n
+
1
)
=
(
N
.
0
)
\
(
N
.
n
)
&
N
.
(
n
+
1
)
c=
N
.
n
) ) holds
rng
F
is
non-decreasing
N_Measure_fam
of
S
proof
end;
theorem
Th18
:
:: MEASURE2:18
for
N
being
Function
st ( for
n
being
Element
of
NAT
holds
N
.
n
c=
N
.
(
n
+
1
)
) holds
for
m
,
n
being
Element
of
NAT
st
n
<=
m
holds
N
.
n
c=
N
.
m
proof
end;
theorem
Th19
:
:: MEASURE2:19
for
N
,
F
being
Function
st
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
)
) ) holds
for
n
,
m
being
Element
of
NAT
st
n
<
m
holds
F
.
n
misses
F
.
m
proof
end;
theorem
Th20
:
:: MEASURE2:20
for
X
being
set
for
S
being
SigmaField
of
X
for
N
,
F
being
Function
of
NAT
,
S
st
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
)
) ) holds
union
(
rng
F
)
=
union
(
rng
N
)
proof
end;
theorem
Th21
:
:: MEASURE2:21
for
X
being
set
for
S
being
SigmaField
of
X
for
N
,
F
being
Function
of
NAT
,
S
st
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
)
) ) holds
F
is
Sep_Sequence
of
S
proof
end;
theorem
:: MEASURE2:22
for
X
being
set
for
S
being
SigmaField
of
X
for
N
,
F
being
Function
of
NAT
,
S
st
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
)
) ) holds
(
N
.
0
=
F
.
0
& ( for
n
being
Element
of
NAT
holds
N
.
(
n
+
1
)
=
(
F
.
(
n
+
1
)
)
\/
(
N
.
n
)
) )
proof
end;
theorem
:: MEASURE2:23
for
X
being
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
F
being
Function
of
NAT
,
S
st ( for
n
being
Element
of
NAT
holds
F
.
n
c=
F
.
(
n
+
1
)
) holds
M
.
(
union
(
rng
F
)
)
=
sup
(
rng
(
M
*
F
)
)
proof
end;