:: Some Properties of the Intervals :: by J\'ozef Bia\las :: :: Received February 5, 1994 :: Copyright (c) 1994-2017 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FUNCT_1, ZFMISC_1, RELAT_1, SUPINF_2, XXREAL_0, CARD_1, SUPINF_1, SUBSET_1, NAT_1, ARYTM_3, ORDINAL1, XXREAL_2, ORDINAL2, XBOOLE_0, REAL_1, ARYTM_1, MEASURE5, XXREAL_1, MEMBERED, MEMBER_1, TARSKI, XCMPLX_0, FREEALG, QUANTAL1, SETFAM_1, FINSET_1, COMPLEX1, SEQ_1, SEQ_2, VALUED_0, SEQ_4, PSCOMP_1, RCOMP_1, PRALG_1, PRE_TOPC, PARTFUN1, INT_1, ASYMPT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, FINSET_1, NUMBERS, MEMBERED, ABSVALUE, COMPLEX1, VALUED_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, MEMBER_1, FUNCT_3, XXREAL_0, XXREAL_1, XXREAL_2, XXREAL_3, XCMPLX_0, XREAL_0, REAL_1, INT_1, NAT_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4, RCOMP_1, SUPINF_1, SUPINF_2, MEASURE5, VALUED_1; constructors WELLORD2, DOMAIN_1, REAL_1, NAT_1, CARD_1, SUPINF_2, MEASURE5, SUPINF_1, RCOMP_1, RELSET_1, COMPLEX1, SEQ_2, SEQM_3, VALUED_0, VALUED_1, FUNCOP_1, SEQ_4, BINOP_2, LIMFUNC1, MEMBER_1, FUNCT_3, COMSEQ_2, SEQ_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XREAL_0, MEMBERED, XXREAL_1, XXREAL_2, XXREAL_3, VALUED_0, VALUED_1, NAT_1, INT_1, FINSET_1, MEMBER_1, RCOMP_1, SEQ_2, SEQ_4, FCONT_3, FUNCT_2, MEASURE5, RELSET_1, XCMPLX_0, SEQ_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; definitions SEQ_2, TARSKI, XBOOLE_0, XXREAL_2, FINSET_1, RCOMP_1; equalities SUPINF_2, SUBSET_1, XXREAL_3, RCOMP_1, VALUED_1, XCMPLX_0, MEMBER_1; expansions SEQ_2, TARSKI, XBOOLE_0, XXREAL_2, RCOMP_1; theorems SUPINF_2, FUNCT_1, MEASURE5, FUNCT_2, NAT_1, CARD_4, WELLORD2, XREAL_0, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, MEMBERED, XXREAL_1, XXREAL_2, XXREAL_3, SETFAM_1, TARSKI, COMPLEX1, ABSVALUE, VALUED_1, SEQ_1, XCMPLX_1, SEQ_4, SEQ_2, RCOMP_1, RELSET_1, INT_1, SUBSET_1, MEMBER_1; schemes RECDEF_1, NAT_1, FINSET_1, FUNCT_2, BINOP_2, DOMAIN_1, FUNCT_1; begin :: Some theorems about R_eal numbers theorem ex F being sequence of [: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 sequence of [:NAT,NAT:] by A2,FUNCT_2:1; hence thesis by A1,A2; end; theorem for F being sequence of ExtREAL st F is nonnegative holds 0. <= SUM(F) proof let F be sequence of ExtREAL; assume F is nonnegative; then 0. <= Ser(F).0 by SUPINF_2:40; hence thesis by FUNCT_2:4,XXREAL_2:4; end; theorem for F being sequence of ExtREAL, 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 sequence of ExtREAL; let x be R_eal; assume that A1: ex n being Element of NAT st x <= F.n and A2: F is nonnegative; 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; per cases by NAT_1:6; suppose n = 0; then Ser(F).n = F.n by SUPINF_2:def 11; hence thesis by A3,A4,XXREAL_0:2; end; suppose ex k being Nat st n = k + 1; then consider k being Nat such that A5: n = k + 1; reconsider 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:def 11; then 0. + x <= Ser(F).n by A3,A5,A6,XXREAL_3:36; then x <= Ser(F).n by XXREAL_3:4; hence thesis by A4,XXREAL_0:2; end; end; definition ::\$CD end; theorem for eps being ExtReal st 0. < eps ex F being sequence of ExtREAL st (for n being Nat holds 0. < F.n) & SUM(F) < eps proof defpred P[set,set,set] means for a,b being R_eal,s being Nat holds (s = \$1 & a = \$2 & b = \$3 implies b = a/2); let eps be ExtReal; assume 0. < eps; then consider x0 being Real such that A1: 0. < x0 and A2: x0 < eps by XXREAL_3:3; consider x being Real such that A3: 0. < x and A4: x + (x qua ExtReal) < x0 by A1,XXREAL_3:50; reconsider x as Element of ExtREAL by XXREAL_0:def 1; A5: for n being Nat for x being Element of ExtREAL ex y being Element of ExtREAL st P[n,x,y] proof let n be Nat; let x be Element of ExtREAL; reconsider m = x/2 as Element of ExtREAL by XXREAL_0:def 1; take m; thus thesis; end; consider F being sequence of ExtREAL such that A6: F.0 = x & for n being Nat holds P[n,F.n,F.(n+1)] from RECDEF_1:sch 2(A5); take F; defpred P[Nat] means 0. < F.\$1; A7: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume A8: 0. < F.k; F.(k+1) = (F.k)/2 by A6; hence thesis by A8; end; A9: P[0] by A3,A6; thus A10: for n being Nat holds P[n] from NAT_1:sch 2(A9,A7); then for n being Element of NAT holds 0. <= F.n; then A11: F is nonnegative by SUPINF_2:39; for s being ExtReal holds s in rng Ser(F) implies s <= x0 proof defpred P[Nat] means Ser(F).\$1 + F.\$1 < x0; let s be ExtReal; assume s in rng Ser(F); then consider n being object such that A12: n in dom Ser(F) and A13: s = Ser(F).n by FUNCT_1:def 3; reconsider n as Element of NAT by A12; A14: for l being Nat st P[l] holds P[l+1] proof let l be Nat; 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:def 11, XXREAL_3:44; assume Ser(F).l + F.l < x0; hence thesis by A16,XXREAL_0:2; end; A17: P[0] by A4,A6,SUPINF_2:def 11; for k being Nat holds P[k] from NAT_1:sch 2(A17,A14); then A18: Ser(F).n + F.n < x0; 0. <= Ser(F).n & 0. <= F.n by A10,A11,SUPINF_2:40; hence thesis by A13,A18,XXREAL_3:48; 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; per cases by A19,XXREAL_0:1; suppose SUM(F) < x0; hence thesis by A2,XXREAL_0:2; end; suppose SUM(F) = x0; hence thesis by A2; end; end; theorem for eps being ExtReal, X being non empty Subset of ExtREAL st 0. < eps & inf X is Real holds ex x being ExtReal st x in X & x < inf X + eps proof let eps be ExtReal; let X be non empty Subset of ExtREAL; assume that A1: 0. < eps and A2: inf X is Real; A3: inf X in REAL by A2,XREAL_0:def 1; assume not ex x being ExtReal st x in X & x < inf X + eps; then inf X + eps is LowerBound of X by XXREAL_2:def 2; then A4: inf X + eps <= inf X by XXREAL_2:def 4; per cases by XXREAL_0:4; suppose eps < +infty; then reconsider a = inf X, b = eps as Element of REAL by A1,A3,XXREAL_0:48; inf X + eps = a + b by SUPINF_2:1; then b <= a - a by A4,XREAL_1:19; hence thesis by A1; end; suppose eps = +infty; then inf X + eps = +infty by A3,XXREAL_3:def 2; hence thesis by A3,A4,XXREAL_0:4; end; end; theorem for eps being ExtReal, X being non empty Subset of ExtREAL st 0. < eps & sup X is Real holds ex x being ExtReal st x in X & sup X - eps < x proof let eps be ExtReal; let X be non empty Subset of ExtREAL; assume that A1: 0. < eps and A2: sup X is Real; A3: sup X in REAL by A2,XREAL_0:def 1; assume not ex x being ExtReal st x in X & sup X - eps < x; then sup X - eps is UpperBound of X by XXREAL_2:def 1; then A4: sup X <= sup X - eps by XXREAL_2:def 3; per cases by XXREAL_0:4; suppose eps < +infty; then reconsider a = sup X, b = eps as Element of REAL by A1,A3,XXREAL_0:48; a <= a - b by A4,SUPINF_2:3; hence thesis by A1,XREAL_1:44; end; suppose eps = +infty; then sup X - eps = -infty by A3,XXREAL_3:13; hence thesis by A3,A4,XXREAL_0:6; end; end; theorem for F being sequence of ExtREAL st F is nonnegative & SUM(F) < +infty holds for n being Element of NAT holds F.n in REAL proof let F be sequence of ExtREAL; assume that A1: F is nonnegative and A2: SUM(F) < +infty; let n be Element of NAT; defpred P[Nat] means F.\$1 <= Ser(F).\$1; A3: for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume F.k <= Ser(F).k; reconsider x = Ser(F).k as R_eal; x + F.(k+1) = Ser(F).(k+1) by SUPINF_2:def 11; hence thesis by A1,SUPINF_2:40,XXREAL_3:39; end; A4: P[0] by SUPINF_2:def 11; for n being Nat holds P[n] from NAT_1:sch 2(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; A7: 0 in REAL by XREAL_0:def 1; 0. = 0 & 0. <= F.n by A1,SUPINF_2:39; hence thesis by A6,XXREAL_0:46,A7; end; :: PROPERTIES OF THE INTERVALS registration cluster non empty interval for Subset of REAL; existence proof take [#]REAL; thus thesis; end; end; theorem for A being non empty Interval, a being ExtReal st ex b being ExtReal st a <= b & A = ].a,b.[ holds a = inf A by XXREAL_1:28,XXREAL_2:28; theorem for A being non empty Interval, a being ExtReal st ex b being ExtReal st a <= b & A = ].a,b.] holds a = inf A by XXREAL_1:26,XXREAL_2:27; theorem for A being non empty Interval, a being ExtReal st ex b being ExtReal st a <= b & A = [.a,b.] holds a = inf A by XXREAL_2:25; theorem Th11: for A being non empty Interval, a being ExtReal st ex b being ExtReal st a <= b & A = [.a,b.[ holds a = inf A proof let A be non empty Interval, IT be ExtReal; given b being ExtReal such that A1: IT <= b and A2: A = [.IT,b.[; IT <> b by A2; then IT < b by A1,XXREAL_0:1; hence thesis by A2,XXREAL_2:26; end; theorem for A being non empty Interval, b being ExtReal st ex a being ExtReal st a <= b & A = ].a,b.[ holds b = sup A by XXREAL_1:28,XXREAL_2:32; theorem Th13: for A being non empty Interval, b being ExtReal st ex a being ExtReal st a <= b & A = ].a,b.] holds b = sup A proof let A be non empty Interval, IT be ExtReal; given a being ExtReal such that A1: a <= IT and A2: A = ].a,IT.]; a <> IT by A2; then a < IT by A1,XXREAL_0:1; hence thesis by A2,XXREAL_2:30; end; theorem for A being non empty Interval, b being ExtReal st ex a being ExtReal st a <= b & A = [.a,b.] holds b = sup A by XXREAL_2:29; theorem Th15: for A being non empty Interval, b being ExtReal st ex a being ExtReal st a <= b & A = [.a,b.[ holds b = sup A proof let A be non empty Interval, IT be ExtReal; given a being ExtReal such that A1: a <= IT and A2: A = [.a,IT.[; a <> IT by A2; then a < IT by A1,XXREAL_0:1; hence thesis by A2,XXREAL_2:31; end; theorem for A being non empty Interval st A is open_interval holds A = ].inf A,sup A.[ proof let A be non empty Interval; assume A is open_interval; 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 thesis by A1,XXREAL_1:28,XXREAL_2:28; end; theorem for A being non empty Interval st A is closed_interval holds A = [.inf A,sup A.] proof let A be non empty Interval; assume A is closed_interval; then consider a,b being Real such that A1: A = [.a,b.] by MEASURE5:def 3; A2: a <= b by A1,XXREAL_1:29; reconsider b as R_eal by XXREAL_0:def 1; sup A = b by A1,A2,XXREAL_2:29; hence thesis by A1,A2,XXREAL_2:25; end; theorem 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; assume A is right_open_interval; then consider a being Real,b being R_eal such that A1: A = [.a,b.[ by MEASURE5:def 4; reconsider 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 thesis by A1,A2,Th11; end; theorem 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; assume A is left_open_interval; then consider a being R_eal,b being Real such that A1: A = ].a,b.] by MEASURE5:def 5; A2: a <= b by A1,XXREAL_1:26; reconsider b as R_eal by XXREAL_0:def 1; sup A = b by A2,A1,Th13; hence thesis by A1,XXREAL_1:26,XXREAL_2:27; end; theorem for A,B being non empty Interval, a,b being Real st a in A & b in B & sup A <= inf B holds a <= b proof let A,B be non empty Interval, a,b be Real; assume that A1: a in A and A2: b in B; A3: inf B <= b by A2,XXREAL_2:3; assume A4: sup A <= inf B; a <= sup A by A1,XXREAL_2:4; then a <= inf B by A4,XXREAL_0:2; hence thesis by A3,XXREAL_0:2; end; theorem for A,B be real-membered set holds 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; let y be Real; hereby assume y in B++A; then consider x,w being Complex such that A1: y = x+w & x in B & w in A; reconsider x,w as Real by A1; take x,w; thus x in B & w in A & y = x + w by A1; end; given w,z being Real such that A2: w in B & z in A & y = w + z; thus thesis by A2; end; theorem for A,B being non empty Interval holds sup A = inf B & (sup A in A or inf B in B) implies A \/ B is Interval by XXREAL_2:def 5,XXREAL_2:def 6,XXREAL_2:90,XXREAL_2:91; definition let A be real-membered set; let x be Real; redefine func x ++ A -> Subset of REAL; coherence by MEMBERED:3; end; Lm1: for A be real-membered set, x be Real holds 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, x be Real; let y be Real; hereby assume y in x++A; then consider w being Complex such that A1: y = x+w & w in A by MEMBER_1:143; reconsider w as Real by A1; take w; thus w in A & y = x + w by A1; end; given z being Real such that A2: z in A & y = x + z; thus thesis by A2,MEMBER_1:141; end; theorem Th23: for A being Subset of REAL, x being Real holds -x ++ (x ++ A) = A proof let A be Subset of REAL, x be Real; thus -x ++ (x ++ A) c= A proof let y be object; assume A1: y in -x ++ (x ++ A); then reconsider 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 thesis by A3; end; let y be object; assume A4: y in A; then reconsider y as Real; reconsider t = y - -x as Real; reconsider z = t -x as Real; A5: z = -x + t; t in x ++ A by A4,Lm1; hence thesis by A5,Lm1; end; theorem for x being Real, A being Subset of REAL st A = REAL holds x ++ A = A proof let x be Real, A be Subset of REAL; assume A1: A = REAL; A c= x ++ A proof let y be object; assume y in A; then reconsider y as Real; reconsider z = y - x as Element of REAL by XREAL_0:def 1; y = x + z; hence thesis by A1,Lm1; end; hence thesis by A1; end; theorem for x being Real holds x ++ {} = {}; theorem Th26: for A being Interval, x being Real holds A is open_interval iff x ++ A is open_interval proof let A be Interval, x be Real; reconsider y = -x as Element of REAL by XREAL_0:def 1; A1: for B being Interval, y being Real st B is open_interval holds y ++ B is open_interval proof let B be Interval; let y be Real; reconsider y as Element of REAL by XREAL_0:def 1; reconsider z = y as R_eal by XXREAL_0:def 1; assume 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.[ proof let c be object; assume A3: c in y ++ B; then reconsider c as Element of 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 thesis by A6,A7; end; let c be object; assume A8: c in ].s,t.[; then reconsider c as Element of 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 thesis by A9,Lm1; end; hence thesis by MEASURE5:def 2; end; hence A is open_interval implies x ++ A is open_interval; assume A12: x ++ A is open_interval; then reconsider B = x ++ A as Interval; y ++ B = A by Th23; hence thesis by A1,A12; end; theorem Th27: for A being Interval, x being Real holds A is closed_interval iff x ++ A is closed_interval proof let A be Interval; let x be Real; A1: for B being Interval, y being Real st B is closed_interval holds y ++ B is closed_interval proof let B be Interval; let y be Real; reconsider y as Real; reconsider z = y as R_eal by XXREAL_0:def 1; assume B is closed_interval; then consider a1,b1 being Real 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.] proof let c be object; assume A3: c in y ++ B; then reconsider 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 thesis by A6,A7,XXREAL_1:1; end; reconsider a,b as R_eal; let c be object; assume A8: c in [.s,t.]; then reconsider c as Real; 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 thesis by A9,Lm1; end; hence thesis by MEASURE5:def 3; end; x ++ A is closed_interval implies A is closed_interval proof reconsider y = -x as Real; assume A12: x ++ A is closed_interval; then reconsider B = x ++ A as Interval; y ++ B = A by Th23; hence thesis by A1,A12; end; hence thesis by A1; end; theorem Th28: for A being Interval, x being Real holds A is right_open_interval iff x ++ A is right_open_interval proof let A be Interval; let x be Real; A1: for B being Interval, y being Real st B is right_open_interval holds y ++ B is right_open_interval proof let B be Interval; let y be Real; reconsider y as Element of REAL by XREAL_0:def 1; reconsider z = y as R_eal by XXREAL_0:def 1; assume B is right_open_interval; then consider a1 being Real,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.[ proof let c be object; assume A3: c in y ++ B; then reconsider c as Element of 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 thesis by A6,A7,XXREAL_1:3; end; let c be object; assume A8: c in [.s,t.[; then reconsider c as Element of 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 thesis by A9,Lm1; end; hence thesis by MEASURE5:def 4; end; x ++ A is right_open_interval implies A is right_open_interval proof reconsider y = -x as Real; assume A12: x ++ A is right_open_interval; then reconsider B = x ++ A as Interval; y ++ B = A by Th23; hence thesis by A1,A12; end; hence thesis by A1; end; theorem Th29: for A being Interval, x being Real holds A is left_open_interval iff x ++ A is left_open_interval proof let A be Interval, x be Real; A1: for B being Interval, y being Real st B is left_open_interval holds y ++ B is left_open_interval proof let B be Interval, y be Real; reconsider y as Element of REAL by XREAL_0:def 1; reconsider z = y as R_eal by XXREAL_0:def 1; assume B is left_open_interval; then consider a being R_eal,b1 being Real 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, t = z + b; y ++ B = ].s,t.] proof thus y ++ B c= ].s,t.] proof let c be object; assume A3: c in y ++ B; then reconsider c as Element of 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: s < z + d1 by XXREAL_3:43; d1 <= b by A2,A4,XXREAL_1:2; then A7: z + d1 <= t by XXREAL_3:36; z + d1 = c by A5,SUPINF_2:1; hence thesis by A6,A7,XXREAL_1:2; end; let c be object; assume A8: c in ].s,t.]; then reconsider c as Real; 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 thesis by A9,Lm1; end; hence thesis by MEASURE5:def 5; end; x ++ A is left_open_interval implies A is left_open_interval proof reconsider y = -x as Real; assume A12: x ++ A is left_open_interval; then reconsider B = x ++ A as Interval; y ++ B = A by Th23; hence thesis by A1,A12; end; hence thesis by A1; end; theorem for A being Interval, x being Real holds x ++ A is Interval proof let A be Interval, x be Real; per cases by MEASURE5:1; suppose A is open_interval; then x ++ A is open_interval by Th26; hence thesis; end; suppose A is closed_interval; then x ++ A is closed_interval by Th27; hence thesis; end; suppose A is right_open_interval; then x ++ A is right_open_interval by Th28; hence thesis; end; suppose A is left_open_interval; then x ++ A is left_open_interval by Th29; hence thesis; end; end; theorem Th31: for A being real-membered set, x being Real, y being R_eal st x = y holds sup(x ++ A) = y + sup A proof let A be real-membered set, x being Real, y being R_eal such that A1: x = y; A2: for z being UpperBound of x ++ A holds y + sup A <= z proof let z be UpperBound of x ++ A; reconsider zz = z as R_eal by XXREAL_0:def 1; zz - y is UpperBound of A proof let u be ExtReal; reconsider uu = u as R_eal by XXREAL_0:def 1; assume A3: u in A; then reconsider u1 = u as Real; 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 thesis by A1,XXREAL_3:45; end; then sup A <= zz - y by XXREAL_2:def 3; hence thesis by A1,XXREAL_3:45; end; y + sup A is UpperBound of x ++ A proof let z be ExtReal; assume z in x ++ 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 st y = a & b = c & y + b = a + c by A1, XXREAL_3:def 2; hence thesis by A1,A5,A6,XXREAL_3:36; end; hence thesis by A2,XXREAL_2:def 3; end; theorem Th32: for A being real-membered set, x being Real, y being R_eal st x = y holds inf(x ++ A) = y + inf A proof let A be real-membered set, x being Real, y being R_eal such that A1: x = y; A2: for z being LowerBound of x ++ A holds z <= y + inf A proof let z be LowerBound of x ++ A; reconsider zz = z as R_eal by XXREAL_0:def 1; zz - y is LowerBound of A proof let u be ExtReal; reconsider uu = u as R_eal by XXREAL_0:def 1; assume A3: u in A; then reconsider u1 = u as Real; 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 thesis by A1,XXREAL_3:42; end; then zz - y <= inf A by XXREAL_2:def 4; hence thesis by A1,XXREAL_3:41; end; y + inf A is LowerBound of x ++ A proof let z be ExtReal; assume z in x ++ 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: inf A <= a by A4,XXREAL_2:3; ex a,c being Complex st y = a & b = c & y + b = a + c by A1, XXREAL_3:def 2; hence thesis by A1,A5,A6,XXREAL_3:36; end; hence thesis by A2,XXREAL_2:def 4; end; theorem for A being Interval, x being Real holds diameter(A) = diameter(x ++ A) proof let A be Interval, x be Real; per cases; suppose A is empty; hence thesis; end; suppose A1: A is non empty; then consider y being Real such that A2: y in A; reconsider y as Real; 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; end; end; begin :: from PSCOMP_1, 2010.02.26, A.T. notation let X be set; synonym X is without_zero for X is with_non-empty_elements; antonym X is with_zero for X is with_non-empty_elements; end; definition let X be set; redefine attr X is without_zero means :Def1: not 0 in X; compatibility by SETFAM_1:def 8; end; registration cluster REAL -> with_zero; coherence by XREAL_0:def 1; cluster NAT -> with_zero; coherence; end; registration cluster non empty without_zero for set; existence proof set s = {1}; take s; thus s is non empty; thus thesis; end; cluster non empty with_zero for set; existence by Def1; end; registration cluster non empty without_zero for Subset of REAL; existence proof set s = {1 qua Real}; take s; thus s is non empty; thus thesis; end; cluster non empty with_zero for Subset of REAL; existence proof take [#]REAL; thus thesis; end; end; theorem Th34: for F being set st F is non empty with_non-empty_elements c=-linear holds F is centered proof defpred P[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; assume that A1: F is non empty and A2: F is with_non-empty_elements and A3: F is c=-linear; thus F <> {} by A1; let G be set; assume that A4: G <> {} and A5: G c= F and A6: G is finite; A7: now let x, B be set; assume that A8: x in G and A9: B c= G and A10: P[B]; thus P[B \/ {x}] proof assume B \/ {x} <> {}; per cases; suppose A11: B is empty; take x9 = x; thus x9 in B \/ {x} by A11,TARSKI:def 1; let y be set; thus thesis by A11,TARSKI:def 1; end; suppose B is non empty; 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 proof z in G by A9,A12; then A14: x, z are_c=-comparable by A3,A5,A8,ORDINAL1:def 8; per cases by A14; suppose A15: x c= z; take x9 = x; x9 in {x} by TARSKI:def 1; hence x9 in B \/ {x} by XBOOLE_0:def 3; let y be set; assume A16: y in B \/ {x}; per cases by A16,XBOOLE_0:def 3; suppose y in B; then z c= y by A13; hence thesis by A15; end; suppose y in {x}; hence thesis by TARSKI:def 1; end; end; suppose A17: z c= x; take x9 = z; thus x9 in B \/ {x} by A12,XBOOLE_0:def 3; let y be set; assume A18: y in B \/ {x}; per cases by A18,XBOOLE_0:def 3; suppose y in B; hence thesis by A13; end; suppose y in {x}; hence thesis by A17,TARSKI:def 1; end; end; end; end; end; end; A19: P[{}]; P[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 object such that A22: xe in x by A2,A5,A20,XBOOLE_0:def 1; now let y be set; assume y in G; then x c= y by A21; hence xe in y by A22; end; hence thesis by A4,SETFAM_1:def 1; end; registration let F be set; cluster non empty with_non-empty_elements c=-linear -> centered for Subset-Family of F; coherence by Th34; end; registration ::: FUNCT_2 let X, Y be non empty set, f be Function of X, Y; cluster f.:X -> non empty; coherence proof set x = the Element of X; A1: dom f = X by FUNCT_2:def 1; thus thesis by A1; end; end; definition ::: FUNCT_3 let X, Y be set, f be Function of X, Y; func "f -> Function of bool Y, bool X means :Def2: for y being Subset of Y holds it.y = f"y; existence proof deffunc F(Subset of Y) = f"\$1; thus ex T be Function of bool Y, bool X st for y be Subset of Y holds T.y = F(y) from FUNCT_2:sch 4; end; uniqueness proof deffunc F(Subset of Y) = f"\$1; thus for T1,T2 be Function of bool Y, bool X st (for y being Subset of Y holds T1.y = F(y)) & (for y being Subset of Y holds T2.y = F(y)) holds T1 = T2 from BINOP_2:sch 1; end; end; theorem for X, Y, x being set, S being Subset-Family of Y, 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, S be Subset-Family of Y, f be Function of X, Y; assume A1: x in meet (("f).:S); A2: now let SS be set; assume A3: SS in S; 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,Def2; hence f.x in SS by A4,FUNCT_1:def 7; end; ("f).:S is non empty by A1,SETFAM_1:def 1; then S is non empty; hence thesis by A2,SETFAM_1:def 1; end; reserve r, s, t for Real; theorem Th36: ::: SQUARE_1 or ABSVALUE |.r.| + |.s.| = 0 implies r = 0 proof set aa = |.r.|, ab = |.s.|; A1: 0 <= aa & 0 <= ab by COMPLEX1:46; assume |.r.|+|.s.| = 0; then aa = 0 by A1; hence thesis by ABSVALUE:2; end; theorem Th37: ::: SQUARE_1 or ABSVALUE r < s & s < t implies |.s.| < |.r.| + |.t.| proof assume that A1: r < s and A2: s < t; per cases; suppose A3: s<0; -s < -r by A1,XREAL_1:24; then A4: -s+0 < -r+|.t.| by COMPLEX1:46,XREAL_1:8; -s = |.s.| by A3,ABSVALUE:def 1; hence thesis by A1,A3,A4,ABSVALUE:def 1; end; suppose A5: 0<=s; A6: s+0 < t+|.r.| by A2,COMPLEX1:46,XREAL_1:8; s = |.s.| by A5,ABSVALUE:def 1; hence thesis by A2,A5,A6,ABSVALUE:def 1; end; end; reserve seq for Real_Sequence, X, Y for Subset of REAL; theorem Th38: ::: SEQ_2 seq is convergent & seq is non-zero & lim seq = 0 implies seq" is non bounded proof assume that A1: seq is convergent and A2: seq is non-zero and A3: lim seq = 0; given r such that A4: for n being Nat holds (seq").n 0 by A2,SEQ_1:5,XCMPLX_1:202; then A9: 0 < At by COMPLEX1:47; s (aa+ab)" by A9,XREAL_1:88; hence |.seq.n.| > rab by A8; end; A10: (seq").1= aa+ab; then A12: aa+ab = 0 by A6; then r = 0 by Th36; hence contradiction by A11,A10,A12,Th36; end; then consider n being Nat such that A13: for m being Nat st n<=m holds |.seq.m-0 .|= s by A1,FUNCT_2:4,XXREAL_2:def 2,A5; hence thesis by A4,XXREAL_0:2; end; given t such that A6: for n being Nat holds seq.ns; thus rng seq is bounded_below proof take s; let r be ExtReal; assume r in rng seq; then ex n being object st n in dom seq & seq.n = r by FUNCT_1:def 3; hence thesis by A7; end; take t; let r be ExtReal; assume r in rng seq; then ex n being object st n in dom seq & seq.n = r by FUNCT_1:def 3; hence thesis by A6; end; notation let X be real-membered set; synonym X is with_max for X is right_end; synonym X is with_min for X is left_end; end; definition let X be real-membered set; redefine attr X is with_max means X is bounded_above & upper_bound X in X; compatibility proof thus X is with_max implies X is bounded_above & upper_bound X in X proof assume A1: X is with_max; hence X is bounded_above; reconsider X as non empty bounded_above real-membered set by A1; upper_bound X in X by A1; hence thesis; end; assume A2: X is bounded_above & upper_bound X in X; then reconsider X as non empty bounded_above real-membered set; upper_bound X in X by A2; hence thesis; end; redefine attr X is with_min means X is bounded_below & lower_bound X in X; compatibility proof thus X is with_min implies X is bounded_below & lower_bound X in X proof assume A3: X is with_min; hence X is bounded_below; reconsider X as non empty bounded_below real-membered set by A3; lower_bound X in X by A3; hence thesis; end; assume A4: X is bounded_below & lower_bound X in X; then reconsider X as non empty bounded_below real-membered set; lower_bound X in X by A4; hence thesis; end; end; registration cluster non empty closed real-bounded for Subset of REAL; existence proof [. 0,0 .] = {0} by XXREAL_1:17; hence thesis; end; end; definition let R be Subset-Family of REAL; attr R is open means for X being Subset of REAL st X in R holds X is open; attr R is closed means for X being Subset of REAL st X in R holds X is closed; end; reserve r3, r1, q3, p3 for Real; definition let X be Subset of REAL; redefine func --X -> Subset of REAL; coherence by MEMBERED:3; end; theorem 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; given s such that A1: s is UpperBound of X; take -s; let t be ExtReal; assume t in --X; then consider r3 be Complex such that A2: t = -r3 and A3: r3 in X; reconsider r3 as Real by A3; r3 <= s by A1,A3,XXREAL_2:def 1; hence thesis by A2,XREAL_1:24; 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; given s such that A1: s is LowerBound of X; take -s; let t be ExtReal; assume t in --X; then consider r3 be Complex such that A2: t = -r3 and A3: r3 in X; reconsider r3 as Real by A3; r3 >= s by A1,A3,XXREAL_2:def 2; hence thesis by A2,XREAL_1:24; end; theorem Th41: X is bounded_above iff --X is bounded_below proof X = -- --X; hence thesis by Lm2,Lm3; end; theorem X is bounded_below iff --X is bounded_above proof X = -- --X; hence thesis by Th41; end; theorem Th43: 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; set r = - upper_bound --X; A1: now let t; assume A2: for s st s in X holds s >= t; now let s; assume s in --X; then -s in -- --X; then -s >= t by A2; then - -s <= -t by XREAL_1:24; hence s <= -t; end; then -r <= -t by SEQ_4:45; hence r >= t by XREAL_1:24; end; assume X is bounded_below; then A3: --X is bounded_above by Lm3; now let s; assume s in X; then -s in --X; then -s <= -r by A3,SEQ_4:def 1; hence s >= r by XREAL_1:24; end; hence thesis by A1,SEQ_4:44; end; theorem Th44: 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; set r = - lower_bound --X; A1: now let s; assume A2: for t st t in X holds t <= s; now let t; assume t in --X; then -t in -- --X; then -t <= s by A2; then - -t >= -s by XREAL_1:24; hence t >= -s; end; then -r >= -s by SEQ_4:43; hence r <= s by XREAL_1:24; end; assume X is bounded_above; then A3: --X is bounded_below by Lm2; now let t; assume t in X; then -t in --X; then -t >= -r by A3,SEQ_4:def 2; hence t <= r by XREAL_1:24; end; hence thesis by A1,SEQ_4:46; end; Lm4: for X being Subset of REAL st X is closed holds --X is closed proof let X be Subset of REAL; assume A1: X is closed; let s1 be Real_Sequence; assume that A2: rng s1 c= --X and A3: s1 is convergent; A4: - lim s1 = lim -s1 by A3,SEQ_2:10; A5: rng -s1 c= X proof let x be object; assume x in rng -s1; then consider n being object such that A6: n in dom -s1 and A7: x = (-s1).n by FUNCT_1:def 3; reconsider 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 thesis; end; -s1 is convergent by A3; then lim -s1 in X by A1,A5; then - -lim s1 in --X by A4; hence thesis; end; theorem X is closed iff --X is closed proof ----X = X; hence thesis by Lm4; end; Lm5: for X be Subset of REAL, p be Real holds p++X = { p+r3 : r3 in X} proof let X be Subset of REAL, p be Real; thus p++X c= { p+r3 : r3 in X } proof let x be object; assume A1: x in p++X; then reconsider x9 = x as Real; ex z being Real st z in X & x9 = p + z by A1,Lm1; hence thesis; end; let x be object; assume x in { p+r3 : r3 in X }; then ex r3 be Real st x = p + r3 & r3 in X; hence thesis by Lm1; end; theorem Th46: r in X iff q3+r in q3++X proof thus r in X implies q3+r in q3++X by MEMBER_1:141; assume q3+r in q3++X; then q3+r in { q3 + r3 : r3 in X } by Lm5; then ex mr being Real st q3+r = q3+mr & mr in X; hence thesis; end; theorem X = 0++X by MEMBER_1:146; theorem q3++(p3++X) = (q3+p3)++X by MEMBER_1:147; Lm6: for X being Subset of REAL, s being Real st X is bounded_above holds s++X is bounded_above proof let X be Subset of REAL, p be Real; given s such that A1: s is UpperBound of X; take p+s; let t be ExtReal; assume t in p++X; then t in { p+r3 : r3 in X} by Lm5; then consider r3 such that A2: t = p+r3 and A3: r3 in X; r3 <= s by A1,A3,XXREAL_2:def 1; hence thesis by A2,XREAL_1:6; end; theorem X is bounded_above iff q3++X is bounded_above proof -q3++(q3++X) = (-q3+q3)++X by MEMBER_1:147 .= X by MEMBER_1:146; hence thesis by Lm6; end; Lm7: for X being Subset of REAL, p being Real st X is bounded_below holds p++X is bounded_below proof let X be Subset of REAL, p be Real; given s such that A1: s is LowerBound of X; take p+s; let t be ExtReal; assume t in p++X; then t in { p+r3 : r3 in X} by Lm5; then consider r3 such that A2: t = p+r3 and A3: r3 in X; r3 >= s by A1,A3,XXREAL_2:def 2; hence thesis by A2,XREAL_1:6; end; theorem X is bounded_below iff q3++X is bounded_below proof -q3++(q3++X) = (-q3+q3)++X by MEMBER_1:147 .= X by MEMBER_1:146; hence thesis by Lm7; end; theorem for X being non empty Subset of REAL st X is bounded_below holds lower_bound (q3++X) = q3+lower_bound X proof let X be non empty Subset of REAL such that A1: X is bounded_below; set i = q3+lower_bound X; A2: now let t; assume A3: for s st s in q3++X holds s >= t; now let s; assume s in X; then t <= q3+s by A3,MEMBER_1:141; hence t-q3 <= s by XREAL_1:20; end; then lower_bound X >= t-q3 by SEQ_4:43; hence t <= i by XREAL_1:20; end; now let s; assume s in q3++X; then s in { q3+r3 : r3 in X} by Lm5; then consider r3 such that A4: q3+r3 = s and A5: r3 in X; r3 >= lower_bound X by A1,A5,SEQ_4:def 2; hence s >= i by A4,XREAL_1:6; end; hence thesis by A2,SEQ_4:44; end; theorem for X being non empty Subset of REAL st X is bounded_above holds upper_bound (q3++X) = q3+upper_bound X proof let X be non empty Subset of REAL such that A1: X is bounded_above; set i = q3+upper_bound X; A2: now let t; assume A3: for s st s in q3++X holds s <= t; now let s; assume s in X; then q3+s <= t by A3,MEMBER_1:141; hence s <= t-q3 by XREAL_1:19; end; then upper_bound X <= t-q3 by SEQ_4:45; hence i <= t by XREAL_1:19; end; now let s; assume s in q3++X; then s in { q3+r3 : r3 in X} by Lm5; then consider r3 such that A4: q3+r3 = s and A5: r3 in X; r3 <= upper_bound X by A1,A5,SEQ_4:def 1; hence s <= i by A4,XREAL_1:6; end; hence thesis by A2,SEQ_4:46; end; Lm8: for X being Subset of REAL st X is closed holds q3++X is closed proof let X be Subset of REAL; assume A1: X is closed; A2: q3++X = { q3+r3 : r3 in X} by Lm5; reconsider qq3=q3 as Element of REAL by XREAL_0:def 1; set s0 = seq_const q3; let s1 be Real_Sequence; assume that A3: (rng s1) c= q3++X and A4: s1 is convergent; lim (s1-s0) = (lim s1) - s0.0 by A4,SEQ_4:42 .= (lim s1) - q3 by SEQ_1:57; then A5: q3+lim(s1-s0) = lim s1; A6: rng (s1-s0) c= X proof let x be object; assume A7: x in rng (s1-s0); then consider n being object 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 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 SEQ_1:57; then x9+q3 in q3++X by A3,A10; hence thesis by Th46; end; s1-s0 is convergent by A4; then lim (s1-s0) in X by A1,A6; hence thesis by A5,A2; end; theorem X is closed iff q3++X is closed proof -q3++(q3++X) = (-q3+q3)++X by MEMBER_1:147 .= X by MEMBER_1:146; hence thesis by Lm8; end; definition let X be Subset of REAL; func Inv X -> Subset of REAL equals { 1/r3 : r3 in X }; coherence proof set Y = { 1/r3 : r3 in X }; Y c= REAL proof let e be object; assume e in Y; then ex r3 st e = 1/r3 & r3 in X; hence thesis by XREAL_0:def 1; end; hence thesis; end; involutiveness proof let Y,X be Subset of REAL; assume A1: Y = { 1/r3 : r3 in X }; thus X c= { 1/r3 : r3 in Y } proof let e be object; assume A2: e in X; then reconsider r=e as Element of REAL; A3: 1/(1/r) = r; 1/r in Y by A1,A2; hence thesis by A3; end; let e be object; assume e in { 1/r3 : r3 in Y }; then consider r3 such that A4: e = 1/r3 and A5: r3 in Y; ex r1 st r3 = 1/r1 & r1 in X by A1,A5; hence thesis by A4; end; end; theorem Th54: for X being Subset of REAL holds r in X iff 1/r in Inv X proof let X be Subset of REAL; thus r in X implies 1/r in Inv X; assume 1/r in Inv X; then ex mr being Real st 1/r = 1/mr & mr in X; hence thesis by XCMPLX_1:59; end; registration let X be non empty Subset of REAL; cluster Inv X -> non empty; coherence proof ex x being Element of REAL st x in X by SUBSET_1:4; hence thesis by Th54; end; end; registration let X be without_zero Subset of REAL; cluster Inv X -> without_zero; coherence proof now assume 0 in Inv X; then ex r3 st 0 = 1/r3 & r3 in X; hence contradiction; end; hence thesis; end; end; theorem for X being without_zero Subset of REAL st X is closed real-bounded holds Inv X is closed proof let X be without_zero Subset of REAL; assume that A1: X is closed and A2: X is real-bounded; let s1 be Real_Sequence; assume that A3: (rng s1) c= Inv X and A4: s1 is convergent; A5: rng (s1") c= X proof let x be object; assume x in rng (s1"); then consider n being object such that A6: n in dom (s1") and A7: x = (s1").n by FUNCT_1:def 3; reconsider 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 thesis by A7,VALUED_1:10; end; A8: not 0 in rng s1 by A3; A9: now assume not s1 is non-zero; then consider n being Nat such that A10: s1.n = 0 by SEQ_1:5; n in NAT by ORDINAL1:def 12; hence contradiction by A8,FUNCT_2:4,A10; end; A11: now A12: rng (s1") c= X proof let y be object; assume y in rng (s1"); then consider x being object such that A13: x in dom (s1") and A14: y = (s1").x by FUNCT_1:def 3; reconsider x as Element of NAT by A13; s1.x in rng s1 by FUNCT_2:4; then 1/(s1.x) in Inv Inv X by A3; hence thesis by A14,VALUED_1:10; end; assume lim s1 = 0; then s1" is non bounded by A4,A9,Th38; then rng (s1") is non real-bounded by Th39; hence contradiction by A2,A12,XXREAL_2:45; end; then s1" is convergent by A4,A9,SEQ_2:21; then lim s1" in X by A1,A5; then 1/lim s1 in X by A4,A9,A11,SEQ_2:22; then 1/(1/lim s1) in Inv X; hence thesis; end; theorem Th56: for Z being Subset-Family of REAL st Z is closed holds meet Z is closed proof let Z be Subset-Family of REAL; assume A1: Z is closed; let seq be Real_Sequence; set mZ = meet Z; assume that A2: rng seq c= mZ and A3: seq is convergent; per cases; suppose Z = {}; then mZ = {} by SETFAM_1:def 1; hence thesis by A2; end; suppose A4: Z <> {}; now let X be set; assume A5: X in Z; then reconsider X9 = X as Subset of REAL; A6: rng seq c= X by A2,A5,SETFAM_1:def 1; X9 is closed by A1,A5; hence lim seq in X by A3,A6; end; hence thesis by A4,SETFAM_1:def 1; end; end; definition let X be real-membered set; func Cl X -> Subset of REAL equals meet { A where A is Subset of REAL : X c= A & A is closed }; coherence proof defpred P[Subset of REAL] means X c= \$1 & \$1 is closed; reconsider Z = { A where A is Subset of REAL : P[A] } as Subset-Family of REAL from DOMAIN_1:sch 7; reconsider Z as Subset-Family of REAL; meet Z is Subset of REAL; hence thesis; end; projectivity proof reconsider W = [#]REAL as Subset of REAL; let IT be Subset of REAL, X be real-membered set; set ClX = { A where A is Subset of REAL : X c= A & A is closed }, ClIT = { A where A is Subset of REAL : IT c= A & A is closed }; assume A1: IT = meet ClX; X c= W by MEMBERED:3; then A2: W in ClX; A3: W in ClIT; thus IT c= meet { A where A is Subset of REAL : IT c= A & A is closed } proof let e be object; assume A4: e in IT; for Y being set holds Y in ClIT implies e in Y proof let Y be set; assume Y in ClIT; 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 ClX holds X c= Z proof let Z be set; assume Z in ClX; then ex B being Subset of REAL st Z = B & X c= B & B is closed; hence thesis; end; then X c= IT by A1,A2,SETFAM_1:5; then X c= A by A6; then A in ClX by A7; hence thesis by A1,A4,A5,SETFAM_1:def 1; end; hence thesis by A3,SETFAM_1:def 1; end; let e be object; assume A8: e in meet ClIT; for Y being set holds Y in ClX implies e in Y proof let Y be set; assume A9: Y in ClX; 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 ClIT by A11; hence thesis by A8,A10,SETFAM_1:def 1; end; hence thesis by A1,A2,SETFAM_1:def 1; end; end; registration let X be real-membered set; cluster Cl X -> closed; coherence proof defpred P[Subset of REAL] means X c= \$1 & \$1 is closed; reconsider Z = { A where A is Subset of REAL : P[A] } as Subset-Family of REAL from DOMAIN_1:sch 7; reconsider Z as Subset-Family of REAL; Z is closed proof let Y be Subset of REAL; assume Y in Z; then ex A being Subset of REAL st Y = A & X c= A & A is closed; hence thesis; end; hence thesis by Th56; end; end; theorem Th57: for Y being closed Subset of REAL st X c= Y holds Cl X c= Y proof let Y be closed Subset of REAL; set ClX = { A where A is Subset of REAL : X c= A & A is closed }; assume X c= Y; then Y in ClX; hence thesis by SETFAM_1:3; end; theorem Th58: for X being real-membered set holds X c= Cl X proof let X be real-membered set; let x be object; set ClX = { A where A is Subset of REAL : X c= A & A is closed }; assume A1: x in X; A2: now let Y be set; assume Y in ClX; then ex YY being Subset of REAL st YY = Y & X c= YY & YY is closed; hence x in Y by A1; end; X c= [#]REAL by MEMBERED:3; then [#]REAL in ClX; hence thesis by A2,SETFAM_1:def 1; end; theorem Th59: X is closed iff X = Cl X proof hereby set ClX = { A where A is Subset of REAL : X c= A & A is closed }; assume X is closed; then X in ClX; then A1: Cl X c= X by SETFAM_1:3; X c= Cl X by Th58; hence X = Cl X by A1; end; thus thesis; end; theorem Cl ({}REAL) = {} by Th59; theorem Cl ([#]REAL) = REAL by Th59; theorem for X, Y being real-membered set holds X c= Y implies Cl X c= Cl Y proof let X, Y be real-membered set; assume A1: X c= 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; then Cl Y in ClX; hence thesis by SETFAM_1:3; end; theorem Th63: r3 in Cl X iff for O being open Subset of REAL st r3 in O holds O /\ X is non empty proof hereby assume A1: r3 in Cl X; let O be open Subset of REAL such that A2: r3 in O and A3: O /\ X is empty; O misses X by A3; 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; end; A6: (Cl X)` is open; X c= Cl X & (Cl X)` /\ X c= X by Th58,XBOOLE_1:17; then A7: (Cl X)` /\ X c= Cl X; (Cl X)` /\ X c= (Cl X)` by XBOOLE_1:17; then A8: (Cl X)` /\ X is empty by A7,SUBSET_1:20; reconsider rr3=r3 as Element of REAL by XREAL_0:def 1; assume for O being open Subset of REAL st r3 in O holds O /\ X is non empty; then not rr3 in (Cl X)` by A6,A8; hence thesis by SUBSET_1:29; end; theorem r3 in Cl X implies ex seq st rng seq c= X & seq is convergent & lim seq = r3 proof defpred P[object,object] means ex n being Nat st \$1 = n & \$2 = the Element of X/\].r3-1/(n+1),r3+1/(n+1).[; assume A1: r3 in Cl X; A2: now let x be object; assume x in NAT; then reconsider n = x as Element of NAT; set n1 = n+1; set oi = ].r3-1/n1,r3+1/n1.[; reconsider u = the Element of X/\oi as object; take u; A3: r3 < r3+1/n1 by XREAL_1:29; then r3-1/n1 < r3 by XREAL_1:19; then r3 in oi by A3; then X/\oi is non empty by A1,Th63; then u in X/\oi; hence u in REAL; thus P[x,u]; end; consider seq being Function such that A4: dom seq = NAT & rng seq c= REAL and A5: for x being object st x in NAT holds P[x,seq.x] from FUNCT_1:sch 6(A2); reconsider seq as Real_Sequence by A4,FUNCT_2:def 1,RELSET_1:4; take seq; thus rng seq c= X proof let y be object; assume y in rng seq; then consider x being object 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 = the Element of X/\].r3-1/(n+1),r3+1/(n+1).[ by A5,A6; reconsider n as Element of NAT by ORDINAL1:def 12; set n1 = n+1; set oi = ].r3-1/n1,r3+1/n1.[; A9: r3 < r3+1/n1 by XREAL_1:29; then r3-1/n1 < r3 by XREAL_1:19; then r3 in oi by A9; then X/\oi is non empty by A1,Th63; hence thesis by A7,A8,XBOOLE_0:def 4; end; A10: now let p be Real; set cp = [/ 1/p \]; A11: 1/p <= cp by INT_1:def 7; assume A12: 0= 1/cp by A12,A11,XREAL_1:85; then A15: 1/(n+1) < p by A14,XXREAL_0:2; let m be Nat; assume n<=m; then A16: n+1 <= m+1 by XREAL_1:6; set m1 = m+1; 1/m1 <= 1/(n+1) by A16,XREAL_1:85; then A17: 1/m1 < p by A15,XXREAL_0:2; set oi = ].r3-1/m1,r3+1/m1.[; A18: r3 < r3+1/m1 by XREAL_1:29; then r3-1/m1 < r3 by XREAL_1:19; then r3 in oi by A18; then A19: X/\oi is non empty by A1,Th63; m in NAT by ORDINAL1:def 12; then ex m9 being Nat st m9 = m & seq.m = the Element of X/\].r3-1/(m9+ 1),r3+1/(m9+1).[ by A5; then seq.m in oi by A19,XBOOLE_0:def 4; then consider s such that A20: seq.m = s and A21: r3-1/m1 < s & s < r3+1/m1; -1/m1 < s-r3 & s-r3 < 1/m1 by A21,XREAL_1:19,20; then |.s-r3.| < 1/m1 by SEQ_2:1; hence |.seq.m-r3.|

f.y; take r; let s be ExtReal; assume s in f.:X; then ex x being object st x in X & x in X & s = f.x by FUNCT_2:64; hence thesis by A5,A6; end; given p being Real such that A7: p is UpperBound of f.:X; take p + 1; let y be object; assume y in dom f; 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 thesis by A8,XXREAL_0:2; end; end; definition let X be set, f be Function of X, REAL; attr f is with_max means f.:X is with_max; attr f is with_min means f.:X is with_min; end; theorem Th65: for X, A being set, f being Function of X, REAL holds (-f).:A = --(f.:A) proof let X, A be set, f be Function of X, REAL; now let x be object; hereby assume x in (-f).:A; then consider x1 being object 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); end; assume x in --(f.:A); then consider r3 being Complex such that A2: x = -r3 and A3: r3 in f.:A; reconsider r3 as Real by A3; consider x1 being object 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; end; hence thesis by TARSKI:2; end; Lm9: for X being non empty set, f being Function of X, REAL st f is with_max holds -f is with_min proof let X be non empty set, f be Function of X, REAL; assume that A1: f.:X is bounded_above and A2: upper_bound (f.:X) in f.:X; A3: --(f.:X) = (-f).:X by Th65; hence (-f).:X is bounded_below by A1,Lm2; 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; hence thesis by A4,Th65; end; Lm10: for X being non empty set, f being Function of X, REAL st f is with_min holds -f is with_max proof let X be non empty set, f be Function of X, REAL; assume that A1: f.:X is bounded_below and A2: lower_bound (f.:X) in f.:X; A3: --(f.:X) = (-f).:X by Th65; hence (-f).:X is bounded_above by A1,Lm3; 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; hence thesis by A4,Th65; end; theorem Th66: for X being non empty set, f being Function of X, REAL holds f is with_min iff -f is with_max proof let X be non empty set, f be Function of X, REAL; - -f = f; hence thesis by Lm9,Lm10; end; theorem for X being non empty set, f being Function of X, REAL holds f is with_max iff -f is with_min proof let X be non empty set, f be Function of X, REAL; - -f = f; hence thesis by Th66; end; theorem for X being set, A being Subset of REAL, f being Function of X, REAL holds (-f)"A = f"(--A) proof let X be set, A be Subset of REAL, f be Function of X, REAL; now let x be object; reconsider xx=x as set by TARSKI:1; hereby A1: (-f).x = -(f.xx) by VALUED_1:8; assume A2: x in (-f)"A; then (-f).x in A by FUNCT_2:38; then - -f.xx in --A by A1; hence x in f"(--A) by A2,FUNCT_2:38; end; A3: (-f).x = -(f.xx) by VALUED_1:8; assume A4: 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; end; hence thesis by TARSKI:2; end; theorem for X, A being set, f being Function of X, REAL, s being Real holds (s+f).:A = s++(f.:A) proof let X, A be set, f be Function of X, REAL, s be Real; now let x be object; hereby assume x in (s+f).:A; then consider x1 being object 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 : q3 in f.:A }; hence x in s++(f.:A) by Lm5; end; assume x in s++(f.:A); then x in { s + q3 : q3 in f.:A } by Lm5; then consider r3 such that A2: x = s+r3 and A3: r3 in f.:A; consider x1 being object 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; end; hence thesis by TARSKI:2; end; theorem for X being set, A being Subset of REAL, f being Function of X,REAL, q3 holds (q3+f)"A = f"(-q3++A) proof let X be set, A be Subset of REAL, f be Function of X, REAL, q3 be Real; now let x be object; reconsider xx=x as set by TARSKI:1; hereby assume A1: x in (q3+f)"A; then (q3+f).x in A & (q3+f).x = q3+(f.xx) by FUNCT_2:38,VALUED_1:2; then -q3+(q3+(f.xx)) in { -q3 + p3 : p3 in A }; then -q3+(q3+(f.xx)) in -q3++A by Lm5; hence x in f"(-q3++A) by A1,FUNCT_2:38; end; assume A2: x in f"(-q3++A); then f.x in -q3++A & (q3+f).x = q3+(f.xx) by FUNCT_2:38,VALUED_1:2; then (q3+f).x in { q3+p3 : 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; end; hence thesis by TARSKI:2; 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; redefine func Inv f -> PartFunc of C,REAL; coherence proof f" is PartFunc of C,REAL; hence thesis; end; end; theorem for X being set, A being without_zero Subset of REAL, f being Function of X, REAL holds (Inv f)"A = f"(Inv A) proof let X be set, A be without_zero Subset of REAL, f be Function of X, REAL; now let x be object; reconsider xx=x as set by TARSKI:1; hereby A1: (Inv f).x = (f.xx)" by VALUED_1:10; assume A2: x in (Inv f)"A; then (Inv f).x in A by FUNCT_2:38; then 1/((f.xx)") in Inv A by A1; hence x in f"(Inv A) by A2,FUNCT_2:38; end; A3: (f.xx)" = 1/(f.xx) & (Inv f).x = (f.xx)" by VALUED_1:10; assume A4: x in f"(Inv 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; end; hence thesis by TARSKI:2; end; theorem for A being Subset of REAL, 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, x be Real; assume x in --A; then x in {-a where a is Complex: a in A}; then consider a being Complex such that A1: x = -a & a in A; reconsider a as Real by A1; take a; thus thesis by A1; end;