:: Definitions and Basic Properties of Measurable Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received September 7, 2000
:: Copyright (c) 2000-2011 Association of Mizar Users


begin

definition
func INT- -> Subset of REAL means :Def1: :: MESFUNC1:def 1
for r being Real holds
( r in it iff ex k being Element of NAT st r = - k );
existence
ex b1 being Subset of REAL st
for r being Real holds
( r in b1 iff ex k being Element of NAT st r = - k )
proof end;
uniqueness
for b1, b2 being Subset of REAL st ( for r being Real holds
( r in b1 iff ex k being Element of NAT st r = - k ) ) & ( for r being Real holds
( r in b2 iff ex k being Element of NAT st r = - k ) ) holds
b1 = b2
proof end;
correctness
;
end;

:: deftheorem Def1 defines INT- MESFUNC1:def 1 :
for b1 being Subset of REAL holds
( b1 = INT- iff for r being Real holds
( r in b1 iff ex k being Element of NAT st r = - k ) );

Lm1: 0 = - 0
;

registration
cluster INT- -> non empty ;
coherence
not INT- is empty
by Def1, Lm1;
end;

theorem Th1: :: MESFUNC1:1
NAT , INT- are_equipotent
proof end;

theorem Th2: :: MESFUNC1:2
INT = INT- \/ NAT
proof end;

theorem Th3: :: MESFUNC1:3
NAT , INT are_equipotent by Th1, Th2, CARD_3:119;

definition
:: original: INT
redefine func INT -> Subset of REAL;
correctness
coherence
INT is Subset of REAL
;
by NUMBERS:15;
end;

definition
let n be Nat;
func RAT_with_denominator n -> Subset of RAT means :Def2: :: MESFUNC1:def 2
for q being Rational holds
( q in it iff ex i being Integer st q = i / n );
existence
ex b1 being Subset of RAT st
for q being Rational holds
( q in b1 iff ex i being Integer st q = i / n )
proof end;
uniqueness
for b1, b2 being Subset of RAT st ( for q being Rational holds
( q in b1 iff ex i being Integer st q = i / n ) ) & ( for q being Rational holds
( q in b2 iff ex i being Integer st q = i / n ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines RAT_with_denominator MESFUNC1:def 2 :
for n being Nat
for b2 being Subset of RAT holds
( b2 = RAT_with_denominator n iff for q being Rational holds
( q in b2 iff ex i being Integer st q = i / n ) );

registration
let n be Nat;
cluster RAT_with_denominator (n + 1) -> non empty ;
coherence
not RAT_with_denominator (n + 1) is empty
proof end;
end;

theorem Th4: :: MESFUNC1:4
for n being Nat holds INT , RAT_with_denominator (n + 1) are_equipotent
proof end;

theorem :: MESFUNC1:5
NAT , RAT are_equipotent
proof end;

begin

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) ) )
proof end;
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
proof end;
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) ) )
proof end;
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
proof end;
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) ) )
proof end;
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
proof end;
end;

:: deftheorem Def3 defines + MESFUNC1:def 3 :
for C being non empty set
for f1, f2, b4 being PartFunc of C,ExtREAL holds
( b4 = f1 + f2 iff ( dom b4 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b4 holds
b4 . c = (f1 . c) + (f2 . c) ) ) );

:: deftheorem defines - MESFUNC1:def 4 :
for C being non empty set
for f1, f2, b4 being PartFunc of C,ExtREAL holds
( b4 = f1 - f2 iff ( dom b4 = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b4 holds
b4 . c = (f1 . c) - (f2 . c) ) ) );

:: deftheorem Def5 defines (#) MESFUNC1:def 5 :
for C being non empty set
for f1, f2, b4 being PartFunc of C,ExtREAL holds
( b4 = f1 (#) f2 iff ( dom b4 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b4 holds
b4 . c = (f1 . c) * (f2 . c) ) ) );

definition
let C be non empty set ;
let f be PartFunc of C,ExtREAL;
let r be Real;
deffunc H1( Element of C) -> Element of ExtREAL = (R_EAL r) * (f . $1);
func r (#) f -> PartFunc of C,ExtREAL means :Def6: :: MESFUNC1:def 6
( dom it = dom f & ( for c being Element of C st c in dom it holds
it . c = (R_EAL r) * (f . c) ) );
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 . c = (R_EAL r) * (f . c) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 . c = (R_EAL r) * (f . c) ) & dom b2 = dom f & ( for c being Element of C st c in dom b2 holds
b2 . c = (R_EAL r) * (f . c) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines (#) MESFUNC1:def 6 :
for C being non empty set
for f being PartFunc of C,ExtREAL
for r being Real
for b4 being PartFunc of C,ExtREAL holds
( b4 = r (#) f iff ( dom b4 = dom f & ( for c being Element of C st c in dom b4 holds
b4 . c = (R_EAL r) * (f . c) ) ) );

theorem Th6: :: MESFUNC1:6
for C being non empty set
for f being PartFunc of C,ExtREAL
for r being Real st r <> 0 holds
for c being Element of C st c in dom (r (#) f) holds
f . c = ((r (#) f) . c) / (R_EAL r)
proof end;

definition
let C be non empty set ;
let f be PartFunc of C,ExtREAL;
deffunc H1( Element of C) -> Element of ExtREAL = - (f . $1);
func - f -> PartFunc of C,ExtREAL means :: MESFUNC1:def 7
( dom it = dom f & ( for c being Element of C st c in dom it holds
it . c = - (f . c) ) );
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 . c = - (f . c) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 . c = - (f . c) ) & dom b2 = dom f & ( for c being Element of C st c in dom b2 holds
b2 . c = - (f . c) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines - MESFUNC1:def 7 :
for C being non empty set
for f, b3 being PartFunc of C,ExtREAL holds
( b3 = - f iff ( dom b3 = dom f & ( for c being Element of C st c in dom b3 holds
b3 . c = - (f . c) ) ) );

definition
func 1. -> R_eal equals :: MESFUNC1:def 8
1;
correctness
coherence
1 is R_eal
;
by XXREAL_0:def 1;
end;

:: deftheorem defines 1. MESFUNC1:def 8 :
1. = 1;

definition
let C be non empty set ;
let f be PartFunc of C,ExtREAL;
let r be Real;
deffunc H1( Element of C) -> Element of ExtREAL = (R_EAL r) / (f . $1);
func r / f -> PartFunc of C,ExtREAL means :Def9: :: MESFUNC1:def 9
( dom it = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom it holds
it . c = (R_EAL r) / (f . c) ) );
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom b1 holds
b1 . c = (R_EAL r) / (f . c) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom b1 holds
b1 . c = (R_EAL r) / (f . c) ) & dom b2 = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom b2 holds
b2 . c = (R_EAL r) / (f . c) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines / MESFUNC1:def 9 :
for C being non empty set
for f being PartFunc of C,ExtREAL
for r being Real
for b4 being PartFunc of C,ExtREAL holds
( b4 = r / f iff ( dom b4 = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom b4 holds
b4 . c = (R_EAL r) / (f . c) ) ) );

theorem :: MESFUNC1:7
for C being non empty set
for f being PartFunc of C,ExtREAL holds
( dom (1 / f) = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom (1 / f) holds
(1 / f) . c = 1. / (f . c) ) )
proof end;

definition
let C be non empty set ;
let f be PartFunc of C,ExtREAL;
deffunc H1( Element of C) -> Element of ExtREAL = |.(f . $1).|;
func |.f.| -> PartFunc of C,ExtREAL means :: MESFUNC1:def 10
( dom it = dom f & ( for c being Element of C st c in dom it holds
it . c = |.(f . c).| ) );
existence
ex b1 being PartFunc of C,ExtREAL st
( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 . c = |.(f . c).| ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = dom f & ( for c being Element of C st c in dom b1 holds
b1 . c = |.(f . c).| ) & dom b2 = dom f & ( for c being Element of C st c in dom b2 holds
b2 . c = |.(f . c).| ) holds
b1 = b2
proof end;
end;

:: deftheorem defines |. MESFUNC1:def 10 :
for C being non empty set
for f, b3 being PartFunc of C,ExtREAL holds
( b3 = |.f.| iff ( dom b3 = dom f & ( for c being Element of C st c in dom b3 holds
b3 . c = |.(f . c).| ) ) );

theorem :: MESFUNC1:8
canceled;

theorem :: MESFUNC1:9
canceled;

theorem :: MESFUNC1:10
canceled;

definition
let C be non empty set ;
let f1, f2 be PartFunc of C,ExtREAL;
:: original: +
redefine func f1 + f2 -> PartFunc of C,ExtREAL;
commutativity
for f1, f2 being PartFunc of C,ExtREAL holds f1 + f2 = f2 + f1
proof end;
:: original: (#)
redefine func f1 (#) f2 -> PartFunc of C,ExtREAL;
commutativity
for f1, f2 being PartFunc of C,ExtREAL holds f1 (#) f2 = f2 (#) f1
proof end;
end;

begin

theorem Th11: :: MESFUNC1:11
for r being Real ex n being Element of NAT st r <= n
proof end;

theorem Th12: :: MESFUNC1:12
for r being Real ex n being Element of NAT st - n <= r
proof end;

theorem Th13: :: MESFUNC1:13
for r, s being real number st r < s holds
ex n being Element of NAT st 1 / (n + 1) < s - r
proof end;

theorem Th14: :: MESFUNC1:14
for r, s being real number st ( for n being Element of NAT holds r - (1 / (n + 1)) <= s ) holds
r <= s
proof end;

theorem Th15: :: MESFUNC1:15
for a being R_eal st ( for r being Real holds R_EAL r < a ) holds
a = +infty
proof end;

theorem Th16: :: MESFUNC1:16
for a being R_eal st ( for r being Real holds a < R_EAL r ) holds
a = -infty
proof end;

notation
let f be ext-real-valued Function;
let a be ext-real number ;
synonym eq_dom (f,a) for Coim (f,a);
end;

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 ) )
proof end;
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
proof end;
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 ) )
proof end;
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
proof end;
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 ) )
proof end;
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
proof end;
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 ) )
proof end;
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
proof end;
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 ) ) )
proof end;
end;

:: deftheorem MESFUNC1:def 11 :
canceled;

:: deftheorem Def12 defines less_dom MESFUNC1:def 12 :
for f being ext-real-valued Function
for a being ext-real number
for b3 being set holds
( b3 = less_dom (f,a) iff for x being set holds
( x in b3 iff ( x in dom f & f . x < a ) ) );

:: deftheorem Def13 defines less_eq_dom MESFUNC1:def 13 :
for f being ext-real-valued Function
for a being ext-real number
for b3 being set holds
( b3 = less_eq_dom (f,a) iff for x being set holds
( x in b3 iff ( x in dom f & f . x <= a ) ) );

:: deftheorem Def14 defines great_dom MESFUNC1:def 14 :
for f being ext-real-valued Function
for a being ext-real number
for b3 being set holds
( b3 = great_dom (f,a) iff for x being set holds
( x in b3 iff ( x in dom f & a < f . x ) ) );

:: deftheorem Def15 defines great_eq_dom MESFUNC1:def 15 :
for f being ext-real-valued Function
for a being ext-real number
for b3 being set holds
( b3 = great_eq_dom (f,a) iff for x being set holds
( x in b3 iff ( x in dom f & a <= f . x ) ) );

:: deftheorem Def16 defines eq_dom MESFUNC1:def 16 :
for f being ext-real-valued Function
for a being ext-real number
for b3 being set holds
( b3 = eq_dom (f,a) iff for x being set holds
( x in b3 iff ( x in dom f & f . x = a ) ) );

definition
let X be set ;
let f be PartFunc of X,ExtREAL;
let a be ext-real number ;
:: original: less_dom
redefine func less_dom (f,a) -> Subset of X;
coherence
less_dom (f,a) is Subset of X
proof end;
:: original: less_eq_dom
redefine func less_eq_dom (f,a) -> Subset of X;
coherence
less_eq_dom (f,a) is Subset of X
proof end;
:: original: great_dom
redefine func great_dom (f,a) -> Subset of X;
coherence
great_dom (f,a) is Subset of X
proof end;
:: original: great_eq_dom
redefine func great_eq_dom (f,a) -> Subset of X;
coherence
great_eq_dom (f,a) is Subset of X
proof end;
:: original: eq_dom
redefine func eq_dom (f,a) -> Subset of X;
coherence
eq_dom (f,a) is Subset of X
proof end;
end;

theorem :: MESFUNC1:17
canceled;

theorem Th18: :: MESFUNC1:18
for X being set
for f being PartFunc of X,ExtREAL
for A being set
for a being R_eal st A c= dom f holds
A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a)))
proof end;

theorem Th19: :: MESFUNC1:19
for X being set
for f being PartFunc of X,ExtREAL
for A being set
for a being R_eal st A c= dom f holds
A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))
proof end;

theorem Th20: :: MESFUNC1:20
for X being set
for f being PartFunc of X,ExtREAL
for A being set
for a being R_eal st A c= dom f holds
A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))
proof end;

theorem Th21: :: MESFUNC1:21
for X being set
for f being PartFunc of X,ExtREAL
for A being set
for a being R_eal st A c= dom f holds
A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a)))
proof end;

theorem :: MESFUNC1:22
for X being set
for f being PartFunc of X,ExtREAL
for A being set
for a being R_eal holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
proof end;

theorem :: MESFUNC1:23
for X being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,ExtREAL
for A being set
for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) holds
A /\ (great_eq_dom (f,(R_EAL r))) = meet (rng F)
proof end;

theorem Th24: :: MESFUNC1:24
for X being set
for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for F being Function of NAT,S
for A being set
for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) holds
A /\ (less_eq_dom (f,(R_EAL r))) = meet (rng F)
proof end;

theorem Th25: :: MESFUNC1:25
for X being set
for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for F being Function of NAT,S
for A being set
for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) holds
A /\ (less_dom (f,(R_EAL r))) = union (rng F)
proof end;

theorem Th26: :: MESFUNC1:26
for X being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,ExtREAL
for A being set
for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_eq_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) holds
A /\ (great_dom (f,(R_EAL r))) = union (rng F)
proof end;

theorem Th27: :: MESFUNC1:27
for X being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,ExtREAL
for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL n))) ) holds
A /\ (eq_dom (f,+infty)) = meet (rng F)
proof end;

theorem Th28: :: MESFUNC1:28
for X being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,ExtREAL
for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL n))) ) holds
A /\ (less_dom (f,+infty)) = union (rng F)
proof end;

theorem Th29: :: MESFUNC1:29
for X being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,ExtREAL
for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (- n)))) ) holds
A /\ (eq_dom (f,-infty)) = meet (rng F)
proof end;

theorem Th30: :: MESFUNC1:30
for X being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,ExtREAL
for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (- n)))) ) holds
A /\ (great_dom (f,-infty)) = union (rng F)
proof end;

begin

definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
let A be Element of S;
pred f is_measurable_on A means :Def17: :: MESFUNC1:def 17
for r being real number holds A /\ (less_dom (f,(R_EAL r))) in S;
end;

:: deftheorem Def17 defines is_measurable_on MESFUNC1:def 17 :
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_dom (f,(R_EAL r))) in S );

theorem :: MESFUNC1:31
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S st A c= dom f holds
( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S )
proof end;

theorem Th32: :: MESFUNC1:32
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S )
proof end;

theorem Th33: :: MESFUNC1:33
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S st A c= dom f holds
( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S )
proof end;

theorem :: MESFUNC1:34
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A, B being Element of S st B c= A & f is_measurable_on A holds
f is_measurable_on B
proof end;

theorem :: MESFUNC1:35
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds
f is_measurable_on A \/ B
proof end;

theorem :: MESFUNC1:36
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S
for r, s being Real st f is_measurable_on A & A c= dom f holds
(A /\ (great_dom (f,(R_EAL r)))) /\ (less_dom (f,(R_EAL s))) in S
proof end;

theorem :: MESFUNC1:37
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S st f is_measurable_on A & A c= dom f holds
A /\ (eq_dom (f,+infty)) in S
proof end;

theorem :: MESFUNC1:38
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S st f is_measurable_on A holds
A /\ (eq_dom (f,-infty)) in S
proof end;

theorem :: MESFUNC1:39
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S st f is_measurable_on A & A c= dom f holds
(A /\ (great_dom (f,-infty))) /\ (less_dom (f,+infty)) in S
proof end;

theorem :: MESFUNC1:40
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for A being Element of S
for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
(A /\ (less_dom (f,(R_EAL r)))) /\ (great_dom (g,(R_EAL r))) in S
proof end;

theorem :: MESFUNC1:41
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S
for r being Real st f is_measurable_on A & A c= dom f holds
r (#) f is_measurable_on A
proof end;