:: On the Continuity of Some Functions
:: by Artur Korni{\l}owicz
::
:: Received February 9, 2010
:: Copyright (c) 2010-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 RELAT_1, FUNCT_1, VALUED_0, TOPS_1, MEMBERED, XBOOLE_0, ARYTM_1,
COMPLEX1, ARYTM_3, XCMPLX_0, FINSEQ_1, EUCLID, PRE_TOPC, ORDINAL2,
TOPREALB, METRIC_1, TOPMETR, RCOMP_1, PCOMPS_1, FUNCT_3, FINSEQ_2,
RLVECT_1, RVSUM_1, SQUARE_1, FUNCT_4, VALUED_2, ALGSTR_0, SUBSET_1,
FUNCOP_1, PARTFUN1, CARD_3, FINSET_1, ZFMISC_1, TARSKI, CARD_1, TOPREALC,
NAT_1, XXREAL_0, VALUED_1, NUMBERS, ORDINAL4, STRUCT_0, XXREAL_1,
SUPINF_2, FUNCT_7, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, ORDINAL1, CARD_1, NUMBERS,
VALUED_0, VALUED_1, XCMPLX_0, XREAL_0, XXREAL_0, FUNCT_3, MEMBERED,
COMPLEX1, SQUARE_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, RCOMP_1, FUNCT_7,
VALUED_2, STRUCT_0, RVSUM_1, PRE_TOPC, TOPS_1, METRIC_1, PCOMPS_1,
TOPMETR, T_0TOPSP, BORSUK_1, ALGSTR_0, RLVECT_1, RLTOPSP1, EUCLID,
WAYBEL18, TOPREAL9, TOPREALB;
constructors MONOID_0, FUNCT_7, FINSEQOP, VALUED_2, TOPREAL9, TOPREALB,
TOPS_1, COMPLEX1, T_0TOPSP, SQUARE_1, FUNCT_4, FUNCSDOM, CONVEX1,
WAYBEL18, BINOP_2, EUCLID_9, PARTFUN3, REAL_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, VALUED_0, VALUED_1, MEMBERED,
XCMPLX_0, XREAL_0, VALUED_2, PRE_TOPC, STRUCT_0, EUCLID, MONOID_0,
TOPREALB, XXREAL_0, NAT_1, TOPMETR, FUNCT_2, RVSUM_1, TOPREAL9, SQUARE_1,
RCOMP_1, TOPS_1, FUNCT_7, NUMBERS, RLVECT_1, FINSEQ_1, FUNCOP_1,
WAYBEL18, BORSUK_1, PRE_POLY, JORDAN2B, FINSEQ_2, PARTFUN3, EUCLID_9,
CARD_1, FINSET_1, RELSET_1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, LATTICE7, FUNCT_1, FUNCT_2, VALUED_0, VALUED_2,
STRUCT_0;
equalities FINSEQ_1, RLVECT_1, XCMPLX_0, SQUARE_1, BINOP_1, FUNCOP_1,
VALUED_1, FINSEQ_2, VALUED_2, STRUCT_0, METRIC_1, PCOMPS_1, TOPMETR,
CONVEX1, RLTOPSP1, EUCLID, TOPREALB, RVSUM_1, ORDINAL1;
expansions XBOOLE_0, FUNCT_1, STRUCT_0, TOPMETR;
theorems FUNCT_1, PARTFUN1, FUNCT_2, VALUED_1, FUNCT_7, SEQ_2, VALUED_2,
BORSUK_1, TOPREALB, TOPMETR, TOPREAL9, EUCLID, JGRAPH_2, JGRAPH_6,
GOBOARD6, TOPS_1, METRIC_1, JGRAPH_1, TOPRNS_1, XXREAL_0, XREAL_1,
XBOOLE_0, RCOMP_1, JORDAN2B, FINSEQ_2, XREAL_0, FINSEQ_1, NAT_1,
FUNCOP_1, PRE_TOPC, SQUARE_1, TOPREAL6, RVSUM_1, COMPLEX1, XXREAL_1,
XCMPLX_1, ORDINAL1, TSP_1, RLVECT_1, TOPS_3, YELLOW12, TOPGEN_5,
YELLOW17, ZFMISC_1, REAL_NS1, WAYBEL18, BINOP_1, JGRAPH_4, ABSVALUE,
CARD_1, STRUCT_0, PRVECT_2, TOPREAL7, EUCLID_9, TOPS_4, NAT_D;
schemes FUNCT_2, BINOP_1, FINSEQ_2;
begin :: Preliminaries
reserve
x for object, X for set,
i, n, m for Nat,
r, s for Real,
c, c1, c2, d for Complex,
f, g for complex-valued Function,
g1 for n-element complex-valued FinSequence,
f1 for n-element real-valued FinSequence,
T for non empty TopSpace,
p for Element of TOP-REAL n;
theorem
for X being trivial set, Y being set st X,Y are_equipotent holds Y is trivial
proof
let X be trivial set, Y be set such that
A1: X,Y are_equipotent;
A2: card X < 2 by NAT_D:60;
A3: Y is finite by A1,CARD_1:38;
card X = card Y by A1,CARD_1:5;
hence thesis by A2,A3,NAT_D:60;
end;
registration
let r be Real;
cluster r^2 -> non negative;
coherence;
end;
registration
let r be positive Real;
cluster r^2 -> positive;
coherence;
end;
registration
cluster sqrt(0) -> zero;
coherence;
end;
registration
let f be empty set;
cluster sqr(f) -> empty;
coherence;
cluster |.f.| -> zero;
coherence by RVSUM_1:72;
end;
theorem Th2:
f(#)(c1+c2) = f(#)c1 + f(#)c2
proof
A1: dom (f(#)(c1+c2)) = dom f by VALUED_1:def 5;
A2: dom (f(#)c1) = dom f by VALUED_1:def 5;
A3: dom (f(#)c2) = dom f by VALUED_1:def 5;
A4: dom (f(#)c1 + f(#)c2) = dom (f(#)c1) /\ dom (f(#)c2) by VALUED_1:def 1;
hence dom (f(#)(c1+c2)) = dom (f(#)c1 + f(#)c2) by A2,A3,VALUED_1:def 5;
let x be object;
assume
A5: x in dom (f(#)(c1+c2));
hence (f(#)(c1+c2)).x = f.x * (c1+c2) by VALUED_1:def 5
.= f.x*c1 + f.x*c2
.= (f(#)c1).x + f.x*c2 by A1,A2,A5,VALUED_1:def 5
.= (f(#)c1).x + (f(#)c2).x by A1,A3,A5,VALUED_1:def 5
.= (f(#)c1 + f(#)c2).x by A1,A2,A3,A4,A5,VALUED_1:def 1;
end;
theorem
f(#)(c1-c2) = f(#)c1 - f(#)c2
proof
thus f(#)(c1-c2) = f(#)c1 + f(#)-c2 by Th2
.= f(#)c1 - f(#)c2 by VALUED_2:24;
end;
theorem Th4:
f(/)c + g(/)c = (f+g)(/)c
proof
A1: dom (f(/)c + g(/)c) = dom (f(/)c) /\ dom (g(/)c) by VALUED_1:def 1;
A2: dom (f(/)c) = dom f by VALUED_2:28;
A3: dom (g(/)c) = dom g by VALUED_2:28;
A4: dom ((f+g)(/)c) = dom (f+g) by VALUED_2:28;
A5: dom (f+g) = dom f /\ dom g by VALUED_1:def 1;
thus dom (f(/)c + g(/)c) = dom ((f+g)(/)c) by A1,A2,A3,A4,VALUED_1:def 1;
let x be object;
assume
A6: x in dom (f(/)c + g(/)c);
thus ((f+g)(/)c).x = (f+g).x/c by VALUED_2:29
.= (f.x+g.x)/c by A1,A2,A3,A6,A5,VALUED_1:def 1
.= f.x/c + g.x/c
.= f.x/c + (g(/)c).x by VALUED_2:29
.= (f(/)c).x + (g(/)c).x by VALUED_2:29
.= (f(/)c + g(/)c).x by A6,VALUED_1:def 1;
end;
theorem
f(/)c - g(/)c = (f-g)(/)c
proof
thus f(/)c - g(/)c = f(/)c + (-g)(/)c by VALUED_2:30
.= (f-g)(/)c by Th4;
end;
theorem
c1 <> 0 & c2 <> 0 implies f(/)c1 - g(/)c2 = (f(#)c2-g(#)c1) (/) (c1*c2)
proof
assume
A1: c1 <> 0 & c2 <> 0;
A2: dom (f(/)c1) = dom f by VALUED_2:28;
A3: dom (g(/)c2) = dom g by VALUED_2:28;
A4: dom (f(#)c2) = dom f by VALUED_1:def 5;
A5: dom (g(#)c1) = dom g by VALUED_1:def 5;
A6: dom (f(/)c1-g(/)c2) = dom (f(/)c1) /\ dom (g(/)c2) by VALUED_1:12;
A7: dom (f(#)c2-g(#)c1) = dom (f(#)c2) /\ dom (g(#)c1) by VALUED_1:12;
hence dom (f(/)c1 - g(/)c2) = dom ((f(#)c2-g(#)c1) (/) (c1*c2))
by A2,A3,A4,A5,A6,VALUED_2:28;
let x be object;
assume
A8: x in dom (f(/)c1 - g(/)c2);
hence ((f(/)c1 - g(/)c2)).x = (f(/)c1).x - (g(/)c2).x by VALUED_1:13
.= (f.x/c1) - (g(/)c2).x by VALUED_2:29
.= (f.x/c1) - (g.x/c2) by VALUED_2:29
.= (f.x*c2-g.x*c1) / (c1*c2) by A1,XCMPLX_1:130
.= (f.x*c2-(g(#)c1).x) / (c1*c2) by VALUED_1:6
.= ((f(#)c2).x-(g(#)c1).x) / (c1*c2) by VALUED_1:6
.= ((f(#)c2-g(#)c1)).x / (c1*c2) by A2,A3,A4,A5,A6,A7,A8,VALUED_1:13
.= ((f(#)c2-g(#)c1) (/) (c1*c2)).x by VALUED_2:29;
end;
theorem
c <> 0 implies f(/)c - g = (f-c(#)g) (/) c
proof
assume
A1: c <> 0;
A2: dom(f(/)c - g) = dom(f(/)c) /\ dom g by VALUED_1:12
.= dom f /\ dom g by VALUED_2:28;
A3: dom(f-c(#)g) = dom f /\ dom(c(#)g) by VALUED_1:12
.= dom f /\ dom g by VALUED_1:def 5;
hence dom(f(/)c - g) = dom((f-c(#)g) (/) c) by A2,VALUED_2:28;
let x be object;
assume
A4: x in dom(f(/)c - g);
hence (f(/)c - g).x = (f(/)c).x - g.x by VALUED_1:13
.= f.x/c - g.x by VALUED_2:29
.= f.x/c - c*g.x/c by A1,XCMPLX_1:89
.= f.x/c - (c(#)g).x/c by VALUED_1:6
.= (f.x-(c(#)g).x) / c
.= ((f-c(#)g)).x / c by A2,A3,A4,VALUED_1:13
.= ((f-c(#)g) (/) c).x by VALUED_2:29;
end;
theorem
(c-d)(#)f = c(#)f - d(#)f
proof
dom(c(#)f - d(#)f) = dom(c(#)f) /\ dom(d(#)f) by VALUED_1:12
.= dom f /\ dom(d(#)f) by VALUED_1:def 5
.= dom f /\ dom f by VALUED_1:def 5;
hence
A1: dom((c-d)(#)f) = dom(c(#)f - d(#)f) by VALUED_1:def 5;
let x be object;
assume
A2: x in dom((c-d)(#)f);
thus ((c-d)(#)f).x = (c-d)*f.x by VALUED_1:6
.= c*f.x - d*f.x
.= c*f.x - (d(#)f).x by VALUED_1:6
.= (c(#)f).x - (d(#)f).x by VALUED_1:6
.= (c(#)f - d(#)f).x by A1,A2,VALUED_1:13;
end;
theorem
(f-g)^2 = (g-f)^2
proof
A1: dom(f-g) = dom f /\ dom g by VALUED_1:12;
A2: dom(g-f) = dom g /\ dom f by VALUED_1:12;
A3: dom((f-g)^2) = dom(f-g) by VALUED_1:11;
hence dom((f-g)^2) = dom((g-f)^2) by A1,A2,VALUED_1:11;
let x be object;
assume
A4: x in dom((f-g)^2);
then
A5: (f-g).x = f.x - g.x by A3,VALUED_1:13;
A6: (g-f).x = g.x - f.x by A1,A3,A4,A2,VALUED_1:13;
thus ((f-g)^2).x = (f-g).x * (f-g).x by VALUED_1:5
.= (g-f).x * (g-f).x by A5,A6
.= ((g-f)^2).x by VALUED_1:5;
end;
theorem
(f(/)c)^2 = f^2 (/) c^2
proof
thus dom((f(/)c)^2) = dom(f(/)c) by VALUED_1:11
.= dom f by VALUED_2:28
.= dom(f^2) by VALUED_1:11
.= dom(f^2 (/) c^2) by VALUED_2:28;
let x be object;
assume x in dom((f(/)c)^2);
thus ((f(/)c)^2).x = ((f(/)c).x)^2 by VALUED_1:11
.= (f.x/c)^2 by VALUED_2:29
.= (f.x)^2 / c^2 by XCMPLX_1:76
.= (f^2).x / c^2 by VALUED_1:11
.= (f^2 (/) c^2).x by VALUED_2:29;
end;
theorem Th11:
|. (n|->r) - (n|->s) .| = sqrt(n) * |.r-s.|
proof
thus |. (n|->r) - (n|->s) .| = sqrt Sum sqr (n|->(r-s)) by RVSUM_1:30
.= sqrt Sum (n|->(r-s)^2) by RVSUM_1:56
.= sqrt (n*(r-s)^2) by RVSUM_1:80
.= sqrt n * sqrt((r-s)^2) by SQUARE_1:29
.= sqrt n * |.r-s.| by COMPLEX1:72;
end;
registration
let f,x,c;
cluster f+*(x,c) -> complex-valued;
coherence
proof
set F = f+*(x,c);
let a be object such that a in dom F;
per cases;
suppose x in dom f & x = a;
hence thesis by FUNCT_7:31;
end;
suppose x in dom f & x <> a;
then F.a = f.a by FUNCT_7:32;
hence thesis;
end;
suppose not x in dom f;
then F.a = f.a by FUNCT_7:def 3;
hence thesis;
end;
end;
end;
theorem Th12:
((0*n)+*(x,c))^2 = (0*n)+*(x,c^2)
proof
set f = (0*n)+*(x,c);
set g = (0*n)+*(x,c^2);
A1: dom f = dom (0*n) by FUNCT_7:30;
A2: dom g = dom (0*n) by FUNCT_7:30;
A3: dom (f^2) = dom f by VALUED_1:11;
thus dom (f^2) = dom g by A1,A2,VALUED_1:11;
let a be object;
assume
A4: a in dom (f^2);
A5: (f^2).a = (f.a)^2 by VALUED_1:11;
per cases;
suppose
A6: a = x;
then f.a = c by A1,A3,A4,FUNCT_7:31;
hence thesis by A6,A1,A3,A4,A5,FUNCT_7:31;
end;
suppose
A7: a <> x;
then
A8: f.a = (n|->0).a by FUNCT_7:32
.= {}.x;
g.a = (n|->0).a by A7,FUNCT_7:32
.= {}.x;
hence thesis by A5,A8;
end;
end;
theorem Th13:
x in Seg n implies |.(0*n)+*(x,r).| = |.r.|
proof
set f = (0*n)+*(x,r);
A1: n in NAT by ORDINAL1:def 12;
assume
A2: x in Seg n;
f^2 = (0*n)+*(x,r^2) by Th12;
then Sum (f^2) = r^2 by A2,A1,JORDAN2B:10;
hence thesis by COMPLEX1:72;
end;
theorem Th14:
(0.REAL n)+*(x,0) = 0.REAL n
proof
set p = (0.REAL n)+*(x,0);
A1: dom p = Seg n by FINSEQ_1:89;
A2: dom ((0.REAL n)+*(x,0)) = dom (0.REAL n) by FUNCT_7:30;
A3: dom (0.REAL n) = Seg n;
now
let z be object;
assume
A4: z in dom p;
per cases;
suppose z = x;
hence p.z = 0 by A1,A3,A4,FUNCT_7:31
.= (0.REAL n).z;
end;
suppose z <> x;
hence p.z = (0.REAL n).z by FUNCT_7:32;
end;
end;
hence thesis by A2;
end;
theorem Th15:
mlt(f1,(0.REAL n)+*(x,r)) = (0.REAL n)+*(x,f1.x*r)
proof
set p = (0.REAL n)+*(x,r);
A1: dom f1 = Seg n by FINSEQ_1:89;
A2: dom p = Seg n by FINSEQ_1:89;
A3: dom mlt(f1,p) = dom f1 /\ dom p by VALUED_1:def 4;
A4: dom ((0.REAL n)+*(x,f1.x*r)) = dom (0.REAL n) by FUNCT_7:30;
A5: dom (0.REAL n) = Seg n;
now
let z be object;
assume
A6: z in dom mlt(f1,p);
A7: (mlt(f1,p)).z = f1.z*p.z by VALUED_1:5;
per cases;
suppose
A8: z = x;
hence (mlt(f1,p)).z = f1.z*r by A1,A2,A3,A5,A6,A7,FUNCT_7:31
.= ((0.REAL n)+*(x,f1.x*r)).z by A1,A2,A3,A5,A6,A8,FUNCT_7:31;
end;
suppose
A9: z <> x;
hence (mlt(f1,p)).z = f1.z*(0.REAL n).z by A7,FUNCT_7:32
.= f1.z*(n|->0).z
.= ((0.REAL n)+*(x,f1.x*r)).z by A9,FUNCT_7:32;
end;
end;
hence thesis by A4,FINSEQ_1:89;
end;
theorem
|(f1,(0.REAL n)+*(x,r))| = f1.x * r
proof
A1: mlt(f1,(0.REAL n)+*(x,r)) = (0.REAL n)+*(x,f1.x*r) by Th15;
A2: dom f1 = Seg n by FINSEQ_1:89;
A3: n in NAT by ORDINAL1:def 12;
per cases;
suppose x in dom f1;
hence thesis by A1,A2,A3,JORDAN2B:10;
end;
suppose not x in dom f1;
then
A4: f1.x = 0 by FUNCT_1:def 2;
hence |(f1,(0.REAL n)+*(x,r))| = Sum 0.REAL n by A1,Th14
.= f1.x * r by A4,A3,JORDAN2B:9;
end;
end;
theorem Th17:
(g1+*(i,c)) - g1 = (0*n)+*(i,c-(g1.i))
proof
A1: dom (g1+*(i,c) - g1) = dom (g1+*(i,c)) /\ dom g1 by VALUED_1:12;
A2: dom (0*n) = Seg n;
A3: dom g1 = Seg n by FINSEQ_1:89;
A4: dom (g1+*(i,c)) = dom g1 by FUNCT_7:30;
hence dom (g1+*(i,c) - g1) = dom ((0*n)+*(i,c-(g1.i)))
by A1,A3,FINSEQ_1:89;
let x be object;
assume
A5: x in dom (g1+*(i,c) - g1);
then
A6: (g1+*(i,c) - g1).x = (g1+*(i,c)).x - g1.x by VALUED_1:13;
per cases;
suppose
A7: x = i;
hence (g1+*(i,c) - g1).x = c - g1.x by A6,A1,A5,A4,FUNCT_7:31
.= ((0*n)+*(i,c-(g1.i))).x by A1,A2,A3,A5,A4,A7,FUNCT_7:31;
end;
suppose
A8: x <> i;
hence (g1+*(i,c) - g1).x = g1.x - g1.x by A6,FUNCT_7:32
.= (n|->0).x
.= ((0*n)+*(i,c-(g1.i))).x by A8,FUNCT_7:32;
end;
end;
theorem
|.<*r*>.| = |.r.|
proof
set f = <*r*>;
sqr f = <*r^2*> by RVSUM_1:55;
then Sum sqr f = r^2 by RVSUM_1:73;
hence thesis by COMPLEX1:72;
end;
theorem
for f being real-valued FinSequence holds f is FinSequence of REAL
by RVSUM_1:145;
theorem
for f being real-valued FinSequence st |.f.| <> 0
ex i being Nat st i in dom f & f.i <> 0
proof
let f be real-valued FinSequence;
assume |.f.| <> 0;
then consider i being Element of NAT such that
A1: i in dom sqr f and
A2: (sqr f).i <> 0 by PRVECT_2:3,SQUARE_1:17;
take i;
thus i in dom f by A1,VALUED_1:11;
(sqr f).i = (f.i)^2 by VALUED_1:11;
hence thesis by A2;
end;
theorem Th21:
for f being real-valued FinSequence holds |.Sum f.| <= Sum abs f
proof
let f be real-valued FinSequence;
defpred P[set] means ex F being real-valued FinSequence st F = $1 &
|.Sum F.| <= Sum abs F;
A1: P[<*>REAL]
proof
take <*>REAL;
thus thesis by ABSVALUE:2,RVSUM_1:72;
end;
A2: for p being FinSequence of REAL, x being Element of REAL st P[p] holds
P[p^<*x*>]
proof
let p be FinSequence of REAL, x be Element of REAL;
given F being real-valued FinSequence such that
A3: F = p and
A4: |.Sum F.| <= Sum abs F;
A5: |.Sum F.| + |.x.| <= Sum abs F + |.x.| by A4,XREAL_1:6;
take G = p^<*x*>;
A6: abs <*x*> = <*|.x.|*> by JORDAN2B:19;
A7: Sum <*|.x.|*> = |.x.| by RVSUM_1:73;
abs G = (abs p)^abs<*x*> by TOPREAL7:11;
then
A8: Sum abs G = Sum abs p + |.x.| by A6,A7,RVSUM_1:75;
Sum G = Sum p + x by RVSUM_1:74;
then |.Sum G.| <= |.Sum p.| + |.x.| by COMPLEX1:56;
hence thesis by A8,A3,A5,XXREAL_0:2;
end;
A9: for p being FinSequence of REAL holds P[p] from FINSEQ_2:sch 2(A1,A2);
f is FinSequence of REAL by RVSUM_1:145;
then P[f] by A9;
hence thesis;
end;
theorem
for A being non empty 1-sorted, B being 1-element 1-sorted
for t being Point of B
for f being Function of A,B holds f = A --> t
proof
let A be non empty 1-sorted;
let B be 1-element 1-sorted;
let t be Point of B;
let f be Function of A,B;
let a be Element of A;
thus f.a = (A --> t).a by STRUCT_0:def 10;
end;
registration
let n be non zero Nat, i be Element of Seg n;
let T be real-membered non empty TopSpace;
cluster proj(Seg n --> T,i) -> real-valued;
coherence;
end;
definition
let n; let p be Element of REAL n; let r;
redefine func p(/)r -> Element of REAL n; :: redefines (/) (VALUED_2, definition)
coherence
proof
A1: p(/)r is FinSequence of REAL by RVSUM_1:145;
A2: len p = n by CARD_1:def 7;
Seg len (p(/)r) = dom (p(/)r) by FINSEQ_1:def 3
.= dom p by VALUED_1:def 5
.= Seg n by A2,FINSEQ_1:def 3;
then len (p(/)r) = n by FINSEQ_1:6;
hence thesis by A1,FINSEQ_2:92;
end;
end;
theorem Th23:
for p, q being Point of TOP-REAL m holds p in Ball(q,r) iff -p in Ball(-q,r)
proof
let p, q be Point of TOP-REAL m;
A1: now
let a, b be Point of TOP-REAL m;
assume a in Ball(b,r);
then
A2: |.a-b.| < r by TOPREAL9:7;
-a--b = (-a)+-(-b) .= -(a-b) by RLVECT_1:31;
then |.-a--b.| = |.a-b.| by EUCLID:71;
hence -a in Ball(-b,r) by A2,TOPREAL9:7;
end;
--p = p & --q = q;
hence thesis by A1;
end;
definition
let S be 1-sorted;
attr S is complex-functions-membered means
:Def1:
the carrier of S is complex-functions-membered;
attr S is real-functions-membered means
:Def2:
the carrier of S is real-functions-membered;
end;
registration
let n;
cluster TOP-REAL n -> real-functions-membered;
coherence
proof
let x;
assume x in the carrier of TOP-REAL n;
then reconsider x as Point of TOP-REAL n;
x is real-valued;
hence thesis;
end;
end;
registration
cluster TOP-REAL 0 -> real-membered;
coherence
by EUCLID:22,EUCLID:77;
end;
registration
cluster TOP-REAL 0 -> trivial;
coherence;
end;
registration
cluster real-functions-membered -> complex-functions-membered for 1-sorted;
coherence;
end;
registration
cluster strict non empty real-functions-membered for 1-sorted;
existence
proof
take S = 1-sorted(#{the real-valued Function}#);
thus S is strict;
thus the carrier of S is non empty;
let x;
thus thesis;
end;
end;
registration
let S be complex-functions-membered 1-sorted;
cluster the carrier of S -> complex-functions-membered;
coherence by Def1;
end;
registration
let S be real-functions-membered 1-sorted;
cluster the carrier of S -> real-functions-membered;
coherence by Def2;
end;
registration
cluster strict non empty real-functions-membered for TopSpace;
existence
proof
take the TopStruct of TOP-REAL 1;
thus thesis;
end;
end;
registration
let S be complex-functions-membered TopSpace;
cluster -> complex-functions-membered for SubSpace of S;
coherence
proof
let A be SubSpace of S;
let x;
the carrier of A c= the carrier of S by BORSUK_1:1;
hence thesis;
end;
end;
registration
let S be real-functions-membered TopSpace;
cluster -> real-functions-membered for SubSpace of S;
coherence
proof
let A be SubSpace of S;
let x;
the carrier of A c= the carrier of S by BORSUK_1:1;
hence thesis;
end;
end;
definition
let X be complex-functions-membered set;
func (-)X -> complex-functions-membered set means
:Def3:
for f being complex-valued Function holds -f in it iff f in X;
existence
proof
set F = {-f where f is Element of X: f in X};
F is complex-functions-membered
proof
let x;
assume x in F;
then ex f being Element of X st x = -f & f in X;
hence thesis;
end;
then reconsider F as complex-functions-membered set;
take F;
let f be complex-valued Function;
hereby
assume -f in F;
then ex g being Element of X st -f = -g & g in X;
hence f in X by RVSUM_1:24;
end;
thus thesis;
end;
uniqueness
proof
let A, B be complex-functions-membered set such that
A1: for f being complex-valued Function holds -f in A iff f in X and
A2: for f being complex-valued Function holds -f in B iff f in X;
thus A c= B
proof
let x be object;
assume
A3: x in A;
then reconsider x as Element of A;
A4: --x = x;
then -x in X by A1,A3;
hence thesis by A2,A4;
end;
let x be object;
assume
A5: x in B;
then reconsider x as Element of B;
A6: --x = x;
then -x in X by A2,A5;
hence thesis by A1,A6;
end;
involutiveness
proof
let r, A be complex-functions-membered set;
assume
A7: for f being complex-valued Function holds -f in r iff f in A;
let f be complex-valued Function;
hereby
assume -f in A;
then --f in r by A7;
hence f in r;
end;
assume f in r;
then --f in r;
hence -f in A by A7;
end;
end;
registration
let X be empty set;
cluster (-)X -> empty;
coherence
proof
assume not thesis;
then consider x being object such that
A1: x in (-)X;
reconsider x as Element of (-)X by A1;
--x = x;
hence thesis by A1,Def3;
end;
end;
registration
let X be non empty complex-functions-membered set;
cluster (-)X -> non empty;
coherence
proof
consider x being object such that
A1: x in X by XBOOLE_0:def 1;
reconsider x as Element of X by A1;
-x in (-)X by Def3;
hence thesis;
end;
end;
theorem Th24:
for X being complex-functions-membered set,
f being complex-valued Function holds
-f in X iff f in (-)X
proof
let X be complex-functions-membered set,
f be complex-valued Function;
--f = f & (-)(-)X = X;
hence thesis by Def3;
end;
registration
let X be real-functions-membered set;
cluster (-)X -> real-functions-membered;
coherence
proof
let x;
assume
A1: x in (-)X;
then reconsider x as Element of (-)X;
A2: -x in X by A1,Th24;
--x = x & (-)(-)X = X;
hence thesis by A2;
end;
end;
theorem Th25:
for X being Subset of TOP-REAL n holds -X = (-)X
proof
set T = TOP-REAL n;
let X be Subset of T;
for f being complex-valued Function holds -f in -X iff f in X
proof
let f be complex-valued Function;
hereby
assume -f in -X;
then consider v being Element of T such that
A1: -f = (-1)*v and
A2: v in X;
reconsider g = -f as Element of T by A1;
-g = --v by A1
.= v;
hence f in X by A2;
end;
assume
A3: f in X;
then reconsider g = f as Element of T;
-g = (-1)*g;
hence thesis by A3;
end;
hence thesis by Def3;
end;
definition
let n;
let X be Subset of TOP-REAL n;
redefine func (-)X -> Subset of TOP-REAL n; :: redefines (-) (TOPREALC, definition)
coherence
proof
-X = (-)X by Th25;
hence thesis;
end;
end;
registration
let n;
let X be open Subset of TOP-REAL n;
cluster (-)X -> open for Subset of TOP-REAL n;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider Y = (-)X as Subset of TOP-REAL n;
for p being Point of TOP-REAL n st p in Y
ex r being positive Real st Ball(p,r) c= Y
proof
let p be Point of TOP-REAL n;
assume p in Y;
then -(p qua real-valued Function) in (-)Y by Def3;
then consider r being positive Real such that
A1: Ball(-p,r) c= X by TOPS_4:2;
take r;
let x be Element of TOP-REAL n;
assume x in Ball(p,r);
then -x in Ball(-p,r) by Th23;
hence thesis by A1,Th24;
end;
hence thesis by TOPS_4:2;
end;
end;
definition
let R,S,T be non empty TopSpace, f be Function of [:R,S:],T;
let x be Point of [:R,S:];
redefine func f.x -> Point of T; :: redefines . (FUNCT_1, definition)
coherence
proof
consider x1 being Point of R, x2 being Point of S such that
A1: x = [x1,x2] by BORSUK_1:10;
f. [x1,x2] is Point of T;
hence thesis by A1;
end;
end;
definition
let R,S,T be non empty TopSpace, f be Function of [:R,S:],T;
let r be Point of R, s be Point of S;
redefine func f.(r,s) -> Point of T; :: redefines . (BINOP_1, definition)
coherence
proof
f.(r,s) = f. [r,s];
hence thesis;
end;
end;
definition
let n, p, r;
redefine func p + r -> Point of TOP-REAL n; :: redefines + (VALUED_1, synonym) → + (VALUED_1, definition)
coherence
proof
A1: p+r is FinSequence of REAL by RVSUM_1:145;
A2: len p = n by CARD_1:def 7;
Seg len (p+r) = dom (p+r) by FINSEQ_1:def 3
.= dom p by VALUED_1:def 2
.= Seg n by A2,FINSEQ_1:def 3;
then len (p+r) = n by FINSEQ_1:6;
then p+r is Element of REAL n by A1,FINSEQ_2:92;
hence thesis by EUCLID:22;
end;
end;
definition
let n, p, r;
redefine func p - r -> Point of TOP-REAL n; :: redefines - (VALUED_1, definition)
coherence
proof
p+-r is Point of TOP-REAL n;
hence thesis;
end;
end;
definition
let n, p, r;
redefine func p (#) r -> Point of TOP-REAL n; :: redefines (#) (VALUED_1, synonym) → (#) (VALUED_1, definition)
coherence
proof
A1: p(#)r is FinSequence of REAL by RVSUM_1:145;
A2: len p = n by CARD_1:def 7;
Seg len (p(#)r) = dom (p(#)r) by FINSEQ_1:def 3
.= dom p by VALUED_1:def 5
.= Seg n by A2,FINSEQ_1:def 3;
then len (p(#)r) = n by FINSEQ_1:6;
then p(#)r is Element of REAL n by A1,FINSEQ_2:92;
hence thesis by EUCLID:22;
end;
end;
definition
let n, p, r;
redefine func p (/) r -> Point of TOP-REAL n; :: redefines (/) (VALUED_2, definition)
coherence
proof
reconsider f = p as Element of REAL n by EUCLID:22;
f(/)r is Element of REAL n;
hence thesis by EUCLID:22;
end;
end;
definition
let n; let p1, p2 be Point of TOP-REAL n;
redefine func p1 (#) p2 -> Point of TOP-REAL n; :: redefines (#) (VALUED_1, definition)
coherence
proof
A1: p1(#)p2 is FinSequence of REAL by RVSUM_1:145;
A2: len p1 = n & len p2 = n by CARD_1:def 7;
Seg len (p1(#)p2) = dom (p1(#)p2) by FINSEQ_1:def 3
.= dom p1 /\ dom p2 by VALUED_1:def 4
.= Seg n /\ dom p2 by A2,FINSEQ_1:def 3
.= Seg n /\ Seg n by A2,FINSEQ_1:def 3;
then len (p1(#)p2) = n by FINSEQ_1:6;
then p1(#)p2 is Element of REAL n by A1,FINSEQ_2:92;
hence thesis by EUCLID:22;
end;
end;
definition
let n; let p be Point of TOP-REAL n;
redefine func sqr p -> Point of TOP-REAL n; :: redefines sqr (RVSUM_1, synonym) → ^2 (VALUED_1, definition)
coherence
proof
sqr p = p(#)p;
hence thesis;
end;
end;
definition
let n; let p1, p2 be Point of TOP-REAL n;
redefine func p1 /" p2 -> Point of TOP-REAL n; :: redefines /" (VALUED_1, definition)
coherence
proof
A1: p1/"p2 is FinSequence of REAL by RVSUM_1:145;
A2: len p1 = n & len p2 = n by CARD_1:def 7;
Seg len (p1/"p2) = dom (p1/"p2) by FINSEQ_1:def 3
.= dom p1 /\ dom p2 by VALUED_1:16
.= Seg n /\ dom p2 by A2,FINSEQ_1:def 3
.= Seg n /\ Seg n by A2,FINSEQ_1:def 3;
then len (p1/"p2) = n by FINSEQ_1:6;
then p1/"p2 is Element of REAL n by A1,FINSEQ_2:92;
hence thesis by EUCLID:22;
end;
end;
definition
let n, p, x, r;
redefine func p+*(x,r) -> Point of TOP-REAL n; :: redefines +* (FUNCT_7, definition)
coherence
proof
A1: p+*(x,r) is FinSequence of REAL by RVSUM_1:145;
A2: len p = n by CARD_1:def 7;
Seg len (p+*(x,r)) = dom (p+*(x,r)) by FINSEQ_1:def 3
.= dom p by FUNCT_7:30
.= Seg n by A2,FINSEQ_1:def 3;
then len (p+*(x,r)) = n by FINSEQ_1:6;
then p+*(x,r) is Element of REAL n by A1,FINSEQ_2:92;
hence thesis by EUCLID:22;
end;
end;
theorem
for a, o being Point of TOP-REAL n holds
n <> 0 & a in Ball(o,r) implies |.Sum(a-o).| < n*r
proof
let a, o be Point of TOP-REAL n;
set R1 = a-o, R2 = n|->r;
assume that
A1: n <> 0 and
A2: a in Ball(o,r);
A3: Sum R2 = n*r by RVSUM_1:80;
A5: for j being Nat st j in Seg n holds (abs R1).j < R2.j
proof
let j be Nat;
assume j in Seg n;
then
A6: R2.j = r by FINSEQ_2:57;
|.R1.j.| < r by A2,EUCLID_9:9;
hence thesis by A6,VALUED_1:18;
end;
then
A7: for j being Nat st j in Seg n holds (abs R1).j <= R2.j;
ex j being Nat st j in Seg n & (abs R1).j < R2.j
proof
take 1;
1 <= n by A1,NAT_1:14;
hence 1 in Seg n;
hence thesis by A5;
end;
then
A8: Sum abs R1 < Sum R2 by A7,RVSUM_1:83;
|.Sum R1.| <= Sum abs R1 by Th21;
hence thesis by A3,A8,XXREAL_0:2;
end;
registration
let n;
cluster Euclid n -> real-functions-membered;
coherence;
end;
theorem
for V being add-associative right_zeroed
right_complementable non empty addLoopStr, v,u being Element of V
holds v + u - u = v
proof
let V be add-associative right_zeroed
right_complementable non empty addLoopStr, v,u be Element of V;
thus v + u - u = v + (u-u) by RLVECT_1:28
.= v + 0.V by RLVECT_1:5
.= v;
end;
theorem
for V being Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, v,u being Element of V
holds v - u + u = v
proof
let V be Abelian add-associative right_zeroed
right_complementable non empty addLoopStr, v,u be Element of V;
thus v - u + u = v - (u-u) by RLVECT_1:29
.= v - 0.V by RLVECT_1:5
.= v;
end;
theorem Th29:
for Y being complex-functions-membered set, f being PartFunc of X,Y holds
f[+]c = f<+>(dom f-->c)
proof
let Y be complex-functions-membered set, f be PartFunc of X,Y;
set g = dom f-->c;
A1: dom (f[+]c) = dom f by VALUED_2:def 37;
A2: dom (f<+>g) = dom f /\ dom g by VALUED_2:def 41;
now
let x be object;
assume
A4: x in dom (f[+]c);
hence (f[+]c).x = f.x+c by VALUED_2:def 37
.= f.x+g.x by A1,A4,FUNCOP_1:7
.= (f<+>g).x by A1,A2,A4,VALUED_2:def 41;
end;
hence thesis by A1,A2;
end;
theorem
for Y being complex-functions-membered set, f being PartFunc of X,Y holds
f[-]c = f<->(dom f-->c)
proof
let Y be complex-functions-membered set, f be PartFunc of X,Y;
set g = dom f-->c;
A1: dom (f[-]c) = dom f by VALUED_2:def 37;
A2: dom (f<->g) = dom f /\ dom g by VALUED_2:61;
now
let x be object;
assume
A4: x in dom (f[-]c);
hence (f[-]c).x = f.x-c by VALUED_2:def 37
.= f.x-g.x by A1,A4,FUNCOP_1:7
.= (f<->g).x by A1,A2,A4,VALUED_2:62;
end;
hence thesis by A1,A2;
end;
theorem Th31:
for Y being complex-functions-membered set, f being PartFunc of X,Y holds
f[#]c = f<#>(dom f-->c)
proof
let Y be complex-functions-membered set, f be PartFunc of X,Y;
set g = dom f-->c;
A1: dom (f[#]c) = dom f by VALUED_2:def 39;
A2: dom (f<#>g) = dom f /\ dom g by VALUED_2:def 43;
now
let x be object;
assume
A4: x in dom (f[#]c);
hence (f[#]c).x = c(#)(f.x) by VALUED_2:def 39
.= (f.x)(#)(g.x) by A1,A4,FUNCOP_1:7
.= (f<#>g).x by A1,A2,A4,VALUED_2:def 43;
end;
hence thesis by A1,A2;
end;
theorem
for Y being complex-functions-membered set, f being PartFunc of X,Y holds
f[/]c = f</>(dom f-->c)
proof
let Y be complex-functions-membered set, f be PartFunc of X,Y;
set g = dom f-->c;
A1: dom (f[/]c) = dom f by VALUED_2:def 39;
A2: dom (f</>g) = dom f /\ dom g by VALUED_2:71;
now
let x be object;
assume
A4: x in dom (f[/]c);
hence (f[/]c).x = (f.x)(/)c by VALUED_2:56
.= (f.x)(/)(g.x) by A1,A4,FUNCOP_1:7
.= (f</>g).x by A1,A2,A4,VALUED_2:72;
end;
hence thesis by A1,A2;
end;
registration
let D be complex-functions-membered set;
let f, g be FinSequence of D;
cluster f<++>g -> FinSequence-like;
coherence
proof
dom(f<++>g) = dom f /\ dom g by VALUED_2:def 45;
hence thesis by VALUED_1:19;
end;
cluster f<-->g -> FinSequence-like;
coherence
proof
dom(f<-->g) = dom f /\ dom g by VALUED_2:def 46;
hence thesis by VALUED_1:19;
end;
cluster f<##>g -> FinSequence-like;
coherence
proof
dom(f<##>g) = dom f /\ dom g by VALUED_2:def 47;
hence thesis by VALUED_1:19;
end;
cluster f<//>g -> FinSequence-like;
coherence
proof
dom(f<//>g) = dom f /\ dom g by VALUED_2:def 48;
hence thesis by VALUED_1:19;
end;
end;
theorem
for f being Function of X,TOP-REAL n holds <->f is Function of X,TOP-REAL n
proof
let f be Function of X,TOP-REAL n;
set g = <->f;
A1: dom g = dom f by VALUED_2:def 33;
A2: dom f = X by FUNCT_2:def 1;
for x st x in X holds g.x in the carrier of TOP-REAL n
proof
let x;
assume
A3: x in X;
then reconsider X as non empty set;
reconsider x as Element of X by A3;
reconsider f as Function of X,TOP-REAL n;
A4: -((f.x) qua real-valued Function) = -f.x;
g.x = -((f.x) qua real-valued Function) by A1,A2,VALUED_2:def 33;
hence thesis by A4;
end;
hence thesis by A1,A2,FUNCT_2:3;
end;
theorem Th34:
for f being Function of TOP-REAL i,TOP-REAL n holds
f(-) is Function of TOP-REAL i,TOP-REAL n
proof
set X = the carrier of TOP-REAL i;
let f be Function of X,TOP-REAL n;
set g = f(-);
A1: dom g = dom f by VALUED_2:def 34;
A2: dom f = X by FUNCT_2:def 1;
for x st x in X holds g.x in the carrier of TOP-REAL n
proof
let x;
assume x in X;
then reconsider x as Element of X;
reconsider y = -x as Element of X;
reconsider f as Function of X,TOP-REAL n;
g.x = f.y by A1,A2,VALUED_2:def 34;
hence thesis;
end;
hence thesis by A1,A2,FUNCT_2:3;
end;
theorem Th35:
for f being Function of X,TOP-REAL n holds f[+]r is Function of X,TOP-REAL n
proof
let f be Function of X,TOP-REAL n;
set h = f[+]r;
dom f = X by FUNCT_2:def 1;
then A1: dom h = X by VALUED_2:def 37;
for x st x in X holds h.x in the carrier of TOP-REAL n
proof
let x;
assume
A2: x in X;
then reconsider X as non empty set;
reconsider x as Element of X by A2;
reconsider f as Function of X,TOP-REAL n;
A3: ((f.x) qua real-valued Function)+r = f.x+r;
h.x = ((f.x) qua real-valued Function)+r by A1,VALUED_2:def 37;
hence thesis by A3;
end;
hence thesis by A1,FUNCT_2:3;
end;
theorem
for f being Function of X,TOP-REAL n holds
f[-]r is Function of X,TOP-REAL n by Th35;
theorem Th37:
for f being Function of X,TOP-REAL n holds f[#]r is Function of X,TOP-REAL n
proof
let f be Function of X,TOP-REAL n;
set h = f[#]r;
dom f = X by FUNCT_2:def 1;
then A1: dom h = X by VALUED_2:def 39;
for x st x in X holds h.x in the carrier of TOP-REAL n
proof
let x;
assume
A2: x in X;
then reconsider X as non empty set;
reconsider x as Element of X by A2;
reconsider f as Function of X,TOP-REAL n;
A3: ((f.x) qua real-valued Function)(#)r = f.x(#)r;
h.x = ((f.x) qua real-valued Function)(#)r by A1,VALUED_2:def 39;
hence thesis by A3;
end;
hence thesis by A1,FUNCT_2:3;
end;
theorem
for f being Function of X,TOP-REAL n holds
f[/]r is Function of X,TOP-REAL n by Th37;
theorem Th39:
for f, g being Function of X,TOP-REAL n holds
f<++>g is Function of X,TOP-REAL n
proof
let f, g be Function of X,TOP-REAL n;
set h = f<++>g;
A1: dom f = X by FUNCT_2:def 1;
dom g = X by FUNCT_2:def 1;
then A2: dom h = X by A1,VALUED_2:def 45;
for x st x in X holds h.x in the carrier of TOP-REAL n
proof
let x;
assume
A3: x in X;
then reconsider X as non empty set;
reconsider x as Element of X by A3;
reconsider f, g as Function of X,TOP-REAL n;
A4: ((f.x) qua real-valued Function)+g.x = f.x+g.x;
h.x = ((f.x) qua real-valued Function)+g.x by A2,VALUED_2:def 45;
hence thesis by A4;
end;
hence thesis by A2,FUNCT_2:3;
end;
theorem Th40:
for f, g being Function of X,TOP-REAL n holds
f<-->g is Function of X,TOP-REAL n
proof
let f, g be Function of X,TOP-REAL n;
set h = f<-->g;
A1: dom f = X by FUNCT_2:def 1;
dom g = X by FUNCT_2:def 1;
then A2: dom h = X by A1,VALUED_2:def 46;
for x st x in X holds h.x in the carrier of TOP-REAL n
proof
let x;
assume
A3: x in X;
then reconsider X as non empty set;
reconsider x as Element of X by A3;
reconsider f, g as Function of X,TOP-REAL n;
A4: ((f.x) qua real-valued Function)-g.x = f.x-g.x;
h.x = ((f.x) qua real-valued Function)-g.x by A2,VALUED_2:def 46;
hence thesis by A4;
end;
hence thesis by A2,FUNCT_2:3;
end;
theorem Th41:
for f, g being Function of X,TOP-REAL n holds
f<##>g is Function of X,TOP-REAL n
proof
let f, g be Function of X,TOP-REAL n;
set h = f<##>g;
A1: dom f = X by FUNCT_2:def 1;
dom g = X by FUNCT_2:def 1;
then A2: dom h = X by A1,VALUED_2:def 47;
for x st x in X holds h.x in the carrier of TOP-REAL n
proof
let x;
assume
A3: x in X;
then reconsider X as non empty set;
reconsider x as Element of X by A3;
reconsider f, g as Function of X,TOP-REAL n;
h.x = f.x(#)g.x by A2,VALUED_2:def 47;
hence thesis;
end;
hence thesis by A2,FUNCT_2:3;
end;
theorem Th42:
for f, g being Function of X,TOP-REAL n holds
f<//>g is Function of X,TOP-REAL n
proof
let f, g be Function of X,TOP-REAL n;
set h = f<//>g;
A1: dom f = X by FUNCT_2:def 1;
dom g = X by FUNCT_2:def 1;
then A2: dom h = X by A1,VALUED_2:def 48;
for x st x in X holds h.x in the carrier of TOP-REAL n
proof
let x;
assume
A3: x in X;
then reconsider X as non empty set;
reconsider x as Element of X by A3;
reconsider f, g as Function of X,TOP-REAL n;
h.x = f.x /" g.x by A2,VALUED_2:def 48;
hence thesis;
end;
hence thesis by A2,FUNCT_2:3;
end;
theorem Th43:
for f being Function of X,TOP-REAL n, g being Function of X,R^1 holds
f<+>g is Function of X,TOP-REAL n
proof
let f be Function of X,TOP-REAL n, g be Function of X,R^1;
set h = f<+>g;
A1: dom f = X by FUNCT_2:def 1;
dom g = X by FUNCT_2:def 1;
then A2: dom h = X by A1,VALUED_2:def 41;
for x st x in X holds h.x in the carrier of TOP-REAL n
proof
let x;
assume
A3: x in X;
then reconsider X as non empty set;
reconsider x as Element of X by A3;
reconsider f as Function of X,TOP-REAL n;
h.x = f.x+g.x by A2,VALUED_2:def 41;
hence thesis;
end;
hence thesis by A2,FUNCT_2:3;
end;
theorem Th44:
for f being Function of X,TOP-REAL n, g being Function of X,R^1 holds
f<->g is Function of X,TOP-REAL n
proof
let f be Function of X,TOP-REAL n, g be Function of X,R^1;
set h = f<->g;
A1: dom f = X by FUNCT_2:def 1;
dom g = X by FUNCT_2:def 1;
then A2: dom h = X by A1,VALUED_2:61;
for x st x in X holds h.x in the carrier of TOP-REAL n
proof
let x;
assume
A3: x in X;
then reconsider X as non empty set;
reconsider x as Element of X by A3;
reconsider f as Function of X,TOP-REAL n;
h.x = f.x-g.x by A2,VALUED_2:62;
hence thesis;
end;
hence thesis by A2,FUNCT_2:3;
end;
theorem Th45:
for f being Function of X,TOP-REAL n, g being Function of X,R^1 holds
f<#>g is Function of X,TOP-REAL n
proof
let f be Function of X,TOP-REAL n, g be Function of X,R^1;
set h = f<#>g;
A1: dom f = X by FUNCT_2:def 1;
dom g = X by FUNCT_2:def 1;
then A2: dom h = X by A1,VALUED_2:def 43;
for x st x in X holds h.x in the carrier of TOP-REAL n
proof
let x;
assume
A3: x in X;
then reconsider X as non empty set;
reconsider x as Element of X by A3;
reconsider f as Function of X,TOP-REAL n;
h.x = f.x(#)g.x by A2,VALUED_2:def 43;
hence thesis;
end;
hence thesis by A2,FUNCT_2:3;
end;
theorem Th46:
for f being Function of X,TOP-REAL n, g being Function of X,R^1 holds
f</>g is Function of X,TOP-REAL n
proof
let f be Function of X,TOP-REAL n, g be Function of X,R^1;
set h = f</>g;
A1: dom f = X by FUNCT_2:def 1;
dom g = X by FUNCT_2:def 1;
then A2: dom h = X by A1,VALUED_2:71;
for x st x in X holds h.x in the carrier of TOP-REAL n
proof
let x;
assume
A3: x in X;
then reconsider X as non empty set;
reconsider x as Element of X by A3;
reconsider f as Function of X,TOP-REAL n;
h.x = f.x(/)g.x by A2,VALUED_2:72;
hence thesis;
end;
hence thesis by A2,FUNCT_2:3;
end;
definition
let n be Nat;
let T be non empty set;
let R be real-membered set;
let f be Function of T,R;
func incl(f,n) -> Function of T,TOP-REAL n means
:Def4:
for t being Element of T holds it.t = n |-> f.t;
existence
proof
defpred P[set,set] means $2 = n |-> f.$1;
A1: for x being Element of T ex y being Element of TOP-REAL n st P[x,y]
proof
let x be Element of T;
f.x in REAL by XREAL_0:def 1;
then n |-> f.x is Element of REAL n by FINSEQ_2:112;
then reconsider y = n |-> f.x as Point of TOP-REAL n by EUCLID:22;
take y;
thus thesis;
end;
ex F being Function of T,TOP-REAL n st
for x being Element of T holds P[x,F.x] from FUNCT_2:sch 3(A1);
hence thesis;
end;
uniqueness
proof
let F, G be Function of T,TOP-REAL n such that
A2: for t being Element of T holds F.t = n |-> f.t and
A3: for t being Element of T holds G.t = n |-> f.t;
let t be Element of T;
thus F.t = n |-> f.t by A2
.= G.t by A3;
end;
end;
theorem Th47:
for R being real-membered set for f being Function of T,R, t being Point of T
st x in Seg n holds incl(f,n).t.x = f.t
proof
let R be real-membered set;
let f be Function of T,R;
let t be Point of T;
assume
A1: x in Seg n;
thus incl(f,n).t.x = (n |-> f.t).x by Def4
.= f.t by A1,FINSEQ_2:57;
end;
theorem Th48:
for T being non empty set, R being real-membered set, f being Function of T,R
holds incl(f,0) = T --> 0
proof
let T be non empty set;
let R be real-membered set;
let f be Function of T,R;
reconsider z = 0 as Element of TOP-REAL 0;
incl(f,0) = T --> z
proof
let x be Element of T;
thus incl(f,0).x = (T --> z).x;
end;
hence thesis;
end;
theorem Th49:
for f being Function of T,TOP-REAL n, g being Function of T,R^1 holds
f<+>g = f<++>incl(g,n)
proof
let f be Function of T,TOP-REAL n;
let g be Function of T,R^1;
set I = incl(g,n);
reconsider h = f<+>g as Function of T,TOP-REAL n by Th43;
reconsider G = f<++>I as Function of T,TOP-REAL n by Th39;
h = G
proof
let t be Point of T;
A1: dom h = the carrier of T by FUNCT_2:def 1;
A2: f.t + I.t = f.t + g.t
proof
A3: dom (f.t) = Seg n & dom (I.t) = Seg n by FINSEQ_1:89;
A4: dom (f.t + I.t) = dom (f.t) /\ dom (I.t) by VALUED_1:def 1
.= Seg n by A3;
A5: dom (f.t + g.t) = dom (f.t) by VALUED_1:def 2;
thus dom (f.t + I.t) = dom (f.t + g.t) by A4,FINSEQ_1:89;
let x be object;
assume
A6: x in dom (f.t + I.t);
hence (f.t + I.t).x = f.t.x + I.t.x by VALUED_1:def 1
.= f.t.x + g.t by A4,A6,Th47
.= (f.t + g.t).x by A3,A4,A6,A5,VALUED_1:def 2;
end;
dom G = the carrier of T by FUNCT_2:def 1;
hence G.t = f.t + I.t by VALUED_2:def 45
.= h.t by A1,A2,VALUED_2:def 41;
end;
hence thesis;
end;
theorem Th50:
for f being Function of T,TOP-REAL n, g being Function of T,R^1 holds
f<->g = f<-->incl(g,n)
proof
let f be Function of T,TOP-REAL n;
let g be Function of T,R^1;
set I = incl(g,n);
reconsider h = f<->g as Function of T,TOP-REAL n by Th44;
reconsider G = f<-->I as Function of T,TOP-REAL n by Th40;
h = G
proof
let t be Point of T;
A1: dom h = the carrier of T by FUNCT_2:def 1;
A2: f.t - I.t = f.t - g.t
proof
A3: dom (f.t) = Seg n & dom (I.t) = Seg n by FINSEQ_1:89;
A4: dom (f.t - I.t) = dom (f.t) /\ dom (I.t) by VALUED_1:12
.= Seg n by A3;
A5: dom (f.t - g.t) = dom (f.t) by VALUED_1:def 2;
thus dom (f.t - I.t) = dom (f.t - g.t) by A4,FINSEQ_1:89;
let x be object;
assume
A6: x in dom (f.t - I.t);
hence (f.t - I.t).x = f.t.x - I.t.x by VALUED_1:13
.= f.t.x - g.t by A4,A6,Th47
.= (f.t - g.t).x by A3,A4,A6,A5,VALUED_1:def 2;
end;
dom G = the carrier of T by FUNCT_2:def 1;
hence G.t = f.t - I.t by VALUED_2:def 46
.= h.t by A1,A2,VALUED_2:62;
end;
hence thesis;
end;
theorem Th51:
for f being Function of T,TOP-REAL n, g being Function of T,R^1 holds
f<#>g = f<##>incl(g,n)
proof
let f be Function of T,TOP-REAL n;
let g be Function of T,R^1;
set I = incl(g,n);
reconsider h = f<#>g as Function of T,TOP-REAL n by Th45;
reconsider G = f<##>I as Function of T,TOP-REAL n by Th41;
h = G
proof
let t be Point of T;
A1: dom h = the carrier of T by FUNCT_2:def 1;
A2: f.t (#) I.t = f.t (#) g.t
proof
A3: dom (f.t) = Seg n & dom (I.t) = Seg n by FINSEQ_1:89;
A4: dom (f.t (#) I.t) = dom (f.t) /\ dom (I.t) by VALUED_1:def 4
.= Seg n by A3;
hence dom (f.t (#) I.t) = dom (f.t (#) g.t) by FINSEQ_1:89;
let x be object;
assume
A5: x in dom (f.t (#) I.t);
hence (f.t (#) I.t).x = f.t.x * I.t.x by VALUED_1:def 4
.= f.t.x * g.t by A4,A5,Th47
.= (f.t (#) g.t).x by VALUED_1:6;
end;
dom G = the carrier of T by FUNCT_2:def 1;
hence G.t = f.t (#) I.t by VALUED_2:def 47
.= h.t by A1,A2,VALUED_2:def 43;
end;
hence thesis;
end;
theorem
for f being Function of T,TOP-REAL n, g being Function of T,R^1 holds
f</>g = f<//>incl(g,n)
proof
let f be Function of T,TOP-REAL n;
let g be Function of T,R^1;
set I = incl(g,n);
reconsider h = f</>g as Function of T,TOP-REAL n by Th46;
reconsider G = f<//>I as Function of T,TOP-REAL n by Th42;
h = G
proof
let t be Point of T;
A1: dom h = the carrier of T by FUNCT_2:def 1;
A2: f.t /" I.t = f.t (#) (g".t)
proof
A3: dom (f.t) = Seg n & dom (I.t) = Seg n by FINSEQ_1:89;
A4: dom (f.t /" I.t) = dom (f.t) /\ dom (I.t) by VALUED_1:16
.= Seg n by A3;
hence dom (f.t /" I.t) = dom (f.t (#) g".t) by FINSEQ_1:89;
let x be object;
assume
A5: x in dom (f.t /" I.t);
thus (f.t /" I.t).x = f.t.x / I.t.x by VALUED_1:17
.= f.t.x / g.t by A4,A5,Th47
.= f.t.x * (g".t) by VALUED_1:10
.= (f.t (#) g".t).x by VALUED_1:6;
end;
dom G = the carrier of T by FUNCT_2:def 1;
hence G.t = f.t /" I.t by VALUED_2:def 48
.= h.t by A1,A2,VALUED_2:def 43;
end;
hence thesis;
end;
definition
let n;
set T = TOP-REAL n;
set c = the carrier of T;
A1: the carrier of [:T,T:] = [:c,c:] by BORSUK_1:def 2;
func TIMES(n) -> Function of [:TOP-REAL n,TOP-REAL n:],TOP-REAL n means
:Def5:
for x,y being Point of TOP-REAL n holds it.(x,y) = x(#)y;
existence
proof
deffunc F(Point of T,Point of T) = $1(#)$2;
ex f being Function of [:c,c:],c st
for x,y being Element of c holds f.(x,y) = F(x,y) from BINOP_1:sch 4;
hence thesis by A1;
end;
uniqueness
proof
let f,g be Function of [:T,T:],T such that
A2: for x,y being Point of T holds f.(x,y) = x(#)y and
A3: for x,y being Point of T holds g.(x,y) = x(#)y;
now
let x,y be Point of T;
thus f.(x,y) = x(#)y by A2
.= g.(x,y) by A3;
end;
hence thesis by A1,BINOP_1:2;
end;
end;
theorem Th53:
TIMES(0) = [:TOP-REAL 0,TOP-REAL 0:] --> 0.TOP-REAL 0
proof
set T = TOP-REAL 0;
let x be Element of the carrier of [:T,T:];
thus TIMES(0).x = ([:T,T:] --> 0.T).x;
end;
theorem Th54:
for f, g being Function of T,TOP-REAL n holds f <##> g = TIMES(n).:(f,g)
proof
set R = TOP-REAL n;
set F = TIMES(n);
let f, g be Function of T,R;
A1: dom(f<##>g) = dom f /\ dom g by VALUED_2:def 47;
dom F = the carrier of [:R,R:] by FUNCT_2:def 1
.= [:the carrier of R,the carrier of R:] by BORSUK_1:def 2;
then [:rng f, rng g:] c= dom F by ZFMISC_1:96;
then
A2: dom(F.:(f,g)) = dom f /\ dom g by FUNCOP_1:69;
now
let x be object;
assume
A3: x in dom (f<##>g);
then
A4: f.x is Point of R & g.x is Point of R by FUNCT_2:5;
thus (f<##>g).x = f.x(#)g.x by A3,VALUED_2:def 47
.= F.(f.x,g.x) by A4,Def5
.= F.:(f,g).x by A1,A2,A3,FUNCOP_1:22;
end;
hence thesis by A1,A2;
end;
definition
let m, n;
A1: m in NAT & n in NAT by ORDINAL1:def 12;
func PROJ(m,n) -> Function of TOP-REAL m,R^1 means
:Def6:
for p being Element of TOP-REAL m holds it.p = p/.n;
existence by A1,JORDAN2B:1;
uniqueness
proof
let F, G be Function of TOP-REAL m,R^1 such that
A2: for p being Element of TOP-REAL m holds F.p = p/.n and
A3: for p being Element of TOP-REAL m holds G.p = p/.n;
let p be Element of TOP-REAL m;
thus F.p = p/.n by A2
.= G.p by A3;
end;
end;
theorem Th55:
for p being Point of TOP-REAL m st n in dom p holds
PROJ(m,n).:Ball(p,r) = ]. p/.n-r , p/.n+r .[
proof
let p be Point of TOP-REAL m such that
A1: n in dom p;
per cases;
suppose
A2: r <= 0;
then ]. p/.n-r , p/.n+r .[ = {};
hence thesis by A2;
end;
suppose
A3: 0 < r;
A4: dom p = Seg m by FINSEQ_1:89;
thus PROJ(m,n).:Ball(p,r) c= ]. p/.n-r , p/.n+r .[
proof
let y be object;
assume y in PROJ(m,n).:Ball(p,r);
then consider x being Element of TOP-REAL m such that
A5: x in Ball(p,r) and
A6: y = PROJ(m,n).x by FUNCT_2:65;
A7: PROJ(m,n).x = x/.n by Def6;
A8: |.x-p.| < r by A5,TOPREAL9:7;
0 <= Sum sqr (x-p) by RVSUM_1:86;
then (sqrt Sum sqr (x-p))^2 = Sum sqr (x-p) by SQUARE_1:def 2;
then
A9: Sum sqr (x-p) < r^2 by A8,SQUARE_1:16;
dom x = Seg m by FINSEQ_1:89;
then (x/.n - p/.n)^2 <= Sum sqr (x-p) by A4,A1,EUCLID_9:8;
then (x/.n - p/.n)^2 < r^2 by A9,XXREAL_0:2;
then -r < x/.n - p/.n & x/.n - p/.n < r by A3,SQUARE_1:48;
then -r + p/.n < x/.n - p/.n + p/.n &
x/.n - p/.n + p/.n < r + p/.n by XREAL_1:6;
hence thesis by A6,A7,XXREAL_1:4;
end;
let y be object;
assume
A10: y in ]. p/.n-r , p/.n+r .[;
then reconsider y as Element of REAL;
set x = p+*(n,y);
reconsider X = x as FinSequence of REAL by EUCLID:24;
A11: dom X = dom p by FUNCT_7:30;
A12: p/.n = p.n by A1,PARTFUN1:def 6;
p/.n-r < y & y < p/.n+r by A10,XXREAL_1:4;
then
A13: y - p/.n < r & -r < y - p/.n by XREAL_1:19,20;
x-p = (0*m)+*(n,y-p.n) by Th17;
then |.x-p.| = |.y-p.n.| by A1,A4,Th13;
then |.x-p.| < r by A12,A13,SEQ_2:1;
then
A14: x in Ball(p,r) by TOPREAL9:7;
PROJ(m,n).x = x/.n by Def6
.= X.n by A11,A1,PARTFUN1:def 6
.= y by A1,FUNCT_7:31;
hence thesis by A14,FUNCT_2:35;
end;
end;
theorem
for m being non zero Nat for f being Function of T,R^1 holds
f = PROJ(m,m) * incl(f,m)
proof
let m be non zero Nat;
let f be Function of T,R^1;
let p be Point of T;
set I = incl(f,m);
reconsider G = m|->f.p as FinSequence of REAL;
1 <= m by NAT_1:14;
then
A1: m in Seg m;
A2: dom (m|->f.p) = Seg m;
thus (PROJ(m,m)*I).p = PROJ(m,m).(I.p) by FUNCT_2:15
.= I.p/.m by Def6
.= G/.m by Def4
.= G.m by A1,A2,PARTFUN1:def 6
.= f.p by A1,FINSEQ_2:57;
end;
begin :: Continuity
registration
let T;
cluster non-empty continuous for Function of T,R^1;
existence
proof
take T --> R^1(1);
thus thesis;
end;
end;
theorem
n in Seg m implies PROJ(m,n) is continuous
proof
assume
A1: n in Seg m;
A2: m in NAT by ORDINAL1:def 12;
for p being Element of TOP-REAL m holds PROJ(m,n).p = p/.n by Def6;
hence thesis by A2,A1,JORDAN2B:18;
end;
theorem
n in Seg m implies PROJ(m,n) is open
proof
set f = PROJ(m,n);
assume
A1: n in Seg m;
for p being Point of TOP-REAL m, r being positive Real holds
ex s being positive Real st ].f.p-s,f.p+s.[ c= f.:Ball(p,r)
proof
let p be Point of TOP-REAL m, r be positive Real;
take r;
A2: dom p = Seg m by FINSEQ_1:89;
p/.n = f.p by Def6;
hence thesis by A2,A1,Th55;
end;
hence thesis by TOPS_4:13;
end;
registration
let n,T;
let f be continuous Function of T,R^1;
cluster incl(f,n) -> continuous;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
set g = incl(f,n);
per cases;
suppose
A1: n = 0;
then reconsider z = 0 as Element of TOP-REAL n;
incl(f,0) = T --> z by Th48;
hence thesis by A1;
end;
suppose
A2: n > 0;
for p being Point of T, V being Subset of TOP-REAL n
st g.p in V & V is open holds
ex W being Subset of T st p in W & W is open & g.:W c= V
proof
let p be Point of T, V be Subset of TOP-REAL n;
assume that
A3: g.p in V and
A4: V is open;
A5: g.p in Int V by A3,A4,TOPS_1:23;
reconsider s = g.p as Point of Euclid n by EUCLID:67;
consider r being Real such that
A6: r > 0 and
A7: Ball(s,r) c= V by A5,GOBOARD6:5;
reconsider G = n|->f.p as FinSequence of REAL;
1 <= n by A2,NAT_1:14;
then
A8: n in Seg n;
reconsider F = g.p as FinSequence of REAL by EUCLID:24;
A9: F = n|->f.p by Def4;
A10: dom (n|->f.p) = Seg n;
A11: g.p/.n = G/.n by Def4
.= G.n by A8,A10,PARTFUN1:def 6
.= f.p by A8,FINSEQ_2:57;
set R = r/sqrt n;
set RR = R^1(].g.p/.n-r/sqrt n,g.p/.n+r/sqrt n.[);
f.p in RR by A2,A11,A6,TOPREAL6:15;
then consider W being Subset of T such that
A12: p in W & W is open and
A13: f.:W c= RR by JGRAPH_2:10;
take W;
thus p in W & W is open by A12;
let y be Element of TOP-REAL n;
assume y in g.:W;
then consider x being Element of T such that
A14: x in W and
A15: g.x = y by FUNCT_2:65;
reconsider y1 = y as Point of Euclid n by EUCLID:67;
reconsider y2 = y1, s2 = s as Element of REAL n;
A16: y2 = n|->f.x by A15,Def4;
A17: (Pitag_dist n).(y1,s) = |.y2-s2.| by EUCLID:def 6
.= (sqrt n) * |.f.x-f.p.| by A16,A9,Th11;
f.x in f.:W by A14,FUNCT_2:35;
then |.f.x-f.p.| < R by A13,A11,RCOMP_1:1;
then dist(y1,s) < r by A2,A17,XREAL_1:79;
then y in Ball(s,r) by METRIC_1:11;
hence thesis by A7;
end;
hence thesis by JGRAPH_2:10;
end;
end;
end;
registration
let n;
cluster TIMES(n) -> continuous;
coherence
proof
per cases;
suppose n is non zero;
then reconsider n as non zero Element of NAT by ORDINAL1:def 12;
set T = TOP-REAL n;
set F = TIMES(n);
set J = Seg n --> R^1;
set c = the carrier of T;
A1: TopSpaceMetr Euclid n = product(J) by EUCLID_9:28;
A2: the TopStruct of T = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider F as Function of [:T,T:], product J by EUCLID_9:28;
A3: the carrier of T = REAL n by EUCLID:22;
now
let i be Element of Seg n;
set P = proj(J,i);
reconsider f = P*F as Function of [:T,T:],R^1;
A5: the carrier of [:T,T:] = [:c,c:] by BORSUK_1:def 2;
A6: for a,b being Point of T holds f.(a,b) = a.i*b.i
proof
let a,b be Point of T;
thus f.(a,b) = P.(F.(a,b)) by A5,BINOP_1:18
.= P.(a(#)b) by Def5
.= (a(#)b).i by A1,A2,YELLOW17:8
.= a.i*b.i by VALUED_1:5;
end;
deffunc F1(Element of c,Element of c) = In($1.i,REAL);
consider f1 being Function of [:c,c:],REAL such that
A7: for a,b being Element of c holds f1.(a,b) = F1(a,b) from BINOP_1:sch 4;
reconsider f1 as Function of [:T,T:],R^1 by A5;
deffunc F2(Element of c,Element of c) = In($2.i,REAL);
consider f2 being Function of [:c,c:],REAL such that
A8: for a,b being Element of c holds f2.(a,b) = F2(a,b) from BINOP_1:sch 4;
reconsider f1,f2 as Function of [:T,T:],R^1 by A5;
for p being Point of [:T,T:], r being positive Real
ex W being open Subset of [:T,T:] st p in W &
f1.:W c= ].f1.p-r,f1.p+r.[
proof
let p be Point of [:T,T:], r be positive Real;
consider p1,p2 being Point of T such that
A9: p = [p1,p2] by BORSUK_1:10;
set B1 = Ball(p1,r), B2 = [#]T;
reconsider W = [:B1,B2:] as open Subset of [:T,T:] by BORSUK_1:6;
take W;
p1 in B1 & p2 in B2 by TOPGEN_5:13;
hence p in W by A9,ZFMISC_1:def 2;
let y be object;
assume y in f1.:W;
then consider x being Point of [:T,T:] such that
A10: x in W and
A11: f1.x = y by FUNCT_2:65;
consider x1,x2 being Point of T such that
A12: x = [x1,x2] by BORSUK_1:10;
A13: f1.(x1,x2) = F1(x1,x2) & f1.(p1,p2) = F1(p1,p2) by A7;
x1 in B1 by A10,A12,ZFMISC_1:87;
then
A14: |.x1-p1.| < r by TOPREAL9:7;
dom(x1-p1) = Seg n by FINSEQ_1:89;
then x1.i-p1.i = (x1-p1).i by VALUED_1:13;
then |.x1.i - p1.i.| <= |.x1-p1.| by A3,REAL_NS1:8;
then |.f1.x-f1.p.| < r by A9,A12,A13,A14,XXREAL_0:2;
hence y in ].f1.p-r,f1.p+r.[ by A11,RCOMP_1:1;
end;
then
A15: f1 is continuous by TOPS_4:21;
for p being Point of [:T,T:], r being positive Real
ex W being open Subset of [:T,T:] st p in W &
f2.:W c= ].f2.p-r,f2.p+r.[
proof
let p be Point of [:T,T:], r be positive Real;
consider p1,p2 being Point of T such that
A16: p = [p1,p2] by BORSUK_1:10;
set B1 = [#]T, B2 = Ball(p2,r);
reconsider W = [:B1,B2:] as open Subset of [:T,T:] by BORSUK_1:6;
take W;
p1 in B1 & p2 in B2 by TOPGEN_5:13;
hence p in W by A16,ZFMISC_1:def 2;
let y be object;
assume y in f2.:W;
then consider x being Point of [:T,T:] such that
A17: x in W and
A18: f2.x = y by FUNCT_2:65;
consider x1,x2 being Point of T such that
A19: x = [x1,x2] by BORSUK_1:10;
A20: f2.(x1,x2) = F2(x1,x2) & f2.(p1,p2) = F2(p1,p2) by A8;
x2 in B2 by A17,A19,ZFMISC_1:87;
then
A21: |.x2-p2.| < r by TOPREAL9:7;
dom(x2-p2) = Seg n by FINSEQ_1:89;
then x2.i-p2.i = (x2-p2).i by VALUED_1:13;
then |.x2.i - p2.i.| <= |.x2-p2.| by A3,REAL_NS1:8;
then |.f2.x-f2.p.| < r by A16,A19,A20,A21,XXREAL_0:2;
hence y in ].f2.p-r,f2.p+r.[ by A18,RCOMP_1:1;
end;
then f2 is continuous by TOPS_4:21;
then consider g being Function of [:T,T:],R^1 such that
A22: for p being Point of [:T,T:], r1,r2 being Real st
f1.p = r1 & f2.p = r2 holds g.p = r1*r2 and
A23: g is continuous by A15,JGRAPH_2:25;
now
let a, b be Point of T;
A24: f1.(a,b) = F1(a,b) & f2.(a,b) = F2(a,b) by A7,A8;
thus f.(a,b) = a.i*b.i by A6
.= g. [a,b] by A22,A24
.= g.(a,b);
end;
hence P*F is continuous by A23,A5,BINOP_1:2;
end;
then F is continuous by WAYBEL18:6;
hence thesis by A1,A2,YELLOW12:36;
end;
suppose n is zero;
then n = 0;
hence thesis by Th53;
end;
end;
end;
theorem
for f being Function of TOP-REAL m,TOP-REAL n st f is continuous holds
f(-) is continuous Function of TOP-REAL m,TOP-REAL n
proof
let f be Function of TOP-REAL m,TOP-REAL n;
assume
A1: f is continuous;
reconsider g = f(-) as Function of TOP-REAL m,TOP-REAL n by Th34;
for p being Point of TOP-REAL m, r being positive Real
ex s being positive Real st g.:Ball(p,s) c= Ball(g.p,r)
proof
let p be Point of TOP-REAL m;
let r be positive Real;
consider s being positive Real such that
A2: f.:Ball(-p,s) c= Ball(f.-p,r) by A1,TOPS_4:20;
take s;
let y be Element of TOP-REAL n;
assume y in g.:Ball(p,s);
then consider x being Element of TOP-REAL m such that
A3: x in Ball(p,s) and
A4: g.x = y by FUNCT_2:65;
dom g = the carrier of TOP-REAL m by FUNCT_2:def 1;
then
A5: g.x = f.-x & g.p = f.-p by VALUED_2:def 34;
-x in Ball(-p,s) by A3,Th23;
then f.-x in f.:Ball(-p,s) by FUNCT_2:35;
hence y in Ball(g.p,r) by A2,A4,A5;
end;
hence thesis by TOPS_4:20;
end;
registration
let T; let f be continuous Function of T,R^1;
cluster -f -> continuous for Function of T,R^1;
coherence
proof
let F be Function of T,R^1 such that
A1: F = -f;
consider g being Function of T,R^1 such that
A2: for p being Point of T, r being Real st f.p = r holds g.p = -r and
A3: g is continuous by JGRAPH_4:8;
F = g
proof
let x be Point of T;
thus F.x = -(f.x) by A1,VALUED_1:8
.= g.x by A2;
end;
hence thesis by A3;
end;
end;
registration
let T; let f be non-empty continuous Function of T,R^1;
cluster f" -> continuous for Function of T,R^1;
coherence
proof
let F be Function of T,R^1 such that
A1: F = f";
dom f = the carrier of T by FUNCT_2:def 1;
then for q being Point of T holds f.q <> 0;
then consider g being Function of T,R^1 such that
A2: for p being Point of T, r being Real st f.p = r holds g.p = 1/r and
A3: g is continuous by JGRAPH_2:26;
F = g
proof
let x be Point of T;
thus F.x = 1/(f.x) by A1,VALUED_1:10
.= g.x by A2;
end;
hence thesis by A3;
end;
end;
registration
let T; let f be continuous Function of T,R^1; let r;
cluster f+r -> continuous for Function of T,R^1;
coherence
proof
let F be Function of T,R^1 such that
A1: F = f+r;
consider g being Function of T,R^1 such that
A2: for p being Point of T, s being Real st f.p = s holds g.p = s + r
and
A3: g is continuous by JGRAPH_2:24;
F = g
proof
let x be Point of T;
thus F.x = (f.x)+r by A1,VALUED_1:2
.= g.x by A2;
end;
hence thesis by A3;
end;
cluster f-r -> continuous for Function of T,R^1;
coherence;
cluster f(#)r -> continuous for Function of T,R^1;
coherence
proof
let F be Function of T,R^1 such that
A4: F = f(#)r;
consider g being Function of T,R^1 such that
A5: for p being Point of T, s being Real st f.p = s holds g.p = r*s and
A6: g is continuous by JGRAPH_2:23;
F = g
proof
let x be Point of T;
thus F.x = (f.x)*r by A4,VALUED_1:6
.= g.x by A5;
end;
hence thesis by A6;
end;
cluster f(/)r -> continuous for Function of T,R^1;
coherence;
end;
registration
let T; let f, g be continuous Function of T,R^1;
cluster f+g -> continuous for Function of T,R^1;
coherence
proof
let F be Function of T,R^1 such that
A1: F = f+g;
consider h being Function of T,R^1 such that
A2: for p being Point of T, r1,r2 being Real st f.p = r1 & g.p = r2
holds h.p = r1 + r2
and
A3: h is continuous by JGRAPH_2:19;
F = h
proof
let x be Point of T;
thus F.x = (f.x)+(g.x) by A1,VALUED_1:1
.= h.x by A2;
end;
hence thesis by A3;
end;
cluster f-g -> continuous for Function of T,R^1;
coherence
proof
f-g = f+-g;
hence thesis;
end;
cluster f(#)g -> continuous for Function of T,R^1;
coherence
proof
let F be Function of T,R^1 such that
A4: F = f(#)g;
consider h being Function of T,R^1 such that
A5: for p being Point of T, r1,r2 being Real st f.p = r1 & g.p = r2
holds h.p = r1 * r2
and
A6: h is continuous by JGRAPH_2:25;
F = h
proof
let x be Point of T;
thus F.x = (f.x)*(g.x) by A4,VALUED_1:5
.= h.x by A5;
end;
hence thesis by A6;
end;
end;
registration
let T; let f be continuous Function of T,R^1;
let g be non-empty continuous Function of T,R^1;
cluster f /" g -> continuous for Function of T,R^1;
coherence
proof
f /" g = f(#)(g");
hence thesis;
end;
end;
registration
let n,T;
let f, g be continuous Function of T,TOP-REAL n;
cluster f<++>g -> continuous for Function of T,TOP-REAL n;
coherence
proof
let h be Function of T,TOP-REAL n such that
A1: h = f<++>g;
consider F being Function of T,TOP-REAL n such that
A2: for r being Point of T holds F.r = f.r + g.r and
A3: F is continuous by JGRAPH_6:12;
F = h
proof
A4: dom h = the carrier of T by FUNCT_2:def 1;
let x be Point of T;
thus F.x = f.x + g.x by A2
.= h.x by A1,A4,VALUED_2:def 45;
end;
hence thesis by A3;
end;
cluster f<-->g -> continuous for Function of T,TOP-REAL n;
coherence
proof
let h be Function of T,TOP-REAL n such that
A5: h = f<-->g;
A6: for r being Point of T holds h.r = f.r - g.r
proof
let r be Point of T;
dom h = the carrier of T by FUNCT_2:def 1;
hence thesis by A5,VALUED_2:def 46;
end;
for p being Point of T, V being Subset of TOP-REAL n
st h.p in V & V is open
ex W being Subset of T st p in W & W is open & h.:W c= V
proof
let p be Point of T, V be Subset of TOP-REAL n;
assume h.p in V & V is open;
then
A7: h.p in Int V by TOPS_1:23;
reconsider r=h.p as Point of Euclid n by EUCLID:67;
consider r0 being Real such that
A8: r0>0 & Ball(r,r0) c= V by A7,GOBOARD6:5;
reconsider r01 = f.p as Point of Euclid n by EUCLID:67;
reconsider G1 = Ball(r01,r0/2) as Subset of TOP-REAL n by EUCLID:67;
A9: f.p in G1 by A8,GOBOARD6:1;
A10: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
G1 is open by A10,TOPMETR:14,TOPS_3:76;
then consider W1 being Subset of T such that
A11: p in W1 & W1 is open & f.:W1 c= G1 by A9,JGRAPH_2:10;
reconsider r02 = g.p as Point of Euclid n by EUCLID:67;
reconsider G2 = Ball(r02,r0/2) as Subset of TOP-REAL n by EUCLID:67;
A12: g.p in G2 by A8,GOBOARD6:1;
G2 is open by A10,TOPMETR:14,TOPS_3:76;
then consider W2 being Subset of T such that
A13: p in W2 & W2 is open & g.:W2 c= G2 by A12,JGRAPH_2:10;
take W = W1 /\ W2;
thus p in W by A11,A13,XBOOLE_0:def 4;
thus W is open by A11,A13;
let x be Element of TOP-REAL n;
assume x in h.:W;
then consider z being object such that
A14: z in dom h & z in W & h.z=x by FUNCT_1:def 6;
A15: z in W1 by A14,XBOOLE_0:def 4;
reconsider pz=z as Point of T by A14;
dom f=the carrier of T by FUNCT_2:def 1;
then
A16: f.pz in f.:W1 by A15,FUNCT_1:def 6;
reconsider bb1=f.pz as Point of Euclid n by EUCLID:67;
dist(r01,bb1)<r0/2 by A11,A16,METRIC_1:11;
then
A17: |.f.p - f.pz .| < r0/2 by JGRAPH_1:28;
A18: z in W2 by A14,XBOOLE_0:def 4;
dom g=the carrier of T by FUNCT_2:def 1;
then
A19: g.pz in g.:W2 by A18,FUNCT_1:def 6;
reconsider bb2=g.pz as Point of Euclid n by EUCLID:67;
dist(r02,bb2)<r0/2 by A13,A19,METRIC_1:11;
then
A20: |.g.p - g.pz.| < r0/2 by JGRAPH_1:28;
A21: f.pz-g.pz = x by A6,A14;
reconsider bb0=f.pz-g.pz as Point of Euclid n by EUCLID:67;
A22: h.pz = f.pz-g.pz by A6;
(f.p-g.p)-(f.pz-g.pz)
= f.p-g.p-f.pz+g.pz by RLVECT_1:29
.= f.p+-g.p+-f.pz+g.pz
.= f.p+-f.pz+-g.p+g.pz by RLVECT_1:def 3
.= f.p-f.pz-g.p+g.pz
.= f.p-f.pz+g.pz+-g.p by RLVECT_1:def 3
.= f.p-f.pz+(g.pz-g.p) by RLVECT_1:def 3;
then
A23: |.(f.p-g.p)-(f.pz-g.pz).|
<= |.f.p-f.pz.| + |.g.pz-g.p.| by TOPRNS_1:29;
A24: |.g.p-g.pz.| = |.-(g.pz-g.p).| by RLVECT_1:33
.= |.g.pz-g.p.| by TOPRNS_1:26;
|.f.p-f.pz.| + |.g.p-g.pz.| < r0/2+r0/2 by A17,A20,XREAL_1:8;
then |.(f.p-g.p)-(f.pz-g.pz).| < r0 by A23,A24,XXREAL_0:2;
then |.h.p - h.pz .| < r0 by A6,A22;
then dist(r,bb0) < r0 by A14,A21,JGRAPH_1:28;
then x in Ball(r,r0) by A21,METRIC_1:11;
hence thesis by A8;
end;
hence thesis by JGRAPH_2:10;
end;
cluster f<##>g -> continuous for Function of T,TOP-REAL n;
coherence
proof
A25: f <##> g = TIMES(n).:(f,g) by Th54;
<:f,g:> is continuous Function of T,[:TOP-REAL n,TOP-REAL n:]
by YELLOW12:41;
hence thesis by A25;
end;
end;
registration
let n,T;
let f be continuous Function of T,TOP-REAL n;
let g be continuous Function of T,R^1;
set I = incl(g,n);
cluster f<+>g -> continuous for Function of T,TOP-REAL n;
coherence
proof
let h be Function of T,TOP-REAL n;
assume
A1: h = f<+>g;
reconsider G = f<++>I as Function of T,TOP-REAL n by Th39;
h = G by A1,Th49;
hence thesis;
end;
cluster f<->g -> continuous for Function of T,TOP-REAL n;
coherence
proof
let h be Function of T,TOP-REAL n;
assume
A2: h = f<->g;
reconsider G = f<-->I as Function of T,TOP-REAL n by Th40;
h = G by A2,Th50;
hence thesis;
end;
cluster f<#>g -> continuous for Function of T,TOP-REAL n;
coherence
proof
let h be Function of T,TOP-REAL n;
assume
A3: h = f<#>g;
reconsider G = f<##>I as Function of T,TOP-REAL n by Th41;
h = G by A3,Th51;
hence thesis;
end;
end;
registration
let n,T;
let f be continuous Function of T,TOP-REAL n;
let g be non-empty continuous Function of T,R^1;
cluster f</>g -> continuous for Function of T,TOP-REAL n;
coherence
proof
let h be Function of T,TOP-REAL n;
reconsider g1 = g" as Function of T,R^1;
g1 is continuous;
hence thesis;
end;
end;
registration
let n,T,r;
let f be continuous Function of T,TOP-REAL n;
cluster f[+]r -> continuous for Function of T,TOP-REAL n;
coherence
proof
let h be Function of T,TOP-REAL n such that
A1: h = f[+]r;
reconsider r as Element of R^1 by XREAL_0:def 1;
dom f = the carrier of T by FUNCT_2:def 1;
then h = f<+>(T-->r) by A1,Th29;
hence thesis;
end;
cluster f[-]r -> continuous for Function of T,TOP-REAL n;
coherence;
cluster f[#]r -> continuous for Function of T,TOP-REAL n;
coherence
proof
let h be Function of T,TOP-REAL n such that
A2: h = f[#]r;
reconsider r as Element of R^1 by XREAL_0:def 1;
dom f = the carrier of T by FUNCT_2:def 1;
then h = f<#>(T-->r) by A2,Th31;
hence thesis;
end;
cluster f[/]r -> continuous for Function of T,TOP-REAL n;
coherence;
end;
theorem Th60:
for r being non negative Real
for n being non zero Nat, p being Point of Tcircle(0.TOP-REAL n,r)
holds -p is Point of Tcircle(0.TOP-REAL n,r)
proof
let r be non negative Real;
let n be non zero Nat;
let p be Point of Tcircle(0.TOP-REAL n,r);
reconsider p1 = p as Point of TOP-REAL n by PRE_TOPC:25;
n in NAT by ORDINAL1:def 12;
then
A1: the carrier of Tcircle(0.TOP-REAL n,r) = Sphere(0.TOP-REAL n,r)
by TOPREALB:9;
|. (-p1) - 0.TOP-REAL n .| = |. -p1 .|
.= |. p1 .| by EUCLID:71
.= |. p1 - 0.TOP-REAL n .|
.= r by A1,TOPREAL9:9;
hence thesis by A1,TOPREAL9:9;
end;
theorem Th61:
for r being non negative Real
for f being Function of Tcircle(0.TOP-REAL(n+1),r),TOP-REAL n holds
f(-) is Function of Tcircle(0.TOP-REAL(n+1),r),TOP-REAL n
proof
let r be non negative Real;
set X = the carrier of Tcircle(0.TOP-REAL(n+1),r);
let f be Function of X,TOP-REAL n;
set g = f(-);
A1: dom g = dom f by VALUED_2:def 34;
A2: dom f = X by FUNCT_2:def 1;
for x st x in X holds g.x in the carrier of TOP-REAL n
proof
let x;
assume x in X;
then reconsider x as Element of X;
reconsider y = -x as Element of X by Th60;
reconsider f as Function of X,TOP-REAL n;
g.x = f.y by A1,A2,VALUED_2:def 34;
hence thesis;
end;
hence thesis by A1,A2,FUNCT_2:3;
end;
definition
let n be Nat, r be non negative Real;
let X be Subset of Tcircle(0.TOP-REAL(n+1),r);
redefine func (-)X -> Subset of Tcircle(0.TOP-REAL(n+1),r); :: redefines (-) (TOPREALC, definition)
coherence
proof
set T = Tcircle(0.TOP-REAL(n+1),r);
(-)X c= the carrier of T
proof
let x be object;
assume
A1: x in (-)X;
then reconsider x as Element of (-)X;
-x in X by A1,Th24;
then --x is Point of T by Th60;
hence thesis;
end;
hence thesis;
end;
end;
registration
let m;
let r be non negative Real;
let X be open Subset of Tcircle(0.TOP-REAL(m+1),r);
cluster (-)X -> open for Subset of Tcircle(0.TOP-REAL(m+1),r);
coherence
proof
set T = Tcircle(0.TOP-REAL(m+1),r);
ex G being Subset of TOP-REAL(m+1) st G is open &
(-)X = G /\ the carrier of T
proof
consider G being Subset of TOP-REAL(m+1) such that
A1: G is open and
A2: X = G /\ the carrier of T by TSP_1:def 1;
take (-)G;
thus (-)G is open by A1;
thus (-)X c= ((-)G) /\ the carrier of T
proof
let x be object;
assume
A3: x in (-)X;
then reconsider x as Element of (-)X;
-x in X by A3,Th24;
then -x in G by A2,XBOOLE_0:def 4;
then x in (-)G by Th24;
hence thesis by A3,XBOOLE_0:def 4;
end;
let x be object;
assume
A4: x in ((-)G) /\ the carrier of T;
then reconsider x as Element of (-)G by XBOOLE_0:def 4;
x in (-)G by A4,XBOOLE_0:def 4;
then
A5: -x in G by Th24;
x in the carrier of T by A4,XBOOLE_0:def 4;
then -x is Point of T by Th60;
then -x in X by A2,A5,XBOOLE_0:def 4;
hence thesis by Th24;
end;
hence thesis by TSP_1:def 1;
end;
end;
theorem
for r being non negative Real
for f being continuous Function of Tcircle(0.TOP-REAL(m+1),r),TOP-REAL m
holds f(-) is continuous Function of Tcircle(0.TOP-REAL(m+1),r),TOP-REAL m
proof
let r be non negative Real;
set T = Tcircle(0.TOP-REAL(m+1),r);
let f be continuous Function of T,TOP-REAL m;
reconsider g = f(-) as Function of T,TOP-REAL m by Th61;
for p being Point of T, r being positive Real
ex W being open Subset of T st p in W & g.:W c= Ball(g.p,r)
proof
let p be Point of T;
let r be positive Real;
reconsider q = -p as Point of T by Th60;
consider W being open Subset of T such that
A1: q in W and
A2: f.:W c= Ball(f.q,r) by TOPS_4:18;
reconsider W1 = (-)W as open Subset of T;
take W1;
-q in W1 by A1,Def3;
hence p in W1;
let y be Element of TOP-REAL m;
assume y in g.:W1;
then consider x being Element of T such that
A3: x in W1 and
A4: g.x = y by FUNCT_2:65;
dom g = the carrier of T by FUNCT_2:def 1;
then
A5: g.x = f.-x & g.p = f.-p by VALUED_2:def 34;
-x in (-)W1 by A3,Def3;
then f.-x in f.:W by FUNCT_2:35;
hence y in Ball(g.p,r) by A2,A4,A5;
end;
hence thesis by TOPS_4:18;
end;