begin
:: deftheorem Def1 defines INT- MESFUNC1:def 1 :
Lm1:
0 = - 0
;
theorem Th1:
theorem Th2:
theorem Th3:
:: deftheorem Def2 defines RAT_with_denominator MESFUNC1:def 2 :
theorem Th4:
theorem
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:
(
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
(
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:
(
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:
:: deftheorem defines - MESFUNC1:def 7 :
:: deftheorem defines 1. MESFUNC1:def 8 :
:: deftheorem Def9 defines / MESFUNC1:def 9 :
theorem
:: deftheorem defines |. MESFUNC1:def 10 :
theorem
canceled;
theorem Th9:
theorem Th10:
begin
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
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:
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:
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:
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:
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:
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 ;
less_domredefine func less_dom f,
a -> Subset of
X;
coherence
less_dom f,a is Subset of X
less_eq_domredefine func less_eq_dom f,
a -> Subset of
X;
coherence
less_eq_dom f,a is Subset of X
great_domredefine func great_dom f,
a -> Subset of
X;
coherence
great_dom f,a is Subset of X
great_eq_domredefine func great_eq_dom f,
a -> Subset of
X;
coherence
great_eq_dom f,a is Subset of X
eq_domredefine func eq_dom f,
a -> Subset of
X;
coherence
eq_dom f,a is Subset of X
end;
theorem
canceled;
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem
theorem
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
begin
:: deftheorem Def17 defines is_measurable_on MESFUNC1:def 17 :
theorem
theorem Th32:
theorem Th33:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem