:: The Hopf Extension Theorem of Measure
:: by Noboru Endou , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received April 7, 2009
:: Copyright (c) 2009 Association of Mizar Users
theorem Lem12: :: MEASURE8:1
theorem Lem12a: :: MEASURE8:2
theorem MEASURE74: :: MEASURE8:3
:: deftheorem Def1 defines FinSequence MEASURE8:def 1 :
:: deftheorem DDef4 defines Set_Sequence MEASURE8:def 2 :
:: deftheorem Def2 defines Covering MEASURE8:def 3 :
Lm:
for X being set
for F being Field_Subset of X holds NAT --> X is Set_Sequence of F
:: deftheorem Def3 defines Covering MEASURE8:def 4 :
:: deftheorem Def4 defines vol MEASURE8:def 5 :
theorem Th13: :: MEASURE8:4
:: deftheorem Def7 defines Volume MEASURE8:def 6 :
theorem Th14: :: MEASURE8:5
definition
let X be
set ;
let F be
Field_Subset of
X;
let M be
Measure of
F;
let A be
Subset of
X;
func Svc M,
A -> Subset of
ExtREAL means :
Def8:
:: MEASURE8:def 7
for
x being
R_eal holds
(
x in it iff ex
CA being
Covering of
A,
F st
x = SUM (vol M,CA) );
existence
ex b1 being Subset of ExtREAL st
for x being R_eal holds
( x in b1 iff ex CA being Covering of A,F st x = SUM (vol M,CA) )
uniqueness
for b1, b2 being Subset of ExtREAL st ( for x being R_eal holds
( x in b1 iff ex CA being Covering of A,F st x = SUM (vol M,CA) ) ) & ( for x being R_eal holds
( x in b2 iff ex CA being Covering of A,F st x = SUM (vol M,CA) ) ) holds
b1 = b2
end;
:: deftheorem Def8 defines Svc MEASURE8:def 7 :
:: deftheorem Def10 defines C_Meas MEASURE8:def 8 :
:: deftheorem defines InvPairFunc MEASURE8:def 9 :
:: deftheorem Def13 defines On MEASURE8:def 10 :
theorem Th15x: :: MEASURE8:6
theorem Th16: :: MEASURE8:7
theorem Lm05: :: MEASURE8:8
theorem M8Th5: :: MEASURE8:9
theorem M8Th6: :: MEASURE8:10
theorem M8Th7: :: MEASURE8:11
theorem M8Th8: :: MEASURE8:12
Lem03:
for X being set
for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds
(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
theorem M8Th9: :: MEASURE8:13
theorem Th51a: :: MEASURE8:14
:: deftheorem Def3 defines completely-additive MEASURE8:def 11 :
theorem Lem06: :: MEASURE8:15
theorem Lem07: :: MEASURE8:16
theorem Lem08: :: MEASURE8:17
theorem Th51b: :: MEASURE8:18
theorem Lem09: :: MEASURE8:19
theorem Th52: :: MEASURE8:20
theorem PROB162a: :: MEASURE8:21
theorem PROB162: :: MEASURE8:22
theorem Lem11: :: MEASURE8:23
theorem Th53: :: MEASURE8:24
theorem :: MEASURE8:25
theorem Th62a: :: MEASURE8:26
theorem :: MEASURE8:27
theorem :: MEASURE8:28
theorem Lem14: :: MEASURE8:29
theorem Lem15: :: MEASURE8:30
theorem :: MEASURE8:31
:: deftheorem DDef2 defines is_extension_of MEASURE8:def 12 :
theorem :: MEASURE8:32
theorem Th91b: :: MEASURE8:33
theorem Lem10: :: MEASURE8:34
theorem :: MEASURE8:35