:: Definitions and Basic Properties of Measurable Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received September 7, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, INT_1, RAT_1, ARYTM_1, CARD_1,
XBOOLE_0, TARSKI, FUNCT_1, FUNCT_2, RELAT_1, NAT_1, ARYTM_3, ZFMISC_1,
CARD_3, ORDINAL1, PARTFUN1, XXREAL_0, VALUED_1, SUPINF_2, SUPINF_1,
COMPLEX1, PROB_1, VALUED_0, SETFAM_1, MESFUNC1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XXREAL_3, XCMPLX_0, XREAL_0, MEASURE6, REAL_1, RELAT_1, FUNCT_1,
PARTFUN1, FUNCT_2, INT_1, NAT_1, RAT_1, CARD_3, XXREAL_0, VALUED_0,
PROB_1, SUPINF_1, SUPINF_2, MEASURE2, MEASURE3, EXTREAL1, RELSET_2;
constructors WELLORD2, REAL_1, NAT_1, RAT_1, MEASURE3, MEASURE6, EXTREAL1,
SUPINF_1, RELSET_2, PARTFUN1, EQREL_1, RELAT_2, RELSET_1, BINOP_2,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, INT_1, CARD_1, MEMBERED, MEASURE1, VALUED_0, XXREAL_3,
FUNCT_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI;
equalities RELAT_1, SUPINF_2;
expansions TARSKI;
theorems MEASURE1, TARSKI, SUBSET_1, PARTFUN1, FUNCT_1, FUNCT_2, MEASURE5,
SETFAM_1, NAT_1, INT_1, CARD_1, CARD_4, WELLORD2, RAT_1, XREAL_0,
XBOOLE_0, XBOOLE_1, XCMPLX_1, NUMBERS, XREAL_1, FINSUB_1, PROB_1,
XXREAL_0, ORDINAL1, CARD_3, XXREAL_3, RELAT_1, CARD_2, EXTREAL1;
schemes SUBSET_1, FUNCT_2, SEQ_1, XBOOLE_0;
begin :: Cardinal numbers of INT and RAT
reserve k for Element of NAT;
reserve r,r1 for Real;
reserve i for Integer;
reserve q for Rational;
definition
func INT- -> Subset of REAL means
:Def1:
r in it iff ex k st r = - k;
existence
proof
defpred P[Element of REAL] means ex k st $1 = -k;
consider IT being Subset of REAL such that
A1: for r being Element of REAL holds r in IT iff P[r] from SUBSET_1:sch 3;
take IT;
let r;
r in REAL by XREAL_0:def 1;
hence thesis by A1;
end;
uniqueness
proof
let D1,D2 be Subset of REAL such that
A2: r in D1 iff ex k st r = - k and
A3: r in D2 iff ex k st r = - k;
for r being Element of REAL holds r in D1 iff r in D2
proof
let r be Element of REAL;
thus r in D1 implies r in D2
proof
assume r in D1;
then ex k st r = - k by A2;
hence thesis by A3;
end;
assume r in D2;
then ex k st r = - k by A3;
hence thesis by A2;
end;
hence thesis by SUBSET_1:3;
end;
correctness;
end;
Lm1: 0 = -0;
registration
cluster INT- -> non empty;
coherence by Def1,Lm1;
end;
theorem Th1:
NAT,INT- are_equipotent
proof
defpred P[Element of NAT,set] means $2=-$1;
A1: for x being Element of NAT ex y being Element of INT- st P[x,y]
proof
let x be Element of NAT;
-x in INT- by Def1;
hence thesis;
end;
consider f being sequence of INT- such that
A2: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(A1);
A3: f in Funcs(NAT,INT-) by FUNCT_2:8;
then A4: dom f = NAT by FUNCT_2:92;
A5: for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1=f.x2
holds x1=x2
proof
let x1,x2 be object;
assume that
A6: x1 in dom f and
A7: x2 in dom f and
A8: f.x1=f.x2;
reconsider x1 as Element of NAT by A3,A6,FUNCT_2:92;
reconsider x2 as Element of NAT by A3,A7,FUNCT_2:92;
f.x1 = -x1 & f.x2 = -x2 by A2;
then --x1=x2 by A8;
hence thesis;
end;
A9: for y being object st y in INT- holds f"{y} <> {}
proof
let y being object;
assume
A10: y in INT-;
then reconsider y as Real;
consider k being Element of NAT such that
A11: y = -k by A10,Def1;
f.k = -k by A2;
then f.k in {y} by A11,TARSKI:def 1;
hence thesis by A4,FUNCT_1:def 7;
end;
A12: f is one-to-one by A5,FUNCT_1:def 4;
rng f = INT- by A9,FUNCT_2:41;
hence thesis by A4,A12,WELLORD2:def 4;
end;
theorem Th2:
INT=INT- \/ NAT
proof
for x being object st x in INT holds x in INT- \/ NAT
proof
let x be object;
assume x in INT;
then consider k being Nat such that
A1: x = k or x = - k by INT_1:def 1;
A2: k in NAT by ORDINAL1:def 12;
per cases by A1;
suppose
x = k;
hence thesis by XBOOLE_0:def 3,A2;
end;
suppose
x = -k;
then x in INT- by Def1,A2;
hence thesis by XBOOLE_0:def 3;
end;
end;
then A3: INT c= INT- \/ NAT;
for x being object st x in INT- \/ NAT holds x in INT
proof
let x be object;
assume
A4: x in INT- \/ NAT;
now per cases by A4,XBOOLE_0:def 3;
suppose
x in INT-;
then ex k being Element of NAT st x = -k by Def1;
hence thesis by INT_1:def 1;
end;
suppose
x in NAT;
hence thesis by INT_1:def 1;
end;
end;
hence thesis;
end;
then INT- \/ NAT c= INT;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th3:
NAT,INT are_equipotent by Th1,Th2,CARD_2:77;
definition
let n be Nat;
func RAT_with_denominator n -> Subset of RAT means
:Def2:
q in it iff ex i st q = i/n;
existence
proof
defpred P[Element of RAT] means ex i st $1 = i/n;
consider X being Subset of RAT such that
A1: for r being Element of RAT holds r in X iff P[r] from SUBSET_1:sch 3;
A2: for q being Rational holds q in X iff ex i st q = i/n
proof
let q be Rational;
reconsider q as Element of RAT by RAT_1:def 2;
q in X iff ex i st q = i/n by A1;
hence thesis;
end;
take X;
thus thesis by A2;
end;
uniqueness
proof
let D1,D2 be Subset of RAT such that
A3: q in D1 iff ex i st q = i/n and
A4: q in D2 iff ex i st q = i/n;
for q being Element of RAT holds q in D1 iff q in D2
proof
let q be Element of RAT;
thus q in D1 implies q in D2
proof
assume
A5: q in D1;
reconsider q as Rational;
ex i st q = i/n by A3,A5;
hence thesis by A4;
end;
assume
A6: q in D2;
reconsider q as Rational;
ex i st q = i/n by A4,A6;
hence thesis by A3;
end;
hence thesis by SUBSET_1:3;
end;
end;
registration
let n be Nat;
cluster RAT_with_denominator(n+1) -> non empty;
coherence
proof
reconsider i1=n+1 as Integer;
reconsider q=0/i1 as Rational;
q in RAT_with_denominator(n+1) by Def2;
hence thesis;
end;
end;
theorem Th4:
for n being Nat holds INT,RAT_with_denominator (n+1) are_equipotent
proof
let n be Nat;
defpred P[Element of INT,set] means $2=$1/(n+1);
A1: for x being Element of INT ex y being Element of RAT_with_denominator(n+1)
st P[x,y]
proof
let x be Element of INT;
reconsider x as Integer;
reconsider i1=n+1 as Integer;
set y=x/i1;
y in RAT by RAT_1:def 1;
then reconsider y as Rational;
y in RAT_with_denominator(n+1) by Def2;
hence thesis;
end;
consider f being Function of INT,RAT_with_denominator(n+1) such that
A2: for x being Element of INT holds P[x,f.x] from FUNCT_2:sch 3(A1);
A3: f in Funcs(INT,RAT_with_denominator(n+1)) by FUNCT_2:8;
then A4: dom f = INT by FUNCT_2:92;
A5: for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1=f.x2
holds x1=x2
proof
let x1,x2 be object;
assume that
A6: x1 in dom f and
A7: x2 in dom f and
A8: f.x1=f.x2;
reconsider x1 as Element of INT by A3,A6,FUNCT_2:92;
reconsider x2 as Element of INT by A3,A7,FUNCT_2:92;
f.x1 = x1/(n+1) & f.x2 = x2/(n+1) by A2;
hence thesis by A8,XCMPLX_1:53;
end;
A9: for y being object st y in RAT_with_denominator(n+1) holds f"{y} <> {}
proof
let y being object;
assume
A10: y in RAT_with_denominator(n+1);
then reconsider y as Rational;
consider i being Integer such that
A11: y = i/(n+1) by A10,Def2;
reconsider i as Element of INT by INT_1:def 2;
f.i = i/(n+1) by A2;
then f.i in {y} by A11,TARSKI:def 1;
hence thesis by A4,FUNCT_1:def 7;
end;
A12: f is one-to-one by A5,FUNCT_1:def 4;
rng f = RAT_with_denominator(n+1) by A9,FUNCT_2:41;
hence thesis by A4,A12,WELLORD2:def 4;
end;
theorem
NAT,RAT are_equipotent
proof
assume
A1: not NAT,RAT are_equipotent;
defpred P[Element of NAT,Subset of REAL] means
$2 = RAT_with_denominator ($1+1);
A2: for n being Element of NAT ex X being Subset of REAL st P[n,X]
proof
let n be Element of NAT;
for x being object st x in RAT_with_denominator (n+1) holds
x in REAL by NUMBERS:12;
then reconsider X=RAT_with_denominator (n+1) as Subset of REAL
by TARSKI:def 3;
take X;
thus thesis;
end;
consider F being sequence of bool REAL such that
A3: for n being Element of NAT holds P[n,F.n] from FUNCT_2:sch 3(A2);
for x being object st x in union rng F holds x in RAT
proof
let x being object;
assume x in union rng F;
then consider Y being set such that
A4: x in Y and
A5: Y in rng F by TARSKI:def 4;
dom F = NAT by FUNCT_2:def 1;
then consider n being object such that
A6: n in NAT and
A7: F.n = Y by A5,FUNCT_1:def 3;
reconsider n as Element of NAT by A6;
Y = RAT_with_denominator (n+1) by A3,A7;
hence thesis by A4;
end;
then A8: union rng F c= RAT;
for x being object st x in RAT holds x in union rng F
proof
let x be object;
assume x in RAT;
then reconsider x as Rational;
A9: dom F = NAT by FUNCT_2:def 1;
denominator x <> 0 by RAT_1:def 3;
then consider m being Nat such that
A10: denominator x = m + 1 by NAT_1:6;
reconsider m as Element of NAT by ORDINAL1:def 12;
denominator x = m + 1 by A10;
then reconsider n = denominator x - 1 as Element of NAT;
x = (numerator x)/(n+1) by RAT_1:15;
then x in RAT_with_denominator (n+1) by Def2;
then A11: x in F.n by A3;
F.n in rng F by A9,FUNCT_1:def 3;
hence thesis by A11,TARSKI:def 4;
end;
then RAT c= union rng F;
then A12: union rng F = RAT by A8,XBOOLE_0:def 10;
dom F = NAT by FUNCT_2:def 1;
then A13: rng F is countable by CARD_3:93;
for Y being set st Y in rng F holds Y is countable
proof
let Y be set;
assume Y in rng F;
then consider n being object such that
A14: n in dom F and
A15: F.n = Y by FUNCT_1:def 3;
reconsider n as Element of NAT by A14,FUNCT_2:def 1;
Y = RAT_with_denominator (n+1) by A3,A15;
then INT,Y are_equipotent by Th4;
then NAT,Y are_equipotent by Th3,WELLORD2:15;
then A16: card NAT = card Y by CARD_1:5;
thus thesis by A16,CARD_3:def 14;
end;
then RAT is countable by A12,A13,CARD_4:12;
then card RAT c= omega by CARD_3:def 14;
then not omega in card RAT;
then not omega c= card RAT or not omega <> card RAT by CARD_1:3;
then card RAT in omega by A1,CARD_1:4,5,47;
hence contradiction;
end;
begin :: Basic operations on R_EAL valued functions
definition
let C be non empty set;
let f1,f2 be C-defined ExtREAL-valued Function;
deffunc F(Element of C) = 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
proof
defpred P[Element of C] means
$1 in (dom f1 /\ dom f2)\((f1"{-infty} /\ f2"{+infty}) \/
(f1"{+infty} /\ f2"{-infty}));
consider F be PartFunc of C,ExtREAL such that
A1: for c being Element of C holds c in dom F iff P[c] and
A2: for c being Element of C st c in dom F holds F.c = F(c) from SEQ_1:sch 3;
take F;
for x being object st x in dom F holds
x in (dom f1 /\ dom f2)\((f1"{-infty} /\ f2"{+infty}) \/
(f1"{+infty} /\ f2"{-infty}))
proof
let x be object;
assume
A3: x in dom F;
dom F c= C by RELAT_1:def 18;
then reconsider x as Element of C by A3;
x in dom F by A3;
hence thesis by A1;
end;
then A4: dom F c= (dom f1 /\ dom f2)\((f1"{-infty} /\ f2"{+infty})
\/ (f1"{+infty} /\ f2"{-infty}));
for x being object
st x in (dom f1 /\ dom f2)\((f1"{-infty} /\ f2"{+infty
})\/ (f1"{+infty} /\ f2"{-infty})) holds x in dom F
proof
let x be object;
assume
A5: x in (dom f1 /\ dom f2)\((f1"{-infty} /\ f2"{+infty}) \/
(f1"{+infty} /\ f2"{-infty}));
then A6: x in dom f1 by XBOOLE_0:def 4;
dom f1 c= C by RELAT_1:def 18;
then reconsider x as Element of C by A6;
x in (dom f1 /\ dom f2)\((f1"{-infty} /\ f2"{+infty}) \/
(f1"{+infty} /\ f2"{-infty})) by A5;
hence thesis by A1;
end;
then (dom f1 /\ dom f2)\((f1"{-infty} /\ f2"{+infty}) \/
(f1"{+infty} /\ f2"{-infty})) c= dom F;
hence
dom F=(dom f1 /\ dom f2)\((f1"{-infty} /\ f2"{+infty}) \/ (f1"{+infty}
/\ f2"{-infty})) by A4,XBOOLE_0:def 10;
let c be Element of C;
assume c in dom F;
hence thesis by A2;
end;
uniqueness
proof
set X = (dom f1 /\ dom f2)\((f1"{-infty} /\ f2"{+infty}) \/ (f1"{+infty} /\
f2"{-infty}));
thus for f,g being PartFunc of C,ExtREAL st
(dom f=X & for c be Element of C st c in dom f holds f.c = F(c)) &
(dom g=X & for c be Element of C st c in dom g holds g.c = F(c))
holds f = g from SEQ_1:sch 4;
end;
commutativity;
deffunc F(Element of C) = 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
proof
defpred P[Element of C] means
$1 in (dom f1 /\ dom f2)\((f1"{+infty} /\ f2"{+infty}) \/
(f1"{-infty} /\ f2"{-infty}));
consider F be PartFunc of C,ExtREAL such that
A7: for c being Element of C holds c in dom F iff P[c] and
A8: for c being Element of C st c in dom F holds F.c = F(c) from SEQ_1:sch 3;
take F;
for x being object st x in dom F holds
x in (dom f1 /\ dom f2)\((f1"{+infty} /\ f2"{+infty}) \/
(f1"{-infty} /\ f2"{-infty}))
proof
let x be object;
assume
A9: x in dom F;
dom F c= C by RELAT_1:def 18;
then reconsider x as Element of C by A9;
x in dom F by A9;
hence thesis by A7;
end;
then A10: dom F c= (dom f1 /\ dom f2)\((f1"{+infty} /\ f2"{+infty})
\/ (f1"{-infty} /\ f2"{-infty}));
for
x being object st x in (dom f1 /\ dom f2)\((f1"{+infty} /\ f2"{+infty }
) \/ (f1"{-infty} /\ f2"{-infty})) holds x in dom F
proof
let x be object;
assume
A11: x in (dom f1 /\ dom f2)\((f1"{+infty} /\ f2"{+infty}) \/
(f1"{-infty} /\ f2"{-infty}));
then A12: x in dom f1 by XBOOLE_0:def 4;
dom f1 c= C by RELAT_1:def 18;
then reconsider x as Element of C by A12;
x in (dom f1 /\ dom f2)\((f1"{+infty} /\ f2"{+infty}) \/
(f1"{-infty} /\ f2"{-infty})) by A11;
hence thesis by A7;
end;
then (dom f1 /\ dom f2)\((f1"{+infty} /\ f2"{+infty}) \/
(f1"{-infty} /\ f2"{-infty})) c= dom F;
hence
dom F=(dom f1 /\ dom f2)\((f1"{+infty} /\ f2"{+infty}) \/ (f1"{-infty
} /\ f2"{-infty})) by A10,XBOOLE_0:def 10;
let c be Element of C;
assume c in dom F;
hence thesis by A8;
end;
uniqueness
proof
set X = (dom f1 /\ dom f2)\((f1"{+infty} /\ f2"{+infty}) \/ (f1"{-infty} /\
f2"{-infty}));
thus for f,g being PartFunc of C,ExtREAL st
(dom f=X & for c be Element of C st c in dom f holds f.c = F(c)) &
(dom g=X & for c be Element of C st c in dom g holds g.c = F(c))
holds f = g from SEQ_1:sch 4;
end;
deffunc F(Element of C) = f1.$1 * f2.$1;
func f1(#)f2 -> PartFunc of C,ExtREAL means
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
defpred P[Element of C] means $1 in dom f1 /\ dom f2;
consider F be PartFunc of C,ExtREAL such that
A13: for c being Element of C holds c in dom F iff P[c] and
A14: for c being Element of C st c in dom F holds F.c = F(c) from SEQ_1:sch 3;
take F;
for x being object st x in dom F holds x in dom f1 /\ dom f2
proof
let x be object;
assume
A15: x in dom F;
dom F c= C by RELAT_1:def 18;
then reconsider x as Element of C by A15;
x in dom F by A15;
hence thesis by A13;
end;
then A16: dom F c= dom f1 /\ dom f2;
for x being object st x in dom f1 /\ dom f2 holds x in dom F
proof
let x be object;
assume
A17: x in dom f1 /\ dom f2;
then A18: x in dom f1 by XBOOLE_0:def 4;
dom f1 c= C by RELAT_1:def 18;
then reconsider x as Element of C by A18;
x in dom f1 /\ dom f2 by A17;
hence thesis by A13;
end;
then dom f1 /\ dom f2 c= dom F;
hence dom F=dom f1 /\ dom f2 by A16,XBOOLE_0:def 10;
let c be Element of C;
assume c in dom F;
hence thesis by A14;
end;
uniqueness
proof
set X = dom f1 /\ dom f2;
thus for F,G being PartFunc of C,ExtREAL st
(dom F=X & for c be Element of C st c in dom F holds F.c = F(c)) &
(dom G=X & for c be Element of C st c in dom G holds G.c = F(c))
holds F = G from SEQ_1:sch 4;
end;
commutativity;
end;
definition
let C be non empty set,
f be C-defined ExtREAL-valued Function,
r be Real;
deffunc F(Element of C) = In(r*f.$1,ExtREAL);
func r(#)f -> PartFunc of C,ExtREAL means
:Def6:
dom it = dom f
& for c being Element of C st c in dom it holds it.c = r * f.c;
existence
proof
defpred P[Element of C] means $1 in dom f;
consider F be PartFunc of C,ExtREAL such that
A1: for c being Element of C holds c in dom F iff P[c] and
A2: for c being Element of C st c in dom F holds F.c = F(c) from SEQ_1:sch 3;
take F;
for x being object st x in dom F holds x in dom f
proof
let x be object;
assume
A3: x in dom F;
dom F c= C by RELAT_1:def 18;
then reconsider x as Element of C by A3;
x in dom F by A3;
hence thesis by A1;
end;
then A4: dom F c= dom f;
for x being object st x in dom f holds x in dom F
proof
let x be object;
assume
A5: x in dom f;
dom f c= C by RELAT_1:def 18;
then reconsider x as Element of C by A5;
x in dom f by A5;
hence thesis by A1;
end;
then dom f c= dom F;
hence dom F=dom f by A4,XBOOLE_0:def 10;
let c be Element of C;
assume c in dom F;
then F.c = F(c) by A2;
hence thesis;
end;
uniqueness
proof
set X = dom f;
deffunc F(Element of C) = r*f.$1;
thus for F,G being PartFunc of C,ExtREAL st
(dom F=X & for c be Element of C st c in dom F holds F.c = F(c)) &
(dom G=X & for c be Element of C st c in dom G holds G.c = F(c))
holds F = G from SEQ_1:sch 4;
end;
end;
theorem Th6:
for C being non empty set, f being PartFunc of C,ExtREAL, r
st r <> 0 holds
for c being Element of C st c in dom(r(#)f) holds f.c = (r(#)f).c / r
proof
let C being non empty set;
let f being PartFunc of C,ExtREAL;
let r;
assume
A1: r <> 0;
let c be Element of C;
assume c in dom(r(#)f);
then
A2: (r(#)f).c = r * f.c by Def6;
per cases;
suppose
A3: f.c = +infty;
now per cases by A1;
suppose
A4: 0. < r;
then (r(#)f).c = +infty by A2,A3,XXREAL_3:def 5;
hence thesis by A3,A4,XXREAL_3:83;
end;
suppose
A5: r < 0.;
then (r(#)f).c = -infty by A2,A3,XXREAL_3:def 5;
hence thesis by A3,A5,XXREAL_3:84;
end;
end;
hence thesis;
end;
suppose
A6: f.c = -infty;
now per cases by A1;
suppose
A7: 0. < r;
then (r(#)f).c = -infty by A2,A6,XXREAL_3:def 5;
hence thesis by A6,A7,XXREAL_3:86;
end;
suppose
A8: r < 0.;
then (r(#)f).c = +infty by A2,A6,XXREAL_3:def 5;
hence thesis by A6,A8,XXREAL_3:85;
end;
end;
hence thesis;
end;
suppose
f.c <> +infty & f.c <> -infty;
then reconsider a = f.c as Element of REAL by XXREAL_0:14;
reconsider rr=r as R_eal by XXREAL_0:def 1;
(r(#)f).c = (r qua ExtReal) * a by A2
.= r * a;
then (r(#)f).c / rr = r*a/r by EXTREAL1:2
.= a/(r/r) by XCMPLX_1:77
.= a / 1 by A1,XCMPLX_1:60;
hence thesis;
end;
end;
definition
let C be non empty set;
let f be C-defined ExtREAL-valued Function;
deffunc F(Element of C) = -(f.$1);
func -f -> PartFunc of C,ExtREAL means
dom it = dom f & for c being Element of C st c in dom it holds it.c = -(f.c);
existence
proof
defpred P[Element of C] means $1 in dom f;
consider F be PartFunc of C,ExtREAL such that
A1: for c being Element of C holds c in dom F iff P[c] and
A2: for c being Element of C st c in dom F holds F.c = F(c) from SEQ_1:sch 3;
take F;
for x being object st x in dom F holds x in dom f
proof
let x be object;
assume
A3: x in dom F;
dom F c= C by RELAT_1:def 18;
then reconsider x as Element of C by A3;
x in dom F by A3;
hence thesis by A1;
end;
then A4: dom F c= dom f;
for x being object st x in dom f holds x in dom F
proof
let x be object;
assume
A5: x in dom f;
dom f c= C by RELAT_1:def 18;
then reconsider x as Element of C by A5;
x in dom f by A5;
hence thesis by A1;
end;
then dom f c= dom F;
hence dom F=dom f by A4,XBOOLE_0:def 10;
let c be Element of C;
assume c in dom F;
hence thesis by A2;
end;
uniqueness
proof
set X = dom f;
thus for F,G being PartFunc of C,ExtREAL st
(dom F=X & for c be Element of C st c in dom F holds F.c = F(c)) &
(dom G=X & for c be Element of C st c in dom G holds G.c = F(c))
holds F = G from SEQ_1:sch 4;
end;
end;
::$CD
definition
let C be non empty set;
let f be C-defined ExtREAL-valued Function;
let r be Real;
deffunc F(Element of C) = In(r/(f.$1),ExtREAL);
func r/f -> PartFunc of C,ExtREAL means
:Def9:
dom it = dom f \ f"{0.} &
for c being Element of C st c in dom it holds it.c = r/(f.c);
existence
proof
defpred P[Element of C] means $1 in dom f \ f"{0.};
consider F be PartFunc of C,ExtREAL such that
A1: for c being Element of C holds c in dom F iff P[c] and
A2: for c being Element of C st c in dom F holds F.c = F(c) from SEQ_1:sch 3;
take F;
for x being object st x in dom F holds x in dom f \ f"{0.}
proof
let x be object;
assume
A3: x in dom F;
dom F c= C by RELAT_1:def 18;
then reconsider x as Element of C by A3;
x in dom F by A3;
hence thesis by A1;
end;
then A4: dom F c= dom f \ f"{0.};
for x being object st x in dom f \ f"{0.} holds x in dom F
proof
let x be object;
assume
A5: x in dom f \ f"{0.};
dom f c= C by RELAT_1:def 18;
then dom f \ f"{0.} c= C;
then reconsider x as Element of C by A5;
x in dom f \ f"{0.} by A5;
hence thesis by A1;
end;
then dom f \ f"{0.} c= dom F;
hence dom F=dom f \ f"{0.} by A4,XBOOLE_0:def 10;
let c be Element of C;
assume c in dom F;
then F.c = F(c) by A2;
hence thesis;
end;
uniqueness
proof
set X = dom f \ f"{0.};
deffunc F(Element of C) = r/(f.$1);
thus for F,G being PartFunc of C,ExtREAL st
(dom F=X & for c be Element of C st c in dom F holds F.c = F(c)) &
(dom G=X & for c be Element of C st c in dom G holds G.c = F(c))
holds F = G from SEQ_1:sch 4;
end;
end;
theorem
for C being non empty set, 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)
by Def9;
definition
let C be non empty set;
let f be C-defined ExtREAL-valued Function;
deffunc F(Element of C) = |. f.$1 .|;
func |.f.| -> PartFunc of C,ExtREAL means
dom it = dom f &
for c being Element of C st c in dom it holds it.c = |. f.c .|;
existence
proof
defpred P[Element of C] means $1 in dom f;
consider F be PartFunc of C,ExtREAL such that
A1: for c being Element of C holds c in dom F iff P[c] and
A2: for c being Element of C st c in dom F holds F.c = F(c) from SEQ_1:sch 3;
take F;
for x being object st x in dom F holds x in dom f
proof
let x be object;
assume
A3: x in dom F;
dom F c= C by RELAT_1:def 18;
then reconsider x as Element of C by A3;
x in dom F by A3;
hence thesis by A1;
end;
then A4: dom F c= dom f;
for x being object st x in dom f holds x in dom F
proof
let x be object;
assume
A5: x in dom f;
dom f c= C by RELAT_1:def 18;
then reconsider x as Element of C by A5;
x in dom f by A5;
hence thesis by A1;
end;
then dom f c= dom F;
hence dom F=dom f by A4,XBOOLE_0:def 10;
let c be Element of C;
assume c in dom F;
hence thesis by A2;
end;
uniqueness
proof
set X = dom f;
thus for F,G being PartFunc of C,ExtREAL st
(dom F=X & for c be Element of C st c in dom F holds F.c = F(c)) &
(dom G=X & for c be Element of C st c in dom G holds G.c = F(c))
holds F = G from SEQ_1:sch 4;
end;
end;
begin :: Level sets
theorem Th8:
ex n being Element of NAT st r <= n
proof
per cases;
suppose
[/ r \] >= 0;
then reconsider n=[/ r \] as Element of NAT by INT_1:3;
take n;
thus thesis by INT_1:def 7;
end;
suppose
A1: [/ r \] < 0;
take 0;
thus thesis by A1;
end;
end;
theorem Th9:
ex n being Nat st -n <= r
proof
[\ r /] is Element of INT by INT_1:def 2;
then A1: [\
r /] <= r & ex k being Nat st ( [\ r /] = k or [\ r /] = -k)
by INT_1:def 1,def 6;
per cases;
suppose
[\ r /] < 0;
hence thesis by A1;
end;
suppose
A2: [\ r /] >= 0;
take 0;
thus thesis by A2;
end;
end;
theorem Th10:
for r,s being Real st r < s holds
ex n being Element of NAT st 1/(n+1) < s-r
proof
let r,s be Real;
assume r < s;
then s-r > 0 by XREAL_1:50;
then consider t being Real such that
A1: 0 < t and
A2: t < s-r by XREAL_1:5;
reconsider t as Real;
A3: 1/t > 0 by A1,XREAL_1:139;
A4: [/ 1/t \] + 1 > 1/t by INT_1:32;
set n = [/ 1/t \];
reconsider n as Element of NAT by A3,INT_1:3;
(n+1)*t >= 1 by A1,A4,XREAL_1:81;
then 1/(n+1) <= t by XREAL_1:79;
then 1/(n+1) < s-r by A2,XXREAL_0:2;
hence thesis;
end;
theorem Th11:
for r,s being Real st for n being Element of NAT
holds r-1/(n+1) <= s holds r <= s
proof
let r,s be Real;
assume
A1: for n being Element of NAT holds r-1/(n+1) <= s;
assume r > s;
then consider n being Element of NAT such that
A2: 1/(n+1) < r - s by Th10;
s + 1/(n+1) < r by A2,XREAL_1:20;
then s < r - 1/(n+1) by XREAL_1:20;
hence contradiction by A1;
end;
theorem Th12:
for a being R_eal st for r being Real holds r < a
holds a = +infty
proof
let a being R_eal;
assume
A1: for r being Real holds r < a;
assume not a = +infty;
then a < +infty by XXREAL_0:4;
then consider b being R_eal such that
A2: a < b and b < +infty and
A3: b in REAL by MEASURE5:2;
reconsider b as Real by A3;
a <= b by A2;
hence contradiction by A1;
end;
theorem Th13:
for a being R_eal st for r being Real holds a < r
holds a = -infty
proof
let a being R_eal;
assume
A1: for r being Real holds a < r;
assume
A2: not a = -infty;
-infty <= a by XXREAL_0:5;
then -infty < a by A2,XXREAL_0:1;
then consider b being R_eal such that
-infty < b and
A3: b < a and
A4: b in REAL by MEASURE5:2;
reconsider b as Real by A4;
b <= a by A3;
hence contradiction by A1;
end;
reserve X for set;
reserve f for PartFunc of X,ExtREAL;
reserve S for SigmaField of X;
reserve F for sequence of S;
reserve A for set;
reserve a for ExtReal;
reserve r,s for Real;
reserve n,m for Element of NAT;
notation
let f be ext-real-valued Function, a be ExtReal;
synonym eq_dom(f,a) for Coim(f,a);
end;
definition
let f be ext-real-valued Function, a be ExtReal;
defpred P[object] means $1 in dom f & f.$1 < a;
func less_dom(f,a) -> set means :Def11:
for x being object holds x in it iff x in dom f & f.x < a;
existence
proof
consider A being set such that
A1: for x being object holds x in A iff x in dom f & P[x] from XBOOLE_0:sch 1;
take A;
thus thesis by A1;
end;
uniqueness
proof
thus for D1,D2 be set st (for x be object holds x in D1 iff P[x]) &
(for x be object holds x in D2 iff P[x]) holds D1 = D2
from XBOOLE_0:sch 3;
end;
defpred P[object] means $1 in dom f & f.$1 <= a;
func less_eq_dom(f,a) -> set means
:Def12:
for x being object holds x in it iff x in dom f & f.x <= a;
existence
proof
consider A being set such that
A2: for x being object holds x in A iff x in dom f & P[x]
from XBOOLE_0:sch 1;
take A;
thus thesis by A2;
end;
uniqueness
proof
thus for D1,D2 be set st (for x be object holds x in D1 iff P[x]) &
(for x be object holds x in D2 iff P[x]) holds D1 = D2
from XBOOLE_0:sch 3;
end;
defpred P[object] means $1 in dom f & a < f.$1;
func great_dom(f,a) -> set means
:Def13:
for x being object holds x in it iff x in dom f & a < f.x;
existence
proof
consider A being set such that
A3: for x being object holds x in A iff x in dom f & P[x] from XBOOLE_0:sch 1;
take A;
thus thesis by A3;
end;
uniqueness
proof
thus for D1,D2 be set st (for x be object holds x in D1 iff P[x]) &
(for x be object holds x in D2 iff P[x]) holds D1 = D2
from XBOOLE_0:sch 3;
end;
defpred P[object] means $1 in dom f & a <= f.$1;
func great_eq_dom(f,a) -> set means
:Def14:
for x being object holds x in it iff x in dom f & a <= f.x;
existence
proof
consider A being set such that
A4: for x being object holds x in A iff x in dom f & P[x] from XBOOLE_0:sch 1;
take A;
thus thesis by A4;
end;
uniqueness
proof
thus for D1,D2 be set st (for x be object holds x in D1 iff P[x]) &
(for x be object holds x in D2 iff P[x]) holds D1 = D2
from XBOOLE_0:sch 3;
end;
redefine func eq_dom(f,a) means :: redefines eq_dom (MESFUNC1, synonym) → Coim (RELAT_1, definition)
:Def15:
for x being set holds x in it iff x in dom f & f.x = a;
compatibility
proof
let X be set;
thus X = eq_dom(f,a) implies
for x being set holds x in X iff x in dom f & f.x = a
proof
assume
A5: X = eq_dom(f,a);
let x being set;
thus x in X implies x in dom f & f.x = a
proof
assume
A6: x in X;
hence x in dom f by A5,FUNCT_1:def 7;
f.x in {a} by A5,A6,FUNCT_1:def 7;
hence thesis by TARSKI:def 1;
end;
assume
A7: x in dom f;
assume f.x = a;
then f.x in {a} by TARSKI:def 1;
hence thesis by A5,A7,FUNCT_1:def 7;
end;
assume
A8: for x being set holds x in X iff x in dom f & f.x = a;
for x being object holds x in X iff x in dom f & f.x in {a}
proof
let x be object;
thus x in X implies x in dom f & f.x in {a}
proof
assume
A9: x in X;
hence x in dom f by A8;
f.x = a by A8,A9;
hence thesis by TARSKI:def 1;
end;
assume
A10: x in dom f;
assume f.x in {a};
then f.x = a by TARSKI:def 1;
hence thesis by A8,A10;
end;
hence thesis by FUNCT_1:def 7;
end;
end;
definition
let X be set, f be PartFunc of X,ExtREAL, a be ExtReal;
redefine func less_dom(f,a) -> Subset of X; :: redefines less_dom (MESFUNC1, definition)
coherence
proof
less_dom(f,a) c= X
proof
let x be object;
assume x in less_dom(f,a);
then A1: x in dom f by Def11;
dom f c= X by RELAT_1:def 18;
hence thesis by A1;
end;
hence thesis;
end;
redefine func less_eq_dom(f,a) -> Subset of X; :: redefines less_eq_dom (MESFUNC1, definition)
coherence
proof
less_eq_dom(f,a) c= X
proof
let x be object;
assume x in less_eq_dom(f,a);
then A2: x in dom f by Def12;
dom f c= X by RELAT_1:def 18;
hence thesis by A2;
end;
hence thesis;
end;
redefine func great_dom(f,a) -> Subset of X; :: redefines great_dom (MESFUNC1, definition)
coherence
proof
great_dom(f,a) c= X
proof
let x be object;
assume x in great_dom(f,a);
then A3: x in dom f by Def13;
dom f c= X by RELAT_1:def 18;
hence thesis by A3;
end;
hence thesis;
end;
redefine func great_eq_dom(f,a) -> Subset of X; :: redefines great_eq_dom (MESFUNC1, definition)
coherence
proof
great_eq_dom(f,a) c= X
proof
let x be object;
assume x in great_eq_dom(f,a);
then A4: x in dom f by Def14;
dom f c= X by RELAT_1:def 18;
hence thesis by A4;
end;
hence thesis;
end;
redefine func eq_dom(f,a) -> Subset of X; :: redefines eq_dom (MESFUNC1, redefinition) → eq_dom (MESFUNC1, synonym) → Coim (RELAT_1, definition)
coherence
proof
Coim(f,a) is Subset of X;
hence thesis;
end;
end;
theorem Th14:
A c= dom f implies A /\ great_eq_dom(f,a) = A\(A /\ less_dom(f,a))
proof
assume
A1: A c= dom f;
dom f c= X by RELAT_1:def 18;
then A2: A c= X by A1;
for x being object st x in A /\ great_eq_dom(f,a) holds x in
A\(A /\ less_dom(f,a))
proof
let x be object;
assume
A3: x in A /\ great_eq_dom(f,a);
then A4: x in A by XBOOLE_0:def 4;
x in great_eq_dom(f,a) by A3,XBOOLE_0:def 4;
then a <= f.x by Def14;
then not x in less_dom(f,a) by Def11;
then not x in (A /\ less_dom(f,a)) by XBOOLE_0:def 4;
hence thesis by A4,XBOOLE_0:def 5;
end;
then A5: A /\ great_eq_dom(f,a) c= A\(A /\ less_dom(f,a));
for x being object st x in A\(A /\ less_dom(f,a)) holds x in
A /\ great_eq_dom(f,a)
proof
let x be object;
assume
A6: x in A\(A /\ less_dom(f,a));
then A7: x in A;
not x in A /\ less_dom(f,a) by A6,XBOOLE_0:def 5;
then A8: not x in less_dom(f,a) by A6,XBOOLE_0:def 4;
reconsider x as Element of X by A2,A7;
reconsider y=f.x as R_eal;
not y < a by A1,A7,A8,Def11;
then x in great_eq_dom(f,a) by A1,A7,Def14;
hence thesis by A6,XBOOLE_0:def 4;
end;
then A\(A /\ less_dom(f,a)) c= A /\ great_eq_dom(f,a);
hence thesis by A5,XBOOLE_0:def 10;
end;
theorem Th15:
A c= dom f implies A /\ great_dom(f,a) = A\(A /\ less_eq_dom(f,a))
proof
assume
A1: A c= dom f;
dom f c= X by RELAT_1:def 18;
then A2: A c= X by A1;
for x being object st x in A /\ great_dom(f,a) holds x in
A\(A /\ less_eq_dom(f,a))
proof
let x be object;
assume
A3: x in A /\ great_dom(f,a);
then A4: x in A by XBOOLE_0:def 4;
x in great_dom(f,a) by A3,XBOOLE_0:def 4;
then a < f.x by Def13;
then not x in less_eq_dom(f,a) by Def12;
then not x in (A /\ less_eq_dom(f,a)) by XBOOLE_0:def 4;
hence thesis by A4,XBOOLE_0:def 5;
end;
then A5: A /\ great_dom(f,a) c= A\(A /\ less_eq_dom(f,a));
for x being object st x in A\(A /\ less_eq_dom(f,a)) holds x in
A /\ great_dom(f,a)
proof
let x be object;
assume
A6: x in A\(A /\ less_eq_dom(f,a));
then A7: x in A;
not x in A /\ less_eq_dom(f,a) by A6,XBOOLE_0:def 5;
then A8: not x in less_eq_dom(f,a) by A6,XBOOLE_0:def 4;
reconsider x as Element of X by A2,A7;
reconsider y=f.x as R_eal;
not y <= a by A1,A7,A8,Def12;
then x in great_dom(f,a) by A1,A7,Def13;
hence thesis by A6,XBOOLE_0:def 4;
end;
then A\(A /\ less_eq_dom(f,a)) c= A /\ great_dom(f,a);
hence thesis by A5,XBOOLE_0:def 10;
end;
theorem Th16:
A c= dom f implies A /\ less_eq_dom(f,a) = A\(A /\ great_dom(f,a))
proof
assume
A1: A c= dom f;
dom f c= X by RELAT_1:def 18;
then A2: A c= X by A1;
A3: A /\ less_eq_dom(f,a) c= A\(A /\ great_dom(f,a))
proof
let x be object;
assume
A4: x in A /\ less_eq_dom(f,a);
then A5: x in A by XBOOLE_0:def 4;
x in less_eq_dom(f,a) by A4,XBOOLE_0:def 4;
then f.x <= a by Def12;
then not x in great_dom(f,a) by Def13;
then not x in (A /\ great_dom(f,a)) by XBOOLE_0:def 4;
hence thesis by A5,XBOOLE_0:def 5;
end;
for x being object st x in A\(A /\ great_dom(f,a)) holds x in
A /\ less_eq_dom(f,a)
proof
let x be object;
assume
A6: x in A\(A /\ great_dom(f,a));
then A7: x in A;
not x in A /\ great_dom(f,a) by A6,XBOOLE_0:def 5;
then A8: not x in great_dom(f,a) by A6,XBOOLE_0:def 4;
reconsider x as Element of X by A2,A7;
reconsider y=f.x as R_eal;
not a < y by A1,A7,A8,Def13;
then x in less_eq_dom(f,a) by A1,A7,Def12;
hence thesis by A6,XBOOLE_0:def 4;
end;
then A\(A /\ great_dom(f,a)) c= A /\ less_eq_dom(f,a);
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th17:
A c= dom f implies A /\ less_dom(f,a) = A\(A /\ great_eq_dom(f,a))
proof
assume
A1: A c= dom f;
dom f c= X by RELAT_1:def 18;
then A2: A c= X by A1;
for x being object st x in A /\ less_dom(f,a) holds x in
A\(A /\ great_eq_dom(f,a))
proof
let x be object;
assume
A3: x in A /\ less_dom(f,a);
then A4: x in A by XBOOLE_0:def 4;
x in less_dom(f,a) by A3,XBOOLE_0:def 4;
then f.x < a by Def11;
then not x in great_eq_dom(f,a) by Def14;
then not x in (A /\ great_eq_dom(f,a)) by XBOOLE_0:def 4;
hence thesis by A4,XBOOLE_0:def 5;
end;
then A5: A /\ less_dom(f,a) c= A\(A /\ great_eq_dom(f,a));
for x being object st x in A\(A /\ great_eq_dom(f,a)) holds x in
A /\ less_dom(f,a)
proof
let x be object;
assume
A6: x in A\(A /\ great_eq_dom(f,a));
then A7: x in A;
not x in A /\ great_eq_dom(f,a) by A6,XBOOLE_0:def 5;
then A8: not x in great_eq_dom(f,a) by A6,XBOOLE_0:def 4;
reconsider x as Element of X by A2,A7;
reconsider y=f.x as R_eal;
not a <= y by A1,A7,A8,Def14;
then x in less_dom(f,a) by A1,A7,Def11;
hence thesis by A6,XBOOLE_0:def 4;
end;
then A\(A /\ great_eq_dom(f,a)) c= A /\ less_dom(f,a);
hence thesis by A5,XBOOLE_0:def 10;
end;
theorem
A /\ eq_dom(f,a) = A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a)
proof
for x being object st x in A /\ eq_dom(f,a) holds
x in A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a)
proof
let x be object;
assume
A1: x in A /\ eq_dom(f,a);
then A2: x in A by XBOOLE_0:def 4;
A3: x in eq_dom(f,a) by A1,XBOOLE_0:def 4;
then A4: a = f.x by Def15;
reconsider x as Element of X by A1;
A5: x in dom f by A3,Def15;
then x in great_eq_dom(f,a) by A4,Def14;
then A6: x in A /\ great_eq_dom(f,a) by A2,XBOOLE_0:def 4;
x in less_eq_dom(f,a) by A4,A5,Def12;
hence thesis by A6,XBOOLE_0:def 4;
end;
then A7: A /\ eq_dom(f,a) c= A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a);
for x being object st x in A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a)
holds
x in A /\ eq_dom(f,a)
proof
let x being object;
assume
A8: x in A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a);
then A9: x in A /\ great_eq_dom(f,a) by XBOOLE_0:def 4;
A10: x in less_eq_dom(f,a) by A8,XBOOLE_0:def 4;
A11: x in A by A9,XBOOLE_0:def 4;
x in great_eq_dom(f,a) by A9,XBOOLE_0:def 4;
then A12: a <= f.x by Def14;
A13: f.x <= a by A10,Def12;
reconsider x as Element of X by A8;
A14: x in dom f by A10,Def12;
a = f.x by A12,A13,XXREAL_0:1;
then x in eq_dom(f,a) by A14,Def15;
hence thesis by A11,XBOOLE_0:def 4;
end;
then
A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a) c= A /\ eq_dom(f,a);
hence thesis by A7,XBOOLE_0:def 10;
end;
theorem
for X, S, F, f, A, r st for n holds F.n = A /\ great_dom(f,(r-1/(n+1)))
holds A /\ great_eq_dom(f,r) = meet rng F
proof
let X,S,F,f,A,r;
assume
A1: for n holds F.n = A /\ great_dom(f,(r-1/(n+1)));
for
x being object st x in A /\ great_eq_dom(f,r) holds x in meet rng F
proof
let x be object;
assume
A2: x in A /\ great_eq_dom(f,r);
then A3: x in A by XBOOLE_0:def 4;
A4: x in great_eq_dom(f,r) by A2,XBOOLE_0:def 4;
for Y being set holds Y in rng F implies x in Y
proof
let Y be set;
Y in rng F implies x in Y
proof
assume Y in rng F;
then consider m being Element of NAT such that
m in dom F and
A5: Y = F.m by PARTFUN1:3;
A6: Y = A /\ great_dom(f,(r-1/(m+1))) by A1,A5;
A7: x in dom f by A4,Def14;
reconsider x as Element of X by A2;
A8: r <= f.x by A4,Def14;
(m+1)" > 0;
then 1/(m+1) > 0 by XCMPLX_1:215;
then r < r+1/(m+1) by XREAL_1:29;
then (r-1/(m+1))< r by XREAL_1:19;
then (r-1/(m+1)) < f.x by A8,XXREAL_0:2;
then x in great_dom(f,(r-1/(m+1))) by A7,Def13;
hence thesis by A3,A6,XBOOLE_0:def 4;
end;
hence thesis;
end;
hence thesis by SETFAM_1:def 1;
end;
then A9: A /\ great_eq_dom(f,r) c= meet rng F;
for x being object st x in meet rng F holds x in A /\ great_eq_dom(f,r)
proof
let x be object;
assume
A10: x in meet rng F;
A11: for m holds x in A & x in dom f & (r-1/(m+1)) < f.x
proof
let m;
m in NAT;
then m in dom F by FUNCT_2:def 1;
then F.m in rng F by FUNCT_1:def 3;
then x in F.m by A10,SETFAM_1:def 1;
then A12: x in A /\ great_dom(f,(r-1/(m+1))) by A1;
then x in great_dom(f,(r-1/(m+1))) by XBOOLE_0:def 4;
hence thesis by A12,Def13,XBOOLE_0:def 4;
end;
reconsider y=f.x as R_eal by XXREAL_0:def 1;
1 in NAT;
then 1 in dom F by FUNCT_2:def 1;
then F.1 in rng F by FUNCT_1:def 3;
then x in F.1 by A10,SETFAM_1:def 1;
then x in A /\ great_dom(f,(r-1/(1+1))) by A1;
then reconsider x as Element of X;
r <= y
proof
now per cases;
suppose
y=+infty;
hence thesis by XXREAL_0:4;
end;
suppose
not y=+infty;
then A13: not +infty <= y by XXREAL_0:4;
(r-1/(1+1))<y by A11;
then reconsider y1=y as Element of REAL by A13,XXREAL_0:48;
for m holds r-1/(m+1) <= y1
by A11;
hence thesis by Th11;
end;
end;
hence thesis;
end;
then x in great_eq_dom(f,r) by A11,Def14;
hence thesis by A11,XBOOLE_0:def 4;
end;
then meet rng F c= A /\ great_eq_dom(f,r);
hence thesis by A9,XBOOLE_0:def 10;
end;
theorem Th20:
for r being Real st for n holds F.n = A /\ less_dom(f,(r+1/(n+1)))
holds A /\ less_eq_dom(f,r) = meet rng F
proof
let r be Real;
assume
A1: for n holds F.n = A /\ less_dom(f,(r+1/(n+1)));
for x being object st x in A /\ less_eq_dom(f,r) holds x in meet rng F
proof
let x be object;
assume
A2: x in A /\ less_eq_dom(f,r);
then A3: x in A by XBOOLE_0:def 4;
A4: x in less_eq_dom(f,r) by A2,XBOOLE_0:def 4;
for Y being set holds Y in rng F implies x in Y
proof
let Y be set;
Y in rng F implies x in Y
proof
assume Y in rng F;
then consider m being Element of NAT such that
m in dom F and
A5: Y = F.m by PARTFUN1:3;
A6: Y = A /\ less_dom(f,(r+1/(m+1))) by A1,A5;
A7: x in dom f by A4,Def12;
reconsider x as Element of X by A2;
A8: f.x <= r by A4,Def12;
(m+1)" > 0;
then 1/(m+1) > 0 by XCMPLX_1:215;
then r < (r+1/(m+1)) by XREAL_1:29;
then f.x < (r+1/(m+1)) by A8,XXREAL_0:2;
then x in less_dom(f,(r+1/(m+1))) by A7,Def11;
hence thesis by A3,A6,XBOOLE_0:def 4;
end;
hence thesis;
end;
hence thesis by SETFAM_1:def 1;
end;
then A9: A /\ less_eq_dom(f,r) c= meet rng F;
for
x being object st x in meet rng F holds x in A /\ less_eq_dom(f,r)
proof
let x be object;
assume
A10: x in meet rng F;
A11: for m holds x in A & x in dom f & f.x < (r+1/(m+1))
proof
let m;
m in NAT;
then m in dom F by FUNCT_2:def 1;
then F.m in rng F by FUNCT_1:def 3;
then x in F.m by A10,SETFAM_1:def 1;
then A12: x in A /\ less_dom(f,(r+1/(m+1))) by A1;
then x in less_dom(f,(r+1/(m+1))) by XBOOLE_0:def 4;
hence thesis by A12,Def11,XBOOLE_0:def 4;
end;
reconsider y=f.x as R_eal by XXREAL_0:def 1;
1 in NAT;
then 1 in dom F by FUNCT_2:def 1;
then F.1 in rng F by FUNCT_1:def 3;
then x in F.1 by A10,SETFAM_1:def 1;
then x in A /\ less_dom(f,(r+1/(1+1))) by A1;
then reconsider x as Element of X;
y <= r
proof
now per cases;
suppose
y=-infty;
hence thesis by XXREAL_0:5;
end;
suppose
not y=-infty;
then A13: not y <= -infty by XXREAL_0:6;
y < (r+1/(1+1)) by A11;
then reconsider y1=y as Element of REAL by A13,XXREAL_0:48;
for m holds y1-1/(m+1) <= r
proof
let m;
y1 < (r+1/(m+1)) by A11;
hence thesis by XREAL_1:20;
end;
hence thesis by Th11;
end;
end;
hence thesis;
end;
then x in less_eq_dom(f,r) by A11,Def12;
hence thesis by A11,XBOOLE_0:def 4;
end;
then meet rng F c= A /\ less_eq_dom(f,r);
hence thesis by A9,XBOOLE_0:def 10;
end;
theorem Th21:
for r being Real st for n
holds F.n = A /\ less_eq_dom(f,(r-1/(n+1)))
holds A /\ less_dom(f,r) = union rng F
proof
let r be Real;
assume
A1: for n holds F.n = A /\ less_eq_dom(f,(r-1/(n+1)));
for x being object st x in A /\ less_dom(f,r) holds x in union rng F
proof
let x be object;
assume
A2: x in A /\ less_dom(f,r);
then A3: x in A by XBOOLE_0:def 4;
A4: x in less_dom(f,r) by A2,XBOOLE_0:def 4;
ex Y being set st x in Y & Y in rng F
proof
reconsider x as Element of X by A2;
A5: x in dom f by A4,Def11;
A6: f.x < r by A4,Def11;
ex m st f.x <= (r-1/(m+1))
proof
per cases;
suppose
A7: f.x = -infty;
take 1;
thus thesis by A7,XXREAL_0:5;
end;
suppose
not f.x =-infty;
then not f.x <= -infty by XXREAL_0:6;
then reconsider y1=f.x as Element of REAL by A6,XXREAL_0:48;
consider m such that
A8: 1/(m+1) < r-y1 by A6,Th10;
y1+1/(m+1) < r by A8,XREAL_1:20;
then f.x <= (r-1/(m+1)) by XREAL_1:20;
hence thesis;
end;
end;
then consider m such that
A9: f.x <= (r-1/(m+1));
x in less_eq_dom(f,(r-1/(m+1))) by A5,A9,Def12;
then A10: x in A /\ less_eq_dom(f,(r-1/(m+1))) by A3,XBOOLE_0:def 4;
m in NAT;
then A11: m in dom F by FUNCT_2:def 1;
take F.m;
thus thesis by A1,A10,A11,FUNCT_1:def 3;
end;
hence thesis by TARSKI:def 4;
end;
then A12: A /\ less_dom(f,r) c= union rng F;
for x being object st x in union rng F holds x in A /\ less_dom(f,r )
proof
let x be object;
assume x in union rng F;
then consider Y being set such that
A13: x in Y and
A14: Y in rng F by TARSKI:def 4;
consider m such that
m in dom F and
A15: F.m = Y by A14,PARTFUN1:3;
A16: x in A /\ less_eq_dom(f,(r-1/(m+1))) by A1,A13,A15;
then A17: x in A by XBOOLE_0:def 4;
A18: x in less_eq_dom(f,(r-1/(m+1))) by A16,XBOOLE_0:def 4;
then A19: x in dom f by Def12;
A20: f.x <= (r-1/(m+1)) by A18,Def12;
reconsider x as Element of X by A13,A14;
f.x < r
proof
now
r < r+1/(m+1) by XREAL_1:29,139;
then r-1/(m+1) < r by XREAL_1:19;
hence thesis by A20,XXREAL_0:2;
end;
hence thesis;
end;
then x in less_dom(f,r) by A19,Def11;
hence thesis by A17,XBOOLE_0:def 4;
end;
then union rng F c= A /\ less_dom(f,r);
hence thesis by A12,XBOOLE_0:def 10;
end;
theorem Th22:
for X, S, F, f, A, r st for n holds F.n = A /\
great_eq_dom(f,(r+1/(n+1)))
holds A /\ great_dom(f,r) = union rng F
proof
let X,S,F,f,A,r;
assume
A1: for n holds F.n = A /\ great_eq_dom(f,(r+1/(n+1)));
for x being object st x in A /\ great_dom(f,r) holds x in union rng F
proof
let x be object;
assume
A2: x in A /\ great_dom(f,r);
then A3: x in A by XBOOLE_0:def 4;
A4: x in great_dom(f,r) by A2,XBOOLE_0:def 4;
ex Y being set st x in Y & Y in rng F
proof
reconsider x as Element of X by A2;
A5: x in dom f by A4,Def13;
A6: r < f.x by A4,Def13;
ex m st (r+1/(m+1)) <= f.x
proof
per cases;
suppose
A7: f.x = +infty;
take 1;
thus thesis by A7,XXREAL_0:4;
end;
suppose
not f.x=+infty;
then not +infty <= f.x by XXREAL_0:4;
then reconsider y1=f.x as Element of REAL by A6,XXREAL_0:48;
consider m such that
A8: 1/(m+1) < y1-r by A6,Th10;
take m;
thus thesis by A8,XREAL_1:20;
end;
end;
then consider m such that
A9: (r+1/(m+1)) <= f.x;
x in great_eq_dom(f,(r+1/(m+1))) by A5,A9,Def14;
then A10: x in A /\ great_eq_dom(f,(r+1/(m+1))) by A3,XBOOLE_0:def 4;
m in NAT;
then A11: m in dom F by FUNCT_2:def 1;
take F.m;
thus thesis by A1,A10,A11,FUNCT_1:def 3;
end;
hence thesis by TARSKI:def 4;
end;
then A12: A /\ great_dom(f,r) c= union rng F;
for
x being object st x in union rng F holds x in A /\ great_dom(f,r )
proof
let x be object;
assume x in union rng F;
then consider Y being set such that
A13: x in Y and
A14: Y in rng F by TARSKI:def 4;
consider m such that
m in dom F and
A15: F.m = Y by A14,PARTFUN1:3;
A16: x in A /\ great_eq_dom(f,(r+1/(m+1))) by A1,A13,A15;
then A17: x in A by XBOOLE_0:def 4;
A18: x in great_eq_dom(f,(r+1/(m+1))) by A16,XBOOLE_0:def 4;
then A19: x in dom f by Def14;
A20: (r+1/(m+1)) <= f.x by A18,Def14;
reconsider x as Element of X by A13,A14;
r < f.x
proof
now
r < r+1/(m+1) by XREAL_1:29,139;
hence thesis by A20,XXREAL_0:2;
end;
hence thesis;
end;
then x in great_dom(f,r) by A19,Def13;
hence thesis by A17,XBOOLE_0:def 4;
end;
then union rng F c= A /\ great_dom(f,r);
hence thesis by A12,XBOOLE_0:def 10;
end;
theorem Th23:
for X, S, F, f, A st for n holds F.n = A /\ great_dom(f,n)
holds A /\ eq_dom(f,+infty) = meet rng F
proof
let X,S,F,f,A;
assume
A1: for n holds F.n = A /\ great_dom(f,n);
for x being object st x in A /\ eq_dom(f,+infty) holds x in meet rng F
proof
let x being object;
assume
A2: x in A /\ eq_dom(f,+infty);
then A3: x in A by XBOOLE_0:def 4;
A4: x in eq_dom(f,+infty) by A2,XBOOLE_0:def 4;
for Y being set holds Y in rng F implies x in Y
proof
let Y be set;
Y in rng F implies x in Y
proof
assume Y in rng F;
then consider m being Element of NAT such that
m in dom F and
A5: Y = F.m by PARTFUN1:3;
A6: Y = A /\ great_dom(f,m) by A1,A5;
reconsider x as Element of X by A2;
A7: f.x = +infty by A4,Def15;
m in REAL by XREAL_0:def 1;
then x in dom f & not +infty <= m by A4,Def15,XXREAL_0:9;
then x in great_dom(f,m) by A7,Def13;
hence thesis by A3,A6,XBOOLE_0:def 4;
end;
hence thesis;
end;
hence thesis by SETFAM_1:def 1;
end;
then A8: A /\ eq_dom(f,+infty) c= meet rng F;
for x being object st x in meet rng F holds x in A /\ eq_dom(f,+infty)
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume
A9: x in meet rng F;
A10: for m holds x in A & x in dom f & ex y being R_eal st y=f.x & y = +infty
proof
let m;
m in NAT;
then m in dom F by FUNCT_2:def 1;
then F.m in rng F by FUNCT_1:def 3;
then x in F.m by A9,SETFAM_1:def 1;
then A11: x in A /\ great_dom(f,m) by A1;
then A12: x in great_dom(f,m) by XBOOLE_0:def 4;
for r holds r < f.xx
proof
let r;
consider n such that
A13: r <= n by Th8;
n in NAT;
then n in dom F by FUNCT_2:def 1;
then F.n in rng F by FUNCT_1:def 3;
then x in F.n by A9,SETFAM_1:def 1;
then x in A /\ great_dom(f,n) by A1;
then x in great_dom(f,n) by XBOOLE_0:def 4;
then n < f.x by Def13;
hence thesis by A13,XXREAL_0:2;
end;
then f.x = +infty by Th12;
hence thesis by A11,A12,Def13,XBOOLE_0:def 4;
end;
1 in NAT;
then 1 in dom F by FUNCT_2:def 1;
then F.1 in rng F by FUNCT_1:def 3;
then x in F.1 by A9,SETFAM_1:def 1;
then x in A /\ great_dom(f,1) by A1;
then reconsider x as Element of X;
x in eq_dom(f,+infty) by A10,Def15;
hence thesis by A10,XBOOLE_0:def 4;
end;
then meet rng F c= A /\ eq_dom(f,+infty);
hence thesis by A8,XBOOLE_0:def 10;
end;
theorem Th24:
for X, S, F, f, A st for n holds F.n = A /\ less_dom(f,n)
holds A /\ less_dom(f,+infty) = union rng F
proof
let X,S,F,f,A;
assume
A1: for n holds F.n = A /\ less_dom(f,n);
for x being object st x in A /\ less_dom(f,+infty) holds x in union rng F
proof
let x be object;
assume
A2: x in A /\ less_dom(f,+infty);
then A3: x in A by XBOOLE_0:def 4;
A4: x in less_dom(f,+infty) by A2,XBOOLE_0:def 4;
then A5: x in dom f by Def11;
A6: f.x < +infty by A4,Def11;
ex n being Element of NAT st f.x < n
proof
per cases;
suppose
A7: f.x = -infty;
take 0;
thus thesis by A7;
end;
suppose
not f.x = -infty;
then not f.x <= -infty by XXREAL_0:6;
then reconsider y1=f.x as Element of REAL by A6,XXREAL_0:48;
consider n1 being Element of NAT such that
A8: y1 <= n1 by Th8;
A9: n1 < n1+1 by NAT_1:13;
reconsider m=n1+1 as Element of NAT;
take m;
thus thesis by A8,A9,XXREAL_0:2;
end;
end;
then consider n being Element of NAT such that
A10: f.x < n;
reconsider x as Element of X by A2;
x in less_dom(f,n) by A5,A10,Def11;
then x in A /\ less_dom(f,n) by A3,XBOOLE_0:def 4;
then A11: x in F.n by A1;
n in NAT;
then n in dom F by FUNCT_2:def 1;
then F.n in rng F by FUNCT_1:def 3;
hence thesis by A11,TARSKI:def 4;
end;
then A12: A /\ less_dom(f,+infty) c= union rng F;
for x being object st x in union rng F holds x in A /\ less_dom(f,+infty)
proof
let x being object;
assume x in union rng F;
then consider Y being set such that
A13: x in Y and
A14: Y in rng F by TARSKI:def 4;
consider m such that
m in dom F and
A15: F.m = Y by A14,PARTFUN1:3;
A16: x in A /\ less_dom(f,m) by A1,A13,A15;
then A17: x in A by XBOOLE_0:def 4;
A18: x in less_dom(f,m) by A16,XBOOLE_0:def 4;
then A19: x in dom f by Def11;
A20: f.x < m by A18,Def11;
reconsider x as Element of X by A13,A14;
m in REAL by XREAL_0:def 1;
then f.x < +infty by A20,XXREAL_0:2,9;
then x in less_dom(f,+infty) by A19,Def11;
hence thesis by A17,XBOOLE_0:def 4;
end;
then union rng F c= A /\ less_dom(f,+infty);
hence thesis by A12,XBOOLE_0:def 10;
end;
theorem Th25:
for X, S, F, f, A st for n being Nat holds F.n = A /\ less_dom(f,(-n))
holds A /\ eq_dom(f,-infty) = meet rng F
proof
let X,S,F,f,A;
assume
A1: for n being Nat holds F.n = A /\ less_dom(f,(-n));
for x being object st x in A /\ eq_dom(f,-infty) holds x in meet rng F
proof
let x being object;
assume
A2: x in A /\ eq_dom(f,-infty);
then A3: x in A by XBOOLE_0:def 4;
A4: x in eq_dom(f,-infty) by A2,XBOOLE_0:def 4;
for Y being set holds Y in rng F implies x in Y
proof
let Y be set;
Y in rng F implies x in Y
proof
assume Y in rng F;
then consider m being Element of NAT such that
m in dom F and
A5: Y = F.m by PARTFUN1:3;
A6: Y = A /\ less_dom(f,(-m)) by A1,A5;
reconsider x as Element of X by A2;
A7: f.x = -infty by A4,Def15;
-m in REAL by XREAL_0:def 1;
then x in dom f & not (-m) <= -infty by A4,Def15,XXREAL_0:12;
then x in less_dom(f,(-m)) by A7,Def11;
hence thesis by A3,A6,XBOOLE_0:def 4;
end;
hence thesis;
end;
hence thesis by SETFAM_1:def 1;
end;
then A8: A /\ eq_dom(f,-infty) c= meet rng F;
for x being object st x in meet rng F holds x in A /\ eq_dom(f,-infty)
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume
A9: x in meet rng F;
A10: for m holds x in A & x in dom f & ex y being R_eal st y=f.x & y = -infty
proof
let m;
m in NAT;
then m in dom F by FUNCT_2:def 1;
then F.m in rng F by FUNCT_1:def 3;
then x in F.m by A9,SETFAM_1:def 1;
then A11: x in A /\ less_dom(f,(-m)) by A1;
then A12: x in less_dom(f,(-m)) by XBOOLE_0:def 4;
for r holds f.xx < r
proof
let r;
consider n being Nat such that
A13: -n <= r by Th9;
n in NAT by ORDINAL1:def 12;
then n in dom F by FUNCT_2:def 1;
then F.n in rng F by FUNCT_1:def 3;
then x in F.n by A9,SETFAM_1:def 1;
then x in A /\ less_dom(f,(-n)) by A1;
then x in less_dom(f,(-n)) by XBOOLE_0:def 4;
then f.x < (-n) by Def11;
hence thesis by A13,XXREAL_0:2;
end;
then f.x = -infty by Th13;
hence thesis by A11,A12,Def11,XBOOLE_0:def 4;
end;
1 in NAT;
then 1 in dom F by FUNCT_2:def 1;
then F.1 in rng F by FUNCT_1:def 3;
then x in F.1 by A9,SETFAM_1:def 1;
then x in A /\ less_dom(f,(-1)) by A1;
then reconsider x as Element of X;
x in eq_dom(f,-infty) by A10,Def15;
hence thesis by A10,XBOOLE_0:def 4;
end;
then meet rng F c= A /\ eq_dom(f,-infty);
hence thesis by A8,XBOOLE_0:def 10;
end;
theorem Th26:
for X, S, F, f, A st for n holds F.n = A /\ great_dom(f,(-n))
holds A /\ great_dom(f,-infty) = union rng F
proof
let X,S,F,f,A;
assume
A1: for n holds F.n = A /\ great_dom(f,(-n));
for x being object st x in A /\ great_dom(f,-infty) holds x in union rng F
proof
let x be object;
assume
A2: x in A /\ great_dom(f,-infty);
then A3: x in A by XBOOLE_0:def 4;
A4: x in great_dom(f,-infty) by A2,XBOOLE_0:def 4;
then A5: x in dom f by Def13;
A6: -infty < f.x by A4,Def13;
ex n being Element of NAT st (-n) < f.x
proof
per cases;
suppose
A7: f.x = +infty;
take 0;
thus thesis by A7;
end;
suppose
not f.x = +infty;
then not +infty <= f.x by XXREAL_0:4;
then reconsider y1=f.x as Element of REAL by A6,XXREAL_0:48;
consider n1 being Nat such that
A8: -n1 <= y1 by Th9;
n1 < n1+1 by NAT_1:13;
then A9: -(n1+1) < -n1 by XREAL_1:24;
reconsider m=n1+1 as Element of NAT;
take m;
thus thesis by A8,A9,XXREAL_0:2;
end;
end;
then consider n being Element of NAT such that
A10: (-n) < f.x;
reconsider x as Element of X by A2;
x in great_dom(f,(-n)) by A5,A10,Def13;
then x in A /\ great_dom(f,(-n)) by A3,XBOOLE_0:def 4;
then A11: x in F.n by A1;
n in NAT;
then n in dom F by FUNCT_2:def 1;
then F.n in rng F by FUNCT_1:def 3;
hence thesis by A11,TARSKI:def 4;
end;
then A12: A /\ great_dom(f,-infty) c= union rng F;
for x being object st x in union rng F holds x in A /\ great_dom(f,-infty )
proof
let x being object;
assume x in union rng F;
then consider Y being set such that
A13: x in Y and
A14: Y in rng F by TARSKI:def 4;
consider m such that
m in dom F and
A15: F.m = Y by A14,PARTFUN1:3;
A16: x in A /\ great_dom(f,(-m)) by A1,A13,A15;
then A17: x in A by XBOOLE_0:def 4;
A18: x in great_dom(f,(-m)) by A16,XBOOLE_0:def 4;
then A19: x in dom f by Def13;
A20: (-m) < f.x by A18,Def13;
reconsider x as Element of X by A13,A14;
-m in REAL by XREAL_0:def 1;
then -infty < f.x by A20,XXREAL_0:2,12;
then x in great_dom(f,-infty) by A19,Def13;
hence thesis by A17,XBOOLE_0:def 4;
end;
then union rng F c= A /\ great_dom(f,-infty);
hence thesis by A12,XBOOLE_0:def 10;
end;
begin :: Measurable functions
definition
let X be non empty set;
let S be SigmaField of X;
let A be Element of S;
let f be PartFunc of X,ExtREAL;
attr f is A-measurable means
for r being Real holds A /\ less_dom(f,r) in S;
end;
reserve X for non empty set;
reserve x for Element of X;
reserve f,g for PartFunc of X,ExtREAL;
reserve S for SigmaField of X;
reserve A,B for Element of S;
theorem
for X,S,f,A st A c= dom f holds f is A-measurable iff
for r being Real holds A /\ great_eq_dom(f,r) in S
proof
let X,S,f,A;
assume
A1: A c= dom f;
A2: f is A-measurable implies for r being Real holds A /\
great_eq_dom(f,r) in S
proof
assume
A3: f is A-measurable;
for r being Real holds A /\ great_eq_dom(f,r) in S
proof
let r be Real;
A /\ less_dom(f,r) in S & A /\ great_eq_dom(f,r) = A\(A /\
less_dom(f,r)) by A1,A3,Th14;
hence thesis by MEASURE1:6;
end;
hence thesis;
end;
(for r being Real holds A /\ great_eq_dom(f,r) in S) implies
f is A-measurable
proof
assume
A4: for r being Real holds A /\ great_eq_dom(f,r) in S;
for r being Real holds A /\ less_dom(f,r) in S
proof
let r be Real;
A /\ great_eq_dom(f,r) in S & A /\ less_dom(f,r) = A\(A /\
great_eq_dom(f,r)) by A1,A4,Th17;
hence thesis by MEASURE1:6;
end;
hence thesis;
end;
hence thesis by A2;
end;
theorem Th28:
for X,S,f,A holds f is A-measurable iff
for r being Real holds A /\ less_eq_dom(f,r) in S
proof
let X,S,f,A;
A1: f is A-measurable implies for r being Real
holds A /\ less_eq_dom(f,r) in S
proof
assume
A2: f is A-measurable;
for r being Real holds A /\ less_eq_dom(f,r) in S
proof
let r be Real;
defpred P[Element of NAT,set] means
A /\ less_dom(f,(r+1/($1+1))) = $2;
A3: for n ex y being Element of S st P[n,y]
proof
let n;
reconsider y=A /\ less_dom(f,(r+1/(n+1))) as Element of S
by A2;
take y;
thus thesis;
end;
consider F being sequence of S such that
A4: for n holds P[n,F.n] from FUNCT_2:sch 3(A3);
A /\ less_eq_dom(f,r) = meet rng F by A4,Th20;
hence thesis;
end;
hence thesis;
end;
(for r being Real holds A /\ less_eq_dom(f,r) in S) implies
f is A-measurable
proof
assume
A5: for r being Real holds A /\ less_eq_dom(f,r) in S;
for r being Real holds A /\ less_dom(f,r) in S
proof
let r be Real;
defpred P[Element of NAT,set] means
A /\ less_eq_dom(f,(r-1/($1+1))) = $2;
A6: for n ex y being Element of S st P[n,y]
proof
let n;
reconsider y=A /\ less_eq_dom(f,(r-1/(n+1))) as Element of S
by A5;
take y;
thus thesis;
end;
consider F being sequence of S such that
A7: for n holds P[n,F.n] from FUNCT_2:sch 3(A6);
A /\ less_dom(f,r) = union rng F by A7,Th21;
hence thesis;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th29:
for X,S,f,A st A c= dom f holds f is A-measurable iff
for r being Real holds A /\ great_dom(f,r) in S
proof
let X,S,f,A;
assume
A1: A c= dom f;
A2: f is A-measurable implies
for r being Real holds A /\ great_dom(f,r) in S
proof
assume
A3: f is A-measurable;
for r being Real holds A /\ great_dom(f,r) in S
proof
let r be Real;
A
/\ less_eq_dom(f,r) in S & A /\ great_dom(f,r) = A\(A /\
less_eq_dom(f,r)) by A1,A3,Th15,Th28;
hence thesis by MEASURE1:6;
end;
hence thesis;
end;
(for r being Real holds A /\ great_dom(f,r) in S)
implies f is A-measurable
proof
assume
A4: for r being Real holds A /\ great_dom(f,r) in S;
for r being Real holds A /\ less_eq_dom(f,r) in S
proof
let r be Real;
A
/\ great_dom(f,r) in S & A /\ less_eq_dom(f,r) = A\(A /\
great_dom(f,r)) by A1,A4,Th16;
hence thesis by MEASURE1:6;
end;
hence thesis by Th28;
end;
hence thesis by A2;
end;
theorem
for X,S,f,A,B st B c= A & f is A-measurable holds f is B-measurable
proof
let X,S,f,A,B;
assume that
A1: B c= A and
A2: f is A-measurable;
for r being Real holds (B /\ less_dom(f,r)) in S
proof
let r be Real;
A3: A /\ less_dom(f,r) in S by A2;
B /\ (A /\ less_dom(f,r)) = B /\ A /\ less_dom(f,r) by XBOOLE_1:16
.= B /\ less_dom(f,r) by A1,XBOOLE_1:28;
hence thesis by A3,FINSUB_1:def 2;
end;
hence thesis;
end;
theorem
for X,S,f,A,B st f is A-measurable & f is B-measurable holds
f is (A \/ B)-measurable
proof
let X,S,f,A,B;
assume
A1: f is A-measurable & f is B-measurable;
for r being Real holds ((A \/ B) /\ less_dom(f,r)) in S
proof
let r be Real;
A /\ less_dom(f,r) in S & B /\ less_dom(f,r) in S by A1;
then (A /\ less_dom(f,r)) \/ (B /\ less_dom(f,r)) in S by FINSUB_1:def 1;
hence thesis by XBOOLE_1:23;
end;
hence thesis;
end;
theorem
for X,S,f,A,r,s st f is A-measurable & A c= dom f holds
(A /\ great_dom(f,r) /\ less_dom(f,s)) in S
proof
let X,S,f,A,r,s;
assume that
A1: f is A-measurable and
A2: A c= dom f;
A3: A /\ less_dom(f,s) in S by A1;
A4: for r1 being Real holds A /\ great_eq_dom(f,r1) in S
proof
let r1 be Real;
A
/\ less_dom(f,r1) in S & A /\ great_eq_dom(f,r1) = A\(A /\
less_dom(f,r1)) by A1,A2,Th14;
hence thesis by MEASURE1:6;
end;
for r1 holds A /\ great_dom(f,r1) in S
proof
let r1;
defpred P[Element of NAT,set] means
A /\ great_eq_dom(f,(r1+1/($1+1))) = $2;
A5: for n ex y being Element of S st P[n,y]
proof
let n;
reconsider y=A /\ great_eq_dom(f,(r1+1/(n+1))) as Element of S
by A4;
take y;
thus thesis;
end;
consider F being sequence of S such that
A6: for n holds P[n,F.n] from FUNCT_2:sch 3(A5);
A /\ great_dom(f,r1) = union rng F by A6,Th22;
hence thesis;
end;
then A7: A /\ great_dom(f,r) in S;
(A /\ great_dom(f,r))/\(A /\ less_dom(f,s))
= (A /\ great_dom(f,r) /\ A) /\ less_dom(f,s) by XBOOLE_1:16
.= (great_dom(f,r) /\ (A /\ A)) /\
less_dom(f,s) by XBOOLE_1:16;
hence thesis by A3,A7,FINSUB_1:def 2;
end;
theorem
for X,S,f,A st f is A-measurable & A c= dom f holds
A /\ eq_dom(f,+infty) in S
proof
let X,S,f,A;
assume
A1: f is A-measurable & A c= dom f;
defpred P[Element of NAT,set]means A /\ great_dom(f,$1) = $2;
A2: for n ex y being Element of S st P[n,y]
proof
let n;
reconsider y=A /\ great_dom(f,n) as Element of S by A1,Th29;
take y;
thus thesis;
end;
consider F being sequence of S such that
A3: for n holds P[n,F.n] from FUNCT_2:sch 3(A2);
A /\ eq_dom(f,+infty) = meet rng F by A3,Th23;
hence thesis;
end;
theorem
for X,S,f,A st f is A-measurable holds A /\ eq_dom(f,-infty) in S
proof
let X,S,f,A;
assume
A1: f is A-measurable;
defpred P[Nat,set] means A /\ less_dom(f,(-$1)) = $2;
A2: for n ex y being Element of S st P[n,y]
proof
let n;
reconsider y=A /\ less_dom(f,(-n)) as Element of S by A1;
take y;
thus thesis;
end;
consider F being sequence of S such that
A3: for n holds P[n,F.n] from FUNCT_2:sch 3(A2);
for n being Nat holds P[n,F.n]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A3;
end;
then A /\ eq_dom(f,-infty) = meet rng F by Th25;
hence thesis;
end;
theorem
for X,S,f,A st f is A-measurable & A c= dom f holds
A /\ great_dom(f,-infty) /\ less_dom(f,+infty) in S
proof
let X,S,f,A;
assume that
A1: f is A-measurable and
A2: A c= dom f;
A3: A /\ great_dom(f,-infty) in S
proof
defpred P[Element of NAT,set] means A /\ great_dom(f,(-$1)) = $2;
A4: for n ex y being Element of S st P[n,y]
proof
let n;
reconsider y=A /\ great_dom(f,(-n)) as Element of S by A1,A2,Th29;
take y;
thus thesis;
end;
consider F being sequence of S such that
A5: for n holds P[n,F.n] from FUNCT_2:sch 3(A4);
A /\ great_dom(f,-infty) = union rng F by A5,Th26;
hence thesis;
end;
A6: A /\ less_dom(f,+infty) in S
proof
defpred P[Element of NAT,set] means A /\ less_dom(f,$1) = $2;
A7: for n ex y being Element of S st P[n,y]
proof
let n;
reconsider y=A /\ less_dom(f,n) as Element of S by A1;
take y;
thus thesis;
end;
consider F being sequence of S such that
A8: for n holds P[n,F.n] from FUNCT_2:sch 3(A7);
A /\ less_dom(f,+infty) = union rng F by A8,Th24;
hence thesis;
end;
(A /\ great_dom(f,-infty)) /\ (A /\ less_dom(f,+infty))
= (A /\ great_dom(f,-infty) /\ A) /\ less_dom(f,+infty) by XBOOLE_1:16
.= (great_dom(f,-infty) /\ (A /\ A)) /\ less_dom(f,+infty) by XBOOLE_1:16;
hence thesis by A3,A6,FINSUB_1:def 2;
end;
theorem
for X,S,f,g,A,r st f is A-measurable & g is A-measurable & A c= dom g
holds A /\ less_dom(f,r) /\ great_dom(g,r) in S
proof
let X,S,f,g,A,r;
assume f is A-measurable & g is A-measurable & A c= dom g;
then A1: A
/\ less_dom(f,r) in S & A /\ great_dom(g,r) in S by Th29;
(A /\ less_dom(f,r)) /\ (A /\ great_dom(g,r))
=((A /\ less_dom(f,r)) /\ A) /\ great_dom(g,r) by XBOOLE_1:16
.=((A /\ A) /\ less_dom(f,r)) /\ great_dom(g,r) by XBOOLE_1:16
.=A /\ less_dom(f,r) /\ great_dom(g,r);
hence thesis by A1,FINSUB_1:def 2;
end;
theorem
for X,S,f,A,r st f is A-measurable & A c= dom f
holds r(#)f is A-measurable
proof
let X,S,f,A,r;
assume that
A1: f is A-measurable and
A2: A c= dom f;
for r1 being Real holds A /\ less_dom(r(#)f,r1) in S
proof
let r1 being Real;
now per cases;
suppose
A3: r<>0;
reconsider r0=r1/r as Real;
A4: r1=r*r0 by A3,XCMPLX_1:87;
now per cases by A3;
suppose
A5: r > 0;
for x being Element of X st x in less_dom(f,r0)
holds x in less_dom(r(#)f,r1)
proof
let x be Element of X;
assume
A6: x in less_dom(f,r0);
then x in dom f by Def11;
then A7: x in dom(r(#)f) by Def6;
A8: f.x < r0 by A6,Def11;
f.x < r1 / r by A8;
then A9: f.x * r < r1 / r * (r qua ExtReal) by A5,XXREAL_3:72;
A10: r1 / r * r = (r1/r)*r
.= r1/(r/r) by XCMPLX_1:81
.= r1/1 by A3,XCMPLX_1:60
.= r1;
(r(#)f).x = r * f.x by A7,Def6;
hence thesis by A7,A9,A10,Def11;
end;
then A11: less_dom
(f,r0) c= less_dom(r(#)f,r1);
for x being Element of X st x in less_dom(r(#)f,r1)
holds x in less_dom(f,r0)
proof
let x being Element of X;
assume
A12: x in less_dom(r(#)f,r1);
then
A13: x in dom(r(#)f) by Def11;
(r(#)f).x < r1 by A12,Def11;
then (r(#)f).x < r * r0 by A4;
then
A14: (r(#)f).x / r < r * r0 / (r qua ExtReal)
by A5,XXREAL_3:80;
A15: r * r0 / r = (r*r0)/r
.= r0/(r/r) by XCMPLX_1:77
.= r0/1 by A3,XCMPLX_1:60
.= r0;
x in dom f & f.x = (r(#)f).x / r by A3,A13,Def6,Th6;
hence thesis by A14,A15,Def11;
end;
then
less_dom(r(#)f,r1) c= less_dom(f,r0);
then less_dom
(f,r0) = less_dom(r(#)f,r1) by A11,XBOOLE_0:def 10;
hence thesis by A1;
end;
suppose
A16: r < 0;
for x being Element of X st x in great_dom(f,r0)
holds x in less_dom(r(#)f,r1)
proof
let x be Element of X;
assume
A17: x in great_dom(f,r0);
then x in dom f by Def13;
then A18: x in dom(r(#)f) by Def6;
r0 < f.x by A17,Def13;
then r1 / r < f.x;
then A19: f .x * r < r1 / r * (r qua ExtReal) by A16,
XXREAL_3:102;
A20: r1 / r * r = (r1/r)*r
.= r1/(r/r) by XCMPLX_1:81
.= r1/1 by A3,XCMPLX_1:60
.= r1;
(r(#)f).x = r * f.x by A18,Def6;
hence thesis by A18,A19,A20,Def11;
end;
then A21: great_dom
(f,r0) c= less_dom(r(#)f,r1);
for x being Element of X st x in less_dom(r(#)f,r1)
holds x in great_dom(f,r0)
proof
let x being Element of X;
assume
A22: x in less_dom(r(#)f,r1);
then A23: x in dom(r(#)f) by Def11;
(r(#)f).x < r1 by A22,Def11;
then (r(#)f).x < r * r0 by A4;
then
A24: r * r0 / (r qua ExtReal) < (r(#)f).x / r
by A16,XXREAL_3:104;
A25: r * r0 / r = (r*r0)/r
.= r0/(r/r) by XCMPLX_1:77
.= r0/1 by A3,XCMPLX_1:60
.= r0;
x in dom f & f.x = (r(#)f).x / r by A3,A23,Def6,Th6;
hence thesis by A24,A25,Def13;
end;
then less_dom
(r(#)f,r1) c= great_dom(f,r0);
then great_dom(f,r0) = less_dom(r(#)f,r1) by A21,
XBOOLE_0:def 10;
hence thesis by A1,A2,Th29;
end;
end;
hence thesis;
end;
suppose
A26: r=0;
now per cases;
suppose
A27: r1>0;
for x1 being object holds x1 in A implies x1 in A /\
less_dom(r(#)f,r1)
proof
let x1 being object;
assume
A28: x1 in A;
then reconsider x1 as Element of X;
x1 in dom f by A2,A28;
then A29: x1 in dom (r(#)f) by Def6;
reconsider y = (r(#)f).x1 as R_eal;
y = (r) * f.x1 by A29,Def6
.= 0. by A26;
then x1 in less_dom(r(#)f,r1) by A27,A29,Def11;
hence thesis by A28,XBOOLE_0:def 4;
end;
then A
/\ less_dom(r(#)f,r1) c= A & A c= A /\ less_dom(r(#)f,r1) by
XBOOLE_1:17;
then A /\ less_dom(r(#)f,r1) = A by XBOOLE_0:def 10;
hence thesis;
end;
suppose
A30: r1<=0;
less_dom(r(#)f,r1) = {}
proof
assume less_dom(r(#)f,r1) <> {};
then consider x1 being Element of X such that
A31: x1 in less_dom(r(#)f,r1) by SUBSET_1:4;
A32: x1 in dom (r(#)f) by A31,Def11;
A33: (r(#)f).x1 < r1 by A31,Def11;
A34: (r(#)f).x1 in rng(r(#)f) by A32,FUNCT_1:def 3;
for
y being R_eal st y in rng(r(#)f) holds not y < r1
proof
let y being R_eal;
assume y in rng(r(#)f);
then consider x such that
A35: x in dom(r(#)f) & y = (r(#)f).x by PARTFUN1:3;
y = (r) * f.x by A35,Def6
.= 0. by A26;
hence thesis by A30;
end;
hence contradiction by A33,A34;
end;
hence thesis by PROB_1:4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;