:: Definitions and Basic Properties of Measurable Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received September 7, 2000
:: Copyright (c) 2000 Association of Mizar Users
:: deftheorem Def1 defines INT- MESFUNC1:def 1 :
Lm1:
0 = - 0
;
theorem Th1: :: MESFUNC1:1
theorem Th2: :: MESFUNC1:2
theorem Th3: :: MESFUNC1:3
:: deftheorem Def2 defines RAT_with_denominator MESFUNC1:def 2 :
theorem Th4: :: MESFUNC1:4
theorem :: MESFUNC1:5
definition
let C be non
empty set ;
let f1,
f2 be
PartFunc of
C,
ExtREAL ;
deffunc H1(
Element of
C)
-> Element of
ExtREAL =
(f1 . $1) + (f2 . $1);
func f1 + f2 -> PartFunc of
C,
ExtREAL means :
Def3:
:: MESFUNC1:def 3
(
dom it = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty }) /\ (f2 " {+infty })) \/ ((f1 " {+infty }) /\ (f2 " {-infty }))) & ( for
c being
Element of
C st
c in dom it holds
it . c = (f1 . c) + (f2 . c) ) );
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty }) /\ (f2 " {+infty })) \/ ((f1 " {+infty }) /\ (f2 " {-infty }))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) )
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty }) /\ (f2 " {+infty })) \/ ((f1 " {+infty }) /\ (f2 " {-infty }))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) + (f2 . c) ) & dom b2 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty }) /\ (f2 " {+infty })) \/ ((f1 " {+infty }) /\ (f2 " {-infty }))) & ( for c being Element of C st c in dom b2 holds
b2 . c = (f1 . c) + (f2 . c) ) holds
b1 = b2
deffunc H2(
Element of
C)
-> Element of
ExtREAL =
(f1 . $1) - (f2 . $1);
func f1 - f2 -> PartFunc of
C,
ExtREAL means :: MESFUNC1:def 4
(
dom it = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty }))) & ( for
c being
Element of
C st
c in dom it holds
it . c = (f1 . c) - (f2 . c) ) );
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty }))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) - (f2 . c) ) )
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty }))) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) - (f2 . c) ) & dom b2 = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty }) /\ (f2 " {+infty })) \/ ((f1 " {-infty }) /\ (f2 " {-infty }))) & ( for c being Element of C st c in dom b2 holds
b2 . c = (f1 . c) - (f2 . c) ) holds
b1 = b2
deffunc H3(
Element of
C)
-> Element of
ExtREAL =
(f1 . $1) * (f2 . $1);
func f1 (#) f2 -> PartFunc of
C,
ExtREAL means :
Def5:
:: MESFUNC1:def 5
(
dom it = (dom f1) /\ (dom f2) & ( for
c being
Element of
C st
c in dom it holds
it . c = (f1 . c) * (f2 . c) ) );
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) )
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds
b1 . c = (f1 . c) * (f2 . c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b2 holds
b2 . c = (f1 . c) * (f2 . c) ) holds
b1 = b2
end;
:: deftheorem Def3 defines + MESFUNC1:def 3 :
:: deftheorem defines - MESFUNC1:def 4 :
:: deftheorem Def5 defines (#) MESFUNC1:def 5 :
:: deftheorem Def6 defines (#) MESFUNC1:def 6 :
theorem Th6: :: MESFUNC1:6
:: deftheorem defines - MESFUNC1:def 7 :
:: deftheorem defines 1. MESFUNC1:def 8 :
:: deftheorem Def9 defines / MESFUNC1:def 9 :
theorem :: MESFUNC1:7
:: deftheorem defines |. MESFUNC1:def 10 :
theorem :: MESFUNC1:8
canceled;
theorem Th9: :: MESFUNC1:9
theorem Th10: :: MESFUNC1:10
theorem Th11: :: MESFUNC1:11
theorem Th12: :: MESFUNC1:12
theorem Th13: :: MESFUNC1:13
theorem Th14: :: MESFUNC1:14
theorem Th15: :: MESFUNC1:15
theorem Th16: :: MESFUNC1:16
definition
canceled;let f be
ext-real-valued Function;
let a be
ext-real number ;
defpred S1[
set ]
means ( $1
in dom f &
f . $1
< a );
func less_dom f,
a -> set means :
Def12:
:: MESFUNC1:def 12
for
x being
set holds
(
x in it iff (
x in dom f &
f . x < a ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in dom f & f . x < a ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in dom f & f . x < a ) ) ) & ( for x being set holds
( x in b2 iff ( x in dom f & f . x < a ) ) ) holds
b1 = b2
defpred S2[
set ]
means ( $1
in dom f &
f . $1
<= a );
func less_eq_dom f,
a -> set means :
Def13:
:: MESFUNC1:def 13
for
x being
set holds
(
x in it iff (
x in dom f &
f . x <= a ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in dom f & f . x <= a ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in dom f & f . x <= a ) ) ) & ( for x being set holds
( x in b2 iff ( x in dom f & f . x <= a ) ) ) holds
b1 = b2
defpred S3[
set ]
means ( $1
in dom f &
a < f . $1 );
func great_dom f,
a -> set means :
Def14:
:: MESFUNC1:def 14
for
x being
set holds
(
x in it iff (
x in dom f &
a < f . x ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in dom f & a < f . x ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in dom f & a < f . x ) ) ) & ( for x being set holds
( x in b2 iff ( x in dom f & a < f . x ) ) ) holds
b1 = b2
defpred S4[
set ]
means ( $1
in dom f &
a <= f . $1 );
func great_eq_dom f,
a -> set means :
Def15:
:: MESFUNC1:def 15
for
x being
set holds
(
x in it iff (
x in dom f &
a <= f . x ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in dom f & a <= f . x ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in dom f & a <= f . x ) ) ) & ( for x being set holds
( x in b2 iff ( x in dom f & a <= f . x ) ) ) holds
b1 = b2
defpred S5[
set ]
means ( $1
in dom f &
a = f . $1 );
redefine func Coim f,
a means :
Def16:
:: MESFUNC1:def 16
for
x being
set holds
(
x in it iff (
x in dom f &
f . x = a ) );
compatibility
for b1 being set holds
( b1 = eq_dom f,a iff for x being set holds
( x in b1 iff ( x in dom f & f . x = a ) ) )
end;
:: deftheorem MESFUNC1:def 11 :
canceled;
:: deftheorem Def12 defines less_dom MESFUNC1:def 12 :
:: deftheorem Def13 defines less_eq_dom MESFUNC1:def 13 :
:: deftheorem Def14 defines great_dom MESFUNC1:def 14 :
:: deftheorem Def15 defines great_eq_dom MESFUNC1:def 15 :
:: deftheorem Def16 defines eq_dom MESFUNC1:def 16 :
definition
let X be
set ;
let f be
PartFunc of
X,
ExtREAL ;
let a be
ext-real number ;
:: original: less_domredefine func less_dom f,
a -> Subset of
X;
coherence
less_dom f,a is Subset of X
:: original: less_eq_domredefine func less_eq_dom f,
a -> Subset of
X;
coherence
less_eq_dom f,a is Subset of X
:: original: great_domredefine func great_dom f,
a -> Subset of
X;
coherence
great_dom f,a is Subset of X
:: original: great_eq_domredefine func great_eq_dom f,
a -> Subset of
X;
coherence
great_eq_dom f,a is Subset of X
:: original: eq_domredefine func eq_dom f,
a -> Subset of
X;
coherence
eq_dom f,a is Subset of X
end;
theorem :: MESFUNC1:17
canceled;
theorem Th18: :: MESFUNC1:18
theorem Th19: :: MESFUNC1:19
theorem Th20: :: MESFUNC1:20
theorem Th21: :: MESFUNC1:21
theorem :: MESFUNC1:22
theorem :: MESFUNC1:23
theorem Th24: :: MESFUNC1:24
theorem Th25: :: MESFUNC1:25
theorem Th26: :: MESFUNC1:26
theorem Th27: :: MESFUNC1:27
theorem Th28: :: MESFUNC1:28
theorem Th29: :: MESFUNC1:29
theorem Th30: :: MESFUNC1:30
:: deftheorem Def17 defines is_measurable_on MESFUNC1:def 17 :
theorem :: MESFUNC1:31
theorem Th32: :: MESFUNC1:32
theorem Th33: :: MESFUNC1:33
theorem :: MESFUNC1:34
theorem :: MESFUNC1:35
theorem :: MESFUNC1:36
theorem :: MESFUNC1:37
theorem :: MESFUNC1:38
theorem :: MESFUNC1:39
theorem :: MESFUNC1:40
theorem :: MESFUNC1:41