:: Some Properties of the Intervals
:: by J\'ozef Bia\las
::
:: Received February 5, 1994
:: Copyright (c) 1994-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, 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; :: redefines ++ (MEMBER_1, definition)
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 :: redefines without_zero (MEASURE6, synonym) → with_non-empty_elements (SETFAM_1, definition)
: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<r;
given s such that
A5: for n being Nat holds s<(seq").n;
set aa = |.r.|, ab = |.s.|;
set rab = 1/(aa+ab);
A6: 0 <= aa & 0 <= ab by COMPLEX1:46;
A7: now
let n be Element of NAT;
set g = seq.n, t = (seq").n;
set At = |.t.|;
t= 1/g by VALUED_1:10;
then
A8: At = 1/|.g.| by ABSVALUE:7;
t" = g " " by VALUED_1:10;
then t <> 0 by A2,SEQ_1:5,XCMPLX_1:202; then
A9: 0 < At by COMPLEX1:47;
s<t & t<r by A4,A5;
then At < aa+ab by Th37;
then At" > (aa+ab)" by A9,XREAL_1:88;
hence |.seq.n.| > rab by A8;
end;
A10: (seq").1<r by A4;
A11: s<(seq").1 by A5;
now
assume 0 >= 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 .|<rab by A1,A3,
SEQ_2:def 7;
A14: n in NAT by ORDINAL1:def 12;
|.seq.n-0 .|<rab by A13;
hence contradiction by A7,A14;
end;
theorem Th39: ::: SEQ_2
rng seq is real-bounded iff seq is bounded
proof
thus rng seq is real-bounded implies seq is bounded
proof
given s such that
A1: s is LowerBound of rng seq;
given t such that
A2: t is UpperBound of rng seq;
thus seq is bounded_above
proof
take t+1;
let n be Nat;
A3: n in NAT by ORDINAL1:def 12;
seq.n <= t & t < t+1 by A2,FUNCT_2:4,XREAL_1:29,XXREAL_2:def 1,A3;
hence thesis by XXREAL_0:2;
end;
take s-1;
let n be Nat;
s < s+1 by XREAL_1:29;
then
A4: s-1 < s by XREAL_1:19;
A5: n in NAT by ORDINAL1:def 12;
seq.n >= 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.n<t;
given s such that
A7: for n being Nat holds seq.n>s;
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 :: redefines with_max (MEASURE6, synonym) → right_end (XXREAL_2, definition)
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 :: redefines with_min (MEASURE6, synonym) → left_end (XXREAL_2, definition)
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; :: redefines -- (MEMBER_1, definition)
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<p;
then
A13: 0 < cp;
then reconsider cp as Element of NAT by INT_1:3;
reconsider n = cp as Nat;
take n;
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 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.|<p by A20,A17,XXREAL_0:2;
end;
hence seq is convergent;
hence thesis by A10,SEQ_2:def 7;
end;
begin :: Functions into Reals
definition
let X be set, f be Function of X, REAL;
redefine attr f is bounded_below means :: redefines bounded_below (SEQ_2, definition)
f.:X is bounded_below;
compatibility
proof
A1: dom f = X by FUNCT_2:def 1;
thus f is bounded_below implies f.:X is bounded_below
proof
given r such that
A2: for y being object st y in dom f holds r<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 A1,A2;
end;
given p being Real such that
A3: p is LowerBound 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
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 thesis by XREAL_1:19;
end;
redefine attr f is bounded_above means :: redefines bounded_above (SEQ_2, definition)
f.:X is bounded_above;
compatibility
proof
A5: dom f = X by FUNCT_2:def 1;
thus f is bounded_above implies f.:X is bounded_above
proof
given r such that
A6: for y being object st y in dom f holds r>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; :: redefines Inv (MEASURE6, synonym) → " (VALUED_1, definition)
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;