:: On Outside Fashoda Meet Theorem
:: by Yatsuka Nakamura
::
:: Received July 16, 2001
:: Copyright (c) 2001-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, XBOOLE_0, PRE_TOPC, FUNCT_1, SUBSET_1, RCOMP_1,
ORDINAL2, FUNCT_4, RELAT_1, STRUCT_0, TARSKI, EUCLID, METRIC_1, COMPLEX1,
ARYTM_1, ARYTM_3, SUPINF_2, MCART_1, CARD_1, JORDAN2C, FINSEQ_1, REAL_1,
XXREAL_0, PCOMPS_1, SQUARE_1, TOPMETR, XXREAL_1, FUNCOP_1, PARTFUN1,
BORSUK_1, JGRAPH_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XXREAL_0,
FUNCOP_1, FINSEQ_1, FINSEQ_2, NAT_1, DOMAIN_1, STRUCT_0, PRE_TOPC,
PCOMPS_1, TOPMETR, METRIC_1, RCOMP_1, SQUARE_1, PSCOMP_1, RLVECT_1,
EUCLID, FUNCT_4;
constructors FUNCT_4, REAL_1, SQUARE_1, RCOMP_1, MONOID_0, TOPMETR, PSCOMP_1,
PCOMPS_1, FUNCOP_1, FUNCSDOM, FINSEQOP, MEASURE6, NUMBERS, COMSEQ_2;
registrations RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1,
STRUCT_0, PRE_TOPC, BORSUK_1, MONOID_0, EUCLID, TOPMETR, PSCOMP_1,
TOPS_1, ORDINAL1, VALUED_0, PARTFUN3;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, SQUARE_1, EUCLID, STRUCT_0, XCMPLX_0;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, RELAT_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCT_4, TOPS_1, TOPS_2,
PARTFUN1, PRE_TOPC, REVROT_1, FINSEQ_2, FRECHET, TOPMETR, JORDAN6,
EUCLID, JGRAPH_1, SQUARE_1, TOPREAL3, JORDAN5A, PSCOMP_1, METRIC_1,
SPPOL_2, TSEP_1, XBOOLE_0, XBOOLE_1, XREAL_0, XCMPLX_0, XCMPLX_1,
FUNCOP_1, XREAL_1, XXREAL_0, XXREAL_1;
schemes FUNCT_2, CLASSES1;
begin
reserve T,T1,T2,S for non empty TopSpace;
theorem Th1: :: BORSUK_2:1
for f being Function of T1,S, g being Function of T2,S,F1,F2
being Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1=[#] T1 & F2
=[#] T2 & ([#] T1) \/ ([#] T2) = [#] T & F1 is closed & F2 is closed & f is
continuous & g is continuous & (for p be object st p in ([#] T1) /\ ([#] T2)
holds f.p = g.p ) ex h being Function of T,S st h = f+*g & h is continuous
proof
let f be Function of T1,S, g be Function of T2,S,F1,F2 being Subset of T;
assume that
A1: T1 is SubSpace of T and
A2: T2 is SubSpace of T and
A3: F1=[#] T1 and
A4: F2=[#] T2 and
A5: ([#] T1) \/ ([#] T2) = [#] T and
A6: F1 is closed and
A7: F2 is closed and
A8: f is continuous and
A9: g is continuous and
A10: for p be object st p in ([#] T1) /\ ([#] T2) holds f.p = g.p;
set h = f+*g;
A11: dom g = the carrier of T2 by FUNCT_2:def 1
.= [#] T2;
A12: dom f = the carrier of T1 by FUNCT_2:def 1
.= [#] T1;
then
A13: dom h = [#] T by A5,A11,FUNCT_4:def 1
.= the carrier of T;
rng h c= rng f \/ rng g by FUNCT_4:17;
then reconsider h as Function of T,S by A13,FUNCT_2:2,XBOOLE_1:1;
take h;
thus h = f+*g;
for P being Subset of S st P is closed holds h"P is closed
proof
let P be Subset of S;
set P3 = f"P, P4 = g"P;
[#] T1 c= [#] T by A5,XBOOLE_1:7;
then reconsider P1 = f"P as Subset of T by XBOOLE_1:1;
[#] T2 c= [#] T by A5,XBOOLE_1:7;
then reconsider P2 = g"P as Subset of T by XBOOLE_1:1;
A14: dom h = dom f \/ dom g by FUNCT_4:def 1;
A15: now
let x be object;
thus x in h"P /\ [#] T2 implies x in g"P
proof
assume
A16: x in h"P /\ [#] T2;
then x in h"P by XBOOLE_0:def 4;
then
A17: h.x in P by FUNCT_1:def 7;
g.x = h.x by A11,A16,FUNCT_4:13;
hence thesis by A11,A16,A17,FUNCT_1:def 7;
end;
assume
A18: x in g"P;
then
A19: x in dom g by FUNCT_1:def 7;
g.x in P by A18,FUNCT_1:def 7;
then
A20: h.x in P by A19,FUNCT_4:13;
x in dom h by A14,A19,XBOOLE_0:def 3;
then x in h"P by A20,FUNCT_1:def 7;
hence x in h"P /\ [#] T2 by A18,XBOOLE_0:def 4;
end;
A21: for x being set st x in [#] T1 holds h.x = f.x
proof
let x be set such that
A22: x in [#] T1;
now
per cases;
suppose
A23: x in [#] T2;
then x in [#] T1 /\ [#] T2 by A22,XBOOLE_0:def 4;
then f.x = g.x by A10;
hence thesis by A11,A23,FUNCT_4:13;
end;
suppose
not x in [#] T2;
hence thesis by A11,FUNCT_4:11;
end;
end;
hence thesis;
end;
now
let x be object;
thus x in h"P /\ [#] T1 implies x in f"P
proof
assume
A24: x in h"P /\ [#] T1;
then x in h"P by XBOOLE_0:def 4;
then
A25: h.x in P by FUNCT_1:def 7;
f.x = h.x by A21,A24;
hence thesis by A12,A24,A25,FUNCT_1:def 7;
end;
assume
A26: x in f"P;
then x in dom f by FUNCT_1:def 7;
then
A27: x in dom h by A14,XBOOLE_0:def 3;
f.x in P by A26,FUNCT_1:def 7;
then h.x in P by A21,A26;
then x in h"P by A27,FUNCT_1:def 7;
hence x in h"P /\ [#] T1 by A26,XBOOLE_0:def 4;
end;
then
A28: h"P /\ [#] T1 = f"P by TARSKI:2;
assume
A29: P is closed;
then P3 is closed by A8,PRE_TOPC:def 6;
then ex F01 being Subset of T st F01 is closed & P3=F01 /\ [#] T1 by A1,
PRE_TOPC:13;
then
A30: P1 is closed by A3,A6;
P4 is closed by A9,A29,PRE_TOPC:def 6;
then ex F02 being Subset of T st F02 is closed & P4=F02 /\ [#] T2 by A2,
PRE_TOPC:13;
then
A31: P2 is closed by A4,A7;
h"P = h"P /\ ([#] T1 \/ [#] T2) by A12,A11,A14,RELAT_1:132,XBOOLE_1:28
.= (h"P /\ [#](T1)) \/ (h"P /\ [#](T2)) by XBOOLE_1:23;
then h"P = f"P \/ g"P by A28,A15,TARSKI:2;
hence thesis by A30,A31;
end;
hence thesis by PRE_TOPC:def 6;
end;
theorem Th2:
for n being Element of NAT,q2 being Point of Euclid n, q being
Point of TOP-REAL n, r being Real st q=q2 holds Ball(q2,r) = {q3 where
q3 is Point of TOP-REAL n: |.q-q3.|<r}
proof
let n be Element of NAT,q2 be Point of (Euclid n), q be Point of TOP-REAL n,
r be Real;
assume
A1: q=q2;
A2: {q4 where q4 is Element of Euclid n: dist(q2,q4) < r} c= {q3 where q3 is
Point of TOP-REAL n: |.q-q3.|<r}
proof
let x be object;
assume x in {q4 where q4 is Element of Euclid n: dist(q2,q4) < r};
then consider q4 being Element of Euclid n such that
A3: q4=x & dist(q2,q4) < r;
reconsider q44=q4 as Point of TOP-REAL n by TOPREAL3:8;
dist(q2,q4)=|.q-q44.| by A1,JGRAPH_1:28;
hence thesis by A3;
end;
A4: {q3 where q3 is Point of TOP-REAL n: |.q-q3.|<r} c={q4 where q4 is
Element of Euclid n: dist(q2,q4) < r}
proof
let x be object;
assume x in {q3 where q3 is Point of TOP-REAL n: |.q-q3.|<r};
then consider q3 being Point of TOP-REAL n such that
A5: x=q3 & |.q-q3.|<r;
reconsider q34=q3 as Point of Euclid n by TOPREAL3:8;
dist(q2,q34)=|.q-q3.| by A1,JGRAPH_1:28;
hence thesis by A5;
end;
Ball(q2,r)= {q4 where q4 is Element of Euclid n: dist(q2,q4) < r} by
METRIC_1:17;
hence thesis by A2,A4;
end;
theorem Th3:
(0.TOP-REAL 2)`1=0 & (0.TOP-REAL 2)`2=0 by EUCLID:52,54;
theorem Th4:
1.REAL 2 = <* 1, 1 *> by FINSEQ_2:61;
theorem Th5:
(1.REAL 2)`1=1 & (1.REAL 2)`2=1 by Th4,EUCLID:52;
theorem Th6:
dom proj1=the carrier of TOP-REAL 2 & dom proj1=REAL 2
proof
thus dom proj1=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
hence thesis by EUCLID:22;
end;
theorem Th7:
dom proj2=the carrier of TOP-REAL 2 & dom proj2=REAL 2
proof
thus dom proj2=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
hence thesis by EUCLID:22;
end;
theorem Th8:
for p being Point of TOP-REAL 2 holds p=|[proj1.p,proj2.p]|
proof
let p be Point of TOP-REAL 2;
p=|[p`1,p`2]| & p`1=proj1.p by EUCLID:53,PSCOMP_1:def 5;
hence thesis by PSCOMP_1:def 6;
end;
theorem Th9:
for B being Subset of TOP-REAL 2 st B={0.TOP-REAL 2} holds B`<>
{} & (the carrier of TOP-REAL 2)\B<>{}
proof
let B be Subset of TOP-REAL 2;
assume
A1: B={0.TOP-REAL 2};
now
assume |[0,1]| in B;
then |[0,1]|`2=0 by A1,Th3,TARSKI:def 1;
hence contradiction by EUCLID:52;
end;
then |[0,1]| in (the carrier of TOP-REAL 2) \ B by XBOOLE_0:def 5;
hence thesis by SUBSET_1:def 4;
end;
theorem Th10: :: BORSUK_1:def 2
for X,Y being non empty TopSpace,f being Function of X,Y holds f
is continuous iff for p being Point of X,V being Subset of Y st f.p in V & V is
open holds ex W being Subset of X st p in W & W is open & f.:W c= V
proof
let X,Y be non empty TopSpace,f be Function of X,Y;
A1: [#]Y <> {};
A2: dom f=the carrier of X by FUNCT_2:def 1;
hereby
assume
A3: f is continuous;
thus for p being Point of X,V being Subset of Y st f.p in V & V is open
holds ex W being Subset of X st p in W & W is open & f.:W c= V
proof
let p be Point of X,V be Subset of Y;
assume f.p in V & V is open;
then
A4: f"V is open & p in f"V by A2,A1,A3,FUNCT_1:def 7,TOPS_2:43;
f.:(f"V) c= V by FUNCT_1:75;
hence thesis by A4;
end;
end;
assume
A5: for p being Point of X,V being Subset of Y st f.p in V & V is open
holds ex W being Subset of X st p in W & W is open & f.:W c= V;
for G being Subset of Y st G is open holds f"G is open
proof
let G be Subset of Y;
assume
A6: G is open;
for z being set holds z in f"G iff ex Q being Subset of X st Q is
open & Q c= f"G & z in Q
proof
let z be set;
now
assume
A7: z in f"G;
then reconsider p=z as Point of X;
f.z in G by A7,FUNCT_1:def 7;
then consider W being Subset of X such that
A8: p in W & W is open and
A9: f.:W c= G by A5,A6;
A10: W c= f"(f.:W) by A2,FUNCT_1:76;
f"(f.:W) c= f"G by A9,RELAT_1:143;
hence ex Q being Subset of X st Q is open & Q c= f"G & z in Q by A8,A10
,XBOOLE_1:1;
end;
hence thesis;
end;
hence thesis by TOPS_1:25;
end;
hence thesis by A1,TOPS_2:43;
end;
theorem Th11:
for p being Point of TOP-REAL 2, G being Subset of TOP-REAL 2 st
G is open & p in G ex r being Real st r>0 & {q where q is Point of
TOP-REAL 2: p`1-r<q`1 & q`1<p`1+r & p`2-r<q`2 & q`2<p`2+r} c= G
proof
let p be Point of TOP-REAL 2,G being Subset of TOP-REAL 2;
assume that
A1: G is open and
A2: p in G;
reconsider GG=G as Subset of the TopStruct of TOP-REAL 2;
reconsider q2=p as Point of Euclid 2 by TOPREAL3:8;
TopSpaceMetr Euclid 2 = the TopStruct of TOP-REAL 2 & GG is open by A1,
EUCLID:def 8,PRE_TOPC:30;
then consider r being Real such that
A3: r>0 and
A4: Ball(q2,r) c= GG by A2,TOPMETR:15;
set s=r/sqrt(2);
A5: Ball(q2,r)= {q3 where q3 is Point of TOP-REAL 2: |.p-q3.|<r} by Th2;
A6: {q where q is Point of TOP-REAL 2: p`1-s<q`1 & q`1<p`1+s & p`2-s<q`2 & q
`2<p`2+s} c= Ball(q2,r)
proof
let x be object;
assume x in {q where q is Point of TOP-REAL 2: p`1-s<q`1 & q`1<p`1+s & p
`2-s<q`2 & q`2<p`2+s};
then consider q being Point of TOP-REAL 2 such that
A7: q=x and
A8: p`1-s<q`1 and
A9: q`1<p`1+s and
A10: p`2-s<q`2 and
A11: q`2<p`2+s;
p`1+s-s>q`1-s by A9,XREAL_1:14;
then
A12: p`1-q`1>q`1+-s-q`1 by XREAL_1:14;
p`2+s-s>q`2-s by A11,XREAL_1:14;
then
A13: p`2-q`2>q`2+-s-q`2 by XREAL_1:14;
p`2-s+s<q`2+s by A10,XREAL_1:8;
then p`2-q`2<q`2+s-q`2 by XREAL_1:14;
then
A14: (p`2-q`2)^2<s^2 by A13,SQUARE_1:50;
s^2=r^2/(sqrt(2))^2 by XCMPLX_1:76
.=r^2/2 by SQUARE_1:def 2;
then
A15: s^2+s^2=r^2;
p`1-s+s<q`1+s by A8,XREAL_1:8;
then p`1-q`1<q`1+s-q`1 by XREAL_1:14;
then
A16: (p-q)`2=p`2-q`2 & (p`1-q`1)^2<s^2 by A12,SQUARE_1:50,TOPREAL3:3;
(|.p-q.|)^2=((p-q)`1)^2+((p-q)`2)^2 & (p-q)`1=p`1-q`1 by JGRAPH_1:29
,TOPREAL3:3;
then (|.p-q.|)^2<r^2 by A16,A14,A15,XREAL_1:8;
then |.p-q.|<r by A3,SQUARE_1:48;
hence thesis by A5,A7;
end;
s>0 by A3,XREAL_1:139;
hence thesis by A4,A6,XBOOLE_1:1;
end;
theorem Th12:
for X,Y,Z being non empty TopSpace, B being Subset of Y, C being
Subset of Z, f being Function of X,Y, h being Function of Y|B,Z|C st f is
continuous & h is continuous & rng f c= B & B<>{} & C<>{} holds ex g being
Function of X,Z st g is continuous & g=h*f
proof
let X,Y,Z be non empty TopSpace, B be Subset of Y, C be Subset of Z, f be
Function of X,Y, h be Function of Y|B,Z|C;
assume that
A1: f is continuous and
A2: h is continuous and
A3: rng f c= B and
A4: B<>{} and
A5: C<>{};
A6: the carrier of X=dom f by FUNCT_2:def 1;
the carrier of Y|B=[#](Y|B) .=B by PRE_TOPC:def 5;
then reconsider u=f as Function of X,Y|B by A3,A6,FUNCT_2:2;
reconsider V=B as non empty Subset of Y by A4;
Y|V is non empty;
then reconsider H=Y|B as non empty TopSpace;
reconsider F=C as non empty Subset of Z by A5;
reconsider k=u as Function of X,H;
Z|F is non empty;
then reconsider G=Z|C as non empty TopSpace;
reconsider j=h as Function of H,G;
A7: the carrier of (Z|C)=[#](Z|C) .=C by PRE_TOPC:def 5;
j*k is Function of X,G;
then reconsider v=h*u as Function of X,Z by A7,FUNCT_2:7;
u is continuous by A1,TOPMETR:6;
then v is continuous by A2,A4,A5,PRE_TOPC:26;
hence thesis;
end;
reserve p,q for Point of TOP-REAL 2;
definition
func Out_In_Sq -> Function of NonZero TOP-REAL 2, NonZero TOP-REAL 2 means
:
Def1: for
p being Point of TOP-REAL 2 st p<>0.TOP-REAL 2 holds ((p`2<=p`1 & -p
`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies it.p=|[1/p`1,p`2/p`1/p`1]|) & (not(p`2
<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies it.p=|[p`1/p`2/p`2,1/p`2]|);
existence
proof
reconsider BP= NonZero TOP-REAL 2 as non empty set by Th9;
defpred P[set,set] means (for p being Point of TOP-REAL 2 st p=$1 holds ((
p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)implies $2=|[1/p`1,p`2/p`1/p`1]|)
& (not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies $2=|[p`1/p`2/p`2,1
/p`2]|));
A1: for x being Element of BP ex y being Element of BP st P[x,y]
proof
let x be Element of BP;
reconsider q=x as Point of TOP-REAL 2 by TARSKI:def 3;
now
per cases;
case
A2: q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1;
now
assume |[1/q`1,q`2/q`1/q`1]| in {0.TOP-REAL 2};
then 0.TOP-REAL 2= |[1/q`1,q`2/q`1/q`1]| by TARSKI:def 1;
then 0=1/q`1 by Th3,EUCLID:52;
then
A3: 0=1/q`1*q`1;
now
per cases;
case
A4: q`1=0;
then q`2=0 by A2;
then q=0.TOP-REAL 2 by A4,EUCLID:53,54;
then q in {0.TOP-REAL 2} by TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5;
end;
case
q`1<>0;
hence contradiction by A3,XCMPLX_1:87;
end;
end;
hence contradiction;
end;
then reconsider r= |[1/q`1,q`2/q`1/q`1]| as Element of BP by
XBOOLE_0:def 5;
for p being Point of TOP-REAL 2 st p=x holds ((p`2<=p`1 & -p`1
<=p`2 or p`2>=p`1 & p`2<=-p`1)implies r=|[1/p`1,p`2/p`1/p`1]|) & (not(p`2<=p`1
& -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies r=|[p`1/p`2/p`2,1/p`2]|) by A2;
hence thesis;
end;
case
A5: not (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
now
assume |[q`1/q`2/q`2,1/q`2]| in {0.TOP-REAL 2};
then 0.TOP-REAL 2= |[q`1/q`2/q`2,1/q`2]| by TARSKI:def 1;
then (0.TOP-REAL 2)`2=1/q`2 by EUCLID:52;
then
A6: 0=1/q`2*q`2 by Th3;
q`2 <> 0 by A5;
hence contradiction by A6,XCMPLX_1:87;
end;
then reconsider r= |[q`1/q`2/q`2,1/q`2]| as Element of BP by
XBOOLE_0:def 5;
for p being Point of TOP-REAL 2 st p=x holds ((p`2<=p`1 & -p`1
<=p`2 or p`2>=p`1 & p`2<=-p`1)implies r=|[1/p`1,p`2/p`1/p`1]|) & (not(p`2<=p`1
& -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies r=|[p`1/p`2/p`2,1/p`2]|) by A5;
hence thesis;
end;
end;
hence thesis;
end;
ex h being Function of BP, BP st for x being Element of BP holds P[x,
h.x] from FUNCT_2:sch 3(A1);
then consider h being Function of BP, BP such that
A7: for x being Element of BP holds for p being Point of TOP-REAL 2
st p=x holds ((p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)implies h.x=|[1/p`1
,p`2/p`1/p`1]|) & (not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies h.
x=|[p`1/p`2/p`2,1/p`2]|);
for p being Point of TOP-REAL 2 st p<>0.TOP-REAL 2 holds ((p`2<=p`1 &
-p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)implies h.p=|[1/p`1,p`2/p`1/p`1]|) & (not(p`2
<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies h.p=|[p`1/p`2/p`2,1/p`2]|)
proof
let p be Point of TOP-REAL 2;
assume p<>0.TOP-REAL 2;
then not p in {0.TOP-REAL 2} by TARSKI:def 1;
then p in NonZero TOP-REAL 2 by XBOOLE_0:def 5;
hence thesis by A7;
end;
hence thesis;
end;
uniqueness
proof
let h1,h2 be Function of NonZero TOP-REAL 2, NonZero TOP-REAL 2;
assume that
A8: for p being Point of TOP-REAL 2 st p<>0.TOP-REAL 2 holds ((p`2<=p
`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)implies h1.p=|[1/p`1,p`2/p`1/p`1]|) & (
not(p `2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies h1.p=|[p`1/p`2/p`2,1
/p`2]| ) and
A9: for p being Point of TOP-REAL 2 st p<>0.TOP-REAL 2 holds ((p`2<=p
`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1)implies h2.p=|[1/p`1,p`2/p`1/p`1]|) & (
not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) implies h2.p=|[p`1/p`2/p`2,1/
p`2]|);
for x being object st x in NonZero TOP-REAL 2 holds h1.x=h2.x
proof
let x be object;
assume
A10: x in NonZero TOP-REAL 2;
then reconsider q=x as Point of TOP-REAL 2;
not q in {0.TOP-REAL 2} by A10,XBOOLE_0:def 5;
then
A11: q<>0.TOP-REAL 2 by TARSKI:def 1;
now
per cases;
case
A12: q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1;
then h1.q=|[1/q`1,q`2/q`1/q`1]| by A8,A11;
hence thesis by A9,A11,A12;
end;
case
A13: not (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then h1.q=|[q`1/q`2/q`2,1/q`2]| by A8,A11;
hence thesis by A9,A11,A13;
end;
end;
hence thesis;
end;
hence h1=h2 by FUNCT_2:12;
end;
end;
theorem Th13:
for p being Point of TOP-REAL 2 st not(p`2<=p`1 & -p`1<=p`2 or p
`2>=p`1 & p`2<=-p`1) holds p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2
proof
let p being Point of TOP-REAL 2;
A1: -p`1<p`2 implies --p`1>-p`2 by XREAL_1:24;
A2: -p`1>p`2 implies --p`1<-p`2 by XREAL_1:24;
assume not(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1);
hence thesis by A1,A2;
end;
theorem Th14:
for p being Point of TOP-REAL 2 st p<>0.TOP-REAL 2 holds ((p`1<=
p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2)implies Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2
]|) & (not (p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) implies Out_In_Sq.p=
|[1/p`1,p`2/p`1/p`1]|)
proof
let p be Point of TOP-REAL 2;
assume
A1: p<>0.TOP-REAL 2;
hereby
assume
A2: p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2;
now
per cases by A2;
case
A3: p`1<=p`2 & -p`2<=p`1;
now
assume
A4: p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1;
A5: now
per cases by A4;
case
p`2<=p`1 & -p`1<=p`2;
hence p`1=p`2 or p`1=-p`2 by A3,XXREAL_0:1;
end;
case
p`2>=p`1 & p`2<=-p`1;
then -p`2>=--p`1 by XREAL_1:24;
hence p`1=p`2 or p`1=-p`2 by A3,XXREAL_0:1;
end;
end;
now
per cases by A5;
case
A6: p`1=p`2;
then p`1<>0 by A1,EUCLID:53,54;
then p`1/p`2/p`2=1/p`1 by A6,XCMPLX_1:60;
hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,A4,A6,Def1;
end;
case
A7: p`1=-p`2;
then
A8: p`2<>0 by A1,EUCLID:53,54;
A9: p`1/p`2/p`2=(-(p`2/p`2))/p`2 by A7
.=(-1)/p`2 by A8,XCMPLX_1:60
.= 1/p`1 by A7,XCMPLX_1:192;
-p`1=p`2 by A7;
then 1/p`2= -(1/p`1) by XCMPLX_1:188
.=-(p`2/p`1/(-p`1)) by A7,A9,XCMPLX_1:192
.=--(p`2/p`1/p`1) by XCMPLX_1:188
.=p`2/p`1/p`1;
hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,A4,A9,Def1;
end;
end;
hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]|;
end;
hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,Def1;
end;
case
A10: p`1>=p`2 & p`1<=-p`2;
now
assume
A11: p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1;
A12: now
per cases by A11;
case
p`2<=p`1 & -p`1<=p`2;
then --p`1>=-p`2 by XREAL_1:24;
hence p`1=p`2 or p`1=-p`2 by A10,XXREAL_0:1;
end;
case
p`2>=p`1 & p`2<=-p`1;
hence p`1=p`2 or p`1=-p`2 by A10,XXREAL_0:1;
end;
end;
now
per cases by A12;
case
A13: p`1=p`2;
then p`1 <> 0 by A1,EUCLID:53,54;
then p`1/p`2/p`2=1/p`1 by A13,XCMPLX_1:60;
hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,A11,A13,Def1;
end;
case
A14: p`1=-p`2;
then
A15: p`2<>0 by A1,EUCLID:53,54;
A16: p`1/p`2/p`2 =(-(p`2/p`2))/p`2 by A14
.=(-1)/p`2 by A15,XCMPLX_1:60
.= 1/p`1 by A14,XCMPLX_1:192;
-p`1=p`2 by A14;
then 1/p`2=-(p`1/p`2/p`2) by A16,XCMPLX_1:188
.=-(p`2/p`1/(-p`1)) by A14,XCMPLX_1:191
.=--(p`2/p`1/p`1) by XCMPLX_1:188
.=p`2/p`1/p`1;
hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,A11,A16,Def1;
end;
end;
hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]|;
end;
hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by A1,Def1;
end;
end;
hence Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]|;
end;
hereby
A17: -p`2>p`1 implies --p`2<-p`1 by XREAL_1:24;
A18: -p`2<p`1 implies --p`2>-p`1 by XREAL_1:24;
assume not(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2);
hence Out_In_Sq.p=|[1/p`1,p`2/p`1/p`1]| by A1,A18,A17,Def1;
end;
end;
theorem Th15:
for D being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL 2
)|D st K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2}
holds rng (Out_In_Sq|K0) c= the carrier of ((TOP-REAL 2)|D)|K0
proof
let D be Subset of TOP-REAL 2, K0 be Subset of (TOP-REAL 2)|D;
A1: the carrier of ((TOP-REAL 2)|D) =[#]((TOP-REAL 2)|D)
.=D by PRE_TOPC:def 5;
then reconsider K00=K0 as Subset of TOP-REAL 2 by XBOOLE_1:1;
assume
A2: K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2};
A3: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K00
holds q`1<>0
proof
let q be Point of TOP-REAL 2;
A4: the carrier of (TOP-REAL 2)|K00=[#]((TOP-REAL 2)|K00)
.=K0 by PRE_TOPC:def 5;
assume q in the carrier of (TOP-REAL 2)|K00;
then
A5: ex p3 being Point of TOP-REAL 2 st q=p3 &( p3`2<=p3`1 & - p3`1<=p3`2
or p3`2>=p3`1 & p3`2<=-p3`1)& p3<>0.TOP-REAL 2 by A2,A4;
now
assume
A6: q`1=0;
then q`2=0 by A5;
hence contradiction by A5,A6,EUCLID:53,54;
end;
hence thesis;
end;
let y be object;
assume y in rng (Out_In_Sq|K0);
then consider x being object such that
A7: x in dom (Out_In_Sq|K0) and
A8: y=(Out_In_Sq|K0).x by FUNCT_1:def 3;
A9: x in (dom Out_In_Sq) /\ K0 by A7,RELAT_1:61;
then
A10: x in K0 by XBOOLE_0:def 4;
K0 c= the carrier of TOP-REAL 2 by A1,XBOOLE_1:1;
then reconsider p=x as Point of TOP-REAL 2 by A10;
A11: Out_In_Sq.p=y by A8,A10,FUNCT_1:49;
A12: ex px being Point of TOP-REAL 2 st x=px &( px`2<=px`1 & - px`1<=px`2 or
px`2>=px`1 & px`2<=-px`1)& px<>0.TOP-REAL 2 by A2,A10;
then
A13: Out_In_Sq.p=|[1/p`1,p`2/p`1/p`1]| by Def1;
set p9=|[1/p`1,p`2/p`1/p`1]|;
K00=[#]((TOP-REAL 2)|K00) by PRE_TOPC:def 5
.=the carrier of ((TOP-REAL 2)|K00);
then
A14: p in the carrier of ((TOP-REAL 2)|K00) by A9,XBOOLE_0:def 4;
A15: p9`1=1/p`1 by EUCLID:52;
A16: now
assume p9=0.TOP-REAL 2;
then 0 *p`1=1/p`1*p`1 by A15,EUCLID:52,54;
hence contradiction by A14,A3,XCMPLX_1:87;
end;
A17: p`1<>0 by A14,A3;
now
per cases;
suppose
A18: p`1>=0;
then p`2/p`1<=p`1/p`1 & (-1 *p`1)/p`1<=p`2/p`1 or p`2>=p`1 & p`2<=-1 *p
`1 by A12,XREAL_1:72;
then
A19: p`2/p`1<=1 & (-1)*p`1/p`1<=p`2/p`1 or p`2>=p`1 & p`2<=-1 *p`1 by A14,A3,
XCMPLX_1:60;
then p`2/p`1<=1 & -1<=p`2/p`1 or p`2/p`1>=1 & p`2/p`1<=(-1)*p`1/p`1 by
A17,A18,XCMPLX_1:89;
then (-1)/p`1<= p`2/p`1/p`1 by A18,XREAL_1:72;
then
A20: p`2/p`1/p`1 <=1/p`1 & -(1/p`1)<= p`2/p`1/p`1 or p`2/p`1/p`1 >=1/p`1
& p`2/p`1/p`1<= -(1/p`1) by A17,A18,A19,XREAL_1:72;
p9`1=1/p`1 & p9`2=p`2/p`1/p`1 by EUCLID:52;
hence y in K0 by A2,A11,A16,A13,A20;
end;
suppose
A21: p`1<0;
A22: now
per cases by A12;
case that
A23: p`2<=p`1 and
A24: (-1 *p`1)<=p`2;
p`2/p`1 >=1 by A21,A23,XREAL_1:182;
hence p`2/p`1/p`1 <=1/p`1 by A21,XREAL_1:73;
(-1) *p`1<=p`2 by A24;
then -1 >= p`2/p`1 by A21,XREAL_1:78;
then (-1)/p`1<= p`2/p`1/p`1 by A21,XREAL_1:73;
hence -(1/p`1)<= p`2/p`1/p`1;
end;
case that
A25: p`2>=p`1 and
A26: p`2<=-1 *p`1;
p`2/p`1 <=1 by A21,A25,XREAL_1:186;
hence p`2/p`1/p`1 >=1/p`1 by A21,XREAL_1:73;
(-1) *p`1>=p`2 by A26;
then -1 <= p`2/p`1 by A21,XREAL_1:80;
then (-1)/p`1>= p`2/p`1/p`1 by A21,XREAL_1:73;
hence -(1/p`1)>= p`2/p`1/p`1;
end;
end;
p9`1=1/p`1 & p9`2=p`2/p`1/p`1 by EUCLID:52;
hence y in K0 by A2,A11,A16,A13,A22;
end;
end;
then y in [#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 5;
hence thesis;
end;
theorem Th16:
for D being Subset of TOP-REAL 2, K0 being Subset of (TOP-REAL 2
)|D st K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2}
holds rng (Out_In_Sq|K0) c= the carrier of ((TOP-REAL 2)|D)|K0
proof
let D be Subset of TOP-REAL 2, K0 be Subset of (TOP-REAL 2)|D;
A1: the carrier of ((TOP-REAL 2)|D) =[#]((TOP-REAL 2)|D)
.=D by PRE_TOPC:def 5;
then reconsider K00=K0 as Subset of TOP-REAL 2 by XBOOLE_1:1;
assume
A2: K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2};
A3: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K00
holds q`2<>0
proof
let q be Point of TOP-REAL 2;
A4: the carrier of (TOP-REAL 2)|K00=[#]((TOP-REAL 2)|K00)
.=K0 by PRE_TOPC:def 5;
assume q in the carrier of (TOP-REAL 2)|K00;
then
A5: ex p3 being Point of TOP-REAL 2 st q=p3 &( p3`1<=p3`2 & - p3`2<=p3`1
or p3`1>=p3`2 & p3`1<=-p3`2)& p3<>0.TOP-REAL 2 by A2,A4;
now
assume
A6: q`2=0;
then q`1=0 by A5;
hence contradiction by A5,A6,EUCLID:53,54;
end;
hence thesis;
end;
let y be object;
assume y in rng (Out_In_Sq|K0);
then consider x being object such that
A7: x in dom (Out_In_Sq|K0) and
A8: y=(Out_In_Sq|K0).x by FUNCT_1:def 3;
x in (dom Out_In_Sq) /\ K0 by A7,RELAT_1:61;
then
A9: x in K0 by XBOOLE_0:def 4;
K0 c= the carrier of TOP-REAL 2 by A1,XBOOLE_1:1;
then reconsider p=x as Point of TOP-REAL 2 by A9;
A10: Out_In_Sq.p=y by A8,A9,FUNCT_1:49;
A11: ex px being Point of TOP-REAL 2 st x=px &( px`1<=px`2 & - px`2<=px`1 or
px`1>=px`2 & px`1<=-px`2)& px<>0.TOP-REAL 2 by A2,A9;
then
A12: Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by Th14;
A13: K00=[#]((TOP-REAL 2)|K00) by PRE_TOPC:def 5
.=the carrier of ((TOP-REAL 2)|K00);
set p9=|[p`1/p`2/p`2,1/p`2]|;
A14: p9`2=1/p`2 by EUCLID:52;
A15: now
assume p9=0.TOP-REAL 2;
then 0 *p`2=1/p`2*p`2 by A14,EUCLID:52,54;
hence contradiction by A9,A13,A3,XCMPLX_1:87;
end;
A16: p`2<>0 by A9,A13,A3;
now
per cases;
case
A17: p`2>=0;
then p`1/p`2<=p`2/p`2 & (-1 *p`2)/p`2<=p`1/p`2 or p`1>=p`2 & p`1<=-1 *p
`2 by A11,XREAL_1:72;
then
A18: p`1/p`2<=1 & (-1)*p`2/p`2<=p`1/p`2 or p`1>=p`2 & p`1<=-1 *p`2 by A9,A13
,A3,XCMPLX_1:60;
then p`1/p`2<=1 & -1<=p`1/p`2 or p`1/p`2>=1 & p`1/p`2<=(-1)*p`2/p`2 by
A16,A17,XCMPLX_1:89;
then (-1)/p`2<= p`1/p`2/p`2 by A17,XREAL_1:72;
then
A19: p`1/p`2/p`2 <=1/p`2 & -(1/p`2)<= p`1/p`2/p`2 or p`1/p`2/p`2 >=1/p`2
& p`1/p`2/p`2<= -(1/p`2) by A16,A17,A18,XREAL_1:72;
p9`2=1/p`2 & p9`1=p`1/p`2/p`2 by EUCLID:52;
hence y in K0 by A2,A10,A15,A12,A19;
end;
case
A20: p`2<0;
then
p`1<=p`2 & (-1 *p`2)<=p`1 or p`1/p`2<=p`2/p`2 & p`1/p`2>=(-1 *p`2)/
p`2 by A11,XREAL_1:73;
then
A21: p`1<=p`2 & (-1 *p`2)<=p`1 or p`1/p`2<=1 & p`1/p`2>=(-1)*p`2/p`2 by A20,
XCMPLX_1:60;
then p`1/p`2>=1 & (-1)*p`2/p`2>=p`1/p`2 or p`1/p`2<=1 & p`1/p`2>=-1 by
A20,XCMPLX_1:89;
then (-1)/p`2>= p`1/p`2/p`2 by A20,XREAL_1:73;
then
A22: p`1/p`2/p`2 <=1/p`2 & -(1/p`2)<= p`1/p`2/p`2 or p`1/p`2/p`2 >=1/p`2
& p`1/p`2/p`2<= -(1/p`2) by A20,A21,XREAL_1:73;
p9`2=1/p`2 & p9`1=p`1/p`2/p`2 by EUCLID:52;
hence y in K0 by A2,A10,A15,A12,A22;
end;
end;
then y in [#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 5;
hence thesis;
end;
Lm1: 0.TOP-REAL 2 = 0.REAL 2 by EUCLID:66;
theorem Th17:
for K0a being set,D being non empty Subset of TOP-REAL 2 st K0a=
{p where p is Point of TOP-REAL 2: (p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p
`1) & p<>0.TOP-REAL 2} & D`={0.TOP-REAL 2} holds K0a is non empty Subset of (
TOP-REAL 2)|D & K0a is non empty Subset of TOP-REAL 2
proof
A1: (1.REAL 2)<>0.TOP-REAL 2 by Lm1,REVROT_1:19;
let K0a be set,D be non empty Subset of TOP-REAL 2;
assume that
A2: K0a={p where p is Point of TOP-REAL 2: (p`2<=p`1 & -p`1<=p`2 or p`2
>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} and
A3: D`={0.TOP-REAL 2};
(1.REAL 2)`2<=(1.REAL 2)`1 & -(1.REAL 2)`1<=(1.REAL 2)`2 or (1.REAL 2)
`2>=(1.REAL 2)`1 & (1.REAL 2)`2<=-(1.REAL 2)`1 by Th5;
then
A4: 1.REAL 2 in K0a by A2,A1;
A5: K0a c= D
proof
let x be object;
A6: D=D`` .=NonZero TOP-REAL 2 by A3,SUBSET_1:def 4;
assume x in K0a;
then
A7: ex p8 being Point of TOP-REAL 2 st x=p8 &( p8`2<=p8`1 & - p8`1<=p8`2 or
p8`2>=p8`1 & p8`2<=-p8`1)& p8<>0.TOP-REAL 2 by A2;
then not x in {0.TOP-REAL 2} by TARSKI:def 1;
hence thesis by A7,A6,XBOOLE_0:def 5;
end;
the carrier of (TOP-REAL 2)|D=[#]((TOP-REAL 2)|D) .=D by PRE_TOPC:def 5;
hence K0a is non empty Subset of ((TOP-REAL 2)|D) by A4,A5;
thus thesis by A4,A5,XBOOLE_1:1;
end;
theorem Th18:
for K0a being set,D being non empty Subset of TOP-REAL 2 st K0a=
{p where p is Point of TOP-REAL 2: (p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p
`2) & p<>0.TOP-REAL 2} & D`={0.TOP-REAL 2} holds K0a is non empty Subset of (
TOP-REAL 2)|D & K0a is non empty Subset of TOP-REAL 2
proof
A1: (1.REAL 2)<>0.TOP-REAL 2 by Lm1,REVROT_1:19;
let K0a be set,D be non empty Subset of TOP-REAL 2;
assume that
A2: K0a={p where p is Point of TOP-REAL 2: (p`1<=p`2 & -p`2<=p`1 or p`1
>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} and
A3: D`={0.TOP-REAL 2};
(1.REAL 2)`1<=(1.REAL 2)`2 & -(1.REAL 2)`2<=(1.REAL 2)`1 or (1.REAL 2)
`1>=(1.REAL 2)`2 & (1.REAL 2)`1<=-(1.REAL 2)`2 by Th5;
then
A4: 1.REAL 2 in K0a by A2,A1;
A5: K0a c= D
proof
let x be object;
A6: D=D`` .=NonZero TOP-REAL 2 by A3,SUBSET_1:def 4;
assume x in K0a;
then
A7: ex p8 being Point of TOP-REAL 2 st x=p8 &( p8`1<=p8`2 & - p8`2<=p8`1 or
p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2 by A2;
then not x in {0.TOP-REAL 2} by TARSKI:def 1;
hence thesis by A7,A6,XBOOLE_0:def 5;
end;
the carrier of (TOP-REAL 2)|D=[#]((TOP-REAL 2)|D) .=D by PRE_TOPC:def 5;
hence K0a is non empty Subset of ((TOP-REAL 2)|D) by A4,A5;
thus thesis by A4,A5,XBOOLE_1:1;
end;
theorem Th19:
for X being non empty TopSpace, f1,f2 being Function of X,R^1 st
f1 is continuous & f2 is continuous holds ex g being Function of X,R^1 st (for
p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1+r2
) & g is continuous
proof
let X being non empty TopSpace,f1,f2 be Function of X,R^1;
assume that
A1: f1 is continuous and
A2: f2 is continuous;
defpred P[set,set] means (for r1,r2 being Real st f1.$1=r1 & f2.$1=r2
holds $2=r1+r2);
A3: for x being Element of X ex y being Element of REAL st P[x,y]
proof
let x be Element of X;
reconsider r1=f1.x as Element of REAL by TOPMETR:17;
reconsider r2=f2.x as Element of REAL by TOPMETR:17;
set r3=r1+r2;
for r1,r2 being Real st f1.x=r1 & f2.x=r2 holds r3=r1+r2;
hence ex y being Element of REAL st for r1,r2 being Real st f1.x=r1
& f2.x=r2 holds y=r1+r2;
end;
ex f being Function of the carrier of X,REAL st for x being Element of X
holds P[x,f.x] from FUNCT_2:sch 3(A3);
then consider f being Function of the carrier of X,REAL such that
A4: for x being Element of X holds for r1,r2 being Real st f1.x=
r1 & f2.x=r2 holds f.x=r1+r2;
reconsider g0=f as Function of X,R^1 by TOPMETR:17;
for p being Point of X,V being Subset of R^1 st g0.p in V & V is open
holds ex W being Subset of X st p in W & W is open & g0.:W c= V
proof
let p be Point of X,V be Subset of R^1;
reconsider r=g0.p as Real;
reconsider r1=f1.p as Real;
reconsider r2=f2.p as Real;
assume g0.p in V & V is open;
then consider r0 being Real such that
A5: r0>0 and
A6: ].r-r0,r+r0.[ c= V by FRECHET:8;
reconsider G1=].r1-r0/2,r1+r0/2.[ as Subset of R^1 by TOPMETR:17;
A7: r1<r1+r0/2 by A5,XREAL_1:29,215;
then r1-r0/2<r1 by XREAL_1:19;
then
A8: f1.p in G1 by A7,XXREAL_1:4;
reconsider G2=].r2-r0/2,r2+r0/2.[ as Subset of R^1 by TOPMETR:17;
A9: r2<r2+r0/2 by A5,XREAL_1:29,215;
then r2-r0/2<r2 by XREAL_1:19;
then
A10: f2.p in G2 by A9,XXREAL_1:4;
G2 is open by JORDAN6:35;
then consider W2 being Subset of X such that
A11: p in W2 & W2 is open and
A12: f2.:W2 c= G2 by A2,A10,Th10;
G1 is open by JORDAN6:35;
then consider W1 being Subset of X such that
A13: p in W1 & W1 is open and
A14: f1.:W1 c= G1 by A1,A8,Th10;
set W=W1 /\ W2;
A15: g0.:W c= ].r-r0,r+r0.[
proof
let x be object;
assume x in g0.:W;
then consider z being object such that
A16: z in dom g0 and
A17: z in W and
A18: g0.z=x by FUNCT_1:def 6;
reconsider pz=z as Point of X by A16;
reconsider aa2=f2.pz as Real;
reconsider aa1=f1.pz as Real;
A19: pz in the carrier of X;
then
A20: pz in dom f2 by FUNCT_2:def 1;
z in W2 by A17,XBOOLE_0:def 4;
then
A21: f2.pz in f2.:W2 by A20,FUNCT_1:def 6;
then
A22: r2-r0/2<aa2 by A12,XXREAL_1:4;
A23: pz in dom f1 by A19,FUNCT_2:def 1;
z in W1 by A17,XBOOLE_0:def 4;
then
A24: f1.pz in f1.:W1 by A23,FUNCT_1:def 6;
then r1-r0/2<aa1 by A14,XXREAL_1:4;
then r1-r0/2+(r2-r0/2)<aa1+aa2 by A22,XREAL_1:8;
then r1+r2-(r0/2+r0/2)<aa1+aa2;
then
A25: r-r0<aa1+aa2 by A4;
A26: aa2<r2+r0/2 by A12,A21,XXREAL_1:4;
A27: x=aa1+aa2 by A4,A18;
then reconsider rx=x as Real;
aa1<r1+r0/2 by A14,A24,XXREAL_1:4;
then aa1+aa2<r1+r0/2+(r2+r0/2) by A26,XREAL_1:8;
then aa1+aa2<r1+r2+(r0/2+r0/2);
then rx<r+r0 by A4,A27;
hence thesis by A27,A25,XXREAL_1:4;
end;
W is open & p in W by A13,A11,XBOOLE_0:def 4;
hence thesis by A6,A15,XBOOLE_1:1;
end;
then
A28: g0 is continuous by Th10;
for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2
holds g0.p=r1+r2 by A4;
hence thesis by A28;
end;
theorem
for X being non empty TopSpace, a being Real holds ex g being
Function of X,R^1 st (for p being Point of X holds g.p=a) & g is continuous
proof
let X be non empty TopSpace,a be Real;
reconsider a1 = a as Element of R^1 by TOPMETR:17,XREAL_0:def 1;
set g1 = (the carrier of X) --> a1;
reconsider g0=g1 as Function of X,R^1;
for p being Point of X,V being Subset of R^1 st g0.p in V & V is open
holds ex W being Subset of X st p in W & W is open & g0.:W c= V
proof
set f1=g0;
let p be Point of X,V be Subset of R^1;
assume that
A1: g0.p in V and
V is open;
set G1=V;
f1.: [#]X c= G1
proof
let y be object;
assume y in f1.: [#]X;
then ex x being object
st x in dom f1 & x in [#]X & y=f1.x by FUNCT_1:def 6;
then y=a by FUNCOP_1:7;
hence thesis by A1,FUNCOP_1:7;
end;
hence thesis;
end;
then ( for p being Point of X holds g1.p=a)& g0 is continuous by Th10,
FUNCOP_1:7;
hence thesis;
end;
theorem Th21:
for X being non empty TopSpace, f1,f2 being Function of X,R^1 st
f1 is continuous & f2 is continuous holds ex g being Function of X,R^1 st (for
p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1-r2
) & g is continuous
proof
let X being non empty TopSpace,f1,f2 be Function of X,R^1;
assume that
A1: f1 is continuous and
A2: f2 is continuous;
defpred P[set,set] means (for r1,r2 being Real st f1.$1=r1 & f2.$1=r2
holds $2=r1-r2);
A3: for x being Element of X ex y being Element of REAL st P[x,y]
proof
let x be Element of X;
reconsider r1=f1.x as Element of REAL by TOPMETR:17;
reconsider r2=f2.x as Element of REAL by TOPMETR:17;
set r3=r1-r2;
for r1,r2 being Real st f1.x=r1 & f2.x=r2 holds r3=r1-r2;
hence ex y being Element of REAL st for r1,r2 being Real st f1.x=r1
& f2.x=r2 holds y=r1-r2;
end;
ex f being Function of the carrier of X,REAL st for x being Element of X
holds P[x,f.x] from FUNCT_2:sch 3(A3);
then consider f being Function of the carrier of X,REAL such that
A4: for x being Element of X holds for r1,r2 being Real st f1.x=
r1 & f2.x=r2 holds f.x=r1-r2;
reconsider g0=f as Function of X,R^1 by TOPMETR:17;
for p being Point of X,V being Subset of R^1 st g0.p in V & V is open
holds ex W being Subset of X st p in W & W is open & g0.:W c= V
proof
let p be Point of X,V be Subset of R^1;
reconsider r=g0.p as Real;
reconsider r1=f1.p as Real;
reconsider r2=f2.p as Real;
assume g0.p in V & V is open;
then consider r0 being Real such that
A5: r0>0 and
A6: ].r-r0,r+r0.[ c= V by FRECHET:8;
reconsider G1=].r1-r0/2,r1+r0/2.[ as Subset of R^1 by TOPMETR:17;
A7: r1<r1+r0/2 by A5,XREAL_1:29,215;
then r1-r0/2<r1 by XREAL_1:19;
then
A8: f1.p in G1 by A7,XXREAL_1:4;
reconsider G2=].r2-r0/2,r2+r0/2.[ as Subset of R^1 by TOPMETR:17;
A9: r2<r2+r0/2 by A5,XREAL_1:29,215;
then r2-r0/2<r2 by XREAL_1:19;
then
A10: f2.p in G2 by A9,XXREAL_1:4;
G2 is open by JORDAN6:35;
then consider W2 being Subset of X such that
A11: p in W2 & W2 is open and
A12: f2.:W2 c= G2 by A2,A10,Th10;
G1 is open by JORDAN6:35;
then consider W1 being Subset of X such that
A13: p in W1 & W1 is open and
A14: f1.:W1 c= G1 by A1,A8,Th10;
set W=W1 /\ W2;
A15: g0.:W c= ].r-r0,r+r0.[
proof
let x be object;
assume x in g0.:W;
then consider z being object such that
A16: z in dom g0 and
A17: z in W and
A18: g0.z=x by FUNCT_1:def 6;
reconsider pz=z as Point of X by A16;
reconsider aa2=f2.pz as Real;
reconsider aa1=f1.pz as Real;
A19: pz in the carrier of X;
then
A20: pz in dom f1 by FUNCT_2:def 1;
A21: pz in dom f2 by A19,FUNCT_2:def 1;
z in W2 by A17,XBOOLE_0:def 4;
then
A22: f2.pz in f2.:W2 by A21,FUNCT_1:def 6;
then
A23: r2-r0/2<aa2 by A12,XXREAL_1:4;
A24: aa2<r2+r0/2 by A12,A22,XXREAL_1:4;
z in W1 by A17,XBOOLE_0:def 4;
then
A25: f1.pz in f1.:W1 by A20,FUNCT_1:def 6;
then r1-r0/2<aa1 by A14,XXREAL_1:4;
then r1-r0/2-(r2+r0/2)<aa1-aa2 by A24,XREAL_1:14;
then r1-r2-(r0/2+r0/2)<aa1-aa2;
then
A26: r-r0<aa1-aa2 by A4;
A27: x=aa1-aa2 by A4,A18;
then reconsider rx=x as Real;
aa1<r1+r0/2 by A14,A25,XXREAL_1:4;
then aa1-aa2<r1+r0/2-(r2-r0/2) by A23,XREAL_1:14;
then aa1-aa2<r1-r2+(r0/2+r0/2);
then rx<r+r0 by A4,A27;
hence thesis by A27,A26,XXREAL_1:4;
end;
W is open & p in W by A13,A11,XBOOLE_0:def 4;
hence thesis by A6,A15,XBOOLE_1:1;
end;
then
A28: g0 is continuous by Th10;
for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2
holds g0.p=r1-r2 by A4;
hence thesis by A28;
end;
theorem Th22:
for X being non empty TopSpace, f1 being Function of X,R^1 st f1
is continuous ex g being Function of X,R^1 st (for p being Point of X,r1 being
Real st f1.p=r1 holds g.p=r1*r1) & g is continuous
proof
let X being non empty TopSpace,f1 be Function of X,R^1;
defpred P[set,set] means (for r1 being Real st f1.$1=r1 holds $2=r1*
r1);
A1: for x being Element of X ex y being Element of REAL st P[x,y]
proof
let x be Element of X;
reconsider r1=f1.x as Element of REAL by TOPMETR:17;
set r3=r1*r1;
for r1 being Real st f1.x=r1 holds r3=r1*r1;
hence ex y being Element of REAL st for r1 being Real st f1.x=r1
holds y=r1*r1;
end;
ex f being Function of the carrier of X,REAL st for x being Element of X
holds P[x,f.x] from FUNCT_2:sch 3(A1);
then consider f being Function of the carrier of X,REAL such that
A2: for x being Element of X holds for r1 being Real st f1.x=r1
holds f.x=r1*r1;
reconsider g0=f as Function of X,R^1 by TOPMETR:17;
assume
A3: f1 is continuous;
for p being Point of X,V being Subset of R^1 st g0.p in V & V is open
holds ex W being Subset of X st p in W & W is open & g0.:W c= V
proof
let p be Point of X,V be Subset of R^1;
reconsider r=g0.p as Real;
reconsider r1=f1.p as Real;
assume g0.p in V & V is open;
then consider r0 being Real such that
A4: r0>0 and
A5: ].r-r0,r+r0.[ c= V by FRECHET:8;
A6: r=r1^2 by A2;
A7: r=r1*r1 by A2;
then
A8: 0<=r;
then
A9: (sqrt(r+r0))^2=r+r0 by A4,SQUARE_1:def 2;
now
per cases;
case
A10: r1>=0;
set r4=sqrt(r+r0)-sqrt(r);
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1 by TOPMETR:17;
A11: G1 is open by JORDAN6:35;
r+r0>r by A4,XREAL_1:29;
then sqrt(r+r0)>sqrt(r) by A7,SQUARE_1:27;
then
A12: r4>0 by XREAL_1:50;
then
A13: r1<r1+r4 by XREAL_1:29;
then r1-r4<r1 by XREAL_1:19;
then f1.p in G1 by A13,XXREAL_1:4;
then consider W1 being Subset of X such that
A14: p in W1 & W1 is open and
A15: f1.:W1 c= G1 by A3,A11,Th10;
A16: r1=sqrt r by A6,A10,SQUARE_1:def 2;
set W=W1;
A17: r4^2=(sqrt(r+r0))^2-2*sqrt(r+r0)*sqrt(r)+(sqrt(r))^2
.=r+r0-2*sqrt(r+r0)*sqrt(r)+(sqrt(r))^2 by A4,A8,SQUARE_1:def 2
.=r+(r0-2*sqrt(r+r0)*sqrt(r))+r by A8,SQUARE_1:def 2
.=2*r+r0-2*sqrt(r+r0)*sqrt(r);
g0.:W c= ].r-r0,r+r0.[
proof
let x be object;
assume x in g0.:W;
then consider z being object such that
A18: z in dom g0 and
A19: z in W and
A20: g0.z=x by FUNCT_1:def 6;
reconsider pz=z as Point of X by A18;
reconsider aa1=f1.pz as Real;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then
A21: f1.pz in f1.:W1 by A19,FUNCT_1:def 6;
then
A22: r1-r4<aa1 by A15,XXREAL_1:4;
A23: now
per cases;
case
A24: 0<=r1-r4;
A25: (r1-r4)^2 -aa1^2+-2*r4^2<= (r1-r4)^2 -aa1^2+0 by XREAL_1:7;
(r1-r4)^2<aa1^2 by A22,A24,SQUARE_1:16;
then (r1-r4)^2 -2*r4^2 -aa1^2<0 by A25,XREAL_1:49;
hence r-r0< aa1*aa1 by A7,A16,A17,XREAL_1:48;
end;
case
0>r1-r4;
then r1<r4 by XREAL_1:48;
then r1^2<r4^2 by A10,SQUARE_1:16;
then r1^2-r4^2<0 by XREAL_1:49;
then r1^2-r4^2 -2*r1*r4<0-0 by A10,A12;
hence r-r0< aa1*aa1 by A7,A16,A17;
end;
end;
-r1-r4<=r1-r4 by A10,XREAL_1:9;
then -(r1+r4)<aa1 by A22,XXREAL_0:2;
then
A26: aa1--(r1+r4)>0 by XREAL_1:50;
aa1<r1+r4 by A15,A21,XXREAL_1:4;
then r1+r4-aa1>0 by XREAL_1:50;
then (r1+r4-aa1)*(r1+r4+aa1)>0 by A26,XREAL_1:129;
then (r1+r4)^2-aa1^2>0;
then
A27: aa1^2<(r1+r4)^2 by XREAL_1:47;
x=aa1*aa1 by A2,A20;
hence thesis by A7,A16,A17,A27,A23,XXREAL_1:4;
end;
hence thesis by A5,A14,XBOOLE_1:1;
end;
case
A28: r1<0;
set r4=sqrt(r+r0)-sqrt(r);
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1 by TOPMETR:17;
A29: G1 is open by JORDAN6:35;
r+r0>r by A4,XREAL_1:29;
then sqrt(r+r0)>sqrt(r) by A7,SQUARE_1:27;
then
A30: r4>0 by XREAL_1:50;
then
A31: r1<r1+r4 by XREAL_1:29;
then r1-r4<r1 by XREAL_1:19;
then f1.p in G1 by A31,XXREAL_1:4;
then consider W1 being Subset of X such that
A32: p in W1 & W1 is open and
A33: f1.:W1 c= G1 by A3,A29,Th10;
A34: (-r1)^2=r1^2;
then
A35: -r1=sqrt r by A7,A28,SQUARE_1:22;
set W=W1;
A36: r4^2=r+r0-2*sqrt(r+r0)*sqrt(r)+(sqrt(r))^2 by A9
.=r+(r0-2*sqrt(r+r0)*sqrt(r))+r by A7,A28,A34,SQUARE_1:22
.=2*r+r0-2*sqrt(r+r0)*sqrt(r);
then
A37: -2*r1*r4+r4^2=r0 by A7,A35;
g0.:W c= ].r-r0,r+r0.[
proof
let x be object;
assume x in g0.:W;
then consider z being object such that
A38: z in dom g0 and
A39: z in W and
A40: g0.z=x by FUNCT_1:def 6;
reconsider pz=z as Point of X by A38;
reconsider aa1=f1.pz as Real;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then
A41: f1.pz in f1.:W1 by A39,FUNCT_1:def 6;
then
A42: aa1<r1+r4 by A33,XXREAL_1:4;
A43: now
per cases;
case
A44: 0>=r1+r4;
A45: (r1+r4)^2 -aa1^2+-2*r4^2<= (r1+r4)^2 -aa1^2+0 by XREAL_1:7;
-aa1>-(r1+r4) by A42,XREAL_1:24;
then (-(r1+r4))^2<(-aa1)^2 by A44,SQUARE_1:16;
then (r1+r4)^2 -2*r4^2 -aa1^2<0 by A45,XREAL_1:49;
hence r-r0< aa1*aa1 by A7,A37,XREAL_1:48;
end;
case
0<r1+r4;
then 0+-r1<(r1+r4)+-r1 by XREAL_1:8;
then (-r1)^2<r4^2 by A28,SQUARE_1:16;
then r1^2 -r1^2>r1^2-r4^2 by XREAL_1:15;
then r1^2-r4^2 +2*r1*r4<0+0 by A28,A30;
hence r-r0< aa1*aa1 by A7,A35,A36;
end;
end;
r1-r4<aa1 by A33,A41,XXREAL_1:4;
then aa1-(r1-r4)>0 by XREAL_1:50;
then -(-aa1+(r1-r4))>0;
then
A46: ((r1-r4)+-aa1)<0;
-r1-r4>=r1-r4 by A28,XREAL_1:9;
then -(-r1-r4)<=-(r1-r4) by XREAL_1:24;
then -(r1-r4)>aa1 by A42,XXREAL_0:2;
then -(r1-r4)+(r1-r4)>aa1+(r1-r4) by XREAL_1:8;
then (r1-r4-aa1)*(r1-r4+aa1)>0 by A46,XREAL_1:130;
then (r1-r4)^2-aa1^2>0;
then
A47: aa1^2<(r1-r4)^2 by XREAL_1:47;
x=aa1*aa1 by A2,A40;
hence thesis by A7,A37,A47,A43,XXREAL_1:4;
end;
hence thesis by A5,A32,XBOOLE_1:1;
end;
end;
hence thesis;
end;
then
A48: g0 is continuous by Th10;
for p being Point of X,r1 being Real st f1.p=r1 holds g0.p=r1*r1
by A2;
hence thesis by A48;
end;
theorem Th23:
for X being non empty TopSpace, f1 being Function of X,R^1,a
being Real st f1 is continuous holds ex g being Function of X,R^1 st (
for p being Point of X,r1 being Real st f1.p=r1 holds g.p=a*r1) & g is
continuous
proof
let X being non empty TopSpace,f1 be Function of X,R^1,a being Real;
defpred P[set,set] means (for r1 being Real st f1.$1=r1 holds $2=a*r1);
A1: for x being Element of X ex y being Element of REAL st P[x,y]
proof
let x be Element of X;
reconsider r1=f1.x as Real;
reconsider r3=a*r1 as Element of REAL by XREAL_0:def 1;
for r1 being Real st f1.x=r1 holds r3=a*r1;
hence
ex y being Element of REAL st for r1 being Real st f1.x=r1 holds y=a* r1;
end;
ex f being Function of the carrier of X,REAL st for x being Element of X
holds P[x,f.x] from FUNCT_2:sch 3(A1);
then consider f being Function of the carrier of X,REAL such that
A2: for x being Element of X holds for r1 being Real st f1.x=r1 holds f.
x=a*r1;
reconsider g0=f as Function of X,R^1 by TOPMETR:17;
A3: for p being Point of X,r1 being Real st f1.p=r1 holds g0.p=a*r1
by A2;
assume
A4: f1 is continuous;
for p being Point of X,V being Subset of R^1 st g0.p in V & V is open
holds ex W being Subset of X st p in W & W is open & g0.:W c= V
proof
let p be Point of X,V be Subset of R^1;
reconsider r=g0.p as Real;
reconsider r1=f1.p as Real;
assume g0.p in V & V is open;
then consider r0 being Real such that
A5: r0>0 and
A6: ].r-r0,r+r0.[ c= V by FRECHET:8;
A7: r=a*r1 by A2;
A8: r=a*r1 by A2;
now
per cases;
case
A9: a>=0;
now
per cases by A9;
case
A10: a>0;
set r4=r0/a;
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1 by TOPMETR:17;
A11: r1<r1+r4 by A5,A10,XREAL_1:29,139;
then r1-r4<r1 by XREAL_1:19;
then
A12: f1.p in G1 by A11,XXREAL_1:4;
G1 is open by JORDAN6:35;
then consider W1 being Subset of X such that
A13: p in W1 & W1 is open and
A14: f1.:W1 c= G1 by A4,A12,Th10;
set W=W1;
g0.:W c= ].r-r0,r+r0.[
proof
let x be object;
assume x in g0.:W;
then consider z being object such that
A15: z in dom g0 and
A16: z in W and
A17: g0.z=x by FUNCT_1:def 6;
reconsider pz=z as Point of X by A15;
reconsider aa1=f1.pz as Real;
A18: x=a*aa1 by A2,A17;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then
A19: f1.pz in f1.:W1 by A16,FUNCT_1:def 6;
then r1-r4<aa1 by A14,XXREAL_1:4;
then
A20: a*(r1-r4)<a*aa1 by A10,XREAL_1:68;
reconsider rx=x as Real by A17;
A21: a*(r1+r4) =a*r1+a*r4 .=r+r0 by A7,A10,XCMPLX_1:87;
A22: a*(r1-r4) =a*r1-a*r4 .=r-r0 by A7,A10,XCMPLX_1:87;
aa1<r1+r4 by A14,A19,XXREAL_1:4;
then rx<r+r0 by A10,A18,A21,XREAL_1:68;
hence thesis by A18,A20,A22,XXREAL_1:4;
end;
hence thesis by A6,A13,XBOOLE_1:1;
end;
case
A23: a=0;
set r4=r0;
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1 by TOPMETR:17;
A24: r1<r1+r4 by A5,XREAL_1:29;
then r1-r4<r1 by XREAL_1:19;
then
A25: f1.p in G1 by A24,XXREAL_1:4;
G1 is open by JORDAN6:35;
then consider W1 being Subset of X such that
A26: p in W1 & W1 is open and
f1.:W1 c= G1 by A4,A25,Th10;
set W=W1;
g0.:W c= ].r-r0,r+r0.[
proof
let x be object;
assume x in g0.:W;
then consider z being object such that
A27: z in dom g0 and
z in W and
A28: g0.z=x by FUNCT_1:def 6;
reconsider pz=z as Point of X by A27;
reconsider aa1=f1.pz as Real;
x=a*aa1 by A2,A28
.=0 by A23;
hence thesis by A5,A8,A23,XXREAL_1:4;
end;
hence thesis by A6,A26,XBOOLE_1:1;
end;
end;
hence thesis;
end;
case
A29: a<0;
set r4=r0/(-a);
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1 by TOPMETR:17;
-a>0 by A29,XREAL_1:58;
then
A30: r1<r1+r4 by A5,XREAL_1:29,139;
then r1-r4<r1 by XREAL_1:19;
then
A31: f1.p in G1 by A30,XXREAL_1:4;
G1 is open by JORDAN6:35;
then consider W1 being Subset of X such that
A32: p in W1 & W1 is open and
A33: f1.:W1 c= G1 by A4,A31,Th10;
set W=W1;
-a<>0 by A29;
then
A34: (-a)*r4=r0 by XCMPLX_1:87;
g0.:W c= ].r-r0,r+r0.[
proof
let x be object;
assume x in g0.:W;
then consider z being object such that
A35: z in dom g0 and
A36: z in W and
A37: g0.z=x by FUNCT_1:def 6;
reconsider pz=z as Point of X by A35;
reconsider aa1=f1.pz as Real;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then
A38: f1.pz in f1.:W1 by A36,FUNCT_1:def 6;
then r1-r4<aa1 by A33,XXREAL_1:4;
then
A39: (a)*aa1<(a)*(r1-r4) by A29,XREAL_1:69;
A40: (a)*(r1+r4) =a*r1--(a*r4) .=r-r0 by A3,A34;
A41: (a)*(r1-r4) =a*r1+-(a*r4) .=r+r0 by A3,A34;
aa1<r1+r4 by A33,A38,XXREAL_1:4;
then
A42: r-r0< (a)*aa1 by A29,A40,XREAL_1:69;
x=a*aa1 by A2,A37;
hence thesis by A39,A41,A42,XXREAL_1:4;
end;
hence thesis by A6,A32,XBOOLE_1:1;
end;
end;
hence thesis;
end;
then g0 is continuous by Th10;
hence thesis by A3;
end;
theorem Th24:
for X being non empty TopSpace, f1 being Function of X,R^1,a
being Real st f1 is continuous holds ex g being Function of X,R^1 st (
for p being Point of X,r1 being Real st f1.p=r1 holds g.p=r1+a) & g is
continuous
proof
let X being non empty TopSpace,f1 be Function of X,R^1,a being Real;
defpred P[set,set] means (for r1 being Real st f1.$1=r1 holds $2=r1+a);
A1: for x being Element of X ex y being Element of REAL st P[x,y]
proof
reconsider r2=a as Element of REAL by XREAL_0:def 1;
let x be Element of X;
reconsider r1=f1.x as Element of REAL by TOPMETR:17;
set r3 =r1+r2;
for r1 being Real st f1.x=r1 holds r3=r1+r2;
hence
ex y being Element of REAL st for r1 being Real st f1.x=r1 holds y=r1 +a;
end;
ex f being Function of the carrier of X,REAL st for x being Element of X
holds P[x,f.x] from FUNCT_2:sch 3(A1);
then consider f being Function of the carrier of X,REAL such that
A2: for x being Element of X holds for r1 being Real st f1.x=r1 holds f.
x=r1+a;
reconsider g0=f as Function of X,R^1 by TOPMETR:17;
assume
A3: f1 is continuous;
for p being Point of X,V being Subset of R^1 st g0.p in V & V is open
holds ex W being Subset of X st p in W & W is open & g0.:W c= V
proof
let p be Point of X,V be Subset of R^1;
reconsider r=g0.p as Real;
reconsider r1=f1.p as Real;
assume g0.p in V & V is open;
then consider r0 being Real such that
A4: r0>0 and
A5: ].r-r0,r+r0.[ c= V by FRECHET:8;
set r4=r0;
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1 by TOPMETR:17;
A6: r1<r1+r4 by A4,XREAL_1:29;
then r1-r4<r1 by XREAL_1:19;
then
A7: f1.p in G1 by A6,XXREAL_1:4;
G1 is open by JORDAN6:35;
then consider W1 being Subset of X such that
A8: p in W1 & W1 is open and
A9: f1.:W1 c= G1 by A3,A7,Th10;
set W=W1;
g0.:W c= ].r-r0,r+r0.[
proof
let x be object;
assume x in g0.:W;
then consider z being object such that
A10: z in dom g0 and
A11: z in W and
A12: g0.z=x by FUNCT_1:def 6;
reconsider pz=z as Point of X by A10;
reconsider aa1=f1.pz as Real;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then
A13: f1.pz in f1.:W1 by A11,FUNCT_1:def 6;
then r1-r4<aa1 by A9,XXREAL_1:4;
then
A14: (r1-r4)+a<aa1+a by XREAL_1:8;
A15: (r1-r4)+a =r1+a-r4 .=r-r0 by A2;
aa1<r1+r4 by A9,A13,XXREAL_1:4;
then
A16: (r1+r4)+a>aa1+a by XREAL_1:8;
x=aa1+a by A2,A12;
hence thesis by A16,A14,A15,XXREAL_1:4;
end;
hence thesis by A5,A8,XBOOLE_1:1;
end;
then
A17: g0 is continuous by Th10;
for p being Point of X,r1 being Real st f1.p=r1 holds g0.p=r1+a
by A2;
hence thesis by A17;
end;
theorem Th25:
for X being non empty TopSpace, f1,f2 being Function of X,R^1 st
f1 is continuous & f2 is continuous holds ex g being Function of X,R^1 st (for
p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2 holds g.p=r1*r2
) & g is continuous
proof
let X be non empty TopSpace, f1,f2 be Function of X,R^1;
assume
A1: f1 is continuous & f2 is continuous;
then consider g1 being Function of X,R^1 such that
A2: for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2
holds g1.p=r1+r2 and
A3: g1 is continuous by Th19;
consider g3 being Function of X,R^1 such that
A4: for p being Point of X,r1 being Real st g1.p=r1 holds g3.p=r1
*r1 and
A5: g3 is continuous by A3,Th22;
consider g2 being Function of X,R^1 such that
A6: for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2
holds g2.p=r1-r2 and
A7: g2 is continuous by A1,Th21;
consider g4 being Function of X,R^1 such that
A8: for p being Point of X,r1 being Real st g2.p=r1 holds g4.p=r1
*r1 and
A9: g4 is continuous by A7,Th22;
consider g5 being Function of X,R^1 such that
A10: for p being Point of X,r1,r2 being Real st g3.p=r1 & g4.p=r2
holds g5.p=r1-r2 and
A11: g5 is continuous by A5,A9,Th21;
consider g6 being Function of X,R^1 such that
A12: for p being Point of X,r1 being Real st g5.p=r1 holds g6.p=(
1/4) *r1 and
A13: g6 is continuous by A11,Th23;
for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2
holds g6.p=r1*r2
proof
let p be Point of X,r1,r2 be Real;
assume
A14: f1.p=r1 & f2.p=r2;
then g2.p=r1-r2 by A6;
then
A15: g4.p=(r1-r2)^2 by A8;
g1.p=r1+r2 by A2,A14;
then g3.p=(r1+r2)^2 by A4;
then g5.p= (r1+r2)^2 -(r1-r2)^2 by A10,A15;
then g6.p=(1/4)*( r1^2+2*r1*r2+r2^2 -(r1-r2)^2) by A12
.= r1*r2;
hence thesis;
end;
hence thesis by A13;
end;
theorem Th26:
for X being non empty TopSpace, f1 being Function of X,R^1 st f1
is continuous & (for q being Point of X holds f1.q<>0) holds ex g being
Function of X,R^1 st (for p being Point of X,r1 being Real st f1.p=r1
holds g.p=1/r1) & g is continuous
proof
let X being non empty TopSpace,f1 be Function of X,R^1;
assume that
A1: f1 is continuous and
A2: for q being Point of X holds f1.q<>0;
defpred P[set,set] means (for r1 being Real st f1.$1=r1 holds $2=1/r1);
A3: for x being Element of X ex y being Element of REAL st P[x,y]
proof
let x be Element of X;
reconsider r1=f1.x as Element of REAL by TOPMETR:17;
reconsider r3=1/r1 as Element of REAL by XREAL_0:def 1;
take r3;
thus for r1 being Real st f1.x=r1 holds r3=1/r1;
end;
ex f being Function of the carrier of X,REAL st for x being Element of X
holds P[x,f.x] from FUNCT_2:sch 3(A3);
then consider f being Function of the carrier of X,REAL such that
A4: for x being Element of X holds for r1 being Real st f1.x=r1 holds f.
x=1/r1;
reconsider g0=f as Function of X,R^1 by TOPMETR:17;
for p being Point of X,V being Subset of R^1 st g0.p in V & V is open
holds ex W being Subset of X st p in W & W is open & g0.:W c= V
proof
let p be Point of X,V be Subset of R^1;
reconsider r=g0.p as Real;
reconsider r1=f1.p as Real;
assume g0.p in V & V is open;
then consider r0 being Real such that
A5: r0>0 and
A6: ].r-r0,r+r0.[ c= V by FRECHET:8;
A7: r=1/r1 by A4;
A8: r1<>0 by A2;
now
per cases;
case
A9: r1>=0;
set r4=r0/r/(r+r0);
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1 by TOPMETR:17;
r0/r>0 by A5,A8,A7,A9,XREAL_1:139;
then
A10: r1<r1+r4 by A5,A7,A9,XREAL_1:29,139;
then r1-r4<r1 by XREAL_1:19;
then
A11: f1.p in G1 by A10,XXREAL_1:4;
A12: r/(r+r0)>0 by A5,A8,A7,A9,XREAL_1:139;
G1 is open by JORDAN6:35;
then consider W1 being Subset of X such that
A13: p in W1 & W1 is open and
A14: f1.:W1 c= G1 by A1,A11,Th10;
set W=W1;
r1-r4=1/r-r0/(r+r0)/r by A7
.=(1-r0/(r+r0))/r
.=((r+r0)/(r+r0)-r0/(r+r0))/r by A5,A7,A9,XCMPLX_1:60
.=((r+r0-r0)/(r+r0))/r
.=r/(r+r0)/r;
then
A15: r1-r4>0 by A8,A7,A9,A12,XREAL_1:139;
g0.:W c= ].r-r0,r+r0.[
proof
0<r0^2 by A5,SQUARE_1:12;
then r0 *r< r0 *r+(r0 *r0+r0 *r0) by XREAL_1:29;
then r0 *r-(r0 *r0+r0 *r0)< r0 *r by XREAL_1:19;
then (r0 *r-(r0 *r0+r0 *r0))+ r*r<r*r+r0 *r by XREAL_1:8;
then (r-r0)*(r+r0+r0)/(r+r0+r0)<r*(r+r0)/(r+r0+r0) by A5,A7,A9,
XREAL_1:74;
then r-r0<r*(r+r0)/(r+r0+r0) by A5,A7,A9,XCMPLX_1:89;
then r-r0<r/((r+r0+r0)/(r+r0)) by XCMPLX_1:77;
then r-r0<r/((r+r0)/(r+r0)+r0/(r+r0));
then r-r0<r*1/(1+r0/(r+r0)) by A5,A7,A9,XCMPLX_1:60;
then
A16: r-r0<1/((1+r0/(r+r0))/r) by XCMPLX_1:77;
let x be object;
assume x in g0.:W;
then consider z being object such that
A17: z in dom g0 and
A18: z in W and
A19: g0.z=x by FUNCT_1:def 6;
reconsider pz=z as Point of X by A17;
reconsider aa1=f1.pz as Real;
A20: x=1/aa1 by A4,A19;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then
A21: f1.pz in f1.:W1 by A18,FUNCT_1:def 6;
then
A22: r1-r4<aa1 by A14,XXREAL_1:4;
then
A23: 1/aa1<1/(r1-r4) by A15,XREAL_1:88;
aa1<r1+r4 by A14,A21,XXREAL_1:4;
then 1/(1/r+r4)<1/aa1 by A7,A15,A22,XREAL_1:76;
then
A24: r-r0<1/aa1 by A16,XXREAL_0:2;
1/(r1-r4) =1/(r1-r0 *r"/(r+r0)) .=1/(r1-r0 *(1/r)/(r+r0))
.=1/(r1-r0/((r+r0)/r1)) by A7,XCMPLX_1:77
.=1/(r1*1-r1*(r0/(r+r0))) by XCMPLX_1:81
.=1/((1-(r0/(r+r0)))*r1)
.=1/(((r+r0)/(r+r0)-(r0/(r+r0)))*r1) by A5,A7,A9,XCMPLX_1:60
.=1/((r+r0-r0)/(r+r0)*r1)
.=1/(r/((r+r0)/r1)) by XCMPLX_1:81
.=1/(r*r1/(r+r0)) by XCMPLX_1:77
.=(r+r0)/(r*r1)*1 by XCMPLX_1:80
.=(r+r0)/1 by A8,A7,XCMPLX_0:def 7
.=r+r0;
hence thesis by A20,A24,A23,XXREAL_1:4;
end;
hence thesis by A6,A13,XBOOLE_1:1;
end;
case
A25: r1<0;
set r4=r0/(-r)/(-r+r0);
reconsider G1=].r1-r4,r1+r4.[ as Subset of R^1 by TOPMETR:17;
A26: G1 is open by JORDAN6:35;
A27: 0<-r by A7,A25,XREAL_1:58;
then (-r)/(-r+r0)>0 by A5,XREAL_1:139;
then -(r/(-r+r0))>0;
then
A28: (r/(-r+r0))<0;
r0/(-r)>0 by A5,A27,XREAL_1:139;
then
A29: r1<r1+r4 by A5,A7,A25,XREAL_1:29,139;
then r1-r4<r1 by XREAL_1:19;
then f1.p in G1 by A29,XXREAL_1:4;
then consider W1 being Subset of X such that
A30: p in W1 & W1 is open and
A31: f1.:W1 c= G1 by A1,A26,Th10;
set W=W1;
r1*((-r)*(1/(-r)))=r1*1 by A27,XCMPLX_1:87;
then (-(r*r1))*(1/(-r))=r1;
then
A32: (-1)*(1/(-r))=r1 by A2,A7,XCMPLX_1:87;
then r1+r4=-(1/(-r))+r0/(-r+r0)/(-r) .=(-1)/(-r)+r0/(-r+r0)/(-r)
.=(-1+r0/(-r+r0))/(-r)
.=(-((-r+r0)/(-r+r0))+r0/(-r+r0))/(-r) by A5,A7,A25,XCMPLX_1:60
.=((-(-r+r0))/(-r+r0)+r0/(-r+r0))/(-r)
.=((r-r0+r0)/(-r+r0))/(-r)
.=r/(-r+r0)/(-r);
then
A33: (r1+r4)<0 by A27,A28,XREAL_1:141;
g0.:W c= ].r-r0,r+r0.[
proof
0<r0^2 by A5,SQUARE_1:12;
then r0 *(-r)< r0 *(-r)+(r0 *r0+r0 *r0) by XREAL_1:29;
then r0 *(-r)-(r0 *r0+r0 *r0)< r0 *(-r) by XREAL_1:19;
then
(r0 *(-r)-(r0 *r0+r0 *r0))+ (-r)*(-r)<r0 *(-r)+(-r)*(-r) by XREAL_1:8;
then
((-r)-r0)*((-r)+r0+r0)/((-r)+r0+r0)<(-r)*((-r)+r0)/((-r)+r0+r0)
by A5,A7,A25,XREAL_1:74;
then (-r)-r0<(-r)*((-r)+r0)/((-r)+r0+r0) by A5,A7,A25,XCMPLX_1:89;
then (-r)-r0<(-r)/(((-r)+r0+r0)/((-r)+r0)) by XCMPLX_1:77;
then (-r)-r0<(-r)/(((-r)+r0)/((-r)+r0)+r0/((-r)+r0));
then (-r)-r0<(-r)*1/(1+r0/((-r)+r0)) by A5,A7,A25,XCMPLX_1:60;
then (-r)-r0<1/((1+r0/((-r)+r0))/(-r)) by XCMPLX_1:77;
then -(r+r0)<1/(1/(-r)+r4);
then (r+r0)>-(1/(1/(-r)+r4)) by XREAL_1:25;
then
A34: (r+r0)>(1/-(1/(-r)+r4)) by XCMPLX_1:188;
let x be object;
assume x in g0.:W;
then consider z being object such that
A35: z in dom g0 and
A36: z in W and
A37: g0.z=x by FUNCT_1:def 6;
reconsider pz=z as Point of X by A35;
reconsider aa1=f1.pz as Real;
A38: x=1/aa1 by A4,A37;
pz in the carrier of X;
then pz in dom f1 by FUNCT_2:def 1;
then
A39: f1.pz in f1.:W1 by A36,FUNCT_1:def 6;
then
A40: aa1<r1+r4 by A31,XXREAL_1:4;
then
A41: 1/aa1>1/(r1+r4) by A33,XREAL_1:87;
r1-r4<aa1 by A31,A39,XXREAL_1:4;
then 1/(-(1/(-r))-r4)>1/aa1 by A32,A33,A40,XREAL_1:99;
then
A42: r+r0>1/aa1 by A34,XXREAL_0:2;
1/(r1+r4) =1/(r1+r0 *(-r)"/(-r+r0)) .=1/(r1+r0 *(1/(-r))/(-r+r0))
.=1/(r1+(-(r1*r0))/(-r+r0)) by A32
.=1/(r1+-((r1*r0)/(-r+r0)))
.=1/(r1-((r1*r0))/(-r+r0))
.=1/(r1-r0/((-r+r0)/r1)) by XCMPLX_1:77
.=1/(r1*1-r1*(r0/(-r+r0))) by XCMPLX_1:81
.=1/(r1*(1-r0/(-r+r0)))
.=1/(((-r+r0)/(-r+r0)-(r0/(-r+r0)))*r1) by A5,A7,A25,XCMPLX_1:60
.=1/((-r+r0-r0)/(-(r-r0))*(r1))
.=1/((-(-r+r0-r0)/(r-r0))*(r1)) by XCMPLX_1:188
.=1/((-r+r0-r0)/((r-r0))*(-r1))
.=1/((-r)/((r-r0)/(-r1))) by XCMPLX_1:81
.=1/((-r)*(-r1)/(r-r0)) by XCMPLX_1:77
.=(r-r0)/((-r)*(-r1))*1 by XCMPLX_1:80
.=(r-r0)/((-r)*(-r)") by A32
.=(r-r0)/1 by A27,XCMPLX_0:def 7
.=r-r0;
hence thesis by A38,A42,A41,XXREAL_1:4;
end;
hence thesis by A6,A30,XBOOLE_1:1;
end;
end;
hence thesis;
end;
then
A43: g0 is continuous by Th10;
for p being Point of X,r1 being Real st f1.p=r1 holds g0.p=1/r1
by A4;
hence thesis by A43;
end;
theorem Th27:
for X being non empty TopSpace, f1,f2 being Function of X,R^1 st
f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0)
holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real
st f1.p=r1 & f2.p=r2 holds g.p=r1/r2) & g is continuous
proof
let X be non empty TopSpace, f1,f2 be Function of X,R^1;
assume that
A1: f1 is continuous and
A2: f2 is continuous & for q being Point of X holds f2.q<>0;
consider g1 being Function of X,R^1 such that
A3: for p being Point of X,r2 being Real st f2.p=r2 holds g1.p=1/ r2 and
A4: g1 is continuous by A2,Th26;
consider g2 being Function of X,R^1 such that
A5: for p being Point of X,r1,r2 being Real st f1.p=r1 & g1.p=r2
holds g2.p=r1*r2 and
A6: g2 is continuous by A1,A4,Th25;
for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2
holds g2.p=r1/r2
proof
let p be Point of X,r1,r2 be Real;
assume that
A7: f1.p=r1 and
A8: f2.p=r2;
g1.p=1/r2 by A3,A8;
then g2.p=r1*(1/r2) by A5,A7
.=r1/r2;
hence thesis;
end;
hence thesis by A6;
end;
theorem Th28:
for X being non empty TopSpace, f1,f2 being Function of X,R^1 st
f1 is continuous & f2 is continuous & (for q being Point of X holds f2.q<>0)
holds ex g being Function of X,R^1 st (for p being Point of X,r1,r2 being Real
st f1.p=r1 & f2.p=r2 holds g.p=r1/r2/r2) & g is continuous
proof
let X be non empty TopSpace, f1,f2 be Function of X,R^1;
assume that
A1: f1 is continuous and
A2: f2 is continuous & for q being Point of X holds f2.q<>0;
consider g2 being Function of X,R^1 such that
A3: for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2
holds g2.p=r1/r2 and
A4: g2 is continuous by A1,A2,Th27;
consider g3 being Function of X,R^1 such that
A5: for p being Point of X,r1,r2 being Real st g2.p=r1 & f2.p=r2
holds g3.p=r1/r2 and
A6: g3 is continuous by A2,A4,Th27;
for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2
holds g3.p=r1/r2/r2
proof
let p be Point of X,r1,r2 be Real;
assume that
A7: f1.p=r1 and
A8: f2.p=r2;
g2.p=r1/r2 by A3,A7,A8;
hence thesis by A5,A8;
end;
hence thesis by A6;
end;
theorem Th29:
for K0 being Subset of TOP-REAL 2, f being Function of (TOP-REAL
2)|K0,R^1 st (for p being Point of (TOP-REAL 2)|K0 holds f.p=proj1.p) holds f
is continuous
proof
reconsider g=proj1 as Function of TOP-REAL 2,R^1 by TOPMETR:17;
let K0 be Subset of TOP-REAL 2, f be Function of (TOP-REAL 2)|K0,R^1;
A1: dom f= the carrier of (TOP-REAL 2)|K0 & (the carrier of TOP-REAL 2)/\K0=
K0 by FUNCT_2:def 1,XBOOLE_1:28;
A2: g is continuous by JORDAN5A:27;
assume for p being Point of (TOP-REAL 2)|K0 holds f.p=proj1.p;
then
A3: for x being object st x in dom f holds f.x=proj1.x;
the carrier of (TOP-REAL 2)|K0 =[#]((TOP-REAL 2)|K0) .=K0 by PRE_TOPC:def 5;
then f=g|K0 by A1,A3,Th6,FUNCT_1:46;
hence thesis by A2,TOPMETR:7;
end;
theorem Th30:
for K0 being Subset of TOP-REAL 2, f being Function of (TOP-REAL
2)|K0,R^1 st (for p being Point of (TOP-REAL 2)|K0 holds f.p=proj2.p) holds f
is continuous
proof
let K0 be Subset of TOP-REAL 2, f be Function of (TOP-REAL 2)|K0,R^1;
A1: dom f= the carrier of (TOP-REAL 2)|K0 & (the carrier of TOP-REAL 2) /\
K0=K0 by FUNCT_2:def 1,XBOOLE_1:28;
assume for p being Point of (TOP-REAL 2)|K0 holds f.p=proj2.p;
then
A2: for x being object st x in dom f holds f.x=proj2.x;
the carrier of (TOP-REAL 2)|K0 =[#]((TOP-REAL 2)|K0) .=K0 by PRE_TOPC:def 5;
then f=proj2|K0 by A1,A2,Th7,FUNCT_1:46;
hence thesis by JORDAN5A:27;
end;
theorem Th31:
for K1 being non empty Subset of TOP-REAL 2, f being Function of
(TOP-REAL 2)|K1,R^1 st (for p being Point of (TOP-REAL 2) st p in the carrier
of (TOP-REAL 2)|K1 holds f.p=1/p`1) & (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`1<>0 ) holds f is continuous
proof
let K1 be non empty Subset of TOP-REAL 2, f be Function of (TOP-REAL 2)|K1,
R^1;
assume that
A1: for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2
)| K1 holds f.p=1/p`1 and
A2: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)
|K1 holds q`1<>0;
reconsider g1=proj1|K1 as Function of (TOP-REAL 2)|K1,R^1 by TOPMETR:17;
A3: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1)
.=K1 by PRE_TOPC:def 5;
A4: for q being Point of (TOP-REAL 2)|K1 holds g1.q=proj1.q
proof
let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1 & dom proj1=the carrier of
TOP-REAL 2 by FUNCT_2:def 1;
then q in dom proj1 /\ K1 by A3,XBOOLE_0:def 4;
hence thesis by FUNCT_1:48;
end;
A5: for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0
proof
let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1;
then reconsider q2=q as Point of TOP-REAL 2 by A3;
g1.q=proj1.q by A4
.=q2`1 by PSCOMP_1:def 5;
hence thesis by A2;
end;
g1 is continuous by A4,Th29;
then consider g3 being Function of (TOP-REAL 2)|K1,R^1 such that
A6: for q being Point of (TOP-REAL 2)|K1,r2 being Real st g1.q=
r2 holds g3.q=1/r2 and
A7: g3 is continuous by A5,Th26;
A8: for x being object st x in dom f holds f.x=g3.x
proof
let x be object;
assume
A9: x in dom f;
then reconsider s=x as Point of (TOP-REAL 2)|K1;
x in [#]((TOP-REAL 2)|K1) by A9;
then x in K1 by PRE_TOPC:def 5;
then reconsider r=x as Point of (TOP-REAL 2);
A10: g1.s=proj1.s & proj1.r=r`1 by A4,PSCOMP_1:def 5;
f.r=1/r`1 by A1,A9;
hence thesis by A6,A10;
end;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then dom f=dom g3 by FUNCT_2:def 1;
hence thesis by A7,A8,FUNCT_1:2;
end;
theorem Th32:
for K1 being non empty Subset of TOP-REAL 2, f being Function of
(TOP-REAL 2)|K1,R^1 st (for p being Point of (TOP-REAL 2) st p in the carrier
of (TOP-REAL 2)|K1 holds f.p=1/p`2) & (for q being Point of TOP-REAL 2 st q in
the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds f is continuous
proof
let K1 be non empty Subset of TOP-REAL 2, f be Function of (TOP-REAL 2)|K1,
R^1;
assume that
A1: for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2
)| K1 holds f.p=1/p`2 and
A2: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)
|K1 holds q`2<>0;
reconsider g1=proj2|K1 as Function of (TOP-REAL 2)|K1,R^1 by TOPMETR:17;
A3: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1)
.=K1 by PRE_TOPC:def 5;
A4: for q being Point of (TOP-REAL 2)|K1 holds g1.q=proj2.q
proof
let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1 & dom proj2=the carrier of
TOP-REAL 2 by FUNCT_2:def 1;
then q in dom proj2 /\ K1 by A3,XBOOLE_0:def 4;
hence thesis by FUNCT_1:48;
end;
A5: for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0
proof
let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1;
then reconsider q2=q as Point of TOP-REAL 2 by A3;
g1.q=proj2.q by A4
.=q2`2 by PSCOMP_1:def 6;
hence thesis by A2;
end;
g1 is continuous by A4,Th30;
then consider g3 being Function of (TOP-REAL 2)|K1,R^1 such that
A6: for q being Point of (TOP-REAL 2)|K1,r2 being Real st g1.q=
r2 holds g3.q=1/r2 and
A7: g3 is continuous by A5,Th26;
A8: for x being object st x in dom f holds f.x=g3.x
proof
let x be object;
assume
A9: x in dom f;
then reconsider s=x as Point of (TOP-REAL 2)|K1;
x in [#]((TOP-REAL 2)|K1) by A9;
then x in K1 by PRE_TOPC:def 5;
then reconsider r=x as Point of (TOP-REAL 2);
A10: g1.s=proj2.s & proj2.r=r`2 by A4,PSCOMP_1:def 6;
f.r=1/r`2 by A1,A9;
hence thesis by A6,A10;
end;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then dom f=dom g3 by FUNCT_2:def 1;
hence thesis by A7,A8,FUNCT_1:2;
end;
theorem Th33:
for K1 being non empty Subset of TOP-REAL 2, f being Function of
(TOP-REAL 2)|K1,R^1 st (for p being Point of (TOP-REAL 2) st p in the carrier
of (TOP-REAL 2)|K1 holds f.p=p`2/p`1/p`1) & (for q being Point of TOP-REAL 2 st
q in the carrier of (TOP-REAL 2)|K1 holds q`1<>0 ) holds f is continuous
proof
let K1 be non empty Subset of TOP-REAL 2, f be Function of (TOP-REAL 2)|K1,
R^1;
assume that
A1: for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2
)| K1 holds f.p=p`2/p`1/p`1 and
A2: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)
|K1 holds q`1<>0;
reconsider g2=proj2|K1 as Function of (TOP-REAL 2)|K1,R^1 by TOPMETR:17;
reconsider g1=proj1|K1 as Function of (TOP-REAL 2)|K1,R^1 by TOPMETR:17;
A3: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1)
.=K1 by PRE_TOPC:def 5;
A4: for q being Point of (TOP-REAL 2)|K1 holds g1.q=proj1.q
proof
let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1 & dom proj1=the carrier of
TOP-REAL 2 by FUNCT_2:def 1;
then q in dom proj1 /\ K1 by A3,XBOOLE_0:def 4;
hence thesis by FUNCT_1:48;
end;
then
A5: g1 is continuous by Th29;
A6: for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0
proof
let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1;
then reconsider q2=q as Point of TOP-REAL 2 by A3;
g1.q=proj1.q by A4
.=q2`1 by PSCOMP_1:def 5;
hence thesis by A2;
end;
A7: for q being Point of (TOP-REAL 2)|K1 holds g2.q=proj2.q
proof
let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1 & dom proj2=the carrier of
TOP-REAL 2 by FUNCT_2:def 1;
then q in dom proj2 /\ K1 by A3,XBOOLE_0:def 4;
hence thesis by FUNCT_1:48;
end;
then g2 is continuous by Th30;
then consider g3 being Function of (TOP-REAL 2)|K1,R^1 such that
A8: for q being Point of (TOP-REAL 2)|K1,r1,r2 being Real st g2.
q= r1 & g1.q=r2 holds g3.q=r1/r2/r2 and
A9: g3 is continuous by A5,A6,Th28;
A10: for x being object st x in dom f holds f.x=g3.x
proof
let x be object;
assume
A11: x in dom f;
then reconsider s=x as Point of (TOP-REAL 2)|K1;
x in [#]((TOP-REAL 2)|K1) by A11;
then x in K1 by PRE_TOPC:def 5;
then reconsider r=x as Point of (TOP-REAL 2);
A12: proj2.r=r`2 & proj1.r=r`1 by PSCOMP_1:def 5,def 6;
A13: g2.s=proj2.s & g1.s=proj1.s by A7,A4;
f.r=r`2/r`1/r`1 by A1,A11;
hence thesis by A8,A13,A12;
end;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then dom f=dom g3 by FUNCT_2:def 1;
hence thesis by A9,A10,FUNCT_1:2;
end;
theorem Th34:
for K1 being non empty Subset of TOP-REAL 2, f being Function of
(TOP-REAL 2)|K1,R^1 st (for p being Point of (TOP-REAL 2) st p in the carrier
of (TOP-REAL 2)|K1 holds f.p=p`1/p`2/p`2) & (for q being Point of TOP-REAL 2 st
q in the carrier of (TOP-REAL 2)|K1 holds q`2<>0 ) holds f is continuous
proof
let K1 be non empty Subset of TOP-REAL 2, f be Function of (TOP-REAL 2)|K1,
R^1;
assume that
A1: for p being Point of (TOP-REAL 2) st p in the carrier of (TOP-REAL 2
)| K1 holds f.p=p`1/p`2/p`2 and
A2: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)
|K1 holds q`2<>0;
reconsider g2=proj1|K1 as Function of (TOP-REAL 2)|K1,R^1 by TOPMETR:17;
reconsider g1=proj2|K1 as Function of (TOP-REAL 2)|K1,R^1 by TOPMETR:17;
A3: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1)
.=K1 by PRE_TOPC:def 5;
A4: for q being Point of (TOP-REAL 2)|K1 holds g1.q=proj2.q
proof
let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1 & dom proj2=the carrier of
TOP-REAL 2 by FUNCT_2:def 1;
then q in dom proj2 /\ K1 by A3,XBOOLE_0:def 4;
hence thesis by FUNCT_1:48;
end;
then
A5: g1 is continuous by Th30;
A6: for q being Point of (TOP-REAL 2)|K1 holds g1.q<>0
proof
let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1;
then reconsider q2=q as Point of TOP-REAL 2 by A3;
g1.q=proj2.q by A4
.=q2`2 by PSCOMP_1:def 6;
hence thesis by A2;
end;
A7: for q being Point of (TOP-REAL 2)|K1 holds g2.q=proj1.q
proof
let q be Point of (TOP-REAL 2)|K1;
q in the carrier of (TOP-REAL 2)|K1 & dom proj1=the carrier of
TOP-REAL 2 by FUNCT_2:def 1;
then q in dom proj1 /\ K1 by A3,XBOOLE_0:def 4;
hence thesis by FUNCT_1:48;
end;
then g2 is continuous by Th29;
then consider g3 being Function of (TOP-REAL 2)|K1,R^1 such that
A8: for q being Point of (TOP-REAL 2)|K1,r1,r2 being Real st g2.
q= r1 & g1.q=r2 holds g3.q=r1/r2/r2 and
A9: g3 is continuous by A5,A6,Th28;
A10: for x being object st x in dom f holds f.x=g3.x
proof
let x be object;
assume
A11: x in dom f;
then reconsider s=x as Point of (TOP-REAL 2)|K1;
x in [#]((TOP-REAL 2)|K1) by A11;
then x in K1 by PRE_TOPC:def 5;
then reconsider r=x as Point of (TOP-REAL 2);
A12: proj1.r=r`1 & proj2.r=r`2 by PSCOMP_1:def 5,def 6;
A13: g2.s=proj1.s & g1.s=proj2.s by A7,A4;
f.r=r`1/r`2/r`2 by A1,A11;
hence thesis by A8,A13,A12;
end;
dom g3=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1;
then dom f=dom g3 by FUNCT_2:def 1;
hence thesis by A9,A10,FUNCT_1:2;
end;
theorem Th35:
for K0,B0 being Subset of TOP-REAL 2, f being Function of (
TOP-REAL 2)|K0,(TOP-REAL 2)|B0, f1,f2 being Function of (TOP-REAL 2)|K0,R^1 st
f1 is continuous & f2 is continuous & K0<>{} & B0<>{} & (for x,y,r,s being Real
st |[x,y]| in K0 & r=f1.(|[x,y]|) & s=f2.(|[x,y]|) holds f.(|[x,y]|)=|[r
,s]|) holds f is continuous
proof
let K0,B0 be Subset of TOP-REAL 2, f be Function of (TOP-REAL 2)|K0,(
TOP-REAL 2)|B0, f1,f2 be Function of (TOP-REAL 2)|K0,R^1;
assume that
A1: f1 is continuous and
A2: f2 is continuous and
A3: K0<>{} and
A4: B0<>{} and
A5: for x,y,r,s being Real st |[x,y]| in K0 & r=f1.(|[x,y]|) & s
=f2.(|[x,y]|) holds f. |[x,y]|=|[r,s]|;
reconsider B1=B0 as non empty Subset of TOP-REAL 2 by A4;
reconsider K1=K0 as non empty Subset of TOP-REAL 2 by A3;
reconsider X=(TOP-REAL 2)|K1,Y=(TOP-REAL 2)|B1 as non empty TopSpace;
reconsider f0=f as Function of X,Y;
for r being Point of X,V being Subset of Y st f0.r in V & V is open
holds ex W being Subset of X st r in W & W is open & f0.:W c= V
proof
let r be Point of X,V be Subset of Y;
assume that
A6: f0.r in V and
A7: V is open;
consider V2 being Subset of TOP-REAL 2 such that
A8: V2 is open and
A9: V=V2 /\ [#]Y by A7,TOPS_2:24;
A10: V2 /\ [#]Y c= V2 by XBOOLE_1:17;
then f0.r in V2 by A6,A9;
then reconsider p=f0.r as Point of TOP-REAL 2;
consider r2 being Real such that
A11: r2>0 and
A12: {q where q is Point of TOP-REAL 2: p`1-r2<q`1 & q`1<p`1+r2 & p`2-
r2< q`2 & q`2<p`2+r2} c= V2 by A6,A8,A9,A10,Th11;
reconsider G1= ].p`1-r2,p`1+r2.[,G2= ].p`2-r2,p`2+r2.[ as Subset of R^1 by
TOPMETR:17;
A13: G1 is open by JORDAN6:35;
reconsider r3=f1.r,r4=f2.r as Real;
A14: the carrier of X=[#]X .=K0 by PRE_TOPC:def 5;
then r in K0;
then reconsider pr=r as Point of TOP-REAL 2;
A15: r= |[pr`1,pr`2]| by EUCLID:53;
then
A16: f0. |[pr`1,pr`2]|=|[r3,r4]| by A5,A14;
A17: p`2 <p`2+r2 by A11,XREAL_1:29;
then p`2-r2< p`2 by XREAL_1:19;
then p`2 in ].p`2-r2,p`2+r2.[ by A17,XXREAL_1:4;
then G2 is open & f2.r in G2 by A15,A16,EUCLID:52,JORDAN6:35;
then consider W2 being Subset of X such that
A18: r in W2 and
A19: W2 is open and
A20: f2.:W2 c= G2 by A2,Th10;
A21: p`1 <p`1+r2 by A11,XREAL_1:29;
then p`1-r2< p`1 by XREAL_1:19;
then p`1 in ].p`1-r2,p`1+r2.[ by A21,XXREAL_1:4;
then f1.r in ].p`1-r2,p`1+r2.[ by A15,A16,EUCLID:52;
then consider W1 being Subset of X such that
A22: r in W1 and
A23: W1 is open and
A24: f1.:W1 c= G1 by A1,A13,Th10;
reconsider W5=W1 /\ W2 as Subset of X;
f2.:W5 c= f2.:W2 by RELAT_1:123,XBOOLE_1:17;
then
A25: f2.:W5 c= G2 by A20;
f1.:W5 c= f1.:W1 by RELAT_1:123,XBOOLE_1:17;
then
A26: f1.:W5 c= G1 by A24;
A27: f0.:W5 c= V
proof
let v be object;
assume
A28: v in f0.:W5;
then reconsider q2=v as Point of Y;
consider k being object such that
A29: k in dom f0 and
A30: k in W5 and
A31: q2=f0.k by A28,FUNCT_1:def 6;
the carrier of X=[#]X .=K0 by PRE_TOPC:def 5;
then k in K0 by A29;
then reconsider r8=k as Point of TOP-REAL 2;
A32: dom f0=the carrier of (TOP-REAL 2)|K1 by FUNCT_2:def 1
.=[#]((TOP-REAL 2)|K1)
.=K0 by PRE_TOPC:def 5;
then
A33: |[r8`1,r8`2]| in K0 by A29,EUCLID:53;
A34: dom f2=the carrier of (TOP-REAL 2)|K0 by FUNCT_2:def 1
.=[#]((TOP-REAL 2)|K0)
.=K0 by PRE_TOPC:def 5;
A35: dom f1=the carrier of (TOP-REAL 2)|K0 by FUNCT_2:def 1
.=[#]((TOP-REAL 2)|K0)
.=K0 by PRE_TOPC:def 5;
reconsider r7=f1.(|[r8`1,r8`2]|), s7=f2.(|[r8`1,r8`2]|) as Real;
A36: |[r8`1,r8`2]| in W5 by A30,EUCLID:53;
then f1.(|[r8`1,r8`2]|) in f1.:W5 by A33,A35,FUNCT_1:def 6;
then
A37: p`1-r2< r7 & r7<p`1+r2 by A26,XXREAL_1:4;
f2.(|[r8`1,r8`2]|) in f2.:W5 by A33,A34,A36,FUNCT_1:def 6;
then
A38: p`2-r2< s7 & s7<p`2+r2 by A25,XXREAL_1:4;
k= |[r8`1,r8`2]| by EUCLID:53;
then
A39: v=|[r7,s7]| by A5,A29,A31,A32;
(|[r7,s7]|)`1 =r7 & (|[r7,s7]|)`2 =s7 by EUCLID:52;
then q2 in [#]Y & v in {q3 where q3 is Point of TOP-REAL 2: p`1-r2<q3`1
& q3`1<p `1+r2 & p`2-r2<q3`2 & q3`2<p`2+r2} by A39,A37,A38;
hence thesis by A9,A12,XBOOLE_0:def 4;
end;
r in W5 by A22,A18,XBOOLE_0:def 4;
hence thesis by A23,A19,A27;
end;
hence thesis by Th10;
end;
theorem Th36:
for K0,B0 being Subset of TOP-REAL 2,f being Function of (
TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=Out_In_Sq|K0 & B0=NonZero TOP-REAL 2 & K0={
p: (p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} holds f is
continuous
proof
let K0,B0 be Subset of TOP-REAL 2,f be Function of (TOP-REAL 2)|K0,(TOP-REAL
2)|B0;
A1: (1.REAL 2)<>0.TOP-REAL 2 by Lm1,REVROT_1:19;
assume
A2: f=Out_In_Sq|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`2<=p`1 & -p`1<=p`2
or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2};
A3: K0 c= B0
proof
let x be object;
assume
A4: x in K0;
then
ex p8 being Point of TOP-REAL 2 st x=p8 &( p8`2<=p8`1 & - p8`1<=p8`2 or
p8`2>=p8`1 & p8`2<=-p8`1)& p8<>0.TOP-REAL 2 by A2;
then not x in {0.TOP-REAL 2} by TARSKI:def 1;
hence thesis by A2,A4,XBOOLE_0:def 5;
end;
(1.REAL 2)`2<=(1.REAL 2)`1 & -(1.REAL 2)`1<=(1.REAL 2)`2 or (1.REAL 2)
`2>=(1.REAL 2)`1 & (1.REAL 2)`2<=-(1.REAL 2)`1 by Th5;
then
A5: 1.REAL 2 in K0 by A2,A1;
then reconsider K1=K0 as non empty Subset of TOP-REAL 2;
A6: K1 c= NonZero TOP-REAL 2
proof
let z be object;
assume
A7: z in K1;
then ex p8 being Point of TOP-REAL 2 st p8=z &( p8`2<=p8`1 & - p8`1<=p8`2
or p8`2>=p8`1 & p8`2<=-p8`1)& p8<>0.TOP-REAL 2 by A2;
then not z in {0.TOP-REAL 2} by TARSKI:def 1;
hence thesis by A7,XBOOLE_0:def 5;
end;
A8: dom (Out_In_Sq|K1) c= dom ((proj2)*(Out_In_Sq|K1))
proof
let x be object;
assume
A9: x in dom (Out_In_Sq|K1);
then x in dom Out_In_Sq /\ K1 by RELAT_1:61;
then x in dom Out_In_Sq by XBOOLE_0:def 4;
then Out_In_Sq.x in rng Out_In_Sq by FUNCT_1:3;
then
A10: dom proj2 = (the carrier of TOP-REAL 2) & Out_In_Sq.x in the carrier
of TOP-REAL 2 by FUNCT_2:def 1,XBOOLE_0:def 5;
(Out_In_Sq|K1).x=Out_In_Sq.x by A9,FUNCT_1:47;
hence thesis by A9,A10,FUNCT_1:11;
end;
A11: rng ((proj2)*(Out_In_Sq|K1)) c= the carrier of R^1 by TOPMETR:17;
A12: NonZero TOP-REAL 2<>{} by Th9;
A13: dom (Out_In_Sq|K1) c= dom ((proj1)*(Out_In_Sq|K1))
proof
let x be object;
assume
A14: x in dom (Out_In_Sq|K1);
then x in dom Out_In_Sq /\ K1 by RELAT_1:61;
then x in dom Out_In_Sq by XBOOLE_0:def 4;
then Out_In_Sq.x in rng Out_In_Sq by FUNCT_1:3;
then
A15: dom proj1 = (the carrier of TOP-REAL 2) & Out_In_Sq.x in the carrier
of TOP-REAL 2 by FUNCT_2:def 1,XBOOLE_0:def 5;
(Out_In_Sq|K1).x=Out_In_Sq.x by A14,FUNCT_1:47;
hence thesis by A14,A15,FUNCT_1:11;
end;
A16: rng ((proj1)*(Out_In_Sq|K1)) c= the carrier of R^1 by TOPMETR:17;
dom ((proj1)*(Out_In_Sq|K1)) c= dom (Out_In_Sq|K1) by RELAT_1:25;
then dom ((proj1)*(Out_In_Sq|K1)) =dom (Out_In_Sq|K1) by A13
.=dom Out_In_Sq /\ K1 by RELAT_1:61
.=(NonZero TOP-REAL 2)/\ K1 by A12,FUNCT_2:def 1
.=K1 by A6,XBOOLE_1:28
.=[#]((TOP-REAL 2)|K1) by PRE_TOPC:def 5
.=the carrier of (TOP-REAL 2)|K1;
then reconsider
g1=(proj1)*(Out_In_Sq|K1) as Function of (TOP-REAL 2)|K1,R^1 by A16,FUNCT_2:2
;
for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds g1.p=1/p`1
proof
A17: K1 c= NonZero TOP-REAL 2
proof
let z be object;
assume
A18: z in K1;
then
ex p8 being Point of TOP-REAL 2 st p8=z &( p8`2<=p8`1 & - p8`1<=p8`2
or p8`2>=p8`1 & p8`2<=-p8`1)& p8<>0.TOP-REAL 2 by A2;
then not z in {0.TOP-REAL 2} by TARSKI:def 1;
hence thesis by A18,XBOOLE_0:def 5;
end;
A19: NonZero TOP-REAL 2<>{} by Th9;
A20: dom (Out_In_Sq|K1)=dom Out_In_Sq /\ K1 by RELAT_1:61
.=(NonZero TOP-REAL 2)/\ K1 by A19,FUNCT_2:def 1
.=K1 by A17,XBOOLE_1:28;
let p be Point of TOP-REAL 2;
A21: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1)
.=K1 by PRE_TOPC:def 5;
assume
A22: p in the carrier of (TOP-REAL 2)|K1;
then ex p3 being Point of TOP-REAL 2 st p=p3 &( p3`2<=p3`1 & - p3`1<=p3`2
or p3`2>=p3`1 & p3`2<=-p3`1)& p3<>0.TOP-REAL 2 by A2,A21;
then
A23: Out_In_Sq.p=|[1/p`1,p`2/p`1/p`1]| by Def1;
(Out_In_Sq|K1).p=Out_In_Sq.p by A22,A21,FUNCT_1:49;
then g1.p=(proj1).(|[1/p`1,p`2/p`1/p`1]|) by A22,A20,A21,A23,FUNCT_1:13
.=(|[1/p`1,p`2/p`1/p`1]|)`1 by PSCOMP_1:def 5
.=1/p`1 by EUCLID:52;
hence thesis;
end;
then consider f1 being Function of (TOP-REAL 2)|K1,R^1 such that
A24: for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)
|K1 holds f1.p=1/p`1;
dom ((proj2)*(Out_In_Sq|K1)) c= dom (Out_In_Sq|K1) by RELAT_1:25;
then dom ((proj2)*(Out_In_Sq|K1)) =dom (Out_In_Sq|K1) by A8
.=dom Out_In_Sq /\ K1 by RELAT_1:61
.=(NonZero TOP-REAL 2)/\ K1 by A12,FUNCT_2:def 1
.=K1 by A6,XBOOLE_1:28
.=[#]((TOP-REAL 2)|K1) by PRE_TOPC:def 5
.=the carrier of (TOP-REAL 2)|K1;
then reconsider
g2=(proj2)*(Out_In_Sq|K1) as Function of (TOP-REAL 2)|K1,R^1 by A11,FUNCT_2:2
;
for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds g2.p=p`2/p`1/p`1
proof
A25: NonZero TOP-REAL 2<>{} by Th9;
A26: dom (Out_In_Sq|K1)=dom Out_In_Sq /\ K1 by RELAT_1:61
.=(NonZero TOP-REAL 2)/\ K1 by A25,FUNCT_2:def 1
.=K1 by A6,XBOOLE_1:28;
let p be Point of TOP-REAL 2;
A27: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1)
.=K1 by PRE_TOPC:def 5;
assume
A28: p in the carrier of (TOP-REAL 2)|K1;
then ex p3 being Point of TOP-REAL 2 st p=p3 &( p3`2<=p3`1 & - p3`1<=p3`2
or p3`2>=p3`1 & p3`2<=-p3`1)& p3<>0.TOP-REAL 2 by A2,A27;
then
A29: Out_In_Sq.p=|[1/p`1,p`2/p`1/p`1]| by Def1;
(Out_In_Sq|K1).p=Out_In_Sq.p by A28,A27,FUNCT_1:49;
then g2.p=(proj2).(|[1/p`1,p`2/p`1/p`1]|) by A28,A26,A27,A29,FUNCT_1:13
.=(|[1/p`1,p`2/p`1/p`1]|)`2 by PSCOMP_1:def 6
.=p`2/p`1/p`1 by EUCLID:52;
hence thesis;
end;
then consider f2 being Function of (TOP-REAL 2)|K1,R^1 such that
A30: for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)
|K1 holds f2.p=p`2/p`1/p`1;
A31: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1
holds q`1<>0
proof
let q be Point of TOP-REAL 2;
A32: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1)
.=K1 by PRE_TOPC:def 5;
assume q in the carrier of (TOP-REAL 2)|K1;
then
A33: ex p3 being Point of TOP-REAL 2 st q=p3 &( p3`2<=p3`1 & - p3`1<=p3`2
or p3`2>=p3`1 & p3`2<=-p3`1)& p3<>0.TOP-REAL 2 by A2,A32;
now
assume
A34: q`1=0;
then q`2=0 by A33;
hence contradiction by A33,A34,EUCLID:53,54;
end;
hence thesis;
end;
then
A35: f1 is continuous by A24,Th31;
A36: for x,y,r,s being Real st |[x,y]| in K1 & r=f1.(|[x,y]|) & s=f2.
(|[x,y]|) holds f. |[x,y]|=|[r,s]|
proof
let x,y,r,s be Real;
assume that
A37: |[x,y]| in K1 and
A38: r=f1.(|[x,y]|) & s=f2.(|[x,y]|);
set p99=|[x,y]|;
A39: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1)
.=K1 by PRE_TOPC:def 5;
then
A40: f1.p99=1/p99`1 by A24,A37;
A41: ex p3 being Point of TOP-REAL 2 st p99=p3 &( p3`2<=p3`1 & -p3`1<=p3`2
or p3`2>=p3`1 & p3`2<=-p3`1)& p3<>0.TOP-REAL 2 by A2,A37;
then (p99`2<=p99`1 & -p99`1<=p99`2 or p99`2>=p99`1 & p99`2<=-p99`1)
implies Out_In_Sq.p99=|[1/p99`1,p99`2/p99`1/p99`1]| by Def1;
then
(Out_In_Sq|K0). |[x,y]|= |[1/p99`1,p99`2/p99`1/p99`1]| by A37,A41,FUNCT_1:49
.=|[r,s]| by A30,A37,A38,A39,A40;
hence thesis by A2;
end;
f2 is continuous by A31,A30,Th33;
hence thesis by A5,A3,A35,A36,Th35;
end;
theorem Th37:
for K0,B0 being Subset of TOP-REAL 2,f being Function of (
TOP-REAL 2)|K0,(TOP-REAL 2)|B0 st f=Out_In_Sq|K0 & B0=NonZero TOP-REAL 2 & K0={
p: (p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} holds f is
continuous
proof
let K0,B0 be Subset of TOP-REAL 2,f be Function of (TOP-REAL 2)|K0,(TOP-REAL
2)|B0;
A1: (1.REAL 2)<>0.TOP-REAL 2 by Lm1,REVROT_1:19;
assume
A2: f=Out_In_Sq|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`1<=p`2 & -p`2<=p`1
or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2};
A3: K0 c= B0
proof
let x be object;
assume
A4: x in K0;
then
ex p8 being Point of TOP-REAL 2 st x=p8 &( p8`1<=p8`2 & - p8`2<=p8`1 or
p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2 by A2;
then not x in {0.TOP-REAL 2} by TARSKI:def 1;
hence thesis by A2,A4,XBOOLE_0:def 5;
end;
(1.REAL 2)`1<=(1.REAL 2)`2 & -(1.REAL 2)`2<=(1.REAL 2)`1 or (1.REAL 2)
`1>=(1.REAL 2)`2 & (1.REAL 2)`1<=-(1.REAL 2)`2 by Th5;
then
A5: 1.REAL 2 in K0 by A2,A1;
then reconsider K1=K0 as non empty Subset of TOP-REAL 2;
A6: K1 c= NonZero TOP-REAL 2
proof
let z be object;
assume
A7: z in K1;
then ex p8 being Point of TOP-REAL 2 st p8=z &( p8`1<=p8`2 & - p8`2<=p8`1
or p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2 by A2;
then not z in {0.TOP-REAL 2} by TARSKI:def 1;
hence thesis by A7,XBOOLE_0:def 5;
end;
A8: dom (Out_In_Sq|K1) c= dom ((proj1)*(Out_In_Sq|K1))
proof
let x be object;
assume
A9: x in dom (Out_In_Sq|K1);
then x in dom Out_In_Sq /\ K1 by RELAT_1:61;
then x in dom Out_In_Sq by XBOOLE_0:def 4;
then Out_In_Sq.x in rng Out_In_Sq by FUNCT_1:3;
then
A10: dom proj1 = (the carrier of TOP-REAL 2) & Out_In_Sq.x in the carrier
of TOP-REAL 2 by FUNCT_2:def 1,XBOOLE_0:def 5;
(Out_In_Sq|K1).x=Out_In_Sq.x by A9,FUNCT_1:47;
hence thesis by A9,A10,FUNCT_1:11;
end;
A11: rng ((proj1)*(Out_In_Sq|K1)) c= the carrier of R^1 by TOPMETR:17;
A12: NonZero TOP-REAL 2<>{} by Th9;
A13: dom (Out_In_Sq|K1) c= dom ((proj2)*(Out_In_Sq|K1))
proof
let x be object;
assume
A14: x in dom (Out_In_Sq|K1);
then x in dom Out_In_Sq /\ K1 by RELAT_1:61;
then x in dom Out_In_Sq by XBOOLE_0:def 4;
then Out_In_Sq.x in rng Out_In_Sq by FUNCT_1:3;
then
A15: dom proj2 = (the carrier of TOP-REAL 2) & Out_In_Sq.x in the carrier
of TOP-REAL 2 by FUNCT_2:def 1,XBOOLE_0:def 5;
(Out_In_Sq|K1).x=Out_In_Sq.x by A14,FUNCT_1:47;
hence thesis by A14,A15,FUNCT_1:11;
end;
A16: rng ((proj2)*(Out_In_Sq|K1)) c= the carrier of R^1 by TOPMETR:17;
dom ((proj2)*(Out_In_Sq|K1)) c= dom (Out_In_Sq|K1) by RELAT_1:25;
then dom ((proj2)*(Out_In_Sq|K1)) =dom (Out_In_Sq|K1) by A13
.=dom Out_In_Sq /\ K1 by RELAT_1:61
.=(NonZero TOP-REAL 2)/\ K1 by A12,FUNCT_2:def 1
.=K1 by A6,XBOOLE_1:28
.=[#]((TOP-REAL 2)|K1) by PRE_TOPC:def 5
.=the carrier of (TOP-REAL 2)|K1;
then reconsider
g1=(proj2)*(Out_In_Sq|K1) as Function of (TOP-REAL 2)|K1,R^1 by A16,FUNCT_2:2
;
for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds g1.p=1/p`2
proof
A17: K1 c= NonZero TOP-REAL 2
proof
let z be object;
assume
A18: z in K1;
then
ex p8 being Point of TOP-REAL 2 st p8=z &( p8`1<=p8`2 & - p8`2<=p8`1
or p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2 by A2;
then not z in {0.TOP-REAL 2} by TARSKI:def 1;
hence thesis by A18,XBOOLE_0:def 5;
end;
A19: NonZero TOP-REAL 2<>{} by Th9;
A20: dom (Out_In_Sq|K1)=dom Out_In_Sq /\ K1 by RELAT_1:61
.=(NonZero TOP-REAL 2)/\ K1 by A19,FUNCT_2:def 1
.=K1 by A17,XBOOLE_1:28;
let p be Point of TOP-REAL 2;
A21: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1)
.=K1 by PRE_TOPC:def 5;
assume
A22: p in the carrier of (TOP-REAL 2)|K1;
then ex p3 being Point of TOP-REAL 2 st p=p3 &( p3`1<=p3`2 & - p3`2<=p3`1
or p3`1>=p3`2 & p3`1<=-p3`2)& p3<>0.TOP-REAL 2 by A2,A21;
then
A23: Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by Th14;
(Out_In_Sq|K1).p=Out_In_Sq.p by A22,A21,FUNCT_1:49;
then g1.p=(proj2).(|[p`1/p`2/p`2,1/p`2]|) by A22,A20,A21,A23,FUNCT_1:13
.=(|[p`1/p`2/p`2,1/p`2]|)`2 by PSCOMP_1:def 6
.=1/p`2 by EUCLID:52;
hence thesis;
end;
then consider f1 being Function of (TOP-REAL 2)|K1,R^1 such that
A24: for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)
|K1 holds f1.p=1/p`2;
dom ((proj1)*(Out_In_Sq|K1)) c= dom (Out_In_Sq|K1) by RELAT_1:25;
then dom ((proj1)*(Out_In_Sq|K1)) =dom (Out_In_Sq|K1) by A8
.=dom Out_In_Sq /\ K1 by RELAT_1:61
.=(NonZero TOP-REAL 2)/\ K1 by A12,FUNCT_2:def 1
.=K1 by A6,XBOOLE_1:28
.=[#]((TOP-REAL 2)|K1) by PRE_TOPC:def 5
.=the carrier of (TOP-REAL 2)|K1;
then reconsider
g2=(proj1)*(Out_In_Sq|K1) as Function of (TOP-REAL 2)|K1,R^1 by A11,FUNCT_2:2
;
for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)|K1
holds g2.p=p`1/p`2/p`2
proof
A25: NonZero TOP-REAL 2<>{} by Th9;
A26: dom (Out_In_Sq|K1)=dom Out_In_Sq /\ K1 by RELAT_1:61
.=(NonZero TOP-REAL 2)/\ K1 by A25,FUNCT_2:def 1
.=K1 by A6,XBOOLE_1:28;
let p be Point of TOP-REAL 2;
A27: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1)
.=K1 by PRE_TOPC:def 5;
assume
A28: p in the carrier of (TOP-REAL 2)|K1;
then ex p3 being Point of TOP-REAL 2 st p=p3 &( p3`1<=p3`2 & - p3`2<=p3`1
or p3`1>=p3`2 & p3`1<=-p3`2)& p3<>0.TOP-REAL 2 by A2,A27;
then
A29: Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by Th14;
(Out_In_Sq|K1).p=Out_In_Sq.p by A28,A27,FUNCT_1:49;
then g2.p=(proj1).(|[p`1/p`2/p`2,1/p`2]|) by A28,A26,A27,A29,FUNCT_1:13
.=(|[p`1/p`2/p`2,1/p`2]|)`1 by PSCOMP_1:def 5
.=p`1/p`2/p`2 by EUCLID:52;
hence thesis;
end;
then consider f2 being Function of (TOP-REAL 2)|K1,R^1 such that
A30: for p being Point of TOP-REAL 2 st p in the carrier of (TOP-REAL 2)
|K1 holds f2.p=p`1/p`2/p`2;
A31: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|K1
holds q`2<>0
proof
let q be Point of TOP-REAL 2;
A32: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1)
.=K1 by PRE_TOPC:def 5;
assume q in the carrier of (TOP-REAL 2)|K1;
then
A33: ex p3 being Point of TOP-REAL 2 st q=p3 &( p3`1<=p3`2 & - p3`2<=p3`1
or p3`1>=p3`2 & p3`1<=-p3`2)& p3<>0.TOP-REAL 2 by A2,A32;
now
assume
A34: q`2=0;
then q`1=0 by A33;
hence contradiction by A33,A34,EUCLID:53,54;
end;
hence thesis;
end;
then
A35: f1 is continuous by A24,Th32;
A36: for x,y,s,r being Real st |[x,y]| in K1 & s=f2.(|[x,y]|) & r=f1.
(|[x,y]|) holds f. |[x,y]|=|[s,r]|
proof
let x,y,s,r be Real;
assume that
A37: |[x,y]| in K1 and
A38: s=f2.(|[x,y]|) & r=f1.(|[x,y]|);
set p99=|[x,y]|;
A39: ex p3 being Point of TOP-REAL 2 st p99=p3 &( p3`1<=p3`2 & -p3`2<=p3`1
or p3`1>=p3`2 & p3`1<=-p3`2)& p3<>0.TOP-REAL 2 by A2,A37;
A40: the carrier of (TOP-REAL 2)|K1=[#]((TOP-REAL 2)|K1)
.=K1 by PRE_TOPC:def 5;
then
A41: f1.p99=1/p99`2 by A24,A37;
(Out_In_Sq|K0). |[x,y]|=(Out_In_Sq). |[x,y]| by A37,FUNCT_1:49
.= |[p99`1/p99`2/p99`2,1/p99`2]| by A39,Th14
.=|[s,r]| by A30,A37,A38,A40,A41;
hence thesis by A2;
end;
f2 is continuous by A31,A30,Th34;
hence thesis by A5,A3,A35,A36,Th35;
end;
scheme
TopSubset { P[set] } : { p where p is Point of TOP-REAL 2 : P[p] } is Subset
of TOP-REAL 2 proof
{ p where p is Point of TOP-REAL 2 : P[p] } c= the carrier of TOP-REAL 2
proof
let x be object;
assume x in { p where p is Point of TOP-REAL 2 : P[p] };
then ex p being Point of TOP-REAL 2 st p = x & P[p];
hence thesis;
end;
hence thesis;
end;
scheme
TopCompl { P[set], K() -> Subset of TOP-REAL 2 } : K()` = { p where p is
Point of TOP-REAL 2 : not P[p] }
provided
A1: K() = { p where p is Point of TOP-REAL 2 : P[p] }
proof
thus K()` c= { p where p is Point of TOP-REAL 2: not P[p] }
proof
let x be object;
assume
A2: x in K()`;
then reconsider qx=x as Point of TOP-REAL 2;
x in (the carrier of TOP-REAL 2) \ K() by A2,SUBSET_1:def 4;
then not x in K() by XBOOLE_0:def 5;
then not P[qx] by A1;
hence thesis;
end;
let x be object;
assume x in {p7 where p7 is Point of TOP-REAL 2: not P[p7]};
then
A3: ex p7 being Point of TOP-REAL 2 st p7=x & not P[p7];
then not ex q7 being Point of TOP-REAL 2 st x=q7 & P[q7];
then not x in K() by A1;
then x in (the carrier of TOP-REAL 2) \ K() by A3,XBOOLE_0:def 5;
hence thesis by SUBSET_1:def 4;
end;
Lm2: now
let p01, p02,px1,px2 be Real;
set r0 = (p01 -p02)/4;
assume p01 - px1 - (p02 - px2)<=r0--r0;
then p01 - p02 - (px1 - px2)<=r0+r0;
then p01 - p02<= (px1 - px2)+(r0+r0) by XREAL_1:20;
then p01 - p02 - (p01 -p02)/2<= (px1 - px2) by XREAL_1:20;
hence (p01 - p02)/2<= px1 - px2;
end;
scheme
ClosedSubset { F,G(Point of TOP-REAL 2) -> Real } : {p where p is
Point of TOP-REAL 2 : F(p) <= G(p) } is closed Subset of TOP-REAL 2
provided
A1: for p,q being Point of TOP-REAL 2 holds F(p-q) = F(p) - F(q) & G(p-q
) = G(p) - G(q) and
A2: for p,q being Point of TOP-REAL 2 holds (|. (p-q).|)^2 = (F(p-q))^2+
(G(p-q))^2
proof
defpred P[Point of TOP-REAL 2] means F($1) <= G($1);
reconsider K2 = {p7 where p7 is Point of TOP-REAL 2: P[p7] } as Subset of
TOP-REAL 2 from TopSubset;
A3: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;
then reconsider K21 = K2` as Subset of TopSpaceMetr Euclid 2;
A4: K2 = {p7 where p7 is Point of TOP-REAL 2: P[p7] };
A5: K2`={p7 where p7 is Point of TOP-REAL 2:not P[p7]} from TopCompl(A4);
for p being Point of Euclid 2 st p in K21 ex r being Real st r>0
& Ball(p,r) c= K21
proof
let p be Point of Euclid 2;
assume
A6: p in K21;
then reconsider p0=p as Point of TOP-REAL 2;
set r0=(F(p0) -G(p0))/4;
ex p7 being Point of TOP-REAL 2 st p0=p7 & F(p7)>G(p7) by A5,A6;
then
A7: F(p0)- G(p0)>0 by XREAL_1:50;
then
A8: (F(p0) -G(p0))/2 >0 by XREAL_1:139;
Ball(p,r0) c= K2`
proof
let x be object;
A9: Ball(p,r0)={q where q is Element of Euclid 2: dist(p,q) < r0} by
METRIC_1:17;
assume
A10: x in Ball(p,r0);
then reconsider px=x as Point of TOP-REAL 2 by TOPREAL3:8;
consider q being Element of Euclid 2 such that
A11: q=x and
A12: dist(p,q) < r0 by A10,A9;
dist(p,q)= |. (p0-px).| by A11,JGRAPH_1:28;
then
A13: (|.(p0-px).|)^2 <= r0^2 by A12,SQUARE_1:15;
A14: F(p0-px)=F(p0) - F(px) by A1;
A15: (|. (p0-px).|)^2 =(F(p0-px))^2+(G(p0-px))^2 by A2;
0+(F(p0-px))^2 <= (G(p0-px))^2 + (F(p0-px))^2 by XREAL_1:7;
then (F(p0-px))^2 <= r0^2 by A15,A13,XXREAL_0:2;
then
A16: F(p0) - F(px)<=r0 by A7,A14,SQUARE_1:47;
A17: G(p0-px)=G(p0) - G(px) by A1;
(G(p0-px))^2+0 <= (G(p0-px))^2 + (F(p0-px))^2 by XREAL_1:7;
then (G(p0-px))^2 <= r0^2 by A15,A13,XXREAL_0:2;
then -r0 <=G(p0) - G(px) by A7,A17,SQUARE_1:47;
then F(p0) - F(px) - (G(p0) - G(px))<=r0--r0 by A16,XREAL_1:13;
then F(px)-G(px)>0 by A8,Lm2;
then F(px)>G(px) by XREAL_1:47;
hence thesis by A5;
end;
hence thesis by A7,XREAL_1:139;
end;
then K21 is open by TOPMETR:15;
then K2` is open by A3,PRE_TOPC:30;
hence thesis by TOPS_1:3;
end;
deffunc F(Point of TOP-REAL 2)=$1`1;
deffunc G(Point of TOP-REAL 2)=$1`2;
Lm3: for p,q being Point of TOP-REAL 2 holds F(p-q) = F(p) - F(q) & G(p-q) = G
(p) - G(q) by TOPREAL3:3;
Lm4: for p,q being Point of TOP-REAL 2 holds (|. (p-q).|)^2 = (F(p-q))^2+(G(p-
q))^2 by JGRAPH_1:29;
Lm5: {p7 where p7 is Point of TOP-REAL 2:F(p7)<=G(p7) } is closed Subset of
TOP-REAL 2 from ClosedSubset(Lm3,Lm4);
Lm6: for p,q being Point of TOP-REAL 2 holds G(p-q) = G(p) - G(q) & F(p-q) = F
(p) - F(q) by TOPREAL3:3;
Lm7: for p,q being Point of TOP-REAL 2 holds (|. (p-q).|)^2 = (G(p-q))^2+(F(p-
q))^2 by JGRAPH_1:29;
Lm8: {p7 where p7 is Point of TOP-REAL 2:G(p7)<=F(p7) } is closed Subset of
TOP-REAL 2 from ClosedSubset(Lm6,Lm7);
deffunc H(Point of TOP-REAL 2)=-$1`1;
deffunc I(Point of TOP-REAL 2)=-$1`2;
Lm9: now
let p,q be Point of TOP-REAL 2;
thus H(p-q) = -(p`1 - q`1) by TOPREAL3:3
.= H(p) - H(q);
thus G(p-q) = G(p) - G(q) by TOPREAL3:3;
end;
Lm10: now
let p,q be Point of TOP-REAL 2;
(H(p-q))^2 = (F(p-q))^2;
hence (|. (p-q).|)^2 = (H(p-q))^2+(G(p-q))^2 by JGRAPH_1:29;
end;
Lm11: {p7 where p7 is Point of TOP-REAL 2:H(p7)<=G(p7) } is closed Subset of
TOP-REAL 2 from ClosedSubset(Lm9,Lm10);
Lm12: now
let p,q be Point of TOP-REAL 2;
thus G(p-q) = G(p) - G(q) by TOPREAL3:3;
thus H(p-q) = -(p`1 - q`1) by TOPREAL3:3
.= H(p) - H(q);
end;
Lm13: now
let p,q be Point of TOP-REAL 2;
(-(p-q)`1)^2 = ((p-q)`1)^2;
hence (|. (p-q).|)^2 = (G(p-q))^2+(H(p-q))^2 by JGRAPH_1:29;
end;
Lm14: {p7 where p7 is Point of TOP-REAL 2:G(p7)<=H(p7) } is closed Subset of
TOP-REAL 2 from ClosedSubset(Lm12,Lm13);
Lm15: now
let p,q be Point of TOP-REAL 2;
thus I(p-q) = -(p`2 - q`2) by TOPREAL3:3
.= I(p) - I(q);
thus F(p-q) = F(p) - F(q) by TOPREAL3:3;
end;
Lm16: now
let p,q be Point of TOP-REAL 2;
(-(p-q)`2)^2 = ((p-q)`2)^2;
hence (|. (p-q).|)^2 = (I(p-q))^2+(F(p-q))^2 by JGRAPH_1:29;
end;
Lm17: {p7 where p7 is Point of TOP-REAL 2:I(p7)<=F(p7) } is closed Subset of
TOP-REAL 2 from ClosedSubset(Lm15,Lm16);
Lm18: now
let p,q be Point of TOP-REAL 2;
thus F(p-q) = F(p) - F(q) by TOPREAL3:3;
thus I(p-q) = -(p`2 - q`2) by TOPREAL3:3
.= I(p) - I(q);
end;
Lm19: now
let p,q be Point of TOP-REAL 2;
(I(p-q))^2 = (G(p-q))^2;
hence (|. (p-q).|)^2 = (F(p-q))^2+(I(p-q))^2 by JGRAPH_1:29;
end;
Lm20: {p7 where p7 is Point of TOP-REAL 2: F(p7)<=I(p7) } is closed Subset of
TOP-REAL 2 from ClosedSubset(Lm18,Lm19);
theorem Th38:
for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2
)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=Out_In_Sq|
K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p
`1) & p<>0.TOP-REAL 2} holds f is continuous & K0 is closed
proof
reconsider K5={p7 where p7 is Point of TOP-REAL 2: p7`2<=-p7`1 } as closed
Subset of TOP-REAL 2 by Lm14;
reconsider K4={p7 where p7 is Point of TOP-REAL 2: p7`1<=p7`2 } as closed
Subset of TOP-REAL 2 by Lm5;
reconsider K3={p7 where p7 is Point of TOP-REAL 2: -p7`1<=p7`2 } as closed
Subset of TOP-REAL 2 by Lm11;
reconsider K2={p7 where p7 is Point of TOP-REAL 2: p7`2<=p7`1 } as closed
Subset of TOP-REAL 2 by Lm8;
let B0 be Subset of TOP-REAL 2,K0 be Subset of (TOP-REAL 2)|B0,f being
Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0);
defpred P[Point of TOP-REAL 2] means ($1`2<=$1`1 & -$1`1<=$1`2 or $1`2>=$1`1
& $1`2<=-$1`1);
the carrier of (TOP-REAL 2)|B0=[#]((TOP-REAL 2)|B0) .= B0 by PRE_TOPC:def 5;
then reconsider K1=K0 as Subset of TOP-REAL 2 by XBOOLE_1:1;
assume
A1: f=Out_In_Sq|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`2<=p`1 & -p`1<=p`2
or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2};
K0 c= B0
proof
let x be object;
assume x in K0;
then
A2: ex p8 being Point of TOP-REAL 2 st x=p8 &( p8`2<=p8`1 & - p8`1<=p8`2 or
p8`2>=p8`1 & p8`2<=-p8`1)& p8<>0.TOP-REAL 2 by A1;
then not x in {0.TOP-REAL 2} by TARSKI:def 1;
hence thesis by A1,A2,XBOOLE_0:def 5;
end;
then
A3: ((TOP-REAL 2)|B0)|K0=(TOP-REAL 2)|K1 by PRE_TOPC:7;
reconsider K1={p7 where p7 is Point of TOP-REAL 2: P[p7]} as Subset of
TOP-REAL 2 from TopSubset;
A4: K1 /\ B0 c= K0
proof
let x be object;
assume
A5: x in K1 /\ B0;
then x in B0 by XBOOLE_0:def 4;
then not x in {0.TOP-REAL 2} by A1,XBOOLE_0:def 5;
then
A6: not x=0.TOP-REAL 2 by TARSKI:def 1;
x in K1 by A5,XBOOLE_0:def 4;
then ex p7 being Point of TOP-REAL 2 st p7=x &( p7`2<=(p7`1) & -(p7`1)<=p7
`2 or p7`2>=(p7`1) & p7`2<=-(p7`1));
hence thesis by A1,A6;
end;
A7: K2 /\ K3 \/ K4 /\ K5 c= K1
proof
let x be object;
assume
A8: x in K2 /\ K3 \/ K4 /\ K5;
now
per cases by A8,XBOOLE_0:def 3;
case
A9: x in K2 /\ K3;
then x in K3 by XBOOLE_0:def 4;
then
A10: ex p8 being Point of TOP-REAL 2 st p8=x & -p8`1<=p8`2;
x in K2 by A9,XBOOLE_0:def 4;
then ex p7 being Point of TOP-REAL 2 st p7=x & p7`2<=(p7`1);
hence thesis by A10;
end;
case
A11: x in K4 /\ K5;
then x in K5 by XBOOLE_0:def 4;
then
A12: ex p8 being Point of TOP-REAL 2 st p8=x & p8`2<= -p8`1;
x in K4 by A11,XBOOLE_0:def 4;
then ex p7 being Point of TOP-REAL 2 st p7=x & p7`2>=(p7`1);
hence thesis by A12;
end;
end;
hence thesis;
end;
K1 c= K2 /\ K3 \/ K4 /\ K5
proof
let x be object;
assume x in K1;
then ex p being Point of TOP-REAL 2 st p=x &( p`2<=p`1 & -p`1 <=p`2 or p`2
>=p`1 & p`2<=-p`1);
then x in K2 & x in K3 or x in K4 & x in K5;
then x in K2 /\ K3 or x in K4 /\ K5 by XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
then K1=K2 /\ K3 \/ K4 /\ K5 by A7;
then
A13: K1 is closed;
K0 c= K1 /\ B0
proof
let x be object;
assume x in K0;
then
A14: ex p being Point of TOP-REAL 2 st x=p &( p`2<=p`1 & -p`1 <=p`2 or p`2
>=p`1 & p`2<=-p`1)& p<>0.TOP-REAL 2 by A1;
then not x in {0.TOP-REAL 2} by TARSKI:def 1;
then
A15: x in B0 by A1,A14,XBOOLE_0:def 5;
x in K1 by A14;
hence thesis by A15,XBOOLE_0:def 4;
end;
then K0=K1 /\ B0 by A4
.=K1 /\ [#]((TOP-REAL 2)|B0) by PRE_TOPC:def 5;
hence thesis by A1,A3,A13,Th36,PRE_TOPC:13;
end;
theorem Th39:
for B0 being Subset of TOP-REAL 2,K0 being Subset of (TOP-REAL 2
)|B0,f being Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0) st f=Out_In_Sq|
K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p
`2) & p<>0.TOP-REAL 2} holds f is continuous & K0 is closed
proof
reconsider K5={p7 where p7 is Point of TOP-REAL 2: p7`1<=-p7`2 } as closed
Subset of TOP-REAL 2 by Lm20;
reconsider K4={p7 where p7 is Point of TOP-REAL 2: p7`2<=p7`1 } as closed
Subset of TOP-REAL 2 by Lm8;
reconsider K3={p7 where p7 is Point of TOP-REAL 2: -p7`2<=p7`1 } as closed
Subset of TOP-REAL 2 by Lm17;
reconsider K2={p7 where p7 is Point of TOP-REAL 2: p7`1<=p7`2 } as closed
Subset of TOP-REAL 2 by Lm5;
let B0 be Subset of TOP-REAL 2,K0 be Subset of (TOP-REAL 2)|B0,f being
Function of ((TOP-REAL 2)|B0)|K0,((TOP-REAL 2)|B0);
defpred P[Point of TOP-REAL 2] means ($1`1<=$1`2 & -$1`2<=$1`1 or $1`1>=$1`2
& $1`1<=-$1`2);
the carrier of (TOP-REAL 2)|B0=[#]((TOP-REAL 2)|B0) .= B0 by PRE_TOPC:def 5;
then reconsider K1=K0 as Subset of TOP-REAL 2 by XBOOLE_1:1;
assume
A1: f=Out_In_Sq|K0 & B0=NonZero TOP-REAL 2 & K0={p:(p`1<=p`2 & -p`2<=p`1
or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2};
K0 c= B0
proof
let x be object;
assume x in K0;
then
A2: ex p8 being Point of TOP-REAL 2 st x=p8 &( p8`1<=p8`2 & - p8`2<=p8`1 or
p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2 by A1;
then not x in {0.TOP-REAL 2} by TARSKI:def 1;
hence thesis by A1,A2,XBOOLE_0:def 5;
end;
then
A3: ((TOP-REAL 2)|B0)|K0=(TOP-REAL 2)|K1 by PRE_TOPC:7;
reconsider K1={p7 where p7 is Point of TOP-REAL 2: P[p7]} as Subset of
TOP-REAL 2 from TopSubset;
A4: K1 /\ B0 c= K0
proof
let x be object;
assume
A5: x in K1 /\ B0;
then x in B0 by XBOOLE_0:def 4;
then not x in {0.TOP-REAL 2} by A1,XBOOLE_0:def 5;
then
A6: not x=0.TOP-REAL 2 by TARSKI:def 1;
x in K1 by A5,XBOOLE_0:def 4;
then ex p7 being Point of TOP-REAL 2 st p7=x &( p7`1<=(p7`2) & -(p7`2)<=p7
`1 or p7`1>=(p7`2) & p7`1<=-(p7`2));
hence thesis by A1,A6;
end;
A7: K2 /\ K3 \/ K4 /\ K5 c= K1
proof
let x be object;
assume
A8: x in K2 /\ K3 \/ K4 /\ K5;
now
per cases by A8,XBOOLE_0:def 3;
case
A9: x in K2 /\ K3;
then x in K3 by XBOOLE_0:def 4;
then
A10: ex p8 being Point of TOP-REAL 2 st p8=x & -p8`2<=p8`1;
x in K2 by A9,XBOOLE_0:def 4;
then ex p7 being Point of TOP-REAL 2 st p7=x & p7`1<=(p7`2);
hence thesis by A10;
end;
case
A11: x in K4 /\ K5;
then x in K5 by XBOOLE_0:def 4;
then
A12: ex p8 being Point of TOP-REAL 2 st p8=x & p8`1<= -p8`2;
x in K4 by A11,XBOOLE_0:def 4;
then ex p7 being Point of TOP-REAL 2 st p7=x & p7`1>=(p7`2);
hence thesis by A12;
end;
end;
hence thesis;
end;
K1 c= K2 /\ K3 \/ K4 /\ K5
proof
let x be object;
assume x in K1;
then ex p being Point of TOP-REAL 2 st p=x &( p`1<=p`2 & -p`2 <=p`1 or p`1
>=p`2 & p`1<=-p`2);
then x in K2 & x in K3 or x in K4 & x in K5;
then x in K2 /\ K3 or x in K4 /\ K5 by XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
then K1=K2 /\ K3 \/ K4 /\ K5 by A7;
then
A13: K1 is closed;
K0 c= K1 /\ B0
proof
let x be object;
assume x in K0;
then
A14: ex p being Point of TOP-REAL 2 st x=p &( p`1<=p`2 & -p`2 <=p`1 or p`1
>=p`2 & p`1<=-p`2)& p<>0.TOP-REAL 2 by A1;
then not x in {0.TOP-REAL 2} by TARSKI:def 1;
then
A15: x in B0 by A1,A14,XBOOLE_0:def 5;
x in K1 by A14;
hence thesis by A15,XBOOLE_0:def 4;
end;
then K0=K1 /\ B0 by A4
.=K1 /\ [#]((TOP-REAL 2)|B0) by PRE_TOPC:def 5;
hence thesis by A1,A3,A13,Th37,PRE_TOPC:13;
end;
theorem Th40:
for D being non empty Subset of TOP-REAL 2 st D`={0.TOP-REAL 2}
holds ex h being Function of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h=Out_In_Sq & h
is continuous
proof
set Y1=|[-1,1]|;
reconsider B0= {0.TOP-REAL 2} as Subset of TOP-REAL 2;
let D be non empty Subset of TOP-REAL 2;
assume
A1: D`={0.TOP-REAL 2};
then
A2: D=(B0)` .=(NonZero TOP-REAL 2) by SUBSET_1:def 4;
A3: {p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} c=
the carrier of (TOP-REAL 2)|D
proof
let x be object;
assume
x in {p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0. TOP-REAL 2};
then
A4: ex p st x=p &( p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p `1)& p<>0.
TOP-REAL 2;
now
assume not x in D;
then x in (the carrier of TOP-REAL 2) \ D by A4,XBOOLE_0:def 5;
then x in D` by SUBSET_1:def 4;
hence contradiction by A1,A4,TARSKI:def 1;
end;
then x in [#]((TOP-REAL 2)|D) by PRE_TOPC:def 5;
hence thesis;
end;
A5: NonZero TOP-REAL 2<> {} by Th9;
A6: (1.REAL 2)<>0.TOP-REAL 2 by Lm1,REVROT_1:19;
(1.REAL 2)`2<=(1.REAL 2)`1 & -(1.REAL 2)`1<=(1.REAL 2)`2 or (1.REAL 2)
`2>=(1.REAL 2)`1 & (1.REAL 2)`2<=-(1.REAL 2)`1 by Th5;
then
1.REAL 2 in {p where p is Point of TOP-REAL 2: (p`2<=p`1 & -p`1<=p`2 or
p`2>=p`1 & p`2<=-p`1) & p<>0.TOP-REAL 2} by A6;
then reconsider K0={p:(p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) & p<>0.
TOP-REAL 2} as non empty Subset of (TOP-REAL 2)|D by A3;
A7: K0=[#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 5
.=the carrier of ((TOP-REAL 2)|D)|K0;
A8: {p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} c=
the carrier of (TOP-REAL 2)|D
proof
let x be object;
assume
x in {p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0. TOP-REAL 2};
then
A9: ex p st x=p &( p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p `2)& p<>0.
TOP-REAL 2;
now
assume not x in D;
then x in (the carrier of TOP-REAL 2) \ D by A9,XBOOLE_0:def 5;
then x in D` by SUBSET_1:def 4;
hence contradiction by A1,A9,TARSKI:def 1;
end;
then x in [#]((TOP-REAL 2)|D) by PRE_TOPC:def 5;
hence thesis;
end;
Y1`1=-1 & Y1`2=1 by EUCLID:52;
then
Y1 in {p where p is Point of TOP-REAL 2: (p`1<=p`2 & -p`2<=p`1 or p`1>=
p`2 & p`1<=-p`2) & p<>0.TOP-REAL 2} by Th3;
then reconsider K1={p:(p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2) & p<>0.
TOP-REAL 2} as non empty Subset of (TOP-REAL 2)|D by A8;
A10: K1=[#](((TOP-REAL 2)|D)|K1) by PRE_TOPC:def 5
.=the carrier of ((TOP-REAL 2)|D)|K1;
A11: the carrier of ((TOP-REAL 2)|D) =[#]((TOP-REAL 2)|D)
.=D by PRE_TOPC:def 5;
A12: rng (Out_In_Sq|K1) c= the carrier of ((TOP-REAL 2)|D)|K1
proof
reconsider K10=K1 as Subset of TOP-REAL 2 by A11,XBOOLE_1:1;
let y be object;
A13: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|
K10 holds q`2<>0
proof
let q be Point of TOP-REAL 2;
A14: the carrier of (TOP-REAL 2)|K10=[#]((TOP-REAL 2)|K10)
.=K1 by PRE_TOPC:def 5;
assume q in the carrier of (TOP-REAL 2)|K10;
then
A15: ex p3 being Point of TOP-REAL 2 st q=p3 &( p3`1<=p3`2 & - p3`2<=p3`1
or p3`1>=p3`2 & p3`1<=-p3`2)& p3<>0.TOP-REAL 2 by A14;
now
assume
A16: q`2=0;
then q`1=0 by A15;
hence contradiction by A15,A16,EUCLID:53,54;
end;
hence thesis;
end;
assume y in rng (Out_In_Sq|K1);
then consider x being object such that
A17: x in dom (Out_In_Sq|K1) and
A18: y=(Out_In_Sq|K1).x by FUNCT_1:def 3;
A19: x in (dom Out_In_Sq) /\ K1 by A17,RELAT_1:61;
then
A20: x in K1 by XBOOLE_0:def 4;
K1 c= the carrier of TOP-REAL 2 by A11,XBOOLE_1:1;
then reconsider p=x as Point of TOP-REAL 2 by A20;
A21: Out_In_Sq.p=y by A18,A20,FUNCT_1:49;
set p9=|[p`1/p`2/p`2,1/p`2]|;
K10=[#]((TOP-REAL 2)|K10) by PRE_TOPC:def 5
.=the carrier of ((TOP-REAL 2)|K10);
then
A22: p in the carrier of ((TOP-REAL 2)|K10) by A19,XBOOLE_0:def 4;
A23: now
assume p9=0.TOP-REAL 2;
then p9`2=0 by EUCLID:52,54;
then 0 *p`2=1/p`2*p`2 by EUCLID:52;
hence contradiction by A22,A13,XCMPLX_1:87;
end;
A24: ex px being Point of TOP-REAL 2 st x=px &( px`1<=px`2 & - px`2<=px`1
or px`1>=px`2 & px`1<=-px`2)& px<>0.TOP-REAL 2 by A20;
then
A25: Out_In_Sq.p=|[p`1/p`2/p`2,1/p`2]| by Th14;
now
per cases;
case
A26: p`2>=0;
then p`1/p`2<=p`2/p`2 & (-1 *p`2)/p`2<=p`1/p`2 or p`1>=p`2 & p`1<=-1
* p `2 by A24,XREAL_1:72;
then
A27: p`1/p`2<=1 & (-1)*p`2/p`2<=p`1/p`2 or p`1>=p`2 & p`1<=-1 *p`2 by A22
,A13,XCMPLX_1:60;
then
A28: p`1/p`2<=1 & -1<=p`1/p`2 or p`1/p`2>=1 & p`1/p`2<=(-1)*p`2 /p`2
by A22,A13,A26,XCMPLX_1:89,XREAL_1:72;
p`1/p`2<=1 & -1<=p`1/p`2 or p`1/p`2>=p`2/p`2 & p`1<=-1 *p `2 by A22,A13
,A26,A27,XCMPLX_1:89;
then (-1)/p`2<= p`1/p`2/p`2 by A26,XREAL_1:72;
then
A29: p`1/p`2/p`2 <=1/p`2 & -(1/p`2)<= p`1/p`2/p`2 or p`1/p`2/p`2 >=1/
p`2 & p`1/p`2/p`2<= -(1/p`2) by A26,A28,XREAL_1:72;
p9`2=1/p`2 & p9`1=p`1/p`2/p`2 by EUCLID:52;
hence y in K1 by A21,A23,A25,A29;
end;
case
A30: p`2<0;
then p`1<=p`2 & (-1 *p`2)<=p`1 or p`1/p`2<=p`2/p`2 & p`1/p`2>=(-1 *p
`2)/ p`2 by A24,XREAL_1:73;
then
A31: p`1<=p`2 & (-1 *p`2)<=p`1 or p`1/p`2<=1 & p`1/p`2>=(-1)*p`2/p`2
by A30,XCMPLX_1:60;
then p`1/p`2>=1 & (-1)*p`2/p`2>=p`1/p`2 or p`1/p`2<=1 & p`1/p`2 >=-1
by A30,XCMPLX_1:89;
then (-1)/p`2>= p`1/p`2/p`2 by A30,XREAL_1:73;
then
A32: p`1/p`2/p`2 <=1/p`2 & -(1/p`2)<= p`1/p`2/p`2 or p`1/p`2/p`2 >=1/
p`2 & p`1/p`2/p`2<= -(1/p`2) by A30,A31,XREAL_1:73;
p9`2=1/p`2 & p9`1=p`1/p`2/p`2 by EUCLID:52;
hence y in K1 by A21,A23,A25,A32;
end;
end;
then y in [#](((TOP-REAL 2)|D)|K1) by PRE_TOPC:def 5;
hence thesis;
end;
A33: D c= K0 \/ K1
proof
let x be object;
assume
A34: x in D;
then reconsider px=x as Point of TOP-REAL 2;
not x in {0.TOP-REAL 2} by A2,A34,XBOOLE_0:def 5;
then (px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1) & px<>0.
TOP-REAL 2 or (px`1<=px`2 & -px`2<=px`1 or px`1>=px`2 & px`1<=-px`2) & px<>0.
TOP-REAL 2 by TARSKI:def 1,XREAL_1:26;
then x in K0 or x in K1;
hence thesis by XBOOLE_0:def 3;
end;
A35: NonZero TOP-REAL 2<> {} by Th9;
A36: K1 c= NonZero TOP-REAL 2
proof
let z be object;
assume z in K1;
then
A37: ex p8 being Point of TOP-REAL 2 st p8=z &( p8`1<=p8`2 & - p8`2<=p8`1
or p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2;
then not z in {0.TOP-REAL 2} by TARSKI:def 1;
hence thesis by A37,XBOOLE_0:def 5;
end;
A38: the carrier of ((TOP-REAL 2)|D) =[#](((TOP-REAL 2)|D))
.=(NonZero TOP-REAL 2) by A2,PRE_TOPC:def 5;
A39: rng (Out_In_Sq|K0) c= the carrier of ((TOP-REAL 2)|D)|K0
proof
reconsider K00=K0 as Subset of TOP-REAL 2 by A11,XBOOLE_1:1;
let y be object;
A40: for q being Point of TOP-REAL 2 st q in the carrier of (TOP-REAL 2)|
K00 holds q`1<>0
proof
let q be Point of TOP-REAL 2;
A41: the carrier of (TOP-REAL 2)|K00=[#]((TOP-REAL 2)|K00)
.=K0 by PRE_TOPC:def 5;
assume q in the carrier of (TOP-REAL 2)|K00;
then
A42: ex p3 being Point of TOP-REAL 2 st q=p3 &( p3`2<=p3`1 & - p3`1<=p3`2
or p3`2>=p3`1 & p3`2<=-p3`1)& p3<>0.TOP-REAL 2 by A41;
now
assume
A43: q`1=0;
then q`2=0 by A42;
hence contradiction by A42,A43,EUCLID:53,54;
end;
hence thesis;
end;
assume y in rng (Out_In_Sq|K0);
then consider x being object such that
A44: x in dom (Out_In_Sq|K0) and
A45: y=(Out_In_Sq|K0).x by FUNCT_1:def 3;
A46: x in (dom Out_In_Sq) /\ K0 by A44,RELAT_1:61;
then
A47: x in K0 by XBOOLE_0:def 4;
K0 c= the carrier of TOP-REAL 2 by A11,XBOOLE_1:1;
then reconsider p=x as Point of TOP-REAL 2 by A47;
A48: Out_In_Sq.p=y by A45,A47,FUNCT_1:49;
set p9=|[1/p`1,p`2/p`1/p`1]|;
K00=[#]((TOP-REAL 2)|K00) by PRE_TOPC:def 5
.=the carrier of ((TOP-REAL 2)|K00);
then
A49: p in the carrier of ((TOP-REAL 2)|K00) by A46,XBOOLE_0:def 4;
A50: p9`1=1/p`1 by EUCLID:52;
A51: now
assume p9=0.TOP-REAL 2;
then 0 *p`1=1/p`1*p`1 by A50,EUCLID:52,54;
hence contradiction by A49,A40,XCMPLX_1:87;
end;
A52: ex px being Point of TOP-REAL 2 st x=px &( px`2<=px`1 & - px`1<=px`2
or px`2>=px`1 & px`2<=-px`1)& px<>0.TOP-REAL 2 by A47;
then
A53: Out_In_Sq.p=|[1/p`1,p`2/p`1/p`1]| by Def1;
A54: p`1<>0 by A49,A40;
now
per cases;
case
A55: p`1>=0;
p`2/p`1<=p`1/p`1 & (-1 *p`1)/p`1<=p`2/p`1 or p`2>=p`1 & p`2<=-1 *
p `1 by A52,A55,XREAL_1:72;
then
A56: p`2/p`1<=1 & (-1)*p`1/p`1<=p`2/p`1 or p`2>=p`1 & p`2<=-1 *p`1 by A49
,A40,XCMPLX_1:60;
then p`2/p`1<=1 & -1<=p`2/p`1 or p`2/p`1>=p`1/p`1 & p`2<=-1 *p `1 by
A49,A40,A55,XCMPLX_1:89;
then (-1)/p`1<= p`2/p`1/p`1 by A55,XREAL_1:72;
then
A57: p`2/p`1/p`1 <=1/p`1 & -(1/p`1)<= p`2/p`1/p`1 or p`2/p`1/p`1 >=1/p
`1 & p`2/p`1/p`1<= -(1/p`1) by A54,A55,A56,XREAL_1:72;
p9`1=1/p`1 & p9`2=p`2/p`1/p`1 by EUCLID:52;
hence y in K0 by A48,A51,A53,A57;
end;
case
A58: p`1<0;
A59: -(1/p`1) =(-1)/p`1;
p`2<=p`1 & (-1 *p`1)<=p`2 or p`2/p`1<=p`1/p`1 & p`2/p`1>=(-1 *p`1
)/ p`1 by A52,A58,XREAL_1:73;
then
A60: p`2<=p`1 & (-1 *p`1)<=p`2 or p`2/p`1<=1 & p`2/p`1>=(-1)*p`1/p`1
by A58,XCMPLX_1:60;
then
p`2/p`1>=p`1/p`1 & (-1 *p`1)<=p`2 or p`2/p`1<=1 & p`2/p`1 >=-1 by A58,
XCMPLX_1:89;
then (-1)/p`1>= p`2/p`1/p`1 by A58,XREAL_1:73;
then
A61: p`2/p`1/p`1 <=1/p`1 & (-1)/p`1<= p`2/p`1/p`1
or p`2/p`1/p`1 >=1/p`1 & p`2/p`1/p`1<= -(1/p`1)
by A58,A60,XREAL_1:73;
p9`1=1/p`1 & p9`2=p`2/p`1/p`1 by EUCLID:52;
hence y in K0 by A48,A51,A53,A61,A59;
end;
end;
then y in [#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 5;
hence thesis;
end;
A62: K0 c= NonZero TOP-REAL 2
proof
let z be object;
assume z in K0;
then
A63: ex p8 being Point of TOP-REAL 2 st p8=z &( p8`2<=p8`1 & - p8`1<=p8`2
or p8`2>=p8`1 & p8`2<=-p8`1)& p8<>0.TOP-REAL 2;
then not z in {0.TOP-REAL 2} by TARSKI:def 1;
hence thesis by A63,XBOOLE_0:def 5;
end;
dom (Out_In_Sq|K0)= dom (Out_In_Sq) /\ K0 by RELAT_1:61
.=(NonZero TOP-REAL 2) /\ K0 by A5,FUNCT_2:def 1
.=K0 by A62,XBOOLE_1:28;
then reconsider
f=Out_In_Sq|K0 as Function of ((TOP-REAL 2)|D)|K0,((TOP-REAL 2)|D
) by A7,A39,FUNCT_2:2,XBOOLE_1:1;
A64: K1=[#](((TOP-REAL 2)|D)|K1) by PRE_TOPC:def 5;
dom (Out_In_Sq|K1)= dom (Out_In_Sq) /\ K1 by RELAT_1:61
.=(NonZero TOP-REAL 2) /\ K1 by A35,FUNCT_2:def 1
.=K1 by A36,XBOOLE_1:28;
then reconsider
g=Out_In_Sq|K1 as Function of ((TOP-REAL 2)|D)|K1, ((TOP-REAL 2)|
D) by A10,A12,FUNCT_2:2,XBOOLE_1:1;
A65: dom g=K1 by A10,FUNCT_2:def 1;
g=Out_In_Sq|K1;
then
A66: K1 is closed by A2,Th39;
A67: K0=[#](((TOP-REAL 2)|D)|K0) by PRE_TOPC:def 5;
A68: for x be object st x in ([#]((((TOP-REAL 2)|D)|K0))) /\ ([#] ((((TOP-REAL
2)|D)|K1))) holds f.x = g.x
proof
let x be object;
assume
A69: x in ([#]((((TOP-REAL 2)|D)|K0))) /\ ([#] ((((TOP-REAL 2)|D)|K1) ));
then x in K0 by A67,XBOOLE_0:def 4;
then f.x=Out_In_Sq.x by FUNCT_1:49;
hence thesis by A64,A69,FUNCT_1:49;
end;
f=Out_In_Sq|K0;
then
A70: K0 is closed by A2,Th38;
A71: dom f=K0 by A7,FUNCT_2:def 1;
D= [#]((TOP-REAL 2)|D) by PRE_TOPC:def 5;
then
A72: ([#](((TOP-REAL 2)|D)|K0)) \/ ([#](((TOP-REAL 2)|D)|K1)) = [#]((
TOP-REAL 2)|D) by A67,A64,A33;
A73: f is continuous & g is continuous by A2,Th38,Th39;
then consider h being Function of (TOP-REAL 2)|D,(TOP-REAL 2)|D such that
A74: h= f+*g and
h is continuous by A67,A64,A72,A70,A66,A68,Th1;
K0=[#](((TOP-REAL 2)|D)|K0) & K1=[#](((TOP-REAL 2)|D)|K1) by PRE_TOPC:def 5;
then
A75: f tolerates g by A68,A71,A65,PARTFUN1:def 4;
A76: for x being object st x in dom h holds h.x=Out_In_Sq.x
proof
let x be object;
assume
A77: x in dom h;
then reconsider p=x as Point of TOP-REAL 2 by A38,XBOOLE_0:def 5;
not x in {0.TOP-REAL 2} by A38,A77,XBOOLE_0:def 5;
then
A78: x <>0.TOP-REAL 2 by TARSKI:def 1;
now
per cases;
case
A79: x in K0;
h.p=(g+*f).p by A74,A75,FUNCT_4:34
.=f.p by A71,A79,FUNCT_4:13;
hence thesis by A79,FUNCT_1:49;
end;
case
not x in K0;
then not (p`2<=p`1 & -p`1<=p`2 or p`2>=p`1 & p`2<=-p`1) by A78;
then p`1<=p`2 & -p`2<=p`1 or p`1>=p`2 & p`1<=-p`2 by XREAL_1:26;
then
A80: x in K1 by A78;
then Out_In_Sq.p=g.p by FUNCT_1:49;
hence thesis by A74,A65,A80,FUNCT_4:13;
end;
end;
hence thesis;
end;
dom h=the carrier of ((TOP-REAL 2)|D) & dom Out_In_Sq=the carrier of (
( TOP-REAL 2)|D) by A38,FUNCT_2:def 1;
then f+*g=Out_In_Sq by A74,A76,FUNCT_1:2;
hence thesis by A67,A64,A72,A70,A73,A66,A68,Th1;
end;
theorem Th41:
for B,K0,Kb being Subset of TOP-REAL 2 st B={0.TOP-REAL 2} & K0=
{p: -1<p`1 & p`1<1 & -1<p`2 & p`2<1} & Kb={q: -1=q`1 & -1<=q`2 & q`2<=1 or q`1=
1 & -1<=q`2 & q`2<=1 or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q`1 & q`1<=1}
ex f being Function of (TOP-REAL 2)|B`,(TOP-REAL 2)|B` st f is continuous & f
is one-to-one & (for t being Point of TOP-REAL 2 st t in K0 & t<>0.TOP-REAL 2
holds not f.t in K0 \/ Kb) &(for r being Point of TOP-REAL 2 st not r in K0 \/
Kb holds f.r in K0) & for s being Point of TOP-REAL 2 st s in Kb holds f.s=s
proof
set K1a={p8 where p8 is Point of TOP-REAL 2: (p8`1<=p8`2 & -p8`2<=p8`1 or p8
`1>=p8`2 & p8`1<=-p8`2) & p8<>0.TOP-REAL 2 };
set K0a={p8 where p8 is Point of TOP-REAL 2: (p8`2<=p8`1 & -p8`1<=p8`2 or p8
`2>=p8`1 & p8`2<=-p8`1) & p8<>0.TOP-REAL 2};
let B,K0,Kb be Subset of TOP-REAL 2;
assume
A1: B={0.TOP-REAL 2} & K0={p: -1<p`1 & p`1<1 & -1<p`2 & p`2<1} & Kb={q:
-1=q`1 & -1<=q`2 & q`2<=1 or q`1=1 & -1<=q`2 & q`2<=1 or -1=q`2 & -1<=q`1 & q`1
<=1 or 1=q`2 & -1<=q`1 & q`1<=1};
then reconsider D=B` as non empty Subset of TOP-REAL 2 by Th9;
A2: D`={0.TOP-REAL 2} by A1;
A3: B`=NonZero TOP-REAL 2 by A1,SUBSET_1:def 4;
A4: for t being Point of TOP-REAL 2 st t in K0 & t<>0.TOP-REAL 2 holds not
Out_In_Sq.t in K0 \/ Kb
proof
let t be Point of TOP-REAL 2;
assume that
A5: t in K0 and
A6: t<>0.TOP-REAL 2;
A7: ex p3 being Point of TOP-REAL 2 st p3=t & -1<p3`1 & p3 `1<1 & -1<p3`2
& p3`2<1 by A1,A5;
now
assume
A8: Out_In_Sq.t in K0 \/ Kb;
now
per cases by A8,XBOOLE_0:def 3;
case
Out_In_Sq.t in K0;
then consider p4 being Point of TOP-REAL 2 such that
A9: p4=Out_In_Sq.t and
A10: -1<p4`1 and
A11: p4`1<1 and
A12: -1<p4`2 and
A13: p4`2<1 by A1;
now
per cases;
case
A14: t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1;
then Out_In_Sq.t=|[1/t`1,t`2/t`1/t`1]| by A6,Def1;
then
A15: p4`1=1/t`1 by A9,EUCLID:52;
now
per cases;
case
A16: t`1>=0;
now
per cases by A16;
case
A17: t`1>0;
then 1/t`1*t`1<1 *t`1 by A11,A15,XREAL_1:68;
hence contradiction by A7,A17,XCMPLX_1:87;
end;
case
A18: t`1=0;
then t`2=0 by A14;
hence contradiction by A6,A18,EUCLID:53,54;
end;
end;
hence contradiction;
end;
case
A19: t`1<0;
then (-1)*t`1>1/t`1*t`1 by A10,A15,XREAL_1:69;
then (-1)*t`1>1 by A19,XCMPLX_1:87;
then --t`1<=-1 by XREAL_1:24;
hence contradiction by A7;
end;
end;
hence contradiction;
end;
case
A20: not(t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1);
then Out_In_Sq.t=|[t`1/t`2/t`2,1/t`2]| by A6,Def1;
then
A21: p4`2=1/t`2 by A9,EUCLID:52;
now
per cases;
case
A22: t`2>=0;
now
per cases by A22;
case
A23: t`2>0;
then 1/t`2*t`2<1 *t`2 by A13,A21,XREAL_1:68;
hence contradiction by A7,A23,XCMPLX_1:87;
end;
case
t`2=0;
hence contradiction by A20;
end;
end;
hence contradiction;
end;
case
A24: t`2<0;
then (-1)*t`2>1/t`2*t`2 by A12,A21,XREAL_1:69;
then (-1)*t`2>1 by A24,XCMPLX_1:87;
then --t`2<=-1 by XREAL_1:24;
hence contradiction by A7;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
case
Out_In_Sq.t in Kb;
then consider p4 being Point of TOP-REAL 2 such that
A25: p4=Out_In_Sq.t and
A26: -1=p4`1 & -1<=p4`2 & p4`2<=1 or p4`1=1 & -1<=p4`2 & p4`2<=
1 or -1 =p4`2 & -1<=p4`1 & p4`1<=1 or 1=p4`2 & -1<=p4`1 & p4`1<=1 by A1;
now
per cases;
case
A27: t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1;
then
A28: Out_In_Sq.t=|[1/t`1,t`2/t`1/t`1]| by A6,Def1;
then
A29: p4`1=1/t`1 by A25,EUCLID:52;
now
per cases by A26;
case
-1=p4`1 & -1<=p4`2 & p4`2<=1;
then
A30: (t`1)*(t`1)" =-t`1 by A29;
now
per cases;
case
t`1<>0;
then -t`1=1 by A30,XCMPLX_0:def 7;
hence contradiction by A7;
end;
case
A31: t`1=0;
then t`2=0 by A27;
hence contradiction by A6,A31,EUCLID:53,54;
end;
end;
hence contradiction;
end;
case
p4`1=1 & -1<=p4`2 & p4`2<=1;
then
A32: (t`1)*(t`1)"=t`1 by A29;
now
per cases;
case
t`1<>0;
hence contradiction by A7,A32,XCMPLX_0:def 7;
end;
case
A33: t`1=0;
then t`2=0 by A27;
hence contradiction by A6,A33,EUCLID:53,54;
end;
end;
hence contradiction;
end;
case
A34: -1=p4`2 & -1<=p4`1 & p4`1<=1;
reconsider K01=K0a as non empty Subset of (TOP-REAL 2)|D by
A2,Th17;
A35: the carrier of ((TOP-REAL 2)|D)|K01=[#](((TOP-REAL 2)|
D)|K01)
.=K01 by PRE_TOPC:def 5;
A36: dom (Out_In_Sq|K01)=(dom Out_In_Sq) /\ K01 by RELAT_1:61
.=D /\ K01 by A3,FUNCT_2:def 1
.=[#]((TOP-REAL 2)|D) /\ K01 by PRE_TOPC:def 5
.=(the carrier of ((TOP-REAL 2)|D)) /\ K01
.=K01 by XBOOLE_1:28;
t in K01 by A6,A27;
then
A37: (Out_In_Sq|K01).t in rng (Out_In_Sq|K01) by A36,FUNCT_1:3;
rng (Out_In_Sq|K01) c= the carrier of ((TOP-REAL 2)|D)
|K01 by Th15;
then
A38: (Out_In_Sq|K01).t in the carrier of (( TOP-REAL 2)|D)|
K01 by A37;
t in K01 by A6,A27;
then Out_In_Sq.t in K0a by A38,A35,FUNCT_1:49;
then
A39: ex p5 being Point of TOP-REAL 2 st p5=p4 &( p5`2<=p5`1
& -p5`1<=p5`2 or p5`2>=p5`1 & p5`2<=-p5`1)& p5<>0.TOP-REAL 2 by A25;
now
per cases by A34,A39,XREAL_1:24;
case
A40: p4`1>=1;
then t`2/t`1/t`1=(t`2/t`1)*1 by A29,A34,XXREAL_0:1
.=t`2*1 by A29,A34,A40,XXREAL_0:1
.=t`2;
hence contradiction by A7,A25,A28,A34,EUCLID:52;
end;
case
A41: -1>=p4`1;
then t`2/t`1/t`1=(t`2/t`1)*(-1) by A29,A34,XXREAL_0:1
.=-(t`2/t`1)
.=-(t`2*(-1)) by A29,A34,A41,XXREAL_0:1
.=t`2;
hence contradiction by A7,A25,A28,A34,EUCLID:52;
end;
end;
hence contradiction;
end;
case
A42: 1=p4`2 & -1<=p4`1 & p4`1<=1;
reconsider K01=K0a as non empty Subset of (TOP-REAL 2)|D by
A2,Th17;
t in K01 by A6,A27;
then
A43: Out_In_Sq.t=(Out_In_Sq|K01).t by FUNCT_1:49;
dom (Out_In_Sq|K01)=(dom Out_In_Sq) /\ K01 by RELAT_1:61
.=D /\ K01 by A3,FUNCT_2:def 1
.=[#]((TOP-REAL 2)|D) /\ K01 by PRE_TOPC:def 5
.=(the carrier of ((TOP-REAL 2)|D)) /\ K01
.=K01 by XBOOLE_1:28;
then t in dom (Out_In_Sq|K01) by A6,A27;
then
A44: (Out_In_Sq|K01).t in rng (Out_In_Sq|K01) by FUNCT_1:3;
rng (Out_In_Sq|K01) c= the carrier of ((TOP-REAL 2)|D)
|K01 by Th15;
then
A45: (Out_In_Sq|K01).t in the carrier of (( TOP-REAL 2)|D)|
K01 by A44;
the carrier of ((TOP-REAL 2)|D)|K01=[#](((TOP-REAL 2)|
D)|K01)
.=K01 by PRE_TOPC:def 5;
then
A46: ex p5 being Point of TOP-REAL 2 st p5=p4 &( p5`2<=p5`1
& -p5`1<=p5`2 or p5`2>=p5`1 & p5`2<=-p5`1)& p5<>0.TOP-REAL 2 by A25,A45,A43;
now
per cases by A42,A46,XREAL_1:25;
case
A47: p4`1>=1;
then t`2/t`1/t`1=(t`2/t`1)*1 by A29,A42,XXREAL_0:1
.=t`2*1 by A29,A42,A47,XXREAL_0:1
.=t`2;
hence contradiction by A7,A25,A28,A42,EUCLID:52;
end;
case
A48: -1>=p4`1;
then t`2/t`1/t`1=(t`2/t`1)*(-1) by A29,A42,XXREAL_0:1
.=-(t`2/t`1)
.=-(t`2*(-1)) by A29,A42,A48,XXREAL_0:1
.=t`2;
hence contradiction by A7,A25,A28,A42,EUCLID:52;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
case
A49: not(t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1);
then
A50: Out_In_Sq.t=|[t`1/t`2/t`2,1/t`2]| by A6,Def1;
then
A51: p4`2=1/t`2 by A25,EUCLID:52;
now
per cases by A26;
case
-1=p4`2 & -1<=p4`1 & p4`1<=1;
then
A52: (t`2)*(t`2)"=-t`2 by A51;
now
per cases;
case
t`2<>0;
then -t`2=1 by A52,XCMPLX_0:def 7;
hence contradiction by A7;
end;
case
t`2=0;
hence contradiction by A49;
end;
end;
hence contradiction;
end;
case
p4`2=1 & -1<=p4`1 & p4`1<=1;
then
A53: (t`2)*(t`2)" =t`2 by A51;
now
per cases;
case
t`2<>0;
hence contradiction by A7,A53,XCMPLX_0:def 7;
end;
case
t`2=0;
hence contradiction by A49;
end;
end;
hence contradiction;
end;
case
A54: -1=p4`1 & -1<=p4`2 & p4`2<=1;
reconsider K11=K1a as non empty Subset of (TOP-REAL 2)|D by
A2,Th18;
A55: dom (Out_In_Sq|K11)=(dom Out_In_Sq) /\ K11 by RELAT_1:61
.=D /\ K11 by A3,FUNCT_2:def 1
.=[#]((TOP-REAL 2)|D) /\ K11 by PRE_TOPC:def 5
.=(the carrier of ((TOP-REAL 2)|D)) /\ K11
.=K11 by XBOOLE_1:28;
A56: t`1<=t`2 & -t`2<=t`1 or t`1>=t`2 & t`1<=-t`2 by A49,Th13;
then t in K11 by A6;
then
A57: Out_In_Sq.t=(Out_In_Sq|K11).t by FUNCT_1:49;
t in K11 by A6,A56;
then
A58: (Out_In_Sq|K11).t in rng (Out_In_Sq|K11) by A55,FUNCT_1:3;
rng (Out_In_Sq|K11) c= the carrier of ((TOP-REAL 2)|D)
|K11 by Th16;
then
A59: (Out_In_Sq|K11).t in the carrier of (( TOP-REAL 2)|D)|
K11 by A58;
the carrier of ((TOP-REAL 2)|D)|K11=[#](((TOP-REAL 2)|
D)|K11)
.=K11 by PRE_TOPC:def 5;
then
A60: ex p5 being Point of TOP-REAL 2 st p5=p4 &( p5`1<=p5`2
& -p5`2<=p5`1 or p5`1>=p5`2 & p5`1<=-p5`2)& p5<>0.TOP-REAL 2 by A25,A59,A57;
now
per cases by A54,A60,XREAL_1:24;
case
A61: p4`2>=1;
then t`1/t`2/t`2=(t`1/t`2)*1 by A51,A54,XXREAL_0:1
.=t`1*1 by A51,A54,A61,XXREAL_0:1
.=t`1;
hence contradiction by A7,A25,A50,A54,EUCLID:52;
end;
case
A62: -1>=p4`2;
then t`1/t`2/t`2=(t`1/t`2)*(-1) by A51,A54,XXREAL_0:1
.=-(t`1/t`2)
.=-(t`1*(-1)) by A51,A54,A62,XXREAL_0:1
.=t`1;
hence contradiction by A7,A25,A50,A54,EUCLID:52;
end;
end;
hence contradiction;
end;
case
A63: 1=p4`1 & -1<=p4`2 & p4`2<=1;
reconsider K11=K1a as non empty Subset of (TOP-REAL 2)|D by
A2,Th18;
A64: the carrier of ((TOP-REAL 2)|D)|K11=[#](((TOP-REAL 2)|
D)|K11)
.=K11 by PRE_TOPC:def 5;
A65: dom (Out_In_Sq|K11)=(dom Out_In_Sq) /\ K11 by RELAT_1:61
.=D /\ K11 by A3,FUNCT_2:def 1
.=[#]((TOP-REAL 2)|D) /\ K11 by PRE_TOPC:def 5
.=(the carrier of ((TOP-REAL 2)|D)) /\ K11
.=K11 by XBOOLE_1:28;
A66: t`1<=t`2 & -t`2<=t`1 or t`1>=t`2 & t`1<=-t`2 by A49,Th13;
then t in K11 by A6;
then
A67: (Out_In_Sq|K11).t in rng (Out_In_Sq|K11) by A65,FUNCT_1:3;
rng (Out_In_Sq|K11) c= the carrier of ((TOP-REAL 2)|D)
|K11 by Th16;
then
A68: (Out_In_Sq|K11).t in the carrier of (( TOP-REAL 2)|D)|
K11 by A67;
t in K11 by A6,A66;
then Out_In_Sq.t in K1a by A68,A64,FUNCT_1:49;
then
A69: ex p5 being Point of TOP-REAL 2 st p5=p4 &( p5`1<=p5`2
& -p5`2<=p5`1 or p5`1>=p5`2 & p5`1<=-p5`2)& p5<>0.TOP-REAL 2 by A25;
now
per cases by A63,A69,XREAL_1:25;
case
A70: p4`2>=1;
then t`1/t`2/t`2=(t`1/t`2)*1 by A51,A63,XXREAL_0:1
.=t`1*1 by A51,A63,A70,XXREAL_0:1
.=t`1;
hence contradiction by A7,A25,A50,A63,EUCLID:52;
end;
case
A71: -1>=p4`2;
then t`1/t`2/t`2=(t`1/t`2)*(-1) by A51,A63,XXREAL_0:1
.=-(t`1/t`2)
.=-(t`1*(-1)) by A51,A63,A71,XXREAL_0:1
.=t`1;
hence contradiction by A7,A25,A50,A63,EUCLID:52;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
hence thesis;
end;
A72: for t being Point of TOP-REAL 2 st not t in K0 \/ Kb holds Out_In_Sq.t
in K0
proof
let t be Point of TOP-REAL 2;
assume
A73: not t in K0 \/ Kb;
then
A74: not t in K0 by XBOOLE_0:def 3;
then
A75: not t=0.TOP-REAL 2 by A1,Th3;
then not t in {0.TOP-REAL 2} by TARSKI:def 1;
then t in NonZero TOP-REAL 2 by XBOOLE_0:def 5;
then Out_In_Sq.t in NonZero TOP-REAL 2 by FUNCT_2:5;
then reconsider p4=Out_In_Sq.t as Point of TOP-REAL 2;
A76: not t in Kb by A73,XBOOLE_0:def 3;
now
per cases;
case
A77: t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1;
A78: now
per cases;
case
A79: t`1>0;
now
per cases;
case
A80: t`2>0;
-1>=t`1 or t`1>=1 or -1>=t`2 or t`2>=1 by A1,A74;
then
A81: t`1>=1 by A77,A79,A80,XXREAL_0:2;
not t`1=1 by A1,A76,A77;
then
A82: t`1>1 by A81,XXREAL_0:1;
then t`1<(t`1)^2 by SQUARE_1:14;
then (t`2)<(t`1)^2 by A77,A79,XXREAL_0:2;
then t`2/t`1<(t`1)^2/t`1 by A79,XREAL_1:74;
then t`2/t`1<(t`1) by A79,XCMPLX_1:89;
then
A83: t`2/t`1/t`1<(t`1)/t`1 by A79,XREAL_1:74;
0<t`2/t`1 by A79,A80,XREAL_1:139;
then
A84: (-1)*t`1/t`1< t`2/t`1/t`1 by A79,XREAL_1:74;
t`1/t`1>1/t`1 by A82,XREAL_1:74;
hence -1<1/t`1 & 1/t`1<1 & -1< t`2/t`1/t`1 & t`2/t`1/t`1<1 by
A79,A84,A83,XCMPLX_1:60,89;
end;
case
A85: t`2<=0;
A86: now
assume t`1<1;
then -1>=t`2 by A1,A74,A79,A85;
then -t`1<=-1 by A77,A79,XXREAL_0:2;
hence t`1>=1 by XREAL_1:24;
end;
not t`1=1 by A1,A76,A77;
then
A87: t`1>1 by A86,XXREAL_0:1;
then
A88: t`1<(t`1)^2 by SQUARE_1:14;
--t`1>=-t`2 by A77,A79,XREAL_1:24;
then (t`1)^2 >-t`2 by A88,XXREAL_0:2;
then (t`1)^2/t`1 >(-t`2)/t`1 by A79,XREAL_1:74;
then t`1>-(t`2/t`1) by A79,XCMPLX_1:89;
then -t`1<--(t`2/t`1) by XREAL_1:24;
then
A89: (-1)*t`1/t`1< t`2/t`1/t`1 by A79,XREAL_1:74;
t`1/t`1>1/t`1 by A87,XREAL_1:74;
hence -1<1/t`1 & 1/t`1<1 & -1< t`2/t`1/t`1 & t`2/t`1/t`1<1 by
A79,A85,A89,XCMPLX_1:60,89;
end;
end;
hence -1<1/t`1 & 1/t`1<1 & -1< t`2/t`1/t`1 & t`2/t`1/t`1<1;
end;
case
A90: t`1<=0;
now
per cases by A90;
case
A91: t`1=0;
then t`2=0 by A77;
hence contradiction by A1,A74,A91;
end;
case
A92: t`1<0;
now
per cases;
case
A93: t`2>0;
-1>=t`1 or t`1>=1 or -1>=t`2 or t`2>=1 by A1,A74;
then t`1<=-1 or 1<=-t`1 by A77,A92,XXREAL_0:2;
then
A94: t`1<=-1 or -1>=--t`1 by XREAL_1:24;
not t`1=-1 by A1,A76,A77;
then
A95: t`1<-1 by A94,XXREAL_0:1;
then t`1/t`1>(-1)/t`1 by XREAL_1:75;
then
A96: -(t`1/t`1)<-((-1)/t`1) by XREAL_1:24;
-t`1<(t`1)^2 by A95,SQUARE_1:46;
then (t`2)<(t`1)^2 by A77,A92,XXREAL_0:2;
then t`2/t`1>(t`1)^2/t`1 by A92,XREAL_1:75;
then t`2/t`1>(t`1) by A92,XCMPLX_1:89;
then
A97: t`2/t`1/t`1<(t`1)/t`1 by A92,XREAL_1:75;
0>t`2/t`1 by A92,A93,XREAL_1:142;
then (-1)*t`1/t`1< t`2/t`1/t`1 by A92,XREAL_1:75;
hence -1<1/t`1 & 1/t`1<1 & -1< t`2/t`1/t`1 & t`2/t`1/t`1<1
by A92,A96,A97,XCMPLX_1:60;
end;
case
A98: t`2<=0;
then -1>=t`1 or -1>=t`2 by A1,A74,A92;
then
A99: t`1<=-1 by A77,A92,XXREAL_0:2;
not t`1=-1 by A1,A76,A77;
then
A100: t`1< -1 by A99,XXREAL_0:1;
then
A101: -t`1<(t`1)^2 by SQUARE_1:46;
t`1<=t`2 by A77,A92;
then -t`1>=-t`2 by XREAL_1:24;
then (t`1)^2 >-t`2 by A101,XXREAL_0:2;
then (t`1)^2/t`1 <(-t`2)/t`1 by A92,XREAL_1:75;
then t`1<-(t`2/t`1) by A92,XCMPLX_1:89;
then -t`1>--(t`2/t`1) by XREAL_1:24;
then
A102: (-1)*t`1/t`1< t`2/t`1/t`1 by A92,XREAL_1:75;
t`1/t`1> (-1)/t`1 by A100,XREAL_1:75;
then 1> (-1)/t`1 by A92,XCMPLX_1:60;
then -1<-(-1)/t`1 by XREAL_1:24;
hence -1<1/t`1 & 1/t`1<1 & -1< t`2/t`1/t`1 & t`2/t`1/t`1<1
by A92,A98,A102,XCMPLX_1:89;
end;
end;
hence -1<1/t`1 & 1/t`1<1 & -1< t`2/t`1/t`1 & t`2/t`1/t`1<1;
end;
end;
hence -1<1/t`1 & 1/t`1<1 & -1< t`2/t`1/t`1 & t`2/t`1/t`1<1;
end;
end;
Out_In_Sq.t=|[1/t`1,t`2/t`1/t`1]| by A75,A77,Def1;
then p4`1=1/t`1 & p4`2=t`2/t`1/t`1 by EUCLID:52;
hence thesis by A1,A78;
end;
case
A103: not(t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1);
then
A104: t`1<=t`2 & -t`2<=t`1 or t`1>=t`2 & t`1<=-t`2 by Th13;
A105: now
per cases;
case
A106: t`2>0;
now
per cases;
case
A107: t`1>0;
A108: -1>=t`2 or t`2>=1 or -1>=t`1 or t`1>=1 by A1,A74;
not t`2=1 by A1,A76,A103,A107;
then
A109: t`2>1 by A103,A106,A107,A108,XXREAL_0:1,2;
then t`2<(t`2)^2 by SQUARE_1:14;
then (t`1)<(t`2)^2 by A103,A106,XXREAL_0:2;
then t`1/t`2<(t`2)^2/t`2 by A106,XREAL_1:74;
then t`1/t`2<(t`2) by A106,XCMPLX_1:89;
then
A110: t`1/t`2/t`2<(t`2)/t`2 by A106,XREAL_1:74;
0<t`1/t`2 by A106,A107,XREAL_1:139;
then
A111: (-1)*t`2/t`2< t`1/t`2/t`2 by A106,XREAL_1:74;
t`2/t`2>1/t`2 by A109,XREAL_1:74;
hence -1<1/t`2 & 1/t`2<1 & -1< t`1/t`2/t`2 & t`1/t`2/t`2<1 by
A106,A111,A110,XCMPLX_1:60,89;
end;
case
A112: t`1<=0;
A113: now
assume t`2<1;
then -1>=t`1 by A1,A74,A106,A112;
then -t`2<=-1 by A104,A106,XXREAL_0:2;
hence t`2>=1 by XREAL_1:24;
end;
not t`2=1 by A1,A76,A104;
then
A114: t`2>1 by A113,XXREAL_0:1;
then t`2<(t`2)^2 by SQUARE_1:14;
then (t`2)^2 >-t`1 by A103,A106,XXREAL_0:2;
then (t`2)^2/t`2 >(-t`1)/t`2 by A106,XREAL_1:74;
then t`2>-(t`1/t`2) by A106,XCMPLX_1:89;
then -t`2<--(t`1/t`2) by XREAL_1:24;
then
A115: (-1)*t`2/t`2< t`1/t`2/t`2 by A106,XREAL_1:74;
t`2/t`2>1/t`2 by A114,XREAL_1:74;
hence -1<1/t`2 & 1/t`2<1 & -1< t`1/t`2/t`2 & t`1/t`2/t`2<1 by
A106,A112,A115,XCMPLX_1:60,89;
end;
end;
hence -1<1/t`2 & 1/t`2<1 & -1< t`1/t`2/t`2 & t`1/t`2/t`2<1;
end;
case
A116: t`2<=0;
then
A117: t`2<0 by A103;
A118: t`1<=t`2 or t`1<=-t`2 by A103,Th13;
now
per cases;
case
A119: t`1>0;
-1>=t`2 or t`2>=1 or -1>=t`1 or t`1>=1 by A1,A74;
then t`2<=-1 or 1<=-t`2 by A104,A116,XXREAL_0:2;
then
A120: t`2<=-1 or -1>=--t`2 by XREAL_1:24;
not t`2=-1 by A1,A76,A104;
then
A121: t`2<-1 by A120,XXREAL_0:1;
then t`2/t`2>(-1)/t`2 by XREAL_1:75;
then
A122: -(t`2/t`2)<-((-1)/t`2) by XREAL_1:24;
-t`2<(t`2)^2 by A121,SQUARE_1:46;
then (t`1)<(t`2)^2 by A116,A118,XXREAL_0:2;
then t`1/t`2>(t`2)^2/t`2 by A117,XREAL_1:75;
then t`1/t`2>(t`2) by A117,XCMPLX_1:89;
then
A123: t`1/t`2/t`2<(t`2)/t`2 by A117,XREAL_1:75;
0>t`1/t`2 by A117,A119,XREAL_1:142;
then (-1)*t`2/t`2< t`1/t`2/t`2 by A117,XREAL_1:75;
hence -1<1/t`2 & 1/t`2<1 & -1< t`1/t`2/t`2 & t`1/t`2/t`2<1 by
A117,A122,A123,XCMPLX_1:60;
end;
case
A124: t`1<=0;
A125: not t`2=-1 by A1,A76,A104;
-1>=t`2 or -1>=t`1 by A1,A74,A116,A124;
then
A126: t`2< -1 by A103,A116,A125,XXREAL_0:1,2;
then
A127: -t`2<(t`2)^2 by SQUARE_1:46;
-t`2>=-t`1 by A103,A116,XREAL_1:24;
then (t`2)^2 >-t`1 by A127,XXREAL_0:2;
then (t`2)^2/t`2 <(-t`1)/t`2 by A117,XREAL_1:75;
then t`2<-(t`1/t`2) by A117,XCMPLX_1:89;
then -t`2>--(t`1/t`2) by XREAL_1:24;
then
A128: (-1)*t`2/t`2< t`1/t`2/t`2 by A117,XREAL_1:75;
t`2/t`2> (-1)/t`2 by A126,XREAL_1:75;
then 1> (-1)/t`2 by A117,XCMPLX_1:60;
then -1<-(-1)/t`2 by XREAL_1:24;
hence -1<1/t`2 & 1/t`2<1 & -1< t`1/t`2/t`2 & t`1/t`2/t`2<1 by
A103,A116,A124,A128,XCMPLX_1:89;
end;
end;
hence -1<1/t`2 & 1/t`2<1 & -1< t`1/t`2/t`2 & t`1/t`2/t`2<1;
end;
end;
Out_In_Sq.t=|[t`1/t`2/t`2,1/t`2]| by A75,A103,Def1;
then p4`2=1/t`2 & p4`1=t`1/t`2/t`2 by EUCLID:52;
hence thesis by A1,A105;
end;
end;
hence thesis;
end;
A129: D =(NonZero TOP-REAL 2) by A1,SUBSET_1:def 4;
for x1,x2 being object st x1 in dom Out_In_Sq & x2 in dom Out_In_Sq &
Out_In_Sq.x1=Out_In_Sq.x2 holds x1=x2
proof
A130: K1a c= D
proof
let x be object;
assume x in K1a;
then
A131: ex p8 being Point of TOP-REAL 2 st x=p8 &( p8`1<=p8`2 & - p8`2<=p8`1
or p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2;
then not x in {0.TOP-REAL 2} by TARSKI:def 1;
hence thesis by A3,A131,XBOOLE_0:def 5;
end;
A132: (1.REAL 2)<>0.TOP-REAL 2 by Lm1,REVROT_1:19;
(1.REAL 2)`1<=(1.REAL 2)`2 & -(1.REAL 2)`2<=(1.REAL 2)`1 or (1.REAL 2
) `1>=(1.REAL 2)`2 & (1.REAL 2)`1<=-(1.REAL 2)`2 by Th5;
then
A133: 1.REAL 2 in K1a by A132;
the carrier of (TOP-REAL 2)|D=[#]((TOP-REAL 2)|D) .=D by PRE_TOPC:def 5;
then reconsider K11=K1a as non empty Subset of ((TOP-REAL 2)|D) by A133
,A130;
reconsider K01=K0a as non empty Subset of ((TOP-REAL 2)|D) by A2,Th17;
let x1,x2 be object;
assume that
A134: x1 in dom Out_In_Sq and
A135: x2 in dom Out_In_Sq and
A136: Out_In_Sq.x1=Out_In_Sq.x2;
NonZero TOP-REAL 2<>{} by Th9;
then
A137: dom Out_In_Sq=NonZero TOP-REAL 2 by FUNCT_2:def 1;
then
A138: x2 in D by A1,A135,SUBSET_1:def 4;
reconsider p1=x1,p2=x2 as Point of TOP-REAL 2 by A134,A135,XBOOLE_0:def 5;
A139: D c= K01 \/ K11
proof
let x be object;
assume
A140: x in D;
then reconsider px=x as Point of TOP-REAL 2;
not x in {0.TOP-REAL 2} by A129,A140,XBOOLE_0:def 5;
then (px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1) & px<>0.
TOP-REAL 2 or (px`1<=px`2 & -px`2<=px`1 or px`1>=px`2 & px`1<=-px`2) & px<>0.
TOP-REAL 2 by TARSKI:def 1,XREAL_1:25;
then x in K01 or x in K11;
hence thesis by XBOOLE_0:def 3;
end;
A141: x1 in D by A1,A134,A137,SUBSET_1:def 4;
now
per cases by A139,A141,XBOOLE_0:def 3;
case
x1 in K01;
then
A142: ex p7 being Point of TOP-REAL 2 st p1=p7 &( p7`2<=p7`1 & -p7`1<=p7
`2 or p7`2>=p7`1 & p7`2<=-p7`1)& p7<>0.TOP-REAL 2;
then
A143: Out_In_Sq.p1=|[1/p1`1,p1`2/p1`1/p1`1]| by Def1;
now
per cases by A139,A138,XBOOLE_0:def 3;
case
x2 in K0a;
then
ex p8 being Point of (TOP-REAL 2) st p2=p8 &( p8`2<=p8`1 & -p8
`1<=p8`2 or p8`2>=p8`1 & p8`2<=-p8`1)& p8<>0.TOP-REAL 2;
then
A144: |[1/p2`1,p2`2/p2`1/p2`1]| =|[1/p1`1,p1`2/p1`1/p1`1]| by A136,A143
,Def1;
A145: p1=|[p1`1,p1`2]| by EUCLID:53;
set qq=|[1/p2`1,p2`2/p2`1/p2`1]|;
A146: (1/p1`1)"=(p1`1)"" .=p1`1;
A147: now
assume
A148: p1`1=0;
then p1`2=0 by A142;
hence contradiction by A142,A148,EUCLID:53,54;
end;
qq`1=1/p2`1 by EUCLID:52;
then
A149: 1/p1`1= 1/p2`1 by A144,EUCLID:52;
qq`2=p2`2/p2`1/p2`1 by EUCLID:52;
then p1`2/p1`1= p2`2/p1`1 by A144,A149,A146,A147,EUCLID:52
,XCMPLX_1:53;
then p1`2=p2`2 by A147,XCMPLX_1:53;
hence thesis by A149,A146,A145,EUCLID:53;
end;
case
A150: x2 in K1a & not x2 in K0a;
A151: now
assume
A152: p1`1=0;
then p1`2=0 by A142;
hence contradiction by A142,A152,EUCLID:53,54;
end;
A153: now
per cases by A142;
case
A154: p1`2<=p1`1 & -p1`1<=p1`2;
then -p1`1 <= p1`1 by XXREAL_0:2;
then p1`1>=0;
then p1`2/p1`1<=p1`1/p1`1 by A154,XREAL_1:72;
hence p1`2/p1`1<=1 by A151,XCMPLX_1:60;
end;
case
A155: p1`2>=p1`1 & p1`2<=-p1`1;
then -p1`1 >= p1`1 by XXREAL_0:2;
then p1`1 <= 0;
then p1`2/p1`1<=p1`1/p1`1 by A155,XREAL_1:73;
hence p1`2/p1`1<=1 by A151,XCMPLX_1:60;
end;
end;
A156: now
per cases by A142;
case
A157: p1`2<=p1`1 & -p1`1<=p1`2;
then -p1`1 <= p1`1 by XXREAL_0:2;
then p1`1>=0;
then (-p1`1)/p1`1<=p1`2/p1`1 by A157,XREAL_1:72;
hence -1<=p1`2/p1`1 by A151,XCMPLX_1:197;
end;
case
A158: p1`2>=p1`1 & p1`2<=-p1`1;
-p1`2>=--p1`1 & p1`1 <= 0 by XREAL_1:24,A158;
then (-p1`2)/(-p1`1)>=p1`1/(-p1`1) by XREAL_1:72;
then (-p1`2)/(-p1`1)>= -1 by A151,XCMPLX_1:198;
hence -1<=p1`2/p1`1 by XCMPLX_1:191;
end;
end;
A159: ex p8 being Point of (TOP-REAL 2) st p2=p8 &( p8`1<=p8`2 & -p8
`2<=p8`1 or p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2 by A150;
A160: now
assume
A161: p2`2=0;
then p2`1=0 by A159;
hence contradiction by A159,A161,EUCLID:53,54;
end;
not((p2`2<=p2`1 & -p2`1<=p2`2 or p2`2>=p2`1 & p2`2<=-p2`1) &
p2 <> 0.TOP-REAL 2) by A150;
then
A162: Out_In_Sq.p2=|[p2`1/p2`2/p2`2,1/p2`2]| by A159,Def1;
then p1`2/p1`1/p1`1=1/p2`2 by A136,A143,SPPOL_2:1;
then
A163: p1`2/p1`1=1/p2`2*p1`1 by A151,XCMPLX_1:87
.= p1`1/p2`2;
1/p1`1=p2`1/p2`2/p2`2 by A136,A143,A162,SPPOL_2:1;
then
A164: p2`1/p2`2=1/p1`1*p2`2 by A160,XCMPLX_1:87
.= p2`2/p1`1;
then
A165: (p2`1/p2`2)* (p1`2/p1`1)=1 by A160,A151,A163,XCMPLX_1:112;
A166: (p2`1/p2`2)* (p1`2/p1`1)*p1`1=1 *p1`1 by A160,A151,A164,A163,
XCMPLX_1:112;
then
A167: p1`2<>0 by A151;
A168: ex p9 being Point of (TOP-REAL 2) st p2=p9 &( p9`1<=p9`2 & -p9
`2<=p9`1 or p9`1>=p9`2 & p9`1<=-p9`2)& p9<>0.TOP-REAL 2 by A150;
A169: now
per cases by A168;
case
A170: p2`1<=p2`2 & -p2`2<=p2`1;
then -p2`2 <= p2`2 by XXREAL_0:2;
then p2`2>=0;
then (-p2`2)/p2`2<=p2`1/p2`2 by A170,XREAL_1:72;
hence -1<=p2`1/p2`2 by A160,XCMPLX_1:197;
end;
case
A171: p2`1>=p2`2 & p2`1<=-p2`2;
-p2`1>=--p2`2 & p2`2 <= 0 by XREAL_1:24,A171;
then (-p2`1)/(-p2`2)>=p2`2/(-p2`2) by XREAL_1:72;
then (-p2`1)/(-p2`2)>= -1 by A160,XCMPLX_1:198;
hence -1<=p2`1/p2`2 by XCMPLX_1:191;
end;
end;
(p2`1/p2`2)* ((p1`2/p1`1)*p1`1)=p1`1 by A166;
then
A172: (p2`1/p2`2)*p1`2=p1`1 by A151,XCMPLX_1:87;
then
A173: (p2`1/p2`2)=p1`1/p1`2 by A167,XCMPLX_1:89;
A174: now
per cases by A168;
case
A175: p2`1<=p2`2 & -p2`2<=p2`1;
then -p2`2 <= p2`2 by XXREAL_0:2;
then p2`2>=0;
then p2`1/p2`2<=p2`2/p2`2 by A175,XREAL_1:72;
hence p2`1/p2`2<=1 by A160,XCMPLX_1:60;
end;
case
A176: p2`1>=p2`2 & p2`1<=-p2`2;
then -p2`2 >= p2`2 by XXREAL_0:2;
then p2`2 <= 0;
then p2`1/p2`2<=p2`2/p2`2 by A176,XREAL_1:73;
hence p2`1/p2`2<=1 by A160,XCMPLX_1:60;
end;
end;
now
per cases;
case
0<=p2`1/p2`2;
then
A177: p1`2>0 & p1`1>=0 or p1`2<0 & p1`1<=0 by A151,A172;
now
assume p1`2/p1`1<>1;
then p1`2/p1`1<1 by A153,XXREAL_0:1;
hence contradiction by A165,A174,A177,XREAL_1:162;
end;
then p1`2=(1)*p1`1 by A151,XCMPLX_1:87;
then (p2`1/p2`2)*p2`2=(1)*p2`2 by A151,A173,XCMPLX_1:60
.=p2`2;
then p2`1=p2`2 by A160,XCMPLX_1:87;
hence contradiction by A150,A168;
end;
case
0>p2`1/p2`2;
then
A178: p1`2<0 & p1`1>0 or p1`2>0 & p1`1<0 by A173,XREAL_1:143;
now
assume p1`2/p1`1<>-1;
then -1<p1`2/p1`1 by A156,XXREAL_0:1;
hence contradiction by A165,A169,A178,XREAL_1:166;
end;
then p1`2=(-1)*p1`1 by A151,XCMPLX_1:87
.= -p1`1;
then -p1`2 =p1`1;
then p2`1/p2`2=-1 by A167,A173,XCMPLX_1:197;
then p2`1=(-1)*p2`2 by A160,XCMPLX_1:87;
then -p2`1=p2`2;
hence contradiction by A150,A168;
end;
end;
hence contradiction;
end;
end;
hence thesis;
end;
case
x1 in K1a;
then
A179: ex p7 being Point of TOP-REAL 2 st p1=p7 &( p7`1<=p7`2 & -p7`2<=
p7`1 or p7`1>=p7`2 & p7`1<=-p7`2)& p7<>0.TOP-REAL 2;
then
A180: Out_In_Sq.p1=|[p1`1/p1`2/p1`2,1/p1`2]| by Th14;
now
per cases by A139,A138,XBOOLE_0:def 3;
case
x2 in K1a;
then ex p8 being Point of (TOP-REAL 2) st p2=p8 &( p8`1<=p8`2 & -
p8`2<=p8`1 or p8`1>=p8`2 & p8`1<=-p8`2)& p8<>0.TOP-REAL 2;
then
A181: |[p2`1/p2`2/p2`2,1/p2`2]| =|[p1`1/p1`2/p1`2,1/p1`2]| by A136,A180
,Th14;
A182: p1=|[p1`1,p1`2]| by EUCLID:53;
set qq=|[p2`1/p2`2/p2`2,1/p2`2]|;
A183: (1/p1`2)"=(p1`2)"" .=p1`2;
A184: now
assume
A185: p1`2=0;
then p1`1=0 by A179;
hence contradiction by A179,A185,EUCLID:53,54;
end;
qq`2=1/p2`2 by EUCLID:52;
then
A186: 1/p1`2= 1/p2`2 by A181,EUCLID:52;
qq`1=p2`1/p2`2/p2`2 by EUCLID:52;
then p1`1/p1`2= p2`1/p1`2 by A181,A186,A183,A184,EUCLID:52
,XCMPLX_1:53;
then p1`1=p2`1 by A184,XCMPLX_1:53;
hence thesis by A186,A183,A182,EUCLID:53;
end;
case
A187: x2 in K0a & not x2 in K1a;
A188: now
assume
A189: p1`2=0;
then p1`1=0 by A179;
hence contradiction by A179,A189,EUCLID:53,54;
end;
A190: now
per cases by A179;
case
A191: p1`1<=p1`2 & -p1`2<=p1`1;
then -p1`2 <= p1`2 by XXREAL_0:2;
then p1`2>=0;
then p1`1/p1`2<=p1`2/p1`2 by A191,XREAL_1:72;
hence p1`1/p1`2<=1 by A188,XCMPLX_1:60;
end;
case
A192: p1`1>=p1`2 & p1`1<=-p1`2;
then
-p1`2 >= p1`2 by XXREAL_0:2;
then p1`2 <= 0;
then p1`1/p1`2<=p1`2/p1`2 by A192,XREAL_1:73;
hence p1`1/p1`2<=1 by A188,XCMPLX_1:60;
end;
end;
A193: now
per cases by A179;
case
A194: p1`1<=p1`2 & -p1`2<=p1`1;
then -p1`2 <= p1`2 by XXREAL_0:2;
then p1`2>=0;
then (-p1`2)/p1`2<=p1`1/p1`2 by A194,XREAL_1:72;
hence -1<=p1`1/p1`2 by A188,XCMPLX_1:197;
end;
case
A195: p1`1>=p1`2 & p1`1<=-p1`2;
-p1`1>=--p1`2 & p1`2 <= 0 by XREAL_1:24,A195;
then (-p1`1)/(-p1`2)>=p1`2/(-p1`2) by XREAL_1:72;
then (-p1`1)/(-p1`2)>= -1 by A188,XCMPLX_1:198;
hence -1<=p1`1/p1`2 by XCMPLX_1:191;
end;
end;
A196: ex p8 being Point of (TOP-REAL 2) st p2=p8 &( p8`2<=p8`1 & -
p8`1<=p8`2 or p8`2>=p8`1 & p8`2<=-p8`1)& p8<>0.TOP-REAL 2 by A187;
A197: now
assume
A198: p2`1=0;
then p2`2=0 by A196;
hence contradiction by A196,A198,EUCLID:53,54;
end;
A199: ex p9 being Point of (TOP-REAL 2) st p2=p9 &( p9`2<=p9`1 & -
p9`1<=p9`2 or p9`2>=p9`1 & p9`2<=-p9`1)& p9<>0.TOP-REAL 2 by A187;
A200: now
per cases by A199;
case
A201: p2`2<=p2`1 & -p2`1<=p2`2;
then -p2`1 <= p2`1 by XXREAL_0:2;
then p2`1>=0;
then (-p2`1)/p2`1<=p2`2/p2`1 by A201,XREAL_1:72;
hence -1<=p2`2/p2`1 by A197,XCMPLX_1:197;
end;
case
A202: p2`2>=p2`1 & p2`2<=-p2`1;
-p2`2>=--p2`1 & p2`1 <= 0 by XREAL_1:24,A202;
then (-p2`2)/(-p2`1)>=p2`1/(-p2`1) by XREAL_1:72;
then (-p2`2)/(-p2`1)>= -1 by A197,XCMPLX_1:198;
hence -1<=p2`2/p2`1 by XCMPLX_1:191;
end;
end;
A203: Out_In_Sq.p2=|[1/p2`1,p2`2/p2`1/p2`1]| by A196,Def1;
then 1/p1`2=p2`2/p2`1/p2`1 by A136,A180,SPPOL_2:1;
then
A204: p2`2/p2`1=1/p1`2*p2`1 by A197,XCMPLX_1:87
.= p2`1/p1`2;
p1`1/p1`2/p1`2=1/p2`1 by A136,A180,A203,SPPOL_2:1;
then p1`1/p1`2=1/p2`1*p1`2 by A188,XCMPLX_1:87
.= p1`2/p2`1;
then
A205: (p2`2/p2`1)* (p1`1/p1`2)=1 by A197,A188,A204,XCMPLX_1:112;
then
A206: p1`1<>0;
(p2`2/p2`1)* (p1`1/p1`2)*p1`2=p1`2 by A205;
then (p2`2/p2`1)* ((p1`1/p1`2)*p1`2)=p1`2;
then (p2`2/p2`1)*p1`1=p1`2 by A188,XCMPLX_1:87;
then
A207: (p2`2/p2`1)=p1`2/p1`1 by A206,XCMPLX_1:89;
A208: now
per cases by A199;
case
A209: p2`2<=p2`1 & -p2`1<=p2`2;
then -p2`1 <= p2`1 by XXREAL_0:2;
then p2`1>=0;
then p2`2/p2`1<=p2`1/p2`1 by A209,XREAL_1:72;
hence p2`2/p2`1<=1 by A197,XCMPLX_1:60;
end;
case
A210: p2`2>=p2`1 & p2`2<=-p2`1;
then -p2`1 >= p2`1 by XXREAL_0:2;
then p2`1 <= 0;
then p2`2/p2`1<=p2`1/p2`1 by A210,XREAL_1:73;
hence p2`2/p2`1<=1 by A197,XCMPLX_1:60;
end;
end;
now
per cases;
case
0<=p2`2/p2`1;
then
A211: p1`1>0 & p1`2>=0 or p1`1<0 & p1`2<=0 by A205,A206;
now
assume p1`1/p1`2<>1;
then p1`1/p1`2<1 by A190,XXREAL_0:1;
hence contradiction by A205,A208,A211,XREAL_1:162;
end;
then p1`1=(1)*p1`2 by A188,XCMPLX_1:87;
then (p2`2/p2`1)*p2`1 =(1)*p2`1 by A188,A207,XCMPLX_1:60
.=p2`1;
then p2`2=p2`1 by A197,XCMPLX_1:87;
hence contradiction by A187,A199;
end;
case
0>p2`2/p2`1;
then
A212: p1`1<0 & p1`2>0 or p1`1>0 & p1`2<0 by A207,XREAL_1:143;
now
assume p1`1/p1`2<>-1;
then -1<p1`1/p1`2 by A193,XXREAL_0:1;
hence contradiction by A205,A200,A212,XREAL_1:166;
end;
then p1`1=(-1)*p1`2 by A188,XCMPLX_1:87
.= -p1`2;
then -p1`1 =p1`2;
then p2`2/p2`1=-1 by A206,A207,XCMPLX_1:197;
then p2`2=(-1)*p2`1 by A197,XCMPLX_1:87;
then -p2`2=p2`1;
hence contradiction by A187,A199;
end;
end;
hence contradiction;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then
A213: Out_In_Sq is one-to-one by FUNCT_1:def 4;
A214: for s being Point of TOP-REAL 2 st s in Kb holds Out_In_Sq.s=s
proof
let t be Point of TOP-REAL 2;
assume t in Kb;
then
A215: ex p4 being Point of TOP-REAL 2 st p4=t &( -1=p4`1 & -1<= p4`2 & p4`2
<=1 or p4`1=1 & -1<=p4`2 & p4`2<=1 or -1 =p4`2 & -1<=p4`1 & p4`1<=1 or 1=p4`2 &
-1<=p4`1 & p4`1<=1) by A1;
then
A216: t<>0.TOP-REAL 2 by EUCLID:52,54;
A217: not t=0.TOP-REAL 2 by A215,EUCLID:52,54;
now
per cases;
case
A218: t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1;
then
A219: Out_In_Sq.t=|[1/t`1,t`2/t`1/t`1]| by A217,Def1;
A220: 1<=t`1 & t`1>=-1 or 1>=t`1 & -1>=--t`1 by A215,A218,XREAL_1:24;
now
per cases by A215,A220,XXREAL_0:1;
case
t`1=1;
hence thesis by A219,EUCLID:53;
end;
case
t`1=-1;
hence thesis by A219,EUCLID:53;
end;
end;
hence thesis;
end;
case
A221: not (t`2<=t`1 & -t`1<=t`2 or t`2>=t`1 & t`2<=-t`1);
then
A222: Out_In_Sq.t=|[t`1/t`2/t`2,1/t`2]| by A216,Def1;
now
per cases by A215,A221;
case
t`2=1;
hence thesis by A222,EUCLID:53;
end;
case
t`2=-1;
hence thesis by A222,EUCLID:53;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
ex h being Function of (TOP-REAL 2)|D,(TOP-REAL 2)|D st h =Out_In_Sq & h
is continuous by A2,Th40;
hence thesis by A213,A4,A72,A214;
end;
theorem Th42:
for f,g being Function of I[01],TOP-REAL 2, K0 being Subset of
TOP-REAL 2, O,I being Point of I[01] st O=0 & I=1 & f is continuous one-to-one
& g is continuous one-to-one & K0={p: -1<p`1 & p`1<1 & -1<p`2 & p`2<1}& (f.O)`1
=-1 & (f.I)`1=1 & -1<=(f.O)`2 & (f.O)`2<=1 & -1<=(f.I)`2 & (f.I)`2<=1 & (g.O)`2
=-1 & (g.I)`2=1 & -1<=(g.O)`1 & (g.O)`1<=1 & -1<=(g.I)`1 & (g.I)`1<=1 & rng f
misses K0 & rng g misses K0 holds rng f meets rng g
proof
reconsider B={0.TOP-REAL 2} as Subset of TOP-REAL 2;
A1: B`<>{} by Th9;
reconsider W=B` as non empty Subset of TOP-REAL 2 by Th9;
defpred P[Point of TOP-REAL 2] means -1=$1`1 & -1<=$1`2 & $1`2<=1 or $1`1=1
& -1<=$1`2 & $1`2<=1 or -1=$1`2 & -1<=$1`1 & $1`1<=1 or 1=$1`2 & -1<=$1`1 & $1
`1<=1;
A2: the carrier of (TOP-REAL 2)|B` =[#]((TOP-REAL 2)|B`)
.=B` by PRE_TOPC:def 5;
reconsider Kb={q: P[q]} as Subset of TOP-REAL 2 from TopSubset;
let f,g be Function of I[01],TOP-REAL 2, K0 be Subset of TOP-REAL 2, O,I be
Point of I[01];
A3: dom f =the carrier of I[01] by FUNCT_2:def 1;
assume
A4: O=0 & I=1 & f is continuous & f is one-to-one & g is continuous & g
is one-to-one & K0={p: -1<p`1 & p`1<1 & -1<p`2 & p`2<1}& (f.O)`1=-1 & (f.I)`1=1
& -1<=(f.O)`2 & (f.O)`2<=1 & -1<=(f.I)`2 & (f.I)`2<=1 & (g.O)`2=-1 & (g.I)`2=1
& -1<=(g.O)`1 & (g.O)`1<=1 & -1<=(g.I)`1 & (g.I)`1<=1 & rng f /\ K0={} & rng g
/\ K0={};
then consider h being Function of (TOP-REAL 2)|B`,(TOP-REAL 2)|B` such that
A5: h is continuous and
A6: h is one-to-one and
for t being Point of TOP-REAL 2 st t in K0 & t<>0.TOP-REAL 2 holds not h
.t in K0 \/ Kb and
A7: for r being Point of TOP-REAL 2 st not r in K0 \/ Kb holds h.r in K0 and
A8: for s being Point of TOP-REAL 2 st s in Kb holds h.s=s by Th41;
rng f c= B`
proof
let x be object;
assume
A9: x in rng f;
now
assume x in B;
then
A10: x=0.TOP-REAL 2 by TARSKI:def 1;
(0.TOP-REAL 2)`1=0 & (0.TOP-REAL 2)`2=0 by EUCLID:52,54;
then 0.TOP-REAL 2 in K0 by A4;
hence contradiction by A4,A9,A10,XBOOLE_0:def 4;
end;
then x in (the carrier of TOP-REAL 2)\ B by A9,XBOOLE_0:def 5;
hence thesis by SUBSET_1:def 4;
end;
then
A11: ex w being Function of I[01],TOP-REAL 2 st w is continuous & w=h*f by A4
,A5,A1,Th12;
then reconsider d1=h*f as Function of I[01],TOP-REAL 2;
the carrier of (TOP-REAL 2)|W <>{};
then
A12: dom h=the carrier of (TOP-REAL 2)|B` by FUNCT_2:def 1;
rng g c= B`
proof
let x be object;
assume
A13: x in rng g;
now
assume x in B;
then
A14: x=0.TOP-REAL 2 by TARSKI:def 1;
0.TOP-REAL 2 in K0 by A4,Th3;
hence contradiction by A4,A13,A14,XBOOLE_0:def 4;
end;
then x in (the carrier of TOP-REAL 2)\ B by A13,XBOOLE_0:def 5;
hence thesis by SUBSET_1:def 4;
end;
then
A15: ex w2 being Function of I[01],TOP-REAL 2 st w2 is continuous & w2=h*g by
A4,A5,A1,Th12;
then reconsider d2=h*g as Function of I[01],TOP-REAL 2;
A16: dom g =the carrier of I[01] by FUNCT_2:def 1;
A17: for r being Point of I[01] holds -1<=(d1.r)`1 & (d1.r)`1<=1 & -1<=(d2.r
)`1 & (d2.r)`1<=1 & -1<=(d1.r)`2 & (d1.r)`2<=1 & -1<=(d2.r)`2 & (d2.r)`2<=1
proof
let r be Point of I[01];
A18: g.r in Kb implies d2.r in K0 \/ Kb
proof
A19: d2.r=h.(g.r) by A16,FUNCT_1:13;
assume
A20: g.r in Kb;
then h.(g.r)=g.r by A8;
hence thesis by A20,A19,XBOOLE_0:def 3;
end;
f.r in rng f by A3,FUNCT_1:3;
then
A21: not f.r in K0 by A4,XBOOLE_0:def 4;
A22: not f.r in Kb implies d1.r in K0 \/ Kb
proof
assume not f.r in Kb;
then not f.r in K0 \/ Kb by A21,XBOOLE_0:def 3;
then
A23: h.(f.r) in K0 by A7;
d1.r=h.(f.r) by A3,FUNCT_1:13;
hence thesis by A23,XBOOLE_0:def 3;
end;
g.r in rng g by A16,FUNCT_1:3;
then
A24: not g.r in K0 by A4,XBOOLE_0:def 4;
A25: not g.r in Kb implies d2.r in K0 \/ Kb
proof
assume not g.r in Kb;
then not g.r in K0 \/ Kb by A24,XBOOLE_0:def 3;
then
A26: h.(g.r) in K0 by A7;
d2.r=h.(g.r) by A16,FUNCT_1:13;
hence thesis by A26,XBOOLE_0:def 3;
end;
A27: f.r in Kb implies d1.r in K0 \/ Kb
proof
A28: d1.r=h.(f.r) by A3,FUNCT_1:13;
assume
A29: f.r in Kb;
then h.(f.r)=f.r by A8;
hence thesis by A29,A28,XBOOLE_0:def 3;
end;
now
per cases by A22,A27,A25,A18,XBOOLE_0:def 3;
case
d1.r in K0 & d2.r in K0;
then
(ex p being Point of TOP-REAL 2 st p=d1.r & -1<p`1 & p`1 <1 & -1<
p`2 & p `2<1 )& ex q being Point of TOP-REAL 2 st q=d2.r & -1<q`1 & q`1 <1 & -1
<q `2 & q`2<1 by A4;
hence thesis;
end;
case
d1.r in K0 & d2.r in Kb;
then
(ex p being Point of TOP-REAL 2 st p=d1.r & -1<p`1 & p`1 <1 & -1<
p`2 & p `2<1 )& ex q being Point of TOP-REAL 2 st q=d2.r &( -1=q`1 & -1<= q`2 &
q`2<= 1 or q`1=1 & -1<=q`2 & q`2<=1 or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1
<=q`1 & q`1<=1) by A4;
hence thesis;
end;
case
d1.r in Kb & d2.r in K0;
then
(ex p being Point of TOP-REAL 2 st p=d2.r & -1<p`1 & p`1 <1 & -1<
p`2 & p `2<1 )& ex q being Point of TOP-REAL 2 st q=d1.r &( -1=q`1 & -1<= q`2 &
q`2<= 1 or q`1=1 & -1<=q`2 & q`2<=1 or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1
<=q`1 & q`1<=1) by A4;
hence thesis;
end;
case
d1.r in Kb & d2.r in Kb;
then (ex p being Point of TOP-REAL 2 st p=d2.r &( -1=p`1 & -1<= p`2 &
p`2<=1 or p `1=1 & -1<=p`2 & p`2<=1 or -1=p`2 & -1<=p`1 & p`1<=1 or 1=p`2 & -1
<=p`1 & p`1<= 1))& ex q being Point of TOP-REAL 2 st q=d1.r &( -1=q`1 & -1<= q
`2 & q`2<=1 or q`1=1 & -1<=q`2 & q`2<=1 or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 &
-1<=q`1 & q `1<=1);
hence thesis;
end;
end;
hence thesis;
end;
f.I in Kb by A4;
then h.(f.I)=f.I by A8;
then
A30: (d1.I)`1=1 by A4,A3,FUNCT_1:13;
f.O in Kb by A4;
then h.(f.O)=f.O by A8;
then
A31: (d1.O)`1=-1 by A4,A3,FUNCT_1:13;
g.I in Kb by A4;
then h.(g.I)=g.I by A8;
then
A32: (d2.I)`2=1 by A4,A16,FUNCT_1:13;
g.O in Kb by A4;
then h.(g.O)=g.O by A8;
then
A33: (d2.O)`2=-1 by A4,A16,FUNCT_1:13;
set s = the Element of rng d1 /\ rng d2;
d1 is one-to-one & d2 is one-to-one by A4,A6,FUNCT_1:24;
then rng d1 meets rng d2 by A4,A11,A15,A31,A30,A33,A32,A17,JGRAPH_1:47;
then
A34: rng d1 /\ rng d2<>{};
then s in rng d1 by XBOOLE_0:def 4;
then consider t1 being object such that
A35: t1 in dom d1 and
A36: s=d1.t1 by FUNCT_1:def 3;
A37: f.t1 in rng f by A3,A35,FUNCT_1:3;
s in rng d2 by A34,XBOOLE_0:def 4;
then consider t2 being object such that
A38: t2 in dom d2 and
A39: s=d2.t2 by FUNCT_1:def 3;
h.(f.t1)=d1.t1 by A35,FUNCT_1:12;
then
A40: h.(f.t1)=h.(g.t2) by A36,A38,A39,FUNCT_1:12;
rng g c=(the carrier of (TOP-REAL 2))\B
proof
let e be object;
assume
A41: e in rng g;
now
assume e in B;
then
A42: e=0.TOP-REAL 2 by TARSKI:def 1;
0.TOP-REAL 2 in {p: -1<p`1 & p`1<1 & -1<p`2 & p`2<1} by Th3;
hence contradiction by A4,A41,A42,XBOOLE_0:def 4;
end;
hence thesis by A41,XBOOLE_0:def 5;
end;
then
A43: rng g c= the carrier of (TOP-REAL 2)|B` by A2,SUBSET_1:def 4;
dom g =the carrier of I[01] by FUNCT_2:def 1;
then
A44: g.t2 in rng g by A38,FUNCT_1:3;
rng f c=(the carrier of (TOP-REAL 2))\B
proof
let e be object;
assume
A45: e in rng f;
now
assume e in B;
then
A46: e=0.TOP-REAL 2 by TARSKI:def 1;
0.TOP-REAL 2 in {p: -1<p`1 & p`1<1 & -1<p`2 & p`2<1} by Th3;
hence contradiction by A4,A45,A46,XBOOLE_0:def 4;
end;
hence thesis by A45,XBOOLE_0:def 5;
end;
then rng f c= the carrier of (TOP-REAL 2)|B` by A2,SUBSET_1:def 4;
then f.t1=g.t2 by A6,A43,A40,A12,A37,A44,FUNCT_1:def 4;
then rng f /\ rng g <> {} by A37,A44,XBOOLE_0:def 4;
hence thesis;
end;
theorem Th43:
for A,B,C,D being Real, f being Function of TOP-REAL 2,
TOP-REAL 2 st (for t being Point of TOP-REAL 2 holds f.t=|[A*(t`1)+B,C*(t`2)+D
]|) holds f is continuous
proof
reconsider h11=proj1 as Function of TOP-REAL 2,R^1 by TOPMETR:17;
set K0=[#](TOP-REAL 2);
let A,B,C,D be Real,f be Function of TOP-REAL 2,TOP-REAL 2;
A1: (TOP-REAL 2)| [#](TOP-REAL 2)=the TopStruct of TOP-REAL 2 by TSEP_1:93;
then reconsider h1=h11 as Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1;
h11 is continuous by JORDAN5A:27;
then h1 is continuous by A1,PRE_TOPC:32;
then consider
g1 being Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1 such that
A2: for p being Point of (TOP-REAL 2)| [#](TOP-REAL 2),r1 being Real
st h1.p=r1 holds g1.p=A*r1 and
A3: g1 is continuous by Th23;
reconsider f1=proj1*f as Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1 by A1,
TOPMETR:17;
consider g11 being Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1 such that
A4: for p being Point of (TOP-REAL 2)| [#](TOP-REAL 2),r1 being Real
st g1.p=r1 holds g11.p=r1+B and
A5: g11 is continuous by A3,Th24;
reconsider f2=proj2*f as Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1 by A1,
TOPMETR:17;
reconsider h11=proj2 as Function of TOP-REAL 2,R^1 by TOPMETR:17;
reconsider h1=h11 as Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1 by A1;
dom f1=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then
A6: dom f1=dom g11 by A1,FUNCT_2:def 1;
assume
A7: for t being Point of TOP-REAL 2 holds f.t=|[A*(t`1)+B,C*(t`2)+D]|;
A8: for x being object st x in dom f1 holds f1.x=g11.x
proof
let x be object;
assume
A9: x in dom f1;
then reconsider p=x as Point of TOP-REAL 2 by FUNCT_2:def 1;
f1.x=proj1.(f.x) by A9,FUNCT_1:12;
then
A10: f1.x=proj1.(|[A*(p`1)+B,C*(p`2)+D]|) by A7
.=A*(p`1)+B by PSCOMP_1:65
.=A*(proj1.p)+B by PSCOMP_1:def 5;
A*(proj1.p)=g1.p by A1,A2;
hence thesis by A1,A4,A10;
end;
h11 is continuous by JORDAN5A:27;
then h1 is continuous by A1,PRE_TOPC:32;
then consider
g1 being Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1 such that
A11: for p being Point of (TOP-REAL 2)| [#](TOP-REAL 2),r1 being Real
st h1.p=r1 holds g1.p=C*r1 and
A12: g1 is continuous by Th23;
consider g11 being Function of (TOP-REAL 2)| [#](TOP-REAL 2),R^1 such that
A13: for p being Point of (TOP-REAL 2)| [#](TOP-REAL 2),r1 being Real
st g1.p=r1 holds g11.p=r1+D and
A14: g11 is continuous by A12,Th24;
A15: for x being object st x in dom f2 holds f2.x=g11.x
proof
let x be object;
assume
A16: x in dom f2;
then reconsider p=x as Point of TOP-REAL 2 by FUNCT_2:def 1;
f2.x=proj2.(f.x) by A16,FUNCT_1:12;
then
A17: f2.x=proj2.(|[A*(p`1)+B,C*(p`2)+D]|) by A7
.=C*(p`2)+D by PSCOMP_1:65
.=C*(proj2.p)+D by PSCOMP_1:def 6;
C*(proj2.p)=g1.p by A1,A11;
hence thesis by A1,A13,A17;
end;
reconsider f0=f as Function of (TOP-REAL 2)| [#](TOP-REAL 2), (TOP-REAL 2)|
[#](TOP-REAL 2) by A1;
A18: for x,y,r,s being Real st |[x,y]| in K0 & r=f1.(|[x,y]|) & s=f2.
(|[x,y]|) holds f0. |[x,y]|=|[r,s]|
proof
let x,y,r,s be Real;
assume that
|[x,y]| in K0 and
A19: r=f1.(|[x,y]|) & s=f2.(|[x,y]|);
A20: f. |[x,y]| is Point of TOP-REAL 2;
dom f =the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then proj1.(f0. |[x,y]|) =r & proj2.(f0. |[x,y]|) =s by A19,FUNCT_1:13;
hence thesis by A20,Th8;
end;
dom f2=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then dom f2=dom g11 by A1,FUNCT_2:def 1;
then
A21: f2 is continuous by A14,A15,FUNCT_1:2;
f1 is continuous by A5,A6,A8,FUNCT_1:2;
then f0 is continuous by A21,A18,Th35;
hence f is continuous by A1,PRE_TOPC:34;
end;
definition
let A,B,C,D be Real;
func AffineMap(A,B,C,D) -> Function of TOP-REAL 2,TOP-REAL 2 means
:Def2:
for t being Point of TOP-REAL 2 holds it.t=|[A*(t`1)+B,C*(t`2)+D]|;
existence
proof
defpred P[object,object] means
for t being Point of TOP-REAL 2 st t=$1 holds $2=
|[A*(t`1)+B,C*(t`2)+D]|;
A1: for x being object st x in the carrier of TOP-REAL 2
ex y being object st P[ x,y]
proof
let x be object;
assume x in the carrier of TOP-REAL 2;
then reconsider t2=x as Point of TOP-REAL 2;
reconsider y2=|[A*(t2`1)+B,C*(t2`2)+D]| as set;
for t being Point of TOP-REAL 2 st t=x holds y2 =|[A*(t`1)+B,C*(t`2)
+D]|;
hence thesis;
end;
ex ff being Function st dom ff=(the carrier of TOP-REAL 2) & for x
being object st x in (the carrier of TOP-REAL 2) holds P[x,ff.x]
from CLASSES1:sch
1(A1);
then consider ff being Function such that
A2: dom ff=the carrier of TOP-REAL 2 and
A3: for x being object st x in the carrier of TOP-REAL 2 holds for t
being Point of TOP-REAL 2 st t=x holds ff.x=|[A*(t`1)+B,C*(t`2)+D]|;
for x being object st x in the carrier of TOP-REAL 2 holds ff.x in the
carrier of TOP-REAL 2
proof
let x be object;
assume x in the carrier of TOP-REAL 2;
then reconsider t=x as Point of TOP-REAL 2;
ff.t=|[A*(t`1)+B,C*(t`2)+D]| by A3;
hence thesis;
end;
then reconsider ff as Function of TOP-REAL 2,TOP-REAL 2 by A2,FUNCT_2:3;
take ff;
thus thesis by A3;
end;
uniqueness
proof
let m1,m2 be Function of TOP-REAL 2,TOP-REAL 2 such that
A4: for t being Point of TOP-REAL 2 holds m1.t=|[A*(t`1)+B,C*(t`2)+D ]| and
A5: for t being Point of TOP-REAL 2 holds m2.t=|[A*(t`1)+B,C*(t`2)+D ]|;
for x being Point of TOP-REAL 2 holds m1.x = m2.x
proof
let t be Point of TOP-REAL 2;
thus m1.t = |[A*(t`1)+B,C*(t`2)+D]| by A4
.= m2.t by A5;
end;
hence m1 = m2 by FUNCT_2:63;
end;
end;
registration
let a,b,c,d be Real;
cluster AffineMap(a,b,c,d) -> continuous;
coherence
proof
for t being Point of TOP-REAL 2 holds AffineMap(a,b,c,d).t=|[a*(t`1)+b
,c*(t`2)+d]| by Def2;
hence thesis by Th43;
end;
end;
theorem Th44:
for A,B,C,D being Real st A>0 & C>0 holds AffineMap(A,B,C
,D) is one-to-one
proof
let A,B,C,D be Real such that
A1: A>0 and
A2: C>0;
set ff = AffineMap(A,B,C,D);
for x1,x2 being object st x1 in dom ff & x2 in dom ff & ff.x1=ff.x2
holds x1=x2
proof
let x1,x2 be object;
assume that
A3: x1 in dom ff and
A4: x2 in dom ff and
A5: ff.x1=ff.x2;
reconsider p2=x2 as Point of TOP-REAL 2 by A4;
reconsider p1=x1 as Point of TOP-REAL 2 by A3;
A6: ff.x1= |[A*(p1`1)+B,C*(p1`2)+D]| & ff.x2= |[A*(p2`1)+B,C*(p2`2)+D]| by Def2
;
then A*(p1`1)+B=A*(p2`1)+B by A5,SPPOL_2:1;
then (p1`1)=A*(p2`1)/A by A1,XCMPLX_1:89;
then
A7: (p1`1)=(p2`1) by A1,XCMPLX_1:89;
C*(p1`2)+D=C*(p2`2)+D by A5,A6,SPPOL_2:1;
then (p1`2)=C*(p2`2)/C by A2,XCMPLX_1:89;
hence thesis by A2,A7,TOPREAL3:6,XCMPLX_1:89;
end;
hence thesis by FUNCT_1:def 4;
end;
theorem
for f,g being Function of I[01],TOP-REAL 2,a,b,c,d being Real ,
O,I being Point of I[01] st O=0 & I=1 & f is continuous one-to-one & g is
continuous one-to-one & (f.O)`1=a & (f.I)`1=b & c <=(f.O)`2 & (f.O)`2<=d & c <=
(f.I)`2 & (f.I)`2<=d & (g.O)`2=c & (g.I)`2=d & a<=(g.O)`1 & (g.O)`1<=b & a<=(g.
I)`1 & (g.I)`1<=b & a < b & c < d & not (ex r being Point of I[01] st a<(f.r)`1
& (f.r)`1<b & c <(f.r)`2 & (f.r)`2<d)& not (ex r being Point of I[01] st a<(g.r
)`1 & (g.r)`1<b & c <(g.r)`2 & (g.r)`2<d) holds rng f meets rng g
proof
defpred P[Point of TOP-REAL 2] means -1<$1`1 & $1`1<1 & -1<$1`2 & $1`2<1;
reconsider K0={p: P[p]} as Subset of TOP-REAL 2 from TopSubset;
let f,g be Function of I[01],TOP-REAL 2,a,b,c,d be Real, O,I be Point
of I[01];
assume that
A1: O=0 & I=1 and
A2: f is continuous one-to-one & g is continuous one-to-one and
A3: (f.O)`1=a and
A4: (f.I)`1=b and
A5: c <=(f.O)`2 and
A6: (f.O)`2<=d and
A7: c <=(f.I)`2 and
A8: (f.I)`2<=d and
A9: (g.O)`2=c and
A10: (g.I)`2=d and
A11: a<=(g.O)`1 and
A12: (g.O)`1<=b and
A13: a<=(g.I)`1 and
A14: (g.I)`1<=b and
A15: a < b and
A16: c < d and
A17: not(ex r being Point of I[01] st a<(f.r)`1 & (f.r)`1<b & c <(f.r)`2
& (f.r)`2<d) and
A18: not(ex r being Point of I[01] st a<(g.r)`1 & (g.r)`1<b & c <(g.r)`2
& (g.r)`2<d);
set A=2/(b-a),B=1-2*b/(b-a),C=2/(d-c),D=1-2*d/(d-c);
set ff =AffineMap(A,B,C,D);
reconsider f2=ff*f,g2=ff*g as Function of I[01],TOP-REAL 2;
A19: d-c>0 by A16,XREAL_1:50;
then
A20: C>0 by XREAL_1:139;
A21: dom g=the carrier of I[01] by FUNCT_2:def 1;
then
A22: g2.I=ff.(g.I) by FUNCT_1:13
.=|[A*((g.I)`1)+B,C*d+D]| by A10,Def2;
then
A23: (g2.I)`2=C*d+D by EUCLID:52
.= d*2/(d-c)+(1-2*d/(d-c))
.= 1;
A24: g2.O=ff.(g.O) by A21,FUNCT_1:13
.=|[A*((g.O)`1)+B,C*c+D]| by A9,Def2;
then
A25: (g2.O)`2=2/(d-c)*c+(1-2*d/(d-c)) by EUCLID:52
.= c*2/(d-c)+(1-2*d/(d-c))
.= c*2/(d-c)+((d-c)/(d-c)-2*d/(d-c)) by A19,XCMPLX_1:60
.= c*2/(d-c)+((d-c)-2*d)/(d-c)
.= (c*2+((d-c)-2*d))/(d-c)
.= (-(d-c))/(d-c)
.= -((d-c)/(d-c))
.= -1 by A19,XCMPLX_1:60;
A26: b-a>0 by A15,XREAL_1:50;
A27: -1<=(g2.O)`1 & (g2.O)`1<=1 & -1<=(g2.I)`1 & (g2.I)`1<=1
proof
reconsider s1=(g.I)`1 as Real;
reconsider s0=(g.O)`1 as Real;
A28: (a-b)/(b-a) = (-(b-a))/(b-a) .= -((b-a)/(b-a))
.= -1 by A26,XCMPLX_1:60;
A29: (g2.I)`1=A*s1+B by A22,EUCLID:52
.= s1*2/(b-a)+(1-2*b/(b-a))
.= s1*2/(b-a)+((b-a)/(b-a)-2*b/(b-a)) by A26,XCMPLX_1:60
.= s1*2/(b-a)+((b-a)-2*b)/(b-a)
.= (s1*2+((b-a)-2*b))/(b-a)
.= ((s1-b)+(s1-b)-(a-b))/(b-a);
b-b>=s0-b by A12,XREAL_1:9;
then 0+(b-b)-(a-b)>=(s0-b)+(s0-b)-(a-b) by XREAL_1:9;
then
A30: (b-a)/(b-a)>=((s0-b)+(s0-b)-(a-b))/(b-a) by A26,XREAL_1:72;
b-b>=s1-b by A14,XREAL_1:9;
then
A31: 0+(b-b)-(a-b)>=(s1-b)+(s1-b)-(a-b) by XREAL_1:9;
a-b<=s1-b by A13,XREAL_1:9;
then a-b+(a-b)<=(s1-b)+(s1-b) by XREAL_1:7;
then
A32: a-b+(a-b)-(a-b)<=(s1-b)+(s1-b)-(a-b) by XREAL_1:9;
a-b<=s0-b by A11,XREAL_1:9;
then a-b+(a-b)<=(s0-b)+(s0-b) by XREAL_1:7;
then
A33: a-b+(a-b)-(a-b)<=(s0-b)+(s0-b)-(a-b) by XREAL_1:9;
(g2.O)`1=A*s0+B by A24,EUCLID:52
.= s0 *2/(b-a)+(1-2*b/(b-a))
.= s0 *2/(b-a)+((b-a)/(b-a)-2*b/(b-a)) by A26,XCMPLX_1:60
.= s0 *2/(b-a)+((b-a)-2*b)/(b-a)
.= (s0 *2+((b-a)-2*b))/(b-a)
.= ((s0-b)+(s0-b)-(a-b))/(b-a);
hence thesis by A26,A33,A28,A30,A29,A32,A31,XREAL_1:72;
end;
A34: now
assume rng f2 meets K0;
then consider x being object such that
A35: x in rng f2 and
A36: x in K0 by XBOOLE_0:3;
reconsider q=x as Point of TOP-REAL 2 by A35;
consider p such that
A37: p=q and
A38: -1<p`1 and
A39: p`1<1 and
A40: -1<p`2 and
A41: p`2<1 by A36;
consider z being object such that
A42: z in dom f2 and
A43: x=f2.z by A35,FUNCT_1:def 3;
reconsider u=z as Point of I[01] by A42;
reconsider t=f.u as Point of TOP-REAL 2;
A44: A*(t`1)+B= (t`1)*2/(b-a)+(1-2*b/(b-a))
.= (t`1)*2/(b-a)+((b-a)/(b-a)-2*b/(b-a)) by A26,XCMPLX_1:60
.= (t`1)*2/(b-a)+((b-a)-2*b)/(b-a)
.= ((t`1)*2+((b-a)-2*b))/(b-a)
.= (2*((t`1)-b)-(a-b))/(b-a);
A45: ff.t=p by A37,A42,A43,FUNCT_1:12;
A46: C*(t`2)+D= (t`2)*2/(d-c)+(1-2*d/(d-c))
.= (t`2)*2/(d-c)+((d-c)/(d-c)-2*d/(d-c)) by A19,XCMPLX_1:60
.= (t`2)*2/(d-c)+((d-c)-2*d)/(d-c)
.= ((t`2)*2+((d-c)-2*d))/(d-c)
.= (2*((t`2)-d)-(c-d))/(d-c);
A47: ff.t=|[A*(t`1)+B,C*(t`2)+D]| by Def2;
then -1<C*(t`2)+D by A40,A45,EUCLID:52;
then (-1)*(d-c)< (2*((t`2)-d)-(c-d))/(d-c)*(d-c) by A19,A46,XREAL_1:68;
then (-1)*(d-c)< 2*((t`2)-d)-(c-d) by A19,XCMPLX_1:87;
then (-1)*(d-c)+(c-d)< 2*((t`2)-d)-(c-d)+(c-d) by XREAL_1:8;
then 2*(c-d)/2< 2*((t`2)-d)/2 by XREAL_1:74;
then
A48: c < (t`2) by XREAL_1:9;
C*(t`2)+D<1 by A41,A47,A45,EUCLID:52;
then (1)*(d-c)> (2*((t`2)-d)-(c-d))/(d-c)*(d-c) by A19,A46,XREAL_1:68;
then (1)*(d-c)> 2*((t`2)-d)-(c-d) by A19,XCMPLX_1:87;
then (1)*(d-c)+(c-d)> 2*((t`2)-d)-(c-d)+(c-d) by XREAL_1:8;
then 0/2>((t`2)-d)*2/2;
then
A49: 0+d>t`2 by XREAL_1:19;
A*(t`1)+B<1 by A39,A47,A45,EUCLID:52;
then (1)*(b-a)> (2*((t`1)-b)-(a-b))/(b-a)*(b-a) by A26,A44,XREAL_1:68;
then (1)*(b-a)> 2*((t`1)-b)-(a-b) by A26,XCMPLX_1:87;
then (1)*(b-a)+(a-b)> 2*((t`1)-b)-(a-b)+(a-b) by XREAL_1:8;
then 0/2>((t`1)-b)*2/2;
then
A50: 0+b>t`1 by XREAL_1:19;
-1<A*(t`1)+B by A38,A47,A45,EUCLID:52;
then (-1)*(b-a)< (2*((t`1)-b)-(a-b))/(b-a)*(b-a) by A26,A44,XREAL_1:68;
then (-1)*(b-a)< 2*((t`1)-b)-(a-b) by A26,XCMPLX_1:87;
then (-1)*(b-a)+(a-b)< 2*((t`1)-b)-(a-b)+(a-b) by XREAL_1:8;
then 2*(a-b)/2< 2*((t`1)-b)/2 by XREAL_1:74;
then a < (t`1) by XREAL_1:9;
hence contradiction by A17,A50,A48,A49;
end;
A51: dom f=the carrier of I[01] by FUNCT_2:def 1;
then
A52: f2.I=ff.(f.I) by FUNCT_1:13
.=|[A*b+B,C*((f.I)`2)+D]| by A4,Def2;
then
A53: (f2.I)`1=A*b+B by EUCLID:52
.= b*2/(b-a)+(1-2*b/(b-a))
.= 1;
A54: f2.O=ff.(f.O) by A51,FUNCT_1:13
.=|[A*a+B,C*((f.O)`2)+D]| by A3,Def2;
then
A55: (f2.O)`1=A*a+B by EUCLID:52
.= a*2/(b-a)+(1-2*b/(b-a))
.= a*2/(b-a)+((b-a)/(b-a)-2*b/(b-a)) by A26,XCMPLX_1:60
.= a*2/(b-a)+((b-a)-2*b)/(b-a)
.= (a*2+((b-a)-2*b))/(b-a)
.= (-(b-a))/(b-a)
.= -((b-a)/(b-a))
.= -1 by A26,XCMPLX_1:60;
A56: now
assume rng g2 meets K0;
then consider x being object such that
A57: x in rng g2 and
A58: x in K0 by XBOOLE_0:3;
reconsider q=x as Point of TOP-REAL 2 by A57;
consider p such that
A59: p=q and
A60: -1<p`1 and
A61: p`1<1 and
A62: -1<p`2 and
A63: p`2<1 by A58;
consider z being object such that
A64: z in dom g2 and
A65: x=g2.z by A57,FUNCT_1:def 3;
reconsider u=z as Point of I[01] by A64;
reconsider t=g.u as Point of TOP-REAL 2;
A66: A*(t`1)+B= (t`1)*2/(b-a)+(1-2*b/(b-a))
.= (t`1)*2/(b-a)+((b-a)/(b-a)-2*b/(b-a)) by A26,XCMPLX_1:60
.= (t`1)*2/(b-a)+((b-a)-2*b)/(b-a)
.= ((t`1)*2+((b-a)-2*b))/(b-a)
.= (2*((t`1)-b)-(a-b))/(b-a);
A67: ff.t=p by A59,A64,A65,FUNCT_1:12;
A68: C*(t`2)+D= (t`2)*2/(d-c)+(1-2*d/(d-c))
.= (t`2)*2/(d-c)+((d-c)/(d-c)-2*d/(d-c)) by A19,XCMPLX_1:60
.= (t`2)*2/(d-c)+((d-c)-2*d)/(d-c)
.= ((t`2)*2+((d-c)-2*d))/(d-c)
.= (2*((t`2)-d)-(c-d))/(d-c);
A69: ff.t=|[A*(t`1)+B,C*(t`2)+D]| by Def2;
then -1<C*(t`2)+D by A62,A67,EUCLID:52;
then (-1)*(d-c)< (2*((t`2)-d)-(c-d))/(d-c)*(d-c) by A19,A68,XREAL_1:68;
then (-1)*(d-c)< 2*((t`2)-d)-(c-d) by A19,XCMPLX_1:87;
then (-1)*(d-c)+(c-d)< 2*((t`2)-d)-(c-d)+(c-d) by XREAL_1:8;
then 2*(c-d)/2< 2*((t`2)-d)/2 by XREAL_1:74;
then
A70: c < (t`2) by XREAL_1:9;
C*(t`2)+D<1 by A63,A69,A67,EUCLID:52;
then (1)*(d-c)> (2*((t`2)-d)-(c-d))/(d-c)*(d-c) by A19,A68,XREAL_1:68;
then (1)*(d-c)> 2*((t`2)-d)-(c-d) by A19,XCMPLX_1:87;
then (1)*(d-c)+(c-d)> 2*((t`2)-d)-(c-d)+(c-d) by XREAL_1:8;
then 0/2>((t`2)-d)*2/2;
then
A71: 0+d>t`2 by XREAL_1:19;
A*(t`1)+B<1 by A61,A69,A67,EUCLID:52;
then (1)*(b-a)> (2*((t`1)-b)-(a-b))/(b-a)*(b-a) by A26,A66,XREAL_1:68;
then (1)*(b-a)> 2*((t`1)-b)-(a-b) by A26,XCMPLX_1:87;
then (1)*(b-a)+(a-b)> 2*((t`1)-b)-(a-b)+(a-b) by XREAL_1:8;
then 0/2>((t`1)-b)*2/2;
then
A72: 0+b>t`1 by XREAL_1:19;
-1<A*(t`1)+B by A60,A69,A67,EUCLID:52;
then (-1)*(b-a)< (2*((t`1)-b)-(a-b))/(b-a)*(b-a) by A26,A66,XREAL_1:68;
then (-1)*(b-a)< 2*((t`1)-b)-(a-b) by A26,XCMPLX_1:87;
then (-1)*(b-a)+(a-b)< 2*((t`1)-b)-(a-b)+(a-b) by XREAL_1:8;
then 2*(a-b)/2< 2*((t`1)-b)/2 by XREAL_1:74;
then a < (t`1) by XREAL_1:9;
hence contradiction by A18,A72,A70,A71;
end;
A73: -1<=(f2.O)`2 & (f2.O)`2<=1 & -1<=(f2.I)`2 & (f2.I)`2<=1
proof
reconsider s1=(f.I)`2 as Real;
reconsider s0=(f.O)`2 as Real;
A74: (c-d)/(d-c) = (-(d-c))/(d-c) .= -((d-c)/(d-c))
.= -1 by A19,XCMPLX_1:60;
A75: (f2.I)`2=C*s1+D by A52,EUCLID:52
.= s1*2/(d-c)+(1-2*d/(d-c))
.= s1*2/(d-c)+((d-c)/(d-c)-2*d/(d-c)) by A19,XCMPLX_1:60
.= s1*2/(d-c)+((d-c)-2*d)/(d-c)
.= (s1*2+((d-c)-2*d))/(d-c)
.= ((s1-d)+(s1-d)-(c-d))/(d-c);
d-d>=s0-d by A6,XREAL_1:9;
then 0+(d-d)-(c-d)>=(s0-d)+(s0-d)-(c-d) by XREAL_1:9;
then
A76: (d-c)/(d-c)>=((s0-d)+(s0-d)-(c-d))/(d-c) by A19,XREAL_1:72;
d-d>=s1-d by A8,XREAL_1:9;
then
A77: 0+(d-d)-(c-d)>=(s1-d)+(s1-d)-(c-d) by XREAL_1:9;
c-d<=s1-d by A7,XREAL_1:9;
then c-d+(c-d)<=(s1-d)+(s1-d) by XREAL_1:7;
then
A78: c-d+(c-d)-(c-d)<=(s1-d)+(s1-d)-(c-d) by XREAL_1:9;
c-d<=s0-d by A5,XREAL_1:9;
then c-d+(c-d)<=(s0-d)+(s0-d) by XREAL_1:7;
then
A79: c-d+(c-d)-(c-d)<=(s0-d)+(s0-d)-(c-d) by XREAL_1:9;
(f2.O)`2=C*s0+D by A54,EUCLID:52
.= s0 *2/(d-c)+(1-2*d/(d-c))
.= s0 *2/(d-c)+((d-c)/(d-c)-2*d/(d-c)) by A19,XCMPLX_1:60
.= s0 *2/(d-c)+((d-c)-2*d)/(d-c)
.= (s0 *2+((d-c)-2*d))/(d-c)
.= ((s0-d)+(s0-d)-(c-d))/(d-c);
hence thesis by A19,A79,A74,A76,A75,A78,A77,XREAL_1:72;
end;
set y = the Element of rng f2 /\ rng g2;
A>0 by A26,XREAL_1:139;
then
A80: ff is one-to-one by A20,Th44;
then f2 is one-to-one & g2 is one-to-one by A2,FUNCT_1:24;
then rng f2 meets rng g2 by A1,A2,A55,A53,A25,A23,A73,A27,A34,A56,Th42;
then
A81: rng f2 /\ rng g2 <> {};
then y in rng f2 by XBOOLE_0:def 4;
then consider x being object such that
A82: x in dom f2 and
A83: y=f2.x by FUNCT_1:def 3;
dom f2 c= dom f by RELAT_1:25;
then
A84: f.x in rng f by A82,FUNCT_1:3;
y in rng g2 by A81,XBOOLE_0:def 4;
then consider x2 being object such that
A85: x2 in dom g2 and
A86: y=g2.x2 by FUNCT_1:def 3;
A87: y=ff.(g.x2) by A85,A86,FUNCT_1:12;
dom g2 c= dom g by RELAT_1:25;
then
A88: g.x2 in rng g by A85,FUNCT_1:3;
dom ff=the carrier of TOP-REAL 2 & y=ff.(f.x) by A82,A83,FUNCT_1:12
,FUNCT_2:def 1;
then f.x=g.x2 by A80,A87,A84,A88,FUNCT_1:def 4;
then rng f /\ rng g <> {} by A84,A88,XBOOLE_0:def 4;
hence thesis;
end;
theorem
{p7 where p7 is Point of TOP-REAL 2: p7`2<=p7`1 } is closed Subset of
TOP-REAL 2 & {p7 where p7 is Point of TOP-REAL 2: p7`1<=p7`2 } is closed Subset
of TOP-REAL 2 by Lm5,Lm8;
theorem
{p7 where p7 is Point of TOP-REAL 2: -p7`1<=p7`2 } is closed Subset of
TOP-REAL 2 & {p7 where p7 is Point of TOP-REAL 2: p7`2<=-p7`1 } is closed
Subset of TOP-REAL 2 by Lm11,Lm14;
theorem
{p7 where p7 is Point of TOP-REAL 2: -p7`2<=p7`1 } is closed Subset of
TOP-REAL 2 & {p7 where p7 is Point of TOP-REAL 2: p7`1<=-p7`2 } is closed
Subset of TOP-REAL 2 by Lm17,Lm20;