:: Brouwer Fixed Point Theorem for Disks on the Plane
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received February 22, 2005
:: Copyright (c) 2005-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, EUCLID, SUBSET_1, PRE_TOPC, XBOOLE_0, ZFMISC_1, TARSKI,
STRUCT_0, METRIC_1, CARD_1, COMPLEX1, ARYTM_1, RELAT_1, XXREAL_0,
CONVEX1, TOPREALB, PROB_1, RVSUM_1, ARYTM_3, SQUARE_1, FUNCT_3, CARD_3,
POLYEQ_1, REAL_1, SUPINF_2, MCART_1, FUNCT_1, ABIAN, BORSUK_1, ALGSTR_1,
FUNCOP_1, BORSUK_2, ORDINAL2, TOPALG_1, EQREL_1, WAYBEL20, RCOMP_1,
TOPREALA, PSCOMP_1, TOPMETR, XXREAL_1, VALUED_1, PARTFUN3, PARTFUN1,
TOPS_2, SETFAM_1, BROUWER, FUNCT_2, NAT_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, EQREL_1, COMPLEX1,
SQUARE_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_3,
FUNCOP_1, PSCOMP_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RVSUM_1, RCOMP_1,
VALUED_1, STRUCT_0, PRE_TOPC, BORSUK_1, TOPS_2, JORDAN1, QUIN_1,
POLYEQ_1, BORSUK_2, TOPALG_1, TOPREAL9, TOPALG_2, TOPREALA, TOPREALB,
PARTFUN3, ABIAN, XXREAL_0, RLVECT_1, EUCLID;
constructors SQUARE_1, BINOP_2, COMPLEX1, QUIN_1, POLYEQ_1, ABIAN, MONOID_0,
TOPALG_1, TOPREAL9, TOPREALA, TOPREALB, PARTFUN3, BORSUK_6, CONVEX1,
PSCOMP_1, REAL_1, BINOP_1;
registrations SUBSET_1, FUNCT_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0,
SQUARE_1, NAT_1, MEMBERED, QUIN_1, RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1,
BORSUK_1, TEX_1, MONOID_0, EUCLID, TOPMETR, PSCOMP_1, BORSUK_2, TOPALG_1,
TOPREAL9, TOPREALB, PARTFUN3, TOPALG_5, VALUED_0, ZFMISC_1, RELSET_1,
PARTFUN4, VALUED_1, RELAT_1, ORDINAL1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, BORSUK_1, BORSUK_2, PSCOMP_1, ABIAN;
equalities XBOOLE_0, SQUARE_1, BINOP_1, STRUCT_0, RLVECT_1, TOPALG_1;
expansions XBOOLE_0, BORSUK_1, BORSUK_2, TOPALG_2, ABIAN;
theorems TOPRNS_1, XREAL_0, TARSKI, FUNCT_2, TSEP_1, RFUNCT_1, PRE_TOPC,
EUCLID, RELAT_1, FUNCT_1, ZFMISC_1, JGRAPH_2, XBOOLE_1, XBOOLE_0, TOPS_2,
BORSUK_1, TOPALG_1, EQREL_1, BORSUK_2, FUNCOP_1, TOPMETR, XCMPLX_0,
SQUARE_1, XCMPLX_1, FUNCT_3, COMPLEX1, JGRAPH_1, QUIN_1, POLYEQ_1,
TOPREAL3, TOPREAL9, TOPALG_2, TOPREALB, BORSUK_5, RCOMP_1, PSCOMP_1,
TOPREALA, YELLOW12, TOPGRP_1, PARTFUN3, RVSUM_1, EUCLID_2, XREAL_1,
SEQ_2, XXREAL_0, VALUED_1, XXREAL_1, SUBSET_1, JORDAN5A, XTUPLE_0,
RLVECT_1;
schemes FUNCT_2;
begin
set T2 = TOP-REAL 2;
reserve n for Element of NAT,
a, r for Real,
x for Point of TOP-REAL n;
definition
let S, T be non empty TopSpace;
func DiffElems(S,T) -> Subset of [:S,T:] equals
{[s,t] where s is Point of S, t is Point of T: s <> t};
coherence
proof
set A = {[s,t] where s is Point of S, t is Point of T: s <> t};
A c= the carrier of [:S,T:]
proof
let a be object;
assume a in A;
then ex s being Point of S, t being Point of T st a = [s,t] & s <> t;
hence thesis;
end;
hence thesis;
end;
end;
theorem
for S, T being non empty TopSpace, x being set holds x in DiffElems(S,
T) iff ex s being Point of S, t being Point of T st x = [s,t] & s <> t;
registration
let S be non trivial TopSpace;
let T be non empty TopSpace;
cluster DiffElems(S,T) -> non empty;
coherence
proof
set t1 = the Element of T;
consider s1, s2 being Element of S such that
A1: s1 <> s2 by SUBSET_1:def 7;
per cases;
suppose
s1 = t1;
then [s2,t1] in DiffElems(S,T) by A1;
hence thesis;
end;
suppose
s1 <> t1;
then [s1,t1] in DiffElems(S,T);
hence thesis;
end;
end;
end;
registration
let S be non empty TopSpace;
let T be non trivial TopSpace;
cluster DiffElems(S,T) -> non empty;
coherence
proof
set s1 = the Element of S;
consider t1, t2 being Element of T such that
A1: t1 <> t2 by SUBSET_1:def 7;
per cases;
suppose
s1 = t1;
then [s1,t2] in DiffElems(S,T) by A1;
hence thesis;
end;
suppose
s1 <> t1;
then [s1,t1] in DiffElems(S,T);
hence thesis;
end;
end;
end;
theorem Th2:
cl_Ball(x,0) = {x}
proof
thus cl_Ball(x,0) c= {x}
proof
let a be object;
assume
A1: a in cl_Ball(x,0);
then reconsider a as Point of TOP-REAL n;
|. a-x .| = 0 by A1,TOPREAL9:8;
then a = x by TOPRNS_1:28;
hence thesis by TARSKI:def 1;
end;
let a be object;
assume a in {x};
then
A2: a = x by TARSKI:def 1;
|. x-x .| = 0 by TOPRNS_1:28;
hence thesis by A2,TOPREAL9:8;
end;
definition
let n be Nat, x be Point of TOP-REAL n, r be Real;
func Tdisk(x,r) -> SubSpace of TOP-REAL n equals
(TOP-REAL n) | cl_Ball(x,r);
coherence;
end;
registration
let n be Nat, x be Point of TOP-REAL n;
let r be non negative Real;
cluster Tdisk(x,r) -> non empty;
coherence;
end;
theorem Th3:
the carrier of Tdisk(x,r) = cl_Ball(x,r)
proof
[#]Tdisk(x,r) = cl_Ball(x,r) by PRE_TOPC:def 5;
hence thesis;
end;
registration
let n be Element of NAT, x be Point of TOP-REAL n, r be Real;
cluster Tdisk(x,r) -> convex;
coherence
by Th3;
end;
reserve n for Element of NAT,
r for non negative Real,
s, t, x for Point of TOP-REAL n;
theorem Th4:
s <> t & s is Point of Tdisk(x,r) & s is not Point of Tcircle(x,r
) implies ex e being Point of Tcircle(x,r) st {e} = halfline(s,t) /\ Sphere(x,r
)
proof
assume that
A1: s <> t and
A2: s is Point of Tdisk(x,r) and
A3: s is not Point of Tcircle(x,r);
reconsider S = s, T = t, X = x as Element of REAL n by EUCLID:22;
set a = (-(2*|(t-s,s-x)|) + sqrt delta (Sum sqr (T-S), 2 * |(t-s,s-x)|, Sum
sqr (S-X) - r^2)) / (2 * Sum sqr (T-S));
the carrier of Tdisk(x,r) = cl_Ball(x,r) by Th3;
then
A4: |. s-x .| <= r by A2,TOPREAL9:8;
A5: the carrier of Tcircle(x,r) = Sphere(x,r) by TOPREALB:9;
then |. s-x .| <> r by A3,TOPREAL9:9;
then |. s-x .| < r by A4,XXREAL_0:1;
then s in Ball(x,r) by TOPREAL9:7;
then consider e1 being Point of TOP-REAL n such that
A6: {e1} = halfline(s,t) /\ Sphere(x,r) and
e1 = (1-a)*s + a*t by A1,TOPREAL9:37;
e1 in {e1} by TARSKI:def 1;
then e1 in Sphere(x,r) by A6,XBOOLE_0:def 4;
hence thesis by A5,A6;
end;
theorem Th5:
s <> t & s in the carrier of Tcircle(x,r) & t is Point of Tdisk(x
,r) implies ex e being Point of Tcircle(x,r) st e <> s & {s,e} = halfline(s,t)
/\ Sphere(x,r)
proof
assume
A1: s <> t & s in the carrier of Tcircle(x,r) & t is Point of Tdisk(x,r);
reconsider S = 1/2*s + 1/2*t, T = t, X = x as Element of REAL n by EUCLID:22;
A2: the carrier of Tcircle(x,r) = Sphere(x,r) by TOPREALB:9;
set a = (-(2*|(t-(1/2*s + 1/2*t),1/2*s + 1/2*t-x)|) + sqrt delta (Sum sqr (T
-S), 2 * |(t-(1/2*s + 1/2*t),1/2*s + 1/2*t-x)|, Sum sqr (S-X) - r^2)) / (2 *
Sum sqr (T-S));
the carrier of Tdisk(x,r) = cl_Ball(x,r) by Th3;
then consider e1 being Point of TOP-REAL n such that
A3: e1 <> s and
A4: {s,e1} = halfline(s,t) /\ Sphere(x,r) and
t in Sphere(x,r) implies e1 = t and
not t in Sphere(x,r) & a = (-(2*|(t-(1/2*s + 1/2*t),1/2*s + 1/2*t-x )|)
+ sqrt delta (Sum sqr (T-S), 2 * |(t-(1/2*s + 1/2*t),1/2*s + 1/2*t-x)|, Sum sqr
(S-X) - r^2)) / (2 * Sum sqr (T-S)) implies e1 = (1-a)*(1/2*s + 1/2*t) + a* t
by A1,A2,TOPREAL9:38;
e1 in {s,e1} by TARSKI:def 2;
then e1 in Sphere(x,r) by A4,XBOOLE_0:def 4;
hence thesis by A2,A3,A4;
end;
definition
let n be non zero Element of NAT, o be Point of TOP-REAL n, s, t be Point
of TOP-REAL n, r be non negative Real;
assume that
A1: s is Point of Tdisk(o,r) and
A2: t is Point of Tdisk(o,r) and
A3: s <> t;
func HC(s,t,o,r) -> Point of TOP-REAL n means
:Def3:
it in halfline(s,t) /\ Sphere(o,r) & it <> s;
existence
proof
per cases;
suppose
s is Point of Tcircle(o,r);
then consider e being Point of Tcircle(o,r) such that
A4: e <> s & {s,e} = halfline(s,t) /\ Sphere(o,r) by A2,A3,Th5;
reconsider e as Point of TOP-REAL n by PRE_TOPC:25;
take e;
thus thesis by A4,TARSKI:def 2;
end;
suppose
A5: s is not Point of Tcircle(o,r);
then consider e1 being Point of Tcircle(o,r) such that
A6: {e1} = halfline(s,t) /\ Sphere(o,r) by A1,A3,Th4;
reconsider e1 as Point of TOP-REAL n by PRE_TOPC:25;
take e1;
thus thesis by A5,A6,TARSKI:def 1;
end;
end;
uniqueness
proof
let m, u be Point of TOP-REAL n such that
A7: m in halfline(s,t) /\ Sphere(o,r) and
A8: m <> s and
A9: u in halfline(s,t) /\ Sphere(o,r) and
A10: u <> s;
per cases;
suppose
s is Point of Tcircle(o,r);
then consider f1 being Point of Tcircle(o,r) such that
f1 <> s and
A11: {s,f1} = halfline(s,t) /\ Sphere(o,r) by A2,A3,Th5;
per cases by A7,A9,A11,TARSKI:def 2;
suppose
m = f1 & u = f1;
hence thesis;
end;
suppose
m = f1 & u = s;
hence thesis by A10;
end;
suppose
m = s & u = f1;
hence thesis by A8;
end;
suppose
m = s & u = s;
hence thesis;
end;
end;
suppose
s is not Point of Tcircle(o,r);
then consider e being Point of Tcircle(o,r) such that
A12: {e} = halfline(s,t) /\ Sphere(o,r) by A1,A3,Th4;
m = e by A7,A12,TARSKI:def 1;
hence thesis by A9,A12,TARSKI:def 1;
end;
end;
end;
reserve n for non zero Element of NAT,
s, t, o for Point of TOP-REAL n;
theorem Th6:
s is Point of Tdisk(o,r) & t is Point of Tdisk(o,r) & s <> t
implies HC(s,t,o,r) is Point of Tcircle(o,r)
proof
assume s is Point of Tdisk(o,r) & t is Point of Tdisk(o,r) & s <> t;
then
the carrier of Tcircle(o,r) = Sphere(o,r) & HC(s,t,o,r) in halfline(s,t)
/\ Sphere(o,r) by Def3,TOPREALB:9;
hence thesis by XBOOLE_0:def 4;
end;
theorem
for S, T, O being Element of REAL n st S = s & T = t & O = o holds s
is Point of Tdisk(o,r) & t is Point of Tdisk(o,r) & s <> t & a = (-|(t-s,s-o)|
+ sqrt(|(t-s,s-o)|^2-(Sum sqr (T-S))*(Sum sqr (S-O)-r^2))) / Sum sqr (T-S)
implies HC(s,t,o,r) = (1-a)*s+a*t
proof
let S, T, O be Element of REAL n such that
A1: S = s and
A2: T = t and
A3: O = o and
A4: s is Point of Tdisk(o,r) and
A5: t is Point of Tdisk(o,r) and
A6: s <> t;
A7: |. T-S .| = sqrt Sum sqr (T-S) & Sum sqr (T-S) >= 0 by EUCLID:def 5
,RVSUM_1:86;
set H = HC(s,t,o,r);
A8: H in halfline(s,t) /\ Sphere(o,r) by A4,A5,A6,Def3;
then H in halfline(s,t) by XBOOLE_0:def 4;
then consider l being Real such that
A9: H = (1-l)*s + l*t and
A10: 0 <= l by TOPREAL9:26;
H in Sphere(o,r) by A8,XBOOLE_0:def 4;
then r = |. (1-l)*s+l*t - o .| by A9,TOPREAL9:9
.= |. 1 * s - l*s + l*t - o .| by RLVECT_1:35
.= |. s - l*s + l*t - o .| by RLVECT_1:def 8
.= |. s - (l*s - l*t) - o .| by RLVECT_1:29
.= |. s +- (l*s - l*t) +- o .|
.= |. s+-o +- (l*s - l*t) .| by RLVECT_1:def 3
.= |. s-o - (l*s - l*t) .|
.= |. s-o +- l*(s-t) .| by RLVECT_1:34
.= |. s-o + l*(-(s-t)) .| by RLVECT_1:25
.= |. s-o + l*(t-s) .| by RLVECT_1:33;
then
A11: r^2 = |. s-o .|^2 + 2*|(l*(t-s),s-o)| + |. l*(t-s) .|^2 by EUCLID_2:45
.= |. s-o .|^2 + 2*(l*|(t-s,s-o)|) + |. l*(t-s) .|^2 by EUCLID_2:19;
set A = Sum sqr (T-S);
A12: |. T-S .| <> 0 by A1,A2,A6,EUCLID:16;
A13: now
assume A <= 0;
then A = 0 by RVSUM_1:86;
hence contradiction by A12,EUCLID:def 5,SQUARE_1:17;
end;
set C = Sum sqr (S-O) - r^2;
set M = |(t-s,s-o)|;
set B = 2*M;
set l1 = (- B - sqrt delta(A,B,C)) / (2 * A);
set l2 = (- B + sqrt delta(A,B,C)) / (2 * A);
A14: |. S-O .| = sqrt Sum sqr (S-O) by EUCLID:def 5;
Sum sqr (S-O) >= 0 by RVSUM_1:86;
then
A15: |. S-O .|^2 = Sum sqr (S-O) by A14,SQUARE_1:def 2;
A16: delta(A,B,C) = B^2 - 4*A*C by QUIN_1:def 1;
the carrier of Tdisk(o,r) = cl_Ball(o,r) by Th3;
then |. s-o .| <= r by A4,TOPREAL9:8;
then
A17: (sqrt Sum sqr (S-O))^2 <= r^2 by A1,A3,A14,SQUARE_1:15;
then
A18: C <= 0 by A14,A15,XREAL_1:47;
now
let x be Real;
thus Polynom(A,B,C,x) = A*x^2+B*x+C by POLYEQ_1:def 2
.= A*(x-l1)*(x-l2) by A13,A18,A16,QUIN_1:16
.= A*((x-l1)*(x-l2))
.= Quard(A,l1,l2,x) by POLYEQ_1:def 3;
end;
then
A19: C/A = l1*l2 by A13,POLYEQ_1:11;
A20: now
set D = sqrt delta(A,B,C);
assume l1 > l2;
then -D - B > D - B by A13,XREAL_1:72;
hence contradiction by A13,A18,A16,XREAL_1:9;
end;
assume
A21: a = (-M+sqrt(M^2-A*C)) / A;
delta(A,B,C) = B^2 - 4*A*C by QUIN_1:def 1
.= 4*(M^2-A*C);
then
A22: l2 = (-B+sqrt(4)*sqrt(M^2-A*C)) / (2*A) by A13,A18,SQUARE_1:29
.= (2*(-(M-sqrt(M^2-A*C)))) / (2*A) by SQUARE_1:20
.= a by A21,XCMPLX_1:91;
A23: H = 1 * s -l*s + l*t by A9,RLVECT_1:35
.= s -l*s + l*t by RLVECT_1:def 8
.= s+l*t-l*s by RLVECT_1:def 3
.= s+(l*t-l*s) by RLVECT_1:def 3
.= s+l*(t-s) by RLVECT_1:34;
A24: |. l*(t-s) .|^2 = (|.l.|*|. t-s .|)^2 by TOPRNS_1:7
.= (|.l.|)^2 * |. t-s .|^2
.= l^2 * |. t-s .|^2 by COMPLEX1:75;
A*l^2+B*l+C = A*l^2+2*|(t-s,s-o)|*l+(Sum sqr (S-O) - r^2)
.= |. T-S .|^2*l^2+2*|(t-s,s-o)|*l+(|. S-O .|^2 - r^2) by A7,A15,
SQUARE_1:def 2
.= |. t-s .|^2*l^2+2*|(t-s,s-o)|*l+(|. s-o .|^2 - r^2) by A1,A2,A3
.= 0 by A24,A11;
then Polynom(A,B,C,l) = 0 by POLYEQ_1:def 2;
then
A25: l = l1 or l = l2 by A13,A18,A16,POLYEQ_1:5;
per cases by A14,A15,A17,XREAL_1:47;
suppose
C < 0;
hence thesis by A9,A10,A13,A22,A25,A19,A20,XREAL_1:141;
end;
suppose
l1 = l2;
hence thesis by A9,A22,A25;
end;
suppose
A26: C = 0;
now
A27: now
assume l = 0;
then H = s+0.TOP-REAL n by A23,RLVECT_1:10
.= s by RLVECT_1:4;
hence contradiction by A4,A5,A6,Def3;
end;
assume
A28: l = l1;
per cases;
suppose
A29: 0 < B;
then l1 = (-B-B) / (2*A) by A16,A26,SQUARE_1:22;
hence contradiction by A10,A13,A28,A29,XREAL_1:129,141;
end;
suppose
B <= 0;
then l1 = (-B--B) / (2*A) by A16,A26,SQUARE_1:23
.= 0;
hence contradiction by A28,A27;
end;
end;
hence thesis by A9,A22,A25;
end;
end;
theorem Th8:
for r1, r2, s1, s2 being Real, s, t, o being Point of
TOP-REAL 2 holds s is Point of Tdisk(o,r) & t is Point of Tdisk(o,r) & s <> t &
r1 = t`1-s`1 & r2 = t`2-s`2 & s1 = s`1-o`1 & s2 = s`2-o`2 & a = (-(s1*r1+s2*r2)
+sqrt((s1*r1+s2*r2)^2-(r1^2+r2^2)*(s1^2+s2^2-r^2))) / (r1^2+r2^2) implies HC(s,
t,o,r) = |[ s`1+a*r1, s`2+a*r2 ]|
proof
let r1, r2, s1, s2 be Real, s, t, o be Point of TOP-REAL 2 such that
A1: s is Point of Tdisk(o,r) and
A2: t is Point of Tdisk(o,r) and
A3: s <> t and
A4: r1 = t`1-s`1 & r2 = t`2-s`2 and
A5: s1 = s`1-o`1 and
A6: s2 = s`2-o`2 and
A7: a = (-(s1*r1+s2*r2)+sqrt((s1*r1+s2*r2)^2-(r1^2+r2^2)*(s1^2+s2^2-r^2)
)) / (r1^2+r2^2);
the carrier of Tdisk(o,r) = cl_Ball(o,r) by Th3;
then |. s-o .| <= r by A1,TOPREAL9:8;
then
A8: |. s-o .|^2 <= r^2 by SQUARE_1:15;
set C = s1^2+s2^2-r^2;
set A = r1^2+r2^2;
set M = s1*r1+s2*r2;
set B = 2*M;
set l1 = (- B - sqrt delta(A,B,C)) / (2 * A);
set l2 = (- B + sqrt delta(A,B,C)) / (2 * A);
A9: delta(A,B,C) = B^2 - 4*A*C by QUIN_1:def 1;
|. s-o .|^2 = ((s-o)`1)^2+((s-o)`2)^2 by JGRAPH_1:29
.= s1^2+((s-o)`2)^2 by A5,TOPREAL3:3
.= s1^2+s2^2 by A6,TOPREAL3:3;
then
A10: C <= r^2-r^2 by A8,XREAL_1:9;
then
A11: B^2 - 4*A*C >= 0;
A12: now
set D = sqrt delta(A,B,C);
assume l1 > l2;
then -D - B > D - B by XREAL_1:72;
then -D > D by XREAL_1:9;
then -D+D > D+D by XREAL_1:6;
hence contradiction by A9,A11;
end;
r1 <> 0 or r2 <> 0 by A3,A4,TOPREAL3:6;
then
A13: (0 qua Nat)+(0 qua Nat) < A by SQUARE_1:12,XREAL_1:8;
for x being Real holds Polynom(A,B,C,x) = Quard(A,l1,l2,x)
proof
let x be Real;
thus Polynom(A,B,C,x) = A*x^2+B*x+C by POLYEQ_1:def 2
.= A*(x-l1)*(x-l2) by A13,A9,A10,QUIN_1:16
.= A*((x-l1)*(x-l2))
.= Quard(A,l1,l2,x) by POLYEQ_1:def 3;
end;
then
A14: C/A = l1*l2 by A13,POLYEQ_1:11;
delta(A,B,C) = B^2 - 4*A*C by QUIN_1:def 1
.= 4*(M^2-A*C);
then
A15: l2 = (-B+sqrt(4)*sqrt(M^2-A*C)) / (2*A) by A10,SQUARE_1:29
.= (2*(-(M-sqrt(M^2-A*C)))) / (2*A) by SQUARE_1:20
.= a by A7,XCMPLX_1:91;
set H = HC(s,t,o,r);
A16: H in halfline(s,t) /\ Sphere(o,r) by A1,A2,A3,Def3;
then H in halfline(s,t) by XBOOLE_0:def 4;
then consider l being Real such that
A17: H = (1-l)*s + l*t and
A18: 0 <= l by TOPREAL9:26;
A19: H = 1 * s -l*s + l*t by A17,RLVECT_1:35
.= s -l*s + l*t by RLVECT_1:def 8
.= s+l*t-l*s by RLVECT_1:def 3
.= s+(l*t-l*s) by RLVECT_1:def 3
.= s+l*(t-s) by RLVECT_1:34;
then
A20: H`1 = s`1+(l*(t-s))`1 by TOPREAL3:2
.= s`1+l*(t-s)`1 by TOPREAL3:4
.= s`1+l*(t`1-s`1) by TOPREAL3:3;
H in Sphere(o,r) by A16,XBOOLE_0:def 4;
then |. H-o .| = r by TOPREAL9:9;
then r^2 = ((H-o)`1)^2 + ((H-o)`2)^2 by JGRAPH_1:29
.= (H`1-o`1)^2 + ((H-o)`2)^2 by TOPREAL3:3
.= (H`1-o`1)^2 + (H`2-o`2)^2 by TOPREAL3:3
.= ((1-l)*s`1+l*t`1-o`1)^2 + (H`2-o`2)^2 by A17,TOPREAL9:41
.= ((1-l)*s`1+l*t`1-o`1)^2 + ((1-l)*s`2+l*t`2-o`2)^2 by A17,TOPREAL9:42
.= l^2*(r1^2+r2^2)+l*2*M+s1^2+s2^2 by A4,A5,A6;
then A*l^2+B*l+C = 0;
then Polynom(A,B,C,l) = 0 by POLYEQ_1:def 2;
then
A21: l = l1 or l = l2 by A13,A9,A10,POLYEQ_1:5;
A22: H`2 = s`2+(l*(t-s))`2 by A19,TOPREAL3:2
.= s`2+l*(t-s)`2 by TOPREAL3:4
.= s`2+l*(t`2-s`2) by TOPREAL3:3;
per cases by A10;
suppose
C < 0;
hence thesis by A4,A18,A20,A22,A13,A15,A21,A14,A12,EUCLID:53,XREAL_1:141;
end;
suppose
l1 = l2;
hence thesis by A4,A20,A22,A15,A21,EUCLID:53;
end;
suppose
A23: C = 0;
now
A24: now
assume l = 0;
then H = s+0.TOP-REAL 2 by A19,RLVECT_1:10
.= s by RLVECT_1:4;
hence contradiction by A1,A2,A3,Def3;
end;
assume
A25: l = l1;
per cases;
suppose
A26: 0 < B;
then l1 = (-B-B) / (2*A) by A9,A23,SQUARE_1:22;
hence contradiction by A18,A13,A25,A26,XREAL_1:129,141;
end;
suppose
B <= 0;
then l1 = (-B--B) / (2*A) by A9,A23,SQUARE_1:23
.= 0;
hence contradiction by A25,A24;
end;
end;
hence thesis by A4,A20,A22,A15,A21,EUCLID:53;
end;
end;
definition
let n be non zero Element of NAT, o be Point of TOP-REAL n, r be non
negative Real;
let x be Point of Tdisk(o,r);
let f be Function of Tdisk(o,r), Tdisk(o,r) such that
A1: not x is_a_fixpoint_of f;
func HC(x,f) -> Point of Tcircle(o,r) means
:Def4:
ex y, z being Point of TOP-REAL n st y = x & z = f.x & it = HC(z,y,o,r);
existence
proof
reconsider y = x, z = f.x as Point of TOP-REAL n by PRE_TOPC:25;
x <> f.x by A1;
then reconsider a = HC(z,y,o,r) as Point of Tcircle(o,r) by Th6;
take a;
thus thesis;
end;
uniqueness;
end;
theorem Th9:
for x being Point of Tdisk(o,r), f being Function of Tdisk(o,r),
Tdisk(o,r) st not x is_a_fixpoint_of f & x is Point of Tcircle(o,r) holds HC(x,
f) = x
proof
let x be Point of Tdisk(o,r);
let f be Function of Tdisk(o,r), Tdisk(o,r) such that
A1: not x is_a_fixpoint_of f and
A2: x is Point of Tcircle(o,r);
A3: x <> f.x by A1;
A4: the carrier of Tcircle(o,r) = Sphere(o,r) by TOPREALB:9;
consider y, z being Point of TOP-REAL n such that
A5: y = x and
A6: z = f.x & HC(x,f) = HC(z,y,o,r) by A1,Def4;
x in halfline(z,y) by A5,TOPREAL9:28;
then x in halfline(z,y) /\ Sphere(o,r) by A2,A4,XBOOLE_0:def 4;
hence thesis by A3,A5,A6,Def3;
end;
theorem Th10:
for r being positive Real, o being Point of TOP-REAL 2,
Y being non empty SubSpace of Tdisk(o,r) st Y = Tcircle(o,r) holds not Y
is_a_retract_of Tdisk(o,r)
proof
let r be positive Real, o be Point of TOP-REAL 2, Y be non empty
SubSpace of Tdisk(o,r) such that
A1: Y = Tcircle(o,r);
set y0 = the Point of Y;
set X = Tdisk(o,r);
A2: y0 in the carrier of Y;
the carrier of Tcircle(o,r) = Sphere(o,r) & Sphere(o,r) c= cl_Ball(o,r)
by TOPREAL9:17,TOPREALB:9;
then reconsider x0 = y0 as Point of X by A1,A2,Th3;
reconsider a0 = 0, a1 = 1 as Point of I[01] by BORSUK_1:def 14,def 15;
set C = the constant Loop of x0;
A3: C = I[01] --> x0 by BORSUK_2:5
.= (the carrier of I[01]) --> y0;
then reconsider D = C as Function of I[01], Y;
A4: D = I[01] --> y0 & D.a0 = y0 by A3,FUNCOP_1:7;
y0,y0 are_connected & D.a1 = y0 by A3,FUNCOP_1:7;
then reconsider D as constant Loop of y0 by A4,BORSUK_2:def 2;
given R being continuous Function of X,Y such that
A5: R is being_a_retraction;
the carrier of pi_1(Y,y0) = { Class(EqRel(Y,y0),D) }
proof
set E = EqRel(Y,y0);
hereby
let x be object;
assume x in the carrier of pi_1(Y,y0);
then consider f0 being Loop of y0 such that
A6: x = Class(E,f0) by TOPALG_1:47;
reconsider g0 = f0 as Loop of x0 by TOPALG_2:1;
g0,C are_homotopic by TOPALG_2:2;
then consider f being Function of [:I[01],I[01]:], X such that
A7: f is continuous and
A8: for s being Point of I[01] holds f.(s,0) = g0.s & f.(s,1) = C.s
& for t being Point of I[01] holds f.(0,t) = x0 & f.(1,t) = x0;
f0,D are_homotopic
proof
take F = R*f;
thus F is continuous by A7;
let s be Point of I[01];
thus F.(s,0) = F. [s,a0] .= R.(f.(s,0)) by FUNCT_2:15
.= R.(g0.s) by A8
.= f0.s by A5;
thus F.(s,1) = F. [s,a1] .= R.(f.(s,1)) by FUNCT_2:15
.= R.(C.s) by A8
.= D.s by A5;
thus F.(0,s) = F. [a0,s] .= R.(f.(0,s)) by FUNCT_2:15
.= R.x0 by A8
.= y0 by A5;
thus F.(1,s) = F. [a1,s] .= R.(f.(1,s)) by FUNCT_2:15
.= R.x0 by A8
.= y0 by A5;
end;
then x = Class(E,D) by A6,TOPALG_1:46;
hence x in { Class(E,D) } by TARSKI:def 1;
end;
let x be object;
assume x in { Class(E,D) };
then
A9: x = Class(E,D) by TARSKI:def 1;
D in Loops y0 by TOPALG_1:def 1;
then x in Class E by A9,EQREL_1:def 3;
hence thesis by TOPALG_1:def 5;
end;
hence contradiction by A1;
end;
definition
let n be non zero Element of NAT;
let r be non negative Real;
let o be Point of TOP-REAL n;
let f be Function of Tdisk(o,r), Tdisk(o,r);
func BR-map(f) -> Function of Tdisk(o,r), Tcircle(o,r) means
:Def5:
for x being Point of Tdisk(o,r) holds it.x = HC(x,f);
existence
proof
defpred P[Point of Tdisk(o,r),set] means $2 = HC($1,f);
A1: for x being Point of Tdisk(o,r) ex m being Point of Tcircle(o,r) st P[
x,m];
ex h being Function of Tdisk(o,r), Tcircle(o,r) st for x being Point
of Tdisk(o,r) holds P[x,h.x] from FUNCT_2:sch 3(A1);
hence thesis;
end;
uniqueness
proof
let f1, f2 be Function of Tdisk(o,r), Tcircle(o,r) such that
A2: for x being Point of Tdisk(o,r) holds f1.x = HC(x,f) and
A3: for x being Point of Tdisk(o,r) holds f2.x = HC(x,f);
for x being Point of Tdisk(o,r) holds f1.x = f2.x
proof
let x be Point of Tdisk(o,r);
thus f1.x = HC(x,f) by A2
.= f2.x by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th11:
for o being Point of TOP-REAL n, x being Point of Tdisk(o,r), f
being Function of Tdisk(o,r), Tdisk(o,r) st not x is_a_fixpoint_of f & x is
Point of Tcircle(o,r) holds (BR-map(f)).x = x
proof
let o be Point of TOP-REAL n;
let x be Point of Tdisk(o,r);
let f be Function of Tdisk(o,r), Tdisk(o,r) such that
A1: ( not x is_a_fixpoint_of f)& x is Point of Tcircle(o,r);
thus (BR-map(f)).x = HC(x,f) by Def5
.= x by A1,Th9;
end;
theorem
for f being continuous Function of Tdisk(o,r), Tdisk(o,r) holds f
is without_fixpoints implies (BR-map(f)) | Sphere(o,r) = id
Tcircle(o,r)
proof
let f be continuous Function of Tdisk(o,r), Tdisk(o,r) such that
A1: f is without_fixpoints;
set D = cl_Ball(o,r);
set C = Sphere(o,r);
set g = BR-map(f);
dom g = the carrier of Tdisk(o,r) & the carrier of Tdisk(o,r) = D by Th3,
FUNCT_2:def 1;
then
A2: dom (g|C) = C by RELAT_1:62,TOPREAL9:17;
A3: the carrier of Tcircle(o,r) = C by TOPREALB:9;
A4: for x being object st x in dom (g|C) holds (g|C).x = (id Tcircle(o,r)).x
proof
let x be object such that
A5: x in dom (g|C);
x in dom g by A5,RELAT_1:57;
then reconsider y = x as Point of Tdisk(o,r);
A6: not x is_a_fixpoint_of f by A1;
thus (g|C).x = g.x by A5,FUNCT_1:49
.= y by A3,A5,A6,Th11
.= (id Tcircle(o,r)).x by A3,A5,FUNCT_1:18;
end;
dom id Tcircle(o,r) = the carrier of Tcircle(o,r);
hence thesis by A2,A3,A4,FUNCT_1:2;
end;
Lm1: now
let T be non empty TopSpace;
let a be Element of REAL;
set c = the carrier of T;
set f = c --> a;
thus f is continuous
proof
let Y be Subset of REAL;
A1: dom f = c by FUNCT_2:def 1;
assume Y is closed;
A2: rng f = {a} by FUNCOP_1:8;
per cases;
suppose
a in Y;
then
A3: rng f c= Y by A2,ZFMISC_1:31;
f"Y = f"(rng f /\ Y) by RELAT_1:133
.= f"rng f by A3,XBOOLE_1:28
.= [#]T by A1,RELAT_1:134;
hence thesis;
end;
suppose
not a in Y;
then
A4: rng f misses Y by A2,ZFMISC_1:50;
f"Y = f"(rng f /\ Y) by RELAT_1:133
.= f"{} by A4
.= {}T;
hence thesis;
end;
end;
end;
theorem Th13:
for r being positive Real, o being Point of TOP-REAL 2,
f being continuous Function of Tdisk(o,r), Tdisk(o,r) holds
f is without_fixpoints
implies BR-map(f) is continuous
proof
set R = R2Homeomorphism;
defpred fx2[set,set] means ex x1, x2 being Point of T2 st $1 = [x1,x2] & $2
= x2`1;
defpred dx[set,set] means ex x1, x2 being Point of T2 st $1 = [x1,x2] & $2 =
x1`1 - x2`1;
let r be positive Real, o be Point of TOP-REAL 2;
defpred xo[set,set] means ex x1, x2 being Point of T2 st $1 = [x1,x2] & $2 =
x2`1 - o`1;
defpred yo[set,set] means ex x1, x2 being Point of T2 st $1 = [x1,x2] & $2 =
x2`2 - o`2;
reconsider rr = r^2 as Element of REAL by XREAL_0:def 1;
set f1 = (the carrier of [:T2,T2:]) --> rr;
A1: for x being Element of [:T2,T2:] ex r being Element of REAL st xo[x,r]
proof
let x be Element of [:T2,T2:];
consider x1, x2 being Point of T2 such that
A2: x = [x1,x2] by BORSUK_1:10;
reconsider x2o = x2`1 - o`1 as Element of REAL by XREAL_0:def 1;
take x2o, x1, x2;
thus thesis by A2;
end;
consider xo being RealMap of [:T2,T2:] such that
A3: for x being Point of [:T2,T2:] holds xo[x,xo.x] from FUNCT_2:sch 3(
A1);
A4: for x being Element of [:T2,T2:] ex r being Element of REAL st fx2[x,r]
proof
let x be Element of [:T2,T2:];
consider x1, x2 being Point of T2 such that
A5: x = [x1,x2] by BORSUK_1:10;
reconsider x21 = x2`1 as Element of REAL by XREAL_0:def 1;
take x21, x1, x2;
thus thesis by A5;
end;
consider fx2 being RealMap of [:T2,T2:] such that
A6: for x being Point of [:T2,T2:] holds fx2[x,fx2.x] from FUNCT_2:sch
3(A4 );
A7: for x being Element of [:T2,T2:] ex r being Element of REAL st yo[x,r]
proof
let x be Element of [:T2,T2:];
consider x1, x2 being Point of T2 such that
A8: x = [x1,x2] by BORSUK_1:10;
reconsider x2o = x2`2 - o`2 as Element of REAL by XREAL_0:def 1;
take x2o, x1, x2;
thus thesis by A8;
end;
consider yo being RealMap of [:T2,T2:] such that
A9: for x being Point of [:T2,T2:] holds yo[x,yo.x] from FUNCT_2:sch 3(
A7);
reconsider f1 as continuous RealMap of [:T2,T2:] by Lm1;
set D2 = Tdisk(o,r);
set S1 = Tcircle(o,r);
set OK = DiffElems(T2,T2) /\ the carrier of [:D2,D2:];
set s = the Point of S1;
A10: |. o-o .| = |. 0.TOP-REAL 2 .| by RLVECT_1:5
.= 0 by TOPRNS_1:23;
A11: the carrier of S1 = Sphere(o,r) by TOPREALB:9;
A12: now
assume
A13: o = s;
Ball(o,r) misses Sphere(o,r) & o in Ball(o,r) by A10,TOPREAL9:7,19;
hence contradiction by A11,A13,XBOOLE_0:3;
end;
the carrier of D2 = cl_Ball(o,r) by Th3;
then
A14: o is Point of D2 by A10,TOPREAL9:8;
s in the carrier of S1 & Sphere(o,r) c= cl_Ball(o,r) by TOPREAL9:17;
then s is Point of D2 by A11,Th3;
then [o,s] in [:the carrier of D2,the carrier of D2:] by A14,ZFMISC_1:87;
then
A15: [o,s] in the carrier of [:D2,D2:] by BORSUK_1:def 2;
s is Point of T2 by PRE_TOPC:25;
then [o,s] in DiffElems(T2,T2) by A12;
then reconsider OK as non empty Subset of [:T2,T2:] by A15,XBOOLE_0:def 4;
set Zf1 = f1 | OK;
defpred fy2[set,set] means ex x1, x2 being Point of T2 st $1 = [x1,x2] & $2
= x2`2;
defpred dy[set,set] means ex y1, y2 being Point of T2 st $1 = [y1,y2] & $2 =
y1`2 - y2`2;
set TD = [:T2,T2:] | OK;
let f be continuous Function of D2,D2 such that
A16: f is without_fixpoints;
A17: for x being Element of [:T2,T2:] ex r being Element of REAL st dy[x,r]
proof
let x be Element of [:T2,T2:];
consider x1, x2 being Point of T2 such that
A18: x = [x1,x2] by BORSUK_1:10;
reconsider x12 = x1`2 - x2`2 as Element of REAL by XREAL_0:def 1;
take x12, x1, x2;
thus thesis by A18;
end;
consider dy being RealMap of [:T2,T2:] such that
A19: for y being Point of [:T2,T2:] holds dy[y,dy.y] from FUNCT_2:sch 3(
A17);
A20: for x being Element of [:T2,T2:] ex r being Element of REAL st fy2[x,r]
proof
let x be Element of [:T2,T2:];
consider x1, x2 being Point of T2 such that
A21: x = [x1,x2] by BORSUK_1:10;
reconsider x22 = x2`2 as Element of REAL by XREAL_0:def 1;
take x22, x1, x2;
thus thesis by A21;
end;
consider fy2 being RealMap of [:T2,T2:] such that
A22: for x being Point of [:T2,T2:] holds fy2[x,fy2.x] from FUNCT_2:sch
3(A20 );
A23: for x being Element of [:T2,T2:] ex r being Element of REAL st dx[x,r]
proof
let x be Element of [:T2,T2:];
consider x1, x2 being Point of T2 such that
A24: x = [x1,x2] by BORSUK_1:10;
reconsider x12 = x1`1 - x2`1 as Element of REAL by XREAL_0:def 1;
take x12, x1, x2;
thus thesis by A24;
end;
consider dx being RealMap of [:T2,T2:] such that
A25: for x being Point of [:T2,T2:] holds dx[x,dx.x] from FUNCT_2:sch 3(
A23);
reconsider Dx = dx, Dy = dy, fX2 = fx2, fY2 = fy2, Xo = xo, Yo = yo as
Function of [:T2,T2:],R^1 by TOPMETR:17;
for p being Point of [:T2,T2:], V being Subset of R^1 st Yo.p in V & V
is open holds ex W being Subset of [:T2,T2:] st p in W & W is open & Yo.:W c= V
proof
let p be Point of [:T2,T2:], V be Subset of R^1 such that
A26: Yo.p in V and
A27: V is open;
reconsider V1 = V as open Subset of REAL by A27,BORSUK_5:39,TOPMETR:17;
consider p1, p2 being Point of T2 such that
A28: p = [p1,p2] and
A29: Yo.p = p2`2 - o`2 by A9;
set r = p2`2 - o`2;
consider g being Real such that
A30: 0 < g and
A31: ].r-g,r+g.[ c= V1 by A26,A29,RCOMP_1:19;
reconsider g as Element of REAL by XREAL_0:def 1;
set W2 = {|[x,y]| where x, y is Real: p2`2-g < y & y < p2`2+g};
W2 c= the carrier of T2
proof
let a be object;
assume a in W2;
then ex x, y being Real st a = |[x,y]| & p2`2-g < y & y < p2
`2+g;
hence thesis;
end;
then reconsider W2 as Subset of T2;
take [:[#]T2,W2:];
A32: p2 = |[p2`1,p2`2]| by EUCLID:53;
p2`2-g < p2`2-0 & p2`2+(0 qua Nat) < p2`2+g by A30,XREAL_1:6,15;
then p2 in W2 by A32;
hence p in [:[#]T2,W2:] by A28,ZFMISC_1:def 2;
W2 is open by PSCOMP_1:21;
hence [:[#]T2,W2:] is open by BORSUK_1:6;
let b be object;
assume b in Yo.:[:[#]T2,W2:];
then consider a being Point of [:T2,T2:] such that
A33: a in [:[#]T2,W2:] and
A34: Yo.a = b by FUNCT_2:65;
consider a1, a2 being Point of T2 such that
A35: a = [a1,a2] and
A36: yo.a = a2`2 - o`2 by A9;
a2 in W2 by A33,A35,ZFMISC_1:87;
then consider x2, y2 being Real such that
A37: a2 = |[x2,y2]| and
A38: p2`2-g < y2 & y2 < p2`2+g;
a2`2 = y2 by A37,EUCLID:52;
then p2`2 - g - o`2 < a2`2 - o`2 & a2`2 - o`2 < p2`2 + g - o`2 by A38,
XREAL_1:9;
then a2`2 - o`2 in ].r-g,r+g.[ by XXREAL_1:4;
hence thesis by A31,A34,A36;
end;
then Yo is continuous by JGRAPH_2:10;
then reconsider yo as continuous RealMap of [:T2,T2:] by JORDAN5A:27;
for p being Point of [:T2,T2:], V being Subset of R^1 st Xo.p in V & V
is open holds ex W being Subset of [:T2,T2:] st p in W & W is open & Xo.:W c= V
proof
let p be Point of [:T2,T2:], V be Subset of R^1 such that
A39: Xo.p in V and
A40: V is open;
reconsider V1 = V as open Subset of REAL by A40,BORSUK_5:39,TOPMETR:17;
consider p1, p2 being Point of T2 such that
A41: p = [p1,p2] and
A42: Xo.p = p2`1 - o`1 by A3;
set r = p2`1 - o`1;
consider g being Real such that
A43: 0 < g and
A44: ].r-g,r+g.[ c= V1 by A39,A42,RCOMP_1:19;
reconsider g as Element of REAL by XREAL_0:def 1;
set W2 = {|[x,y]| where x, y is Real: p2`1-g < x & x < p2`1+g};
W2 c= the carrier of T2
proof
let a be object;
assume a in W2;
then ex x, y being Real st a = |[x,y]| & p2`1-g < x & x < p2
`1+g;
hence thesis;
end;
then reconsider W2 as Subset of T2;
take [:[#]T2,W2:];
A45: p2 = |[p2`1,p2`2]| by EUCLID:53;
p2`1-g < p2`1-0 & p2`1+(0 qua Nat) < p2`1+g by A43,XREAL_1:6,15;
then p2 in W2 by A45;
hence p in [:[#]T2,W2:] by A41,ZFMISC_1:def 2;
W2 is open by PSCOMP_1:19;
hence [:[#]T2,W2:] is open by BORSUK_1:6;
let b be object;
assume b in Xo.:[:[#]T2,W2:];
then consider a being Point of [:T2,T2:] such that
A46: a in [:[#]T2,W2:] and
A47: Xo.a = b by FUNCT_2:65;
consider a1, a2 being Point of T2 such that
A48: a = [a1,a2] and
A49: xo.a = a2`1 - o`1 by A3;
a2 in W2 by A46,A48,ZFMISC_1:87;
then consider x2, y2 being Real such that
A50: a2 = |[x2,y2]| and
A51: p2`1-g < x2 & x2 < p2`1+g;
a2`1 = x2 by A50,EUCLID:52;
then p2`1 - g - o`1 < a2`1 - o`1 & a2`1 - o`1 < p2`1 + g - o`1 by A51,
XREAL_1:9;
then a2`1 - o`1 in ].r-g,r+g.[ by XXREAL_1:4;
hence thesis by A44,A47,A49;
end;
then Xo is continuous by JGRAPH_2:10;
then reconsider xo as continuous RealMap of [:T2,T2:] by JORDAN5A:27;
set Zyo = yo | OK;
set Zxo = xo | OK;
set p2 = Zxo(#)Zxo + Zyo(#)Zyo - Zf1;
set g = BR-map(f);
A52: the carrier of TD = OK by PRE_TOPC:8;
for p being Point of [:T2,T2:], V being Subset of R^1 st Dy.p in V & V
is open holds ex W being Subset of [:T2,T2:] st p in W & W is open & Dy.:W c= V
proof
let p be Point of [:T2,T2:], V be Subset of R^1 such that
A53: Dy.p in V and
A54: V is open;
reconsider V1 = V as open Subset of REAL by A54,BORSUK_5:39,TOPMETR:17;
consider p1, p2 being Point of T2 such that
A55: p = [p1,p2] and
A56: dy.p = p1`2 - p2`2 by A19;
set r = p1`2 - p2`2;
consider g being Real such that
A57: 0 < g and
A58: ].r-g,r+g.[ c= V1 by A53,A56,RCOMP_1:19;
reconsider g as Element of REAL by XREAL_0:def 1;
set W2 = {|[x,y]| where x, y is Real: p2`2-g/2 < y & y < p2`2+g
/2};
A59: W2 c= the carrier of T2
proof
let a be object;
assume a in W2;
then ex x, y being Real st a = |[x,y]| & p2`2-g/2 < y & y <
p2`2+g/2;
hence thesis;
end;
A60: p2 = |[p2`1,p2`2]| by EUCLID:53;
reconsider W2 as Subset of T2 by A59;
A61: 0/2 < g/2 by A57,XREAL_1:74;
then p2`2-g/2 < p2`2-0 & p2`2+(0 qua Nat) < p2`2+g/2 by XREAL_1:6,15;
then
A62: p2 in W2 by A60;
set W1 = {|[x,y]| where x, y is Real: p1`2-g/2 < y & y < p1`2+g
/2};
W1 c= the carrier of T2
proof
let a be object;
assume a in W1;
then ex x, y being Real st a = |[x,y]| & p1`2-g/2 < y & y <
p1`2+g/2;
hence thesis;
end;
then reconsider W1 as Subset of T2;
take [:W1,W2:];
A63: p1 = |[p1`1,p1`2]| by EUCLID:53;
p1`2-g/2 < p1`2-0 & p1`2+(0 qua Nat) < p1`2+g/2 by A61,XREAL_1:6,15;
then p1 in W1 by A63;
hence p in [:W1,W2:] by A55,A62,ZFMISC_1:def 2;
W1 is open & W2 is open by PSCOMP_1:21;
hence [:W1,W2:] is open by BORSUK_1:6;
let b be object;
assume b in Dy.:[:W1,W2:];
then consider a being Point of [:T2,T2:] such that
A64: a in [:W1,W2:] and
A65: Dy.a = b by FUNCT_2:65;
consider a1, a2 being Point of T2 such that
A66: a = [a1,a2] and
A67: dy.a = a1`2 - a2`2 by A19;
a2 in W2 by A64,A66,ZFMISC_1:87;
then consider x2, y2 being Real such that
A68: a2 = |[x2,y2]| and
A69: p2`2-g/2 < y2 and
A70: y2 < p2`2+g/2;
A71: a2`2 = y2 by A68,EUCLID:52;
p2`2-y2 > p2`2-(p2`2+g/2) by A70,XREAL_1:15;
then
A72: p2`2-y2 > -g/2;
p2`2-g/2+g/2 < y2+g/2 by A69,XREAL_1:6;
then p2`2-y2 < y2+g/2-y2 by XREAL_1:9;
then
A73: |.p2`2-y2.| < g/2 by A72,SEQ_2:1;
a1 in W1 by A64,A66,ZFMISC_1:87;
then consider x1, y1 being Real such that
A74: a1 = |[x1,y1]| and
A75: p1`2-g/2 < y1 and
A76: y1 < p1`2+g/2;
p1`2-y1 > p1`2-(p1`2+g/2) by A76,XREAL_1:15;
then
A77: p1`2-y1 > -g/2;
|.p1`2-y1-(p2`2-y2).| <= |.p1`2-y1.|+|.p2`2-y2.| by COMPLEX1:57;
then
A78: |.-(p1`2-y1-(p2`2-y2)).| <= |.p1`2-y1.|+|.p2`2-y2.| by COMPLEX1:52;
p1`2-g/2+g/2 < y1+g/2 by A75,XREAL_1:6;
then p1`2-y1 < y1+g/2-y1 by XREAL_1:9;
then |.p1`2-y1.| < g/2 by A77,SEQ_2:1;
then |.p1`2-y1.|+|.p2`2-y2.| < g/2+g/2 by A73,XREAL_1:8;
then
A79: |.y1-y2-r.| < g by A78,XXREAL_0:2;
a1`2 = y1 by A74,EUCLID:52;
then a1`2 - a2`2 in ].r-g,r+g.[ by A71,A79,RCOMP_1:1;
hence thesis by A58,A65,A67;
end;
then Dy is continuous by JGRAPH_2:10;
then reconsider dy as continuous RealMap of [:T2,T2:] by JORDAN5A:27;
for p being Point of [:T2,T2:], V being Subset of R^1 st Dx.p in V & V
is open holds ex W being Subset of [:T2,T2:] st p in W & W is open & Dx.:W c= V
proof
let p be Point of [:T2,T2:], V be Subset of R^1 such that
A80: Dx.p in V and
A81: V is open;
reconsider V1 = V as open Subset of REAL by A81,BORSUK_5:39,TOPMETR:17;
consider p1, p2 being Point of T2 such that
A82: p = [p1,p2] and
A83: dx.p = p1`1 - p2`1 by A25;
set r = p1`1 - p2`1;
consider g being Real such that
A84: 0 < g and
A85: ].r-g,r+g.[ c= V1 by A80,A83,RCOMP_1:19;
reconsider g as Element of REAL by XREAL_0:def 1;
set W2 = {|[x,y]| where x, y is Real: p2`1-g/2 < x & x < p2`1+g
/2};
A86: W2 c= the carrier of T2
proof
let a be object;
assume a in W2;
then ex x, y being Real st a = |[x,y]| & p2`1-g/2 < x & x <
p2`1+g/2;
hence thesis;
end;
A87: p2 = |[p2`1,p2`2]| by EUCLID:53;
reconsider W2 as Subset of T2 by A86;
A88: 0/2 < g/2 by A84,XREAL_1:74;
then p2`1-g/2 < p2`1-0 & p2`1+(0 qua Nat) < p2`1+g/2 by XREAL_1:6,15;
then
A89: p2 in W2 by A87;
set W1 = {|[x,y]| where x, y is Real: p1`1-g/2 < x & x < p1`1+g
/2};
W1 c= the carrier of T2
proof
let a be object;
assume a in W1;
then ex x, y being Real st a = |[x,y]| & p1`1-g/2 < x & x <
p1`1+g/2;
hence thesis;
end;
then reconsider W1 as Subset of T2;
take [:W1,W2:];
A90: p1 = |[p1`1,p1`2]| by EUCLID:53;
p1`1-g/2 < p1`1-0 & p1`1+(0 qua Nat) < p1`1+g/2 by A88,XREAL_1:6,15;
then p1 in W1 by A90;
hence p in [:W1,W2:] by A82,A89,ZFMISC_1:def 2;
W1 is open & W2 is open by PSCOMP_1:19;
hence [:W1,W2:] is open by BORSUK_1:6;
let b be object;
assume b in Dx.:[:W1,W2:];
then consider a being Point of [:T2,T2:] such that
A91: a in [:W1,W2:] and
A92: Dx.a = b by FUNCT_2:65;
consider a1, a2 being Point of T2 such that
A93: a = [a1,a2] and
A94: dx.a = a1`1 - a2`1 by A25;
a2 in W2 by A91,A93,ZFMISC_1:87;
then consider x2, y2 being Real such that
A95: a2 = |[x2,y2]| and
A96: p2`1-g/2 < x2 and
A97: x2 < p2`1+g/2;
A98: a2`1 = x2 by A95,EUCLID:52;
p2`1-x2 > p2`1-(p2`1+g/2) by A97,XREAL_1:15;
then
A99: p2`1-x2 > -g/2;
p2`1-g/2+g/2 < x2+g/2 by A96,XREAL_1:6;
then p2`1-x2 < x2+g/2-x2 by XREAL_1:9;
then
A100: |.p2`1-x2.| < g/2 by A99,SEQ_2:1;
a1 in W1 by A91,A93,ZFMISC_1:87;
then consider x1, y1 being Real such that
A101: a1 = |[x1,y1]| and
A102: p1`1-g/2 < x1 and
A103: x1 < p1`1+g/2;
p1`1-x1 > p1`1-(p1`1+g/2) by A103,XREAL_1:15;
then
A104: p1`1-x1 > -g/2;
|.p1`1-x1-(p2`1-x2).| <= |.p1`1-x1.|+|.p2`1-x2.| by COMPLEX1:57;
then
A105: |.-(p1`1-x1-(p2`1-x2)).| <= |.p1`1-x1.|+|.p2`1-x2.| by COMPLEX1:52;
p1`1-g/2+g/2 < x1+g/2 by A102,XREAL_1:6;
then p1`1-x1 < x1+g/2-x1 by XREAL_1:9;
then |.p1`1-x1.| < g/2 by A104,SEQ_2:1;
then |.p1`1-x1.|+|.p2`1-x2.| < g/2+g/2 by A100,XREAL_1:8;
then
A106: |.x1-x2-r.| < g by A105,XXREAL_0:2;
a1`1 = x1 by A101,EUCLID:52;
then a1`1 - a2`1 in ].r-g,r+g.[ by A98,A106,RCOMP_1:1;
hence thesis by A85,A92,A94;
end;
then Dx is continuous by JGRAPH_2:10;
then reconsider dx as continuous RealMap of [:T2,T2:] by JORDAN5A:27;
set Zdy = dy | OK;
set Zdx = dx | OK;
set m = Zdx(#)Zdx + Zdy(#)Zdy;
for p being Point of [:T2,T2:], V being Subset of R^1 st fY2.p in V &
V is open holds ex W being Subset of [:T2,T2:] st p in W & W is open & fY2.:W
c= V
proof
let p be Point of [:T2,T2:], V be Subset of R^1 such that
A107: fY2.p in V and
A108: V is open;
reconsider V1 = V as open Subset of REAL by A108,BORSUK_5:39,TOPMETR:17;
consider p1, p2 being Point of T2 such that
A109: p = [p1,p2] and
A110: fY2.p = p2`2 by A22;
consider g being Real such that
A111: 0 < g and
A112: ].p2`2-g,p2`2+g.[ c= V1 by A107,A110,RCOMP_1:19;
reconsider g as Element of REAL by XREAL_0:def 1;
set W1 = {|[x,y]| where x, y is Real: p2`2-g < y & y < p2`2+g};
W1 c= the carrier of T2
proof
let a be object;
assume a in W1;
then ex x, y being Real st a = |[x,y]| & p2`2-g < y & y < p2
`2+g;
hence thesis;
end;
then reconsider W1 as Subset of T2;
take [:[#]T2,W1:];
A113: p2 = |[p2`1,p2`2]| by EUCLID:53;
p2`2-g < p2`2-0 & p2`2+(0 qua Nat) < p2`2+g by A111,XREAL_1:6,15;
then p2 in W1 by A113;
hence p in [:[#]T2,W1:] by A109,ZFMISC_1:def 2;
W1 is open by PSCOMP_1:21;
hence [:[#]T2,W1:] is open by BORSUK_1:6;
let b be object;
assume b in fY2.:[:[#]T2,W1:];
then consider a being Point of [:T2,T2:] such that
A114: a in [:[#]T2,W1:] and
A115: fY2.a = b by FUNCT_2:65;
consider a1, a2 being Point of T2 such that
A116: a = [a1,a2] and
A117: fY2.a = a2`2 by A22;
a2 in W1 by A114,A116,ZFMISC_1:87;
then consider x1, y1 being Real such that
A118: a2 = |[x1,y1]| and
A119: p2`2-g < y1 and
A120: y1 < p2`2+g;
p2`2-y1 > p2`2-(p2`2+g) by A120,XREAL_1:15;
then
A121: p2`2-y1 > -g;
p2`2-g+g < y1+g by A119,XREAL_1:6;
then p2`2-y1 < y1+g-y1 by XREAL_1:9;
then |.p2`2-y1.| < g by A121,SEQ_2:1;
then |.-(p2`2-y1).| < g by COMPLEX1:52;
then
A122: |.y1-p2`2.| < g;
a2`2 = y1 by A118,EUCLID:52;
then a2`2 in ].p2`2-g,p2`2+g.[ by A122,RCOMP_1:1;
hence thesis by A112,A115,A117;
end;
then fY2 is continuous by JGRAPH_2:10;
then reconsider fy2 as continuous RealMap of [:T2,T2:] by JORDAN5A:27;
for p being Point of [:T2,T2:], V being Subset of R^1 st fX2.p in V &
V is open holds ex W being Subset of [:T2,T2:] st p in W & W is open & fX2.:W
c= V
proof
let p be Point of [:T2,T2:], V be Subset of R^1 such that
A123: fX2.p in V and
A124: V is open;
reconsider V1 = V as open Subset of REAL by A124,BORSUK_5:39,TOPMETR:17;
consider p1, p2 being Point of T2 such that
A125: p = [p1,p2] and
A126: fX2.p = p2`1 by A6;
consider g being Real such that
A127: 0 < g and
A128: ].p2`1-g,p2`1+g.[ c= V1 by A123,A126,RCOMP_1:19;
reconsider g as Element of REAL by XREAL_0:def 1;
set W1 = {|[x,y]| where x, y is Real: p2`1-g < x & x < p2`1+g};
W1 c= the carrier of T2
proof
let a be object;
assume a in W1;
then ex x, y being Real st a = |[x,y]| & p2`1-g < x & x < p2
`1+g;
hence thesis;
end;
then reconsider W1 as Subset of T2;
take [:[#]T2,W1:];
A129: p2 = |[p2`1,p2`2]| by EUCLID:53;
p2`1-g < p2`1-0 & p2`1+(0 qua Nat) < p2`1+g by A127,XREAL_1:6,15;
then p2 in W1 by A129;
hence p in [:[#]T2,W1:] by A125,ZFMISC_1:def 2;
W1 is open by PSCOMP_1:19;
hence [:[#]T2,W1:] is open by BORSUK_1:6;
let b be object;
assume b in fX2.:[:[#]T2,W1:];
then consider a being Point of [:T2,T2:] such that
A130: a in [:[#]T2,W1:] and
A131: fX2.a = b by FUNCT_2:65;
consider a1, a2 being Point of T2 such that
A132: a = [a1,a2] and
A133: fX2.a = a2`1 by A6;
a2 in W1 by A130,A132,ZFMISC_1:87;
then consider x1, y1 being Real such that
A134: a2 = |[x1,y1]| and
A135: p2`1-g < x1 and
A136: x1 < p2`1+g;
p2`1-x1 > p2`1-(p2`1+g) by A136,XREAL_1:15;
then
A137: p2`1-x1 > -g;
p2`1-g+g < x1+g by A135,XREAL_1:6;
then p2`1-x1 < x1+g-x1 by XREAL_1:9;
then |.p2`1-x1.| < g by A137,SEQ_2:1;
then |.-(p2`1-x1).| < g by COMPLEX1:52;
then
A138: |.x1-p2`1.| < g;
a2`1 = x1 by A134,EUCLID:52;
then a2`1 in ].p2`1-g,p2`1+g.[ by A138,RCOMP_1:1;
hence thesis by A128,A131,A133;
end;
then fX2 is continuous by JGRAPH_2:10;
then reconsider fx2 as continuous RealMap of [:T2,T2:] by JORDAN5A:27;
set yy = Zyo(#)Zdy;
set xx = Zxo(#)Zdx;
set Zfy2 = fy2 | OK;
set Zfx2 = fx2 | OK;
set p1 = (xx+yy)(#)(xx+yy);
A139: dom p2 = the carrier of TD by FUNCT_2:def 1;
A140: for y, z being Point of D2 st y <> z holds [y,z] in OK
proof
let y, z be Point of D2;
A141: y is Point of T2 & z is Point of T2 by PRE_TOPC:25;
assume y <> z;
then [y,z] in DiffElems(T2,T2) by A141;
hence thesis by XBOOLE_0:def 4;
end;
A142: now
let b be Real;
assume b in rng p2;
then consider a being object such that
A143: a in dom p2 and
A144: p2.a = b by FUNCT_1:def 3;
a in DiffElems(T2,T2) by A143,XBOOLE_0:def 4;
then consider y, z being Point of T2 such that
A145: a = [y,z] and
A146: y <> z;
a in the carrier of [:D2,D2:] by A143,XBOOLE_0:def 4;
then consider a1, a2 being Point of D2 such that
A147: a = [a1,a2] by BORSUK_1:10;
A148: a2 = z by A145,A147,XTUPLE_0:1;
A149: a1 = y by A145,A147,XTUPLE_0:1;
then
A150: Zf1. [y,z] = f1. [y,z] by A140,A146,A148,FUNCT_1:49;
set r3 = z`1-o`1, r4 = z`2-o`2;
consider x9, x10 being Point of T2 such that
A151: [y,z] = [x9,x10] and
A152: xo. [y,z] = x10`1 - o`1 by A3;
A153: z = x10 by A151,XTUPLE_0:1;
the carrier of D2 = cl_Ball(o,r) by Th3;
then |. z-o .| <= r by A148,TOPREAL9:8;
then
A154: |. z-o .|^2 <= r^2 by SQUARE_1:15;
consider x11, x12 being Point of T2 such that
A155: [y,z] = [x11,x12] and
A156: yo. [y,z] = x12`2 - o`2 by A9;
A157: z = x12 by A155,XTUPLE_0:1;
A158: Zxo. [y,z] = xo. [y,z] & Zyo. [y,z] = yo. [y,z] by A140,A146,A149,A148,
FUNCT_1:49;
|. z-o .|^2 = ((z-o)`1)^2+((z-o)`2)^2 by JGRAPH_1:29
.= r3^2+((z-o)`2)^2 by TOPREAL3:3
.= r3^2+r4^2 by TOPREAL3:3;
then
A159: r3^2+r4^2-r^2 <= r^2-r^2 by A154,XREAL_1:9;
A160: [y,z] is Element of [#]TD by A143,A145,PRE_TOPC:def 5;
p2. [y,z] = (Zxo(#)Zxo + Zyo(#)Zyo). [y,z] - Zf1. [y,z] by A143,A145,
VALUED_1:13
.= (Zxo(#)Zxo + Zyo(#)Zyo). [y,z] - r^2 by A150,FUNCOP_1:7
.= (Zxo(#)Zxo). [y,z] + (Zyo(#)Zyo). [y,z] - r^2 by A160,VALUED_1:1
.= Zxo. [y,z] * Zxo. [y,z] + (Zyo(#)Zyo). [y,z] - r^2 by VALUED_1:5
.= r3^2+r4^2-r^2 by A158,A152,A153,A156,A157,VALUED_1:5;
hence 0 >= b by A144,A145,A159;
end;
now
let b be Real;
assume b in rng m;
then consider a being object such that
A161: a in dom m and
A162: m.a = b by FUNCT_1:def 3;
a in DiffElems(T2,T2) by A161,XBOOLE_0:def 4;
then consider y, z being Point of T2 such that
A163: a = [y,z] and
A164: y <> z;
a in the carrier of [:D2,D2:] by A161,XBOOLE_0:def 4;
then consider a1, a2 being Point of D2 such that
A165: a = [a1,a2] by BORSUK_1:10;
set r1 = y`1-z`1, r2 = y`2-z`2;
A166: now
assume r1^2+r2^2 = 0;
then r1 = 0 & r2 = 0 by COMPLEX1:1;
hence contradiction by A164,TOPREAL3:6;
end;
consider x3, x4 being Point of T2 such that
A167: [y,z] = [x3,x4] and
A168: dx. [y,z] = x3`1 - x4`1 by A25;
A169: y = x3 & z = x4 by A167,XTUPLE_0:1;
a1 = y & a2 = z by A163,A165,XTUPLE_0:1;
then
A170: Zdx. [y,z] = dx. [y,z] & Zdy. [y,z] = dy. [y,z] by A140,A164,FUNCT_1:49;
consider x5, x6 being Point of T2 such that
A171: [y,z] = [x5,x6] and
A172: dy. [y,z] = x5`2 - x6`2 by A19;
A173: y = x5 & z = x6 by A171,XTUPLE_0:1;
A174: [y,z] is Element of [#]TD by A161,A163,PRE_TOPC:def 5;
m. [y,z] = (Zdx(#)Zdx). [y,z] + (Zdy(#)Zdy). [y,z] by A174,VALUED_1:1
.= Zdx. [y,z] * Zdx. [y,z] + (Zdy(#)Zdy). [y,z] by VALUED_1:5
.= r1^2+r2^2 by A168,A169,A172,A173,A170,VALUED_1:5;
hence 0 < b by A162,A163,A166;
end;
then reconsider m as positive-yielding continuous RealMap of TD by
PARTFUN3:def 1;
reconsider p2 as nonpositive-yielding continuous RealMap of TD by A142,
PARTFUN3:def 3;
set pp = p1 - m(#)p2;
set k = (-(xx+yy) + sqrt(pp)) / m;
set x3 = Zfx2 + k(#)Zdx;
set y3 = Zfy2 + k(#)Zdy;
reconsider X3 = x3, Y3 = y3 as Function of TD,R^1 by TOPMETR:17;
set F = <:X3,Y3:>;
A175: for x being Point of D2 holds g.x = (R*F). [x,f.x]
proof
A176: dom pp = the carrier of TD by FUNCT_2:def 1;
let x be Point of D2;
A177: dom X3 = the carrier of TD & dom Y3 = the carrier of TD by FUNCT_2:def 1;
A178: not x is_a_fixpoint_of f by A16;
then
A179: x <> f.x;
consider y, z being Point of T2 such that
A180: y = x & z = f.x and
A181: HC(x,f) = HC(z,y,o,r) by A178,Def4;
A182: Zf1. [y,z] = f1. [y,z] by A140,A180,A179,FUNCT_1:49;
A183: Zxo. [y,z] = xo. [y,z] & Zyo. [y,z] = yo. [y,z] by A140,A180,A179,
FUNCT_1:49;
set r1 = y`1-z`1, r2 = y`2-z`2, r3 = z`1-o`1, r4 = z`2-o`2;
consider x9, x10 being Point of T2 such that
A184: [y,z] = [x9,x10] and
A185: xo. [y,z] = x10`1 - o`1 by A3;
A186: z = x10 by A184,XTUPLE_0:1;
consider x11, x12 being Point of T2 such that
A187: [y,z] = [x11,x12] and
A188: yo. [y,z] = x12`2 - o`2 by A9;
A189: z = x12 by A187,XTUPLE_0:1;
[x,f.x] in DiffElems (T2,T2) by A180,A179;
then
A190: [y,z] in OK by A180,XBOOLE_0:def 4;
then
A191: p2. [y,z] = (Zxo(#)Zxo + Zyo(#)Zyo). [y,z] - Zf1. [y,z] by A52,A139,
VALUED_1:13
.= (Zxo(#)Zxo + Zyo(#)Zyo). [y,z] - r^2 by A182,FUNCOP_1:7
.= (Zxo(#)Zxo). [y,z] + (Zyo(#)Zyo). [y,z] - r^2 by A52,A190,VALUED_1:1
.= Zxo. [y,z] * Zxo. [y,z] + (Zyo(#)Zyo). [y,z] - r^2 by VALUED_1:5
.= r3^2+r4^2-r^2 by A185,A186,A188,A189,A183,VALUED_1:5;
A192: Zdx. [y,z] = dx. [y,z] by A140,A180,A179,FUNCT_1:49;
consider x7, x8 being Point of T2 such that
A193: [y,z] = [x7,x8] and
A194: fy2. [y,z] = x8`2 by A22;
A195: z = x8 by A193,XTUPLE_0:1;
consider x1, x2 being Point of T2 such that
A196: [y,z] = [x1,x2] and
A197: fx2. [y,z] = x2`1 by A6;
A198: z = x2 by A196,XTUPLE_0:1;
consider x3, x4 being Point of T2 such that
A199: [y,z] = [x3,x4] and
A200: dx. [y,z] = x3`1 - x4`1 by A25;
A201: y = x3 & z = x4 by A199,XTUPLE_0:1;
set l = (-(r3*r1+r4*r2)+sqrt((r3*r1+r4*r2)^2-(r1^2+r2^2)*(r3^2+r4^2-r^2)))
/ (r1^2+r2^2);
A202: xx. [y,z] = Zxo. [y,z] * Zdx. [y,z] & yy. [y,z] = Zyo. [y,z] * Zdy.
[y,z] by VALUED_1:5;
A203: Zdy. [y,z] = dy. [y,z] by A140,A180,A179,FUNCT_1:49;
consider x5, x6 being Point of T2 such that
A204: [y,z] = [x5,x6] and
A205: dy. [y,z] = x5`2 - x6`2 by A19;
A206: y = x5 & z = x6 by A204,XTUPLE_0:1;
A207: m. [y,z] = (Zdx(#)Zdx). [y,z] + (Zdy(#)Zdy). [y,z] by A52,A190,VALUED_1:1
.= Zdx. [y,z] * Zdx. [y,z] + (Zdy(#)Zdy). [y,z] by VALUED_1:5
.= r1^2+r2^2 by A200,A201,A205,A206,A192,A203,VALUED_1:5;
A208: (xx+yy). [y,z] = xx. [y,z] + yy. [y,z] by A52,A190,VALUED_1:1;
then
A209: p1. [y,z] = (r3*r1+r4*r2)^2 by A200,A201,A205,A206,A185,A186,A188,A189
,A192,A203,A183,A202,VALUED_1:5;
dom sqrt pp = the carrier of TD by FUNCT_2:def 1;
then
A210: sqrt(pp). [y,z] = sqrt(pp. [y,z]) by A52,A190,PARTFUN3:def 5
.= sqrt(p1. [y,z] - (m(#)p2). [y,z]) by A52,A190,A176,VALUED_1:13
.= sqrt((r3*r1+r4*r2)^2-(r1^2+r2^2)*(r3^2+r4^2-r^2)) by A207,A209,A191,
VALUED_1:5;
dom k = the carrier of TD by FUNCT_2:def 1;
then
A211: k. [y,z] = (-(xx+yy) + sqrt(pp)). [y,z] * (m. [y,z])" by A52,A190,
RFUNCT_1:def 1
.= (-(xx+yy) + sqrt(pp)). [y,z] / m. [y,z] by XCMPLX_0:def 9
.= ((-(xx+yy)). [y,z] + sqrt(pp). [y,z]) / (r1^2+r2^2) by A52,A190,A207,
VALUED_1:1
.= l by A200,A201,A205,A206,A185,A186,A188,A189,A192,A203,A183,A202,A208
,A210,VALUED_1:8;
A212: Y3. [y,z] = Zfy2. [y,z] + (k(#)Zdy). [y,z] by A52,A190,VALUED_1:1
.= z`2 + (k(#)Zdy). [y,z] by A140,A180,A179,A194,A195,FUNCT_1:49
.= z`2+l*r2 by A205,A206,A203,A211,VALUED_1:5;
A213: X3. [y,z] = Zfx2. [y,z] + (k(#)Zdx). [y,z] by A52,A190,VALUED_1:1
.= z`1 + (k(#)Zdx). [y,z] by A140,A180,A179,A197,A198,FUNCT_1:49
.= z`1+l*r1 by A200,A201,A192,A211,VALUED_1:5;
thus g.x = HC(x,f) by Def5
.= |[ z`1+l*r1, z`2+l*r2 ]| by A180,A181,A179,Th8
.= R. [X3. [y,z], Y3. [y,z]] by A213,A212,TOPREALA:def 2
.= R.(F. [y,z]) by A52,A190,A177,FUNCT_3:49
.= (R*F). [x,f.x] by A52,A180,A190,FUNCT_2:15;
end;
X3 is continuous & Y3 is continuous by JORDAN5A:27;
then reconsider F as continuous Function of TD,[:R^1,R^1:] by YELLOW12:41;
for p being Point of D2, V being Subset of S1 st g.p in V & V is open
holds ex W being Subset of D2 st p in W & W is open & g.:W c= V
proof
let p be Point of D2, V be Subset of S1 such that
A214: g.p in V and
A215: V is open;
consider V1 being Subset of T2 such that
A216: V1 is open and
A217: V1 /\ [#]S1 = V by A215,TOPS_2:24;
reconsider p1 = p, fp = f.p as Point of T2 by PRE_TOPC:25;
A218: rng R = [#]T2 by TOPREALA:34,TOPS_2:def 5;
R" is being_homeomorphism by TOPREALA:34,TOPS_2:56;
then
A219: R" .:V1 is open by A216,TOPGRP_1:25;
not p is_a_fixpoint_of f by A16;
then p <> f.p;
then [p1,fp] in DiffElems (T2,T2);
then
A220: [p,f.p] in OK by XBOOLE_0:def 4;
g.p = (R*F). [p,f.p] by A175;
then (R*F). [p1,fp] in V1 by A214,A217,XBOOLE_0:def 4;
then
A221: R" .((R*F). [p1,fp]) in R" .:V1 by FUNCT_2:35;
A222: R is one-to-one by TOPREALA:34,TOPS_2:def 5;
A223: dom R = the carrier of [:R^1,R^1:] by FUNCT_2:def 1;
then
A224: rng F c= dom R;
then dom F = the carrier of [:T2,T2:] | OK & dom (R*F) = dom F by
FUNCT_2:def 1,RELAT_1:27;
then
A225: (R"*(R*F)). [p1,fp] in R" .:V1 by A52,A220,A221,FUNCT_1:13;
A226: for x being object st x in dom F holds (id dom R*F).x = F.x
proof
let x be object such that
A227: x in dom F;
A228: F.x in rng F by A227,FUNCT_1:def 3;
thus (id dom R*F).x = id dom R.(F.x) by A227,FUNCT_1:13
.= F.x by A223,A228,FUNCT_1:18;
end;
dom id dom R = dom R;
then dom (id dom R*F) = dom F by A224,RELAT_1:27;
then
A229: id dom R*F = F by A226,FUNCT_1:2;
R"*(R*F) = R"*R*F by RELAT_1:36
.= id dom R*F by A218,A222,TOPS_2:52;
then consider W being Subset of TD such that
A230: [p1,fp] in W and
A231: W is open and
A232: F.:W c= R" .:V1 by A52,A220,A219,A229,A225,JGRAPH_2:10;
consider WW being Subset of [:T2,T2:] such that
A233: WW is open and
A234: WW /\ [#]TD = W by A231,TOPS_2:24;
consider SF being Subset-Family of [:T2,T2:] such that
A235: WW = union SF and
A236: for e being set st e in SF ex X1 being Subset of T2, Y1 being
Subset of T2 st e = [:X1,Y1:] & X1 is open & Y1 is open by A233,BORSUK_1:5;
[p1,fp] in WW by A230,A234,XBOOLE_0:def 4;
then consider Z being set such that
A237: [p1,fp] in Z and
A238: Z in SF by A235,TARSKI:def 4;
set ZZ = Z /\ [#]TD;
Z c= WW by A235,A238,ZFMISC_1:74;
then ZZ c= WW /\ [#]TD by XBOOLE_1:27;
then
A239: F.:ZZ c= F.:W by A234,RELAT_1:123;
consider X1, Y1 being Subset of T2 such that
A240: Z = [:X1,Y1:] and
A241: X1 is open & Y1 is open by A236,A238;
reconsider XX = X1 /\ [#]D2, YY = Y1 /\ [#]D2 as open Subset of D2 by A241,
TOPS_2:24;
fp in Y1 by A237,A240,ZFMISC_1:87;
then fp in YY by XBOOLE_0:def 4;
then consider M being Subset of D2 such that
A242: p in M and
A243: M is open and
A244: f.:M c= YY by JGRAPH_2:10;
take W1 = XX /\ M;
p in X1 by A237,A240,ZFMISC_1:87;
then p in XX by XBOOLE_0:def 4;
hence p in W1 by A242,XBOOLE_0:def 4;
thus W1 is open by A243;
let b be object;
assume b in g.:W1;
then consider a being Point of D2 such that
A245: a in W1 and
A246: b = g.a by FUNCT_2:65;
reconsider a1 = a, fa = f.a as Point of T2 by PRE_TOPC:25;
a in M by A245,XBOOLE_0:def 4;
then fa in f.:M by FUNCT_2:35;
then
A247: f.a in Y1 by A244,XBOOLE_0:def 4;
not a is_a_fixpoint_of f by A16;
then a <> f.a;
then [a1,fa] in DiffElems (T2,T2);
then
A248: [a,f.a] in OK by XBOOLE_0:def 4;
a in XX by A245,XBOOLE_0:def 4;
then a in X1 by XBOOLE_0:def 4;
then [a,fa] in Z by A240,A247,ZFMISC_1:def 2;
then [a,fa] in ZZ by A52,A248,XBOOLE_0:def 4;
then F. [a1,fa] in F.:ZZ by FUNCT_2:35;
then F. [a1,fa] in F.:W by A239;
then R.(F. [a1,fa]) in R.:(R" .:V1) by A232,FUNCT_2:35;
then
A249: (R*F). [a1,fa] in R.:(R" .:V1) by A52,A248,FUNCT_2:15;
R is onto by A218,FUNCT_2:def 3;
then R qua Function" = R" & dom(R") = [#]T2 by A218,A222,TOPS_2:49,def 4;
then (R*F). [a1,fa] in V1 by A222,A249,PARTFUN3:1;
then g.a in V1 by A175;
hence thesis by A217,A246,XBOOLE_0:def 4;
end;
hence thesis by JGRAPH_2:10;
end;
::$N Brouwer Fixed Point Theorem
theorem Th14:
for r being non negative Real, o being Point of
TOP-REAL 2, f being continuous Function of Tdisk(o,r), Tdisk(o,r) holds f
is with_fixpoint
proof
let r be non negative Real, o be Point of TOP-REAL 2, f be
continuous Function of Tdisk(o,r), Tdisk(o,r);
A1: the carrier of Tcircle(o,r) = Sphere(o,r) by TOPREALB:9;
A2: the carrier of Tdisk(o,r) = cl_Ball(o,r) by Th3;
per cases;
suppose
r is positive;
then reconsider r as positive Real;
Sphere(o,r) c= cl_Ball(o,r) by TOPREAL9:17;
then reconsider
Y = Tcircle(o,r) as non empty SubSpace of Tdisk(o,r) by A1,A2,TSEP_1:4;
reconsider g = BR-map(f) as Function of Tdisk(o,r),Y;
A3: not Y is_a_retract_of Tdisk(o,r) by Th10;
assume
A4: f is without_fixpoints;
A5: g is being_a_retraction
by A4,Th11;
g is continuous by A4,Th13;
hence contradiction by A3,A5;
end;
suppose
r is non positive;
then reconsider r as non negative non positive Real;
take o;
A6: cl_Ball(o,r) = {o} by Th2;
dom f = the carrier of Tdisk(o,r) by FUNCT_2:def 1;
hence o in dom f by A2,A6,TARSKI:def 1;
then f.o in rng f by FUNCT_1:def 3;
hence thesis by A2,A6,TARSKI:def 1;
end;
end;
::$N Brouwer Fixed Point Theorem for Disks on the Plane
theorem
for r being non negative Real, o being Point of TOP-REAL 2, f
being continuous Function of Tdisk(o,r), Tdisk(o,r) ex x being Point of Tdisk(o
,r) st f.x = x
proof
let r be non negative Real, o be Point of TOP-REAL 2, f be
continuous Function of Tdisk(o,r), Tdisk(o,r);
f is with_fixpoint by Th14;
then consider x being object such that
A1: x is_a_fixpoint_of f;
reconsider x as set by TARSKI:1;
take x;
x in dom f by A1;
hence x is Point of Tdisk(o,r);
thus f.x = x by A1;
end;