:: MESFUNC1 semantic presentation

definition

func INT- -> Subset of REAL means :Def1: :: MESFUNC1:def 1
for r being Real holds
( r in it iff ex k being Nat st r = - k );
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def1 defines INT- MESFUNC1:def 1 :

Lm1: 0 = - 0
;

registration

cluster INT- -> non empty ;
coherence 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_4:15, CARD_4:35;

definition

:: original: INT
redefine func INT -> Subset of REAL ;
correctness 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines RAT_with_denominator MESFUNC1:def 2 :

registration

let n be Nat;
cluster RAT_with_denominator (n + 1) -> non empty ;
coherence

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;

definition

let C be non empty set ;
let f be PartFunc of C, ExtREAL ;
let x be set ;
:: original: .
redefine func f . x -> R_eal;
coherence

proof end;

end;

definition

let C be non empty set ;
let f1, f2 be PartFunc of C, ExtREAL ;
deffunc H₁( 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

proof end;

uniqueness

proof end;

deffunc H₂( 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

proof end;

uniqueness

proof end;

deffunc H₃( 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines + MESFUNC1:def 3 :

:: deftheorem defines - MESFUNC1:def 4 :

:: deftheorem Def5 defines (#) MESFUNC1:def 5 :

definition

let C be non empty set ;
let f be PartFunc of C, ExtREAL ;
let r be Real;
deffunc H₁( 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines (#) MESFUNC1:def 6 :

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 H₁( 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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines - MESFUNC1:def 7 :

definition

func 1. -> R_eal equals :: MESFUNC1:def 8
1;
correctness by SUPINF_1:10;

end;

:: deftheorem defines 1. MESFUNC1:def 8 :

definition

let C be non empty set ;
let f be PartFunc of C, ExtREAL ;
let r be Real;
deffunc H₁( 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines / MESFUNC1:def 9 :

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 H₁( 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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines |. MESFUNC1:def 10 :

theorem :: MESFUNC1:8

canceled;

theorem Th9: :: MESFUNC1:9

for C being non empty set
for f1, f2 being PartFunc of C, ExtREAL holds f1 + f2 = f2 + f1

proof end;

theorem Th10: :: MESFUNC1:10

for C being non empty set
for f1, f2 being PartFunc of C, ExtREAL holds f1 (#) f2 = f2 (#) f1

proof end;

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 by Th9;
:: original: (#)
redefine func f1 (#) f2 -> PartFunc of C, ExtREAL ;
commutativity by Th10;

end;

theorem Th11: :: MESFUNC1:11

for r being Real ex n being Nat st r <= n

proof end;

theorem Th12: :: MESFUNC1:12

for r being Real ex n being Nat st - n <= r

proof end;

theorem Th13: :: MESFUNC1:13

for r, s being real number st r < s holds
ex n being Nat st 1 / (n + 1) < s - r

proof end;

theorem Th14: :: MESFUNC1:14

for r, s being real number st ( for n being 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;

definition

let X be set ;
let S be sigma_Field_Subset of X;
let A be set ;
pred A is_measurable_on S means :Def11: :: MESFUNC1:def 11
A in S;

end;

:: deftheorem Def11 defines is_measurable_on MESFUNC1:def 11 :

theorem :: MESFUNC1:17

for X, A being set
for S being sigma_Field_Subset of X holds
( A is_measurable_on S iff for M being sigma_Measure of S holds A is_measurable M )

proof end;

definition

let X be non empty set ;
let f be PartFunc of X, ExtREAL ;
let a be R_eal;
func less_dom f,a -> Subset of X means :Def12: :: MESFUNC1:def 12
for x being Element of X holds
( x in it iff ( x in dom f & ex y being R_eal st
( y = f . x & y <' a ) ) );
existence

proof end;

uniqueness

proof end;

correctness ;
func less_eq_dom f,a -> Subset of X means :Def13: :: MESFUNC1:def 13
for x being Element of X holds
( x in it iff ( x in dom f & ex y being R_eal st
( y = f . x & y <=' a ) ) );
existence

proof end;

uniqueness

proof end;

correctness ;
func great_dom f,a -> Subset of X means :Def14: :: MESFUNC1:def 14
for x being Element of X holds
( x in it iff ( x in dom f & ex y being R_eal st
( y = f . x & a <' y ) ) );
existence

proof end;

uniqueness

proof end;

correctness ;
func great_eq_dom f,a -> Subset of X means :Def15: :: MESFUNC1:def 15
for x being Element of X holds
( x in it iff ( x in dom f & ex y being R_eal st
( y = f . x & a <=' y ) ) );
existence

proof end;

uniqueness

proof end;

correctness ;
func eq_dom f,a -> Subset of X means :Def16: :: MESFUNC1:def 16
for x being Element of X holds
( x in it iff ( x in dom f & ex y being R_eal st
( y = f . x & a = y ) ) );
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: 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 :

theorem Th18: :: MESFUNC1:18

for X being non empty 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 non empty 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 non empty 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 non empty 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 non empty 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 non empty set
for S being sigma_Field_Subset 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 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 non empty set
for f being PartFunc of X, ExtREAL
for S being sigma_Field_Subset of X
for F being Function of NAT ,S
for A being set
for r being real number st ( for n being 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 non empty set
for f being PartFunc of X, ExtREAL
for S being sigma_Field_Subset of X
for F being Function of NAT ,S
for A being set
for r being real number st ( for n being 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 non empty set
for S being sigma_Field_Subset 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 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 non empty set
for S being sigma_Field_Subset of X
for F being Function of NAT ,S
for f being PartFunc of X, ExtREAL
for A being set st ( for n being 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 non empty set
for S being sigma_Field_Subset of X
for F being Function of NAT ,S
for f being PartFunc of X, ExtREAL
for A being set st ( for n being 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 non empty set
for S being sigma_Field_Subset of X
for F being Function of NAT ,S
for f being PartFunc of X, ExtREAL
for A being set st ( for n being 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

proof end;

definition

let X be non empty set ;
let S be sigma_Field_Subset 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)) is_measurable_on S;

end;

:: deftheorem Def17 defines is_measurable_on MESFUNC1:def 17 :

theorem :: MESFUNC1:31

for X being non empty set
for S being sigma_Field_Subset 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)) is_measurable_on S )

proof end;

theorem Th32: :: MESFUNC1:32

for X being non empty set
for S being sigma_Field_Subset 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)) is_measurable_on S )

proof end;

theorem Th33: :: MESFUNC1:33

proof end;

theorem :: MESFUNC1:34

for X being non empty set
for S being sigma_Field_Subset 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 sigma_Field_Subset 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 sigma_Field_Subset 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)) is_measurable_on S

proof end;

theorem :: MESFUNC1:37

for X being non empty set
for S being sigma_Field_Subset 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 ) is_measurable_on S

proof end;

theorem :: MESFUNC1:38

for X being non empty set
for S being sigma_Field_Subset 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 ) is_measurable_on S

proof end;

theorem :: MESFUNC1:39

for X being non empty set
for S being sigma_Field_Subset 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 ) is_measurable_on S

proof end;

theorem :: MESFUNC1:40

for X being non empty set
for S being sigma_Field_Subset 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)) is_measurable_on S

proof end;

theorem :: MESFUNC1:41

for X being non empty set
for S being sigma_Field_Subset 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;