:: 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 Th1: :: MEASURE8:1
theorem Th2: :: MEASURE8:2
theorem Th3: :: MEASURE8:3
:: deftheorem Def1 defines FinSequence MEASURE8:def 1 :
:: deftheorem Def2 defines Set_Sequence MEASURE8:def 2 :
:: deftheorem Def3 defines Covering MEASURE8:def 3 :
Lm1:
for X being set
for F being Field_Subset of X holds NAT --> X is Set_Sequence of F
:: deftheorem Def4 defines Covering MEASURE8:def 4 :
:: deftheorem Def5 defines vol MEASURE8:def 5 :
theorem Th4: :: MEASURE8:4
:: deftheorem Def6 defines Volume MEASURE8:def 6 :
theorem Th5: :: 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 :
Def7:
:: 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 Def7 defines Svc MEASURE8:def 7 :
:: deftheorem Def8 defines C_Meas MEASURE8:def 8 :
:: deftheorem defines InvPairFunc MEASURE8:def 9 :
:: deftheorem Def10 defines On MEASURE8:def 10 :
theorem Th6: :: MEASURE8:6
theorem Th7: :: MEASURE8:7
theorem Th8: :: MEASURE8:8
theorem Th9: :: MEASURE8:9
theorem Th10: :: MEASURE8:10
theorem Th11: :: MEASURE8:11
theorem Th12: :: MEASURE8:12
Lm2:
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 Th13: :: MEASURE8:13
theorem Th14: :: MEASURE8:14
:: deftheorem Def11 defines completely-additive MEASURE8:def 11 :
theorem Th15: :: MEASURE8:15
theorem Th16: :: MEASURE8:16
theorem Th17: :: MEASURE8:17
theorem Th18: :: MEASURE8:18
theorem Th19: :: MEASURE8:19
theorem Th20: :: MEASURE8:20
theorem Th21: :: MEASURE8:21
theorem Th22: :: MEASURE8:22
theorem Th23: :: MEASURE8:23
theorem Th24: :: MEASURE8:24
theorem :: MEASURE8:25
theorem Th26: :: MEASURE8:26
theorem :: MEASURE8:27
theorem :: MEASURE8:28
theorem Th29: :: MEASURE8:29
theorem Th30: :: MEASURE8:30
theorem :: MEASURE8:31
:: deftheorem Def12 defines is_extension_of MEASURE8:def 12 :
theorem :: MEASURE8:32
theorem Th33: :: MEASURE8:33
theorem Th34: :: MEASURE8:34
theorem :: MEASURE8:35