:: MEASURE6 semantic presentation begin theorem :: MEASURE6:1 ex F being Function of NAT,[:NAT,NAT:] st ( F is one-to-one & dom F = NAT & rng F = [:NAT,NAT:] ) proof consider F being Function such that A1: F is one-to-one and A2: ( dom F = NAT & rng F = [:NAT,NAT:] ) by CARD_4:5, WELLORD2:def_4; F is Function of NAT,[:NAT,NAT:] by A2, FUNCT_2:1; hence ex F being Function of NAT,[:NAT,NAT:] st ( F is one-to-one & dom F = NAT & rng F = [:NAT,NAT:] ) by A1, A2; ::_thesis: verum end; theorem :: MEASURE6:2 for F being Function of NAT,ExtREAL st F is nonnegative holds 0. <= SUM F proof let F be Function of NAT,ExtREAL; ::_thesis: ( F is nonnegative implies 0. <= SUM F ) assume F is nonnegative ; ::_thesis: 0. <= SUM F then 0. <= (Ser F) . 0 by SUPINF_2:40; hence 0. <= SUM F by FUNCT_2:4, XXREAL_2:4; ::_thesis: verum end; theorem :: MEASURE6:3 for F being Function of NAT,ExtREAL for x being R_eal st ex n being Element of NAT st x <= F . n & F is nonnegative holds x <= SUM F proof let F be Function of NAT,ExtREAL; ::_thesis: for x being R_eal st ex n being Element of NAT st x <= F . n & F is nonnegative holds x <= SUM F let x be R_eal; ::_thesis: ( ex n being Element of NAT st x <= F . n & F is nonnegative implies x <= SUM F ) assume that A1: ex n being Element of NAT st x <= F . n and A2: F is nonnegative ; ::_thesis: x <= SUM F consider n being Element of NAT such that A3: x <= F . n by A1; A4: (Ser F) . n <= SUM F by FUNCT_2:4, XXREAL_2:4; percases ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6; suppose n = 0 ; ::_thesis: x <= SUM F then (Ser F) . n = F . n by SUPINF_2:44; hence x <= SUM F by A3, A4, XXREAL_0:2; ::_thesis: verum end; suppose ex k being Nat st n = k + 1 ; ::_thesis: x <= SUM F then consider k being Nat such that A5: n = k + 1 ; reconsider k = k as Element of NAT by ORDINAL1:def_12; A6: 0. <= (Ser F) . k by A2, SUPINF_2:40; (Ser F) . n = ((Ser F) . k) + (F . (k + 1)) by A5, SUPINF_2:44; then 0. + x <= (Ser F) . n by A3, A5, A6, XXREAL_3:36; then x <= (Ser F) . n by XXREAL_3:4; hence x <= SUM F by A4, XXREAL_0:2; ::_thesis: verum end; end; end; definition let x be ext-real number ; func R_EAL x -> R_eal equals :: MEASURE6:def 1 x; coherence x is R_eal by XXREAL_0:def_1; end; :: deftheorem defines R_EAL MEASURE6:def_1_:_ for x being ext-real number holds R_EAL x = x; theorem :: MEASURE6:4 for eps being R_eal st 0. < eps holds ex F being Function of NAT,ExtREAL st ( ( for n being Element of NAT holds 0. < F . n ) & SUM F < eps ) proof defpred S1[ set , set , set ] means for a, b being R_eal for s being Element of NAT st s = \$1 & a = \$2 & b = \$3 holds b = a / 2; let eps be R_eal; ::_thesis: ( 0. < eps implies ex F being Function of NAT,ExtREAL st ( ( for n being Element of NAT holds 0. < F . n ) & SUM F < eps ) ) assume 0. < eps ; ::_thesis: ex F being Function of NAT,ExtREAL st ( ( for n being Element of NAT holds 0. < F . n ) & SUM F < eps ) then consider x0 being real number such that A1: 0. < x0 and A2: x0 < eps by XXREAL_3:3; consider x being real number such that A3: 0. < x and A4: x + x < x0 by A1, XXREAL_3:50; reconsider x = x as Element of ExtREAL by XXREAL_0:def_1; A5: for n being Element of NAT for x being Element of ExtREAL ex y being Element of ExtREAL st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Element of ExtREAL ex y being Element of ExtREAL st S1[n,x,y] let x be Element of ExtREAL ; ::_thesis: ex y being Element of ExtREAL st S1[n,x,y] reconsider m = x / 2 as Element of ExtREAL by XXREAL_0:def_1; take m ; ::_thesis: S1[n,x,m] thus S1[n,x,m] ; ::_thesis: verum end; consider F being Function of NAT,ExtREAL such that A6: ( F . 0 = x & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A5); take F ; ::_thesis: ( ( for n being Element of NAT holds 0. < F . n ) & SUM F < eps ) defpred S2[ Element of NAT ] means 0. < F . \$1; A7: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A8: 0. < F . k ; ::_thesis: S2[k + 1] F . (k + 1) = (F . k) / 2 by A6; hence S2[k + 1] by A8; ::_thesis: verum end; A9: S2[ 0 ] by A3, A6; thus A10: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A9, A7); ::_thesis: SUM F < eps then for n being Element of NAT holds 0. <= F . n ; then A11: F is nonnegative by SUPINF_2:39; for s being ext-real number st s in rng (Ser F) holds s <= x0 proof defpred S3[ Element of NAT ] means ((Ser F) . \$1) + (F . \$1) < x0; let s be ext-real number ; ::_thesis: ( s in rng (Ser F) implies s <= x0 ) assume s in rng (Ser F) ; ::_thesis: s <= x0 then consider n being set such that A12: n in dom (Ser F) and A13: s = (Ser F) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A12; A14: for l being Element of NAT st S3[l] holds S3[l + 1] proof let l be Element of NAT ; ::_thesis: ( S3[l] implies S3[l + 1] ) F . (l + 1) = (F . l) / 2 by A6; then A15: ((Ser F) . l) + ((F . (l + 1)) + (F . (l + 1))) <= ((Ser F) . l) + (F . l) by XXREAL_3:105; ( 0. <= (Ser F) . l & 0. <= F . (l + 1) ) by A10, A11, SUPINF_2:40; then A16: ( ((Ser F) . (l + 1)) + (F . (l + 1)) = (((Ser F) . l) + (F . (l + 1))) + (F . (l + 1)) & (((Ser F) . l) + (F . (l + 1))) + (F . (l + 1)) <= ((Ser F) . l) + (F . l) ) by A15, SUPINF_2:44, XXREAL_3:44; assume ((Ser F) . l) + (F . l) < x0 ; ::_thesis: S3[l + 1] hence S3[l + 1] by A16, XXREAL_0:2; ::_thesis: verum end; A17: S3[ 0 ] by A4, A6, SUPINF_2:44; for k being Element of NAT holds S3[k] from NAT_1:sch_1(A17, A14); then A18: ((Ser F) . n) + (F . n) < x0 ; ( 0. <= (Ser F) . n & 0. <= F . n ) by A10, A11, SUPINF_2:40; hence s <= x0 by A13, A18, XXREAL_3:48; ::_thesis: verum end; then x0 is UpperBound of rng (Ser F) by XXREAL_2:def_1; then A19: sup (rng (Ser F)) <= x0 by XXREAL_2:def_3; percases ( SUM F < x0 or SUM F = x0 ) by A19, XXREAL_0:1; suppose SUM F < x0 ; ::_thesis: SUM F < eps hence SUM F < eps by A2, XXREAL_0:2; ::_thesis: verum end; suppose SUM F = x0 ; ::_thesis: SUM F < eps hence SUM F < eps by A2; ::_thesis: verum end; end; end; theorem :: MEASURE6:5 for eps being R_eal for X being non empty Subset of ExtREAL st 0. < eps & inf X is Real holds ex x being ext-real number st ( x in X & x < (inf X) + eps ) proof let eps be R_eal; ::_thesis: for X being non empty Subset of ExtREAL st 0. < eps & inf X is Real holds ex x being ext-real number st ( x in X & x < (inf X) + eps ) let X be non empty Subset of ExtREAL; ::_thesis: ( 0. < eps & inf X is Real implies ex x being ext-real number st ( x in X & x < (inf X) + eps ) ) assume that A1: 0. < eps and A2: inf X is Real ; ::_thesis: ex x being ext-real number st ( x in X & x < (inf X) + eps ) assume for x being ext-real number holds ( not x in X or not x < (inf X) + eps ) ; ::_thesis: contradiction then (inf X) + eps is LowerBound of X by XXREAL_2:def_2; then A3: (inf X) + eps <= inf X by XXREAL_2:def_4; percases ( eps < +infty or eps = +infty ) by XXREAL_0:4; suppose eps < +infty ; ::_thesis: contradiction then reconsider a = inf X, b = eps as Real by A1, A2, XXREAL_0:48; (inf X) + eps = a + b by SUPINF_2:1; then b <= a - a by A3, XREAL_1:19; hence contradiction by A1; ::_thesis: verum end; suppose eps = +infty ; ::_thesis: contradiction then (inf X) + eps = +infty by A2, XXREAL_3:def_2; hence contradiction by A2, A3, XXREAL_0:4; ::_thesis: verum end; end; end; theorem :: MEASURE6:6 for eps being R_eal for X being non empty Subset of ExtREAL st 0. < eps & sup X is Real holds ex x being ext-real number st ( x in X & (sup X) - eps < x ) proof let eps be R_eal; ::_thesis: for X being non empty Subset of ExtREAL st 0. < eps & sup X is Real holds ex x being ext-real number st ( x in X & (sup X) - eps < x ) let X be non empty Subset of ExtREAL; ::_thesis: ( 0. < eps & sup X is Real implies ex x being ext-real number st ( x in X & (sup X) - eps < x ) ) assume that A1: 0. < eps and A2: sup X is Real ; ::_thesis: ex x being ext-real number st ( x in X & (sup X) - eps < x ) assume for x being ext-real number holds ( not x in X or not (sup X) - eps < x ) ; ::_thesis: contradiction then (sup X) - eps is UpperBound of X by XXREAL_2:def_1; then A3: sup X <= (sup X) - eps by XXREAL_2:def_3; percases ( eps < +infty or eps = +infty ) by XXREAL_0:4; suppose eps < +infty ; ::_thesis: contradiction then reconsider a = sup X, b = eps as Real by A1, A2, XXREAL_0:48; a <= a - b by A3, SUPINF_2:3; hence contradiction by A1, XREAL_1:44; ::_thesis: verum end; suppose eps = +infty ; ::_thesis: contradiction then (sup X) - eps = -infty by A2, XXREAL_3:13; hence contradiction by A2, A3, XXREAL_0:6; ::_thesis: verum end; end; end; theorem :: MEASURE6:7 for F being Function of NAT,ExtREAL st F is nonnegative & SUM F < +infty holds for n being Element of NAT holds F . n in REAL proof let F be Function of NAT,ExtREAL; ::_thesis: ( F is nonnegative & SUM F < +infty implies for n being Element of NAT holds F . n in REAL ) assume that A1: F is nonnegative and A2: SUM F < +infty ; ::_thesis: for n being Element of NAT holds F . n in REAL let n be Element of NAT ; ::_thesis: F . n in REAL defpred S1[ Element of NAT ] means F . \$1 <= (Ser F) . \$1; A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume F . k <= (Ser F) . k ; ::_thesis: S1[k + 1] reconsider x = (Ser F) . k as R_eal ; x + (F . (k + 1)) = (Ser F) . (k + 1) by SUPINF_2:44; hence S1[k + 1] by A1, SUPINF_2:40, XXREAL_3:39; ::_thesis: verum end; A4: S1[ 0 ] by SUPINF_2:44; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3); then A5: F . n <= (Ser F) . n ; (Ser F) . n <= SUM F by FUNCT_2:4, XXREAL_2:4; then F . n <= SUM F by A5, XXREAL_0:2; then A6: F . n < +infty by A2, XXREAL_0:2; ( 0. = 0 & 0. <= F . n ) by A1, SUPINF_2:39; hence F . n in REAL by A6, XXREAL_0:46; ::_thesis: verum end; registration cluster non empty complex-membered ext-real-membered real-membered interval for Element of bool REAL; existence ex b1 being Subset of REAL st ( not b1 is empty & b1 is interval ) proof take [#] REAL ; ::_thesis: ( not [#] REAL is empty & [#] REAL is interval ) thus ( not [#] REAL is empty & [#] REAL is interval ) ; ::_thesis: verum end; end; theorem :: MEASURE6:8 for A being non empty Interval for a being R_eal st ex b being R_eal st ( a <= b & A = ].a,b.[ ) holds a = inf A by XXREAL_1:28, XXREAL_2:28; theorem :: MEASURE6:9 for A being non empty Interval for a being R_eal st ex b being R_eal st ( a <= b & A = ].a,b.] ) holds a = inf A by XXREAL_1:26, XXREAL_2:27; theorem :: MEASURE6:10 for A being non empty Interval for a being R_eal st ex b being R_eal st ( a <= b & A = [.a,b.] ) holds a = inf A by XXREAL_2:25; theorem Th11: :: MEASURE6:11 for A being non empty Interval for a being R_eal st ex b being R_eal st ( a <= b & A = [.a,b.[ ) holds a = inf A proof let A be non empty Interval; ::_thesis: for a being R_eal st ex b being R_eal st ( a <= b & A = [.a,b.[ ) holds a = inf A let IT be R_eal; ::_thesis: ( ex b being R_eal st ( IT <= b & A = [.IT,b.[ ) implies IT = inf A ) given b being R_eal such that A1: IT <= b and A2: A = [.IT,b.[ ; ::_thesis: IT = inf A IT <> b by A2; then IT < b by A1, XXREAL_0:1; hence IT = inf A by A2, XXREAL_2:26; ::_thesis: verum end; theorem :: MEASURE6:12 for A being non empty Interval for b being R_eal st ex a being R_eal st ( a <= b & A = ].a,b.[ ) holds b = sup A by XXREAL_1:28, XXREAL_2:32; theorem Th13: :: MEASURE6:13 for A being non empty Interval for b being R_eal st ex a being R_eal st ( a <= b & A = ].a,b.] ) holds b = sup A proof let A be non empty Interval; ::_thesis: for b being R_eal st ex a being R_eal st ( a <= b & A = ].a,b.] ) holds b = sup A let IT be R_eal; ::_thesis: ( ex a being R_eal st ( a <= IT & A = ].a,IT.] ) implies IT = sup A ) given a being R_eal such that A1: a <= IT and A2: A = ].a,IT.] ; ::_thesis: IT = sup A a <> IT by A2; then a < IT by A1, XXREAL_0:1; hence IT = sup A by A2, XXREAL_2:30; ::_thesis: verum end; theorem :: MEASURE6:14 for A being non empty Interval for b being R_eal st ex a being R_eal st ( a <= b & A = [.a,b.] ) holds b = sup A by XXREAL_2:29; theorem Th15: :: MEASURE6:15 for A being non empty Interval for b being R_eal st ex a being R_eal st ( a <= b & A = [.a,b.[ ) holds b = sup A proof let A be non empty Interval; ::_thesis: for b being R_eal st ex a being R_eal st ( a <= b & A = [.a,b.[ ) holds b = sup A let IT be R_eal; ::_thesis: ( ex a being R_eal st ( a <= IT & A = [.a,IT.[ ) implies IT = sup A ) given a being R_eal such that A1: a <= IT and A2: A = [.a,IT.[ ; ::_thesis: IT = sup A a <> IT by A2; then a < IT by A1, XXREAL_0:1; hence IT = sup A by A2, XXREAL_2:31; ::_thesis: verum end; theorem :: MEASURE6:16 for A being non empty Interval st A is open_interval holds A = ].(inf A),(sup A).[ proof let A be non empty Interval; ::_thesis: ( A is open_interval implies A = ].(inf A),(sup A).[ ) assume A is open_interval ; ::_thesis: A = ].(inf A),(sup A).[ then consider a, b being R_eal such that A1: A = ].a,b.[ by MEASURE5:def_2; sup A = b by A1, XXREAL_1:28, XXREAL_2:32; hence A = ].(inf A),(sup A).[ by A1, XXREAL_1:28, XXREAL_2:28; ::_thesis: verum end; theorem :: MEASURE6:17 for A being non empty Interval st A is closed_interval holds A = [.(inf A),(sup A).] proof let A be non empty Interval; ::_thesis: ( A is closed_interval implies A = [.(inf A),(sup A).] ) assume A is closed_interval ; ::_thesis: A = [.(inf A),(sup A).] then consider a, b being real number such that A1: A = [.a,b.] by MEASURE5:def_3; A2: a <= b by A1, XXREAL_1:29; reconsider b = b as R_eal by XXREAL_0:def_1; sup A = b by A1, A2, XXREAL_2:29; hence A = [.(inf A),(sup A).] by A1, A2, XXREAL_2:25; ::_thesis: verum end; theorem :: MEASURE6:18 for A being non empty Interval st A is right_open_interval holds A = [.(inf A),(sup A).[ proof let A be non empty Interval; ::_thesis: ( A is right_open_interval implies A = [.(inf A),(sup A).[ ) assume A is right_open_interval ; ::_thesis: A = [.(inf A),(sup A).[ then consider a being real number , b being R_eal such that A1: A = [.a,b.[ by MEASURE5:def_4; reconsider a = a as R_eal by XXREAL_0:def_1; A2: a <= b by A1, XXREAL_1:27; then sup A = b by A1, Th15; hence A = [.(inf A),(sup A).[ by A1, A2, Th11; ::_thesis: verum end; theorem :: MEASURE6:19 for A being non empty Interval st A is left_open_interval holds A = ].(inf A),(sup A).] proof let A be non empty Interval; ::_thesis: ( A is left_open_interval implies A = ].(inf A),(sup A).] ) assume A is left_open_interval ; ::_thesis: A = ].(inf A),(sup A).] then consider a being R_eal, b being real number such that A1: A = ].a,b.] by MEASURE5:def_5; A2: a <= b by A1, XXREAL_1:26; reconsider b = b as R_eal by XXREAL_0:def_1; sup A = b by A2, A1, Th13; hence A = ].(inf A),(sup A).] by A1, XXREAL_1:26, XXREAL_2:27; ::_thesis: verum end; theorem :: MEASURE6:20 for A, B being non empty Interval for a, b being real number st a in A & b in B & sup A <= inf B holds a <= b proof let A, B be non empty Interval; ::_thesis: for a, b being real number st a in A & b in B & sup A <= inf B holds a <= b let a, b be real number ; ::_thesis: ( a in A & b in B & sup A <= inf B implies a <= b ) assume that A1: a in A and A2: b in B ; ::_thesis: ( not sup A <= inf B or a <= b ) A3: inf B <= R_EAL b by A2, XXREAL_2:3; assume A4: sup A <= inf B ; ::_thesis: a <= b R_EAL a <= sup A by A1, XXREAL_2:4; then R_EAL a <= inf B by A4, XXREAL_0:2; hence a <= b by A3, XXREAL_0:2; ::_thesis: verum end; theorem :: MEASURE6:21 for A, B being real-membered set for y being Real holds ( y in B ++ A iff ex x, z being Real st ( x in B & z in A & y = x + z ) ) proof let A, B be real-membered set ; ::_thesis: for y being Real holds ( y in B ++ A iff ex x, z being Real st ( x in B & z in A & y = x + z ) ) let y be Real; ::_thesis: ( y in B ++ A iff ex x, z being Real st ( x in B & z in A & y = x + z ) ) hereby ::_thesis: ( ex x, z being Real st ( x in B & z in A & y = x + z ) implies y in B ++ A ) assume y in B ++ A ; ::_thesis: ex x, w being Element of REAL st ( x in B & w in A & y = x + w ) then consider x, w being Element of COMPLEX such that A1: ( y = x + w & x in B & w in A ) ; ( B c= REAL & A c= REAL ) by MEMBERED:3; then reconsider x = x, w = w as Element of REAL by A1; take x = x; ::_thesis: ex w being Element of REAL st ( x in B & w in A & y = x + w ) take w = w; ::_thesis: ( x in B & w in A & y = x + w ) thus ( x in B & w in A & y = x + w ) by A1; ::_thesis: verum end; given w, z being Real such that A2: ( w in B & z in A & y = w + z ) ; ::_thesis: y in B ++ A thus y in B ++ A by A2, MEMBER_1:46; ::_thesis: verum end; theorem :: MEASURE6:22 for A, B being non empty Interval st sup A = inf B & ( sup A in A or inf B in B ) holds A \/ B is Interval proof let A, B be non empty Interval; ::_thesis: ( sup A = inf B & ( sup A in A or inf B in B ) implies A \/ B is Interval ) assume that A1: sup A = inf B and A2: ( sup A in A or inf B in B ) ; ::_thesis: A \/ B is Interval ( A is right_end or B is left_end ) by A2, XXREAL_2:def_5, XXREAL_2:def_6; hence A \/ B is Interval by A1, XXREAL_2:90, XXREAL_2:91; ::_thesis: verum end; definition let A be real-membered set ; let x be real number ; :: original: ++ redefine funcx ++ A -> Subset of REAL; coherence x ++ A is Subset of REAL by MEMBERED:3; end; Lm1: for A being real-membered set for x being real number for y being Real holds ( y in x ++ A iff ex z being Real st ( z in A & y = x + z ) ) proof let A be real-membered set ; ::_thesis: for x being real number for y being Real holds ( y in x ++ A iff ex z being Real st ( z in A & y = x + z ) ) let x be real number ; ::_thesis: for y being Real holds ( y in x ++ A iff ex z being Real st ( z in A & y = x + z ) ) let y be Real; ::_thesis: ( y in x ++ A iff ex z being Real st ( z in A & y = x + z ) ) hereby ::_thesis: ( ex z being Real st ( z in A & y = x + z ) implies y in x ++ A ) assume y in x ++ A ; ::_thesis: ex w being Element of REAL st ( w in A & y = x + w ) then consider w being Element of COMPLEX such that A1: ( y = x + w & w in A ) by MEMBER_1:143; A c= REAL by MEMBERED:3; then reconsider w = w as Element of REAL by A1; take w = w; ::_thesis: ( w in A & y = x + w ) thus ( w in A & y = x + w ) by A1; ::_thesis: verum end; given z being Real such that A2: ( z in A & y = x + z ) ; ::_thesis: y in x ++ A thus y in x ++ A by A2, MEMBER_1:141; ::_thesis: verum end; theorem Th23: :: MEASURE6:23 for A being Subset of REAL for x being real number holds (- x) ++ (x ++ A) = A proof let A be Subset of REAL; ::_thesis: for x being real number holds (- x) ++ (x ++ A) = A let x be real number ; ::_thesis: (- x) ++ (x ++ A) = A thus (- x) ++ (x ++ A) c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= (- x) ++ (x ++ A) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (- x) ++ (x ++ A) or y in A ) assume A1: y in (- x) ++ (x ++ A) ; ::_thesis: y in A then reconsider y = y as Real ; consider z being Real such that A2: z in x ++ A and A3: y = (- x) + z by A1, Lm1; ex t being Real st ( t in A & z = x + t ) by A2, Lm1; hence y in A by A3; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A or y in (- x) ++ (x ++ A) ) assume A4: y in A ; ::_thesis: y in (- x) ++ (x ++ A) then reconsider y = y as real number ; reconsider t = y - (- x) as Real by XREAL_0:def_1; reconsider z = t - x as Real ; A5: z = (- x) + t ; t in x ++ A by A4, Lm1; hence y in (- x) ++ (x ++ A) by A5, Lm1; ::_thesis: verum end; theorem :: MEASURE6:24 for x being real number for A being Subset of REAL st A = REAL holds x ++ A = A proof let x be real number ; ::_thesis: for A being Subset of REAL st A = REAL holds x ++ A = A let A be Subset of REAL; ::_thesis: ( A = REAL implies x ++ A = A ) assume A1: A = REAL ; ::_thesis: x ++ A = A A c= x ++ A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A or y in x ++ A ) assume y in A ; ::_thesis: y in x ++ A then reconsider y = y as Real ; reconsider z = y - x as Real ; y = x + z ; hence y in x ++ A by A1, Lm1; ::_thesis: verum end; hence x ++ A = A by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MEASURE6:25 for x being real number holds x ++ {} = {} ; theorem Th26: :: MEASURE6:26 for A being Interval for x being real number holds ( A is open_interval iff x ++ A is open_interval ) proof let A be Interval; ::_thesis: for x being real number holds ( A is open_interval iff x ++ A is open_interval ) let x be real number ; ::_thesis: ( A is open_interval iff x ++ A is open_interval ) reconsider y = - x as Real by XREAL_0:def_1; A1: for B being Interval for y being real number st B is open_interval holds y ++ B is open_interval proof let B be Interval; ::_thesis: for y being real number st B is open_interval holds y ++ B is open_interval let y be real number ; ::_thesis: ( B is open_interval implies y ++ B is open_interval ) reconsider y = y as Real by XREAL_0:def_1; reconsider z = y as R_eal by XXREAL_0:def_1; assume B is open_interval ; ::_thesis: y ++ B is open_interval then consider a, b being R_eal such that A2: B = ].a,b.[ by MEASURE5:def_2; reconsider s = z + a, t = z + b as R_eal ; y ++ B = ].s,t.[ proof thus y ++ B c= ].s,t.[ :: according to XBOOLE_0:def_10 ::_thesis: ].s,t.[ c= y ++ B proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in y ++ B or c in ].s,t.[ ) assume A3: c in y ++ B ; ::_thesis: c in ].s,t.[ then reconsider c = c as Real ; consider d being Real such that A4: d in B and A5: c = y + d by A3, Lm1; reconsider d1 = d as R_eal by XXREAL_0:def_1; a < d1 by A2, A4, MEASURE5:def_1; then A6: s < z + d1 by XXREAL_3:43; d1 < b by A2, A4, MEASURE5:def_1; then A7: z + d1 < t by XXREAL_3:43; z + d1 = c by A5, SUPINF_2:1; hence c in ].s,t.[ by A6, A7; ::_thesis: verum end; let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in ].s,t.[ or c in y ++ B ) assume A8: c in ].s,t.[ ; ::_thesis: c in y ++ B then reconsider c = c as Real ; reconsider c1 = c as R_eal by XXREAL_0:def_1; A9: c = y + (c - y) ; c1 < z + b by A8, MEASURE5:def_1; then c1 - z < (b + z) - z by XXREAL_3:43; then A10: c1 - z < b by XXREAL_3:22; z + a < c1 by A8, MEASURE5:def_1; then (a + z) - z < c1 - z by XXREAL_3:43; then A11: a < c1 - z by XXREAL_3:22; c1 - z = c - y by SUPINF_2:3; then c - y in B by A2, A11, A10; hence c in y ++ B by A9, Lm1; ::_thesis: verum end; hence y ++ B is open_interval by MEASURE5:def_2; ::_thesis: verum end; hence ( A is open_interval implies x ++ A is open_interval ) ; ::_thesis: ( x ++ A is open_interval implies A is open_interval ) assume A12: x ++ A is open_interval ; ::_thesis: A is open_interval then reconsider B = x ++ A as Interval ; y ++ B = A by Th23; hence A is open_interval by A1, A12; ::_thesis: verum end; theorem Th27: :: MEASURE6:27 for A being Interval for x being real number holds ( A is closed_interval iff x ++ A is closed_interval ) proof let A be Interval; ::_thesis: for x being real number holds ( A is closed_interval iff x ++ A is closed_interval ) let x be real number ; ::_thesis: ( A is closed_interval iff x ++ A is closed_interval ) A1: for B being Interval for y being real number st B is closed_interval holds y ++ B is closed_interval proof let B be Interval; ::_thesis: for y being real number st B is closed_interval holds y ++ B is closed_interval let y be real number ; ::_thesis: ( B is closed_interval implies y ++ B is closed_interval ) reconsider y = y as Real by XREAL_0:def_1; reconsider z = y as R_eal by XXREAL_0:def_1; assume B is closed_interval ; ::_thesis: y ++ B is closed_interval then consider a1, b1 being real number such that A2: B = [.a1,b1.] by MEASURE5:def_3; reconsider a = a1, b = b1 as R_eal by XXREAL_0:def_1; reconsider s = z + a, t = z + b as R_eal ; y ++ B = [.s,t.] proof thus y ++ B c= [.s,t.] :: according to XBOOLE_0:def_10 ::_thesis: [.s,t.] c= y ++ B proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in y ++ B or c in [.s,t.] ) assume A3: c in y ++ B ; ::_thesis: c in [.s,t.] then reconsider c = c as Real ; consider d being Real such that A4: d in B and A5: c = y + d by A3, Lm1; reconsider d1 = d as R_eal by XXREAL_0:def_1; a <= d1 by A2, A4, XXREAL_1:1; then A6: s <= z + d1 by XXREAL_3:36; d1 <= b by A2, A4, XXREAL_1:1; then A7: z + d1 <= t by XXREAL_3:36; z + d1 = c by A5, SUPINF_2:1; hence c in [.s,t.] by A6, A7, XXREAL_1:1; ::_thesis: verum end; reconsider a = a, b = b as R_eal ; let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in [.s,t.] or c in y ++ B ) assume A8: c in [.s,t.] ; ::_thesis: c in y ++ B then reconsider c = c as Real by XREAL_0:def_1; reconsider c1 = c as R_eal by XXREAL_0:def_1; A9: c = y + (c - y) ; c1 <= z + b by A8, XXREAL_1:1; then c1 - z <= (b + z) - z by XXREAL_3:36; then A10: c1 - z <= b by XXREAL_3:22; z + a <= c1 by A8, XXREAL_1:1; then (a + z) - z <= c1 - z by XXREAL_3:36; then A11: a <= c1 - z by XXREAL_3:22; c1 - z = c - y by SUPINF_2:3; then c - y in B by A2, A11, A10; hence c in y ++ B by A9, Lm1; ::_thesis: verum end; hence y ++ B is closed_interval by MEASURE5:def_3; ::_thesis: verum end; ( x ++ A is closed_interval implies A is closed_interval ) proof reconsider y = - x as Real by XREAL_0:def_1; assume A12: x ++ A is closed_interval ; ::_thesis: A is closed_interval then reconsider B = x ++ A as Interval ; y ++ B = A by Th23; hence A is closed_interval by A1, A12; ::_thesis: verum end; hence ( A is closed_interval iff x ++ A is closed_interval ) by A1; ::_thesis: verum end; theorem Th28: :: MEASURE6:28 for A being Interval for x being real number holds ( A is right_open_interval iff x ++ A is right_open_interval ) proof let A be Interval; ::_thesis: for x being real number holds ( A is right_open_interval iff x ++ A is right_open_interval ) let x be real number ; ::_thesis: ( A is right_open_interval iff x ++ A is right_open_interval ) A1: for B being Interval for y being real number st B is right_open_interval holds y ++ B is right_open_interval proof let B be Interval; ::_thesis: for y being real number st B is right_open_interval holds y ++ B is right_open_interval let y be real number ; ::_thesis: ( B is right_open_interval implies y ++ B is right_open_interval ) reconsider y = y as Real by XREAL_0:def_1; reconsider z = y as R_eal by XXREAL_0:def_1; assume B is right_open_interval ; ::_thesis: y ++ B is right_open_interval then consider a1 being real number , b being R_eal such that A2: B = [.a1,b.[ by MEASURE5:def_4; reconsider a = a1 as R_eal by XXREAL_0:def_1; reconsider s = z + a, t = z + b as R_eal ; y ++ B = [.s,t.[ proof thus y ++ B c= [.s,t.[ :: according to XBOOLE_0:def_10 ::_thesis: [.s,t.[ c= y ++ B proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in y ++ B or c in [.s,t.[ ) assume A3: c in y ++ B ; ::_thesis: c in [.s,t.[ then reconsider c = c as Real ; consider d being Real such that A4: d in B and A5: c = y + d by A3, Lm1; reconsider d1 = d as R_eal by XXREAL_0:def_1; a <= d1 by A2, A4, XXREAL_1:3; then A6: s <= z + d1 by XXREAL_3:36; d1 < b by A2, A4, XXREAL_1:3; then A7: z + d1 < t by XXREAL_3:43; z + d1 = c by A5, SUPINF_2:1; hence c in [.s,t.[ by A6, A7, XXREAL_1:3; ::_thesis: verum end; let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in [.s,t.[ or c in y ++ B ) assume A8: c in [.s,t.[ ; ::_thesis: c in y ++ B then reconsider c = c as Real by XREAL_0:def_1; reconsider c1 = c as R_eal by XXREAL_0:def_1; A9: c = y + (c - y) ; c1 < z + b by A8, XXREAL_1:3; then c1 - z < (b + z) - z by XXREAL_3:43; then A10: c1 - z < b by XXREAL_3:22; z + a <= c1 by A8, XXREAL_1:3; then (a + z) - z <= c1 - z by XXREAL_3:36; then A11: a <= c1 - z by XXREAL_3:22; c1 - z = c - y by SUPINF_2:3; then c - y in B by A2, A11, A10; hence c in y ++ B by A9, Lm1; ::_thesis: verum end; hence y ++ B is right_open_interval by MEASURE5:def_4; ::_thesis: verum end; ( x ++ A is right_open_interval implies A is right_open_interval ) proof reconsider y = - x as Real by XREAL_0:def_1; assume A12: x ++ A is right_open_interval ; ::_thesis: A is right_open_interval then reconsider B = x ++ A as Interval ; y ++ B = A by Th23; hence A is right_open_interval by A1, A12; ::_thesis: verum end; hence ( A is right_open_interval iff x ++ A is right_open_interval ) by A1; ::_thesis: verum end; theorem Th29: :: MEASURE6:29 for A being Interval for x being real number holds ( A is left_open_interval iff x ++ A is left_open_interval ) proof let A be Interval; ::_thesis: for x being real number holds ( A is left_open_interval iff x ++ A is left_open_interval ) let x be real number ; ::_thesis: ( A is left_open_interval iff x ++ A is left_open_interval ) A1: for B being Interval for y being real number st B is left_open_interval holds y ++ B is left_open_interval proof let B be Interval; ::_thesis: for y being real number st B is left_open_interval holds y ++ B is left_open_interval let y be real number ; ::_thesis: ( B is left_open_interval implies y ++ B is left_open_interval ) reconsider y = y as Real by XREAL_0:def_1; reconsider z = y as R_eal by XXREAL_0:def_1; assume B is left_open_interval ; ::_thesis: y ++ B is left_open_interval then consider a being R_eal, b1 being real number such that A2: B = ].a,b1.] by MEASURE5:def_5; reconsider b = b1 as R_eal by XXREAL_0:def_1; set s = z + a; set t = z + b; y ++ B = ].(z + a),(z + b).] proof thus y ++ B c= ].(z + a),(z + b).] :: according to XBOOLE_0:def_10 ::_thesis: ].(z + a),(z + b).] c= y ++ B proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in y ++ B or c in ].(z + a),(z + b).] ) assume A3: c in y ++ B ; ::_thesis: c in ].(z + a),(z + b).] then reconsider c = c as Real ; consider d being Real such that A4: d in B and A5: c = y + d by A3, Lm1; reconsider d1 = d as R_eal by XXREAL_0:def_1; a < d1 by A2, A4, XXREAL_1:2; then A6: z + a < z + d1 by XXREAL_3:43; d1 <= b by A2, A4, XXREAL_1:2; then A7: z + d1 <= z + b by XXREAL_3:36; z + d1 = c by A5, SUPINF_2:1; hence c in ].(z + a),(z + b).] by A6, A7, XXREAL_1:2; ::_thesis: verum end; let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in ].(z + a),(z + b).] or c in y ++ B ) assume A8: c in ].(z + a),(z + b).] ; ::_thesis: c in y ++ B then reconsider c = c as Real by XREAL_0:def_1; reconsider c1 = c as R_eal by XXREAL_0:def_1; A9: c = y + (c - y) ; c1 <= z + b by A8, XXREAL_1:2; then c1 - z <= (b + z) - z by XXREAL_3:36; then A10: c1 - z <= b by XXREAL_3:22; z + a < c1 by A8, XXREAL_1:2; then (a + z) - z < c1 - z by XXREAL_3:43; then A11: a < c1 - z by XXREAL_3:22; c1 - z = c - y by SUPINF_2:3; then c - y in B by A2, A11, A10; hence c in y ++ B by A9, Lm1; ::_thesis: verum end; hence y ++ B is left_open_interval by MEASURE5:def_5; ::_thesis: verum end; ( x ++ A is left_open_interval implies A is left_open_interval ) proof reconsider y = - x as Real by XREAL_0:def_1; assume A12: x ++ A is left_open_interval ; ::_thesis: A is left_open_interval then reconsider B = x ++ A as Interval ; y ++ B = A by Th23; hence A is left_open_interval by A1, A12; ::_thesis: verum end; hence ( A is left_open_interval iff x ++ A is left_open_interval ) by A1; ::_thesis: verum end; theorem :: MEASURE6:30 for A being Interval for x being real number holds x ++ A is Interval proof let A be Interval; ::_thesis: for x being real number holds x ++ A is Interval let x be real number ; ::_thesis: x ++ A is Interval percases ( A is open_interval or A is closed_interval or A is right_open_interval or A is left_open_interval ) by MEASURE5:1; suppose A is open_interval ; ::_thesis: x ++ A is Interval then x ++ A is open_interval by Th26; hence x ++ A is Interval ; ::_thesis: verum end; suppose A is closed_interval ; ::_thesis: x ++ A is Interval then x ++ A is closed_interval by Th27; hence x ++ A is Interval ; ::_thesis: verum end; suppose A is right_open_interval ; ::_thesis: x ++ A is Interval then x ++ A is right_open_interval by Th28; hence x ++ A is Interval ; ::_thesis: verum end; suppose A is left_open_interval ; ::_thesis: x ++ A is Interval then x ++ A is left_open_interval by Th29; hence x ++ A is Interval ; ::_thesis: verum end; end; end; theorem Th31: :: MEASURE6:31 for A being real-membered set for x being real number for y being R_eal st x = y holds sup (x ++ A) = y + (sup A) proof let A be real-membered set ; ::_thesis: for x being real number for y being R_eal st x = y holds sup (x ++ A) = y + (sup A) let x be real number ; ::_thesis: for y being R_eal st x = y holds sup (x ++ A) = y + (sup A) let y be R_eal; ::_thesis: ( x = y implies sup (x ++ A) = y + (sup A) ) assume A1: x = y ; ::_thesis: sup (x ++ A) = y + (sup A) A2: for z being UpperBound of x ++ A holds y + (sup A) <= z proof let z be UpperBound of x ++ A; ::_thesis: y + (sup A) <= z reconsider zz = z as R_eal by XXREAL_0:def_1; zz - y is UpperBound of A proof let u be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not u in A or u <= zz - y ) reconsider uu = u as R_eal by XXREAL_0:def_1; assume A3: u in A ; ::_thesis: u <= zz - y then reconsider u1 = u as Real by XREAL_0:def_1; y + uu = x + u1 by A1, XXREAL_3:def_2; then y + uu in x ++ A by A3, Lm1; then y + uu <= z by XXREAL_2:def_1; hence u <= zz - y by A1, XXREAL_3:45; ::_thesis: verum end; then sup A <= zz - y by XXREAL_2:def_3; hence y + (sup A) <= z by A1, XXREAL_3:45; ::_thesis: verum end; y + (sup A) is UpperBound of x ++ A proof let z be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not z in x ++ A or z <= y + (sup A) ) assume z in x ++ A ; ::_thesis: z <= y + (sup A) then consider a being Real such that A4: a in A and A5: z = x + a by Lm1; reconsider b = a as R_eal by XXREAL_0:def_1; A6: a <= sup A by A4, XXREAL_2:4; ex a, c being complex number st ( y = a & b = c & y + b = a + c ) by A1, XXREAL_3:def_2; hence z <= y + (sup A) by A1, A5, A6, XXREAL_3:36; ::_thesis: verum end; hence sup (x ++ A) = y + (sup A) by A2, XXREAL_2:def_3; ::_thesis: verum end; theorem Th32: :: MEASURE6:32 for A being real-membered set for x being real number for y being R_eal st x = y holds inf (x ++ A) = y + (inf A) proof let A be real-membered set ; ::_thesis: for x being real number for y being R_eal st x = y holds inf (x ++ A) = y + (inf A) let x be real number ; ::_thesis: for y being R_eal st x = y holds inf (x ++ A) = y + (inf A) let y be R_eal; ::_thesis: ( x = y implies inf (x ++ A) = y + (inf A) ) assume A1: x = y ; ::_thesis: inf (x ++ A) = y + (inf A) A2: for z being LowerBound of x ++ A holds z <= y + (inf A) proof let z be LowerBound of x ++ A; ::_thesis: z <= y + (inf A) reconsider zz = z as R_eal by XXREAL_0:def_1; zz - y is LowerBound of A proof let u be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not u in A or zz - y <= u ) reconsider uu = u as R_eal by XXREAL_0:def_1; assume A3: u in A ; ::_thesis: zz - y <= u then reconsider u1 = u as Real by XREAL_0:def_1; y + uu = x + u1 by A1, XXREAL_3:def_2; then y + uu in x ++ A by A3, Lm1; then z <= y + uu by XXREAL_2:def_2; hence zz - y <= u by A1, XXREAL_3:42; ::_thesis: verum end; then zz - y <= inf A by XXREAL_2:def_4; hence z <= y + (inf A) by A1, XXREAL_3:41; ::_thesis: verum end; y + (inf A) is LowerBound of x ++ A proof let z be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not z in x ++ A or y + (inf A) <= z ) assume z in x ++ A ; ::_thesis: y + (inf A) <= z then consider a being Real such that A4: a in A and A5: z = x + a by Lm1; reconsider b = a as R_eal by XXREAL_0:def_1; A6: inf A <= a by A4, XXREAL_2:3; ex a, c being complex number st ( y = a & b = c & y + b = a + c ) by A1, XXREAL_3:def_2; hence y + (inf A) <= z by A1, A5, A6, XXREAL_3:36; ::_thesis: verum end; hence inf (x ++ A) = y + (inf A) by A2, XXREAL_2:def_4; ::_thesis: verum end; theorem :: MEASURE6:33 for A being Interval for x being real number holds diameter A = diameter (x ++ A) proof let A be Interval; ::_thesis: for x being real number holds diameter A = diameter (x ++ A) let x be real number ; ::_thesis: diameter A = diameter (x ++ A) percases ( A is empty or not A is empty ) ; suppose A is empty ; ::_thesis: diameter A = diameter (x ++ A) hence diameter A = diameter (x ++ A) ; ::_thesis: verum end; supposeA1: not A is empty ; ::_thesis: diameter A = diameter (x ++ A) then consider y being real number such that A2: y in A by MEMBERED:9; reconsider y = y as Real by XREAL_0:def_1; A3: x + y in x ++ A by A2, Lm1; reconsider y = x as R_eal by XXREAL_0:def_1; thus diameter A = (sup A) - (inf A) by A1, MEASURE5:def_6 .= (y + (sup A)) - (y + (inf A)) by XXREAL_3:33 .= (sup (x ++ A)) - (y + (inf A)) by Th31 .= (sup (x ++ A)) - (inf (x ++ A)) by Th32 .= diameter (x ++ A) by A3, MEASURE5:def_6 ; ::_thesis: verum end; end; end; begin notation let X be set ; synonym without_zero X for with_non-empty_elements ; antonym with_zero X for with_non-empty_elements ; end; definition let X be set ; redefine attr X is with_non-empty_elements means :Def2: :: MEASURE6:def 2 not 0 in X; compatibility ( X is without_zero iff not 0 in X ) by SETFAM_1:def_8; end; :: deftheorem Def2 defines without_zero MEASURE6:def_2_:_ for X being set holds ( X is without_zero iff not 0 in X ); registration cluster REAL -> with_zero ; coherence not REAL is without_zero by Def2; cluster omega -> with_zero ; coherence not NAT is without_zero by Def2; end; registration cluster non empty without_zero for set ; existence ex b1 being set st ( not b1 is empty & b1 is without_zero ) proof set s = {1}; take {1} ; ::_thesis: ( not {1} is empty & {1} is without_zero ) thus not {1} is empty ; ::_thesis: {1} is without_zero thus {1} is without_zero ; ::_thesis: verum end; cluster non empty with_zero for set ; existence ex b1 being set st ( not b1 is empty & b1 is with_zero ) by Def2; end; registration cluster non empty complex-membered ext-real-membered real-membered without_zero for Element of bool REAL; existence ex b1 being Subset of REAL st ( not b1 is empty & b1 is without_zero ) proof set s = {1}; take {1} ; ::_thesis: ( not {1} is empty & {1} is without_zero ) thus not {1} is empty ; ::_thesis: {1} is without_zero thus {1} is without_zero ; ::_thesis: verum end; cluster non empty complex-membered ext-real-membered real-membered with_zero for Element of bool REAL; existence ex b1 being Subset of REAL st ( not b1 is empty & b1 is with_zero ) by Def2; end; theorem Th34: :: MEASURE6:34 for F being set st not F is empty & F is with_non-empty_elements & F is c=-linear holds F is centered proof defpred S1[ set ] means ( \$1 <> {} implies ex x being set st ( x in \$1 & ( for y being set st y in \$1 holds x c= y ) ) ); let F be set ; ::_thesis: ( not F is empty & F is with_non-empty_elements & F is c=-linear implies F is centered ) assume that A1: not F is empty and A2: F is with_non-empty_elements and A3: F is c=-linear ; ::_thesis: F is centered thus F <> {} by A1; :: according to FINSET_1:def_3 ::_thesis: for b1 being set holds ( b1 = {} or not b1 c= F or not b1 is finite or not meet b1 = {} ) let G be set ; ::_thesis: ( G = {} or not G c= F or not G is finite or not meet G = {} ) assume that A4: G <> {} and A5: G c= F and A6: G is finite ; ::_thesis: not meet G = {} A7: now__::_thesis:_for_x,_B_being_set_st_x_in_G_&_B_c=_G_&_S1[B]_holds_ S1[B_\/_{x}] let x, B be set ; ::_thesis: ( x in G & B c= G & S1[B] implies S1[B \/ {x}] ) assume that A8: x in G and A9: B c= G and A10: S1[B] ; ::_thesis: S1[B \/ {x}] thus S1[B \/ {x}] ::_thesis: verum proof assume B \/ {x} <> {} ; ::_thesis: ex x being set st ( x in B \/ {x} & ( for y being set st y in B \/ {x} holds x c= y ) ) percases ( B is empty or not B is empty ) ; supposeA11: B is empty ; ::_thesis: ex x being set st ( x in B \/ {x} & ( for y being set st y in B \/ {x} holds x c= y ) ) take x9 = x; ::_thesis: ( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds x9 c= y ) ) thus x9 in B \/ {x} by A11, TARSKI:def_1; ::_thesis: for y being set st y in B \/ {x} holds x9 c= y let y be set ; ::_thesis: ( y in B \/ {x} implies x9 c= y ) thus ( y in B \/ {x} implies x9 c= y ) by A11, TARSKI:def_1; ::_thesis: verum end; suppose not B is empty ; ::_thesis: ex x being set st ( x in B \/ {x} & ( for y being set st y in B \/ {x} holds x c= y ) ) then consider z being set such that A12: z in B and A13: for y being set st y in B holds z c= y by A10; thus ex x9 being set st ( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds x9 c= y ) ) ::_thesis: verum proof z in G by A9, A12; then A14: x,z are_c=-comparable by A3, A5, A8, ORDINAL1:def_8; percases ( x c= z or z c= x ) by A14, XBOOLE_0:def_9; supposeA15: x c= z ; ::_thesis: ex x9 being set st ( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds x9 c= y ) ) take x9 = x; ::_thesis: ( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds x9 c= y ) ) x9 in {x} by TARSKI:def_1; hence x9 in B \/ {x} by XBOOLE_0:def_3; ::_thesis: for y being set st y in B \/ {x} holds x9 c= y let y be set ; ::_thesis: ( y in B \/ {x} implies x9 c= y ) assume A16: y in B \/ {x} ; ::_thesis: x9 c= y percases ( y in B or y in {x} ) by A16, XBOOLE_0:def_3; suppose y in B ; ::_thesis: x9 c= y then z c= y by A13; hence x9 c= y by A15, XBOOLE_1:1; ::_thesis: verum end; suppose y in {x} ; ::_thesis: x9 c= y hence x9 c= y by TARSKI:def_1; ::_thesis: verum end; end; end; supposeA17: z c= x ; ::_thesis: ex x9 being set st ( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds x9 c= y ) ) take x9 = z; ::_thesis: ( x9 in B \/ {x} & ( for y being set st y in B \/ {x} holds x9 c= y ) ) thus x9 in B \/ {x} by A12, XBOOLE_0:def_3; ::_thesis: for y being set st y in B \/ {x} holds x9 c= y let y be set ; ::_thesis: ( y in B \/ {x} implies x9 c= y ) assume A18: y in B \/ {x} ; ::_thesis: x9 c= y percases ( y in B or y in {x} ) by A18, XBOOLE_0:def_3; suppose y in B ; ::_thesis: x9 c= y hence x9 c= y by A13; ::_thesis: verum end; suppose y in {x} ; ::_thesis: x9 c= y hence x9 c= y by A17, TARSKI:def_1; ::_thesis: verum end; end; end; end; end; end; end; end; end; A19: S1[ {} ] ; S1[G] from FINSET_1:sch_2(A6, A19, A7); then consider x being set such that A20: x in G and A21: for y being set st y in G holds x c= y by A4; consider xe being set such that A22: xe in x by A2, A5, A20, XBOOLE_0:def_1; now__::_thesis:_for_y_being_set_st_y_in_G_holds_ xe_in_y let y be set ; ::_thesis: ( y in G implies xe in y ) assume y in G ; ::_thesis: xe in y then x c= y by A21; hence xe in y by A22; ::_thesis: verum end; hence not meet G = {} by A4, SETFAM_1:def_1; ::_thesis: verum end; registration let F be set ; cluster c=-linear non empty with_non-empty_elements -> centered for Element of bool (bool F); coherence for b1 being Subset-Family of F st not b1 is empty & b1 is with_non-empty_elements & b1 is c=-linear holds b1 is centered by Th34; end; registration let X, Y be non empty set ; let f be Function of X,Y; clusterf .: X -> non empty ; coherence not f .: X is empty proof set x = the Element of X; A1: dom f = X by FUNCT_2:def_1; thus not f .: X is empty by A1; ::_thesis: verum end; end; definition let X, Y be set ; let f be Function of X,Y; func " f -> Function of (bool Y),(bool X) means :Def3: :: MEASURE6:def 3 for y being Subset of Y holds it . y = f " y; existence ex b1 being Function of (bool Y),(bool X) st for y being Subset of Y holds b1 . y = f " y proof deffunc H1( Subset of Y) -> Element of bool X = f " \$1; thus ex T being Function of (bool Y),(bool X) st for y being Subset of Y holds T . y = H1(y) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function of (bool Y),(bool X) st ( for y being Subset of Y holds b1 . y = f " y ) & ( for y being Subset of Y holds b2 . y = f " y ) holds b1 = b2 proof deffunc H1( Subset of Y) -> Element of bool X = f " \$1; thus for T1, T2 being Function of (bool Y),(bool X) st ( for y being Subset of Y holds T1 . y = H1(y) ) & ( for y being Subset of Y holds T2 . y = H1(y) ) holds T1 = T2 from BINOP_2:sch_1(); ::_thesis: verum end; end; :: deftheorem Def3 defines " MEASURE6:def_3_:_ for X, Y being set for f being Function of X,Y for b4 being Function of (bool Y),(bool X) holds ( b4 = " f iff for y being Subset of Y holds b4 . y = f " y ); theorem :: MEASURE6:35 for X, Y, x being set for S being Subset-Family of Y for f being Function of X,Y st x in meet ((" f) .: S) holds f . x in meet S proof let X, Y, x be set ; ::_thesis: for S being Subset-Family of Y for f being Function of X,Y st x in meet ((" f) .: S) holds f . x in meet S let S be Subset-Family of Y; ::_thesis: for f being Function of X,Y st x in meet ((" f) .: S) holds f . x in meet S let f be Function of X,Y; ::_thesis: ( x in meet ((" f) .: S) implies f . x in meet S ) assume A1: x in meet ((" f) .: S) ; ::_thesis: f . x in meet S A2: now__::_thesis:_for_SS_being_set_st_SS_in_S_holds_ f_._x_in_SS let SS be set ; ::_thesis: ( SS in S implies f . x in SS ) assume A3: SS in S ; ::_thesis: f . x in SS then (" f) . SS in (" f) .: S by FUNCT_2:35; then A4: x in (" f) . SS by A1, SETFAM_1:def_1; (" f) . SS = f " SS by A3, Def3; hence f . x in SS by A4, FUNCT_1:def_7; ::_thesis: verum end; not (" f) .: S is empty by A1, SETFAM_1:def_1; then not S is empty ; hence f . x in meet S by A2, SETFAM_1:def_1; ::_thesis: verum end; theorem Th36: :: MEASURE6:36 for r, s being real number st (abs r) + (abs s) = 0 holds r = 0 proof let r, s be real number ; ::_thesis: ( (abs r) + (abs s) = 0 implies r = 0 ) set aa = abs r; set ab = abs s; A1: ( 0 <= abs r & 0 <= abs s ) by COMPLEX1:46; assume (abs r) + (abs s) = 0 ; ::_thesis: r = 0 then abs r = 0 by A1; hence r = 0 by ABSVALUE:2; ::_thesis: verum end; theorem Th37: :: MEASURE6:37 for r, s, t being real number st r < s & s < t holds abs s < (abs r) + (abs t) proof let r, s, t be real number ; ::_thesis: ( r < s & s < t implies abs s < (abs r) + (abs t) ) assume that A1: r < s and A2: s < t ; ::_thesis: abs s < (abs r) + (abs t) percases ( s < 0 or 0 <= s ) ; supposeA3: s < 0 ; ::_thesis: abs s < (abs r) + (abs t) - s < - r by A1, XREAL_1:24; then A4: (- s) + 0 < (- r) + (abs t) by COMPLEX1:46, XREAL_1:8; - s = abs s by A3, ABSVALUE:def_1; hence abs s < (abs r) + (abs t) by A1, A3, A4, ABSVALUE:def_1; ::_thesis: verum end; supposeA5: 0 <= s ; ::_thesis: abs s < (abs r) + (abs t) A6: s + 0 < t + (abs r) by A2, COMPLEX1:46, XREAL_1:8; s = abs s by A5, ABSVALUE:def_1; hence abs s < (abs r) + (abs t) by A2, A5, A6, ABSVALUE:def_1; ::_thesis: verum end; end; end; theorem Th38: :: MEASURE6:38 for seq being Real_Sequence st seq is convergent & seq is non-zero & lim seq = 0 holds not seq " is bounded proof let seq be Real_Sequence; ::_thesis: ( seq is convergent & seq is non-zero & lim seq = 0 implies not seq " is bounded ) assume that A1: seq is convergent and A2: seq is non-zero and A3: lim seq = 0 ; ::_thesis: not seq " is bounded given r being real number such that A4: for n being Element of NAT holds (seq ") . n < r ; :: according to SEQ_2:def_3,SEQ_2:def_8 ::_thesis: not seq " is bounded_below given s being real number such that A5: for n being Element of NAT holds s < (seq ") . n ; :: according to SEQ_2:def_4 ::_thesis: contradiction set aa = abs r; set ab = abs s; set rab = 1 / ((abs r) + (abs s)); A6: ( 0 <= abs r & 0 <= abs s ) by COMPLEX1:46; A7: now__::_thesis:_for_n_being_Element_of_NAT_holds_abs_(seq_._n)_>_1_/_((abs_r)_+_(abs_s)) let n be Element of NAT ; ::_thesis: abs (seq . n) > 1 / ((abs r) + (abs s)) set g = seq . n; set t = (seq ") . n; set At = abs ((seq ") . n); (seq ") . n = 1 / (seq . n) by VALUED_1:10; then A8: abs ((seq ") . n) = 1 / (abs (seq . n)) by ABSVALUE:7; ((seq ") . n) " = ((seq . n) ") " by VALUED_1:10; then (seq ") . n <> 0 by A2, SEQ_1:5, XCMPLX_1:202; then A9: 0 < abs ((seq ") . n) by COMPLEX1:47; ( s < (seq ") . n & (seq ") . n < r ) by A4, A5; then abs ((seq ") . n) < (abs r) + (abs s) by Th37; then (abs ((seq ") . n)) " > ((abs r) + (abs s)) " by A9, XREAL_1:88; hence abs (seq . n) > 1 / ((abs r) + (abs s)) by A8; ::_thesis: verum end; A10: (seq ") . 1 < r by A4; A11: s < (seq ") . 1 by A5; now__::_thesis:_not_0_>=_(abs_r)_+_(abs_s) assume 0 >= (abs r) + (abs s) ; ::_thesis: contradiction then A12: (abs r) + (abs s) = 0 by A6; then r = 0 by Th36; hence contradiction by A11, A10, A12, Th36; ::_thesis: verum end; then consider n being Element of NAT such that A13: for m being Element of NAT st n <= m holds abs ((seq . m) - 0) < 1 / ((abs r) + (abs s)) by A1, A3, SEQ_2:def_7; abs ((seq . n) - 0) < 1 / ((abs r) + (abs s)) by A13; hence contradiction by A7; ::_thesis: verum end; theorem Th39: :: MEASURE6:39 for seq being Real_Sequence holds ( rng seq is real-bounded iff seq is bounded ) proof let seq be Real_Sequence; ::_thesis: ( rng seq is real-bounded iff seq is bounded ) thus ( rng seq is real-bounded implies seq is bounded ) ::_thesis: ( seq is bounded implies rng seq is real-bounded ) proof given s being real number such that A1: s is LowerBound of rng seq ; :: according to XXREAL_2:def_9,XXREAL_2:def_11 ::_thesis: ( not rng seq is bounded_above or seq is bounded ) given t being real number such that A2: t is UpperBound of rng seq ; :: according to XXREAL_2:def_10 ::_thesis: seq is bounded thus seq is bounded_above :: according to SEQ_2:def_8 ::_thesis: seq is bounded_below proof take t + 1 ; :: according to SEQ_2:def_3 ::_thesis: for b1 being Element of NAT holds not t + 1 <= seq . b1 let n be Element of NAT ; ::_thesis: not t + 1 <= seq . n ( seq . n <= t & t < t + 1 ) by A2, FUNCT_2:4, XREAL_1:29, XXREAL_2:def_1; hence not t + 1 <= seq . n by XXREAL_0:2; ::_thesis: verum end; take s - 1 ; :: according to SEQ_2:def_4 ::_thesis: for b1 being Element of NAT holds not seq . b1 <= s - 1 let n be Element of NAT ; ::_thesis: not seq . n <= s - 1 s < s + 1 by XREAL_1:29; then A3: s - 1 < s by XREAL_1:19; seq . n >= s by A1, FUNCT_2:4, XXREAL_2:def_2; hence not seq . n <= s - 1 by A3, XXREAL_0:2; ::_thesis: verum end; given t being real number such that A4: for n being Element of NAT holds seq . n < t ; :: according to SEQ_2:def_3,SEQ_2:def_8 ::_thesis: ( not seq is bounded_below or rng seq is real-bounded ) given s being real number such that A5: for n being Element of NAT holds seq . n > s ; :: according to SEQ_2:def_4 ::_thesis: rng seq is real-bounded thus rng seq is bounded_below :: according to XXREAL_2:def_11 ::_thesis: rng seq is bounded_above proof take s ; :: according to XXREAL_2:def_9 ::_thesis: s is LowerBound of rng seq let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in rng seq or s <= r ) assume r in rng seq ; ::_thesis: s <= r then ex n being set st ( n in dom seq & seq . n = r ) by FUNCT_1:def_3; hence s <= r by A5; ::_thesis: verum end; take t ; :: according to XXREAL_2:def_10 ::_thesis: t is UpperBound of rng seq let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in rng seq or r <= t ) assume r in rng seq ; ::_thesis: r <= t then ex n being set st ( n in dom seq & seq . n = r ) by FUNCT_1:def_3; hence r <= t by A4; ::_thesis: verum end; notation let X be real-membered set ; synonym with_max X for right_end ; synonym with_min X for left_end ; end; definition let X be real-membered set ; redefine attr X is right_end means :: MEASURE6:def 4 ( X is bounded_above & upper_bound X in X ); compatibility ( X is with_max iff ( X is bounded_above & upper_bound X in X ) ) proof thus ( X is with_max implies ( X is bounded_above & upper_bound X in X ) ) ::_thesis: ( X is bounded_above & upper_bound X in X implies X is with_max ) proof assume A1: X is with_max ; ::_thesis: ( X is bounded_above & upper_bound X in X ) hence X is bounded_above ; ::_thesis: upper_bound X in X reconsider X = X as non empty real-membered bounded_above set by A1; upper_bound X in X by A1, XXREAL_2:def_6; hence upper_bound X in X ; ::_thesis: verum end; assume A2: ( X is bounded_above & upper_bound X in X ) ; ::_thesis: X is with_max then reconsider X = X as non empty real-membered bounded_above set ; upper_bound X in X by A2; hence X is with_max by XXREAL_2:def_6; ::_thesis: verum end; redefine attr X is left_end means :: MEASURE6:def 5 ( X is bounded_below & lower_bound X in X ); compatibility ( X is with_min iff ( X is bounded_below & lower_bound X in X ) ) proof thus ( X is with_min implies ( X is bounded_below & lower_bound X in X ) ) ::_thesis: ( X is bounded_below & lower_bound X in X implies X is with_min ) proof assume A3: X is with_min ; ::_thesis: ( X is bounded_below & lower_bound X in X ) hence X is bounded_below ; ::_thesis: lower_bound X in X reconsider X = X as non empty real-membered bounded_below set by A3; lower_bound X in X by A3, XXREAL_2:def_5; hence lower_bound X in X ; ::_thesis: verum end; assume A4: ( X is bounded_below & lower_bound X in X ) ; ::_thesis: X is with_min then reconsider X = X as non empty real-membered bounded_below set ; lower_bound X in X by A4; hence X is with_min by XXREAL_2:def_5; ::_thesis: verum end; end; :: deftheorem defines with_max MEASURE6:def_4_:_ for X being real-membered set holds ( X is with_max iff ( X is bounded_above & upper_bound X in X ) ); :: deftheorem defines with_min MEASURE6:def_5_:_ for X being real-membered set holds ( X is with_min iff ( X is bounded_below & lower_bound X in X ) ); registration cluster non empty complex-membered ext-real-membered real-membered real-bounded closed for Element of bool REAL; existence ex b1 being Subset of REAL st ( not b1 is empty & b1 is closed & b1 is real-bounded ) proof [.0,0.] = {0} by XXREAL_1:17; hence ex b1 being Subset of REAL st ( not b1 is empty & b1 is closed & b1 is real-bounded ) ; ::_thesis: verum end; end; definition let R be Subset-Family of REAL; attrR is open means :: MEASURE6:def 6 for X being Subset of REAL st X in R holds X is open ; attrR is closed means :Def7: :: MEASURE6:def 7 for X being Subset of REAL st X in R holds X is closed ; end; :: deftheorem defines open MEASURE6:def_6_:_ for R being Subset-Family of REAL holds ( R is open iff for X being Subset of REAL st X in R holds X is open ); :: deftheorem Def7 defines closed MEASURE6:def_7_:_ for R being Subset-Family of REAL holds ( R is closed iff for X being Subset of REAL st X in R holds X is closed ); definition let X be Subset of REAL; :: original: -- redefine func -- X -> Subset of REAL; coherence -- X is Subset of REAL by MEMBERED:3; end; theorem :: MEASURE6:40 for r being real number for X being Subset of REAL holds ( r in X iff - r in -- X ) by MEMBER_1:11; Lm2: for X being Subset of REAL st X is bounded_above holds -- X is bounded_below proof let X be Subset of REAL; ::_thesis: ( X is bounded_above implies -- X is bounded_below ) given s being real number such that A1: s is UpperBound of X ; :: according to XXREAL_2:def_10 ::_thesis: -- X is bounded_below take - s ; :: according to XXREAL_2:def_9 ::_thesis: - s is LowerBound of -- X let t be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not t in -- X or - s <= t ) assume t in -- X ; ::_thesis: - s <= t then consider r3 being Element of COMPLEX such that A2: t = - r3 and A3: r3 in X ; reconsider r3 = r3 as Real by A3; r3 <= s by A1, A3, XXREAL_2:def_1; hence - s <= t by A2, XREAL_1:24; ::_thesis: verum end; Lm3: for X being Subset of REAL st X is bounded_below holds -- X is bounded_above proof let X be Subset of REAL; ::_thesis: ( X is bounded_below implies -- X is bounded_above ) given s being real number such that A1: s is LowerBound of X ; :: according to XXREAL_2:def_9 ::_thesis: -- X is bounded_above take - s ; :: according to XXREAL_2:def_10 ::_thesis: - s is UpperBound of -- X let t be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not t in -- X or t <= - s ) assume t in -- X ; ::_thesis: t <= - s then consider r3 being Element of COMPLEX such that A2: t = - r3 and A3: r3 in X ; reconsider r3 = r3 as Real by A3; r3 >= s by A1, A3, XXREAL_2:def_2; hence t <= - s by A2, XREAL_1:24; ::_thesis: verum end; theorem Th41: :: MEASURE6:41 for X being Subset of REAL holds ( X is bounded_above iff -- X is bounded_below ) proof let X be Subset of REAL; ::_thesis: ( X is bounded_above iff -- X is bounded_below ) X = -- (-- X) ; hence ( X is bounded_above iff -- X is bounded_below ) by Lm2, Lm3; ::_thesis: verum end; theorem :: MEASURE6:42 for X being Subset of REAL holds ( X is bounded_below iff -- X is bounded_above ) proof let X be Subset of REAL; ::_thesis: ( X is bounded_below iff -- X is bounded_above ) X = -- (-- X) ; hence ( X is bounded_below iff -- X is bounded_above ) by Th41; ::_thesis: verum end; theorem Th43: :: MEASURE6:43 for X being non empty Subset of REAL st X is bounded_below holds lower_bound X = - (upper_bound (-- X)) proof let X be non empty Subset of REAL; ::_thesis: ( X is bounded_below implies lower_bound X = - (upper_bound (-- X)) ) set r = - (upper_bound (-- X)); A1: now__::_thesis:_for_t_being_real_number_st_(_for_s_being_real_number_st_s_in_X_holds_ s_>=_t_)_holds_ -_(upper_bound_(--_X))_>=_t let t be real number ; ::_thesis: ( ( for s being real number st s in X holds s >= t ) implies - (upper_bound (-- X)) >= t ) assume A2: for s being real number st s in X holds s >= t ; ::_thesis: - (upper_bound (-- X)) >= t now__::_thesis:_for_s_being_real_number_st_s_in_--_X_holds_ s_<=_-_t let s be real number ; ::_thesis: ( s in -- X implies s <= - t ) assume s in -- X ; ::_thesis: s <= - t then - s in -- (-- X) by MEMBER_1:11; then - s >= t by A2; then - (- s) <= - t by XREAL_1:24; hence s <= - t ; ::_thesis: verum end; then - (- (upper_bound (-- X))) <= - t by SEQ_4:45; hence - (upper_bound (-- X)) >= t by XREAL_1:24; ::_thesis: verum end; assume X is bounded_below ; ::_thesis: lower_bound X = - (upper_bound (-- X)) then A3: -- X is bounded_above by Lm3; now__::_thesis:_for_s_being_real_number_st_s_in_X_holds_ s_>=_-_(upper_bound_(--_X)) let s be real number ; ::_thesis: ( s in X implies s >= - (upper_bound (-- X)) ) assume s in X ; ::_thesis: s >= - (upper_bound (-- X)) then - s in -- X by MEMBER_1:11; then - s <= - (- (upper_bound (-- X))) by A3, SEQ_4:def_1; hence s >= - (upper_bound (-- X)) by XREAL_1:24; ::_thesis: verum end; hence lower_bound X = - (upper_bound (-- X)) by A1, SEQ_4:44; ::_thesis: verum end; theorem Th44: :: MEASURE6:44 for X being non empty Subset of REAL st X is bounded_above holds upper_bound X = - (lower_bound (-- X)) proof let X be non empty Subset of REAL; ::_thesis: ( X is bounded_above implies upper_bound X = - (lower_bound (-- X)) ) set r = - (lower_bound (-- X)); A1: now__::_thesis:_for_s_being_real_number_st_(_for_t_being_real_number_st_t_in_X_holds_ t_<=_s_)_holds_ -_(lower_bound_(--_X))_<=_s let s be real number ; ::_thesis: ( ( for t being real number st t in X holds t <= s ) implies - (lower_bound (-- X)) <= s ) assume A2: for t being real number st t in X holds t <= s ; ::_thesis: - (lower_bound (-- X)) <= s now__::_thesis:_for_t_being_real_number_st_t_in_--_X_holds_ t_>=_-_s let t be real number ; ::_thesis: ( t in -- X implies t >= - s ) assume t in -- X ; ::_thesis: t >= - s then - t in -- (-- X) by MEMBER_1:11; then - t <= s by A2; then - (- t) >= - s by XREAL_1:24; hence t >= - s ; ::_thesis: verum end; then - (- (lower_bound (-- X))) >= - s by SEQ_4:43; hence - (lower_bound (-- X)) <= s by XREAL_1:24; ::_thesis: verum end; assume X is bounded_above ; ::_thesis: upper_bound X = - (lower_bound (-- X)) then A3: -- X is bounded_below by Lm2; now__::_thesis:_for_t_being_real_number_st_t_in_X_holds_ t_<=_-_(lower_bound_(--_X)) let t be real number ; ::_thesis: ( t in X implies t <= - (lower_bound (-- X)) ) assume t in X ; ::_thesis: t <= - (lower_bound (-- X)) then - t in -- X by MEMBER_1:11; then - t >= - (- (lower_bound (-- X))) by A3, SEQ_4:def_2; hence t <= - (lower_bound (-- X)) by XREAL_1:24; ::_thesis: verum end; hence upper_bound X = - (lower_bound (-- X)) by A1, SEQ_4:46; ::_thesis: verum end; Lm4: for X being Subset of REAL st X is closed holds -- X is closed proof let X be Subset of REAL; ::_thesis: ( X is closed implies -- X is closed ) assume A1: X is closed ; ::_thesis: -- X is closed let s1 be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng s1 c= -- X or not s1 is convergent or lim s1 in -- X ) assume that A2: rng s1 c= -- X and A3: s1 is convergent ; ::_thesis: lim s1 in -- X A4: - (lim s1) = lim (- s1) by A3, SEQ_2:10; A5: rng (- s1) c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (- s1) or x in X ) assume x in rng (- s1) ; ::_thesis: x in X then consider n being set such that A6: n in dom (- s1) and A7: x = (- s1) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A6; A8: s1 . n in rng s1 by FUNCT_2:4; x = - (s1 . n) by A7, SEQ_1:10; then x in -- (-- X) by A2, A8; hence x in X ; ::_thesis: verum end; - s1 is convergent by A3; then lim (- s1) in X by A1, A5, RCOMP_1:def_4; then - (- (lim s1)) in -- X by A4, MEMBER_1:11; hence lim s1 in -- X ; ::_thesis: verum end; theorem :: MEASURE6:45 for X being Subset of REAL holds ( X is closed iff -- X is closed ) proof let X be Subset of REAL; ::_thesis: ( X is closed iff -- X is closed ) -- (-- X) = X ; hence ( X is closed iff -- X is closed ) by Lm4; ::_thesis: verum end; Lm5: for X being Subset of REAL for p being Real holds p ++ X = { (p + r3) where r3 is Real : r3 in X } proof let X be Subset of REAL; ::_thesis: for p being Real holds p ++ X = { (p + r3) where r3 is Real : r3 in X } let p be Real; ::_thesis: p ++ X = { (p + r3) where r3 is Real : r3 in X } thus p ++ X c= { (p + r3) where r3 is Real : r3 in X } :: according to XBOOLE_0:def_10 ::_thesis: { (p + r3) where r3 is Real : r3 in X } c= p ++ X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in p ++ X or x in { (p + r3) where r3 is Real : r3 in X } ) assume A1: x in p ++ X ; ::_thesis: x in { (p + r3) where r3 is Real : r3 in X } then reconsider x9 = x as Real ; ex z being Real st ( z in X & x9 = p + z ) by A1, Lm1; hence x in { (p + r3) where r3 is Real : r3 in X } ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (p + r3) where r3 is Real : r3 in X } or x in p ++ X ) assume x in { (p + r3) where r3 is Real : r3 in X } ; ::_thesis: x in p ++ X then ex r3 being Real st ( x = p + r3 & r3 in X ) ; hence x in p ++ X by Lm1; ::_thesis: verum end; theorem Th46: :: MEASURE6:46 for r being real number for X being Subset of REAL for q3 being Real holds ( r in X iff q3 + r in q3 ++ X ) proof let r be real number ; ::_thesis: for X being Subset of REAL for q3 being Real holds ( r in X iff q3 + r in q3 ++ X ) let X be Subset of REAL; ::_thesis: for q3 being Real holds ( r in X iff q3 + r in q3 ++ X ) let q3 be Real; ::_thesis: ( r in X iff q3 + r in q3 ++ X ) thus ( r in X implies q3 + r in q3 ++ X ) by MEMBER_1:141; ::_thesis: ( q3 + r in q3 ++ X implies r in X ) assume q3 + r in q3 ++ X ; ::_thesis: r in X then q3 + r in { (q3 + r3) where r3 is Real : r3 in X } by Lm5; then ex mr being Real st ( q3 + r = q3 + mr & mr in X ) ; hence r in X ; ::_thesis: verum end; theorem :: MEASURE6:47 for X being Subset of REAL holds X = 0 ++ X by MEMBER_1:146; theorem :: MEASURE6:48 for X being Subset of REAL for q3, p3 being Real holds q3 ++ (p3 ++ X) = (q3 + p3) ++ X by MEMBER_1:147; Lm6: for X being Subset of REAL for s being Real st X is bounded_above holds s ++ X is bounded_above proof let X be Subset of REAL; ::_thesis: for s being Real st X is bounded_above holds s ++ X is bounded_above let p be Real; ::_thesis: ( X is bounded_above implies p ++ X is bounded_above ) given s being real number such that A1: s is UpperBound of X ; :: according to XXREAL_2:def_10 ::_thesis: p ++ X is bounded_above take p + s ; :: according to XXREAL_2:def_10 ::_thesis: p + s is UpperBound of p ++ X let t be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not t in p ++ X or t <= p + s ) assume t in p ++ X ; ::_thesis: t <= p + s then t in { (p + r3) where r3 is Real : r3 in X } by Lm5; then consider r3 being Real such that A2: t = p + r3 and A3: r3 in X ; r3 <= s by A1, A3, XXREAL_2:def_1; hence t <= p + s by A2, XREAL_1:6; ::_thesis: verum end; theorem :: MEASURE6:49 for X being Subset of REAL for q3 being Real holds ( X is bounded_above iff q3 ++ X is bounded_above ) proof let X be Subset of REAL; ::_thesis: for q3 being Real holds ( X is bounded_above iff q3 ++ X is bounded_above ) let q3 be Real; ::_thesis: ( X is bounded_above iff q3 ++ X is bounded_above ) (- q3) ++ (q3 ++ X) = ((- q3) + q3) ++ X by MEMBER_1:147 .= X by MEMBER_1:146 ; hence ( X is bounded_above iff q3 ++ X is bounded_above ) by Lm6; ::_thesis: verum end; Lm7: for X being Subset of REAL for p being Real st X is bounded_below holds p ++ X is bounded_below proof let X be Subset of REAL; ::_thesis: for p being Real st X is bounded_below holds p ++ X is bounded_below let p be Real; ::_thesis: ( X is bounded_below implies p ++ X is bounded_below ) given s being real number such that A1: s is LowerBound of X ; :: according to XXREAL_2:def_9 ::_thesis: p ++ X is bounded_below take p + s ; :: according to XXREAL_2:def_9 ::_thesis: p + s is LowerBound of p ++ X let t be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not t in p ++ X or p + s <= t ) assume t in p ++ X ; ::_thesis: p + s <= t then t in { (p + r3) where r3 is Real : r3 in X } by Lm5; then consider r3 being Real such that A2: t = p + r3 and A3: r3 in X ; r3 >= s by A1, A3, XXREAL_2:def_2; hence p + s <= t by A2, XREAL_1:6; ::_thesis: verum end; theorem :: MEASURE6:50 for X being Subset of REAL for q3 being Real holds ( X is bounded_below iff q3 ++ X is bounded_below ) proof let X be Subset of REAL; ::_thesis: for q3 being Real holds ( X is bounded_below iff q3 ++ X is bounded_below ) let q3 be Real; ::_thesis: ( X is bounded_below iff q3 ++ X is bounded_below ) (- q3) ++ (q3 ++ X) = ((- q3) + q3) ++ X by MEMBER_1:147 .= X by MEMBER_1:146 ; hence ( X is bounded_below iff q3 ++ X is bounded_below ) by Lm7; ::_thesis: verum end; theorem :: MEASURE6:51 for q3 being Real for X being non empty Subset of REAL st X is bounded_below holds lower_bound (q3 ++ X) = q3 + (lower_bound X) proof let q3 be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_below holds lower_bound (q3 ++ X) = q3 + (lower_bound X) let X be non empty Subset of REAL; ::_thesis: ( X is bounded_below implies lower_bound (q3 ++ X) = q3 + (lower_bound X) ) assume A1: X is bounded_below ; ::_thesis: lower_bound (q3 ++ X) = q3 + (lower_bound X) set i = q3 + (lower_bound X); A2: now__::_thesis:_for_t_being_real_number_st_(_for_s_being_real_number_st_s_in_q3_++_X_holds_ s_>=_t_)_holds_ t_<=_q3_+_(lower_bound_X) let t be real number ; ::_thesis: ( ( for s being real number st s in q3 ++ X holds s >= t ) implies t <= q3 + (lower_bound X) ) assume A3: for s being real number st s in q3 ++ X holds s >= t ; ::_thesis: t <= q3 + (lower_bound X) now__::_thesis:_for_s_being_real_number_st_s_in_X_holds_ t_-_q3_<=_s let s be real number ; ::_thesis: ( s in X implies t - q3 <= s ) assume s in X ; ::_thesis: t - q3 <= s then t <= q3 + s by A3, MEMBER_1:141; hence t - q3 <= s by XREAL_1:20; ::_thesis: verum end; then lower_bound X >= t - q3 by SEQ_4:43; hence t <= q3 + (lower_bound X) by XREAL_1:20; ::_thesis: verum end; now__::_thesis:_for_s_being_real_number_st_s_in_q3_++_X_holds_ s_>=_q3_+_(lower_bound_X) let s be real number ; ::_thesis: ( s in q3 ++ X implies s >= q3 + (lower_bound X) ) assume s in q3 ++ X ; ::_thesis: s >= q3 + (lower_bound X) then s in { (q3 + r3) where r3 is Real : r3 in X } by Lm5; then consider r3 being Real such that A4: q3 + r3 = s and A5: r3 in X ; r3 >= lower_bound X by A1, A5, SEQ_4:def_2; hence s >= q3 + (lower_bound X) by A4, XREAL_1:6; ::_thesis: verum end; hence lower_bound (q3 ++ X) = q3 + (lower_bound X) by A2, SEQ_4:44; ::_thesis: verum end; theorem :: MEASURE6:52 for q3 being Real for X being non empty Subset of REAL st X is bounded_above holds upper_bound (q3 ++ X) = q3 + (upper_bound X) proof let q3 be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_above holds upper_bound (q3 ++ X) = q3 + (upper_bound X) let X be non empty Subset of REAL; ::_thesis: ( X is bounded_above implies upper_bound (q3 ++ X) = q3 + (upper_bound X) ) assume A1: X is bounded_above ; ::_thesis: upper_bound (q3 ++ X) = q3 + (upper_bound X) set i = q3 + (upper_bound X); A2: now__::_thesis:_for_t_being_real_number_st_(_for_s_being_real_number_st_s_in_q3_++_X_holds_ s_<=_t_)_holds_ q3_+_(upper_bound_X)_<=_t let t be real number ; ::_thesis: ( ( for s being real number st s in q3 ++ X holds s <= t ) implies q3 + (upper_bound X) <= t ) assume A3: for s being real number st s in q3 ++ X holds s <= t ; ::_thesis: q3 + (upper_bound X) <= t now__::_thesis:_for_s_being_real_number_st_s_in_X_holds_ s_<=_t_-_q3 let s be real number ; ::_thesis: ( s in X implies s <= t - q3 ) assume s in X ; ::_thesis: s <= t - q3 then q3 + s <= t by A3, MEMBER_1:141; hence s <= t - q3 by XREAL_1:19; ::_thesis: verum end; then upper_bound X <= t - q3 by SEQ_4:45; hence q3 + (upper_bound X) <= t by XREAL_1:19; ::_thesis: verum end; now__::_thesis:_for_s_being_real_number_st_s_in_q3_++_X_holds_ s_<=_q3_+_(upper_bound_X) let s be real number ; ::_thesis: ( s in q3 ++ X implies s <= q3 + (upper_bound X) ) assume s in q3 ++ X ; ::_thesis: s <= q3 + (upper_bound X) then s in { (q3 + r3) where r3 is Real : r3 in X } by Lm5; then consider r3 being Real such that A4: q3 + r3 = s and A5: r3 in X ; r3 <= upper_bound X by A1, A5, SEQ_4:def_1; hence s <= q3 + (upper_bound X) by A4, XREAL_1:6; ::_thesis: verum end; hence upper_bound (q3 ++ X) = q3 + (upper_bound X) by A2, SEQ_4:46; ::_thesis: verum end; Lm8: for q3 being Real for X being Subset of REAL st X is closed holds q3 ++ X is closed proof let q3 be Real; ::_thesis: for X being Subset of REAL st X is closed holds q3 ++ X is closed let X be Subset of REAL; ::_thesis: ( X is closed implies q3 ++ X is closed ) assume A1: X is closed ; ::_thesis: q3 ++ X is closed A2: q3 ++ X = { (q3 + r3) where r3 is Real : r3 in X } by Lm5; reconsider s0 = NAT --> q3 as Real_Sequence ; let s1 be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng s1 c= q3 ++ X or not s1 is convergent or lim s1 in q3 ++ X ) assume that A3: rng s1 c= q3 ++ X and A4: s1 is convergent ; ::_thesis: lim s1 in q3 ++ X lim (s1 - s0) = (lim s1) - (s0 . 0) by A4, SEQ_4:42 .= (lim s1) - q3 by FUNCOP_1:7 ; then A5: q3 + (lim (s1 - s0)) = lim s1 ; A6: rng (s1 - s0) c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (s1 - s0) or x in X ) assume A7: x in rng (s1 - s0) ; ::_thesis: x in X then consider n being set such that A8: n in dom (s1 - s0) and A9: x = (s1 - s0) . n by FUNCT_1:def_3; reconsider x9 = x as Real by A7; reconsider n = n as Element of NAT by A8; A10: s1 . n in rng s1 by FUNCT_2:4; x = (s1 . n) + ((- s0) . n) by A9, SEQ_1:7 .= (s1 . n) + (- (s0 . n)) by SEQ_1:10 .= (s1 . n) - q3 by FUNCOP_1:7 ; then x9 + q3 in q3 ++ X by A3, A10; hence x in X by Th46; ::_thesis: verum end; s1 - s0 is convergent by A4; then lim (s1 - s0) in X by A1, A6, RCOMP_1:def_4; hence lim s1 in q3 ++ X by A5, A2; ::_thesis: verum end; theorem :: MEASURE6:53 for X being Subset of REAL for q3 being Real holds ( X is closed iff q3 ++ X is closed ) proof let X be Subset of REAL; ::_thesis: for q3 being Real holds ( X is closed iff q3 ++ X is closed ) let q3 be Real; ::_thesis: ( X is closed iff q3 ++ X is closed ) (- q3) ++ (q3 ++ X) = ((- q3) + q3) ++ X by MEMBER_1:147 .= X by MEMBER_1:146 ; hence ( X is closed iff q3 ++ X is closed ) by Lm8; ::_thesis: verum end; definition let X be Subset of REAL; func Inv X -> Subset of REAL equals :: MEASURE6:def 8 { (1 / r3) where r3 is Real : r3 in X } ; coherence { (1 / r3) where r3 is Real : r3 in X } is Subset of REAL proof deffunc H1( Real) -> Element of REAL = 1 / \$1; defpred S1[ set ] means \$1 in X; thus { H1(r3) where r3 is Real : S1[r3] } is Subset of REAL from DOMAIN_1:sch_8(); ::_thesis: verum end; involutiveness for b1, b2 being Subset of REAL st b1 = { (1 / r3) where r3 is Real : r3 in b2 } holds b2 = { (1 / r3) where r3 is Real : r3 in b1 } proof let Y, X be Subset of REAL; ::_thesis: ( Y = { (1 / r3) where r3 is Real : r3 in X } implies X = { (1 / r3) where r3 is Real : r3 in Y } ) assume A1: Y = { (1 / r3) where r3 is Real : r3 in X } ; ::_thesis: X = { (1 / r3) where r3 is Real : r3 in Y } thus X c= { (1 / r3) where r3 is Real : r3 in Y } :: according to XBOOLE_0:def_10 ::_thesis: { (1 / r3) where r3 is Real : r3 in Y } c= X proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in X or e in { (1 / r3) where r3 is Real : r3 in Y } ) assume A2: e in X ; ::_thesis: e in { (1 / r3) where r3 is Real : r3 in Y } then reconsider r = e as Element of REAL ; A3: 1 / (1 / r) = r ; 1 / r in Y by A1, A2; hence e in { (1 / r3) where r3 is Real : r3 in Y } by A3; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (1 / r3) where r3 is Real : r3 in Y } or e in X ) assume e in { (1 / r3) where r3 is Real : r3 in Y } ; ::_thesis: e in X then consider r3 being Real such that A4: e = 1 / r3 and A5: r3 in Y ; ex r1 being Real st ( r3 = 1 / r1 & r1 in X ) by A1, A5; hence e in X by A4; ::_thesis: verum end; end; :: deftheorem defines Inv MEASURE6:def_8_:_ for X being Subset of REAL holds Inv X = { (1 / r3) where r3 is Real : r3 in X } ; theorem Th54: :: MEASURE6:54 for r being real number for X being Subset of REAL holds ( r in X iff 1 / r in Inv X ) proof let r be real number ; ::_thesis: for X being Subset of REAL holds ( r in X iff 1 / r in Inv X ) let X be Subset of REAL; ::_thesis: ( r in X iff 1 / r in Inv X ) thus ( r in X implies 1 / r in Inv X ) ; ::_thesis: ( 1 / r in Inv X implies r in X ) assume 1 / r in Inv X ; ::_thesis: r in X then ex mr being Real st ( 1 / r = 1 / mr & mr in X ) ; hence r in X by XCMPLX_1:59; ::_thesis: verum end; registration let X be non empty Subset of REAL; cluster Inv X -> non empty ; coherence not Inv X is empty proof ex x being Real st x in X by SUBSET_1:4; hence not Inv X is empty by Th54; ::_thesis: verum end; end; registration let X be without_zero Subset of REAL; cluster Inv X -> without_zero ; coherence Inv X is without_zero proof now__::_thesis:_not_0_in_Inv_X assume 0 in Inv X ; ::_thesis: contradiction then ex r3 being Real st ( 0 = 1 / r3 & r3 in X ) ; hence contradiction by XCMPLX_1:202; ::_thesis: verum end; hence Inv X is without_zero by Def2; ::_thesis: verum end; end; theorem :: MEASURE6:55 for X being without_zero Subset of REAL st X is closed & X is real-bounded holds Inv X is closed proof let X be without_zero Subset of REAL; ::_thesis: ( X is closed & X is real-bounded implies Inv X is closed ) assume that A1: X is closed and A2: X is real-bounded ; ::_thesis: Inv X is closed let s1 be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng s1 c= Inv X or not s1 is convergent or lim s1 in Inv X ) assume that A3: rng s1 c= Inv X and A4: s1 is convergent ; ::_thesis: lim s1 in Inv X A5: rng (s1 ") c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (s1 ") or x in X ) assume x in rng (s1 ") ; ::_thesis: x in X then consider n being set such that A6: n in dom (s1 ") and A7: x = (s1 ") . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A6; s1 . n in rng s1 by FUNCT_2:4; then 1 / (s1 . n) in Inv (Inv X) by A3; hence x in X by A7, VALUED_1:10; ::_thesis: verum end; A8: not 0 in rng s1 by A3; A9: now__::_thesis:_s1_is_non-zero assume not s1 is non-zero ; ::_thesis: contradiction then ex n being Element of NAT st s1 . n = 0 by SEQ_1:5; hence contradiction by A8, FUNCT_2:4; ::_thesis: verum end; A10: now__::_thesis:_not_lim_s1_=_0 A11: rng (s1 ") c= X proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (s1 ") or y in X ) assume y in rng (s1 ") ; ::_thesis: y in X then consider x being set such that A12: x in dom (s1 ") and A13: y = (s1 ") . x by FUNCT_1:def_3; reconsider x = x as Element of NAT by A12; s1 . x in rng s1 by FUNCT_2:4; then 1 / (s1 . x) in Inv (Inv X) by A3; hence y in X by A13, VALUED_1:10; ::_thesis: verum end; assume lim s1 = 0 ; ::_thesis: contradiction then not s1 " is bounded by A4, A9, Th38; then not rng (s1 ") is real-bounded by Th39; hence contradiction by A2, A11, XXREAL_2:45; ::_thesis: verum end; then s1 " is convergent by A4, A9, SEQ_2:21; then lim (s1 ") in X by A1, A5, RCOMP_1:def_4; then 1 / (lim s1) in X by A4, A9, A10, SEQ_2:22; then 1 / (1 / (lim s1)) in Inv X ; hence lim s1 in Inv X ; ::_thesis: verum end; theorem Th56: :: MEASURE6:56 for Z being Subset-Family of REAL st Z is closed holds meet Z is closed proof let Z be Subset-Family of REAL; ::_thesis: ( Z is closed implies meet Z is closed ) assume A1: Z is closed ; ::_thesis: meet Z is closed let seq be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng seq c= meet Z or not seq is convergent or lim seq in meet Z ) set mZ = meet Z; assume that A2: rng seq c= meet Z and A3: seq is convergent ; ::_thesis: lim seq in meet Z percases ( Z = {} or Z <> {} ) ; suppose Z = {} ; ::_thesis: lim seq in meet Z then meet Z = {} by SETFAM_1:def_1; hence lim seq in meet Z by A2; ::_thesis: verum end; supposeA4: Z <> {} ; ::_thesis: lim seq in meet Z now__::_thesis:_for_X_being_set_st_X_in_Z_holds_ lim_seq_in_X let X be set ; ::_thesis: ( X in Z implies lim seq in X ) assume A5: X in Z ; ::_thesis: lim seq in X then reconsider X9 = X as Subset of REAL ; A6: rng seq c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng seq or x in X ) assume x in rng seq ; ::_thesis: x in X hence x in X by A2, A5, SETFAM_1:def_1; ::_thesis: verum end; X9 is closed by A1, A5, Def7; hence lim seq in X by A3, A6, RCOMP_1:def_4; ::_thesis: verum end; hence lim seq in meet Z by A4, SETFAM_1:def_1; ::_thesis: verum end; end; end; definition let X be Subset of REAL; func Cl X -> Subset of REAL equals :: MEASURE6:def 9 meet { A where A is Subset of REAL : ( X c= A & A is closed ) } ; coherence meet { A where A is Subset of REAL : ( X c= A & A is closed ) } is Subset of REAL proof defpred S1[ Subset of REAL] means ( X c= \$1 & \$1 is closed ); reconsider Z = { A where A is Subset of REAL : S1[A] } as Subset-Family of REAL from DOMAIN_1:sch_7(); reconsider Z = Z as Subset-Family of REAL ; meet Z is Subset of REAL ; hence meet { A where A is Subset of REAL : ( X c= A & A is closed ) } is Subset of REAL ; ::_thesis: verum end; projectivity for b1, b2 being Subset of REAL st b1 = meet { A where A is Subset of REAL : ( b2 c= A & A is closed ) } holds b1 = meet { A where A is Subset of REAL : ( b1 c= A & A is closed ) } proof reconsider W = [#] REAL as Subset of REAL ; let IT, X be Subset of REAL; ::_thesis: ( IT = meet { A where A is Subset of REAL : ( X c= A & A is closed ) } implies IT = meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } ) set ClX = { A where A is Subset of REAL : ( X c= A & A is closed ) } ; set ClIT = { A where A is Subset of REAL : ( IT c= A & A is closed ) } ; assume A1: IT = meet { A where A is Subset of REAL : ( X c= A & A is closed ) } ; ::_thesis: IT = meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } A2: W in { A where A is Subset of REAL : ( X c= A & A is closed ) } ; A3: W in { A where A is Subset of REAL : ( IT c= A & A is closed ) } ; thus IT c= meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } :: according to XBOOLE_0:def_10 ::_thesis: meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } c= IT proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in IT or e in meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } ) assume A4: e in IT ; ::_thesis: e in meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } for Y being set st Y in { A where A is Subset of REAL : ( IT c= A & A is closed ) } holds e in Y proof let Y be set ; ::_thesis: ( Y in { A where A is Subset of REAL : ( IT c= A & A is closed ) } implies e in Y ) assume Y in { A where A is Subset of REAL : ( IT c= A & A is closed ) } ; ::_thesis: e in Y then consider A being Subset of REAL such that A5: A = Y and A6: IT c= A and A7: A is closed ; for Z being set st Z in { A where A is Subset of REAL : ( X c= A & A is closed ) } holds X c= Z proof let Z be set ; ::_thesis: ( Z in { A where A is Subset of REAL : ( X c= A & A is closed ) } implies X c= Z ) assume Z in { A where A is Subset of REAL : ( X c= A & A is closed ) } ; ::_thesis: X c= Z then ex B being Subset of REAL st ( Z = B & X c= B & B is closed ) ; hence X c= Z ; ::_thesis: verum end; then X c= IT by A1, A2, SETFAM_1:5; then X c= A by A6, XBOOLE_1:1; then A in { A where A is Subset of REAL : ( X c= A & A is closed ) } by A7; hence e in Y by A1, A4, A5, SETFAM_1:def_1; ::_thesis: verum end; hence e in meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } by A3, SETFAM_1:def_1; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } or e in IT ) assume A8: e in meet { A where A is Subset of REAL : ( IT c= A & A is closed ) } ; ::_thesis: e in IT for Y being set st Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } holds e in Y proof let Y be set ; ::_thesis: ( Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } implies e in Y ) assume A9: Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } ; ::_thesis: e in Y then consider A being Subset of REAL such that A10: A = Y and X c= A and A11: A is closed ; IT c= A by A1, A9, A10, SETFAM_1:3; then A in { A where A is Subset of REAL : ( IT c= A & A is closed ) } by A11; hence e in Y by A8, A10, SETFAM_1:def_1; ::_thesis: verum end; hence e in IT by A1, A2, SETFAM_1:def_1; ::_thesis: verum end; end; :: deftheorem defines Cl MEASURE6:def_9_:_ for X being Subset of REAL holds Cl X = meet { A where A is Subset of REAL : ( X c= A & A is closed ) } ; registration let X be Subset of REAL; cluster Cl X -> closed ; coherence Cl X is closed proof defpred S1[ Subset of REAL] means ( X c= X & X is closed ); reconsider Z = { A where A is Subset of REAL : S1[A] } as Subset-Family of REAL from DOMAIN_1:sch_7(); reconsider Z = Z as Subset-Family of REAL ; Z is closed proof let Y be Subset of REAL; :: according to MEASURE6:def_7 ::_thesis: ( Y in Z implies Y is closed ) assume Y in Z ; ::_thesis: Y is closed then ex A being Subset of REAL st ( Y = A & X c= A & A is closed ) ; hence Y is closed ; ::_thesis: verum end; hence Cl X is closed by Th56; ::_thesis: verum end; end; theorem Th57: :: MEASURE6:57 for X being Subset of REAL for Y being closed Subset of REAL st X c= Y holds Cl X c= Y proof let X be Subset of REAL; ::_thesis: for Y being closed Subset of REAL st X c= Y holds Cl X c= Y let Y be closed Subset of REAL; ::_thesis: ( X c= Y implies Cl X c= Y ) set ClX = { A where A is Subset of REAL : ( X c= A & A is closed ) } ; assume X c= Y ; ::_thesis: Cl X c= Y then Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } ; hence Cl X c= Y by SETFAM_1:3; ::_thesis: verum end; theorem Th58: :: MEASURE6:58 for X being Subset of REAL holds X c= Cl X proof let X be Subset of REAL; ::_thesis: X c= Cl X let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Cl X ) set ClX = { A where A is Subset of REAL : ( X c= A & A is closed ) } ; assume A1: x in X ; ::_thesis: x in Cl X A2: now__::_thesis:_for_Y_being_set_st_Y_in__{__A_where_A_is_Subset_of_REAL_:_(_X_c=_A_&_A_is_closed_)__}__holds_ x_in_Y let Y be set ; ::_thesis: ( Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } implies x in Y ) assume Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } ; ::_thesis: x in Y then ex YY being Subset of REAL st ( YY = Y & X c= YY & YY is closed ) ; hence x in Y by A1; ::_thesis: verum end; [#] REAL in { A where A is Subset of REAL : ( X c= A & A is closed ) } ; hence x in Cl X by A2, SETFAM_1:def_1; ::_thesis: verum end; theorem Th59: :: MEASURE6:59 for X being Subset of REAL holds ( X is closed iff X = Cl X ) proof let X be Subset of REAL; ::_thesis: ( X is closed iff X = Cl X ) hereby ::_thesis: ( X = Cl X implies X is closed ) set ClX = { A where A is Subset of REAL : ( X c= A & A is closed ) } ; assume X is closed ; ::_thesis: X = Cl X then X in { A where A is Subset of REAL : ( X c= A & A is closed ) } ; then A1: Cl X c= X by SETFAM_1:3; X c= Cl X by Th58; hence X = Cl X by A1, XBOOLE_0:def_10; ::_thesis: verum end; thus ( X = Cl X implies X is closed ) ; ::_thesis: verum end; theorem :: MEASURE6:60 Cl ({} REAL) = {} by Th59; theorem :: MEASURE6:61 Cl ([#] REAL) = REAL by Th59; theorem :: MEASURE6:62 for X, Y being Subset of REAL st X c= Y holds Cl X c= Cl Y proof let X, Y be Subset of REAL; ::_thesis: ( X c= Y implies Cl X c= Cl Y ) assume A1: X c= Y ; ::_thesis: Cl X c= Cl Y set ClX = { A where A is Subset of REAL : ( X c= A & A is closed ) } ; Y c= Cl Y by Th58; then X c= Cl Y by A1, XBOOLE_1:1; then Cl Y in { A where A is Subset of REAL : ( X c= A & A is closed ) } ; hence Cl X c= Cl Y by SETFAM_1:3; ::_thesis: verum end; theorem Th63: :: MEASURE6:63 for X being Subset of REAL for r3 being Real holds ( r3 in Cl X iff for O being open Subset of REAL st r3 in O holds not O /\ X is empty ) proof let X be Subset of REAL; ::_thesis: for r3 being Real holds ( r3 in Cl X iff for O being open Subset of REAL st r3 in O holds not O /\ X is empty ) let r3 be Real; ::_thesis: ( r3 in Cl X iff for O being open Subset of REAL st r3 in O holds not O /\ X is empty ) hereby ::_thesis: ( ( for O being open Subset of REAL st r3 in O holds not O /\ X is empty ) implies r3 in Cl X ) assume A1: r3 in Cl X ; ::_thesis: for O being open Subset of REAL st r3 in O holds not O /\ X is empty let O be open Subset of REAL; ::_thesis: ( r3 in O implies not O /\ X is empty ) assume that A2: r3 in O and A3: O /\ X is empty ; ::_thesis: contradiction O misses X by A3, XBOOLE_0:def_7; then A4: X c= O ` by SUBSET_1:23; A5: O misses O ` by SUBSET_1:24; O ` is closed by RCOMP_1:def_5; then Cl X c= O ` by A4, Th57; hence contradiction by A1, A2, A5, XBOOLE_0:3; ::_thesis: verum end; ((Cl X) `) ` = Cl X ; then A6: (Cl X) ` is open by RCOMP_1:def_5; ( X c= Cl X & ((Cl X) `) /\ X c= X ) by Th58, XBOOLE_1:17; then A7: ((Cl X) `) /\ X c= Cl X by XBOOLE_1:1; ((Cl X) `) /\ X c= (Cl X) ` by XBOOLE_1:17; then A8: ((Cl X) `) /\ X is empty by A7, SUBSET_1:20; assume for O being open Subset of REAL st r3 in O holds not O /\ X is empty ; ::_thesis: r3 in Cl X then not r3 in (Cl X) ` by A6, A8; hence r3 in Cl X by SUBSET_1:29; ::_thesis: verum end; theorem :: MEASURE6:64 for X being Subset of REAL for r3 being Real st r3 in Cl X holds ex seq being Real_Sequence st ( rng seq c= X & seq is convergent & lim seq = r3 ) proof let X be Subset of REAL; ::_thesis: for r3 being Real st r3 in Cl X holds ex seq being Real_Sequence st ( rng seq c= X & seq is convergent & lim seq = r3 ) let r3 be Real; ::_thesis: ( r3 in Cl X implies ex seq being Real_Sequence st ( rng seq c= X & seq is convergent & lim seq = r3 ) ) defpred S1[ set , set ] means ex n being Nat st ( \$1 = n & \$2 = choose (X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[) ); assume A1: r3 in Cl X ; ::_thesis: ex seq being Real_Sequence st ( rng seq c= X & seq is convergent & lim seq = r3 ) A2: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ ex_u_being_set_st_ (_u_in_REAL_&_S1[x,u]_) let x be set ; ::_thesis: ( x in NAT implies ex u being set st ( u in REAL & S1[x,u] ) ) assume x in NAT ; ::_thesis: ex u being set st ( u in REAL & S1[x,u] ) then reconsider n = x as Element of NAT ; set n1 = n + 1; set oi = ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[; reconsider u = choose (X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[) as set ; take u = u; ::_thesis: ( u in REAL & S1[x,u] ) A3: r3 < r3 + (1 / (n + 1)) by XREAL_1:29; then r3 - (1 / (n + 1)) < r3 by XREAL_1:19; then r3 in ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ by A3; then not X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ is empty by A1, Th63; then u in X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ ; hence u in REAL ; ::_thesis: S1[x,u] thus S1[x,u] ; ::_thesis: verum end; consider seq being Function such that A4: ( dom seq = NAT & rng seq c= REAL ) and A5: for x being set st x in NAT holds S1[x,seq . x] from FUNCT_1:sch_5(A2); reconsider seq = seq as Real_Sequence by A4, FUNCT_2:def_1, RELSET_1:4; take seq ; ::_thesis: ( rng seq c= X & seq is convergent & lim seq = r3 ) thus rng seq c= X ::_thesis: ( seq is convergent & lim seq = r3 ) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng seq or y in X ) assume y in rng seq ; ::_thesis: y in X then consider x being set such that A6: x in dom seq and A7: seq . x = y by FUNCT_1:def_3; consider n being Nat such that x = n and A8: seq . x = choose (X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[) by A5, A6; reconsider n = n as Element of NAT by ORDINAL1:def_12; set n1 = n + 1; set oi = ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[; A9: r3 < r3 + (1 / (n + 1)) by XREAL_1:29; then r3 - (1 / (n + 1)) < r3 by XREAL_1:19; then r3 in ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ by A9; then not X /\ ].(r3 - (1 / (n + 1))),(r3 + (1 / (n + 1))).[ is empty by A1, Th63; hence y in X by A7, A8, XBOOLE_0:def_4; ::_thesis: verum end; A10: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_((seq_._m)_-_r3)_<_p let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - r3) < p ) set cp = [/(1 / p)\]; A11: 1 / p <= [/(1 / p)\] by INT_1:def_7; assume A12: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - r3) < p then A13: 0 < [/(1 / p)\] by INT_1:def_7; then reconsider cp = [/(1 / p)\] as Element of NAT by INT_1:3; take n = cp; ::_thesis: for m being Element of NAT st n <= m holds abs ((seq . m) - r3) < p n < n + 1 by NAT_1:13; then A14: 1 / (n + 1) < 1 / n by A13, XREAL_1:88; 1 / (1 / p) >= 1 / cp by A12, A11, XREAL_1:85; then A15: 1 / (n + 1) < p by A14, XXREAL_0:2; let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((seq . m) - r3) < p ) assume n <= m ; ::_thesis: abs ((seq . m) - r3) < p then A16: n + 1 <= m + 1 by XREAL_1:6; set m1 = m + 1; 1 / (m + 1) <= 1 / (n + 1) by A16, XREAL_1:85; then A17: 1 / (m + 1) < p by A15, XXREAL_0:2; set oi = ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[; A18: r3 < r3 + (1 / (m + 1)) by XREAL_1:29; then r3 - (1 / (m + 1)) < r3 by XREAL_1:19; then r3 in ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[ by A18; then A19: not X /\ ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[ is empty by A1, Th63; ex m9 being Nat st ( m9 = m & seq . m = choose (X /\ ].(r3 - (1 / (m9 + 1))),(r3 + (1 / (m9 + 1))).[) ) by A5; then seq . m in ].(r3 - (1 / (m + 1))),(r3 + (1 / (m + 1))).[ by A19, XBOOLE_0:def_4; then consider s being Real such that A20: seq . m = s and A21: ( r3 - (1 / (m + 1)) < s & s < r3 + (1 / (m + 1)) ) ; ( - (1 / (m + 1)) < s - r3 & s - r3 < 1 / (m + 1) ) by A21, XREAL_1:19, XREAL_1:20; then abs (s - r3) < 1 / (m + 1) by SEQ_2:1; hence abs ((seq . m) - r3) < p by A20, A17, XXREAL_0:2; ::_thesis: verum end; hence seq is convergent by SEQ_2:def_6; ::_thesis: lim seq = r3 hence lim seq = r3 by A10, SEQ_2:def_7; ::_thesis: verum end; begin definition let X be set ; let f be Function of X,REAL; :: original: bounded_below redefine attrf is bounded_below means :: MEASURE6:def 10 f .: X is bounded_below ; compatibility ( f is bounded_below iff f .: X is bounded_below ) proof A1: dom f = X by FUNCT_2:def_1; thus ( f is bounded_below implies f .: X is bounded_below ) ::_thesis: ( f .: X is bounded_below implies f is bounded_below ) proof given r being real number such that A2: for y being set st y in dom f holds r < f . y ; :: according to SEQ_2:def_2 ::_thesis: f .: X is bounded_below take r ; :: according to XXREAL_2:def_9 ::_thesis: r is LowerBound of f .: X let s be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not s in f .: X or r <= s ) assume s in f .: X ; ::_thesis: r <= s then ex x being set st ( x in X & x in X & s = f . x ) by FUNCT_2:64; hence r <= s by A1, A2; ::_thesis: verum end; given p being real number such that A3: p is LowerBound of f .: X ; :: according to XXREAL_2:def_9 ::_thesis: f is bounded_below take p - 1 ; :: according to SEQ_2:def_2 ::_thesis: for b1 being set holds ( not b1 in dom f or not f . b1 <= p - 1 ) let y be set ; ::_thesis: ( not y in dom f or not f . y <= p - 1 ) assume y in dom f ; ::_thesis: not f . y <= p - 1 then f . y in rng f by FUNCT_1:3; then f . y in f .: X by RELSET_1:22; then A4: p <= f . y by A3, XXREAL_2:def_2; f . y < (f . y) + 1 by XREAL_1:29; then p < (f . y) + 1 by A4, XXREAL_0:2; hence not f . y <= p - 1 by XREAL_1:19; ::_thesis: verum end; :: original: bounded_above redefine attrf is bounded_above means :: MEASURE6:def 11 f .: X is bounded_above ; compatibility ( f is bounded_above iff f .: X is bounded_above ) proof A5: dom f = X by FUNCT_2:def_1; thus ( f is bounded_above implies f .: X is bounded_above ) ::_thesis: ( f .: X is bounded_above implies f is bounded_above ) proof given r being real number such that A6: for y being set st y in dom f holds r > f . y ; :: according to SEQ_2:def_1 ::_thesis: f .: X is bounded_above take r ; :: according to XXREAL_2:def_10 ::_thesis: r is UpperBound of f .: X let s be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not s in f .: X or s <= r ) assume s in f .: X ; ::_thesis: s <= r then ex x being set st ( x in X & x in X & s = f . x ) by FUNCT_2:64; hence s <= r by A5, A6; ::_thesis: verum end; given p being real number such that A7: p is UpperBound of f .: X ; :: according to XXREAL_2:def_10 ::_thesis: f is bounded_above take p + 1 ; :: according to SEQ_2:def_1 ::_thesis: for b1 being set holds ( not b1 in dom f or not p + 1 <= f . b1 ) let y be set ; ::_thesis: ( not y in dom f or not p + 1 <= f . y ) assume y in dom f ; ::_thesis: not p + 1 <= f . y then f . y in rng f by FUNCT_1:3; then f . y in f .: X by RELSET_1:22; then p >= f . y by A7, XXREAL_2:def_1; then A8: p + 1 >= (f . y) + 1 by XREAL_1:6; f . y < (f . y) + 1 by XREAL_1:29; hence not p + 1 <= f . y by A8, XXREAL_0:2; ::_thesis: verum end; end; :: deftheorem defines bounded_below MEASURE6:def_10_:_ for X being set for f being Function of X,REAL holds ( f is bounded_below iff f .: X is bounded_below ); :: deftheorem defines bounded_above MEASURE6:def_11_:_ for X being set for f being Function of X,REAL holds ( f is bounded_above iff f .: X is bounded_above ); definition let X be set ; let f be Function of X,REAL; attrf is with_max means :: MEASURE6:def 12 f .: X is with_max ; attrf is with_min means :: MEASURE6:def 13 f .: X is with_min ; end; :: deftheorem defines with_max MEASURE6:def_12_:_ for X being set for f being Function of X,REAL holds ( f is with_max iff f .: X is with_max ); :: deftheorem defines with_min MEASURE6:def_13_:_ for X being set for f being Function of X,REAL holds ( f is with_min iff f .: X is with_min ); theorem Th65: :: MEASURE6:65 for X, A being set for f being Function of X,REAL holds (- f) .: A = -- (f .: A) proof let X, A be set ; ::_thesis: for f being Function of X,REAL holds (- f) .: A = -- (f .: A) let f be Function of X,REAL; ::_thesis: (- f) .: A = -- (f .: A) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(-_f)_.:_A_implies_x_in_--_(f_.:_A)_)_&_(_x_in_--_(f_.:_A)_implies_x_in_(-_f)_.:_A_)_) let x be set ; ::_thesis: ( ( x in (- f) .: A implies x in -- (f .: A) ) & ( x in -- (f .: A) implies x in (- f) .: A ) ) hereby ::_thesis: ( x in -- (f .: A) implies x in (- f) .: A ) assume x in (- f) .: A ; ::_thesis: x in -- (f .: A) then consider x1 being set such that A1: ( x1 in X & x1 in A & x = (- f) . x1 ) by FUNCT_2:64; ( x = - (f . x1) & f . x1 in f .: A ) by A1, FUNCT_2:35, VALUED_1:8; hence x in -- (f .: A) ; ::_thesis: verum end; assume x in -- (f .: A) ; ::_thesis: x in (- f) .: A then consider r3 being Element of COMPLEX such that A2: x = - r3 and A3: r3 in f .: A ; reconsider r3 = r3 as Real by A3; consider x1 being set such that A4: ( x1 in X & x1 in A ) and A5: r3 = f . x1 by A3, FUNCT_2:64; x = (- f) . x1 by A2, A5, VALUED_1:8; hence x in (- f) .: A by A4, FUNCT_2:35; ::_thesis: verum end; hence (- f) .: A = -- (f .: A) by TARSKI:1; ::_thesis: verum end; Lm9: for X being non empty set for f being Function of X,REAL st f is with_max holds - f is with_min proof let X be non empty set ; ::_thesis: for f being Function of X,REAL st f is with_max holds - f is with_min let f be Function of X,REAL; ::_thesis: ( f is with_max implies - f is with_min ) assume that A1: f .: X is bounded_above and A2: upper_bound (f .: X) in f .: X ; :: according to MEASURE6:def_4,MEASURE6:def_12 ::_thesis: - f is with_min A3: -- (f .: X) = (- f) .: X by Th65; hence (- f) .: X is bounded_below by A1, Lm2; :: according to MEASURE6:def_5,MEASURE6:def_13 ::_thesis: lower_bound ((- f) .: X) in (- f) .: X then A4: lower_bound ((- f) .: X) = - (upper_bound (-- (-- (f .: X)))) by A3, Th43 .= - (upper_bound (f .: X)) ; - (upper_bound (f .: X)) in -- (f .: X) by A2, MEMBER_1:11; hence lower_bound ((- f) .: X) in (- f) .: X by A4, Th65; ::_thesis: verum end; Lm10: for X being non empty set for f being Function of X,REAL st f is with_min holds - f is with_max proof let X be non empty set ; ::_thesis: for f being Function of X,REAL st f is with_min holds - f is with_max let f be Function of X,REAL; ::_thesis: ( f is with_min implies - f is with_max ) assume that A1: f .: X is bounded_below and A2: lower_bound (f .: X) in f .: X ; :: according to MEASURE6:def_5,MEASURE6:def_13 ::_thesis: - f is with_max A3: -- (f .: X) = (- f) .: X by Th65; hence (- f) .: X is bounded_above by A1, Lm3; :: according to MEASURE6:def_4,MEASURE6:def_12 ::_thesis: upper_bound ((- f) .: X) in (- f) .: X then A4: upper_bound ((- f) .: X) = - (lower_bound (-- (-- (f .: X)))) by A3, Th44 .= - (lower_bound (f .: X)) ; - (lower_bound (f .: X)) in -- (f .: X) by A2, MEMBER_1:11; hence upper_bound ((- f) .: X) in (- f) .: X by A4, Th65; ::_thesis: verum end; theorem Th66: :: MEASURE6:66 for X being non empty set for f being Function of X,REAL holds ( f is with_min iff - f is with_max ) proof let X be non empty set ; ::_thesis: for f being Function of X,REAL holds ( f is with_min iff - f is with_max ) let f be Function of X,REAL; ::_thesis: ( f is with_min iff - f is with_max ) - (- f) = f ; hence ( f is with_min iff - f is with_max ) by Lm9, Lm10; ::_thesis: verum end; theorem :: MEASURE6:67 for X being non empty set for f being Function of X,REAL holds ( f is with_max iff - f is with_min ) proof let X be non empty set ; ::_thesis: for f being Function of X,REAL holds ( f is with_max iff - f is with_min ) let f be Function of X,REAL; ::_thesis: ( f is with_max iff - f is with_min ) - (- f) = f ; hence ( f is with_max iff - f is with_min ) by Th66; ::_thesis: verum end; theorem :: MEASURE6:68 for X being set for A being Subset of REAL for f being Function of X,REAL holds (- f) " A = f " (-- A) proof let X be set ; ::_thesis: for A being Subset of REAL for f being Function of X,REAL holds (- f) " A = f " (-- A) let A be Subset of REAL; ::_thesis: for f being Function of X,REAL holds (- f) " A = f " (-- A) let f be Function of X,REAL; ::_thesis: (- f) " A = f " (-- A) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(-_f)_"_A_implies_x_in_f_"_(--_A)_)_&_(_x_in_f_"_(--_A)_implies_x_in_(-_f)_"_A_)_) let x be set ; ::_thesis: ( ( x in (- f) " A implies x in f " (-- A) ) & ( x in f " (-- A) implies x in (- f) " A ) ) hereby ::_thesis: ( x in f " (-- A) implies x in (- f) " A ) A1: (- f) . x = - (f . x) by VALUED_1:8; assume A2: x in (- f) " A ; ::_thesis: x in f " (-- A) then (- f) . x in A by FUNCT_2:38; then - (- (f . x)) in -- A by A1; hence x in f " (-- A) by A2, FUNCT_2:38; ::_thesis: verum end; A3: (- f) . x = - (f . x) by VALUED_1:8; assume A4: x in f " (-- A) ; ::_thesis: x in (- f) " A then f . x in -- A by FUNCT_2:38; then (- f) . x in -- (-- A) by A3; hence x in (- f) " A by A4, FUNCT_2:38; ::_thesis: verum end; hence (- f) " A = f " (-- A) by TARSKI:1; ::_thesis: verum end; theorem :: MEASURE6:69 for X, A being set for f being Function of X,REAL for s being Real holds (s + f) .: A = s ++ (f .: A) proof let X, A be set ; ::_thesis: for f being Function of X,REAL for s being Real holds (s + f) .: A = s ++ (f .: A) let f be Function of X,REAL; ::_thesis: for s being Real holds (s + f) .: A = s ++ (f .: A) let s be Real; ::_thesis: (s + f) .: A = s ++ (f .: A) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(s_+_f)_.:_A_implies_x_in_s_++_(f_.:_A)_)_&_(_x_in_s_++_(f_.:_A)_implies_x_in_(s_+_f)_.:_A_)_) let x be set ; ::_thesis: ( ( x in (s + f) .: A implies x in s ++ (f .: A) ) & ( x in s ++ (f .: A) implies x in (s + f) .: A ) ) hereby ::_thesis: ( x in s ++ (f .: A) implies x in (s + f) .: A ) assume x in (s + f) .: A ; ::_thesis: x in s ++ (f .: A) then consider x1 being set such that A1: ( x1 in X & x1 in A & x = (s + f) . x1 ) by FUNCT_2:64; ( x = s + (f . x1) & f . x1 in f .: A ) by A1, FUNCT_2:35, VALUED_1:2; then x in { (s + q3) where q3 is Real : q3 in f .: A } ; hence x in s ++ (f .: A) by Lm5; ::_thesis: verum end; assume x in s ++ (f .: A) ; ::_thesis: x in (s + f) .: A then x in { (s + q3) where q3 is Real : q3 in f .: A } by Lm5; then consider r3 being Real such that A2: x = s + r3 and A3: r3 in f .: A ; consider x1 being set such that A4: x1 in X and A5: x1 in A and A6: r3 = f . x1 by A3, FUNCT_2:64; x = (s + f) . x1 by A2, A4, A6, VALUED_1:2; hence x in (s + f) .: A by A4, A5, FUNCT_2:35; ::_thesis: verum end; hence (s + f) .: A = s ++ (f .: A) by TARSKI:1; ::_thesis: verum end; theorem :: MEASURE6:70 for X being set for A being Subset of REAL for f being Function of X,REAL for q3 being Real holds (q3 + f) " A = f " ((- q3) ++ A) proof let X be set ; ::_thesis: for A being Subset of REAL for f being Function of X,REAL for q3 being Real holds (q3 + f) " A = f " ((- q3) ++ A) let A be Subset of REAL; ::_thesis: for f being Function of X,REAL for q3 being Real holds (q3 + f) " A = f " ((- q3) ++ A) let f be Function of X,REAL; ::_thesis: for q3 being Real holds (q3 + f) " A = f " ((- q3) ++ A) let q3 be Real; ::_thesis: (q3 + f) " A = f " ((- q3) ++ A) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(q3_+_f)_"_A_implies_x_in_f_"_((-_q3)_++_A)_)_&_(_x_in_f_"_((-_q3)_++_A)_implies_x_in_(q3_+_f)_"_A_)_) let x be set ; ::_thesis: ( ( x in (q3 + f) " A implies x in f " ((- q3) ++ A) ) & ( x in f " ((- q3) ++ A) implies x in (q3 + f) " A ) ) hereby ::_thesis: ( x in f " ((- q3) ++ A) implies x in (q3 + f) " A ) assume A1: x in (q3 + f) " A ; ::_thesis: x in f " ((- q3) ++ A) then ( (q3 + f) . x in A & (q3 + f) . x = q3 + (f . x) ) by FUNCT_2:38, VALUED_1:2; then (- q3) + (q3 + (f . x)) in { ((- q3) + p3) where p3 is Real : p3 in A } ; then (- q3) + (q3 + (f . x)) in (- q3) ++ A by Lm5; hence x in f " ((- q3) ++ A) by A1, FUNCT_2:38; ::_thesis: verum end; assume A2: x in f " ((- q3) ++ A) ; ::_thesis: x in (q3 + f) " A then ( f . x in (- q3) ++ A & (q3 + f) . x = q3 + (f . x) ) by FUNCT_2:38, VALUED_1:2; then (q3 + f) . x in { (q3 + p3) where p3 is Real : p3 in (- q3) ++ A } ; then (q3 + f) . x in q3 ++ ((- q3) ++ A) by Lm5; then (q3 + f) . x in (q3 + (- q3)) ++ A by MEMBER_1:147; then (q3 + f) . x in A by MEMBER_1:146; hence x in (q3 + f) " A by A2, FUNCT_2:38; ::_thesis: verum end; hence (q3 + f) " A = f " ((- q3) ++ A) by TARSKI:1; ::_thesis: verum end; notation let f be real-valued Function; synonym Inv f for f " ; end; definition let C be set ; let D be real-membered set ; let f be PartFunc of C,D; :: original: Inv redefine func Inv f -> PartFunc of C,REAL; coherence Inv f is PartFunc of C,REAL proof f " is PartFunc of C,REAL ; hence Inv f is PartFunc of C,REAL ; ::_thesis: verum end; end; theorem :: MEASURE6:71 for X being set for A being without_zero Subset of REAL for f being Function of X,REAL holds (Inv f) " A = f " (Inv A) proof let X be set ; ::_thesis: for A being without_zero Subset of REAL for f being Function of X,REAL holds (Inv f) " A = f " (Inv A) let A be without_zero Subset of REAL; ::_thesis: for f being Function of X,REAL holds (Inv f) " A = f " (Inv A) let f be Function of X,REAL; ::_thesis: (Inv f) " A = f " (Inv A) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(Inv_f)_"_A_implies_x_in_f_"_(Inv_A)_)_&_(_x_in_f_"_(Inv_A)_implies_x_in_(Inv_f)_"_A_)_) let x be set ; ::_thesis: ( ( x in (Inv f) " A implies x in f " (Inv A) ) & ( x in f " (Inv A) implies x in (Inv f) " A ) ) hereby ::_thesis: ( x in f " (Inv A) implies x in (Inv f) " A ) A1: (Inv f) . x = (f . x) " by VALUED_1:10; assume A2: x in (Inv f) " A ; ::_thesis: x in f " (Inv A) then (Inv f) . x in A by FUNCT_2:38; then 1 / ((f . x) ") in Inv A by A1; hence x in f " (Inv A) by A2, FUNCT_2:38; ::_thesis: verum end; A3: ( (f . x) " = 1 / (f . x) & (Inv f) . x = (f . x) " ) by VALUED_1:10; assume A4: x in f " (Inv A) ; ::_thesis: x in (Inv f) " A then f . x in Inv A by FUNCT_2:38; then (Inv f) . x in Inv (Inv A) by A3; hence x in (Inv f) " A by A4, FUNCT_2:38; ::_thesis: verum end; hence (Inv f) " A = f " (Inv A) by TARSKI:1; ::_thesis: verum end; theorem :: MEASURE6:72 for A being Subset of REAL for x being Real st x in -- A holds ex a being Real st ( a in A & x = - a ) proof let A be Subset of REAL; ::_thesis: for x being Real st x in -- A holds ex a being Real st ( a in A & x = - a ) let x be Real; ::_thesis: ( x in -- A implies ex a being Real st ( a in A & x = - a ) ) assume x in -- A ; ::_thesis: ex a being Real st ( a in A & x = - a ) then x in { (- a) where a is Element of COMPLEX : a in A } ; then consider a being Element of COMPLEX such that A1: ( x = - a & a in A ) ; reconsider a = a as Real by A1; take a ; ::_thesis: ( a in A & x = - a ) thus ( a in A & x = - a ) by A1; ::_thesis: verum end;