:: Tietze Extension Theorem for $n$-dimensional Spaces
:: by Karol P\kak
::
:: Received February 11, 2014
:: Copyright (c) 2014-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 ARYTM_1, ARYTM_3, CARD_1, COMPLEX1, CONVEX1, EUCLID, FUNCOP_1,
FUNCT_1, FUNCT_4, MEMBERED, METRIC_1, NAT_1, NUMBERS, ORDINAL2, PCOMPS_1,
PRE_TOPC, RCOMP_1, REAL_1, RELAT_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI,
TOPMETR, TOPS_1, TOPS_2, XBOOLE_0, XREAL_0, XXREAL_0, XXREAL_2, FUNCT_2,
EUCLID_9, TOPREALC, FINSEQ_1, XXREAL_1, FINSEQ_2, CARD_3, PARTFUN3,
SQUARE_1, FUNCT_6, XCMPLX_0, PARTFUN1, FINSET_1, ZFMISC_1, VALUED_0,
SETFAM_1, T_0TOPSP, BROUWER, ORDINAL4, TIETZE_2, FUNCT_3;
notations TARSKI, XBOOLE_0, FINSET_1, SETFAM_1, VALUED_0, SUBSET_1, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, COMPLEX1, ORDINAL1, NUMBERS,
XXREAL_0, XREAL_0, RVSUM_1, XCMPLX_0, MEMBERED, FUNCOP_1, FINSEQ_1,
FINSEQ_2, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, PCOMPS_1, TOPMETR,
FUNCT_7, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL9, PARTFUN3, TOPS_2,
COMPTS_1, TBSP_1, XXREAL_2, EUCLID_9, CARD_3, SQUARE_1, FUNCT_6,
TOPREALC, METRIZTS, ZFMISC_1, RCOMP_1, BORSUK_1, T_0TOPSP, BINOP_1,
FUNCT_3, NAT_1, BORSUK_2, BROUWER, TMAP_1;
constructors COMPLEX1, TBSP_1, MONOID_0, CONVEX1, TOPREAL9, TOPS_1, COMPTS_1,
FUNCSDOM, PARTFUN3, TOPREALC, SEQ_4, EUCLID_9, SQUARE_1, FUNCT_6,
METRIZTS, BORSUK_3, BORSUK_2, BROUWER, TMAP_1;
registrations BORSUK_1, EUCLID, EUCLID_9, FUNCOP_1, FINSEQ_1, FUNCT_1,
FUNCT_2, MEMBERED, NAT_1, PCOMPS_1, PRE_TOPC, RELAT_1, PARTFUN3, RVSUM_1,
SIMPLEX2, STRUCT_0, SUBSET_1, TOPGRP_1, TOPMETR, TOPS_1, VALUED_0,
VALUED_2, XBOOLE_0, XREAL_0, XXREAL_0, RELSET_1, FINSET_1, TBSP_1,
MONOID_0, JORDAN2B, FINSEQ_2, XXREAL_2, COMPTS_1, CARD_1, TOPREAL1,
RLAFFIN3, XCMPLX_0, TOPREAL9, FUNCT_3, FUNCT_6, NUMBERS, TMAP_1,
TOPREALC;
requirements ARITHM, BOOLE, NUMERALS, SUBSET, REAL;
definitions TARSKI, XBOOLE_0, CONVEX1;
equalities BINOP_1, STRUCT_0, FINSEQ_2, XCMPLX_0, TOPREAL9, ORDINAL1;
expansions TARSKI, FUNCT_1, XBOOLE_0, PRE_TOPC;
theorems ABSVALUE, BORSUK_1, BROUWER, EUCLID, FUNCOP_1, FUNCT_1, FUNCT_2,
GOBOARD6, JORDAN2C, MEMBERED, ORDINAL1, PRE_TOPC, RELAT_1, SUBSET_1,
TARSKI, TBSP_1, TOPMETR, TOPREAL9, TOPREALC, TOPS_1, TOPS_2, XBOOLE_0,
XBOOLE_1, XREAL_1, XXREAL_0, XXREAL_2, ZFMISC_1, EUCLID_9, FINSEQ_2,
TIETZE, CARD_1, CARD_3, FINSEQ_1, PARTFUN3, XXREAL_1, FINSEQ_3, VALUED_1,
PARTFUN1, FUNCT_7, TOPREAL7, JORDAN6, SETFAM_1, BROUWER2, FUNCT_6,
METRIZTS, T_0TOPSP, FUNCTOR0, FUNCT_3, TOPGRP_1, BORSUK_2, SIMPLEX2,
JORDAN24, BORSUK_3, NAT_1, JORDAN, TMAP_1;
schemes FINSEQ_1;
begin :: Closed Hypercube
reserve n,m,i for Nat,
p,q for Point of TOP-REAL n,
r,s for Real,
R for real-valued FinSequence;
registration
cluster empty -> nonnegative-yielding for FinSequence;
coherence
proof
let F be FinSequence;
assume F is empty;
then for r st r in rng F holds r >=0;
hence thesis by PARTFUN3:def 4;
end;
end;
definition
let n be non zero Nat;
let X be set;
let F be Element of n-tuples_on Funcs(X,the carrier of R^1);
redefine func <:F:> -> Function of X,TOP-REAL n; :: redefines <: (FUNCT_6, definition)
coherence
proof
set Y = the carrier of R^1,TR=the carrier of TOP-REAL n;
A1: now
let x be object;
assume
A2: x in dom F;
then F.x in rng F by FUNCT_1:def 3;
then ex Fx be Function st Fx=F.x & dom Fx=X & rng Fx c= Y
by FUNCT_2:def 2;
hence (doms F).x = X by A2,FUNCT_6:22;
end;
A3: rng <:F:> c= product rngs F by FUNCT_6:29;
len F= n by CARD_1:def 7;
then
A4: dom F=Seg n by FINSEQ_1:def 3;
A5: dom rngs F = dom F by FUNCT_6:60;
A6: product rngs F c= TR
proof
let y be object;
assume y in product rngs F;
then consider g be Function such that
A7: y = g
and
A8: dom g = dom F
and
A9: for z be object st z in dom F holds g.z in (rngs F).z
by CARD_3:def 5,A5;
reconsider g as FinSequence by A4,A8,FINSEQ_1:def 2;
rng g c= REAL
proof
let z be object;
assume z in rng g;
then consider x be object such that
A10: x in dom g
and
A11: z=g.x by FUNCT_1:def 3;
A12: (rngs F).x = rng (F.x) by A8,A10,FUNCT_6:def 3;
g.x in (rngs F).x by A8,A9,A10;
hence thesis by A12,A11;
end;
then reconsider g as FinSequence of REAL by FINSEQ_1:def 4;
n in NAT by ORDINAL1:def 12;
then len g = n by A8,A4,FINSEQ_1:def 3;
hence thesis by A7,TOPREAL7:17;
end;
dom doms F = dom F by FUNCT_6:59;
then doms F = dom F --> X by A1,FUNCOP_1:11;
then dom <:F:> = meet (dom F --> X) by FUNCT_6:29;
then dom <:F:> = X by FUNCT_6:27;
hence thesis by A6,A3,XBOOLE_1:1,FUNCT_2:2;
end;
end;
theorem Th20:
for X,Y be set for F be Function-yielding Function
for x,y be object st F is Funcs(X,Y)-valued or y in dom <:F:>
holds F.x.y = <:F:>.y.x
proof
let X,Y be set;
let F be Function-yielding Function;
set FF=dom F;
A1: dom doms F= dom F by FUNCT_6:59;
let x,y be object such that
A2:F is Funcs(X,Y)-valued or y in dom <:F:>;
per cases by A2;
suppose y in dom <:F:> & x in dom F;
hence F.x.y = <:F:>.y.x by FUNCT_6:34;
end;
suppose
A3: y in dom <:F:> & not x in dom F;
then dom (<:F:>.y) = FF by FUNCT_6:31;
then
A4: <:F:>.y.x = {} by A3,FUNCT_1:def 2;
F.x={} by A3,FUNCT_1:def 2;
hence thesis by A4;
end;
suppose
A5: not y in dom <:F:> & x in dom F & F is Funcs(X,Y)-valued;
then
A6: <:F:>.y ={} by FUNCT_1:def 2;
A7: rng F c= Funcs(X,Y) by RELAT_1:def 19,A5;
F.x in rng F by A5,FUNCT_1:def 3;
then consider Fx be Function such that
A8: Fx=F.x
and
A9: dom Fx=X
and
rng Fx c= Y by A7,FUNCT_2:def 2;
now
let x be object;
assume
A10: x in dom F;
then F.x in rng F by FUNCT_1:def 3;
then ex Fx be Function st Fx=F.x & dom Fx=X & rng Fx c= Y
by A7,FUNCT_2:def 2;
hence (doms F).x = X by A10,FUNCT_6:22;
end;
then doms F = dom F --> X by A1,FUNCOP_1:11;
then dom <:F:> = meet (dom F --> X) by FUNCT_6:29;
then dom <:F:> = X by A5,FUNCT_6:27;
then Fx.y={} by A9,A5,FUNCT_1:def 2;
hence thesis by A6,A8;
end;
suppose
A11: not y in dom <:F:> & not x in dom F;
then
A12: F.x ={} by FUNCT_1:def 2;
A13: {} .x={};
<:F:>.y ={} by A11,FUNCT_1:def 2;
hence thesis by A12,A13;
end;
end;
definition
let n,p,r;
func OpenHypercube(p,r) -> open Subset of TOP-REAL n means :Def1:
ex e be Point of Euclid n st p=e & it = OpenHypercube(e,r);
existence
proof
reconsider e=p as Point of Euclid n by EUCLID:67;
A1: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider O=OpenHypercube(e,r) as Subset of TOP-REAL n;
OpenHypercube(e,r) in the topology of TOP-REAL n by PRE_TOPC: def 2,A1;
then O is open;
hence thesis;
end;
uniqueness;
end;
theorem Th1:
q in OpenHypercube(p,r) & s in ].p.i - r, p.i + r.[
implies q+*(i,s) in OpenHypercube(p,r)
proof
assume that
A1: q in OpenHypercube(p,r)
and
A2: s in ].p.i - r, p.i + r.[;
consider e be Point of Euclid n such that
A3: p=e
and
A4: OpenHypercube(p,r) = OpenHypercube(e,r) by Def1;
set OH=OpenHypercube(e,r),I=Intervals(e,r), qs = q+*(i,s);
A5: OH = product I by EUCLID_9:def 4;
then
A6: dom q = dom I by A4,A1,CARD_3:9;
A7: dom I = dom e by EUCLID_9:def 3;
A8: for x be object st x in dom I holds qs.x in I.x
proof
let x be object;
assume
A9: x in dom I;
then
A10: I.x = ].e.x-r,e.x+r.[ by A7,EUCLID_9:def 3;
A11: q.x in I.x by A9,A1,A5,A4,CARD_3:9;
i=x or i<>x;
hence thesis by A6,A9,A3,FUNCT_7:31,32,A2,A10,A11;
end;
dom qs=dom q by FUNCT_7:30;
hence thesis by A4,A8,CARD_3:9,A6,A5;
end;
theorem Th2:
i in Seg n implies PROJ(n,i).:OpenHypercube(p,r) = ]. p.i - r, p.i + r .[
proof
assume
A1: i in Seg n;
consider e be Point of Euclid n such that
A2: p=e
and
A3: OpenHypercube(p,r) = OpenHypercube(e,r) by Def1;
set OH=OpenHypercube(e,r),I=Intervals(e,r);
A4:OH = product I by EUCLID_9:def 4;
len e = n by CARD_1:def 7;
then
A5:dom e = Seg n by FINSEQ_1:def 3;
then
A6:I.i = ]. e.i-r,e.i+r.[ by A1,EUCLID_9:def 3;
hereby
let y be object;
assume y in PROJ(n,i).:OpenHypercube(p,r);
then consider x be object such that
A7: x in dom PROJ(n,i)
and
A8: x in OH
and
A9: PROJ(n,i).x = y by A3,FUNCT_1:def 6;
reconsider x as Point of TOP-REAL n by A7;
A10:dom I = dom x by A8,A4,CARD_3:9;
then
A11:dom x = Seg n by EUCLID_9:def 3,A5;
then
A12: x/.i=x.i by A1,PARTFUN1:def 6;
x.i in I.i by A11,A10,CARD_3:9,A8,A4,A1;
hence y in ]. p.i - r, p.i + r .[ by A2,TOPREALC:def 6,A12,A6, A9;
end;
let y be object;
assume
A13:y in ]. p.i - r, p.i + r .[;
then reconsider s=y as Real;
A14: s < e.i+r by A2,A13, XXREAL_1:4;
set ps = p+*(i,s);
e.i -r < s by A2,A13, XXREAL_1:4;
then e.i +- r < e.i +r by A14,XXREAL_0:2;
then r>0 by XREAL_1:6;
then
A15: ps in OH by A2,A3,EUCLID_9:11,Th1,A13;
len ps= n by CARD_1:def 7;
then
A16: dom ps = Seg n by FINSEQ_1:def 3;
len p = n by CARD_1:def 7;
then
A17: dom p = Seg n by FINSEQ_1:def 3;
A18: dom PROJ(n,i)=the carrier of TOP-REAL n by FUNCT_2:def 1;
PROJ(n,i).ps = ps/.i by TOPREALC:def 6
.= ps.i by A16,A1,PARTFUN1:def 6
.= s by A17,A1,FUNCT_7:31;
hence thesis by A3, A18,A15, FUNCT_1:def 6;
end;
theorem Th3:
q in OpenHypercube(p,r)
iff
for i st i in Seg n holds q.i in ]. p.i - r,p.i +r .[
proof
A1: len q = n by CARD_1:def 7;
thus q in OpenHypercube(p,r) implies for i st i in Seg n holds
q.i in ]. p.i-r,p.i+r .[
proof
assume
A2: q in OpenHypercube(p,r);
let i such that
A3: i in Seg n;
set P=PROJ(n,i);
dom P = the carrier of TOP-REAL n by FUNCT_2:def 1;
then
A4: P.q in P.:OpenHypercube(p,r) by A2,FUNCT_1:def 6;
A5: P.q = q/.i by TOPREALC:def 6;
len q = n by CARD_1:def 7;
then dom q = Seg n by FINSEQ_1:def 3;
then q/.i = q.i by A3,PARTFUN1:def 6;
hence thesis by A5,Th2,A3,A4;
end;
assume
A6: for i st i in Seg n holds q.i in ]. p.i - r,p.i+r .[;
consider e be Point of Euclid n such that
A7: p=e
and
A8: OpenHypercube(p,r) = OpenHypercube(e,r) by Def1;
set I= Intervals(e,r);
A9: dom I = dom e by EUCLID_9:def 3;
len p = n by CARD_1:def 7;
then
A10: dom p = dom q by A1, FINSEQ_3:29;
A11: dom q = Seg n by A1,FINSEQ_1:def 3;
A12: now
let x be object;
assume
A13: x in dom q;
then reconsider i= x as Nat;
q.i in ]. p.i - r,p.i+r .[ by A6,A13,A11;
hence q.x in I.x by EUCLID_9:def 3,A7,A13,A10;
end;
product I = OpenHypercube(p,r) by A8,EUCLID_9:def 4;
hence thesis by A12,A7,A10,A9,CARD_3:9;
end;
definition
let n,p,R;
func ClosedHypercube(p,R) -> Subset of TOP-REAL n means :Def2:
q in it iff for i st i in Seg n holds q.i in [. p.i - R.i,p.i+R.i .];
existence
proof
set TR=TOP-REAL n;
set H = {q: for i st i in Seg n holds q.i in [. p.i - R.i,p.i+R.i .]};
H c= the carrier of TR
proof
let x be object;
assume x in H;
then ex q st q=x& for i st i in Seg n holds
q.i in [. p.i - R.i,p.i+R.i.];
hence thesis;
end;
then reconsider H as Subset of TR;
take H;
let q;
hereby
assume
q in H;
then ex Q be Point of TR st q=Q & for i st i in Seg n holds
Q.i in [.p.i-R.i,p.i+R.i .];
hence for i st i in Seg n holds q.i in [. p.i - R.i,p.i+R.i .];
end;
thus thesis;
end;
uniqueness
proof
set TR=TOP-REAL n;
let H1,H2 be Subset of TOP-REAL n such that
A1: q in H1 iff for i st i in Seg n holds q.i in [. p.i - R.i,p.i+R.i.]
and
A2: q in H2 iff for i st i in Seg n holds q.i in [. p.i - R.i,p.i+R.i.];
hereby
let x be object;
assume
A3: x in H1;
then reconsider q=x as Point of TR;
for i st i in Seg n holds q.i in [. p.i - R.i,p.i+R.i .] by A1,A3;
hence x in H2 by A2;
end;
let x be object;
assume
A4: x in H2;
then reconsider q=x as Point of TR;
for i st i in Seg n holds q.i in [. p.i - R.i,p.i+R.i .] by A2, A4;
hence x in H1 by A1;
end;
end;
theorem Th4:
(ex i st i in Seg n /\ dom R & R.i < 0) implies ClosedHypercube(p,R) is empty
proof
given i such that
A1: i in Seg n /\ dom R
and
A2: R.i < 0;
assume ClosedHypercube(p,R) is non empty;
then consider x be object such that
A3: x in ClosedHypercube(p,R);
reconsider x as Point of TOP-REAL n by A3;
i in Seg n by A1,XBOOLE_0:def 4;
then
A4: x.i in [. p.i - R.i,p.i+R.i .] by Def2,A3;
then
A5: x.i <= p.i+R.i by XXREAL_1:1;
p.i - R.i <= x.i by A4,XXREAL_1:1;
then p.i +- R.i <= p.i +R.i by A5,XXREAL_0:2;
hence contradiction by A2,XREAL_1:8;
end;
theorem Th5:
(for i st i in Seg n /\ dom R holds R.i >= 0)
implies p in ClosedHypercube(p,R)
proof
assume
A1: for i st i in Seg n /\ dom R holds R.i >= 0;
now
let i;
assume
A2: i in Seg n;
A3: now
per cases;
suppose i in dom R;
then i in Seg n /\ dom R by A2,XBOOLE_0:def 4;
hence R.i >= 0 by A1;
end;
suppose not i in dom R;
hence R.i >=0 by FUNCT_1:def 2;
end;
end;
then
A4: p.i +R.i >= p.i by XREAL_1:40;
p.i - R.i <= p.i by A3,XREAL_1:43;
hence p.i in [. p.i - R.i,p.i+R.i .] by A4,XXREAL_1:1;
end;
hence thesis by Def2;
end;
registration
let n,p;
let R be nonnegative-yielding real-valued FinSequence;
cluster ClosedHypercube(p,R) -> non empty;
coherence
proof
now let i;
assume i in Seg n /\ dom R;
then i in dom R by XBOOLE_0:def 4;
then R.i in rng R by FUNCT_1:def 3;
hence R.i >= 0 by PARTFUN3:def 4;
end;
hence thesis by Th5;
end;
end;
registration
let n,p,R;
cluster ClosedHypercube(p,R) -> convex compact;
coherence
proof
set E=Euclid n,TE=TopSpaceMetr E,TR=TOP-REAL n;
A1: the carrier of TR = the carrier of E by EUCLID:67;
A2: the TopStruct of TOP-REAL n =TE by EUCLID:def 8;
then reconsider H=ClosedHypercube(p,R) as Subset of the TopStruct of TE;
A3: H`=[#]TE\H by SUBSET_1:def 4;
for e being Point of E st e in H`
ex r st r > 0 & OpenHypercube(e,r) c= H`
proof
let e be Point of E;
reconsider ee = e as Point of TR by EUCLID:67;
assume e in H`;
then not e in H by A3,XBOOLE_0:def 5;
then consider i such that
A4: i in Seg n
and
A5: not e.i in [. p.i - R.i,p.i+R.i .] by A1,Def2;
per cases by A5,XXREAL_1:1;
suppose
A6: e.i < p.i - R.i;
take r=p.i - R.i-e.i;
e.i-e.i < r by A6,XREAL_1:9;
hence r >0;
set I=Intervals(e,r);
let x be object;
assume
A7: x in OpenHypercube(e,r);
then
A8: x in product I by EUCLID_9:def 4;
assume not x in H`;
then not x in [#]TE\H by SUBSET_1:def 4;
then
A9: x in H by A7,XBOOLE_0:def 5;
reconsider x as Point of E by TOPMETR:12,A7;
reconsider xx = x as Point of TR by EUCLID:67;
len ee = n by CARD_1:def 7;
then
A10: dom e = Seg n by FINSEQ_1:def 3;
dom e=dom I by EUCLID_9:def 3;
then x.i in I.i by A10,A4,A8,CARD_3:9;
then x.i in ].e.i-r,e.i+r.[ by A10,A4,EUCLID_9:def 3;
then
A11: x.i < p.i - R.i by XXREAL_1:4;
xx.i in [. p.i - R.i,p.i+R.i .] by A4,A9,Def2;
hence contradiction by A11,XXREAL_1:1;
end;
suppose
A12: e.i > p.i + R.i;
take r=e.i-(p.i + R.i);
e.i-e.i < r by A12,XREAL_1:10;
hence r>0;
set I=Intervals(e,r);
let x be object;
assume
A13: x in OpenHypercube(e,r);
then
A14: x in product I by EUCLID_9:def 4;
assume not x in H`;
then not x in [#]TE\H by SUBSET_1:def 4;
then
A15: x in H by A13,XBOOLE_0:def 5;
reconsider x as Point of E by TOPMETR:12,A13;
reconsider xx = x as Point of TR by EUCLID:67;
len ee = n by CARD_1:def 7;
then
A16: dom e = Seg n by FINSEQ_1:def 3;
dom e=dom I by EUCLID_9:def 3;
then x.i in I.i by A16,A4,A14,CARD_3:9;
then x.i in ].e.i-r,e.i+r.[ by A16,A4,EUCLID_9:def 3;
then
A17: x.i > (p.i + R.i) by XXREAL_1:4;
xx.i in [. p.i - R.i,p.i+R.i .] by A4,A15,Def2;
hence contradiction by A17,XXREAL_1:1;
end;
end;
then H` is open by EUCLID_9:24;
then ClosedHypercube(p,R)` is open by A2;
then
A18: ClosedHypercube(p,R) is closed by TOPS_1:3;
reconsider h=H as Subset of E by EUCLID:67;
reconsider P=p as Point of E by EUCLID:67;
ClosedHypercube(p,R) is convex
proof
let u,w be Point of TR;
let r be Real;
assume that
A19: 0 < r
and
A20: r < 1
and
A21: u in ClosedHypercube(p,R)
and
A22: w in ClosedHypercube(p,R);
set ru=r*u,rw=(1-r)*w;
A23: 1-r > 1-1 by A20,XREAL_1:10;
now
let i;
A24: len rw = n by CARD_1:def 7;
assume
A25: i in Seg n;
then
A26: u.i in [. p.i - R.i,p.i+R.i .] by A21,Def2;
then u.i >= p.i-R.i by XXREAL_1:1;
then
A27: r*(u.i) >=r*(p.i-R.i) by A19,XREAL_1:64;
len ru =n by CARD_1:def 7;
then dom ru=dom rw by A24, FINSEQ_3:29;
then i in dom ru /\dom rw by A24,FINSEQ_1:def 3,A25;
then i in dom (ru+rw) by VALUED_1:def 1;
then
A28: (ru+rw).i = ru.i + rw.i by VALUED_1:def 1;
u.i <= p.i+R.i by A26,XXREAL_1:1;
then
A29: r*(u.i) <=r*(p.i+R.i) by A19,XREAL_1:64;
A30: ru.i = r*(u.i) by VALUED_1:6;
A31: rw.i=(1-r)*w.i by VALUED_1:6;
A32: w.i in [. p.i - R.i,p.i+R.i .] by A25,A22,Def2;
then w.i <= p.i+R.i by XXREAL_1:1;
then (1-r)*(w.i) <= (1-r)*(p.i+R.i) by A23,XREAL_1:64;
then
A33: (ru+rw).i <= r*(p.i+R.i)+(1-r)*(p.i+R.i)
by A29,A30,A31,A28,XREAL_1:7;
w.i >= p.i-R.i by A32,XXREAL_1:1;
then (1-r)*(w.i) >= (1-r)*(p.i-R.i) by A23,XREAL_1:64;
then (ru+rw).i >= r*(p.i-R.i)+(1-r)*(p.i-R.i)
by A27,A30,A31,A28,XREAL_1:7;
hence (ru+rw).i in [. p.i - R.i,p.i+R.i .] by A33,XXREAL_1:1;
end;
hence thesis by Def2;
end;
hence ClosedHypercube(p,R) is convex;
per cases;
suppose
A34: R.:(Seg n) is empty;
H c= {p}
proof
let x be object;
A35: len p=n by CARD_1:def 7;
assume
A36: x in H;
then reconsider x as Point of TR;
A37: now
let i;
assume that
A38: 1<=i
and
A39: i <= n;
A40: i in Seg n by A38,A39,FINSEQ_1:1;
not R.i in R.:(Seg n) by A34;
then not i in dom R by A40,FUNCT_1:def 6;
then
A41: R.i = 0 by FUNCT_1:def 2;
x.i in [. p.i - R.i,p.i+R.i .] by A40,A36,Def2;
then x.i in {p.i} by A41,XXREAL_1:17;
hence x.i=p.i by TARSKI:def 1;
end;
len x = n by CARD_1:def 7;
then x=p by A35,A37,FINSEQ_1:14;
hence thesis by TARSKI:def 1;
end;
then h is bounded;
then ClosedHypercube(p,R) is bounded by JORDAN2C:11;
hence thesis by A18;
end;
suppose
A42: R.:(Seg n) is non empty;
then reconsider RS=R.:(Seg n) as right_end real-membered set;
set m=max RS+1;
set O=OpenHypercube(P,m);
set I=Intervals(P,m);
A43: H c= O
proof
let x be object;
A44: dom I = dom P by EUCLID_9:def 3;
assume
A45: x in H;
then reconsider x as Point of TR;
A46: len x = n by CARD_1:def 7;
len p = n by CARD_1:def 7;
then
A47: dom x=dom p by A46,FINSEQ_3:29;
A48: dom x = Seg n by A46,FINSEQ_1:def 3;
for z be object st z in dom I holds x.z in I.z
proof
let z be object;
assume
A49: z in dom I;
then
A50: x.z in [. P.z - R.z,p.z+R.z .] by A45,A47,A48,A44,Def2;
then
A51: P.z - R.z <= x.z by XXREAL_1:1;
A52: now
per cases;
suppose z in dom R;
then R.z in RS by A49,A47,A48,A44,FUNCT_1:def 6;
then R.z <= max RS by XXREAL_2:def 8;
then R.z+0 < m by XREAL_1:8;
hence R.z < m;
end;
suppose
A53: not z in dom R;
(Seg n) meets dom R by A42,RELAT_1:118;
then consider i be object such that
A54: i in Seg n
and
A55: i in dom R by XBOOLE_0:3;
reconsider i as Nat by A54;
i in Seg n /\dom R by A54,A55,XBOOLE_0:def 4;
then
A56: R.i >=0 by Th4,A45;
R.i in RS by A54,A55,FUNCT_1:def 6;
then R.i <= max RS by XXREAL_2:def 8;
then 0 +0 < m by A56;
hence R.z < m by A53,FUNCT_1:def 2;
end;
end;
then P.z-m < P.z - R.z by XREAL_1:10;
then
A57: P.z-m < x.z by A51,XXREAL_0:2;
A58: x.z <= p.z+R.z by A50,XXREAL_1:1;
P.z+m > P.z + R.z by A52, XREAL_1:8;
then
A59: x.z < P.z+m by A58,XXREAL_0:2;
I.z = ].P.z-m,P.z+m.[ by A49,A44,EUCLID_9:def 3;
hence x.z in I.z by A57,A59,XXREAL_1:4;
end;
then x in product I by A47,A44,CARD_3:9;
hence thesis by EUCLID_9:def 4;
end;
n<>0 by A42;
then O c= Ball(P,m*sqrt(n)) by EUCLID_9:18;
then h is bounded by A43,XBOOLE_1:1,TBSP_1:14;
then ClosedHypercube(p,R) is bounded by JORDAN2C:11;
hence thesis by A18;
end;
end;
end;
theorem Th6:
i in Seg n & q in ClosedHypercube(p,R) & r in [.p.i - R.i, p.i + R.i.]
implies q+*(i,r) in ClosedHypercube(p,R)
proof
set H=ClosedHypercube(p,R),pr=q+*(i,r);
assume that
A1: i in Seg n
and
A2: q in H
and
A3: r in [.p.i - R.i, p.i + R.i.];
for j be Nat st j in Seg n holds pr.j in [. p.j - R.j,p.j+R.j .]
proof
let j be Nat;
assume
A4: j in Seg n;
A5: dom q = Seg len q by FINSEQ_1:def 3;
A6: len q = n by CARD_1:def 7;
per cases;
suppose i <> j;
then pr.j = q.j by FUNCT_7:32;
hence thesis by Def2,A4,A2;
end;
suppose i =j;
hence thesis by FUNCT_7:31,A1,A5,A6,A3;
end;
end;
hence thesis by Def2;
end;
theorem Th7:
i in Seg n & ClosedHypercube(p,R) is non empty implies
PROJ(n,i).:ClosedHypercube(p,R) = [. p.i - R.i, p.i + R.i .]
proof
set P=PROJ(n,i),H=ClosedHypercube(p,R),TR=TOP-REAL n;
assume that
A1: i in Seg n
and
A2: H is non empty;
hereby
let y be object;
assume y in P.:H;
then consider x be object such that
A3: x in dom P
and
A4: x in H
and
A5: P.x =y by FUNCT_1:def 6;
reconsider x as Point of TR by A3;
len x = n by CARD_1:def 7;
then dom x = Seg n by FINSEQ_1:def 3;
then
A6: x/.i = x.i by A1,PARTFUN1:def 6;
P.x = x/.i by TOPREALC:def 6;
hence y in [. p.i - R.i, p.i + R.i .] by A6,A1,A4,A5, Def2;
end;
let y be object;
assume
A7:y in [. p.i - R.i, p.i + R.i .];
then reconsider r=y as Real;
set pr=p+*(i,r);
A8: dom P=the carrier of TR by FUNCT_2:def 1;
A9: dom pr = Seg len pr by FINSEQ_1:def 3;
len pr = n by CARD_1:def 7;
then
A10: pr/.i = pr.i by A9,A1,PARTFUN1:def 6;
A11: dom p = Seg len p by FINSEQ_1:def 3;
for i st i in Seg n /\ dom R holds R.i >= 0 by A2,Th4;
then pr in H by A1,Th6, A7,Th5;
then
A12:P.pr in P.:H by A8,FUNCT_1:def 6;
A13: len p = n by CARD_1:def 7;
P.pr = pr/.i by TOPREALC:def 6;
hence thesis by A13,A11,A10,A1, FUNCT_7:31,A12;
end;
theorem Th8:
n <= len R & r <= inf (rng R) implies
OpenHypercube(p,r) c= ClosedHypercube(p,R)
proof
set H=ClosedHypercube(p,R);
assume that
A1: n <= len R
and
A2: r <= inf rng R;
A3: Seg n c= Seg len R by A1,FINSEQ_1:5;
set E=Euclid n,TE=TopSpaceMetr E,TR=TOP-REAL n;
let x be object;
A4: Seg len R=dom R by FINSEQ_1:def 3;
assume
A5:x in OpenHypercube(p,r);
then reconsider q=x as Point of TR;
consider e be Point of Euclid n such that
A6: p=e
and
A7: OpenHypercube(p,r) = OpenHypercube(e,r) by Def1;
set I=Intervals(e,r);
A8:x in product I by A5,A7,EUCLID_9:def 4;
now
let i;
A9: dom I = dom e by EUCLID_9:def 3;
assume
A10:i in Seg n;
then R.i in rng R by A3,A4,FUNCT_1:def 3;
then inf (rng R) <= R.i by XXREAL_2:3;
then
A11: r <= R.i by A2,XXREAL_0:2;
then
A12: e.i +r <= e.i +R.i by XREAL_1:6;
A13: dom p = Seg len p by FINSEQ_1:def 3;
A14: e.i -r >= e.i - R.i by A11,XREAL_1:10;
A15: len p = n by CARD_1:def 7;
then I.i = ].e.i-r,e.i+r.[ by A13, A6,A10,EUCLID_9:def 3;
then
A16:q.i in ].e.i-r,e.i+r.[ by A9,CARD_3:9, A6,A10, A15,A13, A8;
then e.i -r < q.i by XXREAL_1:4;
then
A17: p.i - R.i < q.i by A14, A6,XXREAL_0:2;
q.i < e.i +r by A16,XXREAL_1:4;
then q.i < p.i + R.i by A12, A6,XXREAL_0:2;
hence q.i in [.p.i-R.i,p.i+R.i.] by A17,XXREAL_1:1;
end;
hence thesis by Def2;
end;
theorem Th9:
q in Fr ClosedHypercube(p,R)
iff
q in ClosedHypercube(p,R) & ex i st i in Seg n &
(q.i = p.i - R.i or q.i = p.i + R. i)
proof
set TR=TOP-REAL n;
A1:Fr ClosedHypercube(p,R) c= ClosedHypercube(p,R) by TOPS_1:35;
thus q in Fr ClosedHypercube(p,R) implies
q in ClosedHypercube(p,R) & ex i st i in Seg n &
( q.i = p .i - R.i or q.i = p.i + R .i)
proof
deffunc l1(set) = q.$1 - (p.$1 - R.$1);
deffunc r1(set) = (p.$1 + R.$1) - q.$1;
consider L1 be FinSequence such that
A2: len L1 = n & for i st i in dom L1 holds L1.i=l1(i)
from FINSEQ_1:sch 2;
now
let y be object;
assume y in rng L1;
then consider x be object such that
A3: x in dom L1
and
A4: L1.x = y by FUNCT_1:def 3;
reconsider x as Nat by A3;
L1.x= l1(x) by A2,A3;
hence y is real by A4;
end;
then
A5: rng L1 is real-membered by MEMBERED:def 3;
consider R1 be FinSequence such that
A6: len R1 = n & for i st i in dom R1 holds R1.i=r1(i)
from FINSEQ_1:sch 2;
now
let y be object;
assume y in rng R1;
then consider x be object such that
A7: x in dom R1
and
A8: R1.x = y by FUNCT_1:def 3;
reconsider x as Nat by A7;
R1.x= r1(x) by A7,A6;
hence y is real by A8;
end;
then
A9: rng R1 is real-membered by MEMBERED:def 3;
A10: dom L1=Seg n by A2,FINSEQ_1:def 3;
assume
A11: q in Fr ClosedHypercube(p,R);
hence q in ClosedHypercube(p,R) by A1;
assume
A12: for i st i in Seg n holds q.i <> p.i - R.i & q.i <> p.i + R.i;
n>0
proof
assume n <= 0;
then n=0;
then
A13: {0.TR} = the carrier of TR by EUCLID:22,JORDAN2C:105;
[#]TR is open;
hence thesis by A13, A11, ZFMISC_1:33;
end;
then n in Seg n by FINSEQ_1:3;
then L1.n in rng L1 by A10,FUNCT_1:def 3;
then reconsider D=(rng L1)\/(rng R1) as
non empty finite real-membered set by A9,A5;
set m=min D;
consider e be Point of Euclid n such that
A14: q=e
and
A15: OpenHypercube(q,m) = OpenHypercube(e,m) by Def1;
A16: dom R1= Seg n by A6,FINSEQ_1:def 3;
A17: m in D by XXREAL_2:def 7;
A18: m >0
proof
per cases by A17,XBOOLE_0:def 3;
suppose min D in rng L1;
then consider x be object such that
A19: x in dom L1
and
A20: L1.x=m by FUNCT_1:def 3;
reconsider x as Nat by A19;
q.x in [. p.x - R.x,p.x+R.x .] by A11,A1,A19,A10,Def2;
then q.x >= p.x - R.x by XXREAL_1:1;
then
A21: q.x > p.x - R.x by A19,A10,A12,XXREAL_0:1;
L1.x=l1(x) by A2,A19;
hence thesis by A21,XREAL_1:50,A20;
end;
suppose min D in rng R1;
then consider x be object such that
A22: x in dom R1
and
A23: R1.x=m by FUNCT_1:def 3;
reconsider x as Nat by A22;
q.x in [. p.x - R.x,p.x+R.x .] by A11,A1,A22,A16,Def2;
then q.x <= p.x + R.x by XXREAL_1:1;
then
A24: q.x < p.x + R.x by A22,A16,A12,XXREAL_0:1;
R1.x=r1(x) by A6,A22;
hence thesis by A24,XREAL_1:50,A23;
end;
end;
set O=OpenHypercube(e,m);
O c= ClosedHypercube(p,R)
proof
let x be object;
assume
A25: x in O;
then reconsider w=x as Point of Euclid n by TOPMETR:12;
reconsider W=w as Point of TR by EUCLID:67;
for i st i in Seg n holds W.i in [. p.i - R.i,p.i+R.i .]
proof
let i;
set P=PROJ(n,i);
len W= n by CARD_1:def 7;
then
A26: dom W = Seg n by FINSEQ_1:def 3;
dom P = the carrier of TR by FUNCT_2:def 1;
then
A27: P.W in P.:O by A25,FUNCT_1:def 6;
assume
A28: i in Seg n;
then L1.i in rng L1 by A10,FUNCT_1:def 3;
then
A29: L1.i in D by XBOOLE_0:def 3;
L1.i = l1(i) by A10,A2, A28;
then m <= l1(i) by A29,XXREAL_2:def 7;
then
A30: q.i-m >= q.i- l1(i) by XREAL_1:10;
P.W = W/.i by TOPREALC:def 6
.= W.i by A28,A26,PARTFUN1:def 6;
then
A31: W.i in ]. e.i - m, e.i + m .[ by A14,A15,A28,Th2,A27;
then W.i > q.i-m by A14,XXREAL_1:4;
then
A32: W.i > p.i - R.i by A30,XXREAL_0:2;
R1.i in rng R1 by A28,A16,FUNCT_1:def 3;
then
A33: R1.i in D by XBOOLE_0:def 3;
R1.i = r1(i) by A16, A6, A28;
then m <= r1(i) by A33,XXREAL_2:def 7;
then
A34: q.i+m <= q.i+ r1(i) by XREAL_1:6;
W.i < q.i + m by A31,A14,XXREAL_1:4;
then W.i < p.i + R.i by A34,XXREAL_0:2;
hence thesis by A32,XXREAL_1:1;
end;
hence thesis by Def2;
end;
then q in Int ClosedHypercube(p,R) by A18,A14,A15,EUCLID_9:11,TOPS_1:22;
hence contradiction by TOPS_1:39,A11,XBOOLE_0:3;
end;
assume
A35: q in ClosedHypercube(p,R);
given i such that
A36:i in Seg n
and
A37: q.i = p.i - R.i or q.i = p.i + R.i;
for S be Subset of TR st S is open & q in S holds ClosedHypercube(p,R)
meets S & ClosedHypercube(p,R)` meets S
proof
let S be Subset of TR;
reconsider Q=q as Point of Euclid n by EUCLID:67;
assume that
A38: S is open
and
A39: q in S;
thus ClosedHypercube(p,R) meets S by A39,A35,XBOOLE_0:3;
Int S = S by A38,TOPS_1:23;
then consider s be Real such that
A40: s>0
and
A41: Ball(Q,s) c= S by A39,GOBOARD6:5;
set s2=s/2;
A42: 0< s2 & s2<s by XREAL_1:216,A40;
A43: Ball(Q,s)=Ball(q,s) by TOPREAL9:13;
per cases by A37;
suppose
A44: q.i = p.i - R.i;
set q1=q+*(i,q.i-s2);
reconsider q1 as Point of TR;
len q = n by CARD_1:def 7;
then dom q = Seg n by FINSEQ_1:def 3;
then q1.i = q.i-s2 by A36,FUNCT_7:31;
then q1.i < q.i+0 by A40,XREAL_1:6;
then not q1.i in [. p.i - R.i,p.i+R.i .] by A44,XXREAL_1:1;
then not q1 in ClosedHypercube(p,R) by A36,Def2;
then q1 in [#]TR\ClosedHypercube(p,R) by XBOOLE_0:def 5;
then
A45: q1 in ClosedHypercube(p,R)` by SUBSET_1:def 4;
q1-q = (0*n) +*(i,(q.i)-s2-(q.i)) by TOPREALC:17;
then |. q1-q.| = |. (q.i)-s2-(q.i) .| by A36, TOPREALC:13
.= --s2 by A40,ABSVALUE:def 1
.= s2;
then q1 in Ball(q,s) by A42;
hence ClosedHypercube(p,R)` meets S by A43,A41,XBOOLE_0:3,A45;
end;
suppose
A46: q.i = p.i + R.i;
set q1=q+*(i,q.i+s2);
reconsider q1 as Point of TR;
len q = n by CARD_1:def 7;
then dom q = Seg n by FINSEQ_1:def 3;
then q1.i = q.i+s2 by A36,FUNCT_7:31;
then q1.i > q.i+0 by A40,XREAL_1:6;
then not q1.i in [. p.i - R.i,p.i+R.i .] by A46,XXREAL_1:1;
then not q1 in ClosedHypercube(p,R) by A36,Def2;
then q1 in [#]TR\ClosedHypercube(p,R) by XBOOLE_0:def 5;
then
A47: q1 in ClosedHypercube(p,R)` by SUBSET_1:def 4;
q1-q = (0*n) +*(i,(q.i)+s2-(q.i)) by TOPREALC:17;
then |. q1-q.| = |. (q.i)+s2-(q.i) .| by A36, TOPREALC:13
.= s2 by A40,ABSVALUE:def 1;
then q1 in Ball(q,s) by A42;
hence ClosedHypercube(p,R)` meets S by A43,A41,XBOOLE_0:3,A47;
end;
end;
hence thesis by TOPS_1:28;
end;
theorem
r >= 0 implies p in ClosedHypercube(p,n|->r)
proof
set R=n |-> r;
assume r>=0;
then for i st i in Seg n /\dom R holds R.i >=0 by FINSEQ_2:57;
hence thesis by Th5;
end;
theorem Th11:
r>0 implies Int ClosedHypercube(p,n|->r) = OpenHypercube(p,r)
proof
assume r>0;
set O=OpenHypercube(p,r);
set C=ClosedHypercube(p,n |-> r);
set TR=TOP-REAL n, R=n |-> r;
A1: Int C c= C by TOPS_1:16;
consider e be Point of Euclid n such that
A2: p=e
and
A3: OpenHypercube(p,r) = OpenHypercube(e,r) by Def1;
set I=Intervals(e,r);
A4:O = product I by A3,EUCLID_9:def 4;
thus Int C c= O
proof
let x be object;
A5: len p =n by CARD_1:def 7;
then
A6: dom p = Seg n by FINSEQ_1:def 3;
assume
A7: x in Int C;
then reconsider q=x as Point of TR;
A8: dom p = dom I by A2,EUCLID_9:def 3;
A9: not q in Fr C by TOPS_1:39,A7,XBOOLE_0:3;
A10:for z be object st z in dom I holds q.z in I.z
proof
let z be object;
assume
A11: z in dom I;
then
A12: I.z = ].e.z-r,e.z+r.[ by A2,A8,EUCLID_9:def 3;
reconsider z as Nat by A11;
A13: R.z = r by FINSEQ_2:57,A8,A6,A11;
A14: q.z in [.p.z - R.z,p.z+R.z.] by A1,A7,A8,A6,A11,Def2;
then p.z - r <= q.z by A13,XXREAL_1:1;
then
A15: p.z - r < q.z by A13, A9, A1,A7,Th9,A8,A6,A11,XXREAL_0:1;
q.z <= p.z + r by A14,A13,XXREAL_1:1;
then q.z < p.z + r
by A13,A9,A1,A7,Th9,A8,A6,A11,XXREAL_0:1;
hence thesis by A15,A2,A12,XXREAL_1:4;
end;
len q = n by CARD_1:def 7;
then dom q=dom p by A5,FINSEQ_3 :29;
hence thesis by A10,CARD_3:9,A8,A4;
end;
let x be object;
assume
A16:x in O;
then reconsider q =x as Point of TR;
len q = n by CARD_1:def 7;
then
A17:dom q = Seg n by FINSEQ_1:def 3;
for i st i in Seg n holds q.i in [. p.i - R.i,p.i+R.i .]
proof
let i;
A18: dom PROJ(n,i) = [#]TR by FUNCT_2:def 1;
assume
A19: i in Seg n;
then
A20: R.i = r by FINSEQ_2:57;
PROJ(n,i).:O = ]. e.i - r, e.i + r .[ by A19,A2,Th2;
then
A21: PROJ(n,i).q in ]. e.i - r, e.i + r .[ by A18,A16,FUNCT_1:def 6;
A22: PROJ(n,i).q = q/.i by TOPREALC:def 6;
A23: q/.i = q.i by A19, A17,PARTFUN1:def 6;
then
A24: q.i <= p.i + R.i by A20,A22,A21,A2,XXREAL_1:4;
q.i >= p.i - R.i by A20,A23,A22,A21,A2,XXREAL_1:4;
hence thesis by A24,XXREAL_1:1;
end;
then
A25:q in C by Def2;
assume not x in Int C;
then q in C\Int C by A25,XBOOLE_0:def 5;
then q in Fr C by TOPS_1:43;
then consider i such that
A26: i in Seg n
and
A27: q.i = p.i - R.i or q.i = p.i + R.i by Th9;
A28: dom PROJ(n,i) = [#]TR by FUNCT_2:def 1;
PROJ(n,i).:O = ]. e.i - r, e.i + r .[ by A2,A26,Th2;
then
A29: PROJ(n,i).q in ]. e.i - r, e.i + r .[ by A28,A16,FUNCT_1:def 6;
A30: R.i = r by A26,FINSEQ_2:57;
PROJ(n,i).q = q/.i by TOPREALC:def 6;
then q.i in ]. e.i - r, e.i + r .[ by A17,A26,PARTFUN1:def 6,A29;
hence contradiction by A2,A30,XXREAL_1:4,A27;
reconsider oo= O as Subset of TR;
end;
theorem Th12:
OpenHypercube(p,r) c= ClosedHypercube(p,n|->r)
proof
set TR= TOP-REAL n;
per cases;
suppose
A1: n=0;
then for i st i in Seg n holds
(0.TR).i in [. p.i - (n|->r).i,p.i+(n|->r).i.];
then
A2: 0.TR in ClosedHypercube(p,n|->r) by Def2;
the carrier of TR = {0.TR} by JORDAN2C:105, A1,EUCLID:22;
then ClosedHypercube(p,n|->r)=[#]TR by A2,ZFMISC_1:33;
hence thesis;
end;
suppose n>0;
then rng (n|->r) = {r} by FUNCOP_1:8;
then
A3: inf rng (n|->r) = r by XXREAL_2:13;
len (n|->r) = n by CARD_1:def 7;
hence thesis by Th8,A3;
end;
end;
theorem
r < s implies ClosedHypercube(p,n|->r) c= OpenHypercube(p,s)
proof
assume
A1: r<s;
let x be object such that
A2: x in ClosedHypercube(p,n|->r);
reconsider q= x as Point of TOP-REAL n by A2;
now
let i such that
A3: i in Seg n;
(n|->r).i = r by A3,FINSEQ_2:57;
then
A4: q.i in [. p.i - r,p.i+r .] by A2,A3,Def2;
A5: p.i + r < p.i + s by A1,XREAL_1:6;
q.i <= p.i+r by A4,XXREAL_1:1;
then
A6: q.i < p.i+s by A5,XXREAL_0:2;
A7: p.i - r > p.i - s by A1,XREAL_1:10;
q.i >=p.i - r by A4,XXREAL_1:1;
then q.i > p.i - s by A7,XXREAL_0:2;
hence q.i in ]. p.i - s,p.i+s .[ by A6,XXREAL_1:4;
end;
hence thesis by Th3;
end;
registration
let n,p;
let r be positive Real;
cluster ClosedHypercube(p,n|->r) -> non boundary;
coherence
proof
A1: ex e be Point of Euclid n st
p=e & OpenHypercube(p,r) = OpenHypercube(e,r) by Def1;
OpenHypercube(p,r) c= Int ClosedHypercube(p,n |-> r)
by Th12,TOPS_1:24;
hence thesis by A1;
end;
end;
begin :: Properties of the Product of Closed Hypercube
reserve T1,T2,S1,S2 for non empty TopSpace,
t1 for Point of T1, t2 for Point of T2,
pn,qn for Point of TOP-REAL n,
pm,qm for Point of TOP-REAL m;
theorem Th14:
for f be Function of T1,T2 for g be Function of S1,S2 st
f is being_homeomorphism & g is being_homeomorphism holds
[:f,g:] is being_homeomorphism
proof
let f be Function of T1,T2;
let g be Function of S1,S2 such that
A1: f is being_homeomorphism
and
A2: g is being_homeomorphism;
A3: rng g=[#]S2 by A2,TOPS_2:def 5;
A4: g" is continuous by A2,TOPS_2:def 5;
A5: f" is continuous by A1,TOPS_2:def 5;
A6:the carrier of [:T2,S2:] = [:the carrier of T2,the carrier of S2:]
by BORSUK_1:def 2;
set fg=[:f,g:];
A7: rng f = [#]T2 by A1,TOPS_2:def 5;
then
A8:rng fg = [#][:T2,S2:] by A3, FUNCT_3:67,A6;
reconsider F=f,G=g,FG=fg as Function;
A9:FG" = [:F",G":] by A1, A2,FUNCTOR0:6;
A10:F"=f" by A1,TOPS_2:def 4;
A11:rng fg = [:rng f, rng g:] by FUNCT_3:67;
then fg is onto by A6,A7,A3,FUNCT_2:def 3;
then
A12:FG" = fg" by A1, A2,TOPS_2:def 4;
A13: now
let P be Subset of [:T2,S2:];
thus P is open implies fg"P is open by BORSUK_2:10, A1, A2;
thus fg"P is open implies P is open
proof
assume
A14: fg"P is open;
[:f",g":]"(fg"P) = (fg")"(fg"P) by A10, A2,TOPS_2:def 4,A9,A12
.= fg.:(fg"P) by TOPS_2:54,A1, A2,A8
.=P by FUNCT_1:77,A7,A3,A11,A6;
hence thesis by BORSUK_2:10,A5,A4,A14;
end;
end;
A15: dom g=[#]S1 by A2,TOPS_2:def 5;
A16:the carrier of [:T1,S1:] = [:the carrier of T1,the carrier of S1:]
by BORSUK_1:def 2;
dom f = [#]T1 by A1,TOPS_2:def 5;
then dom fg = [#][:T1,S1:] by A15, FUNCT_3:def 8,A16;
hence thesis by A13,TOPGRP_1:26,A1, A2,A8;
end;
theorem Th15:
for r,s st r>0 & s>0
ex h be Function of
[: (TOP-REAL n)|ClosedHypercube(pn,n|->r),
(TOP-REAL m)|ClosedHypercube(pm,m|->s):],
(TOP-REAL (n+m))|ClosedHypercube(0.TOP-REAL (n+m),(n+m)|->1) st
h is being_homeomorphism &
h.:[: OpenHypercube(pn,r),OpenHypercube(pm,s):]
= OpenHypercube(0.TOP-REAL (n+m),1)
proof
let r,s such that
A1: r>0
and
A2: s>0;
set TRn=TOP-REAL n,TRm=TOP-REAL m,nm=n+m,TRnm=TOP-REAL nm;
set RN = ClosedHypercube(0.TRn,n|->1),RR = ClosedHypercube(pn,n|->r),
RS = ClosedHypercube(pm,m|->s),
RM = ClosedHypercube(0.TRm, m|->1),RNM = ClosedHypercube(0.TRnm,nm|->1);
reconsider Rs=RS,Rm=RM as non empty Subset of TRm by A2;
consider hm be Function of TRm|Rs,TRm|Rm such that
A3: hm is being_homeomorphism
and
A4: hm.:Fr Rs = Fr Rm by A2, BROUWER2:7;
A5: dom hm = [#](TRm|Rs) by A3,TOPS_2: def 5;
0.TRm = 0*m by EUCLID:70;
then
A6: 0.TRm = m|->0 by EUCLID:def 4;
0.TRn = 0*n by EUCLID:70;
then
A7: 0.TRn = n|->0 by EUCLID:def 4;
reconsider Rr=RR,Rn=RN as non empty Subset of TRn by A1;
consider hn be Function of TRn|Rr,TRn|Rn such that
A8: hn is being_homeomorphism
and
A9: hn.:Fr Rr = Fr Rn by A1, BROUWER2:7;
A10: dom hn = [#](TRn|Rr) by A8,TOPS_2: def 5;
set Or = OpenHypercube(pn,r),Os=OpenHypercube(pm,s),
OO=OpenHypercube(0.TRnm,1);
A11: [#](TRnm | RNM) = RNM by PRE_TOPC:def 5;
A12: Int Rs = Os by A2,Th11;
then
A13: hm.:Os misses hm.: Fr Rs by TOPS_1:39,FUNCT_1:66, A3;
A14: [#](TRm|Rm) = Rm by PRE_TOPC:def 5;
0.TRnm = 0*nm by EUCLID:70;
then
A15: 0.TRnm = nm|->0 by EUCLID:def 4;
set ON = OpenHypercube(0.TRn,1),Om=OpenHypercube(0.TRm,1);
reconsider Rnm=RNM as non empty Subset of TRnm;
A16: n in NAT by ORDINAL1:def 12;
m in NAT by ORDINAL1:def 12;
then consider f be Function of [:TRn,TRm:],TRnm such that
A17: f is being_homeomorphism
and
A18: for fi be Element of TRn,fj be Element of TRm holds
f.(fi,fj) = fi^fj by A16,SIMPLEX2:19;
A19: [#](TRm|Rs) = Rs by PRE_TOPC:def 5;
A20: the carrier of [:TRn,TRm:] = [:the carrier of TRn,the carrier of TRm:]
by BORSUK_1:def 2;
A21: f.: [:Rn,Rm:] c= Rnm
proof
let y be object;
assume
A22: y in f.: [:Rn,Rm:];
then consider x be object such that
A23: x in dom f
and
A24: x in [:Rn,Rm:]
and
A25: f.x = y by FUNCT_1:def 6;
consider p,q be object such that
A26: p in the carrier of TRn
and
A27: q in the carrier of TRm
and
A28: x=[p,q] by A20,A23, ZFMISC_1:def 2;
reconsider q as Point of TRm by A27;
A29: q in Rm by A24,A28,ZFMISC_1:87;
reconsider p as Point of TRn by A26;
A30: f.x = f.(p,q) by A28
.= p^q by A18;
then reconsider pq=p^q as Point of TRnm by A25,A22;
A31: p in Rn by A24,A28,ZFMISC_1:87;
for i st i in Seg nm holds pq.i in
[. (0.TRnm).i - (nm|->1).i,(0.TRnm).i+(nm|->1).i .]
proof
len q = m by CARD_1:def 7;
then
A32: dom q=Seg m by FINSEQ_1:def 3;
len p = n by CARD_1:def 7;
then
A33: dom p = Seg n by FINSEQ_1:def 3;
len pq= nm by CARD_1:def 7;
then
A34: dom pq=Seg nm by FINSEQ_1:def 3;
let i such that
A35: i in Seg nm;
A36: (nm|->1).i =1 by A35,FINSEQ_2:57;
A37: (0.TRnm).i =0 by A15;
per cases by A34,A35,FINSEQ_1:25;
suppose
A38: i in dom p;
then
A39: pq.i=p.i by FINSEQ_1:def 7;
A40: (0.TRn).i =0 by A7;
(n|->1).i =1 by A38,A33,FINSEQ_2:57;
hence thesis by A40,A39, A38,Def2,A33, A31,A37,A36;
end;
suppose
ex k be Nat st k in dom q & i=len p+k;
then consider k be Nat such that
A41: k in dom q
and
A42: i=len p+k;
A43: (m|->1).k =1 by A41,A32,FINSEQ_2:57;
A44: (0.TRm).k =0 by A6;
pq.i=q.k by FINSEQ_1:def 7,A41, A42;
hence thesis by A44,A43, Def2,A32, A29,A41,A37,A36;
end;
end;
hence thesis by Def2,A30,A25;
end;
A45:dom f = [#][:TRn,TRm:] by A17,TOPS_2:def 5;
Rnm c= f.: [:Rn,Rm:]
proof
let x be object;
assume
A46: x in Rnm;
then reconsider pq=x as Point of TRnm;
rng pq c= REAL;
then reconsider pq as FinSequence of REAL by FINSEQ_1:def 4;
len pq= nm by CARD_1:def 7;
then consider p,q be FinSequence of REAL such that
A47: len p = n
and
A48: len q = m
and
A49: pq = p^q by FINSEQ_2:23;
reconsider p as Point of TRn by TOPREAL7:17,A47;
reconsider q as Point of TRm by TOPREAL7:17,A48;
A50: f.([p,q]) = f.(p,q)
.= p^q by A18;
A51: dom p = Seg n by A47,FINSEQ_1:def 3;
now
let i such that
A52: i in Seg n;
A53: (0.TRnm).i = 0 by A15;
A54: Seg n c= Seg nm by NAT_1:11,FINSEQ_1:5;
then (nm|->1).i = 1 by A52,FINSEQ_2:57;
then
A55: pq.i in [. 0-1,0+1 .] by A53, A54,A52,A46,Def2;
A56: (0.TRn).i = 0 by A7;
(n|->1).i = 1 by A52,FINSEQ_2:57;
hence p.i in [. (0.TRn).i - (n|->1).i,(0.TRn).i+(n|->1).i .] by A49,
FINSEQ_1:def 7,A51,A52,A56,A55;
end;
then
A57: p in Rn by Def2;
A58: dom q= Seg m by A48,FINSEQ_1:def 3;
now
let i such that
A59: i in Seg m;
A60: (m|->1).i = 1 by A59,FINSEQ_2:57;
A61: (nm|->1).(i+n) = 1 by A59,FINSEQ_1:60,FINSEQ_2:57;
A62: (0.TRm).i = 0 by A6;
A63: (0.TRnm).(i+n) = 0 by A15;
i+n in Seg nm by A59,FINSEQ_1:60;
then pq.(i+n) in [. 0-1,0+1 .] by A61,A63,A46,Def2;
hence q.i in [. (0.TRm).i - (m|->1).i,(0.TRm).i+(m|->1).i .]
by A47,A49,FINSEQ_1:def 7,A58,A59, A60,A62;
end;
then q in Rm by Def2;
then [p,q] in [:Rn,Rm:] by A57,ZFMISC_1:87;
hence thesis by A50,A49, A45,FUNCT_1:def 6;
end;
then
A64: Rnm = f.: [:Rn,Rm:] by A21;
A65: [#](TRn|Rr) = Rr by PRE_TOPC:def 5;
then
A66: the carrier of [:TRn|Rr,TRm|Rs:] = [:Rr,Rs:] by BORSUK_1:def 2,A19;
set hnm=[:hn,hm:];
A67: hnm is being_homeomorphism by A8,A3,Th14;
then
A68:dom hnm = [#][:TRn|Rr,TRm|Rs:] by TOPS_2:def 5;
A69: Int Rn = ON by Th11;
then
A70: ON c= Rn by TOPS_1:16;
A71: [:TRn,TRm:] | [:Rn,Rm:] = [:TRn|Rn,TRm|Rm:] by BORSUK_3:22;
then
reconsider f1=f| [:Rn,Rm:] as Function of [:TRn|Rn,TRm|Rm:], TRnm | Rnm by
A64, JORDAN24:12;
reconsider h=f1* hnm as Function of [:TRn|RR,TRm|RS:],TRnm | RNM;
take h;
A72: f1 is being_homeomorphism by A17,A71,METRIZTS:2,A64;
hence h is being_homeomorphism by A67, TOPS_2:57;
A73: [#](TRn|Rn) = Rn by PRE_TOPC:def 5;
dom f1 = [#] [:TRn|Rn,TRm|Rm:] by A72,TOPS_2:def 5;
then
A74: dom f1 = [:Rn,Rm:] by BORSUK_1:def 2,A73, A14;
A75: Int Rm = Om by Th11;
then
A76: Om c= Rm by TOPS_1:16;
A77: Int Rr = Or by A1,Th11;
then
A78: hn.:Or misses hn.: Fr Rr by TOPS_1:39,FUNCT_1:66, A8;
thus h.: [:Or,Os:] c= OO
proof
let y be object;
assume
A79: y in h.:[:Or,Os:];
then consider x be object such that
A80: x in dom h
and
A81: x in [:Or,Os:]
and
A82: h.x=y by FUNCT_1:def 6;
consider p,q be object such that
A83: p in Rr
and
A84: q in Rs
and
A85: [p,q] =x by A80,A66,ZFMISC_1:def 2;
reconsider p as Point of TRn by A83;
A86: hn.p in rng hn by A83, A10,A65,FUNCT_1:def 3;
reconsider q as Point of TRm by A84;
A87: hm.q in rng hm by A84,A5,A19,FUNCT_1:def 3;
p in Or by A81,A85,ZFMISC_1:87;
then hn.p in hn.:Or by A83, A10,A65,FUNCT_1:def 6;
then not hn.p in Fr Rn by XBOOLE_0:3,A78,A9;
then
A88: hn.p in Rn\Fr Rn by A86,A73,XBOOLE_0:def 5;
then reconsider hnp=hn.p as Point of TRn;
A89: h.x = f1.(hnm.x) by A80,FUNCT_1:12;
q in Os by A81,A85,ZFMISC_1:87;
then hm.q in hm.:Os by A84,A5,A19,FUNCT_1:def 6;
then not hm.q in Fr Rm by XBOOLE_0:3,A13,A4;
then
A90: hm.q in Rm\Fr Rm by A87,A14,XBOOLE_0:def 5;
then reconsider hmq=hm.q as Point of TRm;
A91:hm.q in Om by A90,TOPS_1:40,A75;
hnm.x =hnm.(p,q) by A85;
then
A92: y = f1. [hnp,hmq] by A82,A89,A83,A84,A10,A65,A5,A19,FUNCT_3:def 8;
A93: f1. [hnp,hmq] = f.(hnp,hmq) by A86,A87,A73,A14,ZFMISC_1:87,FUNCT_1:49
.= hnp^hmq by A18;
then hnp^hmq in [#](TRnm | RNM) by A92,A79;
then reconsider hpq=hnp^hmq as Point of TRnm by A11;
A94: hn. p in ON by A88,TOPS_1:40,A69;
for i st i in Seg nm holds hpq.i in ]. (0.TRnm).i - 1,(0.TRnm).i+1.[
proof
len hmq = m by CARD_1:def 7;
then
A95: dom hmq=Seg m by FINSEQ_1:def 3;
len hnp = n by CARD_1:def 7;
then
A96: dom hnp = Seg n by FINSEQ_1:def 3;
len hpq= nm by CARD_1:def 7;
then
A97: dom hpq=Seg nm by FINSEQ_1:def 3;
let i such that
A98: i in Seg nm;
A99: (0.TRnm).i =0 by A15;
per cases by A97,A98,FINSEQ_1:25;
suppose
A100: i in dom hnp;
A101: (0.TRn).i =0 by A7;
hnp.i in ]. (0.TRn).i - 1,(0.TRn).i+1 .[ by A100,A94,A96,Th3;
hence thesis by A101, A100,FINSEQ_1:def 7,A99;
end;
suppose
ex k be Nat st k in dom hmq & i=len hnp+k;
then consider k be Nat such that
A102: k in dom hmq
and
A103: i=len hnp+k;
A104: (0.TRm).k =0 by A6;
hmq.k in ]. (0.TRm).k - 1,(0.TRm).k+1.[ by A95,A102,Th3,A91;
hence thesis by A104, FINSEQ_1:def 7,A102,A103,A99;
end;
end;
hence thesis by Th3,A93,A92;
end;
let y be object;
assume
A105:y in OO;
then reconsider pq=y as Point of TRnm;
rng pq c= REAL;
then reconsider pq as FinSequence of REAL by FINSEQ_1:def 4;
len pq= nm by CARD_1:def 7;
then consider p,q be FinSequence of REAL such that
A106: len p = n
and
A107: len q = m
and
A108: pq = p^q by FINSEQ_2:23;
reconsider q as Point of TRm by TOPREAL7:17,A107;
A109: dom q= Seg m by A107,FINSEQ_1:def 3;
A110: now
let i such that
A111: i in Seg m;
A112: (0.TRnm).(i+n) = 0 by A15;
A113: (0.TRm).i = 0 by A6;
i+n in Seg nm by A111,FINSEQ_1:60;
then pq.(i+n) in ]. 0-1,0+1 .[ by A112,A105,Th3;
hence q.i in ]. (0.TRm).i - 1,(0.TRm).i+1 .[
by A106,A108,FINSEQ_1:def 7,A109,A111,A113;
end;
then
A114: q in Om by Th3;
q in Rm by A76,Th3,A110;
then q in rng hm by A3,TOPS_2: def 5,A14;
then consider xq be object such that
A115: xq in dom hm
and
A116: hm.xq=q by FUNCT_1:def 3;
reconsider p as Point of TRn by TOPREAL7:17,A106;
A117: dom p = Seg n by A106,FINSEQ_1:def 3;
A118: now
A119: Seg n c= Seg nm by NAT_1:11,FINSEQ_1:5;
let i such that
A120: i in Seg n;
A121: (0.TRn).i = 0 by A7;
(0.TRnm).i = 0 by A15;
then pq.i in ]. 0-1,0+1 .[ by A119,A120,A105,Th3;
hence p.i in ]. (0.TRn).i - 1,(0.TRn).i +1 .[
by A108,FINSEQ_1:def 7,A117,A120,A121;
end;
then
A122: p in ON by Th3;
p in Rn by Th3,A118,A70;
then p in rng hn by A8,TOPS_2: def 5,A73;
then consider xp be object such that
A123: xp in dom hn
and
A124: hn.xp=p by FUNCT_1:def 3;
reconsider xq as Point of TRm by A115,A5,A19;
reconsider xp as Point of TRn by A123, A10,A65;
A125: [xp,xq] in [:Rr,Rs:] by A65, A123, A115,A19,ZFMISC_1:87;
A126: [p, q] = hnm. (xp,xq) by FUNCT_3:def 8,A115,A116, A123, A124
.=hnm. [xp,xq];
[p,q] in [:Rn,Rm:] by A70,A122, A76,A114,ZFMISC_1:87;
then
A127: [xp,xq] in dom h by A125,A68,A66,A126,A74,FUNCT_1:11;
not q in Fr Rm by A114, A75, TOPS_1:39,XBOOLE_0:3;
then not xq in Fr Rs by A4,A115,A116,FUNCT_1:def 6;
then xq in Rs\Fr Rs by A115,A19,XBOOLE_0:def 5;
then
A128: xq in Os by A12,TOPS_1:40;
not p in Fr Rn by A122, A69, TOPS_1:39,XBOOLE_0:3;
then not xp in Fr Rr by A9,A123,A124,FUNCT_1:def 6;
then xp in Rr\Fr Rr by A123,A65,XBOOLE_0:def 5;
then xp in Or by A77,TOPS_1:40;
then
A129: [xp,xq] in [:Or,Os:] by A128,ZFMISC_1:87;
f1. [p,q] = f.(p,q) by A70,A122, A76,A114,ZFMISC_1:87,FUNCT_1:49
.= p^q by A18;
then h. [xp,xq] = y by A127,A126,FUNCT_1:12,A108;
hence y in h.: [:Or,Os:] by A129,A127,FUNCT_1:def 6;
end;
theorem Th16:
for r,s st r>0 & s>0
for f be Function of T1,(TOP-REAL n)|ClosedHypercube(pn,n|->r)
for g be Function of T2,(TOP-REAL m)| ClosedHypercube(pm,m|->s)
st f is being_homeomorphism & g is being_homeomorphism
holds
ex h be Function of [:T1,T2:],(TOP-REAL (n+m))|
ClosedHypercube(0.TOP-REAL (n+m),(n+m)|->1)
st h is being_homeomorphism &
for t1, t2 holds
f.t1 in OpenHypercube(pn,r) & g.t2 in OpenHypercube(pm,s)
iff
h. (t1,t2) in OpenHypercube(0.TOP-REAL (n+m),1)
proof
set nm=n+m,TRn=TOP-REAL n,TRm=TOP-REAL m,TRnm=TOP-REAL nm;
let r,s such that
A1: r>0
and
A2: s>0;
set Rn=n|->r,Rm=m|->s,Rnm=nm|->1;
set RR=ClosedHypercube(pn,Rn),RS=ClosedHypercube(pm,Rm),CL = ClosedHypercube
(0.TRnm,Rnm);
reconsider Rs=RS as non empty Subset of TRm by A2;
reconsider Rr=RR as non empty Subset of TRn by A1;
set Or=OpenHypercube(pn,r),Os=OpenHypercube(pm,s),
O = OpenHypercube(0.TRnm,1);
consider h be Function of [: TRn| Rr,TRm| Rs:],TRnm| CL such that
A3: h is being_homeomorphism
and
A4: h.:[: Or, Os:] = O by Th15,A1,A2;
let f be Function of T1,TRn| RR;
let g be Function of T2,TRm| RS such that
A5: f is being_homeomorphism
and
A6: g is being_homeomorphism;
A7: dom g = [#]T2 by A6,TOPS_2:def 5;
reconsider G=g as Function of T2,TRm| Rs;
reconsider F=f as Function of T1,TRn| Rr;
reconsider fgh=h*[:F,G:] as Function of [:T1,T2:],TRnm| CL;
take fgh;
[:F,G:] is being_homeomorphism by A5,A6,Th14;
hence fgh is being_homeomorphism by A3,TOPS_2:57;
then
A8: dom fgh= [#][:T1,T2:] by TOPS_2:def 5;
let t1,t2;
dom f = [#]T1 by A5,TOPS_2:def 5;
then
A9: [f.t1,g.t2] = [:F,G:]. (t1,t2) by A7,FUNCT_3:def 8
.= [:F,G:]. [t1,t2];
A10: [#] (TRm| Rs)= Rs by PRE_TOPC:def 5;
[#] (TRn| Rr) = Rr by PRE_TOPC:def 5;
then
A11:[#] [: TRn| Rr,TRm| Rs:] = [:Rr,Rs:] by A10,BORSUK_1:def 2;
A12: Os c= Rs by Th12;
A13: Or c= Rr by Th12;
A14: dom h = [#][: TRn| Rr,TRm| Rs:] by A3,TOPS_2:def 5;
thus f.t1 in Or & g.t2 in Os implies fgh.(t1,t2) in O
proof
assume that
A15: f.t1 in Or
and
A16: g.t2 in Os;
A17: [f.t1,g.t2] in [: Or, Os:] by ZFMISC_1:87,A15,A16;
[f.t1,g.t2] in dom h by A15,A13, A16,A12,A11,A14, ZFMISC_1:87;
then
h. [f.t1,g.t2] in O by A17,A4,FUNCT_1:def 6;
hence thesis by A8,A9,FUNCT_1:12;
end;
assume
A18: fgh.(t1,t2) in O;
fgh.(t1,t2) = h. [f.t1,g.t2] by A8,FUNCT_1:12,A9;
then consider xy be object such that
A19: xy in dom h
and
A20: xy in [: Or, Os:]
and
A21: h.xy = h. [f.t1,g.t2] by A18,FUNCT_1: def 6,A4;
[f.t1,g.t2] in dom h by A8,FUNCT_1:11,A9;
then xy = [f.t1,g.t2] by A19,A21, A3,FUNCT_1:def 4;
hence thesis by A20,ZFMISC_1:87;
end;
registration
let n;
cluster non boundary convex compact for Subset of TOP-REAL n;
existence
proof
ClosedHypercube(0.TOP-REAL n,n|->1) is non boundary convex compact;
hence thesis;
end;
end;
theorem Th17:
for A be non boundary convex compact Subset of TOP-REAL n,
B be non boundary convex compact Subset of TOP-REAL m,
C be non boundary convex compact Subset of TOP-REAL (n+m)
for f be Function of T1,(TOP-REAL n)| A,
g be Function of T2,(TOP-REAL m)| B
st f is being_homeomorphism & g is being_homeomorphism
holds
ex h be Function of [:T1,T2:],(TOP-REAL (n+m))| C
st h is being_homeomorphism &
for t1, t2 holds f.t1 in Int A & g.t2 in Int B
iff
h.(t1,t2) in Int C
proof
set TRn = TOP-REAL n,TRm=TOP-REAL m,nm=n+m,TRnm=TOP-REAL nm;
let A be non boundary convex compact Subset of TRn, B be non boundary convex
compact Subset of TRm, C be non boundary convex compact Subset of TRnm;
let f be Function of T1,TRn| A, g be Function of T2,TRm| B such that
A1: f is being_homeomorphism
and
A2: g is being_homeomorphism;
set Rn=ClosedHypercube(0.TRn,n|->1),Rm=ClosedHypercube(0.TRm,m|->1),Rnm=
ClosedHypercube(0.TRnm,nm|->1);
consider gm be Function of TRm |B,TRm |Rm such that
A3: gm is being_homeomorphism
and
A4: gm.:Fr B = Fr Rm by BROUWER2:7;
A5: gm.:Int B misses gm.:Fr B by A3, TOPS_1:39,FUNCT_1:66;
A6: B is non empty;
then reconsider gmg= gm*g as Function of T2,TRm |Rm;
A7: gmg is being_homeomorphism by A2,A3,A6,TOPS_2:57;
then
A8: dom gmg =[#]T2 by TOPS_2:def 5;
reconsider Rn as non empty Subset of TRn;
consider fn be Function of TRn |A,TRn |Rn such that
A9: fn is being_homeomorphism
and
A10: fn.:Fr A = Fr Rn by BROUWER2:7;
A11:fn.:Int A misses fn.:Fr A by A9, TOPS_1:39,FUNCT_1:66;
A12: A is non empty;
then reconsider fnf= fn*f as Function of T1,TRn |Rn;
A13: fnf is being_homeomorphism by A1,A9,A12,TOPS_2:57;
then
A14: dom fnf =[#]T1 by TOPS_2:def 5;
A15: [#](TRm|Rm)=Rm by PRE_TOPC:def 5;
A16: Int C = C\Fr C by TOPS_1:40;
A17: [#](TRnm|C)=C by PRE_TOPC:def 5;
A18: Int Rm = Rm\Fr Rm by TOPS_1:40;
set OHn=OpenHypercube(0.TRn,1),OHm=OpenHypercube(0.TRm,1),
OHnm=OpenHypercube(0. TRnm,1);
consider H be Function of TRnm |Rnm,TRnm |C such that
A19: H is being_homeomorphism
and
A20: H.:Fr Rnm = Fr C by BROUWER2:7;
A21:H.:Int Rnm misses H.:Fr Rnm by A19, TOPS_1:39,FUNCT_1:66;
A22: Int Rm = OHm by Th11;
consider P be Function of [:T1,T2:],TRnm| Rnm such that
A23: P is being_homeomorphism
and
A24: for t1, t2 holds fnf.t1 in OHn & gmg.t2 in OHm
iff P. (t1,t2) in OHnm by A7,A13,Th16;
reconsider HP= H*P as Function of [:T1,T2:],TRnm |C;
take HP;
C is non empty;
hence HP is being_homeomorphism by A23,A19,TOPS_2:57;
then
A25: dom HP=[#][:T1,T2:] by TOPS_2:def 5;
A26: [#](TRn|Rn)=Rn by PRE_TOPC:def 5;
A27: Int Rn = Rn\Fr Rn by TOPS_1:40;
let t1,t2;
A28: P. [t1,t2] in dom H by A25,FUNCT_1:11;
A29:Int Rnm = OHnm by Th11;
A30: HP. [t1,t2] in rng HP by A25,FUNCT_1:def 3;
thus f.t1 in Int A & g.t2 in Int B implies HP. (t1,t2) in Int C
proof
A31: f.t1 in dom fn by A14,FUNCT_1:11;
assume that
A32: f.t1 in Int A
and
A33: g.t2 in Int B;
fnf.t1 = fn.(f.t1) by A14,FUNCT_1:12;
then fnf.t1 in fn.:Int A by A31,A32,FUNCT_1:def 6;
then not fnf.t1 in Fr Rn by A10,A11,XBOOLE_0:3;
then fnf.t1 in Rn \Fr Rn by A26,XBOOLE_0:def 5;
then
A34: fnf.t1 in OHn by Th11,A27;
A35: g.t2 in dom gm by A8,FUNCT_1:11;
A36: P. [t1,t2] in dom H by A25,FUNCT_1:11;
A37: HP. [t1,t2] = H.(P. [t1,t2]) by A25,FUNCT_1:12;
gmg.t2 = gm.(g.t2) by A8,FUNCT_1:12;
then gmg.t2 in gm.:Int B by A35,A33,FUNCT_1:def 6;
then not gmg.t2 in Fr Rm by A4,A5,XBOOLE_0:3;
then gmg.t2 in Rm \Fr Rm by A15,XBOOLE_0:def 5;
then P.(t1,t2) in OHnm by A24,A34,A22,A18;
then HP. [t1,t2] in H.:Int Rnm by A37,A36,FUNCT_1:def 6, A29;
then not HP. [t1,t2] in Fr C by XBOOLE_0:3,A21,A20;
hence thesis by A16, A30,A17,XBOOLE_0:def 5;
end;
assume HP. (t1,t2) in Int C;
then
A38: not HP. [t1,t2] in H.:Fr Rnm by XBOOLE_0:def 5,A16,A20;
A39: [#](TRn|A) = A by PRE_TOPC:def 5;
A40: [#](TRnm|Rnm)=Rnm by PRE_TOPC:def 5;
A41: gmg.t2 = gm.(g.t2) by A8,FUNCT_1:12;
A42: Int Rnm = Rnm\Fr Rnm by TOPS_1:40;
A43: f.t1 in dom fn by A14,FUNCT_1:11;
A44: HP. [t1,t2] = H.(P. [t1,t2]) by A25,FUNCT_1:12;
P. [t1,t2] in Int Rnm
proof
assume not P. [t1,t2] in Int Rnm;
then P. [t1,t2] in Fr Rnm by A40,A42,XBOOLE_0:def 5;
hence thesis by A44,A28,FUNCT_1:def 6,A38;
end;
then
A45: P.(t1,t2) in OHnm by Th11;
then gmg.t2 in Rm\Fr Rm by A24,A22,A18;
then
A46: not gmg.t2 in Fr Rm by XBOOLE_0:def 5;
Int Rn = OHn by Th11;
then fnf.t1 in Rn\Fr Rn by A45,A24,A27;
then
A47: not fnf.t1 in Fr Rn by XBOOLE_0:def 5;
A48: fnf.t1 = fn.(f.t1) by A14,FUNCT_1:12;
thus f.t1 in Int A
proof
assume not f. t1 in Int A;
then not f.t1 in A\Fr A by TOPS_1:40;
then f.t1 in Fr A by A39,A43,XBOOLE_0:def 5;
hence thesis by A48,A43,FUNCT_1:def 6,A47,A10;
end;
assume not g. t2 in Int B;
then
A49: not g.t2 in B\Fr B by TOPS_1:40;
A50: g.t2 in dom gm by A8,FUNCT_1:11;
[#](TRm|B) = B by PRE_TOPC:def 5;
then g.t2 in Fr B by A49,A50,XBOOLE_0:def 5;
hence thesis by A41,A50,FUNCT_1:def 6,A46,A4;
end;
Lm1: r>0 implies cl_Ball(p,r) is non boundary compact
proof
assume
A1: r>0;
Ball(p,r) c= Int cl_Ball(p,r) by TOPREAL9:16,TOPS_1:24;
hence thesis by A1;
end;
theorem Th18:
for pn be Point of TOP-REAL n,pm be Point of TOP-REAL m
for r,s st r>0 & s>0
ex h be Function of [: Tdisk(pn,r),Tdisk(pm,s):],Tdisk(0.TOP-REAL (n+m),1)
st h is being_homeomorphism &
h.:[:Ball(pn,r), Ball(pm,s):] = Ball(0.TOP-REAL (n+m),1)
proof
A1:n in NAT & m in NAT & n+m in NAT by ORDINAL1:def 12;
set TRn=TOP-REAL n,TRm=TOP-REAL m, nm=n+m,TRnm=TOP-REAL nm;
let pn be Point of TRn,pm be Point of TRm;
let r,s such that
A2: r>0
and
A3: s>0;
reconsider CLn=cl_Ball(pn,r) as non empty Subset of TRn by A2;
A4:Int CLn = CLn\Fr CLn by TOPS_1:40
.=CLn \Sphere(pn,r) by A2, BROUWER2:5
.= CLn \(CLn\Ball(pn,r)) by A1,JORDAN:19
.= CLn /\Ball(pn,r) by XBOOLE_1:48
.=Ball(pn,r) by TOPREAL9: 16,XBOOLE_1:28;
reconsider CLm=cl_Ball(pm,s) as non empty Subset of TRm by A3;
A5:Int CLm = CLm\Fr CLm by TOPS_1:40
.= CLm \Sphere(pm,s) by A3, BROUWER2:5
.= CLm \(CLm\Ball(pm,s)) by A1,JORDAN:19
.= CLm /\Ball(pm,s) by XBOOLE_1:48
.= Ball(pm,s) by TOPREAL9: 16,XBOOLE_1:28;
reconsider CLnm=cl_Ball(0.TRnm,1) as non empty Subset of TRnm;
A6: TRn |CLn = Tdisk(pn,r) by BROUWER:def 2;
A7: Ball(0.TRnm,1) c= CLnm by TOPREAL9: 16;
A8: [#]Tdisk(0.TRnm,1) = CLnm by A1,BROUWER:3;
A9: TRnm|CLnm = Tdisk(0.TRnm, 1) by BROUWER:def 2;
A10:Int CLnm = CLnm\Fr CLnm by TOPS_1:40
.= CLnm \Sphere(0.TRnm,1) by BROUWER2:5
.= CLnm \(CLnm\Ball(0.TRnm,1)) by A1,JORDAN:19
.= CLnm /\Ball(0.TRnm,1) by XBOOLE_1:48
.=Ball(0.TRnm,1) by TOPREAL9: 16,XBOOLE_1:28;
set Rn=ClosedHypercube(0.TRn,n|->1),Rm=ClosedHypercube(0.TRm,m|->1),
Rnm=ClosedHypercube(0.TRnm,nm|->1);
A11: [#](TRm |Rm) = Rm by PRE_TOPC:def 5;
A12: Ball(pn,r) c= CLn by TOPREAL9: 16;
CLn is non boundary convex compact Subset of TRn by A2,Lm1;
then consider fn be Function of TRn |CLn,TRn |Rn such that
A13: fn is being_homeomorphism
and
A14: fn.:Fr CLn = Fr Rn by BROUWER2:7;
A15:fn.:Int CLn misses fn.:Fr CLn by TOPS_1:39, A13,FUNCT_1:66;
[#](TRn |Rn) = Rn by PRE_TOPC:def 5;
then
A16: rng fn = Rn by A13, TOPS_2:def 5;
CLm is non boundary convex compact by A3,Lm1;
then consider gm be Function of TRm |CLm,TRm |Rm such that
A17: gm is being_homeomorphism
and
A18: gm.:Fr CLm = Fr Rm by BROUWER2:7;
A19: TRm |CLm = Tdisk(pm,s) by BROUWER:def 2;
[#](TRm |Rm) = Rm by PRE_TOPC:def 5;
then
A20: rng gm = Rm by A17, TOPS_2:def 5;
A21: Ball(pm,s) c= CLm by TOPREAL9: 16;
A22: [#]Tdisk(pn,r) = CLn by A1,BROUWER:3;
then
A23: dom fn = CLn by A6,A13, TOPS_2:def 5;
CLnm is non boundary convex compact by Lm1;
then consider P be Function of [:Tdisk(pn,r),Tdisk(pm,s):], Tdisk(0.TRnm,1)
such that
A24: P is being_homeomorphism
and
A25: for t1 be Point of TRn |CLn, t2 be Point of TRm |CLm holds fn.t1 in
Int Rn & gm.t2 in Int Rm iff P. (t1,t2) in Int CLnm
by A6,A19,A9,Th17,A13,A17;
take P;
thus P is being_homeomorphism by A24;
A26:gm.:Int CLm misses gm.:Fr CLm by TOPS_1:39, A17,FUNCT_1:66;
A27: [#]Tdisk(pm,s) = CLm by A1,BROUWER:3;
then
A28: dom gm = CLm by A19,A17, TOPS_2:def 5;
A29: dom gm = CLm by A19,A17,A27, TOPS_2:def 5;
thus P.:[: Ball(pn,r), Ball(pm,s):] c= Ball(0.TRnm,1)
proof
let y be object;
assume y in P.:[: Ball(pn,r), Ball(pm,s):];
then consider x be object such that
x in dom P
and
A30: x in [: Ball(pn,r), Ball(pm,s):]
and
A31: P.x=y by FUNCT_1:def 6;
consider y1,y2 be object such that
A32: y1 in Ball(pn,r)
and
A33: y2 in Ball(pm,s)
and
A34: x = [y1,y2] by A30,ZFMISC_1:def 2;
reconsider y1 as Point of TRn |CLn by A32,A12,A1,BROUWER:3,A6;
fn.y1 in fn.:Int CLn by A32,A4,A12,A23,FUNCT_1:def 6;
then
A35: not fn.y1 in Fr Rn by A15,XBOOLE_0:3,A14;
reconsider y2 as Point of TRm |CLm by A33,A21,A1,BROUWER:3,A19;
gm.y2 in gm.:Int CLm by A33,A5,A21,A29,FUNCT_1:def 6;
then not gm.y2 in Fr Rm by XBOOLE_0:3,A26,A18;
then gm.y2 in Rm\Fr Rm by A11,XBOOLE_0:def 5;
then
A36: gm.y2 in Int Rm by TOPS_1:40;
fn.y1 in Rn by A32,A12,A23,FUNCT_1:def 3,A16;
then fn.y1 in Rn\Fr Rn by A35,XBOOLE_0:def 5;
then fn.y1 in Int Rn by TOPS_1:40;
then P. (y1,y2) in Int CLnm by A25,A36;
hence thesis by A31,A34,A10;
end;
let y be object;
assume
A37:y in Ball(0.TRnm,1);
rng P = [#]Tdisk(0.TRnm,1) by TOPS_2:def 5,A24;
then consider x be object such that
A38: x in dom P
and
A39: P.x=y by A37,A7,A8,FUNCT_1:def 3;
[#][:Tdisk(pn,r),Tdisk(pm,s):] = [: [#]Tdisk(pn,r),[#]Tdisk(pm,s):] by
BORSUK_1:def 2;
then consider y1,y2 be object such that
A40: y1 in CLn
and
A41: y2 in CLm
and
A42: x=[y1,y2] by A38,A22,A27,ZFMISC_1:def 2;
reconsider y2 as Point of TRm |CLm by A19, A1,BROUWER:3,A41;
reconsider y1 as Point of TRn |CLn by A6,A40,A1,BROUWER:3;
A43: P.x = P.(y1,y2) by A42;
then fn.y1 in Int Rn by A25,A39, A37,A10;
then fn.y1 in Rn\fn.:Fr CLn by TOPS_1:40,A14;
then fn.y1 in (fn.:CLn)\fn.:Fr CLn by RELAT_1: 113,A23,A16;
then fn.y1 in fn.:(CLn\Fr CLn) by A13,FUNCT_1: 64;
then fn.y1 in fn.:(Int CLn) by TOPS_1:40;
then ex z1 be object st z1 in dom fn & z1 in Int CLn & fn.z1 = fn.y1 by
FUNCT_1:def 6;
then
A44:y1 in Int CLn by A23,A40, A13, FUNCT_1:def 4;
gm.y2 in Int Rm by A43,A25,A39, A37,A10;
then gm.y2 in Rm\gm.:Fr CLm by TOPS_1:40,A18;
then gm.y2 in (gm.:CLm)\gm.:Fr CLm by RELAT_1: 113,A28,A20;
then gm.y2 in gm.:(CLm\Fr CLm) by A17,FUNCT_1: 64;
then gm.y2 in gm.:(Int CLm) by TOPS_1:40;
then ex z2 be object st z2 in dom gm & z2 in Int CLm & gm.z2 = gm.y2
by FUNCT_1:def 6;
then y2 in Int CLm by A28,A41, A17, FUNCT_1:def 4;
then [y1,y2] in [:Ball(pn,r), Ball(pm,s):] by A44,A5,A4,ZFMISC_1:87;
hence thesis by A38,A39,A42,FUNCT_1:def 6;
end;
theorem
r >0 & s>0 &
T1,(TOP-REAL n)|Ball(pn,r) are_homeomorphic &
T2,(TOP-REAL m)|Ball(pm,s) are_homeomorphic
implies
[:T1,T2:],(TOP-REAL (n+m))|Ball(0.TOP-REAL (n+m),1) are_homeomorphic
proof
reconsider N=n,M=m as Element of NAT by ORDINAL1:def 12;
set TRn=TOP-REAL N,TRm=TOP-REAL M, NM=N+M,TRnm=TOP-REAL NM;
reconsider Pn=pn as Point of TRn;
reconsider Pm=pm as Point of TRm;
assume that
A1: r >0
and
A2: s>0;
reconsider Bm=Ball(Pm,s) as non empty Subset of TRm by A2;
A3: [#]Tdisk(Pm,s) = cl_Ball(Pm,s) by BROUWER:3;
then reconsider BBm = Ball(Pm,s) as Subset of Tdisk(Pm,s) by TOPREAL9:16;
A4:Tdisk(Pm,s) = TRm|cl_Ball(Pm,s) by BROUWER:def 2;
then
A5:Tdisk(Pm,s) |BBm = TRm|Ball(Pm,s) by A3,PRE_TOPC:7;
reconsider Bn=Ball(Pn,r) as non empty Subset of TRn by A1;
reconsider Bnm=Ball(0.TRnm,1) as non empty Subset of TRnm;
A6: [#]Tdisk(Pn,r) = cl_Ball(pn,r) by BROUWER:3;
then reconsider BBn = Ball(Pn,r) as Subset of Tdisk(Pn,r) by TOPREAL9:16;
A7: [#]Tdisk(0.TRnm,1) = cl_Ball(0.TRnm,1) by BROUWER:3;
then reconsider BBnm = Ball(0.TRnm,1) as Subset of Tdisk(0.TRnm,1)
by TOPREAL9:16;
A8:Tdisk(0.TRnm,1) = TRnm|cl_Ball(0.TRnm,1) by BROUWER:def 2;
then
A9:Tdisk(0.TRnm,1) |BBnm = TRnm|Ball(0.TRnm,1) by A7, PRE_TOPC:7;
assume T1,(TOP-REAL n)|Ball(pn,r) are_homeomorphic;
then consider f1 be Function of T1,TRn|Bn such that
A10: f1 is being_homeomorphism by T_0TOPSP:def 1;
assume T2,(TOP-REAL m)|Ball(pm,s) are_homeomorphic;
then consider f2 be Function of T2,TRm|Bm such that
A11: f2 is being_homeomorphism by T_0TOPSP:def 1;
A12: [:f1,f2:] is being_homeomorphism by A10,A11,Th14;
consider h be Function of [: Tdisk(Pn,r),Tdisk(Pm,s):], Tdisk(0.TRnm,1) such
that
A13: h is being_homeomorphism
and
A14: h.:[: Ball(Pn,r), Ball(Pm,s):] = Ball(0.TRnm,1) by A1,A2, Th18;
A15:Tdisk(Pn,r) = TRn|cl_Ball(Pn,r) by BROUWER:def 2;
then Tdisk(Pn,r) |BBn = TRn|Ball(Pn,r) by A6,PRE_TOPC:7;
then
A16:[: Tdisk(Pn,r),Tdisk(Pm,s):] | [:BBn,BBm:] = [: TRn|Bn,TRm|Bm:] by A5,
BORSUK_3:22;
then reconsider h1=h| [:BBn,BBm:] as Function of [: TRn|Bn,TRm|Bm:],TRnm|Bnm
by JORDAN24:12,A9,A14, A1,A15, A2,A4, A8;
reconsider hf=h1*[:f1,f2:] as Function of [:T1,T2:],TRnm|Bnm;
h1 is being_homeomorphism by A9,A16,A13,A14, METRIZTS:2;
then hf is being_homeomorphism by A12, TOPS_2:57;
hence thesis by T_0TOPSP:def 1;
end;
begin :: Tietze Extension Theorem
reserve T,S for TopSpace,
A for closed Subset of T,
B for Subset of S;
Lm2: for V being Subset of TopSpaceMetr Euclid n holds
V is open implies for e being Point of Euclid n st e in V
ex r be Real st r>0 & OpenHypercube(e,r) c= V
proof
let V be Subset of TopSpaceMetr Euclid n;
assume
A1: V is open;
let e be Point of Euclid n;
assume e in V;
then consider r being Real such that
A2: r > 0
and
A3: Ball(e,r) c= V by A1,TOPMETR:15;
per cases;
suppose
A4: n<>0;
OpenHypercube(e,r/sqrt(n)) c= Ball(e,r) by A4,EUCLID_9:17;
hence thesis by A2,A3,XBOOLE_1:1, A4;
end;
suppose
A5: n=0;
set TR=TOP-REAL 0,Z=0.TR;
A6: OpenHypercube(e,1) = {Z} by EUCLID_9:12, A5;
A7: the carrier of TR = REAL 0 by EUCLID:22;
the carrier of Euclid 0=the carrier of TR by EUCLID:67;
then Ball(e,r) = {} or Ball(e,r) = {Z}
by A7,EUCLID:77,ZFMISC_1:33,A5;
hence thesis by A6,A2,A3;
end;
end;
theorem Th21:
for n be non zero Nat
for F be Element of n-tuples_on Funcs(the carrier of T,the carrier of R^1)
st for i st i in dom F for h be Function of T,R^1 st h = F.i
holds h is continuous holds <:F:> is continuous
proof
let n be non zero Nat;
let F be Element of n-tuples_on Funcs(the carrier of T,the carrier of R^1)
such that
A1: for i st i in dom F for h be Function of T,R^1 st h = F.i
holds h is continuous;
set TR=TOP-REAL n,FF=<:F:>;
A2: for Y be Subset of TR st Y is open holds FF"Y is open
proof
let Y be Subset of TR;
set E=Euclid n;
A3: the TopStruct of TR = TopSpaceMetr E by EUCLID: def 8;
then reconsider YY=Y as Subset of TopSpaceMetr E;
assume Y is open;
then Y in the topology of TR;
then reconsider YY as open Subset of TopSpaceMetr E
by PRE_TOPC:def 2,A3;
A4: dom FF = the carrier of T by FUNCT_2:def 1;
for x be set holds x in FF"Y
iff
ex Q be Subset of T st Q is open & Q c= FF"Y & x in Q
proof
let x be set;
len F = n by CARD_1:def 7;
then
A5: dom F = Seg n by FINSEQ_1:def 3;
hereby
assume
A6: x in FF"Y;
then
A7: FF.x in Y by FUNCT_1:def 7;
then reconsider FFx=FF.x as Point of E by EUCLID: 67;
consider m be Real such that
A8: m>0
and
A9: OpenHypercube(FFx,m) c= YY by A7, Lm2;
defpred P[Nat,object] means ex h be Function of T,R^1 st
h = F.$1 & $2= h"].FFx.$1-m,FFx.$1+m.[;
A10: for k be Nat st k in Seg n ex x be object st P[k,x]
proof
let k be Nat such that
A11: k in Seg n;
F.k in rng F by A5,A11,FUNCT_1:def 3;
then consider h be Function such that
A12: F.k = h
and
A13: dom h = the carrier of T
and
A14: rng h c= the carrier of R^1 by FUNCT_2:def 2;
reconsider h as Function of T,R^1 by A13,A14,FUNCT_2:2;
take h"].FFx.k-m,FFx.k+m.[;
thus thesis by A12;
end;
consider p be FinSequence such that
A15: dom p = Seg n & for k be Nat st k in Seg n holds P[k,p.k]
from FINSEQ_1:sch 1(A10);
A16: for Y be set holds Y in rng p implies x in Y
proof
let Y be set;
assume Y in rng p;
then consider k be object such that
A17: k in dom p
and
A18: p.k=Y by FUNCT_1:def 3;
reconsider k as Nat by A17;
consider h be Function of T,R^1 such that
A19: h = F.k
and
A20: p.k= h"].FFx.k-m,FFx.k+m.[ by A17,A15;
A21: dom h = the carrier of T by FUNCT_2:def 1;
A22: FFx.k > FFx.k-m by A8,XREAL_1:44;
FFx.k+m> FFx.k by A8,XREAL_1:39;
then
A23: FFx.k in ].FFx.k-m,FFx.k+m.[ by A22,XXREAL_1:4;
h.x = FFx.k by A19,Th20;
hence thesis by A21,A6,A23,A20,A18,FUNCT_1:def 7;
end;
rng p c= bool the carrier of T
proof
let y be object;
assume y in rng p;
then consider k be object such that
A24: k in dom p
and
A25: p.k=y by FUNCT_1:def 3;
reconsider k as Nat by A24;
ex h be Function of T,R^1 st
h = F.k & p.k= h"].FFx.k-m,FFx.k+m .[ by A24,A15;
hence thesis by A25;
end;
then reconsider R=rng p as finite Subset-Family of T;
take M=meet R;
now
let A be Subset of T;
A26: [#]R^1 =REAL by TOPMETR:17;
assume A in R;
then consider k be object such that
A27: k in dom p
and
A28: p.k=A by FUNCT_1:def 3;
reconsider k as Nat by A27;
consider h be Function of T,R^1 such that
A29: h = F.k
and
A30: p.k= h"].FFx.k-m,FFx.k+m.[ by A27,A15;
reconsider P=].FFx.k-m,FFx.k+m.[ as Subset of R^1 by TOPMETR:17;
A31: P is open by JORDAN6:35;
h is continuous by A1,A5,A27,A29,A15;
hence A is open by A31,A26,TOPS_2:43,A28,A30;
end;
hence M is open by TOPS_2:def 1,TOPS_2:20;
thus M c= FF"Y
proof
let q be object;
set I = Intervals(FFx,m);
A32: dom I = dom FFx by EUCLID_9:def 3;
assume
A33: q in M;
then reconsider q as Point of T;
FF.q in rng FF by A4,A33,FUNCT_1:def 3;
then reconsider FFq=FF.q as Point of TR;
len FFx = n by CARD_1:def 7;
then
A34: dom FFx = Seg n by FINSEQ_1:def 3;
A35: for y be object st y in dom I holds FFq.y in I.y
proof
let y be object;
assume
A36: y in dom I;
then reconsider i=y as Nat;
consider h be Function of T,R^1 such that
A37: h = F.i
and
A38: p.i= h"].FFx.i-m,FFx.i+m.[ by A36,A15,A34,A32;
A39: h.q = FFq.i by A37,Th20;
p.i in rng p by A36,A34,A32,A15,FUNCT_1:def 3;
then meet rng p c= p.i by SETFAM_1:3;
then h.q in ].FFx.i-m,FFx.i+m.[ by A38, A33,FUNCT_1:def 7;
hence thesis by A39,A32,A36,EUCLID_9:def 3;
end;
len FFq = n by CARD_1:def 7;
then dom FFq = Seg n by FINSEQ_1:def 3;
then FFq in product I by A35,CARD_3:def 5,A32,A34;
then FFq in OpenHypercube(FFx,m) by EUCLID_9:def 4;
hence thesis by A9, A4,A33,FUNCT_1:def 7;
end;
rng p <> {} by A15,RELAT_1:42;
hence x in M by A16,SETFAM_1:def 1;
end;
thus thesis;
end;
hence thesis by TOPS_1:25;
end;
[#]TR<>{};
hence thesis by A2,TOPS_2:43;
end;
theorem Th22:
for T,A st T is normal
for f being Function of (T | A),
(TOP-REAL n) | ClosedHypercube(0.TOP-REAL n,n|->1)
st f is continuous
ex g being Function of T,
(TOP-REAL n) | ClosedHypercube(0.TOP-REAL n,n|->1)
st g is continuous & g|A = f
proof
let T,A such that
A1:T is normal;
set TR=TOP-REAL n;
set N = 0.TOP-REAL n;
set H=ClosedHypercube(N,n |-> 1);
let f be Function of T|A, TR | H such that
A2: f is continuous;
A3: [#](TR | H) = H by PRE_TOPC:def 5;
A4: [#](T|A) = A by PRE_TOPC:def 5;
per cases;
suppose
A5: A is empty;
reconsider TRH=TR|H as non empty TopSpace;
set g=the continuous Function of T,TRH;
A6: g|A={} by A5;
f={} by A5;
hence thesis by A6;
end;
suppose
A7: A is non empty;
set CC=Closed-Interval-TSpace(-1,1);
per cases;
suppose
A8: n=0;
reconsider TRH=TR|H as non empty TopSpace;
A9: {0.TOP-REAL n} = the carrier of TR by EUCLID:22,A8,JORDAN2C:105;
then reconsider Z=0.TOP-REAL n as Point of TRH by A3,ZFMISC_1:33;
H = the carrier of TR by A9,ZFMISC_1:33;
then
A10: rng f = the carrier of TR by A4,A7,A3,A9,ZFMISC_1:33;
reconsider g = T --> Z as Function of T,TR|H;
take g;
A11: (the carrier of T)/\A=A by XBOOLE_1:28;
dom f = A by FUNCT_2:def 1,A4;
then
f = A --> 0.TOP-REAL n
by A10,FUNCOP_1:9,EUCLID:22,A8,JORDAN2C:105;
hence thesis by A11,FUNCOP_1:12;
end;
suppose n<>0;
then reconsider nn=n as non zero Element of NAT by ORDINAL1:def 12;
set CC=Closed-Interval-TSpace(-1,1);
reconsider F=f as Function of T|A,TR by FUNCT_2:7,A3;
defpred F[Nat,object] means ex g be continuous Function of T, R^1 st
$2=g & rng g c= [#]CC & g|A = PROJ(n,$1)*F;
A12: dom f = A by A4,FUNCT_2:def 1;
N = 0*n by EUCLID:70;
then
A13: N = n|->0 by EUCLID:def 4;
A14: for k be Nat st k in Seg n ex x be object st F[k,x]
proof
A15: the carrier of CC = [. -1,1.] by TOPMETR:18;
A16: T is non empty by A7;
let k be Nat such that
A17: k in Seg n;
rng f c= H by A3;
then PROJ(n,k).:rng F c= PROJ(n,k).:H by RELAT_1:123;
then
A18: PROJ(n,k).:rng F c=[. N.k -(n|->1).k, N.k +(n|->1).k .]
by A17,Th7;
A19: dom (PROJ(n,k)*F) = the carrier of (T|A) by FUNCT_2:def 1;
A20: N.k = 0 by A13;
(n|->1).k = 1 by A17,FINSEQ_2:57;
then rng (PROJ(n,k)*F) c= [. -1,1.] by A20,A18,RELAT_1:127;
then reconsider PF=PROJ(n,k)*F as Function of (T|A),CC
by A19,A15,FUNCT_2:2;
A21: F is continuous by A2,PRE_TOPC:26;
PROJ(n,k) is continuous by TOPREALC:57,A17;
then consider g be continuous Function of T, CC such that
A22: g|A = PF by A21,A16, A7,PRE_TOPC:27,A1,TIETZE:23;
A23: rng g c= REAL;
dom g =the carrier of T by FUNCT_2:def 1;
then
reconsider G=g as Function of T, R^1 by A23,TOPMETR:17,FUNCT_2:2;
A24: G is continuous by PRE_TOPC: 26;
rng g c= the carrier of CC by RELAT_1:def 19;
hence thesis by A24,A22;
end;
consider pp be FinSequence such that
A25: dom pp = Seg n
and
A26: for k be Nat st k in Seg n holds F[k,pp.k]
from FINSEQ_1:sch 1(A14);
A27: len pp = nn by A25,FINSEQ_1:def 3;
rng pp c= Funcs(the carrier of T, the carrier of R^1)
proof
let y be object;
assume y in rng pp;
then consider k be object such that
A28: k in dom pp
and
A29: pp.k = y by FUNCT_1:def 3;
reconsider k as Nat by A28;
consider g be continuous Function of T, R^1 such that
A30: pp.k=g
and
rng g c= [#]CC
and
g|A = PROJ(n,k)*F by A25,A26,A28;
A31: rng g c= the carrier of R^1 by RELAT_1:def 19;
dom g = the carrier of T by FUNCT_2 :def 1;
hence thesis by A31,FUNCT_2:def 2,A29,A30;
end;
then
pp is FinSequence of Funcs(the carrier of T, the carrier of R^1)
by FINSEQ_1:def 4;
then reconsider pp as Element of nn-tuples_on
Funcs(the carrier of T, the carrier of R^1) by A27,FINSEQ_2:92;
A32: dom <:pp:> = the carrier of T by FUNCT_2:def 1;
A33: the carrier of CC = [.-1,1.] by TOPMETR:18;
rng <:pp:> c= H
proof
let y be object;
assume
A34: y in rng <:pp:>;
then consider x be object such that
A35: x in dom <:pp:>
and
A36: <:pp:>.x = y by FUNCT_1:def 3;
reconsider p = <:pp:>.x as Point of TR by A34,A36;
now
let j be Nat;
A37: N.j =0 by A13;
assume
A38: j in Seg n;
then consider g be continuous Function of T, R^1 such that
A39: g=pp.j
and
A40: rng g c= [#]CC
and
g|A = PROJ(n,j)*F by A26;
A41: dom g = the carrier of T by FUNCT_2:def 1;
g.x = p.j by Th20,A39;
then
A42: p.j in rng g by A41,A35,FUNCT_1:def 3;
(n|->1).j = 1 by A38,FINSEQ_2:57;
hence p.j in [.N.j-(n|->1).j,N.j+(n|->1).j.]
by A37,A42,A40,A33;
end;
hence thesis by Def2,A36;
end;
then reconsider G=<:pp:> as Function of T,TR|H by A3,A32,FUNCT_2:2;
take G;
for i st i in dom pp for h be Function of T,R^1 st
h = pp.i holds h is continuous
proof
let k be Nat such that
A43: k in dom pp;
ex g be continuous Function of T, R^1 st pp.k=g & rng g c= [#]CC &
g|A = PROJ(n,k)*F by A25,A26,A43;
hence thesis;
end;
hence G is continuous by Th21, PRE_TOPC:27;
A44: dom (G|A) = A by A32,RELAT_1:62;
for e be set st e in dom f holds (G|A).e = f.e
proof
let e be set;
A45: rng F c= the carrier of TR;
assume
A46: e in dom f;
then G.e in rng G by A32,A12,FUNCT_1:def 3;
then
A47: G.e in H by A3;
f.e in rng f by A46,FUNCT_1:def 3;
then reconsider Ge=G.e,fe=f.e as Point of TR by A45,A47;
A48: len fe = n by CARD_1:def 7;
A49: now
A50: dom fe = Seg n by A48,FINSEQ_1:def 3;
let w be Nat;
assume that
A51: 1<= w
and
A52: w <= n;
consider g be continuous Function of T, R^1 such that
A53: g=pp.w
and
rng g c= [#]CC
and
A54: g|A = PROJ(n,w)*F by A51,A52,FINSEQ_1:1,A26;
A55: Ge.w = g.e by Th20,A53;
A56: e in dom (g|A) by A46,A12,FUNCT_2:def 1;
(g|A).e = g.e by A46, A4,FUNCT_1:49;
then Ge.w = PROJ(n,w).fe by A55,A56,A54,FUNCT_1:12;
hence Ge.w = fe/.w by TOPREALC:def 6
.= fe.w by PARTFUN1:def 6, A51,A52,FINSEQ_1:1,A50;
end;
A57: len Ge = n by CARD_1:def 7;
(G|A).e = G.e by A46,A44, A4,FUNCT_1:47;
hence thesis by A49,FINSEQ_1:14,A57,A48;
end;
hence thesis by A44,A12;
end;
end;
end;
theorem Th23:
for T,A st T is normal
for X be Subset of TOP-REAL n st X is compact non boundary convex
for f being Function of T|A,(TOP-REAL n) | X st
f is continuous
ex g being Function of T,(TOP-REAL n) | X st g is continuous & g|A=f
proof
set TR=TOP-REAL n;
let T,A such that
A1: T is normal;
let S be Subset of TR such that
A2:S is compact non boundary convex;
let f be Function of T|A,TR | S such that
A3:f is continuous;
A4: [#](T|A) = A by PRE_TOPC:def 5;
A5: [#](TR | S) = S by PRE_TOPC:def 5;
per cases;
suppose
A6: A is empty;
reconsider TRS=TR|S as non empty TopSpace by A2,A5;
set g=the continuous Function of T,TRS;
A7: g|A={} by A6;
f={} by A6;
hence thesis by A7;
end;
suppose
A8: A is non empty;
set H=ClosedHypercube(0.TOP-REAL n,n |-> 1);
consider h be Function of TR |S,TR |H such that
A9: h is being_homeomorphism
and
h.:Fr S = Fr H by BROUWER2:7,A2;
A10: rng h = [#](TR|H) by A9,TOPS_2:def 5;
A11: TR|S is non empty by A5,A2;
then reconsider hf=h*f as Function of T|A,TR|H;
consider g be Function of T,TR|H such that
A12: g is continuous
and
A13: g|A=hf by A3, A9, A4,A8,A11,A1,Th22;
reconsider hg=h"*g as Function of T,TR|S;
take hg;
h" is being_homeomorphism by A9,TOPS_2:56;
hence hg is continuous by A12,TOPS_2:46;
A14: rng f c= the carrier of (TR|S);
A15: dom h = [#](TR|S) by A9,TOPS_2:def 5;
thus hg|A = h"*hf by RELAT_1:83,A13
.= (h"*h)*f by RELAT_1:36
.= (id [#](TR|S))*f by A9,A10,A15,TOPS_2:52
.= f by A14,RELAT_1:53;
end;
end;
::$N Tietze Extension Theorem for n-dimensional spaces
::$N The First Implication
theorem
for T,S,A,B st T is normal
for X be Subset of TOP-REAL n st
X is compact non boundary convex & B,X are_homeomorphic
for f being Function of T|A,S|B st f is continuous
ex g being Function of T,S|B st g is continuous & g|A = f
proof
let T,S,A,B such that
A1: T is normal;
A2: [#](T|A)=A by PRE_TOPC:def 5;
A3: [#](S|B)=B by PRE_TOPC:def 5;
set TR=TOP-REAL n;
let X be Subset of TR such that
A4: X is compact non boundary convex
and
A5: B,X are_homeomorphic;
consider h be Function of S|B,TR|X such that
A6:h is being_homeomorphism by METRIZTS:def 1,A5,T_0TOPSP:def 1;
A7: h" is continuous by TOPS_2:def 5,A6;
let f being Function of T|A,S|B such that
A8: f is continuous;
A9:rng f c= the carrier of (S|B);
A10: dom h = [#](S|B) by TOPS_2:def 5,A6;
A11:X is non empty by A4;
A12: rng h=[#](TR|X) by TOPS_2:def 5,A6;
then
A13: B is non empty by A11;
per cases;
suppose
A14: A is empty;
reconsider SB=S|B as non empty TopSpace by A11,A12;
set h=the continuous Function of T,SB;
reconsider h as Function of T,S|B;
take h;
f={} by A14;
hence thesis by A14;
end;
suppose
A15: A is non empty;
reconsider hf=h*f as Function of T|A,TR|X by A3,A13;
consider g be Function of T,TR | X such that
A16: g is continuous
and
A17: g|A=hf by A3,A13,A2,A11,A15,A8,A6,A1,A4,Th23;
reconsider hg= h"*g as Function of T,S| B by A11;
take hg;
hg |A = h"*(g|A) by RELAT_1:83
.= (h"*h)*f by A17,RELAT_1:36
.= (id dom h)*f by TOPS_2:52,A12, A6
.= f by A10,A9,RELAT_1:53;
hence thesis by A7,A11, A16,TOPS_2:46;
end;
end;
::$N The Second Implication
theorem
for T be non empty TopSpace, n st n>=1 &
for S be TopSpace,A be non empty closed Subset of T,B being Subset of S
st ex X be Subset of TOP-REAL n st
X is compact non boundary convex & B,X are_homeomorphic
holds
for f being Function of T|A,S|B st f is continuous
ex g being Function of T,S|B st g is continuous & g|A = f
holds T is normal
proof
let T be non empty TopSpace,n;
set TR= TOP-REAL n;
assume that
A1: n>=1 and
A2: for S be TopSpace,A be non empty closed Subset of T,B be Subset of S st
ex X be Subset of TR st
X is compact non boundary convex & B,X are_homeomorphic
holds
for f being Function of T|A,S|B st f is continuous
ex g being Function of T,S|B st g is continuous & g|A = f;
set CC=Closed-Interval-TSpace(-1,1);
for A be non empty closed Subset of T
for f be continuous Function of T|A, CC
ex g being continuous Function of T, Closed-Interval-TSpace(-1,1)
st g|A = f
proof
let A be non empty closed Subset of T;
let f be continuous Function of T|A, CC;
A3: the carrier of CC = [.-1,1.] by TOPMETR:18;
A4: rng f c= REAL;
dom f =the carrier of (T|A) by FUNCT_2:def 1;
then reconsider F=f as Function of T|A, R^1 by A4,TOPMETR:17,FUNCT_2:2;
reconsider F as continuous Function of T|A, R^1 by PRE_TOPC: 26;
set IF1=incl(F,n);
set n1=n|->1;
set CH=ClosedHypercube(0.TR,n1);
A5: dom IF1 = the carrier of (T|A) by FUNCT_2:def 1;
A6: [#](TR|CH)=CH by PRE_TOPC:def 5;
0.TR = 0*n by EUCLID:70;
then
A7: 0.TR = n |-> 0 by EUCLID:def 4;
A8: rng IF1 c= CH
proof
let y be object;
assume
A9: y in rng IF1;
then reconsider y as Point of TR;
consider x be object such that
A10: x in dom IF1 & IF1.x = y by A9,FUNCT_1:def 3;
reconsider x as Point of T|A by A10;
now let i;
assume
A11: i in Seg n;
then
A12: y.i = f.x by A10,TOPREALC:47;
A13: (0.TR) .i = 0 by A7;
n1.i = 1 by A11,FINSEQ_2:57;
hence y.i in [. 0.TR.i - n1.i,0.TR.i+n1.i .] by A3,A13,A12;
end;
hence thesis by Def2;
end;
then reconsider IF=IF1 as Function of T|A, TR|CH by A6,A5,FUNCT_2:2;
A14: IF is continuous by PRE_TOPC:27;
A15: n in Seg n by A1,FINSEQ_1:1;
consider g be Function of T,TR|CH such that
A16: g is continuous & g|A = IF by A2,A14,METRIZTS:def 1;
set P=PROJ(n,n);
A17: P|CH = P|(TR|CH) by A6, TMAP_1:def 4;
reconsider Pch=P|CH as Function of TR|CH,R^1 by PRE_TOPC:9;
reconsider Pg=Pch*g as Function of T,R^1;
A18: P is continuous by A15,TOPREALC:57;
A19: dom Pg = the carrier of T by FUNCT_2:def 1;
A20: rng Pg c= rng Pch by RELAT_1:26;
A21: (0.TR) .n = 0 by A7;
A22: n1.n = 1 by A1,FINSEQ_1:1,FINSEQ_2:57;
P.:CH = [. 0.TR.n - n1.n, 0.TR.n + n1.n .] by A1,FINSEQ_1:1,Th7;
then rng Pg c= [. -1,1 .] by RELAT_1:115,A20,A21,A22;
then reconsider Pg as Function of T,CC by A19,A3,FUNCT_2:2;
A23: Pg is continuous by A18,A17,A16, PRE_TOPC:27;
A24: dom Pch = CH by FUNCT_2:def 1;
(Pch*g) |A = (Pch) * (g|A) by RELAT_1:83
.= P*IF by A16,A8,A24,RELAT_1:165
.= F by TOPREALC:56,A1;
hence thesis by A23;
end;
hence thesis by TIETZE:24;
end;