:: BROUWER2 semantic presentation
begin
Lm1: for n being Nat
for p, q being Point of (TOP-REAL n)
for r being real number holds (((1 - r) * p) + (r * q)) - p = r * (q - p)
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n)
for r being real number holds (((1 - r) * p) + (r * q)) - p = r * (q - p)
let p, q be Point of (TOP-REAL n); ::_thesis: for r being real number holds (((1 - r) * p) + (r * q)) - p = r * (q - p)
let r be real number ; ::_thesis: (((1 - r) * p) + (r * q)) - p = r * (q - p)
thus (((1 - r) * p) + (r * q)) - p = (r * q) + (((1 - r) * p) - p) by EUCLID:45
.= (r * q) + (((1 * p) - (r * p)) - p) by EUCLID:50
.= (r * q) + ((p - (r * p)) - p) by RLVECT_1:def_8
.= (r * q) + ((p + (- (r * p))) + (- p))
.= (r * q) + ((p + (- p)) + (- (r * p))) by EUCLID:26
.= (r * q) + ((p - p) - (r * p))
.= (r * q) + ((0. (TOP-REAL n)) - (r * p)) by RLVECT_1:15
.= (r * q) - (r * p) by RLVECT_1:14
.= r * (q - p) by EUCLID:49 ; ::_thesis: verum
end;
Lm2: for n being Nat
for p being Point of (TOP-REAL n)
for r being real number st r >= 0 holds
r * p in halfline ((0. (TOP-REAL n)),p)
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n)
for r being real number st r >= 0 holds
r * p in halfline ((0. (TOP-REAL n)),p)
let p be Point of (TOP-REAL n); ::_thesis: for r being real number st r >= 0 holds
r * p in halfline ((0. (TOP-REAL n)),p)
let r be real number ; ::_thesis: ( r >= 0 implies r * p in halfline ((0. (TOP-REAL n)),p) )
A1: n in NAT by ORDINAL1:def_12;
assume A2: r >= 0 ; ::_thesis: r * p in halfline ((0. (TOP-REAL n)),p)
( (1 - r) * (0. (TOP-REAL n)) = 0. (TOP-REAL n) & (0. (TOP-REAL n)) + (r * p) = r * p ) by RLVECT_1:4, RLVECT_1:10;
hence r * p in halfline ((0. (TOP-REAL n)),p) by A1, A2, TOPREAL9:26; ::_thesis: verum
end;
theorem Th1: :: BROUWER2:1
for n being Nat
for p, q being Point of (TOP-REAL n)
for r being real number holds ((1 - r) * p) + (r * q) = p + (r * (q - p))
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n)
for r being real number holds ((1 - r) * p) + (r * q) = p + (r * (q - p))
let p, q be Point of (TOP-REAL n); ::_thesis: for r being real number holds ((1 - r) * p) + (r * q) = p + (r * (q - p))
let r be real number ; ::_thesis: ((1 - r) * p) + (r * q) = p + (r * (q - p))
thus p + (r * (q - p)) = ((((1 - r) * p) + (r * q)) - p) + p by Lm1
.= (((1 - r) * p) + (r * q)) - (p - p) by EUCLID:47
.= (((1 - r) * p) + (r * q)) - (0. (TOP-REAL n)) by RLVECT_1:15
.= ((1 - r) * p) + (r * q) by RLVECT_1:13 ; ::_thesis: verum
end;
theorem Th2: :: BROUWER2:2
for n being Nat
for u, p, q, w being Point of (TOP-REAL n) st u in halfline (p,q) & w in halfline (p,q) & |.(u - p).| = |.(w - p).| holds
u = w
proof
let n be Nat; ::_thesis: for u, p, q, w being Point of (TOP-REAL n) st u in halfline (p,q) & w in halfline (p,q) & |.(u - p).| = |.(w - p).| holds
u = w
let u, p, q, w be Point of (TOP-REAL n); ::_thesis: ( u in halfline (p,q) & w in halfline (p,q) & |.(u - p).| = |.(w - p).| implies u = w )
set r1 = u;
set r2 = w;
assume that
A1: u in halfline (p,q) and
A2: w in halfline (p,q) and
A3: |.(u - p).| = |.(w - p).| ; ::_thesis: u = w
A4: n in NAT by ORDINAL1:def_12;
percases ( p <> q or p = q ) ;
suppose p <> q ; ::_thesis: u = w
then A5: |.(q - p).| <> 0 by A4, TOPRNS_1:28;
consider a1 being real number such that
A6: u = ((1 - a1) * p) + (a1 * q) and
A7: a1 >= 0 by A1, A4, TOPREAL9:26;
A8: abs a1 = a1 by A7, ABSVALUE:def_1;
( a1 in REAL & u - p = a1 * (q - p) ) by A6, Lm1, XREAL_0:def_1;
then A9: |.(u - p).| = (abs a1) * |.(q - p).| by A4, TOPRNS_1:7;
consider a2 being real number such that
A10: w = ((1 - a2) * p) + (a2 * q) and
A11: a2 >= 0 by A2, A4, TOPREAL9:26;
( a2 in REAL & w - p = a2 * (q - p) ) by A10, Lm1, XREAL_0:def_1;
then A12: |.(w - p).| = (abs a2) * |.(q - p).| by A4, TOPRNS_1:7;
abs a2 = a2 by A11, ABSVALUE:def_1;
then a1 = a2 by A3, A5, A9, A12, A8, XCMPLX_1:5;
hence u = w by A6, A10; ::_thesis: verum
end;
supposeA13: p = q ; ::_thesis: u = w
then u in {p} by A1, A4, TOPREAL9:29;
then A14: u = p by TARSKI:def_1;
w in {p} by A2, A4, A13, TOPREAL9:29;
hence u = w by A14, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
Lm3: for n being Nat
for p, q being Point of (TOP-REAL n)
for A being Subset of (TOP-REAL n) st p in A & p <> q & A /\ (halfline (p,q)) is bounded holds
ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) & ( for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) )
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n)
for A being Subset of (TOP-REAL n) st p in A & p <> q & A /\ (halfline (p,q)) is bounded holds
ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) & ( for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) )
let p, q be Point of (TOP-REAL n); ::_thesis: for A being Subset of (TOP-REAL n) st p in A & p <> q & A /\ (halfline (p,q)) is bounded holds
ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) & ( for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) )
set TRn = TOP-REAL n;
let A be Subset of (TOP-REAL n); ::_thesis: ( p in A & p <> q & A /\ (halfline (p,q)) is bounded implies ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) & ( for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) ) )
assume that
A1: p in A and
A2: p <> q and
A3: A /\ (halfline (p,q)) is bounded ; ::_thesis: ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) & ( for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) )
reconsider P = p, Q = q as Element of (Euclid n) by EUCLID:67;
A4: dist (P,Q) > 0 by A2, METRIC_1:7;
set H = halfline (p,q);
reconsider AH = A /\ (halfline (p,q)) as bounded Subset of (Euclid n) by A3, JORDAN2C:11;
A5: n in NAT by ORDINAL1:def_12;
then A6: dist (Q,P) = |.(q - p).| by SPPOL_1:39;
p in halfline (p,q) by A5, TOPREAL9:27;
then A7: p in AH by A1, XBOOLE_0:def_4;
set DAH = diameter AH;
set X = { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } ;
set dAH = (diameter AH) + 1;
A8: now__::_thesis:_for_x_being_set_st_x_in__{__r_where_r_is_Real_:_(_((1_-_r)_*_p)_+_(r_*_q)_in_AH_&_0_<=_r_)__}__holds_
x_is_real
let x be set ; ::_thesis: ( x in { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } implies x is real )
assume x in { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } ; ::_thesis: x is real
then ex r being Real st
( x = r & ((1 - r) * p) + (r * q) in AH & 0 <= r ) ;
hence x is real ; ::_thesis: verum
end;
( 1 * p = p & 0 * q = 0. (TOP-REAL n) ) by RLVECT_1:10, RLVECT_1:def_8;
then p = ((1 - 0) * p) + (0 * q) by RLVECT_1:def_4;
then A9: 0 in { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } by A7;
then reconsider X = { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } as non empty real-membered set by A8, MEMBERED:def_3;
A10: (diameter AH) + 0 < (diameter AH) + 1 by XREAL_1:8;
now__::_thesis:_for_x_being_ext-real_number_st_x_in_X_holds_
x_<=_((diameter_AH)_+_1)_/_(dist_(Q,P))
let x be ext-real number ; ::_thesis: ( x in X implies x <= ((diameter AH) + 1) / (dist (Q,P)) )
assume x in X ; ::_thesis: x <= ((diameter AH) + 1) / (dist (Q,P))
then consider r being Real such that
A11: x = r and
A12: ((1 - r) * p) + (r * q) in AH and
A13: 0 <= r ;
reconsider PQ = ((1 - r) * p) + (r * q) as Element of (Euclid n) by A12;
(((1 - r) * p) + (r * q)) - p = r * (q - p) by Lm1;
then dist (PQ,P) = |.(r * (q - p)).| by A5, SPPOL_1:39
.= (abs r) * |.(q - p).| by A5, TOPRNS_1:7
.= r * (dist (Q,P)) by A6, A13, ABSVALUE:def_1 ;
then r * (dist (Q,P)) <= diameter AH by A7, A12, TBSP_1:def_8;
then A14: r * (dist (Q,P)) <= (diameter AH) + 1 by A10, XXREAL_0:2;
(r * (dist (Q,P))) / (dist (Q,P)) = r * ((dist (Q,P)) / (dist (Q,P)))
.= r * 1 by A4, XCMPLX_1:60 ;
hence x <= ((diameter AH) + 1) / (dist (Q,P)) by A11, A14, XREAL_1:72; ::_thesis: verum
end;
then ((diameter AH) + 1) / (dist (P,Q)) is UpperBound of X by XXREAL_2:def_1;
then X is bounded_above by XXREAL_2:def_10;
then reconsider S = sup X as Real by XXREAL_2:16;
A15: 0 <= S by A9, XXREAL_2:4;
set Spq = ((1 - S) * p) + (S * q);
reconsider spq = ((1 - S) * p) + (S * q) as Element of (Euclid n) by EUCLID:67;
A16: for r being real number st r > 0 holds
ex w being Point of (Euclid n) st
( w in AH & dist (spq,w) < r )
proof
let r be real number ; ::_thesis: ( r > 0 implies ex w being Point of (Euclid n) st
( w in AH & dist (spq,w) < r ) )
assume A17: r > 0 ; ::_thesis: ex w being Point of (Euclid n) st
( w in AH & dist (spq,w) < r )
set r2 = r / |.(q - p).|;
assume A18: for w being Point of (Euclid n) st w in AH holds
dist (spq,w) >= r ; ::_thesis: contradiction
now__::_thesis:_for_x_being_ext-real_number_st_x_in_X_holds_
S_-_(r_/_|.(q_-_p).|)_>=_x
let x be ext-real number ; ::_thesis: ( x in X implies S - (r / |.(q - p).|) >= x )
assume A19: x in X ; ::_thesis: S - (r / |.(q - p).|) >= x
then consider w being Real such that
A20: x = w and
A21: ((1 - w) * p) + (w * q) in AH and
0 <= w ;
S - w >= 0 by A19, A20, XREAL_1:48, XXREAL_2:4;
then A22: abs (S - w) = S - w by ABSVALUE:def_1;
reconsider PQ = ((1 - w) * p) + (w * q) as Element of (Euclid n) by A21;
A23: PQ = p + (w * (q - p)) by Th1;
(((1 - S) * p) + (S * q)) - (p + (w * (q - p))) = ((((1 - S) * p) + (S * q)) - p) - (w * (q - p)) by RLVECT_1:27
.= (S * (q - p)) - (w * (q - p)) by Lm1
.= (S - w) * (q - p) by RLVECT_1:35 ;
then dist (spq,PQ) = |.((S - w) * (q - p)).| by A5, A23, SPPOL_1:39
.= (S - w) * |.(q - p).| by A5, A22, TOPRNS_1:7 ;
then (S - w) * |.(q - p).| >= r by A18, A21;
then S - w >= r / |.(q - p).| by A2, A6, METRIC_1:7, XREAL_1:79;
hence S - (r / |.(q - p).|) >= x by A20, XREAL_1:11; ::_thesis: verum
end;
then S - (r / |.(q - p).|) is UpperBound of X by XXREAL_2:def_1;
then S - 0 <= S - (r / |.(q - p).|) by XXREAL_2:def_3;
hence contradiction by A4, A6, A17, XREAL_1:8; ::_thesis: verum
end;
A24: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
now__::_thesis:_for_U_being_Subset_of_(TOP-REAL_n)_st_U_is_open_&_((1_-_S)_*_p)_+_(S_*_q)_in_U_holds_
(_A_meets_U_&_U_\_A_<>_{}_)
let U be Subset of (TOP-REAL n); ::_thesis: ( U is open & ((1 - S) * p) + (S * q) in U implies ( A meets U & U \ A <> {} ) )
reconsider UE = U as Subset of (TopSpaceMetr (Euclid n)) by A24;
assume that
A25: U is open and
A26: ((1 - S) * p) + (S * q) in U ; ::_thesis: ( A meets U & U \ A <> {} )
UE in the topology of (TopSpaceMetr (Euclid n)) by A24, A25, PRE_TOPC:def_2;
then UE is open by PRE_TOPC:def_2;
then consider r being real number such that
A27: r > 0 and
A28: Ball (spq,r) c= UE by A26, TOPMETR:15;
set r2 = r / |.(q - p).|;
set Sr = S + ((r / |.(q - p).|) / 2);
consider w being Element of (Euclid n) such that
A29: ( w in AH & dist (spq,w) < r ) by A16, A27;
( w in Ball (spq,r) & w in A ) by A29, METRIC_1:11, XBOOLE_0:def_4;
hence A meets U by A28, XBOOLE_0:3; ::_thesis: U \ A <> {}
A30: (r / |.(q - p).|) * |.(q - p).| = r * (|.(q - p).| / |.(q - p).|)
.= r * 1 by A4, A6, XCMPLX_1:60 ;
S + ((r / |.(q - p).|) / 2) > S + 0 by A4, A6, A27, XREAL_1:6;
then S - (S + ((r / |.(q - p).|) / 2)) < 0 by XREAL_1:49;
then A31: abs (S - (S + ((r / |.(q - p).|) / 2))) = - (S - (S + ((r / |.(q - p).|) / 2))) by ABSVALUE:def_1
.= (r / |.(q - p).|) / 2 ;
set Srpq = ((1 - (S + ((r / |.(q - p).|) / 2))) * p) + ((S + ((r / |.(q - p).|) / 2)) * q);
reconsider srpq = ((1 - (S + ((r / |.(q - p).|) / 2))) * p) + ((S + ((r / |.(q - p).|) / 2)) * q) as Element of (Euclid n) by EUCLID:67;
A32: srpq in halfline (p,q) by A15, A27;
A33: not srpq in A
proof
assume srpq in A ; ::_thesis: contradiction
then srpq in AH by A32, XBOOLE_0:def_4;
then S + ((r / |.(q - p).|) / 2) in X by A15, A27;
then S + ((r / |.(q - p).|) / 2) <= S + 0 by XXREAL_2:4;
hence contradiction by A4, A6, A27, XREAL_1:8; ::_thesis: verum
end;
(((1 - S) * p) + (S * q)) - (((1 - (S + ((r / |.(q - p).|) / 2))) * p) + ((S + ((r / |.(q - p).|) / 2)) * q)) = (((1 - S) * p) + (S * q)) - (p + ((S + ((r / |.(q - p).|) / 2)) * (q - p))) by Th1
.= ((((1 - S) * p) + (S * q)) - p) - ((S + ((r / |.(q - p).|) / 2)) * (q - p)) by RLVECT_1:27
.= (S * (q - p)) - ((S + ((r / |.(q - p).|) / 2)) * (q - p)) by Lm1
.= (S - (S + ((r / |.(q - p).|) / 2))) * (q - p) by RLVECT_1:35 ;
then dist (spq,srpq) = |.((S - (S + ((r / |.(q - p).|) / 2))) * (q - p)).| by A5, SPPOL_1:39
.= ((r / |.(q - p).|) / 2) * |.(q - p).| by A5, A31, TOPRNS_1:7
.= r / 2 by A30 ;
then dist (spq,srpq) < r by A27, XREAL_1:216;
then srpq in Ball (spq,r) by METRIC_1:11;
hence U \ A <> {} by A28, A33, XBOOLE_0:def_5; ::_thesis: verum
end;
then A34: ((1 - S) * p) + (S * q) in Fr A by TOPGEN_1:9;
take spq ; ::_thesis: ( spq in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,spq) ) & ( for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (spq,u) < r ) ) )
A35: (((1 - S) * p) + (S * q)) - p = S * (q - p) by Lm1;
((1 - S) * p) + (S * q) in halfline (p,q) by A15;
hence spq in (Fr A) /\ (halfline (p,q)) by A34, XBOOLE_0:def_4; ::_thesis: ( ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,spq) ) & ( for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (spq,u) < r ) ) )
A36: abs S = S by A15, ABSVALUE:def_1;
hereby ::_thesis: for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (spq,u) < r )
let u, P be Point of (Euclid n); ::_thesis: ( P = p & u in A /\ (halfline (p,q)) implies dist (P,u) <= dist (P,spq) )
assume that
A37: P = p and
A38: u in A /\ (halfline (p,q)) ; ::_thesis: dist (P,u) <= dist (P,spq)
A39: dist (P,spq) = |.(S * (q - p)).| by A5, A35, A37, SPPOL_1:39
.= S * |.(q - p).| by A5, A36, TOPRNS_1:7 ;
u in halfline (p,q) by A38, XBOOLE_0:def_4;
then consider Ur being real number such that
A40: u = ((1 - Ur) * p) + (Ur * q) and
A41: 0 <= Ur by A5, TOPREAL9:26;
A42: abs Ur = Ur by A41, ABSVALUE:def_1;
Ur in REAL by XREAL_0:def_1;
then Ur in X by A38, A40, A41;
then A43: Ur <= S by XXREAL_2:4;
set du = dist (P,u);
set ds = dist (P,spq);
A44: (((1 - Ur) * p) + (Ur * q)) - p = Ur * (q - p) by Lm1;
dist (P,u) = |.(Ur * (q - p)).| by A5, A37, A40, A44, SPPOL_1:39
.= Ur * |.(q - p).| by A5, A42, TOPRNS_1:7 ;
hence dist (P,u) <= dist (P,spq) by A39, A43, XREAL_1:64; ::_thesis: verum
end;
thus for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (spq,u) < r ) by A16; ::_thesis: verum
end;
theorem :: BROUWER2:3
for n being Nat
for p, q being Point of (TOP-REAL n)
for S being Subset of (TOP-REAL n) st p in S & p <> q & S /\ (halfline (p,q)) is bounded holds
ex w being Point of (TOP-REAL n) st
( w in (Fr S) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in S /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) & ( for r being real number st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in S /\ (halfline (p,q)) & |.(w - u).| < r ) ) )
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n)
for S being Subset of (TOP-REAL n) st p in S & p <> q & S /\ (halfline (p,q)) is bounded holds
ex w being Point of (TOP-REAL n) st
( w in (Fr S) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in S /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) & ( for r being real number st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in S /\ (halfline (p,q)) & |.(w - u).| < r ) ) )
let p, q be Point of (TOP-REAL n); ::_thesis: for S being Subset of (TOP-REAL n) st p in S & p <> q & S /\ (halfline (p,q)) is bounded holds
ex w being Point of (TOP-REAL n) st
( w in (Fr S) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in S /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) & ( for r being real number st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in S /\ (halfline (p,q)) & |.(w - u).| < r ) ) )
set T = TOP-REAL n;
set E = Euclid n;
let A be Subset of (TOP-REAL n); ::_thesis: ( p in A & p <> q & A /\ (halfline (p,q)) is bounded implies ex w being Point of (TOP-REAL n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in A /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) & ( for r being real number st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) ) ) )
assume A1: ( p in A & p <> q & A /\ (halfline (p,q)) is bounded ) ; ::_thesis: ex w being Point of (TOP-REAL n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in A /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) & ( for r being real number st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) ) )
consider W being Point of (Euclid n) such that
A2: W in (Fr A) /\ (halfline (p,q)) and
A3: for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,W) and
A4: for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (W,u) < r ) by A1, Lm3;
reconsider w = W as Point of (TOP-REAL n) by EUCLID:67;
take w ; ::_thesis: ( w in (Fr A) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in A /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) & ( for r being real number st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) ) )
thus w in (Fr A) /\ (halfline (p,q)) by A2; ::_thesis: ( ( for u being Point of (TOP-REAL n) st u in A /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) & ( for r being real number st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) ) )
reconsider P = p as Point of (Euclid n) by EUCLID:67;
A5: n in NAT by ORDINAL1:def_12;
hereby ::_thesis: for r being real number st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r )
let u be Point of (TOP-REAL n); ::_thesis: ( u in A /\ (halfline (p,q)) implies |.(p - u).| <= |.(p - w).| )
assume A6: u in A /\ (halfline (p,q)) ; ::_thesis: |.(p - u).| <= |.(p - w).|
reconsider U = u as Point of (Euclid n) by EUCLID:67;
A7: dist (P,U) = |.(p - u).| by A5, SPPOL_1:39;
dist (P,U) <= dist (P,W) by A3, A6;
hence |.(p - u).| <= |.(p - w).| by A5, A7, SPPOL_1:39; ::_thesis: verum
end;
let r be real number ; ::_thesis: ( r > 0 implies ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) )
assume r > 0 ; ::_thesis: ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r )
then consider U being Point of (Euclid n) such that
A8: ( U in A /\ (halfline (p,q)) & dist (W,U) < r ) by A4;
reconsider u = U as Point of (TOP-REAL n) by EUCLID:67;
n in NAT by ORDINAL1:def_12;
then dist (W,U) = |.(w - u).| by SPPOL_1:39;
hence ex u being Point of (TOP-REAL n) st
( u in A /\ (halfline (p,q)) & |.(w - u).| < r ) by A8; ::_thesis: verum
end;
theorem Th4: :: BROUWER2:4
for n being Nat
for p, q being Point of (TOP-REAL n)
for A being convex Subset of (TOP-REAL n) st A is closed & p in Int A & p <> q & A /\ (halfline (p,q)) is bounded holds
ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u}
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n)
for A being convex Subset of (TOP-REAL n) st A is closed & p in Int A & p <> q & A /\ (halfline (p,q)) is bounded holds
ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u}
let p, q be Point of (TOP-REAL n); ::_thesis: for A being convex Subset of (TOP-REAL n) st A is closed & p in Int A & p <> q & A /\ (halfline (p,q)) is bounded holds
ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u}
set TRn = TOP-REAL n;
set En = Euclid n;
let A be convex Subset of (TOP-REAL n); ::_thesis: ( A is closed & p in Int A & p <> q & A /\ (halfline (p,q)) is bounded implies ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u} )
assume that
A1: A is closed and
A2: p in Int A and
A3: p <> q and
A4: A /\ (halfline (p,q)) is bounded ; ::_thesis: ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u}
A5: n in NAT by ORDINAL1:def_12;
reconsider P = p, Q = q as Point of (Euclid n) by EUCLID:67;
A6: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider I = Int A as Subset of (TopSpaceMetr (Euclid n)) ;
Int A in the topology of (TopSpaceMetr (Euclid n)) by A6, PRE_TOPC:def_2;
then I is open by PRE_TOPC:def_2;
then consider r being real number such that
A7: r > 0 and
A8: Ball (P,r) c= I by A2, TOPMETR:15;
dist (P,P) < r by A7, METRIC_1:1;
then A9: P in Ball (P,r) by METRIC_1:11;
set H = halfline (p,q);
reconsider AH = A /\ (halfline (p,q)) as bounded Subset of (Euclid n) by A4, JORDAN2C:11;
A10: Int A c= A by TOPS_1:16;
then consider W being Point of (Euclid n) such that
A11: W in (Fr A) /\ (halfline (p,q)) and
A12: for u, P being Point of (Euclid n) st P = p & u in AH holds
dist (P,u) <= dist (P,W) and
for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in AH & dist (W,u) < r ) by A2, A3, A4, Lm3;
reconsider w = W as Point of (TOP-REAL n) by EUCLID:67;
A13: W in Fr A by A11, XBOOLE_0:def_4;
W in halfline (p,q) by A11, XBOOLE_0:def_4;
then consider Wr being real number such that
A14: W = ((1 - Wr) * p) + (Wr * q) and
A15: Wr >= 0 by A5, TOPREAL9:26;
A16: Fr A c= A by A1, TOPS_1:35;
A17: Fr A misses Ball (P,r) by A8, TOPS_1:39, XBOOLE_1:63;
(Fr A) /\ (halfline (p,q)) = {W}
proof
assume (Fr A) /\ (halfline (p,q)) <> {W} ; ::_thesis: contradiction
then consider u being set such that
A18: u in (Fr A) /\ (halfline (p,q)) and
A19: u <> W by A11, ZFMISC_1:35;
reconsider u = u as Point of (TOP-REAL n) by A18;
A20: u in halfline (p,q) by A18, XBOOLE_0:def_4;
then consider Ur being real number such that
A21: u = ((1 - Ur) * p) + (Ur * q) and
A22: Ur >= 0 by A5, TOPREAL9:26;
A23: abs Ur = Ur by A22, ABSVALUE:def_1;
reconsider U = u as Element of (Euclid n) by EUCLID:67;
A24: Wr - Ur in REAL by XREAL_0:def_1;
(((1 - Ur) * p) + (Ur * q)) - p = Ur * (q - p) by Lm1;
then A25: dist (U,P) = |.(Ur * (q - p)).| by A5, A21, SPPOL_1:39
.= Ur * |.(q - p).| by A5, A23, TOPRNS_1:7 ;
set R = (r * (Wr - Ur)) / Wr;
reconsider b = Ball (U,((r * (Wr - Ur)) / Wr)) as Subset of (TopSpaceMetr (Euclid n)) by A6, EUCLID:67;
set x = (Wr - Ur) / Wr;
b is open by TOPMETR:14;
then b in the topology of (TOP-REAL n) by A6, PRE_TOPC:def_2;
then reconsider B = b as open Subset of (TOP-REAL n) by PRE_TOPC:def_2;
A26: abs Wr = Wr by A15, ABSVALUE:def_1;
(((1 - Wr) * p) + (Wr * q)) - p = Wr * (q - p) by Lm1;
then A27: dist (W,P) = |.(Wr * (q - p)).| by A5, A14, SPPOL_1:39
.= Wr * |.(q - p).| by A5, A26, TOPRNS_1:7 ;
A28: u in Fr A by A18, XBOOLE_0:def_4;
then A29: u in AH by A16, A20, XBOOLE_0:def_4;
P <> W by A17, A9, A13, XBOOLE_0:3;
then A30: Wr > 0 by A27, METRIC_1:7;
then A31: 1 - ((Wr - Ur) / Wr) = (Wr / Wr) - ((Wr - Ur) / Wr) by XCMPLX_1:60
.= Ur / Wr ;
P <> u by A17, A9, A28, XBOOLE_0:3;
then Ur > 0 by A25, METRIC_1:7;
then 1 - ((Wr - Ur) / Wr) >= ((Wr - Ur) / Wr) - ((Wr - Ur) / Wr) by A30, A31;
then A32: ( (Wr - Ur) / Wr in REAL & (Wr - Ur) / Wr <= 1 ) by XREAL_0:def_1, XREAL_1:6;
A33: ((1 - Wr) * p) + (Wr * q) = (Wr * (q - p)) + p by Th1;
A34: ((1 - Ur) * p) + (Ur * q) = p + (Ur * (q - p)) by Th1;
then (((1 - Wr) * p) + (Wr * q)) - (((1 - Ur) * p) + (Ur * q)) = ((p + (Wr * (q - p))) - p) - (Ur * (q - p)) by A33, RLVECT_1:27
.= ((Wr * (q - p)) + (p - p)) - (Ur * (q - p)) by EUCLID:45
.= ((Wr * (q - p)) + (0. (TOP-REAL n))) - (Ur * (q - p)) by EUCLID:42
.= (Wr * (q - p)) - (Ur * (q - p)) by RLVECT_1:def_4
.= (Wr - Ur) * (q - p) by EUCLID:50 ;
then A35: dist (U,W) = |.((Wr - Ur) * (q - p)).| by A5, A14, A21, SPPOL_1:39
.= (abs (Wr - Ur)) * |.(q - p).| by A5, A24, TOPRNS_1:7 ;
dist (U,W) > 0 by A19, METRIC_1:7;
then |.(q - p).| > 0 by A35, XREAL_1:134;
then Ur <= Wr by A12, A25, A27, A29, XREAL_1:68;
then Wr - Ur >= 0 by XREAL_1:48;
then A36: abs (Wr - Ur) = Wr - Ur by ABSVALUE:def_1;
then A37: Wr - Ur > 0 by A19, A35, METRIC_1:7;
dist (U,U) = 0 by METRIC_1:1;
then U in B by A7, A30, A37, METRIC_1:11;
then B \ A <> {} by A28, TOPGEN_1:9;
then consider t being set such that
A38: t in B \ A by XBOOLE_0:def_1;
A39: t in B by A38, XBOOLE_0:def_5;
reconsider t = t as Point of (TOP-REAL n) by A38;
set z = p + ((Wr / (Wr - Ur)) * (t - u));
reconsider Z = p + ((Wr / (Wr - Ur)) * (t - u)) as Point of (Euclid n) by EUCLID:67;
reconsider T = t as Point of (Euclid n) by EUCLID:67;
A40: dist (U,T) = |.(u - t).| by A5, SPPOL_1:39;
A41: (Wr / (Wr - Ur)) * ((r * (Wr - Ur)) / Wr) = (((Wr / Wr) * (Wr - Ur)) / (Wr - Ur)) * r
.= ((Wr - Ur) / (Wr - Ur)) * r by A30, XCMPLX_1:88
.= r by A37, XCMPLX_1:88 ;
abs (- Wr) = - (- Wr) by A30, ABSVALUE:def_1;
then A42: ( (- Wr) / (Wr - Ur) in REAL & abs ((- Wr) / (Wr - Ur)) = Wr / (Wr - Ur) ) by A36, COMPLEX1:67, XREAL_0:def_1;
A43: (Ur / Wr) * (Wr * (q - p)) = ((Ur / Wr) * Wr) * (q - p) by RLVECT_1:def_7
.= ((Wr / Wr) * Ur) * (q - p)
.= Ur * (q - p) by A30, XCMPLX_1:88 ;
p - (p + ((Wr / (Wr - Ur)) * (t - u))) = (p - p) - ((Wr / (Wr - Ur)) * (t - u)) by RLVECT_1:27
.= (0. (TOP-REAL n)) - ((Wr / (Wr - Ur)) * (t - u)) by RLVECT_1:15
.= - ((Wr / (Wr - Ur)) * (t - u)) by RLVECT_1:14
.= (- 1) * ((Wr / (Wr - Ur)) * (t - u)) by RLVECT_1:16
.= ((- 1) * (Wr / (Wr - Ur))) * (t - u) by RLVECT_1:def_7
.= ((- Wr) / (Wr - Ur)) * (t - u) ;
then A44: dist (P,Z) = |.(((- Wr) / (Wr - Ur)) * (t - u)).| by A5, SPPOL_1:39
.= (Wr / (Wr - Ur)) * |.(t - u).| by A5, A42, TOPRNS_1:7 ;
dist (U,T) < (r * (Wr - Ur)) / Wr by A39, METRIC_1:11;
then (Wr / (Wr - Ur)) * |.(u - t).| < r by A30, A37, A40, A41, XREAL_1:68;
then dist (P,Z) < r by A5, A40, A44, SPPOL_1:39;
then Z in Ball (P,r) by METRIC_1:11;
then A45: Z in I by A8;
((Wr - Ur) / Wr) * ((Wr / (Wr - Ur)) * (t - u)) = (((Wr - Ur) / Wr) * (Wr / (Wr - Ur))) * (t - u) by RLVECT_1:def_7
.= ((((Wr - Ur) / (Wr - Ur)) * Wr) / Wr) * (t - u)
.= (Wr / Wr) * (t - u) by A37, XCMPLX_1:88
.= 1 * (t - u) by A30, XCMPLX_1:60
.= t - u by RLVECT_1:def_8 ;
then ((Wr - Ur) / Wr) * (p + ((Wr / (Wr - Ur)) * (t - u))) = (((Wr - Ur) / Wr) * p) + (t - u) by RLVECT_1:def_5;
then (((Wr - Ur) / Wr) * (p + ((Wr / (Wr - Ur)) * (t - u)))) + ((1 - ((Wr - Ur) / Wr)) * w) = ((t - u) + (((Wr - Ur) / Wr) * p)) + (((1 - ((Wr - Ur) / Wr)) * p) + (Ur * (q - p))) by A14, A31, A33, A43, RLVECT_1:def_5
.= (((t - u) + (((Wr - Ur) / Wr) * p)) + ((1 - ((Wr - Ur) / Wr)) * p)) + (Ur * (q - p)) by RLVECT_1:def_3
.= ((t - u) + ((((Wr - Ur) / Wr) * p) + ((1 - ((Wr - Ur) / Wr)) * p))) + (Ur * (q - p)) by RLVECT_1:def_3
.= ((t - u) + ((((Wr - Ur) / Wr) + (1 - ((Wr - Ur) / Wr))) * p)) + (Ur * (q - p)) by RLVECT_1:def_6
.= ((t - u) + p) + (Ur * (q - p)) by RLVECT_1:def_8
.= (t - u) + u by A21, A34, RLVECT_1:def_3
.= t - (u - u) by RLVECT_1:29
.= t - (0. (TOP-REAL n)) by RLVECT_1:15
.= t by RLVECT_1:13 ;
then t in A by A16, A10, A13, A30, A32, A37, A45, RLTOPSP1:def_1;
hence contradiction by A38, XBOOLE_0:def_5; ::_thesis: verum
end;
hence ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u} by A11; ::_thesis: verum
end;
Lm4: for n being Element of NAT st n > 0 holds
for A being convex Subset of (TOP-REAL n) st A is compact & 0* n in Int A holds
ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
proof
let n be Element of NAT ; ::_thesis: ( n > 0 implies for A being convex Subset of (TOP-REAL n) st A is compact & 0* n in Int A holds
ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) )
set TRn = TOP-REAL n;
set En = Euclid n;
set cTRn = the carrier of (TOP-REAL n);
assume A1: n > 0 ; ::_thesis: for A being convex Subset of (TOP-REAL n) st A is compact & 0* n in Int A holds
ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
the carrier of (TOP-REAL n) \ {(0. (TOP-REAL n))} = {(0. (TOP-REAL n))} ` by SUBSET_1:def_4;
then reconsider cTR0 = the carrier of (TOP-REAL n) \ {(0. (TOP-REAL n))} as non empty open Subset of (TOP-REAL n) by A1;
set CL = cl_Ball ((0. (TOP-REAL n)),1);
set S = Sphere ((0. (TOP-REAL n)),1);
set TRn0 = (TOP-REAL n) | cTR0;
set nN = n NormF ;
set En = Euclid n;
set I0 = (0. (TOP-REAL n)) .--> (0. (TOP-REAL n));
let A be convex Subset of (TOP-REAL n); ::_thesis: ( A is compact & 0* n in Int A implies ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) )
assume that
A2: A is compact and
A3: 0* n in Int A ; ::_thesis: ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
A4: not A is empty by A3;
reconsider 0TRn = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67;
A5: 0* n = 0. (TOP-REAL n) by EUCLID:70;
then consider e being real number such that
A6: e > 0 and
A7: Ball (0TRn,e) c= A by A3, GOBOARD6:5;
Fr A misses Int A by TOPS_1:39;
then A8: not 0* n in Fr A by A3, XBOOLE_0:3;
then A9: (Fr A) \ {(0. (TOP-REAL n))} = Fr A by A5, ZFMISC_1:57;
set TM = TopSpaceMetr (Euclid n);
A10: [#] ((TOP-REAL n) | cTR0) = cTR0 by PRE_TOPC:def_5;
A11: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider a = A as Subset of (TopSpaceMetr (Euclid n)) ;
reconsider aa = a as Subset of (Euclid n) by EUCLID:67;
(TOP-REAL n) | A is compact by A2;
then (TopSpaceMetr (Euclid n)) | a is compact by A11, PRE_TOPC:36;
then A12: a is compact by A4, COMPTS_1:3;
A13: for p being Point of (TOP-REAL n) st p <> 0. (TOP-REAL n) holds
ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {x}
proof
let p be Point of (TOP-REAL n); ::_thesis: ( p <> 0. (TOP-REAL n) implies ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {x} )
assume A14: p <> 0. (TOP-REAL n) ; ::_thesis: ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {x}
A15: A /\ (halfline ((0. (TOP-REAL n)),p)) c= aa by XBOOLE_1:17;
then reconsider F = A /\ (halfline ((0. (TOP-REAL n)),p)) as Subset of (Euclid n) by XBOOLE_1:1;
A16: 0. (TOP-REAL n) in Int A by A3, EUCLID:70;
F is bounded by A12, A15, HAUSDORF:18, TBSP_1:14;
then A /\ (halfline ((0. (TOP-REAL n)),p)) is bounded by JORDAN2C:11;
hence ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {x} by A2, A14, A16, Th4; ::_thesis: verum
end;
not Fr A is empty
proof
set q = the Element of cTR0;
the Element of cTR0 <> 0. (TOP-REAL n) by ZFMISC_1:56;
then ex x being Point of (TOP-REAL n) st (Fr A) /\ (halfline ((0. (TOP-REAL n)), the Element of cTR0)) = {x} by A13;
hence not Fr A is empty ; ::_thesis: verum
end;
then reconsider FrA = Fr A as non empty Subset of ((TOP-REAL n) | cTR0) by A10, A9, XBOOLE_1:33;
A17: Fr A c= A by A2, TOPS_1:35;
set TS = (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1));
reconsider I = incl ((TOP-REAL n) | cTR0) as continuous Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TMAP_1:87;
A18: [#] ((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) = Sphere ((0. (TOP-REAL n)),1) by PRE_TOPC:def_5;
A19: (n NormF) | ((TOP-REAL n) | cTR0) = (n NormF) | the carrier of ((TOP-REAL n) | cTR0) by TMAP_1:def_4;
A20: not 0 in rng ((n NormF) | ((TOP-REAL n) | cTR0))
proof
assume 0 in rng ((n NormF) | ((TOP-REAL n) | cTR0)) ; ::_thesis: contradiction
then consider x being set such that
A21: x in dom ((n NormF) | ((TOP-REAL n) | cTR0)) and
A22: ((n NormF) | ((TOP-REAL n) | cTR0)) . x = 0 by FUNCT_1:def_3;
x in dom (n NormF) by A19, A21, RELAT_1:57;
then reconsider x = x as Element of (TOP-REAL n) ;
reconsider X = x as Element of REAL n by EUCLID:22;
0 = (n NormF) . x by A19, A21, A22, FUNCT_1:47
.= |.X.| by JGRAPH_4:def_1 ;
then x = 0. (TOP-REAL n) by A5, EUCLID:8;
then x in {(0. (TOP-REAL n))} by TARSKI:def_1;
hence contradiction by A10, A21, XBOOLE_0:def_5; ::_thesis: verum
end;
then reconsider nN0 = (n NormF) | ((TOP-REAL n) | cTR0) as non-empty continuous Function of ((TOP-REAL n) | cTR0),R^1 by RELAT_1:def_9;
reconsider b = I nN0 as Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TOPREALC:46;
A23: dom b = cTR0 by A10, FUNCT_2:def_1;
A24: for p being Point of (TOP-REAL n) st p in cTR0 holds
( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 )
proof
let p be Point of (TOP-REAL n); ::_thesis: ( p in cTR0 implies ( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 ) )
assume A25: p in cTR0 ; ::_thesis: ( b . p = (1 / |.p.|) * p & |.((1 / |.p.|) * p).| = 1 )
then A26: ( nN0 . p = (n NormF) . p & I . p = p ) by A10, A19, FUNCT_1:49, TMAP_1:84;
thus b . p = (I . p) (/) (nN0 . p) by A23, A25, VALUED_2:72
.= p (/) |.p.| by A26, JGRAPH_4:def_1
.= (1 / |.p.|) (#) p by VALUED_2:def_32
.= (1 / |.p.|) * p ; ::_thesis: |.((1 / |.p.|) * p).| = 1
A27: ( abs (1 / |.p.|) = 1 / |.p.| & p <> 0. (TOP-REAL n) ) by A25, ABSVALUE:def_1, ZFMISC_1:56;
thus |.((1 / |.p.|) * p).| = (abs (1 / |.p.|)) * |.p.| by TOPRNS_1:7
.= 1 by A27, TOPRNS_1:24, XCMPLX_1:87 ; ::_thesis: verum
end;
A28: rng b c= Sphere ((0. (TOP-REAL n)),1)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng b or y in Sphere ((0. (TOP-REAL n)),1) )
assume y in rng b ; ::_thesis: y in Sphere ((0. (TOP-REAL n)),1)
then consider x being set such that
A29: x in dom b and
A30: b . x = y by FUNCT_1:def_3;
reconsider x = x as Point of (TOP-REAL n) by A23, A29;
A31: ( ((1 / |.x.|) * x) - (0. (TOP-REAL n)) = (1 / |.x.|) * x & |.((1 / |.x.|) * x).| = 1 ) by A10, A24, A29, RLVECT_1:13;
y = (1 / |.x.|) * x by A10, A24, A29, A30;
hence y in Sphere ((0. (TOP-REAL n)),1) by A31; ::_thesis: verum
end;
then reconsider B = b as Function of ((TOP-REAL n) | cTR0),((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) by A10, A18, A23, FUNCT_2:2;
A32: (0. (TOP-REAL n)) .--> (0. (TOP-REAL n)) = {(0. (TOP-REAL n))} --> (0. (TOP-REAL n)) by FUNCOP_1:def_9;
then A33: dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) = {(0. (TOP-REAL n))} by FUNCOP_1:13;
set FRA = ((TOP-REAL n) | cTR0) | FrA;
set H = b | (((TOP-REAL n) | cTR0) | FrA);
A34: dom (b | (((TOP-REAL n) | cTR0) | FrA)) = the carrier of (((TOP-REAL n) | cTR0) | FrA) by FUNCT_2:def_1;
A35: b | (((TOP-REAL n) | cTR0) | FrA) = b | the carrier of (((TOP-REAL n) | cTR0) | FrA) by TMAP_1:def_4;
then A36: rng (b | (((TOP-REAL n) | cTR0) | FrA)) c= rng b by RELAT_1:70;
then A37: rng (b | (((TOP-REAL n) | cTR0) | FrA)) c= Sphere ((0. (TOP-REAL n)),1) by A28, XBOOLE_1:1;
reconsider H = b | (((TOP-REAL n) | cTR0) | FrA) as Function of (((TOP-REAL n) | cTR0) | FrA),((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) by A18, A28, A34, A36, FUNCT_2:2, XBOOLE_1:1;
A38: [#] (((TOP-REAL n) | cTR0) | FrA) = FrA by PRE_TOPC:def_5;
A39: (Fr A) \ {(0. (TOP-REAL n))} c= cTR0 by XBOOLE_1:33;
Sphere ((0. (TOP-REAL n)),1) c= rng H
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Sphere ((0. (TOP-REAL n)),1) or x in rng H )
assume x in Sphere ((0. (TOP-REAL n)),1) ; ::_thesis: x in rng H
then consider p being Point of (TOP-REAL n) such that
A40: x = p and
A41: |.(p - (0. (TOP-REAL n))).| = 1 ;
p <> 0. (TOP-REAL n) by A5, A41;
then consider q being Point of (TOP-REAL n) such that
A42: FrA /\ (halfline ((0. (TOP-REAL n)),p)) = {q} by A13;
A43: q in {q} by TARSKI:def_1;
then A44: q in FrA by A42, XBOOLE_0:def_4;
then A45: ( b . q = (1 / |.q.|) * q & b . q = H . q ) by A9, A24, A35, A38, A39, FUNCT_1:49;
q in halfline ((0. (TOP-REAL n)),p) by A42, A43, XBOOLE_0:def_4;
then halfline ((0. (TOP-REAL n)),p) = halfline ((0. (TOP-REAL n)),q) by A5, A8, A44, TOPREAL9:31;
then A46: (1 / |.q.|) * q in halfline ((0. (TOP-REAL n)),p) by Lm2;
A47: ( ((1 / |.q.|) * q) - (0. (TOP-REAL n)) = (1 / |.q.|) * q & p in halfline ((0. (TOP-REAL n)),p) ) by RLVECT_1:13, TOPREAL9:28;
( H . q in rng H & |.((1 / |.q.|) * q).| = 1 ) by A9, A24, A34, A38, A39, A44, FUNCT_1:def_3;
hence x in rng H by A40, A41, A46, A47, A45, Th2; ::_thesis: verum
end;
then A48: Sphere ((0. (TOP-REAL n)),1) = rng H by A37, XBOOLE_0:def_10;
(Fr A) \ {(0. (TOP-REAL n))} c= cTR0 by XBOOLE_1:33;
then A49: ( dom H = [#] (((TOP-REAL n) | cTR0) | FrA) & (TOP-REAL n) | (Fr A) = ((TOP-REAL n) | cTR0) | FrA ) by A9, FUNCT_2:def_1, PRE_TOPC:7;
for x1, x2 being set st x1 in dom H & x2 in dom H & H . x1 = H . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom H & x2 in dom H & H . x1 = H . x2 implies x1 = x2 )
assume that
A50: x1 in dom H and
A51: x2 in dom H and
A52: H . x1 = H . x2 ; ::_thesis: x1 = x2
A53: x2 in dom b by A35, A51, RELAT_1:57;
A54: x1 in dom b by A35, A50, RELAT_1:57;
then reconsider p1 = x1, p2 = x2 as Point of (TOP-REAL n) by A23, A53;
A55: b . p1 = (1 / |.p1.|) * p1 by A10, A24, A54;
x2 <> 0. (TOP-REAL n) by A10, A53, ZFMISC_1:56;
then consider q being Point of (TOP-REAL n) such that
A56: (Fr A) /\ (halfline ((0. (TOP-REAL n)),p2)) = {q} by A13;
p2 in halfline ((0. (TOP-REAL n)),p2) by TOPREAL9:28;
then p2 in {q} by A38, A51, A56, XBOOLE_0:def_4;
then A57: p2 = q by TARSKI:def_1;
|.((1 / |.p2.|) * p2).| = 1 by A10, A24, A53;
then A58: (1 / |.p2.|) * p2 <> 0. (TOP-REAL n) by TOPRNS_1:23;
A59: (0. (TOP-REAL n)) + ((1 / |.p2.|) * p2) = (1 / |.p2.|) * p2 by RLVECT_1:4;
A60: b . p2 = (1 / |.p2.|) * p2 by A10, A24, A53;
A61: ( H . x1 = b . x1 & H . x2 = b . x2 ) by A35, A50, A51, FUNCT_1:47;
(1 - (1 / |.p1.|)) * (0. (TOP-REAL n)) = 0. (TOP-REAL n) by RLVECT_1:10;
then A62: (1 / |.p1.|) * p1 in halfline ((0. (TOP-REAL n)),p1) by A52, A55, A59, A60, A61;
(1 - (1 / |.p2.|)) * (0. (TOP-REAL n)) = 0. (TOP-REAL n) by RLVECT_1:10;
then (1 / |.p2.|) * p2 in halfline ((0. (TOP-REAL n)),p2) by A59;
then halfline ((0. (TOP-REAL n)),p2) = halfline ((0. (TOP-REAL n)),((1 / |.p1.|) * p1)) by A52, A55, A58, A60, A61, TOPREAL9:31
.= halfline ((0. (TOP-REAL n)),p1) by A52, A55, A58, A60, A61, A62, TOPREAL9:31 ;
then p1 in halfline ((0. (TOP-REAL n)),p2) by TOPREAL9:28;
then p1 in {q} by A38, A50, A56, XBOOLE_0:def_4;
hence x1 = x2 by A57, TARSKI:def_1; ::_thesis: verum
end;
then A63: H is one-to-one by FUNCT_1:def_4;
then H is being_homeomorphism by A2, A18, A48, A49, COMPTS_1:17, PRE_TOPC:27;
then reconsider H1 = H " as continuous Function of ((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))),(((TOP-REAL n) | cTR0) | FrA) by TOPS_2:def_5;
reconsider HH = H as Function ;
set nN0F = nN0 | (((TOP-REAL n) | cTR0) | FrA);
reconsider H1B = H1 * B as Function of ((TOP-REAL n) | cTR0),(((TOP-REAL n) | cTR0) | FrA) by A48;
reconsider NH1B = (nN0 | (((TOP-REAL n) | cTR0) | FrA)) * H1B as Function of ((TOP-REAL n) | cTR0),R^1 ;
A64: nN0 | (((TOP-REAL n) | cTR0) | FrA) = nN0 | the carrier of (((TOP-REAL n) | cTR0) | FrA) by TMAP_1:def_4;
then ( rng NH1B c= rng (nN0 | (((TOP-REAL n) | cTR0) | FrA)) & rng (nN0 | (((TOP-REAL n) | cTR0) | FrA)) c= rng nN0 ) by RELAT_1:26, RELAT_1:70;
then rng NH1B c= rng nN0 by XBOOLE_1:1;
then A65: not 0 in rng NH1B by A20;
( B is continuous & not Sphere ((0. (TOP-REAL n)),1) is empty ) by A28, PRE_TOPC:27;
then reconsider NH1B = NH1B as non-empty continuous Function of ((TOP-REAL n) | cTR0),R^1 by A65, RELAT_1:def_9;
reconsider G = I NH1B as Function of ((TOP-REAL n) | cTR0),(TOP-REAL n) by TOPREALC:46;
A66: dom G = cTR0 by A10, FUNCT_2:def_1;
A67: dom (nN0 | (((TOP-REAL n) | cTR0) | FrA)) = FrA by A38, FUNCT_2:def_1;
A68: for p being Point of (TOP-REAL n) st p in cTR0 holds
ex Hp being Point of (TOP-REAL n) st
( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 )
proof
let p be Point of (TOP-REAL n); ::_thesis: ( p in cTR0 implies ex Hp being Point of (TOP-REAL n) st
( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 ) )
assume A69: p in cTR0 ; ::_thesis: ex Hp being Point of (TOP-REAL n) st
( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 )
then A70: p in dom NH1B by A10, FUNCT_2:def_1;
then A71: H1B . p in dom (nN0 | (((TOP-REAL n) | cTR0) | FrA)) by FUNCT_1:11;
then reconsider Hp = H1B . p as Point of (TOP-REAL n) by A67;
A72: (nN0 | (((TOP-REAL n) | cTR0) | FrA)) . Hp = nN0 . Hp by A64, A71, FUNCT_1:49;
A73: ( (n NormF) . Hp = |.Hp.| & nN0 . Hp = (n NormF) . Hp ) by A19, A67, A71, FUNCT_1:49, JGRAPH_4:def_1;
take Hp ; ::_thesis: ( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 )
A74: NH1B . p = (nN0 | (((TOP-REAL n) | cTR0) | FrA)) . (H1B . p) by A70, FUNCT_1:12;
G . p = (I . p) (/) (NH1B . p) by A66, A69, VALUED_2:72
.= p (/) |.Hp.| by A10, A69, A74, A72, A73, TMAP_1:84
.= (1 / |.Hp.|) (#) p by VALUED_2:def_32
.= (1 / |.Hp.|) * p ;
hence ( Hp = H1B . p & Hp in FrA & G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 ) by A38, A64, A70, A71, A74, A73, FUNCT_1:49; ::_thesis: verum
end;
A75: not 0. (TOP-REAL n) in rng G
proof
assume 0. (TOP-REAL n) in rng G ; ::_thesis: contradiction
then consider p being set such that
A76: p in dom G and
A77: G . p = 0. (TOP-REAL n) by FUNCT_1:def_3;
reconsider p = p as Point of (TOP-REAL n) by A66, A76;
consider Hp being Point of (TOP-REAL n) such that
Hp = H1B . p and
Hp in FrA and
A78: ( G . p = (1 / |.Hp.|) * p & |.Hp.| > 0 ) by A10, A68, A76;
p <> 0. (TOP-REAL n) by A10, A76, ZFMISC_1:56;
hence contradiction by A77, A78, RLVECT_1:11; ::_thesis: verum
end;
A79: for x1, x2 being set st x1 in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) & x2 in (dom G) \ (dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) holds
((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 <> G . x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) & x2 in (dom G) \ (dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) implies ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 <> G . x2 )
assume that
A80: x1 in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) and
A81: x2 in (dom G) \ (dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) ; ::_thesis: ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 <> G . x2
x1 = 0. (TOP-REAL n) by A80, TARSKI:def_1;
then A82: ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 = 0. (TOP-REAL n) by FUNCOP_1:72;
x2 in dom G by A81, XBOOLE_0:def_5;
hence ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . x1 <> G . x2 by A75, A82, FUNCT_1:def_3; ::_thesis: verum
end;
H is onto by A18, A48, FUNCT_2:def_3;
then A83: H " = HH " by A63, TOPS_2:def_4;
A84: for p being Point of (TOP-REAL n) st p in cTR0 holds
(Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {(H1B . p)}
proof
let p be Point of (TOP-REAL n); ::_thesis: ( p in cTR0 implies (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {(H1B . p)} )
assume A85: p in cTR0 ; ::_thesis: (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {(H1B . p)}
then A86: p in dom H1B by A10, FUNCT_2:def_1;
then A87: H1B . p = H1 . (B . p) by FUNCT_1:12;
B . p in dom H1 by A86, FUNCT_1:11;
then consider x being set such that
A88: x in dom H and
A89: H . x = B . p by A18, A48, FUNCT_1:def_3;
reconsider x = x as Point of (TOP-REAL n) by A34, A38, A88;
A90: H . x = b . x by A35, A88, FUNCT_1:47;
set xp = |.x.| / |.p.|;
A91: x in FrA by A38, A88;
then A92: b . x = (1 / |.x.|) * x by A9, A24, A39;
|.((1 / |.x.|) * x).| = 1 by A9, A24, A39, A91;
then (1 / |.x.|) * x <> 0. (TOP-REAL n) by TOPRNS_1:23;
then 1 / |.x.| <> 0 by RLVECT_1:10;
then |.x.| > 0 ;
then 1 = |.x.| / |.x.| by XCMPLX_1:60
.= |.x.| * (1 / |.x.|) ;
then x = (|.x.| * (1 / |.x.|)) * x by RLVECT_1:def_8
.= |.x.| * ((1 / |.x.|) * x) by RLVECT_1:def_7
.= |.x.| * ((1 / |.p.|) * p) by A24, A85, A89, A90, A92
.= (|.x.| / |.p.|) * p by RLVECT_1:def_7 ;
then x in halfline ((0. (TOP-REAL n)),p) by Lm2;
then A93: x in (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) by A38, A88, XBOOLE_0:def_4;
p <> 0. (TOP-REAL n) by A85, ZFMISC_1:56;
then consider y being Point of (TOP-REAL n) such that
A94: (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {y} by A13;
H1 . (B . p) = x by A63, A83, A88, A89, FUNCT_1:34;
hence (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {(H1B . p)} by A87, A93, A94, TARSKI:def_1; ::_thesis: verum
end;
for x1, x2 being set st x1 in dom G & x2 in dom G & G . x1 = G . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom G & x2 in dom G & G . x1 = G . x2 implies x1 = x2 )
assume that
A95: x1 in dom G and
A96: x2 in dom G and
A97: G . x1 = G . x2 ; ::_thesis: x1 = x2
reconsider p1 = x1, p2 = x2 as Point of (TOP-REAL n) by A66, A95, A96;
consider Hp1 being Point of (TOP-REAL n) such that
A98: Hp1 = H1B . p1 and
Hp1 in FrA and
A99: G . p1 = (1 / |.Hp1.|) * p1 and
A100: |.Hp1.| > 0 by A10, A68, A95;
A101: FrA /\ (halfline ((0. (TOP-REAL n)),p1)) = {Hp1} by A10, A84, A95, A98;
consider Hp2 being Point of (TOP-REAL n) such that
A102: Hp2 = H1B . p2 and
Hp2 in FrA and
A103: G . p2 = (1 / |.Hp2.|) * p2 and
|.Hp2.| > 0 by A10, A68, A96;
p1 <> 0. (TOP-REAL n) by A10, A95, ZFMISC_1:56;
then A104: (1 / |.Hp1.|) * p1 <> 0. (TOP-REAL n) by A100, RLVECT_1:11;
then halfline ((0. (TOP-REAL n)),p1) = halfline ((0. (TOP-REAL n)),((1 / |.Hp1.|) * p1)) by Lm2, TOPREAL9:31
.= halfline ((0. (TOP-REAL n)),p2) by A97, A99, A103, A104, Lm2, TOPREAL9:31 ;
then ( Hp1 in {Hp1} & {Hp1} = {Hp2} ) by A10, A84, A96, A101, A102, TARSKI:def_1;
then 1 / |.Hp1.| = 1 / |.Hp2.| by TARSKI:def_1;
hence x1 = x2 by A97, A99, A100, A103, RLVECT_1:36; ::_thesis: verum
end;
then A105: G is one-to-one by FUNCT_1:def_4;
set G0 = G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)));
A106: dom (G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) = (dom G) \/ (dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) by FUNCT_4:def_1
.= cTR0 \/ {(0. (TOP-REAL n))} by A32, A66, FUNCOP_1:13
.= the carrier of (TOP-REAL n) by ZFMISC_1:116 ;
A107: for p, Hp being Point of (TOP-REAL n) st p in cTR0 & Hp = H1B . p holds
( p = G . (|.Hp.| * p) & |.Hp.| * p in dom G )
proof
let p, Hp1 be Point of (TOP-REAL n); ::_thesis: ( p in cTR0 & Hp1 = H1B . p implies ( p = G . (|.Hp1.| * p) & |.Hp1.| * p in dom G ) )
assume that
A108: p in cTR0 and
A109: Hp1 = H1B . p ; ::_thesis: ( p = G . (|.Hp1.| * p) & |.Hp1.| * p in dom G )
reconsider p = p as Point of (TOP-REAL n) ;
consider Hp being Point of (TOP-REAL n) such that
A110: Hp = H1B . p and
Hp in FrA and
G . p = (1 / |.Hp.|) * p and
A111: |.Hp.| > 0 by A68, A108;
set Hpp = |.Hp.| * p;
p <> 0. (TOP-REAL n) by A108, ZFMISC_1:56;
then A112: |.Hp.| * p <> 0. (TOP-REAL n) by A111, RLVECT_1:11;
then A113: |.Hp.| * p in cTR0 by ZFMISC_1:56;
then consider HP being Point of (TOP-REAL n) such that
A114: HP = H1B . (|.Hp.| * p) and
HP in FrA and
A115: G . (|.Hp.| * p) = (1 / |.HP.|) * (|.Hp.| * p) and
|.HP.| > 0 by A68;
A116: Hp in {Hp} by TARSKI:def_1;
{HP} = (Fr A) /\ (halfline ((0. (TOP-REAL n)),(|.Hp.| * p))) by A84, A113, A114
.= (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) by A112, Lm2, TOPREAL9:31
.= {Hp} by A84, A108, A110 ;
then G . (|.Hp.| * p) = (1 / |.Hp.|) * (|.Hp.| * p) by A115, A116, TARSKI:def_1
.= (|.Hp.| / |.Hp.|) * p by RLVECT_1:def_7
.= 1 * p by A111, XCMPLX_1:60
.= p by RLVECT_1:def_8 ;
hence ( p = G . (|.Hp1.| * p) & |.Hp1.| * p in dom G ) by A66, A109, A110, A112, ZFMISC_1:56; ::_thesis: verum
end;
A117: Sphere ((0. (TOP-REAL n)),1) c= G .: FrA
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Sphere ((0. (TOP-REAL n)),1) or p in G .: FrA )
assume A118: p in Sphere ((0. (TOP-REAL n)),1) ; ::_thesis: p in G .: FrA
then reconsider p = p as Point of (TOP-REAL n) ;
|.p.| = 1 by A118, TOPREAL9:12;
then p <> 0. (TOP-REAL n) by TOPRNS_1:23;
then A119: p in cTR0 by ZFMISC_1:56;
then consider Hp being Point of (TOP-REAL n) such that
A120: Hp = H1B . p and
A121: Hp in FrA and
G . p = (1 / |.Hp.|) * p and
|.Hp.| > 0 by A68;
set Hpp = |.Hp.| * p;
A122: ( p = G . (|.Hp.| * p) & |.Hp.| * p in dom G ) by A107, A119, A120;
( Hp in {Hp} & (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp} ) by A84, A119, A120, TARSKI:def_1;
then A123: Hp in halfline ((0. (TOP-REAL n)),p) by XBOOLE_0:def_4;
A124: Hp - (0. (TOP-REAL n)) = Hp by RLVECT_1:13;
abs |.Hp.| = |.Hp.| by ABSVALUE:def_1;
then A125: |.(|.Hp.| * p).| = |.Hp.| * |.p.| by TOPRNS_1:7
.= |.Hp.| * 1 by A118, TOPREAL9:12 ;
( (|.Hp.| * p) - (0. (TOP-REAL n)) = |.Hp.| * p & |.Hp.| * p in halfline ((0. (TOP-REAL n)),p) ) by Lm2, RLVECT_1:13;
then Hp = |.Hp.| * p by A125, A123, A124, Th2;
hence p in G .: FrA by A121, A122, FUNCT_1:def_6; ::_thesis: verum
end;
A126: 0. (TOP-REAL n) in {(0. (TOP-REAL n))} by TARSKI:def_1;
then A127: ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . (0. (TOP-REAL n)) = 0. (TOP-REAL n) by A32, FUNCOP_1:7;
rng ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) = {(0. (TOP-REAL n))} by A32, FUNCOP_1:8;
then rng (G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n)))) = (rng G) \/ {(0. (TOP-REAL n))} by A33, A66, NECKLACE:6, XBOOLE_1:79;
then reconsider G1 = G +* ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) as one-to-one Function of (TOP-REAL n),(TOP-REAL n) by A106, A79, A105, FUNCT_2:2, TOPMETR2:1;
A128: G1 . (0. (TOP-REAL n)) = ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) . (0. (TOP-REAL n)) by A33, A126, FUNCT_4:13;
A129: G .: FrA c= Sphere ((0. (TOP-REAL n)),1)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in G .: FrA or y in Sphere ((0. (TOP-REAL n)),1) )
assume y in G .: FrA ; ::_thesis: y in Sphere ((0. (TOP-REAL n)),1)
then consider p being set such that
A130: p in dom G and
A131: p in FrA and
A132: G . p = y by FUNCT_1:def_6;
reconsider p = p as Point of (TOP-REAL n) by A131;
consider Hp being Point of (TOP-REAL n) such that
A133: Hp = H1B . p and
Hp in FrA and
A134: G . p = (1 / |.Hp.|) * p and
A135: |.Hp.| > 0 by A10, A68, A130;
p in halfline ((0. (TOP-REAL n)),p) by TOPREAL9:28;
then A136: p in FrA /\ (halfline ((0. (TOP-REAL n)),p)) by A131, XBOOLE_0:def_4;
FrA /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp} by A10, A84, A130, A133;
then A137: p = Hp by A136, TARSKI:def_1;
abs (1 / |.Hp.|) = 1 / |.Hp.| by ABSVALUE:def_1;
then |.((1 / |.Hp.|) * p).| = (1 / |.Hp.|) * |.Hp.| by A137, TOPRNS_1:7
.= 1 by A135, XCMPLX_1:106 ;
then |.(((1 / |.Hp.|) * p) - (0. (TOP-REAL n))).| = 1 by RLVECT_1:13;
hence y in Sphere ((0. (TOP-REAL n)),1) by A132, A134; ::_thesis: verum
end;
set TRnCL = (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1));
set TRnA = (TOP-REAL n) | A;
A138: Int A c= A by TOPS_1:16;
set GA = G1 | ((TOP-REAL n) | A);
A139: G1 | ((TOP-REAL n) | A) = G1 | the carrier of ((TOP-REAL n) | A) by TMAP_1:def_4;
A140: [#] ((TOP-REAL n) | A) = A by PRE_TOPC:def_5;
then A141: dom (G1 | ((TOP-REAL n) | A)) = A by FUNCT_2:def_1;
A142: dom (G1 | ((TOP-REAL n) | A)) = the carrier of ((TOP-REAL n) | A) by FUNCT_2:def_1;
A143: cl_Ball ((0. (TOP-REAL n)),1) c= rng (G1 | ((TOP-REAL n) | A))
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in cl_Ball ((0. (TOP-REAL n)),1) or p in rng (G1 | ((TOP-REAL n) | A)) )
assume A144: p in cl_Ball ((0. (TOP-REAL n)),1) ; ::_thesis: p in rng (G1 | ((TOP-REAL n) | A))
then reconsider p = p as Point of (TOP-REAL n) ;
percases ( p = 0. (TOP-REAL n) or p <> 0. (TOP-REAL n) ) ;
suppose p = 0. (TOP-REAL n) ; ::_thesis: p in rng (G1 | ((TOP-REAL n) | A))
then p = (G1 | ((TOP-REAL n) | A)) . (0. (TOP-REAL n)) by A3, A138, A5, A127, A139, A140, A128, FUNCT_1:49;
hence p in rng (G1 | ((TOP-REAL n) | A)) by A3, A138, A5, A140, A142, FUNCT_1:def_3; ::_thesis: verum
end;
supposeA145: p <> 0. (TOP-REAL n) ; ::_thesis: p in rng (G1 | ((TOP-REAL n) | A))
set h = halfline ((0. (TOP-REAL n)),p);
A146: p in cTR0 by A145, ZFMISC_1:56;
then consider Hp being Point of (TOP-REAL n) such that
A147: Hp = H1B . p and
A148: Hp in FrA and
G . p = (1 / |.Hp.|) * p and
A149: |.Hp.| > 0 by A68;
A150: abs |.Hp.| = |.Hp.| by ABSVALUE:def_1;
(Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp} by A84, A146, A147;
then Hp in (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) by TARSKI:def_1;
then A151: Hp in halfline ((0. (TOP-REAL n)),p) by XBOOLE_0:def_4;
Hp <> 0. (TOP-REAL n) by A149, TOPRNS_1:23;
then halfline ((0. (TOP-REAL n)),p) = halfline ((0. (TOP-REAL n)),Hp) by A151, TOPREAL9:31;
then A152: |.p.| * Hp in halfline ((0. (TOP-REAL n)),p) by Lm2;
|.p.| <= 1 by A144, TOPREAL9:11;
then ( (1 - |.p.|) * (0. (TOP-REAL n)) = 0. (TOP-REAL n) & (|.p.| * Hp) + ((1 - |.p.|) * (0. (TOP-REAL n))) in A ) by A3, A138, A5, A17, A148, RLTOPSP1:def_1, RLVECT_1:10;
then |.p.| * Hp in dom (G1 | ((TOP-REAL n) | A)) by A141, RLVECT_1:4;
then A153: ( (G1 | ((TOP-REAL n) | A)) . (|.p.| * Hp) in rng (G1 | ((TOP-REAL n) | A)) & (G1 | ((TOP-REAL n) | A)) . (|.p.| * Hp) = G1 . (|.p.| * Hp) ) by A139, FUNCT_1:47, FUNCT_1:def_3;
A154: |.Hp.| * p in halfline ((0. (TOP-REAL n)),p) by Lm2;
|.Hp.| * p in dom G by A107, A146, A147;
then |.Hp.| * p <> 0. (TOP-REAL n) by A10, ZFMISC_1:56;
then not |.Hp.| * p in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) by TARSKI:def_1;
then A155: G . (|.Hp.| * p) = G1 . (|.Hp.| * p) by FUNCT_4:11;
abs |.p.| = |.p.| by ABSVALUE:def_1;
then |.(|.p.| * Hp).| = |.p.| * |.Hp.| by TOPRNS_1:7
.= |.(|.Hp.| * p).| by A150, TOPRNS_1:7 ;
then A156: |.((|.p.| * Hp) - (0. (TOP-REAL n))).| = |.(|.Hp.| * p).| by RLVECT_1:13
.= |.((|.Hp.| * p) - (0. (TOP-REAL n))).| by RLVECT_1:13 ;
p = G . (|.Hp.| * p) by A107, A146, A147;
hence p in rng (G1 | ((TOP-REAL n) | A)) by A152, A155, A156, A153, A154, Th2; ::_thesis: verum
end;
end;
end;
rng (G1 | ((TOP-REAL n) | A)) c= cl_Ball ((0. (TOP-REAL n)),1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (G1 | ((TOP-REAL n) | A)) or x in cl_Ball ((0. (TOP-REAL n)),1) )
assume x in rng (G1 | ((TOP-REAL n) | A)) ; ::_thesis: x in cl_Ball ((0. (TOP-REAL n)),1)
then consider p being set such that
A157: p in dom (G1 | ((TOP-REAL n) | A)) and
A158: (G1 | ((TOP-REAL n) | A)) . p = x by FUNCT_1:def_3;
reconsider p = p as Point of (TOP-REAL n) by A141, A157;
A159: (G1 | ((TOP-REAL n) | A)) . p = G1 . p by A139, A157, FUNCT_1:47;
A160: (G1 . p) - (0. (TOP-REAL n)) = G1 . p by RLVECT_1:13;
percases ( p = 0. (TOP-REAL n) or p <> 0. (TOP-REAL n) ) ;
suppose p = 0. (TOP-REAL n) ; ::_thesis: x in cl_Ball ((0. (TOP-REAL n)),1)
then G1 . p = 0. (TOP-REAL n) by A32, A126, A128, FUNCOP_1:7;
then |.((G1 . p) - (0. (TOP-REAL n))).| = 0 by A160, TOPRNS_1:23;
hence x in cl_Ball ((0. (TOP-REAL n)),1) by A158, A159; ::_thesis: verum
end;
supposeA161: p <> 0. (TOP-REAL n) ; ::_thesis: x in cl_Ball ((0. (TOP-REAL n)),1)
set h = halfline ((0. (TOP-REAL n)),p);
A162: A /\ (halfline ((0. (TOP-REAL n)),p)) c= aa by XBOOLE_1:17;
then reconsider F = A /\ (halfline ((0. (TOP-REAL n)),p)) as Subset of (Euclid n) by XBOOLE_1:1;
F is bounded by A12, A162, HAUSDORF:18, TBSP_1:14;
then A /\ (halfline ((0. (TOP-REAL n)),p)) is bounded by JORDAN2C:11;
then consider w being Point of (Euclid n) such that
A163: w in (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) and
A164: for u, P being Point of (Euclid n) st P = 0. (TOP-REAL n) & u in A /\ (halfline ((0. (TOP-REAL n)),p)) holds
dist (P,u) <= dist (P,w) and
for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline ((0. (TOP-REAL n)),p)) & dist (w,u) < r ) by A3, A138, A5, A161, Lm3;
reconsider P = p as Point of (Euclid n) by EUCLID:67;
p in halfline ((0. (TOP-REAL n)),p) by TOPREAL9:28;
then A165: p in A /\ (halfline ((0. (TOP-REAL n)),p)) by A140, A157, XBOOLE_0:def_4;
A166: not p in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) by A161, TARSKI:def_1;
A167: p in cTR0 by A161, ZFMISC_1:56;
then consider Hp being Point of (TOP-REAL n) such that
A168: Hp = H1B . p and
Hp in FrA and
A169: G . p = (1 / |.Hp.|) * p and
|.Hp.| > 0 by A68;
abs (1 / |.Hp.|) = 1 / |.Hp.| by ABSVALUE:def_1;
then A170: |.((1 / |.Hp.|) * p).| = |.p.| / |.Hp.| by TOPRNS_1:7;
(Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp} by A84, A167, A168;
then w = Hp by A163, TARSKI:def_1;
then A171: dist (0TRn,w) = |.((0. (TOP-REAL n)) - Hp).| by SPPOL_1:39
.= |.(- Hp).| by RLVECT_1:14
.= |.Hp.| by TOPRNS_1:26 ;
dist (0TRn,P) = |.((0. (TOP-REAL n)) - p).| by SPPOL_1:39
.= |.(- p).| by RLVECT_1:14
.= |.p.| by TOPRNS_1:26 ;
then |.((1 / |.Hp.|) * p).| <= 1 by A164, A165, A170, A171, XREAL_1:183;
then |.(G1 . p).| <= 1 by A166, A169, FUNCT_4:11;
hence x in cl_Ball ((0. (TOP-REAL n)),1) by A158, A159, A160; ::_thesis: verum
end;
end;
end;
then A172: rng (G1 | ((TOP-REAL n) | A)) = cl_Ball ((0. (TOP-REAL n)),1) by A143, XBOOLE_0:def_10;
A173: [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def_5;
then reconsider GA = G1 | ((TOP-REAL n) | A) as Function of ((TOP-REAL n) | A),((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by A140, A141, A172, FUNCT_2:1;
set e2 = e / 2;
A174: GA is one-to-one by A139, FUNCT_1:52;
A175: e / 2 < e by A6, XREAL_1:216;
A176: G1 is continuous
proof
let x be Point of (TOP-REAL n); :: according to BORSUK_1:def_1 ::_thesis: for b1 being a_neighborhood of G1 . x ex b2 being a_neighborhood of x st G1 .: b2 c= b1
let U be a_neighborhood of G1 . x; ::_thesis: ex b1 being a_neighborhood of x st G1 .: b1 c= U
percases ( x <> 0. (TOP-REAL n) or x = 0. (TOP-REAL n) ) ;
supposeA177: x <> 0. (TOP-REAL n) ; ::_thesis: ex b1 being a_neighborhood of x st G1 .: b1 c= U
then A178: x in dom G by A66, ZFMISC_1:56;
then reconsider X = x as Point of ((TOP-REAL n) | cTR0) ;
not x in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) by A177, TARSKI:def_1;
then A179: G . x = G1 . x by FUNCT_4:11;
then A180: G1 . x <> 0. (TOP-REAL n) by A75, A178, FUNCT_1:def_3;
then reconsider G1x = G1 . x as Point of ((TOP-REAL n) | cTR0) by A10, ZFMISC_1:56;
G1 . x in cTR0 by A180, ZFMISC_1:56;
then cTR0 is a_neighborhood of G1 . x by CONNSP_2:3;
then cTR0 /\ U is a_neighborhood of G1 . x by CONNSP_2:2;
then consider H being a_neighborhood of X such that
A181: G .: H c= cTR0 /\ U by A179, BORSUK_1:def_1;
reconsider h = H as Subset of (TOP-REAL n) by A10, XBOOLE_1:1;
reconsider h = h as a_neighborhood of x by CONNSP_2:9;
{(0. (TOP-REAL n))} misses H by A10, XBOOLE_1:63, XBOOLE_1:79;
then ( cTR0 /\ U c= U & G .: H = G1 .: h ) by A32, BOOLMARK:3, XBOOLE_1:17;
hence ex b1 being a_neighborhood of x st G1 .: b1 c= U by A181, XBOOLE_1:1; ::_thesis: verum
reconsider U1 = cTR0 /\ U as Subset of ((TOP-REAL n) | cTR0) by A10, XBOOLE_1:17;
end;
supposeA182: x = 0. (TOP-REAL n) ; ::_thesis: ex b1 being a_neighborhood of x st G1 .: b1 c= U
reconsider 0TRn = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67;
A183: 0. (TOP-REAL n) in Int U by A127, A128, A182, CONNSP_2:def_1;
then consider r being real number such that
A184: r > 0 and
A185: Ball (0TRn,r) c= U by GOBOARD6:5;
reconsider B = Ball (0TRn,(r * (e / 2))) as Subset of (TOP-REAL n) by EUCLID:67;
0TRn in Int B by A6, A184, GOBOARD6:5;
then reconsider Bx = B as a_neighborhood of x by A182, CONNSP_2:def_1;
take Bx ; ::_thesis: G1 .: Bx c= U
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in G1 .: Bx or y in U )
assume A186: y in G1 .: Bx ; ::_thesis: y in U
then reconsider p = y as Point of (TOP-REAL n) ;
A187: Int U c= U by TOPS_1:16;
percases ( y = 0. (TOP-REAL n) or p <> 0. (TOP-REAL n) ) ;
suppose y = 0. (TOP-REAL n) ; ::_thesis: y in U
hence y in U by A183, A187; ::_thesis: verum
end;
supposeA188: p <> 0. (TOP-REAL n) ; ::_thesis: y in U
set PP = ((e / 2) / |.p.|) * p;
abs ((e / 2) / |.p.|) = (e / 2) / |.p.| by A6, ABSVALUE:def_1;
then A189: |.(((e / 2) / |.p.|) * p).| = ((e / 2) / |.p.|) * |.p.| by TOPRNS_1:7
.= (e / 2) * (|.p.| / |.p.|)
.= (e / 2) * 1 by A188, TOPRNS_1:24, XCMPLX_1:60
.= e / 2 ;
then |.((((e / 2) / |.p.|) * p) - (0. (TOP-REAL n))).| < e by A175, RLVECT_1:13;
then A190: ((e / 2) / |.p.|) * p in Ball ((0. (TOP-REAL n)),e) ;
set h = halfline ((0. (TOP-REAL n)),p);
A191: A /\ (halfline ((0. (TOP-REAL n)),p)) c= aa by XBOOLE_1:17;
then reconsider F = A /\ (halfline ((0. (TOP-REAL n)),p)) as Subset of (Euclid n) by XBOOLE_1:1;
F is bounded by A12, A191, HAUSDORF:18, TBSP_1:14;
then A /\ (halfline ((0. (TOP-REAL n)),p)) is bounded by JORDAN2C:11;
then consider w being Point of (Euclid n) such that
A192: w in (Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) and
A193: for u, P being Point of (Euclid n) st P = 0. (TOP-REAL n) & u in A /\ (halfline ((0. (TOP-REAL n)),p)) holds
dist (P,u) <= dist (P,w) and
for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline ((0. (TOP-REAL n)),p)) & dist (w,u) < r ) by A3, A138, A5, A188, Lm3;
A194: p in cTR0 by A188, ZFMISC_1:56;
then consider Hp being Point of (TOP-REAL n) such that
A195: Hp = H1B . p and
Hp in FrA and
G . p = (1 / |.Hp.|) * p and
A196: |.Hp.| > 0 by A68;
(Fr A) /\ (halfline ((0. (TOP-REAL n)),p)) = {Hp} by A84, A194, A195;
then w = Hp by A192, TARSKI:def_1;
then A197: dist (0TRn,w) = |.((0. (TOP-REAL n)) - Hp).| by SPPOL_1:39
.= |.(- Hp).| by RLVECT_1:14
.= |.Hp.| by TOPRNS_1:26 ;
set Hpp = |.Hp.| * p;
|.Hp.| * p in dom G by A107, A194, A195;
then |.Hp.| * p <> 0. (TOP-REAL n) by A10, ZFMISC_1:56;
then not |.Hp.| * p in dom ((0. (TOP-REAL n)) .--> (0. (TOP-REAL n))) by TARSKI:def_1;
then A198: G . (|.Hp.| * p) = G1 . (|.Hp.| * p) by FUNCT_4:11;
|.Hp.| = abs |.Hp.| by ABSVALUE:def_1;
then A199: ( Bx = Ball ((0. (TOP-REAL n)),(r * (e / 2))) & |.(|.Hp.| * p).| = |.Hp.| * |.p.| ) by TOPREAL9:13, TOPRNS_1:7;
reconsider pp = ((e / 2) / |.p.|) * p as Point of (Euclid n) by EUCLID:67;
consider x being set such that
A200: x in dom G1 and
A201: x in Bx and
A202: G1 . x = p by A186, FUNCT_1:def_6;
( ((e / 2) / |.p.|) * p in halfline ((0. (TOP-REAL n)),p) & Ball ((0. (TOP-REAL n)),e) = Ball (0TRn,e) ) by A6, Lm2, TOPREAL9:13;
then A203: pp in A /\ (halfline ((0. (TOP-REAL n)),p)) by A7, A190, XBOOLE_0:def_4;
dist (0TRn,pp) = |.((0. (TOP-REAL n)) - (((e / 2) / |.p.|) * p)).| by SPPOL_1:39
.= |.(- (((e / 2) / |.p.|) * p)).| by RLVECT_1:14
.= e / 2 by A189, TOPRNS_1:26 ;
then (e / 2) / |.Hp.| <= 1 by A193, A197, A203, XREAL_1:183;
then A204: r * ((e / 2) / |.Hp.|) <= r * 1 by A184, XREAL_1:64;
p = G . (|.Hp.| * p) by A107, A194, A195;
then |.Hp.| * p = x by A106, A198, A200, A202, FUNCT_1:def_4;
then |.p.| < (r * (e / 2)) / |.Hp.| by A196, A199, A201, TOPREAL9:10, XREAL_1:81;
then |.p.| < r by A204, XXREAL_0:2;
then |.(p - (0. (TOP-REAL n))).| < r by RLVECT_1:13;
then p in Ball ((0. (TOP-REAL n)),r) ;
then p in Ball (0TRn,r) by TOPREAL9:13;
hence y in U by A185; ::_thesis: verum
end;
end;
end;
end;
end;
GA .: FrA = G1 .: FrA by A2, A139, A140, RELAT_1:129, TOPS_1:35;
then GA .: FrA = G .: FrA by A5, A8, A32, BOOLMARK:3, ZFMISC_1:50;
then A205: GA .: FrA = Sphere ((0. (TOP-REAL n)),1) by A117, A129, XBOOLE_0:def_10;
( dom GA = [#] ((TOP-REAL n) | A) & rng GA = [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) ) by A143, A173, FUNCT_2:def_1, XBOOLE_0:def_10;
then GA is being_homeomorphism by A2, A3, A138, A174, A176, COMPTS_1:17, PRE_TOPC:27;
hence ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) by A205; ::_thesis: verum
end;
theorem Th5: :: BROUWER2:5
for n being Nat
for p being Point of (TOP-REAL n)
for r being real number st r > 0 holds
Fr (cl_Ball (p,r)) = Sphere (p,r)
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n)
for r being real number st r > 0 holds
Fr (cl_Ball (p,r)) = Sphere (p,r)
let p be Point of (TOP-REAL n); ::_thesis: for r being real number st r > 0 holds
Fr (cl_Ball (p,r)) = Sphere (p,r)
let r be real number ; ::_thesis: ( r > 0 implies Fr (cl_Ball (p,r)) = Sphere (p,r) )
set TR = TOP-REAL n;
assume A1: r > 0 ; ::_thesis: Fr (cl_Ball (p,r)) = Sphere (p,r)
set CB = cl_Ball (p,r);
set B = Ball (p,r);
set S = Sphere (p,r);
reconsider tr = TOP-REAL n as TopSpace ;
reconsider cb = cl_Ball (p,r) as Subset of tr ;
A2: n in NAT by ORDINAL1:def_12;
then A3: Ball (p,r) misses Sphere (p,r) by TOPREAL9:19;
A4: (Ball (p,r)) \/ (Sphere (p,r)) = cl_Ball (p,r) by A2, TOPREAL9:18;
A5: Int cb c= Ball (p,r)
proof
reconsider ONE = 1 as Real ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Int cb or x in Ball (p,r) )
assume x in Int cb ; ::_thesis: x in Ball (p,r)
then consider Q being Subset of (TOP-REAL n) such that
A6: Q is open and
A7: Q c= cl_Ball (p,r) and
A8: x in Q by TOPS_1:22;
reconsider q = x as Point of (TOP-REAL n) by A8;
consider w being real positive number such that
A9: Ball (q,w) c= Q by A6, A8, TOPS_4:2;
assume not x in Ball (p,r) ; ::_thesis: contradiction
then q in Sphere (p,r) by A4, A7, A8, XBOOLE_0:def_3;
then A10: |.(q - p).| = r by A2, TOPREAL9:9;
set w2 = w / 2;
set wr = ((w / 2) / r) * (q - p);
A11: abs ((w / 2) / r) = (w / 2) / r by A1, ABSVALUE:def_1;
A12: ((((w / 2) / r) * (q - p)) + q) - p = (((w / 2) / r) * (q - p)) + (q - p) by RLVECT_1:28
.= (((w / 2) / r) * (q - p)) + (ONE * (q - p)) by RLVECT_1:def_8
.= (((w / 2) / r) + ONE) * (q - p) by RLVECT_1:def_6 ;
|.(((((w / 2) / r) * (q - p)) + q) - q).| = |.((((w / 2) / r) * (q - p)) + (q - q)).| by EUCLID:45
.= |.((((w / 2) / r) * (q - p)) + (0. (TOP-REAL n))).| by RLVECT_1:15
.= |.(((w / 2) / r) * (q - p)).| by RLVECT_1:def_4
.= ((w / 2) / r) * r by A2, A10, A11, TOPRNS_1:7
.= w / 2 by A1, XCMPLX_1:87 ;
then |.(((((w / 2) / r) * (q - p)) + q) - q).| < w by XREAL_1:216;
then (((w / 2) / r) * (q - p)) + q in Ball (q,w) ;
then A13: (((w / 2) / r) * (q - p)) + q in Q by A9;
A14: ((w / 2) / r) + ONE = ((w / 2) / r) + (r / r) by A1, XCMPLX_1:60
.= ((w / 2) + r) / r ;
A15: (w / 2) + r > 0 + r by XREAL_1:6;
abs (((w / 2) + r) / r) = ((w / 2) + r) / r by A1, ABSVALUE:def_1;
then |.(((((w / 2) / r) * (q - p)) + q) - p).| = (((w / 2) + r) / r) * r by A2, A10, A14, A12, TOPRNS_1:7
.= (w / 2) + r by A1, XCMPLX_1:87 ;
hence contradiction by A2, A7, A13, A15, TOPREAL9:8; ::_thesis: verum
end;
Ball (p,r) c= Int cb by A2, TOPREAL9:16, TOPS_1:24;
then Int cb = Ball (p,r) by A5, XBOOLE_0:def_10;
then Fr (cl_Ball (p,r)) = (cl_Ball (p,r)) \ (Ball (p,r)) by TOPS_1:43;
hence Fr (cl_Ball (p,r)) = Sphere (p,r) by A4, A3, XBOOLE_1:88; ::_thesis: verum
end;
registration
let n be Element of NAT ;
let A be bounded Subset of (TOP-REAL n);
let p be Point of (TOP-REAL n);
clusterp + A -> bounded ;
coherence
p + A is bounded
proof
set TR = TOP-REAL n;
set En = Euclid n;
reconsider a = A as bounded Subset of (Euclid n) by JORDAN2C:11;
reconsider pA = p + A as Subset of (Euclid n) by EUCLID:67;
consider r being Real such that
A1: 0 < r and
A2: for x, y being Point of (Euclid n) st x in a & y in a holds
dist (x,y) <= r by TBSP_1:def_7;
A3: pA = { (p + u) where u is Element of (TOP-REAL n) : u in A } by RUSUB_4:def_8;
now__::_thesis:_for_x,_y_being_Point_of_(Euclid_n)_st_x_in_pA_&_y_in_pA_holds_
dist_(x,y)_<=_r
let x, y be Point of (Euclid n); ::_thesis: ( x in pA & y in pA implies dist (x,y) <= r )
assume x in pA ; ::_thesis: ( y in pA implies dist (x,y) <= r )
then consider px being Element of (TOP-REAL n) such that
A4: x = p + px and
A5: px in A by A3;
assume y in pA ; ::_thesis: dist (x,y) <= r
then consider py being Element of (TOP-REAL n) such that
A6: y = p + py and
A7: py in A by A3;
reconsider pX = px, pY = py as Point of (Euclid n) by EUCLID:67;
(p + px) - (p + py) = ((p + px) - p) - py by EUCLID:46
.= px - py by EUCLID:48 ;
then dist (x,y) = |.(px - py).| by A4, A6, SPPOL_1:39
.= dist (pX,pY) by SPPOL_1:39 ;
hence dist (x,y) <= r by A2, A5, A7; ::_thesis: verum
end;
then pA is bounded by A1, TBSP_1:def_7;
hence p + A is bounded by JORDAN2C:11; ::_thesis: verum
end;
end;
begin
theorem Th6: :: BROUWER2:6
for n being Element of NAT
for A being convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds
ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
proof
let n be Element of NAT ; ::_thesis: for A being convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds
ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
set TRn = TOP-REAL n;
let A be convex Subset of (TOP-REAL n); ::_thesis: ( A is compact & not A is boundary implies ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) )
assume A1: ( A is compact & not A is boundary ) ; ::_thesis: ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
Int A <> {} by A1, TOPS_1:48;
then consider p being set such that
A2: p in Int A by XBOOLE_0:def_1;
set TRnA = (TOP-REAL n) | A;
reconsider p = p as Point of (TOP-REAL n) by A2;
A3: Int A c= A by TOPS_1:16;
A4: not A is empty by A2;
percases ( n = 0 or n > 0 ) ;
supposeA5: n = 0 ; ::_thesis: ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
set T = Tdisk ((0. (TOP-REAL n)),1);
A6: {(0. (TOP-REAL n))} = the carrier of (TOP-REAL n) by A5, EUCLID:22, EUCLID:77;
then A7: A = {(0. (TOP-REAL n))} by A4, ZFMISC_1:33;
then reconsider I = id ((TOP-REAL n) | A) as Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) by A6, ZFMISC_1:33;
take I ; ::_thesis: ( I is being_homeomorphism & I .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
A8: Fr A = A \ (Int A) by A5, TOPS_1:43;
A9: Sphere ((0. (TOP-REAL n)),1) = {}
proof
assume Sphere ((0. (TOP-REAL n)),1) <> {} ; ::_thesis: contradiction
then Sphere ((0. (TOP-REAL n)),1) = A by A6, A7, ZFMISC_1:33;
then |.(0. (TOP-REAL n)).| = 1 by A6, A7, TOPREAL9:12;
hence contradiction by TOPRNS_1:23; ::_thesis: verum
end;
Int A = A by A2, A3, A7, ZFMISC_1:33;
then A10: Fr A = {} by A8, XBOOLE_1:37;
Tdisk ((0. (TOP-REAL n)),1) = (TOP-REAL n) | A by A6, A7, ZFMISC_1:33;
hence ( I is being_homeomorphism & I .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) ) by A10, A9; ::_thesis: verum
end;
supposeA11: n > 0 ; ::_thesis: ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
set T = transl ((- p),(TOP-REAL n));
set TA = (transl ((- p),(TOP-REAL n))) .: A;
A12: (transl ((- p),(TOP-REAL n))) .: A = (- p) + A by RLTOPSP1:33;
then A13: ( 0. (TOP-REAL n) = 0* n & (transl ((- p),(TOP-REAL n))) .: A is convex ) by CONVEX1:7, EUCLID:70;
reconsider TT = (transl ((- p),(TOP-REAL n))) | A as Function of ((TOP-REAL n) | A),((TOP-REAL n) | ((transl ((- p),(TOP-REAL n))) .: A)) by JORDAN24:12;
A14: TT .: (Int A) = (transl ((- p),(TOP-REAL n))) .: (Int A) by RELAT_1:129, TOPS_1:16;
0. (TOP-REAL n) = (- p) + p by RLVECT_1:5;
then A15: 0. (TOP-REAL n) in { ((- p) + q) where q is Element of (TOP-REAL n) : q in Int A } by A2;
Int ((transl ((- p),(TOP-REAL n))) .: A) = (- p) + (Int A) by A12, RLTOPSP1:37;
then 0. (TOP-REAL n) in Int ((transl ((- p),(TOP-REAL n))) .: A) by A15, RUSUB_4:def_8;
then consider h being Function of ((TOP-REAL n) | ((transl ((- p),(TOP-REAL n))) .: A)),(Tdisk ((0. (TOP-REAL n)),1)) such that
A16: h is being_homeomorphism and
A17: h .: (Fr ((transl ((- p),(TOP-REAL n))) .: A)) = Sphere ((0. (TOP-REAL n)),1) by A1, A11, A12, A13, Lm4;
reconsider hTT = h * TT as Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) by A4;
take hTT ; ::_thesis: ( hTT is being_homeomorphism & hTT .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
A18: Int ((transl ((- p),(TOP-REAL n))) .: A) = (- p) + (Int A) by A12, RLTOPSP1:37
.= (transl ((- p),(TOP-REAL n))) .: (Int A) by RLTOPSP1:33 ;
A19: TT is being_homeomorphism by JORDAN24:14;
then dom TT = [#] ((TOP-REAL n) | A) by TOPS_2:def_5;
then A20: dom TT = A by PRE_TOPC:def_5;
thus hTT is being_homeomorphism by A4, A16, A19, TOPS_2:57; ::_thesis: hTT .: (Fr A) = Sphere ((0. (TOP-REAL n)),1)
rng TT = [#] ((TOP-REAL n) | ((transl ((- p),(TOP-REAL n))) .: A)) by A19, TOPS_2:def_5;
then A21: rng TT = (transl ((- p),(TOP-REAL n))) .: A by PRE_TOPC:def_5;
Fr A = A \ (Int A) by A1, TOPS_1:43;
then A22: TT .: (Fr A) = (TT .: A) \ (TT .: (Int A)) by A19, FUNCT_1:64;
Fr ((transl ((- p),(TOP-REAL n))) .: A) = ((transl ((- p),(TOP-REAL n))) .: A) \ (Int ((transl ((- p),(TOP-REAL n))) .: A)) by A1, A12, TOPS_1:43
.= TT .: (Fr A) by A18, A22, A20, A21, A14, RELAT_1:113 ;
hence hTT .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) by A17, RELAT_1:126; ::_thesis: verum
end;
end;
end;
theorem Th7: :: BROUWER2:7
for n being Nat
for A, B being convex Subset of (TOP-REAL n) st A is compact & not A is boundary & B is compact & not B is boundary holds
ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st
( h is being_homeomorphism & h .: (Fr A) = Fr B )
proof
let n be Nat; ::_thesis: for A, B being convex Subset of (TOP-REAL n) st A is compact & not A is boundary & B is compact & not B is boundary holds
ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st
( h is being_homeomorphism & h .: (Fr A) = Fr B )
set T = TOP-REAL n;
let A, B be convex Subset of (TOP-REAL n); ::_thesis: ( A is compact & not A is boundary & B is compact & not B is boundary implies ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st
( h is being_homeomorphism & h .: (Fr A) = Fr B ) )
assume that
A1: ( A is compact & not A is boundary ) and
A2: ( B is compact & not B is boundary ) ; ::_thesis: ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st
( h is being_homeomorphism & h .: (Fr A) = Fr B )
A3: ( not A is empty & not B is empty ) by A1, A2;
reconsider N = n as Element of NAT by ORDINAL1:def_12;
set TN = TOP-REAL N;
consider hA being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL N)),1)) such that
A4: hA is being_homeomorphism and
A5: hA .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) by A1, Th6;
consider hB being Function of ((TOP-REAL n) | B),(Tdisk ((0. (TOP-REAL N)),1)) such that
A6: hB is being_homeomorphism and
A7: hB .: (Fr B) = Sphere ((0. (TOP-REAL n)),1) by A2, Th6;
reconsider h = (hB ") * hA as Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) ;
take h ; ::_thesis: ( h is being_homeomorphism & h .: (Fr A) = Fr B )
hB " is being_homeomorphism by A6, TOPS_2:56;
hence h is being_homeomorphism by A3, A4, TOPS_2:57; ::_thesis: h .: (Fr A) = Fr B
A8: rng hB = [#] (Tdisk ((0. (TOP-REAL N)),1)) by A6, TOPS_2:def_5;
dom hB = [#] ((TOP-REAL n) | B) by A6, TOPS_2:def_5;
then A9: dom hB = B by PRE_TOPC:def_5;
the carrier of (Tdisk ((0. (TOP-REAL N)),1)) = cl_Ball ((0. (TOP-REAL N)),1) by BROUWER:3;
then A10: Sphere ((0. (TOP-REAL n)),1) is Subset of (Tdisk ((0. (TOP-REAL N)),1)) by TOPREAL9:17;
thus h .: (Fr A) = (hB ") .: (Sphere ((0. (TOP-REAL n)),1)) by A5, RELAT_1:126
.= hB " (Sphere ((0. (TOP-REAL n)),1)) by A6, A8, A10, TOPS_2:55
.= Fr B by A2, A6, A7, A9, FUNCT_1:94, TOPS_1:35 ; ::_thesis: verum
end;
theorem Th8: :: BROUWER2:8
for n being Nat
for A being convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds
for h being continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) holds h is with_fixpoint
proof
let n be Nat; ::_thesis: for A being convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds
for h being continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) holds h is with_fixpoint
set T = TOP-REAL n;
consider I being affinely-independent Subset of (TOP-REAL n) such that
{} (TOP-REAL n) c= I and
I c= [#] (TOP-REAL n) and
A1: Affin I = Affin ([#] (TOP-REAL n)) by RLAFFIN1:60;
reconsider TT = TOP-REAL n as non empty RLSStruct ;
reconsider i = I as Subset of TT ;
set II = Int i;
A2: not I is empty by A1;
then A3: not Int i is empty by RLAFFIN2:20;
reconsider ii = Int i as Subset of (TOP-REAL n) ;
A4: Int ii c= Int (conv I) by RLAFFIN2:5, TOPS_1:19;
let A be convex Subset of (TOP-REAL n); ::_thesis: ( A is compact & not A is boundary implies for h being continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) holds h is with_fixpoint )
assume A5: ( A is compact & not A is boundary ) ; ::_thesis: for h being continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) holds h is with_fixpoint
A6: not A is empty by A5;
let h be continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A); ::_thesis: h is with_fixpoint
[#] (TOP-REAL n) is Affine by RUSUB_4:22;
then ( dim (TOP-REAL n) = n & Affin ([#] (TOP-REAL n)) = [#] (TOP-REAL n) ) by RLAFFIN1:50, RLAFFIN3:4;
then A7: card I = n + 1 by A1, RLAFFIN3:6;
then ii is open by RLAFFIN3:33;
then not conv I is boundary by A3, A4, TOPS_1:23;
then consider f being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (conv I)) such that
A8: f is being_homeomorphism and
f .: (Fr A) = Fr (conv I) by A5, Th7;
reconsider fhf = f * (h * (f ")) as Function of ((TOP-REAL n) | (conv I)),((TOP-REAL n) | (conv I)) by A6;
f " is continuous by A8, TOPS_2:def_5;
then consider p being Point of (TOP-REAL n) such that
A9: p in dom fhf and
A10: fhf . p = p by A7, A2, A8, A6, SIMPLEX2:23;
A11: p in dom (h * (f ")) by A9, FUNCT_1:11;
reconsider F = f as Function ;
A12: rng f = [#] ((TOP-REAL n) | (conv I)) by A8, TOPS_2:def_5;
A13: f " = F " by A8, TOPS_2:def_4;
consider x being set such that
A14: x in dom F and
A15: F . x = p by A12, A9, FUNCT_1:def_3;
(F ") . p = x by A8, A14, A15, FUNCT_1:34;
then (h * (f ")) . p = h . x by A11, A13, FUNCT_1:12;
then A16: p = f . (h . x) by A9, A10, FUNCT_1:12;
A17: dom f = [#] ((TOP-REAL n) | A) by A8, TOPS_2:def_5;
then A18: x in dom h by A14, FUNCT_2:52;
then h . x in rng h by FUNCT_1:def_3;
then h . x = x by A8, A17, A14, A15, A16, FUNCT_1:def_4;
then x is_a_fixpoint_of h by A18, ABIAN:def_3;
hence h is with_fixpoint by ABIAN:def_5; ::_thesis: verum
end;
Lm5: for n being Nat holds not cl_Ball ((0. (TOP-REAL n)),1) is boundary
proof
let n be Nat; ::_thesis: not cl_Ball ((0. (TOP-REAL n)),1) is boundary
set TR = TOP-REAL n;
reconsider tr = TOP-REAL n as TopStruct ;
reconsider cB = cl_Ball ((0. (TOP-REAL n)),1) as Subset of tr ;
n in NAT by ORDINAL1:def_12;
then Ball ((0. (TOP-REAL n)),1) c= Int cB by TOPREAL9:16, TOPS_1:24;
hence not cl_Ball ((0. (TOP-REAL n)),1) is boundary ; ::_thesis: verum
end;
Lm6: for n being Element of NAT
for X being non empty SubSpace of Tdisk ((0. (TOP-REAL n)),1) st X = Tcircle ((0. (TOP-REAL n)),1) holds
not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1)
proof
let n be Element of NAT ; ::_thesis: for X being non empty SubSpace of Tdisk ((0. (TOP-REAL n)),1) st X = Tcircle ((0. (TOP-REAL n)),1) holds
not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1)
set TR = TOP-REAL n;
set Td = Tdisk ((0. (TOP-REAL n)),1);
A1: Sphere ((0. (TOP-REAL n)),1) c= cl_Ball ((0. (TOP-REAL n)),1) by TOPREAL9:17;
set M = mlt ((- 1),(TOP-REAL n));
let X be non empty SubSpace of Tdisk ((0. (TOP-REAL n)),1); ::_thesis: ( X = Tcircle ((0. (TOP-REAL n)),1) implies not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1) )
assume A2: X = Tcircle ((0. (TOP-REAL n)),1) ; ::_thesis: not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1)
A3: the carrier of X = Sphere ((0. (TOP-REAL n)),1) by A2, TOPREALB:9;
assume X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1) ; ::_thesis: contradiction
then consider F being continuous Function of (Tdisk ((0. (TOP-REAL n)),1)),X such that
A4: F is being_a_retraction by BORSUK_1:def_17;
A5: the carrier of (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1) by BROUWER:3;
then reconsider f = F as Function of (Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL n)),1)) by A3, A1, FUNCT_2:7;
set Mf = ((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f;
A6: (mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1)) = (mlt ((- 1),(TOP-REAL n))) | the carrier of (Tdisk ((0. (TOP-REAL n)),1)) by TMAP_1:def_4;
A7: rng (((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) c= Sphere ((0. (TOP-REAL n)),1)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) or y in Sphere ((0. (TOP-REAL n)),1) )
assume y in rng (((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) ; ::_thesis: y in Sphere ((0. (TOP-REAL n)),1)
then consider x being set such that
A8: x in dom (((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) and
A9: (((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) . x = y by FUNCT_1:def_3;
A10: f . x in dom ((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) by A8, FUNCT_1:11;
then f . x in dom (mlt ((- 1),(TOP-REAL n))) by A6, RELAT_1:57;
then reconsider fx = f . x as Point of (TOP-REAL n) ;
x in dom f by A8, FUNCT_1:11;
then f . x in rng F by FUNCT_1:def_3;
then A11: 1 = |.fx.| by A3, TOPREAL9:12
.= |.(- fx).| by EUCLID:10
.= |.((- fx) - (0. (TOP-REAL n))).| by RLVECT_1:13 ;
y = ((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) . (f . x) by A8, A9, FUNCT_1:12;
then y = (mlt ((- 1),(TOP-REAL n))) . (f . x) by A6, A10, FUNCT_1:47;
then y = (- 1) * fx by RLTOPSP1:def_13
.= - fx by RLVECT_1:16 ;
hence y in Sphere ((0. (TOP-REAL n)),1) by A11; ::_thesis: verum
end;
then rng (((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) c= cl_Ball ((0. (TOP-REAL n)),1) by A1, XBOOLE_1:1;
then reconsider MF = ((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f as Function of (Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL n)),1)) by A5, FUNCT_2:6;
A12: not cl_Ball ((0. (TOP-REAL n)),1) is boundary by Lm5;
f is continuous by PRE_TOPC:26;
then MF is continuous by PRE_TOPC:27;
then MF is with_fixpoint by A12, Th8;
then consider p being set such that
A13: p is_a_fixpoint_of MF by ABIAN:def_5;
A14: p in dom MF by A13, ABIAN:def_3;
A15: p = MF . p by A13, ABIAN:def_3;
then A16: p in rng MF by A14, FUNCT_1:def_3;
then reconsider p = p as Point of (TOP-REAL n) by A7;
A17: f . p = p by A4, A3, A7, A16, BORSUK_1:def_16;
then A18: p in dom ((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) by A14, FUNCT_1:11;
p = ((mlt ((- 1),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) . p by A14, A15, A17, FUNCT_1:12;
then p = (mlt ((- 1),(TOP-REAL n))) . p by A6, A18, FUNCT_1:47;
then p = (- 1) * p by RLTOPSP1:def_13
.= - p by RLVECT_1:16 ;
then A19: p = 0. (TOP-REAL n) by RLVECT_1:19;
|.p.| = 1 by A7, A16, TOPREAL9:12;
hence contradiction by A19, TOPRNS_1:23; ::_thesis: verum
end;
theorem :: BROUWER2:9
for n being Nat
for A being non empty convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds
for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds
not FR is_a_retract_of (TOP-REAL n) | A
proof
let n be Nat; ::_thesis: for A being non empty convex Subset of (TOP-REAL n) st A is compact & not A is boundary holds
for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds
not FR is_a_retract_of (TOP-REAL n) | A
set T = TOP-REAL n;
A1: n in NAT by ORDINAL1:def_12;
set cB = cl_Ball ((0. (TOP-REAL n)),1);
set S = Sphere ((0. (TOP-REAL n)),1);
A2: [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def_5;
then reconsider s = Sphere ((0. (TOP-REAL n)),1) as Subset of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by A1, TOPREAL9:17;
A3: (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1)) = ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) | s by A1, PRE_TOPC:7, TOPREAL9:17;
let A be non empty convex Subset of (TOP-REAL n); ::_thesis: ( A is compact & not A is boundary implies for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds
not FR is_a_retract_of (TOP-REAL n) | A )
assume A4: ( A is compact & not A is boundary ) ; ::_thesis: for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds
not FR is_a_retract_of (TOP-REAL n) | A
A5: ( [#] ((TOP-REAL n) | A) = A & Fr A c= A ) by A4, PRE_TOPC:def_5, TOPS_1:35;
let FR be non empty SubSpace of (TOP-REAL n) | A; ::_thesis: ( [#] FR = Fr A implies not FR is_a_retract_of (TOP-REAL n) | A )
assume A6: [#] FR = Fr A ; ::_thesis: not FR is_a_retract_of (TOP-REAL n) | A
n > 0
proof
assume n <= 0 ; ::_thesis: contradiction
then n = 0 ;
then {(0. (TOP-REAL n))} = the carrier of (TOP-REAL n) by EUCLID:22, EUCLID:77;
then A7: A = [#] (TOP-REAL n) by ZFMISC_1:33;
then Fr A = (Cl A) \ A by TOPS_1:42;
hence contradiction by A6, A7, XBOOLE_1:37; ::_thesis: verum
end;
then reconsider Ts = ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) | s as non empty SubSpace of (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)) ;
assume FR is_a_retract_of (TOP-REAL n) | A ; ::_thesis: contradiction
then consider F being continuous Function of ((TOP-REAL n) | A),FR such that
A8: F is being_a_retraction by BORSUK_1:def_17;
reconsider f = F as Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) by A6, A5, FUNCT_2:7;
A9: f is continuous by PRE_TOPC:26;
A10: rng F c= Fr A by A6;
reconsider N = n as Element of NAT by ORDINAL1:def_12;
set TN = TOP-REAL N;
A11: [#] ((TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1))) = Sphere ((0. (TOP-REAL n)),1) by PRE_TOPC:def_5;
( (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)) = Tdisk ((0. (TOP-REAL N)),1) & (TOP-REAL n) | (Sphere ((0. (TOP-REAL n)),1)) = Tcircle ((0. (TOP-REAL N)),1) ) by TOPREALB:def_6;
then A12: not Ts is_a_retract_of (TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)) by A3, Lm6;
not cl_Ball ((0. (TOP-REAL n)),1) is boundary by Lm5;
then consider h being Function of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))),((TOP-REAL n) | A) such that
A13: h is being_homeomorphism and
A14: h .: (Fr (cl_Ball ((0. (TOP-REAL n)),1))) = Fr A by A1, A4, Th7;
A15: dom h = [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by A13, TOPS_2:def_5;
rng ((h ") * f) = ((h ") * f) .: (dom ((h ") * f)) by RELAT_1:113;
then A16: rng ((h ") * f) c= ((h ") * f) .: (dom f) by RELAT_1:25, RELAT_1:123;
reconsider H = h as Function ;
A17: Fr (cl_Ball ((0. (TOP-REAL n)),1)) = Sphere ((0. (TOP-REAL n)),1) by Th5;
rng h = [#] ((TOP-REAL n) | A) by A13, TOPS_2:def_5;
then A18: (h ") .: (Fr A) = h " (Fr A) by A13, A5, TOPS_2:55
.= Fr (cl_Ball ((0. (TOP-REAL n)),1)) by A13, A14, A2, A15, FUNCT_1:94, TOPS_1:35 ;
((h ") * f) .: (dom f) = (h ") .: (f .: (dom f)) by RELAT_1:126
.= (h ") .: (rng f) by RELAT_1:113 ;
then ((h ") * f) .: (dom f) c= Fr (cl_Ball ((0. (TOP-REAL n)),1)) by A18, A10, RELAT_1:123;
then ( rng (((h ") * f) * h) c= rng ((h ") * f) & rng ((h ") * f) c= Fr (cl_Ball ((0. (TOP-REAL n)),1)) ) by A16, RELAT_1:26, XBOOLE_1:1;
then rng (((h ") * f) * h) c= Fr (cl_Ball ((0. (TOP-REAL n)),1)) by XBOOLE_1:1;
then reconsider hfh = ((h ") * f) * h as Function of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))),Ts by A3, A17, A11, FUNCT_2:6;
h " is continuous by A13, TOPS_2:def_5;
then hfh is continuous by A13, A9, PRE_TOPC:27;
then not hfh is being_a_retraction by A12, BORSUK_1:def_17;
then consider x being Point of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) such that
A19: x in Sphere ((0. (TOP-REAL n)),1) and
A20: hfh . x <> x by A3, A11, BORSUK_1:def_16;
set hx = h . x;
A21: dom hfh = the carrier of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by FUNCT_2:def_1;
then A22: hfh . x = ((h ") * f) . (h . x) by FUNCT_1:12;
x in dom h by A21, FUNCT_1:11;
then A23: h . x in the carrier of FR by A6, A14, A17, A19, FUNCT_1:def_6;
h . x in dom ((h ") * f) by A21, FUNCT_1:11;
then A24: ((h ") * f) . (h . x) = (h ") . (f . (h . x)) by FUNCT_1:12;
A25: H " = h " by A13, TOPS_2:def_4;
(H ") . (h . x) = x by A13, A15, FUNCT_1:34;
hence contradiction by A8, A25, A20, A22, A24, A23, BORSUK_1:def_16; ::_thesis: verum
end;