:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama

::

:: Received September 7, 2000

:: Copyright (c) 2000-2012 Association of Mizar Users

begin

definition

ex b_{1} being Subset of REAL st

for r being Real holds

( r in b_{1} iff ex k being Element of NAT st r = - k )

for b_{1}, b_{2} being Subset of REAL st ( for r being Real holds

( r in b_{1} iff ex k being Element of NAT st r = - k ) ) & ( for r being Real holds

( r in b_{2} iff ex k being Element of NAT st r = - k ) ) holds

b_{1} = b_{2}

;

end;

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 for r being Real holds

( r in it iff ex k being Element of NAT st r = - k );

ex b

for r being Real holds

( r in b

proof end;

uniqueness for b

( r in b

( r in b

b

proof end;

correctness ;

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

for b_{1} being Subset of REAL holds

( b_{1} = INT- iff for r being Real holds

( r in b_{1} iff ex k being Element of NAT st r = - k ) );

for b

( b

( r in b

Lm1: 0 = - 0

;

definition

let n be Nat;

ex b_{1} being Subset of RAT st

for q being Rational holds

( q in b_{1} iff ex i being Integer st q = i / n )

for b_{1}, b_{2} being Subset of RAT st ( for q being Rational holds

( q in b_{1} iff ex i being Integer st q = i / n ) ) & ( for q being Rational holds

( q in b_{2} iff ex i being Integer st q = i / n ) ) holds

b_{1} = b_{2}

end;
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 for q being Rational holds

( q in it iff ex i being Integer st q = i / n );

ex b

for q being Rational holds

( q in b

proof end;

uniqueness for b

( q in b

( q in b

b

proof end;

:: deftheorem Def2 defines RAT_with_denominator MESFUNC1:def 2 :

for n being Nat

for b_{2} being Subset of RAT holds

( b_{2} = RAT_with_denominator n iff for q being Rational holds

( q in b_{2} iff ex i being Integer st q = i / n ) );

for n being Nat

for b

( b

( q in b

begin

definition

let C be non empty set ;

let f1, f2 be C -defined ExtREAL -valued Function;

deffunc H_{1}( Element of C) -> Element of ExtREAL = (f1 . $1) + (f2 . $1);

ex b_{1} being PartFunc of C,ExtREAL st

( dom b_{1} = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = (f1 . c) + (f2 . c) ) )

for b_{1}, b_{2} being PartFunc of C,ExtREAL st dom b_{1} = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = (f1 . c) + (f2 . c) ) & dom b_{2} = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b_{2} holds

b_{2} . c = (f1 . c) + (f2 . c) ) holds

b_{1} = b_{2}

for b_{1} being PartFunc of C,ExtREAL

for f1, f2 being C -defined ExtREAL -valued Function st dom b_{1} = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = (f1 . c) + (f2 . c) ) holds

( dom b_{1} = ((dom f2) /\ (dom f1)) \ (((f2 " {-infty}) /\ (f1 " {+infty})) \/ ((f2 " {+infty}) /\ (f1 " {-infty}))) & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = (f2 . c) + (f1 . c) ) )
;

deffunc H_{2}( Element of C) -> Element of ExtREAL = (f1 . $1) - (f2 . $1);

ex b_{1} being PartFunc of C,ExtREAL st

( dom b_{1} = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = (f1 . c) - (f2 . c) ) )

for b_{1}, b_{2} being PartFunc of C,ExtREAL st dom b_{1} = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = (f1 . c) - (f2 . c) ) & dom b_{2} = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b_{2} holds

b_{2} . c = (f1 . c) - (f2 . c) ) holds

b_{1} = b_{2}
_{3}( Element of C) -> Element of ExtREAL = (f1 . $1) * (f2 . $1);

ex b_{1} being PartFunc of C,ExtREAL st

( dom b_{1} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = (f1 . c) * (f2 . c) ) )

for b_{1}, b_{2} being PartFunc of C,ExtREAL st dom b_{1} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = (f1 . c) * (f2 . c) ) & dom b_{2} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{2} holds

b_{2} . c = (f1 . c) * (f2 . c) ) holds

b_{1} = b_{2}

for b_{1} being PartFunc of C,ExtREAL

for f1, f2 being C -defined ExtREAL -valued Function st dom b_{1} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = (f1 . c) * (f2 . c) ) holds

( dom b_{1} = (dom f2) /\ (dom f1) & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = (f2 . c) * (f1 . c) ) )
;

end;
let f1, f2 be C -defined ExtREAL -valued Function;

deffunc H

func f1 + f2 -> PartFunc of C,ExtREAL means :: 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 ( 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) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

for f1, f2 being C -defined ExtREAL -valued Function st dom b

b

( dom b

b

deffunc H

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 ( 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) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

deffunc H
func f1 (#) f2 -> PartFunc of C,ExtREAL means :: 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 ( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds

it . c = (f1 . c) * (f2 . c) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

for f1, f2 being C -defined ExtREAL -valued Function st dom b

b

( dom b

b

:: deftheorem defines + MESFUNC1:def 3 :

for C being non empty set

for f1, f2 being b_{1} -defined ExtREAL -valued Function

for b_{4} being PartFunc of C,ExtREAL holds

( b_{4} = f1 + f2 iff ( dom b_{4} = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b_{4} holds

b_{4} . c = (f1 . c) + (f2 . c) ) ) );

for C being non empty set

for f1, f2 being b

for b

( b

b

:: deftheorem defines - MESFUNC1:def 4 :

for C being non empty set

for f1, f2 being b_{1} -defined ExtREAL -valued Function

for b_{4} being PartFunc of C,ExtREAL holds

( b_{4} = f1 - f2 iff ( dom b_{4} = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b_{4} holds

b_{4} . c = (f1 . c) - (f2 . c) ) ) );

for C being non empty set

for f1, f2 being b

for b

( b

b

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

for C being non empty set

for f1, f2 being b_{1} -defined ExtREAL -valued Function

for b_{4} being PartFunc of C,ExtREAL holds

( b_{4} = f1 (#) f2 iff ( dom b_{4} = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b_{4} holds

b_{4} . c = (f1 . c) * (f2 . c) ) ) );

for C being non empty set

for f1, f2 being b

for b

( b

b

definition

let C be non empty set ;

let f be C -defined ExtREAL -valued Function;

let r be Real;

deffunc H_{1}( Element of C) -> Element of ExtREAL = (R_EAL r) * (f . $1);

ex b_{1} being PartFunc of C,ExtREAL st

( dom b_{1} = dom f & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = (R_EAL r) * (f . c) ) )

for b_{1}, b_{2} being PartFunc of C,ExtREAL st dom b_{1} = dom f & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = (R_EAL r) * (f . c) ) & dom b_{2} = dom f & ( for c being Element of C st c in dom b_{2} holds

b_{2} . c = (R_EAL r) * (f . c) ) holds

b_{1} = b_{2}

end;
let f be C -defined ExtREAL -valued Function;

let r be Real;

deffunc H

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 ( dom it = dom f & ( for c being Element of C st c in dom it holds

it . c = (R_EAL r) * (f . c) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for C being non empty set

for f being b_{1} -defined ExtREAL -valued Function

for r being Real

for b_{4} being PartFunc of C,ExtREAL holds

( b_{4} = r (#) f iff ( dom b_{4} = dom f & ( for c being Element of C st c in dom b_{4} holds

b_{4} . c = (R_EAL r) * (f . c) ) ) );

for C being non empty set

for f being b

for r being Real

for b

( b

b

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)

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 C -defined ExtREAL -valued Function;

deffunc H_{1}( Element of C) -> Element of ExtREAL = - (f . $1);

ex b_{1} being PartFunc of C,ExtREAL st

( dom b_{1} = dom f & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = - (f . c) ) )

for b_{1}, b_{2} being PartFunc of C,ExtREAL st dom b_{1} = dom f & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = - (f . c) ) & dom b_{2} = dom f & ( for c being Element of C st c in dom b_{2} holds

b_{2} . c = - (f . c) ) holds

b_{1} = b_{2}

end;
let f be C -defined ExtREAL -valued Function;

deffunc H

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 ( dom it = dom f & ( for c being Element of C st c in dom it holds

it . c = - (f . c) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines - MESFUNC1:def 7 :

for C being non empty set

for f being b_{1} -defined ExtREAL -valued Function

for b_{3} being PartFunc of C,ExtREAL holds

( b_{3} = - f iff ( dom b_{3} = dom f & ( for c being Element of C st c in dom b_{3} holds

b_{3} . c = - (f . c) ) ) );

for C being non empty set

for f being b

for b

( b

b

definition
end;

definition

let C be non empty set ;

let f be C -defined ExtREAL -valued Function;

let r be Real;

deffunc H_{1}( Element of C) -> Element of ExtREAL = (R_EAL r) / (f . $1);

ex b_{1} being PartFunc of C,ExtREAL st

( dom b_{1} = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = (R_EAL r) / (f . c) ) )

for b_{1}, b_{2} being PartFunc of C,ExtREAL st dom b_{1} = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = (R_EAL r) / (f . c) ) & dom b_{2} = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom b_{2} holds

b_{2} . c = (R_EAL r) / (f . c) ) holds

b_{1} = b_{2}

end;
let f be C -defined ExtREAL -valued Function;

let r be Real;

deffunc H

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 ( 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) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines / MESFUNC1:def 9 :

for C being non empty set

for f being b_{1} -defined ExtREAL -valued Function

for r being Real

for b_{4} being PartFunc of C,ExtREAL holds

( b_{4} = r / f iff ( dom b_{4} = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom b_{4} holds

b_{4} . c = (R_EAL r) / (f . c) ) ) );

for C being non empty set

for f being b

for r being Real

for b

( b

b

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

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 C -defined ExtREAL -valued Function;

deffunc H_{1}( Element of C) -> Element of ExtREAL = |.(f . $1).|;

ex b_{1} being PartFunc of C,ExtREAL st

( dom b_{1} = dom f & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = |.(f . c).| ) )

for b_{1}, b_{2} being PartFunc of C,ExtREAL st dom b_{1} = dom f & ( for c being Element of C st c in dom b_{1} holds

b_{1} . c = |.(f . c).| ) & dom b_{2} = dom f & ( for c being Element of C st c in dom b_{2} holds

b_{2} . c = |.(f . c).| ) holds

b_{1} = b_{2}

end;
let f be C -defined ExtREAL -valued Function;

deffunc H

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 ( dom it = dom f & ( for c being Element of C st c in dom it holds

it . c = |.(f . c).| ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines |. MESFUNC1:def 10 :

for C being non empty set

for f being b_{1} -defined ExtREAL -valued Function

for b_{3} being PartFunc of C,ExtREAL holds

( b_{3} = |.f.| iff ( dom b_{3} = dom f & ( for c being Element of C st c in dom b_{3} holds

b_{3} . c = |.(f . c).| ) ) );

for C being non empty set

for f being b

for b

( b

b

begin

theorem Th11: :: MESFUNC1:11

for r, s being real number st ( for n being Element of NAT holds r - (1 / (n + 1)) <= s ) holds

r <= s

r <= s

proof end;

notation
end;

definition

let f be ext-real-valued Function;

let a be ext-real number ;

defpred S_{1}[ set ] means ( $1 in dom f & f . $1 < a );

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x in dom f & f . x < a ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x in dom f & f . x < a ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in dom f & f . x < a ) ) ) holds

b_{1} = b_{2}
_{2}[ set ] means ( $1 in dom f & f . $1 <= a );

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x in dom f & f . x <= a ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x in dom f & f . x <= a ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in dom f & f . x <= a ) ) ) holds

b_{1} = b_{2}
_{3}[ set ] means ( $1 in dom f & a < f . $1 );

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x in dom f & a < f . x ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x in dom f & a < f . x ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in dom f & a < f . x ) ) ) holds

b_{1} = b_{2}
_{4}[ set ] means ( $1 in dom f & a <= f . $1 );

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x in dom f & a <= f . x ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x in dom f & a <= f . x ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in dom f & a <= f . x ) ) ) holds

b_{1} = b_{2}

for b_{1} being set holds

( b_{1} = eq_dom (f,a) iff for x being set holds

( x in b_{1} iff ( x in dom f & f . x = a ) ) )

end;
let a be ext-real number ;

defpred S

func less_dom (f,a) -> set means :Def11: :: MESFUNC1:def 11

for x being set holds

( x in it iff ( x in dom f & f . x < a ) );

existence for x being set holds

( x in it iff ( x in dom f & f . x < a ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

defpred S
func less_eq_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 for x being set holds

( x in it iff ( x in dom f & f . x <= a ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

defpred S
func great_dom (f,a) -> set means :Def13: :: MESFUNC1:def 13

for x being set holds

( x in it iff ( x in dom f & a < f . x ) );

existence for x being set holds

( x in it iff ( x in dom f & a < f . x ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

defpred S
func great_eq_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 for x being set holds

( x in it iff ( x in dom f & a <= f . x ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

redefine func Coim (f,a) means :Def15: :: MESFUNC1:def 15

for x being set holds

( x in it iff ( x in dom f & f . x = a ) );

compatibility for x being set holds

( x in it iff ( x in dom f & f . x = a ) );

for b

( b

( x in b

proof end;

:: deftheorem Def11 defines less_dom MESFUNC1:def 11 :

for f being ext-real-valued Function

for a being ext-real number

for b_{3} being set holds

( b_{3} = less_dom (f,a) iff for x being set holds

( x in b_{3} iff ( x in dom f & f . x < a ) ) );

for f being ext-real-valued Function

for a being ext-real number

for b

( b

( x in b

:: deftheorem Def12 defines less_eq_dom MESFUNC1:def 12 :

for f being ext-real-valued Function

for a being ext-real number

for b_{3} being set holds

( b_{3} = less_eq_dom (f,a) iff for x being set holds

( x in b_{3} iff ( x in dom f & f . x <= a ) ) );

for f being ext-real-valued Function

for a being ext-real number

for b

( b

( x in b

:: deftheorem Def13 defines great_dom MESFUNC1:def 13 :

for f being ext-real-valued Function

for a being ext-real number

for b_{3} being set holds

( b_{3} = great_dom (f,a) iff for x being set holds

( x in b_{3} iff ( x in dom f & a < f . x ) ) );

for f being ext-real-valued Function

for a being ext-real number

for b

( b

( x in b

:: deftheorem Def14 defines great_eq_dom MESFUNC1:def 14 :

for f being ext-real-valued Function

for a being ext-real number

for b_{3} being set holds

( b_{3} = great_eq_dom (f,a) iff for x being set holds

( x in b_{3} iff ( x in dom f & a <= f . x ) ) );

for f being ext-real-valued Function

for a being ext-real number

for b

( b

( x in b

:: deftheorem Def15 defines eq_dom MESFUNC1:def 15 :

for f being ext-real-valued Function

for a being ext-real number

for b_{3} being set holds

( b_{3} = eq_dom (f,a) iff for x being set holds

( x in b_{3} iff ( x in dom f & f . x = a ) ) );

for f being ext-real-valued Function

for a being ext-real number

for b

( b

( x in b

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

redefine func less_eq_dom (f,a) -> Subset of X;

coherence

less_eq_dom (f,a) is Subset of X

redefine func great_dom (f,a) -> Subset of X;

coherence

great_dom (f,a) is Subset of X

redefine func great_eq_dom (f,a) -> Subset of X;

coherence

great_eq_dom (f,a) is Subset of X

redefine func eq_dom (f,a) -> Subset of X;

coherence

eq_dom (f,a) is Subset of X

end;
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_domredefine func less_eq_dom (f,a) -> Subset of X;

coherence

less_eq_dom (f,a) is Subset of X

proof end;

:: original: great_domredefine func great_dom (f,a) -> Subset of X;

coherence

great_dom (f,a) is Subset of X

proof end;

:: original: great_eq_domredefine func great_eq_dom (f,a) -> Subset of X;

coherence

great_eq_dom (f,a) is Subset of X

proof end;

:: original: eq_domredefine func eq_dom (f,a) -> Subset of X;

coherence

eq_dom (f,a) is Subset of X

proof end;

theorem Th14: :: MESFUNC1:14

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

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 Th15: :: MESFUNC1:15

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

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 Th16: :: MESFUNC1:16

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

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 Th17: :: MESFUNC1:17

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

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

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

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

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)

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 Th20: :: MESFUNC1:20

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)

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 Th21: :: MESFUNC1:21

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)

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 Th22: :: MESFUNC1:22

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)

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

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 Th24: :: MESFUNC1:24

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)

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 Th25: :: MESFUNC1:25

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)

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

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;

end;
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 :Def16: :: MESFUNC1:def 16

for r being real number holds A /\ (less_dom (f,(R_EAL r))) in S;

for r being real number holds A /\ (less_dom (f,(R_EAL r))) in S;

:: deftheorem Def16 defines is_measurable_on MESFUNC1:def 16 :

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

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

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 )

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 Th28: :: MESFUNC1:28

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 )

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 Th29: :: MESFUNC1:29

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 )

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

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

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

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

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

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

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: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 f is_measurable_on A & A c= dom f holds

A /\ (eq_dom (f,+infty)) in S

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

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

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

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

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

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

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

for r being Real st f is_measurable_on A & A c= dom f holds

r (#) f is_measurable_on A

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;