:: Brouwer Fixed Point Theorem for Simplexes
:: by Karol P\kak
::
:: Received December 21, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ABIAN, AOFA_I00, ARYTM_1, ARYTM_3, CARD_1, CARD_3, CLASSES1,
COMPLEX1, CONVEX1, EUCLID, EUCLID_9, FINSEQ_1, FINSEQ_2, FINSEQ_4,
FINSET_1, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_4, GLIB_000, INT_1, MATROID0,
MEASURE5, MEMBERED, METRIC_1, NAT_1, NEWTON, NUMBERS, ORDERS_1, ORDINAL1,
ORDINAL2, ORDINAL4, PARTFUN1, PCOMPS_1, PEPIN, POWER, PRE_TOPC, QC_LANG1,
RCOMP_1, REAL_1, RELAT_1, RLAFFIN1, RLAFFIN2, RLVECT_1, RLVECT_2,
RLVECT_5, RUSUB_4, SEMI_AF1, SEQ_4, SETFAM_1, SGRAPH1, SIMPLEX0,
SIMPLEX1, SQUARE_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, TOPDIM_1,
TOPMETR, TOPS_1, TOPS_2, VALUED_1, WEIERSTR, XBOOLE_0, XREAL_0, XXREAL_0,
XXREAL_1, XXREAL_2, ZFMISC_1, SIMPLEX2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ZFMISC_1, RELAT_1, FUNCT_1,
RELSET_1, FUNCT_2, PARTFUN1, FUNCOP_1, FUNCT_4, XXREAL_3, VALUED_1,
PRE_TOPC, NUMBERS, XCMPLX_0, XREAL_0, FINSEQ_1, BINOP_1, FINSEQ_2,
TOPMETR, METRIC_1, EUCLID, FINSET_1, XXREAL_0, REAL_1, SETFAM_1, TOPS_2,
INT_1, STRUCT_0, COMPTS_1, PCOMPS_1, RCOMP_1, WEIERSTR, SEQ_4, XXREAL_2,
RVSUM_1, RLVECT_1, RUSUB_4, RLVECT_5, SIMPLEX0, RLAFFIN1, RLAFFIN2,
SIMPLEX1, ORDERS_1, CARD_1, DOMAIN_1, PENCIL_1, CLASSES1, RLTOPSP1,
MATROID0, TBSP_1, MEMBERED, RLVECT_2, CONVEX1, TOPREAL9, COMPLEX1,
NEWTON, POWER, SQUARE_1, BORSUK_1, CARD_3, EUCLID_9, TMAP_1, FINSEQOP,
ABIAN, TOPDIM_1, TOPDIM_2, RLAFFIN3;
constructors ABIAN, BINOP_2, COMPTS_1, CONVEX1, EUCLID_9, FINSEQOP, FUNCSDOM,
MONOID_0, NEWTON, POWER, REAL_1, RFINSEQ2, RLAFFIN1, RLAFFIN2, RLAFFIN3,
RLVECT_5, RUSUB_5, SEQ_4, SIMPLEX1, SQUARE_1, TBSP_1, TMAP_1, TOPDIM_1,
TOPDIM_2, TOPREAL9, TOPS_2, WAYBEL23, WEIERSTR, RCOMP_1;
registrations BORSUK_1, BORSUK_2, CARD_1, COMPTS_1, EUCLID, EUCLID_9,
FINSEQ_1, FINSET_1, FUNCT_2, INT_1, JORDAN2B, JORDAN2C, MEMBERED,
METRIZTS, MONOID_0, NAT_1, NEWTON, NUMBERS, PCOMPS_1, PRE_TOPC, RELAT_1,
RELSET_1, RLAFFIN1, RLAFFIN3, SEQ_4, SIMPLEX0, SIMPLEX1, STRUCT_0,
SUBSET_1, TBSP_1, TMAP_1, TOPDIM_1, TOPDIM_2, TOPMETR, TOPREAL9,
TOPREALC, TOPS_1, VALUED_0, VALUED_1, XBOOLE_0, XREAL_0, XXREAL_0,
XXREAL_2, XXREAL_3, YELLOW13, JORDAN, ORDINAL1, FINSEQ_2;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
definitions ORDINAL1, TARSKI, TBSP_1;
equalities EUCLID, METRIC_1, PCOMPS_1, RLVECT_1, SIMPLEX0, SIMPLEX1, STRUCT_0,
SUBSET_1, XCMPLX_0, ORDINAL1;
expansions SIMPLEX0, TARSKI, TBSP_1;
theorems ABIAN, ABSVALUE, BINOP_1, BORSUK_1, BORSUK_3, BORSUK_5, CARD_1,
CARD_2, CLASSES1, COMPTS_1, CONVEX1, EUCLID, EUCLID_9, FINSEQ_1,
FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_4,
HAUSDORF, INT_1, JORDAN1K, JORDAN2B, JORDAN2C, MATROID0, MEMBERED,
METRIC_1, NAT_1, NEWTON, ORDERS_1, ORDINAL1, PARTFUN1, PCOMPS_1,
PCOMPS_2, POWER, PRE_TOPC, RCOMP_1, RELAT_1, RLAFFIN1, RLAFFIN2,
RLAFFIN3, RLVECT_1, RLVECT_2, RLVECT_3, RUSUB_4, RVSUM_1, SETFAM_1,
SIMPLEX0, SIMPLEX1, TARSKI, TBSP_1, TMAP_1, TOPDIM_1, TOPDIM_2, TOPGEN_5,
TOPGRP_1, TOPMETR, TOPREAL3, TOPREAL6, TOPREAL7, TOPREAL9, TOPREALC,
TOPS_1, TOPS_2, TOPS_3, TSEP_1, VALUED_1, WEIERSTR, XBOOLE_0, XBOOLE_1,
XCMPLX_1, XREAL_1, XXREAL_0, XXREAL_1, XXREAL_2, XXREAL_3, ZFMISC_1,
JORDAN5A;
schemes FINSEQ_1, FRAENKEL, FUNCT_2, NAT_1, NAT_2, SUBSET_1;
begin :: The Lebesgue Number
reserve M for non empty MetrSpace,
F,G for open Subset-Family of TopSpaceMetr M;
reconsider jj=1 as positive Real;
definition
let M such that
A1: TopSpaceMetr M is compact;
let F be Subset-Family of TopSpaceMetr M such that
A2: F is open and
A3: F is Cover of TopSpaceMetr M;
mode Lebesgue_number of F -> positive Real means :Def1:
for p be Point of M
ex A be Subset of TopSpaceMetr M st A in F & Ball(p,it) c= A;
existence
proof
set TM=TopSpaceMetr M;
consider G be Subset-Family of TM such that
A4: G c=F and
A5: G is Cover of TM and
A6: G is finite by A1,A2,A3,COMPTS_1:def 1;
per cases;
suppose A7: [#]TM in G;
take R=jj;
let x be Point of M;
take[#]TM;
thus thesis by A4,A7;
end;
suppose A8: not[#]TM in G;
set cTM=[#]TM;
set FUNCS=Funcs([#]TM,REAL);
consider g be FinSequence such that
A9: rng g=G and
g is one-to-one by A6,FINSEQ_4:58;
defpred P[Nat,set,set] means
for f1,f2 be Function of TM,R^1 st f1=$2 & f2=$3 & f1 is continuous holds
f2 is continuous & ex A be non empty Subset of TM st A`=g.($1+1) & for x be
Point of TM holds f2.x=max(f1.x,(dist_min A).x);
union G is non empty by A5,SETFAM_1:45;
then A10: g is non empty by A9,ZFMISC_1:2;
then A11: len g>=1 by NAT_1:14;
then A12: 1 in dom g by FINSEQ_3:25;
then A13: g.1 in rng g by FUNCT_1:def 3;
then reconsider g1=g.1 as Subset of TM by A9;
A14: g1``<>[#]TM by A8,A9,A12,FUNCT_1:def 3;
g1 is open by A2,A4,A9,A13,TOPS_2:def 1;
then reconsider g19=g1` as non empty closed Subset of TM by A14;
reconsider Dg19=dist_min g19 as Element of FUNCS by FUNCT_2:8,TOPMETR:17;
A15: for n be Nat st 1<=n & n<len g for x be Element of FUNCS ex y be
Element of FUNCS st P[n,x,y]
proof
let n be Nat such that
1<=n and
A16: n<len g;
let x be Element of FUNCS;
reconsider fx=x as Function of TM,R^1 by TOPMETR:17;
per cases;
suppose A17: not fx is continuous;
take y=x;
thus thesis by A17;
end;
suppose A18: fx is continuous;
1<=n+1 & n+1<=len g by A16,NAT_1:11,13;
then A19: n+1 in dom g by FINSEQ_3:25;
then g.(n+1) in G by A9,FUNCT_1:def 3;
then reconsider A=g.(n+1) as Subset of TM;
A``<>[#]TM by A8,A9,A19,FUNCT_1:def 3;
then reconsider A9=A` as non empty Subset of TM;
R^1 is SubSpace of R^1 by TSEP_1:2;
then consider h be continuous Function of TM,R^1 such that
A20: for x be Point of TM holds h.x=max(fx.x,(dist_min A9).x) by A18,
TOPGEN_5:50;
reconsider y=h as Element of FUNCS by FUNCT_2:8,TOPMETR:17;
take y;
let f1,f2 be Function of TM,R^1 such that
A21: f1=x and
A22: f2=y and
f1 is continuous;
thus f2 is continuous by A22;
take A9;
thus thesis by A20,A21,A22;
end;
end;
consider p be FinSequence of FUNCS such that
A23: len p=len g and
A24: p/.1=Dg19 or len g=0 and
A25: for n be Nat st 1<=n & n<len g holds P[n,p/.n,p/.(n+1)]
from NAT_2:sch 1(A15);
A26: len p in dom p by A11,A23,FINSEQ_3:25;
p/.(len p) is Element of FUNCS;
then reconsider pL=p/.(len p) as Function of TM,R^1 by TOPMETR:17;
reconsider rngPL=rng pL as Subset of R^1 by RELAT_1:def 19;
set cRpL=[#]rngPL;
A27: cRpL=rng pL by WEIERSTR:def 1;
A28: dom p=dom g by A23,FINSEQ_3:29;
defpred Q[Nat] means
for f be Function of TM,R^1 st$1 in dom p & f=p/.$1 holds f is continuous &
for j be Nat,h be Function of TM,R^1 st j<=$1 & j in dom p & h=p/.j for x be
Point of TM holds h.x<=f.x;
A29: for n be Nat st Q[n] holds Q[n+1]
proof
let n be Nat;
assume A30: Q[n];
let f be Function of TM,R^1 such that
A31: n+1 in dom p and
A32: f=p/.(n+1);
per cases;
suppose A33: n=0;
hence f is continuous by A10,A24,A32;
let j be Nat,g be Function of TM,R^1;
assume that
A34: j<=n+1 and
A35: j in dom p and
A36: g=p/.j;
1<=j by A35,FINSEQ_3:25;
hence thesis by A32,A33,A34,A36,XXREAL_0:1;
end;
suppose n>0;
then reconsider n1=n-1 as Element of NAT by NAT_1:20;
p/.n is Element of FUNCS;
then reconsider pn=p/.n as Function of TM,R^1 by TOPMETR:17;
n+1<=len p by A31,FINSEQ_3:25;
then A37: 1<=n1+1 & n<len p by NAT_1:11,13;
then A38: n in dom p by FINSEQ_3:25;
then A39: pn is continuous by A30;
hence f is continuous by A23,A25,A32,A37;
consider A be non empty Subset of TM such that
A`=g.(n+1) and
A40: for y be Point of TM holds f.y=max(pn.y,(dist_min A).y) by A23,A25
,A32,A37,A39;
let j be Nat,h be Function of TM,R^1 such that
A41: j<=n+1 and
A42: j in dom p and
A43: h=p/.j;
let x be Point of TM;
A44: f.x=max(pn.x,(dist_min A).x) by A40;
per cases by A41,NAT_1:8;
suppose A45: j<=n;
A46: pn.x<=f.x by A44,XXREAL_0:25;
h.x<=pn.x by A30,A38,A42,A43,A45;
hence thesis by A46,XXREAL_0:2;
end;
suppose j=n+1;
hence thesis by A32,A43;
end;
end;
end;
A47: Q[0] by FINSEQ_3:25;
A48: for n be Nat holds Q[n] from NAT_1:sch 2(A47,A29);
A49: dom pL=cTM by FUNCT_2:def 1;
then pL.:cTM=rng pL by RELAT_1:113;
then A50: rngPL is compact by A1,A26,A48,WEIERSTR:9;
then A51: cRpL is compact by WEIERSTR:13;
reconsider cRpL as non empty real-bounded Subset of REAL
by A50,WEIERSTR:11,def 1;
set L=lower_bound cRpL;
L in cRpL by A51,RCOMP_1:14;
then consider x be object such that
A52: x in dom pL and
A53: pL.x=L by A27,FUNCT_1:def 3;
union G=[#]TM by A5,SETFAM_1:45;
then consider Y be set such that
A54: x in Y and
A55: Y in rng g by A9,A52,TARSKI:def 4;
reconsider x as Point of TM by A52;
consider j be object such that
A56: j in dom g and
A57: g.j=Y by A55,FUNCT_1:def 3;
reconsider j as Nat by A56;
A58: j<=len g by A56,FINSEQ_3:25;
A59: 1<=j by A56,FINSEQ_3:25;
now per cases by A59,XXREAL_0:1;
suppose A60: j=1;
then not x in g19 by A54,A57,XBOOLE_0:def 5;
then (dist_min g19).x<>0 by HAUSDORF:9;
then (dist_min g19).x>0 by JORDAN1K:9;
hence 0<L by A23,A24,A26,A28,A48,A53,A56,A58,A60;
end;
suppose A61: j>1;
then reconsider j1=j-1 as Element of NAT by NAT_1:20;
(p/.j1 is Element of FUNCS) & p/.j is Element of FUNCS;
then reconsider pj1=p/.j1,pj=p/.j as Function of TM,R^1 by TOPMETR:17;
j1+1>1 by A61;
then A62: 1<=j1 & j1<len g by A58,NAT_1:13;
then j1 in dom p by A23,FINSEQ_3:25;
then A63: pj1 is continuous by A48;
P[j1,pj1,pj] by A25,A28,A48,A56,A62;
then consider A be non empty Subset of TM such that
A64: A`=g.j and
A65: for x be Point of TM holds pj.x=max(pj1.x,(dist_min A).x) by A63;
A` is open by A2,A4,A9,A55,A57,A64,TOPS_2:def 1;
then A66: A is closed by TOPS_1:3;
not x in A by A54,A57,A64,XBOOLE_0:def 5;
then (dist_min A).x<>0 by A66,HAUSDORF:9;
then A67: (dist_min A).x>0 by JORDAN1K:9;
pj.x=max(pj1.x,(dist_min A).x) by A65;
then pj.x>0 by A67,XXREAL_0:25;
hence 0<L by A23,A26,A28,A48,A53,A56,A58;
end;
end;
then reconsider L as positive Real;
take L;
let X be Point of M;
defpred P[Nat] means
$1 in dom p & for f1 be Function of TM,R^1 st p/.$1=f1 holds f1.X>=L;
pL.X in cRpL by A27,A49,FUNCT_1:def 3;
then P[len p] by A11,A23,FINSEQ_3:25,XXREAL_2:3;
then A68: ex k be Nat st P[k];
consider k being Nat such that
A69: P[k] and
A70: for n be Nat st P[n] holds k<=n from NAT_1:sch 5(A68);
A71: 1<=k by A69,FINSEQ_3:25;
A72: k<=len p by A69,FINSEQ_3:25;
per cases by A71,XXREAL_0:1;
suppose A73: k=1;
take g1;
thus g1 in F by A4,A9,A13;
let y be object such that
A74: y in Ball(X,L);
reconsider Y=y as Point of M by A74;
A75: dist(X,Y)<L by A74,METRIC_1:11;
assume not y in g1;
then Y in g19 by XBOOLE_0:def 5;
then A76: (dist_min g19).X<=dist(X,Y) by HAUSDORF:13;
(dist_min g19).X>=L by A10,A24,A69,A73;
hence contradiction by A75,A76,XXREAL_0:2;
end;
suppose A77: k>1;
then reconsider k1=k-1 as Element of NAT by NAT_1:20;
(p/.k1 is Element of FUNCS) & p/.k is Element of FUNCS;
then reconsider pk1=p/.k1,pk=p/.k as Function of TM,R^1 by TOPMETR:17;
k1+1>1 by A77;
then A78: 1<=k1 & k1<len g by A23,A72,NAT_1:13;
then k1 in dom p by A23,FINSEQ_3:25;
then A79: pk1 is continuous by A48;
P[k1,pk1,pk] by A25,A48,A69,A78;
then consider A be non empty Subset of TM such that
A80: A`=g.k and
A81: for x be Point of TM holds pk.x=max(pk1.x,(dist_min A).x) by A79;
take A`;
A` in G by A9,A28,A69,A80,FUNCT_1:def 3;
hence A` in F by A4;
let y be object such that
A82: y in Ball(X,L);
reconsider Y=y as Point of M by A82;
assume not y in A`;
then Y in A by XBOOLE_0:def 5;
then A83: (dist_min A).X<=dist(X,Y) by HAUSDORF:13;
dist(X,Y)<L by A82,METRIC_1:11;
then A84: (dist_min A).X<L by A83,XXREAL_0:2;
A85: pk.X>=L by A69;
pk.X=max(pk1.X,(dist_min A).X) by A81;
then P[k1] by A23,A78,A84,A85,FINSEQ_3:25,XXREAL_0:16;
then k1>=k1+1 by A70;
hence contradiction by NAT_1:13;
end;
end;
end;
end;
reserve L for Lebesgue_number of F;
theorem
TopSpaceMetr M is compact & F is Cover of TopSpaceMetr M & F c= G
implies L is Lebesgue_number of G
proof
assume that
A1: TopSpaceMetr M is compact and
A2: F is Cover of TopSpaceMetr M and
A3: F c=G;
A4: now let x be Point of M;
ex A be Subset of TopSpaceMetr M st A in F & Ball(x,L)c=A by A1,A2,Def1;
hence ex A be Subset of TopSpaceMetr M st A in G & Ball(x,L)c=A by A3;
end;
set TM=TopSpaceMetr M;
union F=[#]TM & union F c=union G by A2,A3,SETFAM_1:45,ZFMISC_1:77;
then G is Cover of TM by SETFAM_1:def 11;
hence thesis by A1,A4,Def1;
end;
theorem
TopSpaceMetr M is compact & F is Cover of TopSpaceMetr M & F is_finer_than G
implies L is Lebesgue_number of G
proof
assume that
A1: TopSpaceMetr M is compact and
A2: F is Cover of TopSpaceMetr M and
A3: F is_finer_than G;
set TM=TopSpaceMetr M;
A4: now let x be Point of M;
consider A be Subset of TopSpaceMetr M such that
A5: A in F and
A6: Ball(x,L)c=A by A1,A2,Def1;
consider B be set such that
A7: B in G and
A8: A c=B by A3,A5,SETFAM_1:def 2;
reconsider B as Subset of TM by A7;
take B;
thus B in G & Ball(x,L)c=B by A6,A7,A8;
end;
union F=[#]TM & union F c=union G by A2,A3,SETFAM_1:13,45;
then G is Cover of TM by SETFAM_1:def 11;
hence thesis by A1,A4,Def1;
end;
theorem
for L1 be positive Real st TopSpaceMetr M is compact &
F is Cover of TopSpaceMetr M & L1 <= L
holds L1 is Lebesgue_number of F
proof
let L9 be positive Real such that
A1: (TopSpaceMetr M is compact) & F is Cover of TopSpaceMetr M and
A2: L9<=L;
now let x be Point of M;
consider A be Subset of TopSpaceMetr M such that
A3: A in F & Ball(x,L)c=A by A1,Def1;
take A;
Ball(x,L9)c=Ball(x,L) by A2,PCOMPS_1:1;
hence A in F & Ball(x,L9)c=A by A3;
end;
hence thesis by A1,Def1;
end;
begin :: Bounded Simplicial Complexes
reserve n,k for Nat,
r for Real,
X for set,
M for Reflexive non empty MetrStruct,
A for Subset of M,
K for SimplicialComplexStr;
registration let M;
cluster finite -> bounded for Subset of M;
coherence
proof
let A be Subset of M;
per cases;
suppose A is empty;
hence thesis;
end;
suppose A1: A is non empty;
assume A is finite;
then reconsider a=A as finite non empty Subset of M by A1;
deffunc D(Point of M,Point of M)=dist($1,$2);
consider q be object such that
A2: q in a by XBOOLE_0:def 1;
set X={D(x,y) where x is Point of M,y is Point of M:x in a & y in a};
reconsider q as Point of M by A2;
A3: D(q,q) in X by A2;
A4: now let x be object;
assume x in X;
then ex y be Point of M,z be Point of M st x=D(y,z) & y in a & z in a;
hence x is real;
end;
A5: a is finite;
X is finite from FRAENKEL:sch 22(A5,A5);
then reconsider X as real-membered non empty finite set by A3,A4,
MEMBERED:def 3;
reconsider sX=sup X as Real;
reconsider sX1=sX+1 as Real;
take sX1;
D(q,q)=0 & D(q,q)<=sX by A3,METRIC_1:1,XXREAL_2:4;
hence 0<sX1;
let x,y be Point of M;
assume x in A & y in A;
then D(x,y) in X;
then D(x,y)<=sX by XXREAL_2:4;
hence thesis by XREAL_1:39;
end;
end;
end;
theorem
for S be finite non empty Subset of M
ex p,q be Point of M st p in S & q in S & dist(p,q) = diameter S
proof
let S be finite non empty Subset of M;
set q=the Element of S;
reconsider q as Point of M;
deffunc D(Point of M,Point of M)=dist($1,$2);
set X={D(x,y) where x is Point of M,y is Point of M:x in S & y in S};
A1: now let x be object;
assume x in X;
then ex y be Point of M,z be Point of M st x=D(y,z) & y in S & z in S;
hence x is real;
end;
A2: D(q,q) in X;
A3: S is finite;
X is finite from FRAENKEL:sch 22(A3,A3);
then reconsider X as real-membered non empty finite set by A1,A2,
MEMBERED:def 3;
reconsider sX=sup X as Real;
sX in X by XXREAL_2:def 6;
then consider p,q be Point of M such that
A4: sX=D(p,q) & p in S & q in S;
now let x,y be Point of M;
assume x in S & y in S;
then D(x,y) in X;
hence D(x,y)<=sX by XXREAL_2:4;
end;
then A5: diameter S<=sX by TBSP_1:def 8;
sX<=diameter S by A4,TBSP_1:def 8;
hence thesis by A4,A5,XXREAL_0:1;
end;
definition let M,K;
attr K is M bounded means :Def2:
ex r st for A st A in the topology of K holds
A is bounded & diameter A <= r;
end;
theorem Th5:
for K be non void SimplicialComplexStr st
K is M bounded & A is Simplex of K
holds A is bounded
proof
let K be non void SimplicialComplexStr;
assume K is M bounded;
then A1: ex r be Real st for A st A in the topology of K
holds A is bounded & diameter A<=r;
assume A is Simplex of K;
then A in the topology of K by PRE_TOPC:def 2;
hence thesis by A1;
end;
registration let M,X;
cluster M bounded non void for SimplicialComplex of X;
existence
proof
set m=the Element of M;
take K=Complex_of{{}X};
K is M bounded
proof
take r=diameter{}M;
let A;
A1: the topology of K=bool{}X by SIMPLEX0:4;
assume A in the topology of K;
hence thesis by A1;
end;
hence thesis;
end;
end;
registration let M;
cluster M bounded non void subset-closed finite-membered
for SimplicialComplexStr;
existence
proof
take the M bounded non void SimplicialComplex of the set;
thus thesis;
end;
end;
registration let M,X;
let K be M bounded SimplicialComplexStr of X;
cluster -> M bounded for (SubSimplicialComplex of K);
coherence
proof
let SK be SubSimplicialComplex of K;
A1: the topology of SK c=the topology of K by SIMPLEX0:def 13;
consider r be Real such that
A2: for A st A in the topology of K holds A is bounded & diameter A<=r by
Def2;
take r;
let A;
assume A in the topology of SK;
hence thesis by A1,A2;
end;
end;
registration
let M,X;
let K be M bounded subset-closed SimplicialComplexStr of X;
let i be dim-like number;
cluster Skeleton_of(K,i) -> M bounded;
coherence;
end;
theorem Th6:
K is finite-vertices implies K is M bounded
proof
set V=Vertices K;
assume K is finite-vertices;
then V is finite;
then reconsider VM=V/\[#]M as finite Subset of M;
take diameter VM;
let A;
assume A1: A in the topology of K;
then reconsider S=A as Subset of K;
S is simplex-like by A1,PRE_TOPC:def 2;
then A c=V by SIMPLEX0:17;
then A c=VM by XBOOLE_1:19;
hence thesis by TBSP_1:24;
end;
begin
definition let M;
let K be SimplicialComplexStr such that
A1: K is M bounded;
func diameter(M,K) -> Real means :Def3:
(for A st A in the topology of K holds diameter A <= it)
& for r st (for A st A in the topology of K holds diameter A <= r)
holds r >= it if the topology of K meets bool [#]M
otherwise it = 0;
existence
proof
the topology of K meets bool[#]M implies ex d be Real st(for A st A in the
topology of K holds diameter A<=d) & for r be Real st(for A st A in the
topology of K holds diameter A<=r) holds r>=d
proof
defpred P[Subset of M] means
$1 in the topology of K & $1 is bounded;
deffunc D(Subset of M)=diameter$1;
set X={D(S) where S is Subset of M:P[S]};
now let x be object;
assume x in X;
then ex S be Subset of M st x=D(S) & P[S];
hence x is real;
end;
then reconsider X as real-membered set by MEMBERED:def 3;
assume the topology of K meets bool[#]M;
then consider B be object such that
A2: B in the topology of K and
A3: B in bool[#]M by XBOOLE_0:3;
reconsider B as Subset of M by A3;
consider rr be Real such that
A4: for A st A in the topology of K holds A is bounded & D(A)<=rr by A1;
now let x be ExtReal;
assume x in X;
then consider s be Subset of M such that
A5: x=D(s) & P[s];
thus x<=rr by A4,A5;
end;
then rr is UpperBound of X by XXREAL_2:def 1;
then A6: X is bounded_above by XXREAL_2:def 10;
B is bounded by A2,A4;
then D(B) in X by A2;
then reconsider sX=sup X as Real by A6;
take sX;
hereby let A;
assume A in the topology of K;
then P[A] by A4;
then D(A) in X;
hence D(A)<=sX by XXREAL_2:4;
end;
let r be Real such that
A7: for A st A in the topology of K holds diameter A<=r;
now let x be ExtReal;
assume x in X;
then consider A such that
A8: x=D(A) & P[A];
thus x<=r by A7,A8;
end;
then r is UpperBound of X by XXREAL_2:def 1;
hence thesis by XXREAL_2:def 3;
end;
hence thesis;
end;
uniqueness
proof
now let r1,r2 be Real such that
A9: (for A st A in the topology of K holds diameter A<=r1) & ((for r be
Real st(for A st A in the topology of K holds diameter A<=r) holds r>=r1
) & for A st A in the topology of K holds diameter A<=r2) & for r be Real
st(for A st A in the topology of K holds diameter A<=r) holds r>=r2;
r1<=r2 & r2<=r1 by A9;
hence r1=r2 by XXREAL_0:1;
end;
hence thesis;
end;
consistency;
end;
theorem Th7:
K is M bounded implies 0 <= diameter(M,K)
proof
assume A1: K is M bounded;
per cases;
suppose A2: the topology of K meets bool[#]M;
then consider S be object such that
A3: S in the topology of K and
A4: S in bool[#]M by XBOOLE_0:3;
reconsider S as Subset of M by A4;
ex r be Real st for A st A in the topology of K holds A is bounded &
diameter A<=r by A1;
then diameter S>=0 by A3,TBSP_1:21;
hence thesis by A1,A2,A3,Def3;
end;
suppose the topology of K misses bool[#]M;
hence thesis by A1,Def3;
end;
end;
theorem
for K be M bounded SimplicialComplexStr of X,
KX be SubSimplicialComplex of K
holds diameter(M,KX) <= diameter(M,K)
proof
let K be M bounded SimplicialComplexStr of X,KX be SubSimplicialComplex of K;
A1: the topology of KX c=the topology of K by SIMPLEX0:def 13;
per cases;
suppose A2: the topology of KX meets bool[#]M;
then the topology of K meets bool[#]M by A1,XBOOLE_1:63;
then for A st A in the topology of KX holds diameter A<=diameter(M,K) by A1
,Def3;
hence thesis by A2,Def3;
end;
suppose the topology of KX misses bool[#]M;
then diameter(M,KX)=0 by Def3;
hence thesis by Th7;
end;
end;
theorem
for K be M bounded subset-closed SimplicialComplexStr of X,
i be dim-like number
holds
diameter(M,Skeleton_of(K,i)) <= diameter(M,K)
proof
set r = the Real;
let K be M bounded subset-closed SimplicialComplexStr of X,
i be dim-like number;
set SK=Skeleton_of(K,i);
A1: the topology of SK c=the topology of K by SIMPLEX0:def 13;
per cases;
suppose A2: the topology of SK meets bool[#]M;
then A3: the topology of K meets bool[#]M by A1,XBOOLE_1:63;
now let A;
the_family_of K is subset-closed by MATROID0:def 3;
then A4: the topology of K is subset-closed by MATROID0:def 1;
assume A in the topology of SK;
then consider w be set such that
A5: A c=w and
A6: w in the_subsets_with_limited_card(i+1,the topology of K) by
SIMPLEX0:2;
reconsider w as Subset of K by A6;
w in the topology of K by A6,SIMPLEX0:def 2;
then A in the topology of K by A4,A5,CLASSES1:def 1;
hence diameter A<=diameter(M,K) by A3,Def3;
end;
hence thesis by A2,Def3;
end;
suppose the topology of SK misses bool[#]M;
then diameter(M,SK)=0 by Def3;
hence thesis by Th7;
end;
end;
definition let M;
let K be M bounded non void subset-closed SimplicialComplexStr;
redefine func diameter(M,K) means :Def4: :: redefines diameter (SIMPLEX2, definition)
(for A st A is Simplex of K holds diameter A <= it) &
for r st (for A st A is Simplex of K holds diameter A <= r)
holds r >= it;
compatibility
proof
let d be Real;
{}K is simplex-like;
then {}M in the topology of K by PRE_TOPC:def 2;
then A1: the topology of K meets bool[#]M by XBOOLE_0:3;
hereby assume A2: d=diameter(M,K);
hereby let A;
assume A is Simplex of K;
then A in the topology of K by PRE_TOPC:def 2;
hence diameter A<=d by A1,A2,Def3;
end;
let r be Real;
assume A3: for A st A is Simplex of K holds diameter A<=r;
for A st A in the topology of K holds diameter A<=r by A3,PRE_TOPC:def 2;
hence r>=d by A1,A2,Def3;
end;
assume that
A4: for A st A is Simplex of K holds diameter A<=d and
A5: for r be Real st(for A st A is Simplex of K holds diameter A<=r)
holds r>=d;
for A st A in the topology of K holds diameter A<=d by A4,PRE_TOPC:def 2;
then A6: diameter(M,K)<=d by A1,Def3;
now let A;
assume A is Simplex of K;
then A in the topology of K by PRE_TOPC:def 2;
hence diameter A<=diameter(M,K) by A1,Def3;
end;
then d<=diameter(M,K) by A5;
hence d=diameter(M,K) by A6,XXREAL_0:1;
end;
end;
theorem
for S be finite Subset of M holds diameter(M,Complex_of{S}) = diameter S
proof
let S be finite Subset of M;
set C=Complex_of{S};
reconsider C as M bounded non void SimplicialComplex of M by Th6;
reconsider s=S as Subset of C;
A1: the topology of C=bool S by SIMPLEX0:4;
now let W be Subset of M;
assume W is Simplex of C;
then W in bool S by A1,PRE_TOPC:def 2;
hence diameter W<=diameter S by TBSP_1:24;
end;
then A2: diameter(M,C)<=diameter S by Def4;
S c=S;
then s is simplex-like by A1,PRE_TOPC:def 2;
then diameter S<=diameter(M,C) by Def4;
hence thesis by A2,XXREAL_0:1;
end;
definition
let n;
let K be SimplicialComplexStr of TOP-REAL n;
attr K is bounded means
K is (Euclid n) bounded;
func diameter K -> Real equals
diameter(Euclid n,K);
coherence;
end;
registration
let n;
cluster bounded -> Euclid n bounded for (SimplicialComplexStr of TOP-REAL n);
coherence;
cluster bounded affinely-independent simplex-join-closed non void
finite-degree total for SimplicialComplex of TOP-REAL n;
existence
proof
set T=TOP-REAL n;
take C=Complex_of{{}TOP-REAL n};
C is Euclid n bounded by Th6;
hence thesis;
end;
cluster finite-vertices -> bounded for SimplicialComplexStr of TOP-REAL n;
coherence
by Th6;
end;
Lm1: [#]TOP-REAL n=[#]Euclid n
proof
the TopStruct of TOP-REAL n=TopSpaceMetr Euclid n by EUCLID:def 8;
hence thesis;
end;
begin :: The Estimation of Diameter of the Barycentric Subdivision
reserve V for RealLinearSpace,
Kv for non void SimplicialComplex of V;
Lm2: for x be set holds {x} is c=-linear
proof
let x be set;
let y,z be set;
assume that
A1: y in {x} and
A2: z in {x};
y=x by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
theorem Th11:
for S be Simplex of BCS Kv
for F be c=-linear finite finite-membered Subset-Family of V st
S = (center_of_mass V).:F
for a1,a2 be VECTOR of V st a1 in S & a2 in S
ex b1,b2 be VECTOR of V,r be Real st
b1 in Vertices BCS Complex_of{union F} &
b2 in Vertices BCS Complex_of{union F} &
a1-a2 = r*(b1-b2) & 0 <= r & r <= (card union F-1)/card union F
proof
let S be Simplex of BCS Kv;
set cM=center_of_mass V;
let F be c=-linear finite finite-membered Subset-Family of V such that
A1: S=cM.:F;
let a1,a2 be VECTOR of V such that
A2: a1 in S and
A3: a2 in S;
consider A1 be object such that
A4: A1 in dom cM and
A5: A1 in F and
A6: cM.A1=a1 by A1,A2,FUNCT_1:def 6;
consider A2 be object such that
A7: A2 in dom cM and
A8: A2 in F and
A9: cM.A2=a2 by A1,A3,FUNCT_1:def 6;
reconsider A1,A2 as set by TARSKI:1;
A10: A1,A2 are_c=-comparable by A5,A8,ORDINAL1:def 8;
set uF=union F;
set CuF=Complex_of{uF};
A11: for a1,a2 be VECTOR of V for A1,A2 be set st A1 c=A2 & A1 in dom cM & A1
in F & cM.A1=a1 & A1 in dom cM & A2 in F & cM.A2=a2 ex b1,b2 be VECTOR of V,r
be Real st b1 in Vertices BCS CuF & b2 in Vertices BCS CuF & a1-a2=r*(b1-b2) &
0<=r & r<=(card uF-1)/card uF
proof
let a1,a2 be VECTOR of V;
A12: the topology of CuF=bool uF by SIMPLEX0:4;
let A1,A2 be set such that
A13: A1 c=A2 and
A14: A1 in dom cM and
A15: A1 in F and
A16: cM.A1=a1 and
A1 in dom cM and
A17: A2 in F and
A18: cM.A2=a2;
A19: A1 c=uF by A15,ZFMISC_1:74;
A20: A1<>{} by A14,ORDERS_1:1;
then A21: uF is non empty by A19;
A22: A2 c=uF by A17,ZFMISC_1:74;
reconsider A1,A2 as non empty finite Subset of V by A13,A15,A17,A20;
set A21=A2\A1;
reconsider AA1={A1},AA2={A21} as Subset-Family of CuF;
{A1}c=bool uF by A19,ZFMISC_1:31;
then A23: AA1 is c=-linear finite simplex-like by A12,Lm2,SIMPLEX0:14;
A21 c=A2 by XBOOLE_1:36;
then A21 c=uF by A22;
then {A21}c=bool uF by ZFMISC_1:31;
then A24: AA2 is c=-linear finite simplex-like by A12,Lm2,SIMPLEX0:14;
A25: |.CuF.|c=[#]V;
[#]CuF=[#]V;
then A26: BCS CuF=subdivision(cM,CuF) by A25,SIMPLEX1:def 5;
A27: [#]subdivision(cM,CuF)=[#]CuF by SIMPLEX0:def 20;
then reconsider aa1={a1} as Subset of BCS CuF by A25,SIMPLEX1:def 5;
A28: a1 in aa1 by TARSKI:def 1;
then reconsider d1=a1 as Element of BCS CuF;
A29: dom cM=BOOL the carrier of V by FUNCT_2:def 1;
cM.:AA1=Im(cM,A1) by RELAT_1:def 16
.={a1} by A14,A16,FUNCT_1:59;
then aa1 is simplex-like by A23,A26,SIMPLEX0:def 20;
then A30: d1 is vertex-like by A28;
per cases;
suppose A31: A1=A2;
reconsider Z=0 as Real;
take b1=a1,b2=a1,Z;
card uF>=1 by A21,NAT_1:14;
then A32: card uF-1>=1-1 by XREAL_1:6;
a1-a2=0.V by A16,A18,A31,RLVECT_1:5;
hence thesis by A30,A32,RLVECT_1:10,SIMPLEX0:def 4;
end;
suppose A1<>A2;
then not A2 c=A1 by A13,XBOOLE_0:def 10;
then reconsider A21 as non empty finite Subset of V by XBOOLE_1:37;
A33: A21 in dom cM by A29,ORDERS_1:2;
then cM.A21 in rng cM by FUNCT_1:def 3;
then reconsider a21=cM.A21 as VECTOR of V;
reconsider aa2={a21} as Subset of BCS CuF by A25,A27,SIMPLEX1:def 5;
A34: a21 in aa2 by TARSKI:def 1;
then reconsider d2=a21 as Element of BCS CuF;
cM.:AA2=Im(cM,A21) by RELAT_1:def 16
.={a21} by A33,FUNCT_1:59;
then aa2 is simplex-like by A24,A26,SIMPLEX0:def 20;
then A35: d2 is vertex-like by A34;
set r1=1/card A1,r2=1/card A2,r21=1/card A21,r=card A21/card A2;
reconsider r1,r2,r21,r as Real;
take a1,a21,r;
A36: r*r21=(card A21*1)/(card A21*card A2) by XCMPLX_1:76
.=r2 by XCMPLX_1:91;
consider L1 be Linear_Combination of A1 such that
A37: Sum L1=r1*Sum A1 and
sum L1=r1*card A1 and
A38: L1=(ZeroLC V)+*(A1-->r1) by RLAFFIN2:15;
A39: Carrier(L1)c=A1 by RLVECT_2:def 6;
A40: card A21=1 *card A2-1 *card A1 by A13,CARD_2:44;
then A41: r1-r2=(card A21*1)/(card A2*card A1) by XCMPLX_1:130
.=r*r1 by XCMPLX_1:76;
consider L21 be Linear_Combination of A21 such that
A42: Sum L21=r21*Sum A21 and
sum L21=r21*card A21 and
A43: L21=(ZeroLC V)+*(A21-->r21) by RLAFFIN2:15;
A44: Carrier(L21)c=A21 by RLVECT_2:def 6;
consider L2 be Linear_Combination of A2 such that
A45: Sum L2=r2*Sum A2 and
sum L2=r2*card A2 and
A46: L2=(ZeroLC V)+*(A2-->r2) by RLAFFIN2:15;
A47: Carrier(L2)c=A2 by RLVECT_2:def 6;
for v be Element of V holds(L1-L2).v=(r*(L1-L21)).v
proof
let v be Element of V;
A48: dom(A21-->r21)=A21 by FUNCOP_1:13;
A49: (L1-L2).v=L1.v-L2.v by RLVECT_2:54;
A50: dom(A1-->r1)=A1 by FUNCOP_1:13;
A51: dom(A2-->r2)=A2 by FUNCOP_1:13;
(r*(L1-L21)).v=r*((L1-L21).v) by RLVECT_2:def 11;
then A52: (r*(L1-L21)).v=r*(L1.v-L21.v) by RLVECT_2:54;
per cases;
suppose A53: v in A1;
then not v in Carrier(L21) by A44,XBOOLE_0:def 5;
then A54: L21.v=0 by RLVECT_2:19;
A55: (A2-->r2).v=r2 & (A1-->r1).v=r1 by A13,A53,FUNCOP_1:7;
L1.v=(A1-->r1).v by A38,A50,A53,FUNCT_4:13;
hence thesis by A13,A41,A46,A49,A51,A52,A53,A54,A55,FUNCT_4:13;
end;
suppose A56: v in A2 & not v in A1;
then not v in Carrier L1 by A39;
then A57: L1.v=0 by RLVECT_2:19;
(A2-->r2).v=r2 by A56,FUNCOP_1:7;
then A58: (L1-L2).v=-r2 by A46,A49,A51,A56,A57,FUNCT_4:13;
A59: v in A21 by A56,XBOOLE_0:def 5;
then (A21-->r21).v=r21 by FUNCOP_1:7;
then (r*(L1-L21)).v=r*(-r21) by A43,A48,A52,A57,A59,FUNCT_4:13;
hence thesis by A36,A58;
end;
suppose A60: not v in A1 & not v in A2;
then not v in Carrier(L1) by A39;
then A61: L1.v=0 by RLVECT_2:19;
not v in Carrier(L21) by A44,A60,XBOOLE_0:def 5;
then A62: L21.v=0 by RLVECT_2:19;
not v in Carrier(L2) by A47,A60;
hence thesis by A49,A52,A62,A61,RLVECT_2:19;
end;
end;
then A63: L1-L2=r*(L1-L21) by RLVECT_2:def 9;
card A1>=1 & card A2<=card uF by A17,NAT_1:14,43,ZFMISC_1:74;
then card A1*card uF>=1 *card A2 by XREAL_1:66;
then card A2*card uF-card A1*card uF<=card uF*card A2-card A2 by XREAL_1:13
;
then A64: card A21*card uF<=(card uF-1)*card A2 by A40;
A65: Sum L21=a21 by A42,RLAFFIN2:def 2;
A66: Sum L1=a1 by A16,A37,RLAFFIN2:def 2;
Sum L2=a2 by A18,A45,RLAFFIN2:def 2;
then a1-a2=Sum(r*(L1-L21)) by A63,A66,RLVECT_3:4
.=r*Sum(L1-L21) by RLVECT_3:2
.=r*(a1-a21) by A65,A66,RLVECT_3:4;
hence thesis by A21,A30,A35,A64,SIMPLEX0:def 4,XREAL_1:102;
end;
end;
per cases by A10,XBOOLE_0:def 9;
suppose A1 c=A2;
hence thesis by A4,A5,A6,A8,A9,A11;
end;
suppose A2 c=A1;
then consider b1,b2 be VECTOR of V,r be Real such that
A67: b1 in Vertices BCS CuF & b2 in Vertices BCS CuF and
A68: a2-a1=r*(b1-b2) and
A69: 0<=r & r<=(card uF-1)/card uF by A5,A6,A7,A8,A9,A11;
take b2,b1,r;
a1-a2=-(r*(b1-b2)) by A68,RLVECT_1:33
.=r*(-(b1-b2)) by RLVECT_1:25
.=r*(b2-b1) by RLVECT_1:33;
hence thesis by A67,A69;
end;
end;
theorem Th12:
for A be affinely-independent Subset of TOP-REAL n
for E be Enumeration of A st dom E\X is non empty
holds
conv(E.:X) = meet{conv(A\{E.k}) where k is Element of NAT: k in dom E\X}
proof
let A be affinely-independent Subset of TOP-REAL n;
let E be Enumeration of A such that
A1: dom E\X is non empty;
set d=dom E;
defpred P[Nat] means
$1<>0 implies for X st card((dom E)\X)=$1 holds conv(A\E.:(d\X))=meet{conv(A
\{E.k}) where k is Element of NAT:k in dom E\X};
A2: rng E=A by RLAFFIN3:def 1;
A3: for i be Nat st P[i] holds P[i+1]
proof
deffunc C(set)=conv(A\{E.$1});
let i be Nat;
assume A4: P[i];
set i1=i+1;
assume i1<>0;
let X;
set U={C(k) where k is Element of NAT:k in d\X};
assume A5: card(d\X)=i1;
then d\X is non empty;
then consider m be object such that
A6: m in d\X by XBOOLE_0:def 1;
A7: m in d by A6,XBOOLE_0:def 5;
reconsider m as Element of NAT by A6;
A8: E.:{m}=Im(E,m) by RELAT_1:def 16
.={E.m} by A7,FUNCT_1:59;
per cases;
suppose i=0;
then consider x be object such that
A9: d\X={x} by A5,CARD_2:42;
A10: x=m by A6,A9,TARSKI:def 1;
A11: U c={C(m)}
proof
let u be object;
assume u in U;
then ex k be Element of NAT st u=C(k) & k in d\X;
then u=C(m) by A9,A10,TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
C(m) in U by A6;
then A12: U={C(m)} by A11,ZFMISC_1:33;
E.:(d\X)={E.m} by A6,A8,A9,TARSKI:def 1;
hence thesis by A12,SETFAM_1:10;
end;
suppose A13: i>0;
set Xm=X\/{m};
set Um={C(k) where k is Element of NAT:k in d\Xm};
set t=the Element of(d\Xm);
A14: d\X\{m}\/{m}=d\X by A6,ZFMISC_1:116;
A15: d\X\{m}=d\Xm by XBOOLE_1:41;
A16: Um c=U
proof
let x be object;
assume x in Um;
then consider k be Element of NAT such that
A17: x=C(k) and
A18: k in d\Xm;
k in d\X by A15,A14,A18,XBOOLE_0:def 3;
hence thesis by A17;
end;
m in {m} by TARSKI:def 1;
then not m in d\X\{m} by XBOOLE_0:def 5;
then A19: card(d\X\{m})+1=card(d\X) by A14,CARD_2:41;
then d\Xm is non empty by A5,A13,A15;
then t in d\Xm;
then A20: C(t) in Um;
set c =C(m),CC={c};
set CA=Complex_of{A};
A21: the topology of CA =bool A by SIMPLEX0:4;
A22: U c=Um\/CC
proof
let x be object;
assume x in U;
then consider k be Element of NAT such that
A23: x=C(k) and
A24: k in d\X;
k in d\Xm or k in {m} by A15,A14,A24,XBOOLE_0:def 3;
then k in d\Xm or k=m by TARSKI:def 1;
then x in Um or x in CC by A23,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
C(m) in U by A6;
then CC c=U by ZFMISC_1:31;
then A25: Um\/CC c=U by A16,XBOOLE_1:8;
reconsider A1=A\E.:(d\Xm),A2=A\{E.m} as Subset of CA;
A\{E.m}c=A by XBOOLE_1:36;
then A26: A2 is simplex-like by A21,PRE_TOPC:def 2;
A\E.:(d\Xm)c=A by XBOOLE_1:36;
then A1 is simplex-like by A21,PRE_TOPC:def 2;
then A27: conv@A1/\conv@A2=conv@(A1/\A2) by A26,SIMPLEX1:def 8;
E.:(d\Xm)\/{E.m} =E.:((d\Xm)\/{m}) by A8,RELAT_1:120
.=E.:(d\X) by A14,XBOOLE_1:41;
then A28: A1/\A2=A\E.:(d\X) by XBOOLE_1:53;
conv(A\E.:(d\Xm))=meet Um by A4,A5,A13,A15,A19;
then conv(A\E.:(d\X))=meet Um/\meet CC by A28,A27,SETFAM_1:10
.=meet(Um\/CC) by A20,SETFAM_1:9;
hence thesis by A25,A22,XBOOLE_0:def 10;
end;
end;
A29: P[0];
for i be Nat holds P[i] from NAT_1:sch 2(A29,A3);
then A30: P[card(d\X)];
d\(d\X)=d/\X by XBOOLE_1:48;
then E.:X=E.:(d\(d\X)) by RELAT_1:112
.=E.:d\E.:(d\X) by FUNCT_1:64
.=A\E.:(d\X) by A2,RELAT_1:113;
hence thesis by A1,A30;
end;
reserve A for Subset of TOP-REAL n;
theorem Th13:
for a be bounded Subset of Euclid n st a=A
for p be Point of Euclid n st p in conv A holds
conv A c= cl_Ball(p,diameter a)
proof
A1: the TopStruct of TOP-REAL n=TopSpaceMetr Euclid n by EUCLID:def 8;
let a be bounded Subset of Euclid n
such that
A2: A=a;
let x be Point of Euclid n such that
A3: x in conv A;
A4: A c=cl_Ball(x,diameter a)
proof
let p be object;
assume A5: p in A;
then reconsider p as Point of Euclid n by A2;
reconsider pp=p as Point of TOP-REAL n by A1;
A6: cl_Ball(p,diameter a)=cl_Ball(pp,diameter a) by TOPREAL9:14;
A c=cl_Ball(p,diameter a)
proof
let y be object;
assume A7: y in A;
then reconsider q=y as Point of Euclid n by A2;
dist(p,q)<=diameter a by A2,A5,A7,TBSP_1:def 8;
hence thesis by METRIC_1:12;
end;
then conv A c=cl_Ball(pp,diameter a) by A6,CONVEX1:30;
then dist(p,x)<=diameter a by A3,A6,METRIC_1:12;
hence thesis by METRIC_1:12;
end;
reconsider xx=x as Point of TOP-REAL n by A1;
cl_Ball(x,diameter a)=cl_Ball(xx,diameter a) by TOPREAL9:14;
hence thesis by A4,CONVEX1:30;
end;
theorem Th14:
A is bounded iff conv A is bounded
proof
the TopStruct of TOP-REAL n=TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider cA=conv A,a=A as Subset of Euclid n;
hereby assume A is bounded;
then reconsider a as bounded Subset of Euclid n by JORDAN2C:11;
set D=diameter a;
A1: now let x,y be Point of Euclid n;
assume x in cA;
then A2: conv A c=cl_Ball(x,D) by Th13;
assume y in cA;
then dist(x,y)<=D by A2,METRIC_1:12;
hence dist(x,y)<=D+1 by XREAL_1:39;
end;
D>=0 by TBSP_1:21;
then cA is bounded by A1;
hence conv A is bounded by JORDAN2C:11;
end;
assume conv A is bounded;
then cA is bounded by JORDAN2C:11;
then a is bounded by CONVEX1:41,TBSP_1:14;
hence thesis by JORDAN2C:11;
end;
theorem Th15:
for a,ca be bounded Subset of Euclid n st ca = conv A & a = A holds
diameter a = diameter ca
proof
let a,ca be bounded Subset of Euclid n;
assume that
A1: ca=conv A and
A2: a=A;
per cases;
suppose a is empty;
hence thesis by A1,A2;
end;
suppose A3: a is non empty;
now let x,y be Point of Euclid n;
assume x in ca;
then A4: conv A c=cl_Ball(x,diameter a) by A1,A2,Th13;
assume y in ca;
hence dist(x,y)<=diameter a by A1,A4,METRIC_1:12;
end;
then A5: diameter ca<=diameter a by A1,A2,A3,TBSP_1:def 8;
diameter a<=diameter ca by A1,A2,CONVEX1:41,TBSP_1:24;
hence thesis by A5,XXREAL_0:1;
end;
end;
registration
let n;
let K be bounded SimplicialComplexStr of TOP-REAL n;
cluster -> bounded for SubdivisionStr of K;
coherence
proof
let SK be SubdivisionStr of K;
consider r be Real such that
A1: for A be Subset of Euclid n st A in the topology of K holds A is bounded
& diameter A<=r by Def2;
take r;
let A be Subset of Euclid n;
assume A2: A in the topology of SK;
then reconsider a=A as Subset of SK;
a is simplex-like by A2,PRE_TOPC:def 2;
then consider b be Subset of K such that
A3: b is simplex-like and
A4: conv@a c=conv@b by SIMPLEX1:def 4;
A5: [#]TOP-REAL n=[#]Euclid n by Lm1;
then reconsider cA=conv@a as Subset of Euclid n;
[#]K c=[#]TOP-REAL n by SIMPLEX0:def 9;
then reconsider B=b as Subset of Euclid n by A5,XBOOLE_1:1;
A6: B in the topology of K by A3,PRE_TOPC:def 2;
then A7: diameter B<=r by A1;
A8: B is bounded by A1,A6;
then @b is bounded by JORDAN2C:11;
then conv@b is bounded by Th14;
then reconsider cB=conv@b as bounded Subset of Euclid n by JORDAN2C:11;
A9: diameter cA<=diameter cB by A4,TBSP_1:24;
cA c=cB by A4;
then A10: cA is bounded by TBSP_1:14;
then A is bounded by CONVEX1:41,TBSP_1:14;
then A11: diameter cA=diameter A by A10,Th15;
diameter cB=diameter B by A8,Th15;
hence thesis by A9,A10,A11,A7,CONVEX1:41,TBSP_1:14,XXREAL_0:2;
end;
end;
theorem Th16:
for K be bounded finite-degree non void SimplicialComplex of TOP-REAL n st
|.K.| c= [#]K
holds diameter BCS K <= degree K/(degree K+1) * diameter K
proof
set T=TOP-REAL n;
let K be bounded finite-degree non void SimplicialComplex of T;
set BK=BCS K;
set cM=center_of_mass T;
set dK=degree K;
assume |.K.|c=[#]K;
then A1: BCS K=subdivision(cM,K) by SIMPLEX1:def 5;
for A be Subset of Euclid n st A is Simplex of BK holds diameter A<=dK/(dK+1)
*diameter K
proof
let A be Subset of Euclid n;
reconsider ONE=1 as ExtReal;
assume A2: A is Simplex of BK;
then reconsider a=A as Simplex of BK;
consider S be c=-linear finite simplex-like Subset-Family of K such that
A3: A=cM.:S by A1,A2,SIMPLEX0:def 20;
A4: A is bounded by A2,Th5;
reconsider s=@S as c=-linear finite finite-membered Subset-Family of T;
set Us=union s;
set C=Complex_of{Us};
union S is empty or union S in S by SIMPLEX0:9,ZFMISC_1:2;
then A5: union S is simplex-like by TOPS_2:def 1;
then A6: card union S<=degree K+ONE by SIMPLEX0:24;
A7: diameter K>=0 by Th7;
A8: not{} in dom cM by ORDERS_1:1;
then A9: dom cM is with_non-empty_elements by SETFAM_1:def 8;
A10: [#]T=[#]Euclid n by Lm1;
then reconsider US=Us as Subset of Euclid n;
A11: a in the topology of BK by PRE_TOPC:def 2;
per cases;
suppose K is empty-membered;
then A12: dK=-1 by SIMPLEX0:22;
then -1<=degree BK & degree BK<=-1 by A1,A9,SIMPLEX0:23,52;
then degree BK=-1 by XXREAL_0:1;
then BK is empty-membered by SIMPLEX0:22;
then the topology of BK is empty-membered;
then A13: a={} by A11,SETFAM_1:def 10;
dK/(dK+1)=0 by A12;
hence thesis by A13,TBSP_1:def 8;
end;
suppose K is non empty-membered;
then degree K>=-1 & dK<>-1 by SIMPLEX0:22,23;
then dK>-1 by XXREAL_0:1;
then A14: dK>=-1+1 by INT_1:7;
then A15: dK/(dK+1)*diameter K>=0 by A7;
per cases;
suppose a is empty;
hence thesis by A15,TBSP_1:def 8;
end;
suppose A16: a is non empty;
now US is bounded;
then Us is bounded by JORDAN2C:11;
then conv Us is bounded by Th14;
then reconsider cUs=conv Us as bounded Subset of Euclid n by JORDAN2C:11;
let x,y be Point of Euclid n;
assume that
A17: x in A and
A18: y in A;
reconsider X=x,Y=y as Element of T by A10;
A19: |.BCS C.|=|.C.| & |.C.|=conv Us by SIMPLEX1:8,10;
consider p be object such that
A20: p in dom cM and
A21: p in s and
cM.p=x by A3,A17,FUNCT_1:def 6;
reconsider p as set by TARSKI:1;
p c=Us by A21,ZFMISC_1:74;
then A22: Us<>{} by A8,A20;
card Us<=dK+1 by A6,XXREAL_3:def 2;
then A23: (dK+1)"<=(card Us)" by A22,XREAL_1:85;
A24: diameter US<=diameter K by A5,Def4;
A25: (card Us-1)/card Us=card Us/card Us-(1/card Us)
.=1-(1/card Us) by A22,XCMPLX_1:60;
A26: diameter cUs=diameter US by Th15;
consider b1,b2 be VECTOR of T,r be Real such that
A27: b1 in Vertices BCS C and
A28: b2 in Vertices BCS C and
A29: X-Y=r*(b1-b2) and
A30: 0<=r and
A31: r<=(card Us-1)/card Us by A3,A16,A17,A18,Th11;
reconsider B1=b1,B2=b2 as Element of BCS C by A27,A28;
B1 is vertex-like by A27,SIMPLEX0:def 4;
then consider S1 be Subset of BCS C such that
A32: S1 is simplex-like and
A33: B1 in S1;
A34: conv@S1 c=|.BCS C.| by A32,SIMPLEX1:5;
B2 is vertex-like by A28,SIMPLEX0:def 4;
then consider S2 be Subset of BCS C such that
A35: S2 is simplex-like and
A36: B2 in S2;
@S2 c=conv@S2 by CONVEX1:41;
then A37: B2 in conv@S2 by A36;
@S1 c=conv@S1 by CONVEX1:41;
then A38: B1 in conv@S1 by A33;
reconsider bb1=b1,bb2=b2 as Point of Euclid n by A10;
dK/(dK+1)=(dK+1)/(dK+1)-(1/(dK+1))
.=1-(1/(dK+1)) by A14,XCMPLX_1:60;
then (card Us-1)/card Us<=dK/(dK+1) by A23,A25,XREAL_1:10;
then A39: dist(bb1,bb2)>=0 & r<=dK/(dK+1) by A31,XXREAL_0:2;
conv@S2 c=|.BCS C.| by A35,SIMPLEX1:5;
then dist(bb1,bb2)<=diameter US by A19,A26,A38,A37,A34,TBSP_1:def 8;
then A40: dist(bb1,bb2)<=diameter K by A24,XXREAL_0:2;
dist(x,y)=|.x-y.| by EUCLID:def 6
.=|.X-Y.|
.=|.r*(bb1-bb2).| by A29
.=|.r.|*|.bb1-bb2.| by EUCLID:11
.=r*|.bb1-bb2.| by A30,ABSVALUE:def 1
.=r*dist(bb1,bb2) by EUCLID:def 6;
hence dist(x,y)<=dK/(dK+1)*diameter K by A30,A40,A39,XREAL_1:66;
end;
hence thesis by A4,A16,TBSP_1:def 8;
end;
end;
end;
hence thesis by Def4;
end;
theorem Th17:
for K be bounded finite-degree non void SimplicialComplex of TOP-REAL n st
|.K.| c= [#]K
holds diameter BCS(k,K) <= (degree K/(degree K+1))|^k * diameter K
proof
let K be bounded finite-degree non void SimplicialComplex of TOP-REAL n;
set dK=degree K;
set ddK=dK/(dK+1);
defpred P[Nat] means
diameter BCS($1,K)<=ddK|^$1*diameter K & BCS($1,K) is finite-degree & degree
BCS($1,K)<=dK;
assume A1: |.K.|c=[#]K;
A2: for k st P[k] holds P[k+1]
proof
let k;
set T=TOP-REAL n;
set B=BCS(k,K);
set cM=center_of_mass T;
A3: degree K>=-1 by SIMPLEX0:23;
assume A4: P[k];
then reconsider B=BCS(k,K) as bounded finite-degree non void
SimplicialComplex of TOP-REAL n;
set dB=degree B;
A5: degree B>=-1 by SIMPLEX0:23;
A6: 0<=diameter K by Th7;
A7: 0<=diameter B by Th7;
A8: |.B.|=|.K.| & [#]B=[#]K by A1,SIMPLEX1:18,19;
then A9: BCS B=subdivision(cM,B) by A1,SIMPLEX1:def 5;
A10: BCS(k+1,K)=BCS B by A1,SIMPLEX1:20;
then A11: diameter BCS(k+1,K)<=dB/(dB+1)*diameter B by A1,A8,Th16;
not{} in dom cM by ORDERS_1:1;
then dom cM is with_non-empty_elements by SETFAM_1:def 8;
then A12: degree BCS(k+1,K)<=dB by A9,A10,SIMPLEX0:52;
per cases;
suppose dB=-1 or dB=0;
then A13: dB/(dB+1)=0;
per cases;
suppose dK=0 or dK=-1;
then dK/(dK+1)=0;
then 0=(dK/(dK+1))|^(k+1) by NAT_1:11,NEWTON:11;
hence thesis by A1,A4,A9,A11,A12,A13,SIMPLEX1:20,XXREAL_0:2;
end;
suppose A14: dK<>0 & dK<>-1;
then dK>-1 by A3,XXREAL_0:1;
then dK>=-1+1 by INT_1:7;
then ddK>0 by A14,XREAL_1:139;
then ddK|^(k+1)>0 by NEWTON:83;
hence thesis by A1,A4,A6,A9,A11,A12,A13,SIMPLEX1:20,XXREAL_0:2;
end;
end;
suppose dB<>-1 & dB<>0;
then dB>-1 by A5,XXREAL_0:1;
then A15: dB>=-1+1 by INT_1:7;
A16: dB/(dB+1)=(dB+1)/(dB+1)-(1/(dB+1))
.=1-(1/(dB+1)) by A15,XCMPLX_1:60;
A17: ddK=(dK+1)/(dK+1)-(1/(dK+1))
.=1-(1/(dK+1)) by A4,A15,XCMPLX_1:60;
dB+1<=dK+1 by A4,XREAL_1:6;
then 1/(dK+1)<=1/(dB+1) by A15,XREAL_1:85;
then degree B/(degree B+1)<=dK/(dK+1) by A16,A17,XREAL_1:10;
then A18: degree B/(degree B+1)*diameter B<=dK/(dK+1)*((dK/(dK+1))|^k*
diameter K) by A4,A7,A15,XREAL_1:66;
dK/(dK+1)*((dK/(dK+1))|^k*diameter K)=dK/(dK+1)*(dK/(dK+1))|^k*(diameter K)
.=(dK/(dK+1))|^(k+1)*(diameter K) by NEWTON:6;
hence thesis by A1,A4,A9,A11,A12,A18,SIMPLEX1:20,XXREAL_0:2;
end;
end;
ddK|^(0 qua Nat)=1 by NEWTON:4;
then A19: P[0] by A1,SIMPLEX1:16;
for k holds P[k] from NAT_1:sch 2(A19,A2);
hence thesis;
end;
theorem Th18:
for K be bounded finite-degree non void SimplicialComplex of TOP-REAL n st
|.K.| c= [#]K for r st r>0 ex k st diameter BCS(k,K) < r
proof
let K be bounded finite-degree non void SimplicialComplex of TOP-REAL n such
that
A1: |.K.|c=[#]K;
set dK=degree K;
let r be Real such that
A2: r>0;
set ddK=dK/(dK+1);
per cases;
suppose dK=0 or dK=-1;
then A3: ddK=0;
diameter BCS K<=ddK*diameter K & BCS K=BCS(1,K) by A1,Th16,SIMPLEX1:17;
hence thesis by A2,A3;
end;
suppose A4: diameter K=0;
K=BCS(0,K) by A1,SIMPLEX1:16;
hence thesis by A2,A4;
end;
suppose A5: dK<>0 & dK<>-1 & diameter K<>0;
dK>=-1 by SIMPLEX0:23;
then dK>-1 by A5,XXREAL_0:1;
then A6: dK>=-1+1 by INT_1:7;
then A7: ddK>0 by A5,XREAL_1:139;
dK+1>dK by XREAL_1:29;
then A8: ddK<1 by A6,XREAL_1:189;
A9: diameter K>0 by A5,Th7;
then r/diameter K>0 by A2,XREAL_1:139;
then consider k be Nat such that
A10: ddK to_power k<r/diameter K by A7,A8,TBSP_1:3;
A11: r/diameter K*diameter K=r by A5,XCMPLX_1:87;
A12: diameter BCS(k,K)<=ddK|^k*diameter K by A1,Th17;
ddK to_power k=ddK|^k by POWER:41;
then ddK|^k*diameter K<r by A9,A10,A11,XREAL_1:68;
then diameter BCS(k,K)<r by A12,XXREAL_0:2;
hence thesis;
end;
end;
theorem Th19:
for i,j be Element of NAT
ex f be Function of[:TOP-REAL i,TOP-REAL j:],TOP-REAL(i+j) st
f is being_homeomorphism &
for fi be Element of TOP-REAL i,fj be Element of TOP-REAL j
holds f.(fi,fj) = fi^fj
proof
let i,j be Element of NAT;
set TRi=TOP-REAL i,TRj=TOP-REAL j,TRij=TOP-REAL(i+j);
set tri=the TopStruct of TRi,trj=the TopStruct of TRj,trij=the TopStruct of
TRij;
A1: trj=TopSpaceMetr Euclid j by EUCLID:def 8;
trij=TopSpaceMetr Euclid(i+j) & tri=TopSpaceMetr Euclid i by EUCLID:def 8;
then consider f be Function of[:tri,trj:],trij such that
A2: f is being_homeomorphism and
A3: for fi,fj be FinSequence st[fi,fj] in dom f holds f.(fi,fj)=fi^fj by A1,
TOPREAL7:26;
rng f=[#]trij by A2,TOPS_2:60;
then A4: rng f=[#]TRij;
A5: [#][:TRi,TRj:]=[:[#]TRi,[#]TRj:] by BORSUK_1:def 2;
A6: [:TRi,TRj:]=[:TRi,TRj:]|([#][:TRi,TRj:]) by TSEP_1:3
.=[:TRi|([#]TRi),TRj|([#]TRj):] by A5,BORSUK_3:22
.=[:tri,TRj|([#]TRj):] by TSEP_1:93
.=[:tri,trj:] by TSEP_1:93;
then reconsider F=f as Function of[:TRi,TRj:],TRij;
A7: now let P be Subset of[:TRi,TRj:];
thus F.:(Cl P)=Cl(f.:P) by A2,A6,TOPS_2:60
.=Cl(F.:P) by TOPS_3:80;
end;
take F;
A8: F is one-to-one by A2,TOPS_2:60;
dom F=[#][:TRi,TRj:] by A2,A6,TOPS_2:60;
hence F is being_homeomorphism by A4,A7,A8,TOPS_2:60;
let fi be Element of TOP-REAL i,fj be Element of TOP-REAL j;
dom F=[:[#]TRi,[#]TRj:] by A5,FUNCT_2:def 1;
then [fi,fj] in dom F by ZFMISC_1:87;
hence thesis by A3;
end;
Lm3: for n be Nat holds [#]TOP-REAL n=[#]TopSpaceMetr Euclid n
proof
let n be Nat;
the TopStruct of TOP-REAL n=TopSpaceMetr Euclid n by EUCLID:def 8;
hence thesis;
end;
theorem Th20:
for i,j be Element of NAT
for f be Function of [:TOP-REAL i,TOP-REAL j:],TOP-REAL(i+j) st
for fi be Element of TOP-REAL i,fj be Element of TOP-REAL j
holds f.(fi,fj) = fi^fj
for r for fi be Point of Euclid i,fj be Point of Euclid j,
fij be Point of Euclid(i+j) st fij = fi^fj
holds f.:[:OpenHypercube(fi,r),OpenHypercube(fj,r):] = OpenHypercube(fij,r)
proof
let i,j be Element of NAT;
let f be Function of[:TOP-REAL i,TOP-REAL j:],TOP-REAL(i+j) such that
A1: for fi be Element of TOP-REAL i,fj be Element of TOP-REAL j holds f.(fi,
fj)=fi^fj;
let r be Real,fi be Point of Euclid i,fj be Point of Euclid j,fij be
Point of Euclid(i+j) such that
A2: fij=fi^fj;
set Ii=Intervals(fi,r),Ij=Intervals(fj,r),Iij=Intervals(fij,r);
A3: OpenHypercube(fi,r)=product Ii by EUCLID_9:def 4;
A4: [#]TOP-REAL i=[#]TopSpaceMetr Euclid i by Lm3;
A5: [#]TOP-REAL j=[#]TopSpaceMetr Euclid j by Lm3;
A6: OpenHypercube(fj,r)=product Ij by EUCLID_9:def 4;
A7: Ii^Ij=Iij by A2,RLAFFIN3:1;
A8: f.:[:product Ii,product Ij:]c=product Iij
proof
let y be object;
assume y in f.:[:product Ii,product Ij:];
then consider x be object such that
x in dom f and
A9: x in [:product Ii,product Ij:] and
A10: f.x=y by FUNCT_1:def 6;
consider xi,xj be object such that
A11: xi in product Ii and
A12: xj in product Ij and
A13: x=[xi,xj] by A9,ZFMISC_1:def 2;
reconsider xi as Element of TOP-REAL i by A3,A4,A11;
reconsider xj as Element of TOP-REAL j by A5,A6,A12;
y=f.(xi,xj) by A10,A13,BINOP_1:def 1
.=xi^xj by A1;
hence y in product Iij by A7,A11,A12,RLAFFIN3:2;
end;
A14: product Iij c=f.:[:product Ii,product Ij:]
proof
let y be object;
assume y in product Iij;
then consider p1,p2 be FinSequence such that
A15: y=p1^p2 and
A16: p1 in product Ii & p2 in product Ij by A7,RLAFFIN3:2;
A17: [p1,p2] in [:product Ii,product Ij:] by A16,ZFMISC_1:87;
[p1,p2] in [:[#]TOP-REAL i,[#]TOP-REAL j:] by A3,A5,A4,A6,A16,ZFMISC_1:87;
then [p1,p2] in [#][:TOP-REAL i,TOP-REAL j:];
then A18: [p1,p2] in dom f by FUNCT_2:def 1;
y=f.(p1,p2) by A1,A3,A5,A4,A6,A15,A16
.=f. [p1,p2] by BINOP_1:def 1;
hence thesis by A17,A18,FUNCT_1:def 6;
end;
OpenHypercube(fij,r)=product Iij by EUCLID_9:def 4;
hence thesis by A3,A6,A8,A14,XBOOLE_0:def 10;
end;
theorem Th21:
A is bounded iff ex p be Point of Euclid n,r st A c= OpenHypercube(p,r)
proof
reconsider B=A as Subset of Euclid n by TOPREAL3:8;
thus A is bounded implies ex p be Point of Euclid n,r be Real st A c=
OpenHypercube(p,r)
proof
assume A is bounded;
then A1: B is bounded by JORDAN2C:11;
per cases;
suppose A2: A is empty;
take p=the Point of Euclid n,r=the Real;
thus thesis by A2;
end;
suppose A is non empty;
then consider p be object such that
A3: p in B by XBOOLE_0:def 1;
reconsider p as Element of Euclid n by A3;
consider r be Real such that
0<r and
A4: for x,y being Point of Euclid n st x in B & y in B holds dist(x,y)<=r
by A1;
take p,r1=r+1;
A5: B c=Ball(p,r1)
proof
let x be object;
assume A6: x in B;
then reconsider x as Element of Euclid n;
dist(p,x)<r1 by A3,A4,A6,XREAL_1:39;
hence thesis by METRIC_1:11;
end;
Ball(p,r1)c=OpenHypercube(p,r1) by EUCLID_9:22;
hence A c=OpenHypercube(p,r1) by A5;
end;
end;
given p be Point of Euclid n,r be Real such that
A7: A c= OpenHypercube(p,r);
per cases;
suppose n=0; then
OpenHypercube(p,r) = {{}} by EUCLID_9:12; then
B = {} or B = {0} by A7,ZFMISC_1:33;
hence thesis by JORDAN2C:11;
end;
suppose n<>0;
then OpenHypercube(p,r)c=Ball(p,r*sqrt(n)) by EUCLID_9:18;
then B is bounded by A7,TBSP_1:14,XBOOLE_1:1;
hence thesis by JORDAN2C:11;
end;
end;
Lm4: for A be Subset of TOP-REAL 1 holds A is closed & A is bounded implies A
is compact
proof
set TR1=TOP-REAL 1;
let A be Subset of TR1 such that
A1: A is closed and
A2: A is bounded;
consider r be Real such that
A3: for q be Point of TR1 st q in A holds|.q.|<r by A2,JORDAN2C:34;
reconsider L=[.-r,r.] as Subset of R^1 by TOPMETR:17;
consider f be Function of TR1,R^1 such that
A4: for p be Element of TR1 holds f.p=p/.1 by JORDAN2B:1;
A5: f is being_homeomorphism by A4,JORDAN2B:28;
then reconsider F=f as one-to-one Function by TOPS_2:def 5;
rng f=[#]R^1 by A5,TOPS_2:def 5;
then f is onto by FUNCT_2:def 3;
then f/"=F" by TOPS_2:def 4;
then A6: (f/").:L=F"L by FUNCT_1:85;
A7: dom f=[#]TR1 by A5,TOPS_2:def 5;
A8: A c=F"L
proof
let x be object;
assume A9: x in A;
then reconsider v=x as Element of TR1;
set v1=v.1;
A10: len v=1 by CARD_1:def 7;
then v=<*v1*> by FINSEQ_1:40;
then A11: |.v.|=|.v1.| by TOPREALC:18;
|.v.|<r by A3,A9;
then v1<=r & -r<=v1 by A11,ABSVALUE:5;
then A12: v1 in L by XXREAL_1:1;
1 in Seg 1 & dom v=Seg 1 by A10,FINSEQ_1:1,def 3;
then A13: v/.1=v1 by PARTFUN1:def 6;
f.v=v/.1 by A4;
hence thesis by A7,A12,A13,FUNCT_1:def 7;
end;
[.-r,r.] is compact by RCOMP_1:6;
then A14: L is compact by JORDAN5A:25;
f" is continuous by A5,TOPS_2:def 5;
then (f/").:L is compact by A14,WEIERSTR:8;
hence thesis by A1,A6,A8,COMPTS_1:9;
end;
Lm5: for A be Subset of TOP-REAL n holds A is closed & A is bounded implies A
is compact
proof
defpred P[Nat] means
for A be Subset of TOP-REAL$1 holds A is closed & A is bounded implies A is
compact;
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A2: P[n];
per cases;
suppose n=0;
hence thesis by Lm4;
end;
suppose A3: n<>0;
set n1=n+1;
set TR1=TOP-REAL 1;
set TRn=TOP-REAL n;
set TRn1=TOP-REAL n1;
let A be Subset of TRn1;
assume that
A4: A is closed and
A5: A is bounded;
consider p be Point of Euclid n1,r be Real such that
A6: A c=OpenHypercube(p,r) by A5,Th21;
n in NAT by ORDINAL1:def 12;
then consider f be Function of[:TRn,TR1:],TRn1 such that
A7: f is being_homeomorphism and
A8: for fi be Element of TRn,fj be Element of TR1 holds f.(fi,fj)=fi^fj
by Th19;
A9: f is one-to-one & dom f=[#][:TRn,TR1:] by A7,TOPGRP_1:24;
len p=n1 by CARD_1:def 7;
then consider q1,q2 be FinSequence such that
A10: len q1=n and
A11: len q2=1 and
A12: p=q1^q2 by FINSEQ_2:22;
A14: q1 is FinSequence of REAL by A12,FINSEQ_1:36;
A15: q2 is FinSequence of REAL by A12,FINSEQ_1:36;
reconsider q1 as Element of Euclid n by A10,A14,TOPREAL3:45;
reconsider q2 as Element of Euclid 1 by A11,A15,TOPREAL3:45;
A16: f is continuous by A7,TOPS_2:def 5;
reconsider Bn=cl_Ball(q1,r*sqrt(n)) as Subset of TRn by TOPREAL3:8;
reconsider B1=cl_Ball(q2,r*sqrt(1)) as Subset of TR1 by TOPREAL3:8;
Ball(q2,r*sqrt(1))c=B1 & OpenHypercube(q2,r)c=Ball(q2,r*sqrt(1)) by
EUCLID_9:18,METRIC_1:14;
then A17: OpenHypercube(q2,r)c=B1;
Ball(q1,r*sqrt(n))c=Bn & OpenHypercube(q1,r)c=Ball(q1,r*sqrt(n)) by A3,
EUCLID_9:18,METRIC_1:14;
then OpenHypercube(q1,r)c=Bn;
then A18: [:OpenHypercube(q1,r),OpenHypercube(q2,r):]c=[:Bn,B1:] by A17,
ZFMISC_1:96;
cl_Ball(q2,r*sqrt(1)) is bounded by TOPREAL6:59;
then B1 is bounded by JORDAN2C:11;
then A19: B1 is compact by Lm4,TOPREAL6:58;
cl_Ball(q1,r*sqrt(n)) is bounded by TOPREAL6:59;
then Bn is bounded by JORDAN2C:11;
then Bn is compact by A2,TOPREAL6:58;
then A20: [:Bn,B1:] is compact Subset of[:TRn,TR1:] by A19,BORSUK_3:23;
rng f=[#]TRn1 by A7,TOPGRP_1:24;
then A21: f.:(f"A)=A by FUNCT_1:77;
f.:[:OpenHypercube(q1,r),OpenHypercube(q2,r):]=OpenHypercube(p,r) by A8,A10
,A12,Th20;
then A22: f"A c=[:OpenHypercube(q1,r),OpenHypercube(q2,r):] by A6,A9,A21,
FUNCT_1:87;
f"A is closed by A4,A7,TOPGRP_1:24;
then f"A is compact by A18,A20,A22,COMPTS_1:9,XBOOLE_1:1;
hence thesis by A16,A21,WEIERSTR:8;
end;
end;
A23: P[0];
for n holds P[n] from NAT_1:sch 2(A23,A1);
hence thesis;
end;
registration
let n;
cluster closed bounded -> compact for Subset of TOP-REAL n;
coherence by Lm5;
end;
registration
let n;
let A be affinely-independent Subset of TOP-REAL n;
cluster conv A -> compact;
coherence
proof
n in NAT by ORDINAL1:def 12;
then conv A is bounded by Th14;
hence thesis;
end;
end;
begin :: Main Theorems
theorem Th22:
for A be non empty affinely-independent Subset of TOP-REAL n
for E be Enumeration of A
for F be FinSequence of bool the carrier of ((TOP-REAL n)|(conv A)) st
len F = card A & rng F is closed &
for S be Subset of dom F holds conv(E.:S) c= union(F.:S)
holds meet rng F is non empty
proof
set TRn=TOP-REAL n;
let A be non empty affinely-independent Subset of TRn;
set cA=conv A;
let E be Enumeration of A;
let F be FinSequence of bool the carrier of(TRn|cA) such that
A1: len F=card A and
A2: rng F is closed and
A3: for S be Subset of dom F holds conv(E.:S)c=union(F.:S);
A4: F<>{} by A1;
A5: rng E=A by RLAFFIN3:def 1;
then len E=card A by FINSEQ_4:62;
then A6: dom E=dom F by A1,FINSEQ_3:29;
set En=Euclid n;
set Comp=Complex_of{A};
defpred P[object,object] means
$1 in F.(E".$2) & for B be Subset of TRn st B c=A & $1 in conv B holds$2 in
B;
A7: TopSpaceMetr En=the TopStruct of TRn by EUCLID:def 8;
then reconsider CA=cA as non empty Subset of TopSpaceMetr En;
reconsider ca=cA as non empty Subset of En by A7;
A8: (TopSpaceMetr En)|CA=TopSpaceMetr(En|ca) by HAUSDORF:16;
then reconsider CrF=COMPLEMENT(rng F) as Subset-Family of TopSpaceMetr(En|ca)
by A7,PRE_TOPC:36;
CA is compact by A7,COMPTS_1:23;
then A9: TopSpaceMetr(En|ca) is compact by A8,COMPTS_1:3;
A10: (TopSpaceMetr En)|CA=TRn|cA by A7,PRE_TOPC:36;
assume meet rng F is empty;
then [#](TRn|cA)=(meet rng F)`
.=union CrF by A4,TOPS_2:7;
then A11: CrF is Cover of TopSpaceMetr(En|ca) by A8,A10,SETFAM_1:45;
set L=the Lebesgue_number of CrF;
A12: |.Comp.|c=[#]Comp;
then consider k be Nat such that
A13: diameter BCS(k,Comp)<L by Th18;
set Bcs=BCS(k,Comp);
A14: |.Bcs.|=|.Comp.| by A12,SIMPLEX1:19;
A15: the topology of Comp=bool A by SIMPLEX0:4;
A16: for x be object st x in Vertices Bcs
ex y be object st y in A & P[x,y]
proof
let x be object;
assume A17: x in Vertices Bcs;
then reconsider v=x as Element of Bcs;
v is vertex-like by A17,SIMPLEX0:def 4;
then consider S be Subset of Bcs such that
A18: S is simplex-like and
A19: v in S;
@S c=conv@S by RLAFFIN1:2;
then A20: v in conv@S by A19;
conv@S c=|.Comp.| by A14,A18,SIMPLEX1:5;
then consider W be Subset of Comp such that
A21: W is simplex-like and
A22: v in Int@W by A20,SIMPLEX1:6;
A23: v in conv@W by A22,RLAFFIN2:def 1;
A24: W in the topology of Comp by A21,PRE_TOPC:def 2;
then E"W c=dom E & E.:(E"W)=W by A5,A15,FUNCT_1:77,RELAT_1:132;
then conv@W c=union(F.:(E"W)) by A3,A6;
then consider Y be set such that
A25: v in Y and
A26: Y in F.:(E"W) by A23,TARSKI:def 4;
consider i be object such that
i in dom F and
A27: i in E"W and
A28: F.i=Y by A26,FUNCT_1:def 6;
take y=E.i;
A29: y in W by A27,FUNCT_1:def 7;
i in dom E by A27,FUNCT_1:def 7;
hence y in A & x in F.(E".y) by A15,A24,A25,A28,A29,FUNCT_1:34;
let B be Subset of TRn;
assume that
A30: B c=A and
A31: x in conv B;
reconsider b=B as Simplex of Comp by A15,A30,PRE_TOPC:def 2;
conv@b meets Int@W by A22,A31,XBOOLE_0:3;
then W c=b by A21,SIMPLEX1:26;
hence thesis by A29;
end;
consider G be Function of Vertices Bcs,A such that
A32: for x be object st x in Vertices Bcs holds P[x,G.x]
from FUNCT_2:sch 1(A16
);
A33: |.Comp.|=conv A by SIMPLEX1:8;
then Bcs is with_non-empty_element by A14,SIMPLEX1:7;
then for v be Vertex of Bcs,B be Subset of TRn st B c=A & v in conv B holds G
.v in B by A32;
then consider S be Simplex of card A-1,Bcs such that
A34: G.:S=A by SIMPLEX1:47;
A35: [#]Bcs=[#]Comp by A12,SIMPLEX1:18;
then reconsider SS=S as Subset of En by A7;
S is non empty by A34;
then consider s be object such that
A36: s in S by XBOOLE_0:def 1;
A37: conv@S c=cA by A14,A33,SIMPLEX1:5;
reconsider s as Point of En by A7,A35,A36;
A38: S c=conv@S by RLAFFIN1:2;
then s in conv@S by A36;
then reconsider ss=s as Point of En|ca by A37,TOPMETR:def 2;
A39: SS is bounded;
CrF is open by A2,A8,A10,TOPS_2:9;
then consider CRF be Subset of TopSpaceMetr(En|ca) such that
A40: CRF in CrF and
A41: Ball(ss,L)c=CRF by A9,A11,Def1;
CRF` in rng F by A8,A10,A40,SETFAM_1:def 7;
then consider i be object such that
A42: i in dom F and
A43: F.i=CRF` by FUNCT_1:def 3;
E.i in A by A5,A6,A42,FUNCT_1:def 3;
then consider w be object such that
A44: w in dom G and
A45: w in S and
A46: G.w=E.i by A34,FUNCT_1:def 6;
A47: w in conv@S by A38,A45;
A48: conv@S c=cA by A14,A33,SIMPLEX1:5;
then A49: [#](En|ca)=ca & w in cA by A47,TOPMETR:def 2;
reconsider SS=S as bounded Subset of En by A39;
diameter SS<=diameter BCS(k,Comp) by Def4;
then A50: diameter SS<L by A13,XXREAL_0:2;
w in F.(E".(G.w)) by A32,A44;
then A51: w in F.i by A6,A42,A46,FUNCT_1:34;
reconsider w as Point of En by A49;
reconsider ww=w as Point of En|ca by A47,A48,TOPMETR:def 2;
conv@S c=cl_Ball(s,diameter SS) by A36,A38,Th13;
then dist(s,w)=dist(ss,ww) & dist(s,w)<=diameter SS by A47,METRIC_1:12
,TOPMETR:def 1;
then dist(ss,ww)<L by A50,XXREAL_0:2;
then ww in Ball(ss,L) by METRIC_1:11;
hence contradiction by A41,A43,A51,XBOOLE_0:def 5;
end;
reserve A for affinely-independent Subset of TOP-REAL n;
theorem Th23:
for A st card A = n+1
for f be continuous Function of(TOP-REAL n)|conv A,(TOP-REAL n)|conv A
ex p be Point of TOP-REAL n st p in dom f & f.p=p
proof
set TRn=TOP-REAL n;
let A be affinely-independent Subset of TRn such that
A1: card A=n+1;
A2: A is non empty by A1;
set cA=conv A;
let f be continuous Function of TRn|cA,TRn|cA;
reconsider cA as non empty Subset of TRn by A2;
set T=TRn|cA;
reconsider ff=f as continuous Function of T,T;
set E=the Enumeration of A;
deffunc P(object)
={v where v is Element of T: |--(A,E.$1).(f.v)<=|--(A,E.$1).v};
consider F be FinSequence such that
A3: len F=card A & for k st k in dom F holds F.k=P(k) from FINSEQ_1:sch 2;
rng F c=bool the carrier of T
proof
let y be object;
assume y in rng F;
then consider x be object such that
A4: x in dom F and
A5: F.x=y by FUNCT_1:def 3;
A6: P(x)c=the carrier of T
proof
let z be object;
assume z in P(x);
then ex v be Element of T st z=v & |--(A,E.x).(f.v)<=|--(A,E.x).v;
hence thesis;
end;
F.x=P(x) by A3,A4;
hence thesis by A5,A6;
end;
then reconsider F as FinSequence of bool the carrier of T by FINSEQ_1:def 4;
A7: [#]T=cA by PRE_TOPC:def 5;
A8: dom f=the carrier of T by FUNCT_2:def 1;
now let W be Subset of T;
reconsider Z=0 as Real;
reconsider L=].-infty,Z.] as Subset of R^1 by TOPMETR:17;
assume W in rng F;
then consider i be object such that
A9: i in dom F and
A10: F.i=W by FUNCT_1:def 3;
reconsider AEi=|--(A,E.i) as continuous Function of TRn,R^1 by A1,
RLAFFIN3:32;
set AT=AEi|T;
set Af=AT*ff;
set AfT=Af-AT;
A11: dom AfT=the carrier of T by FUNCT_2:def 1;
reconsider AfT as Function of T,R^1 by TOPMETR:17;
A12: dom AT=the carrier of T by FUNCT_2:def 1;
A13: AT=AEi|the carrier of T by A7,TMAP_1:def 3;
A14: dom Af=the carrier of T by FUNCT_2:def 1;
A15: AfT"L c=P(i)
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume A16: x in AfT"L;
then reconsider v=x as Point of T;
x in dom AfT by A16,FUNCT_1:def 7;
then A17: AfT.x=Af.xx-AT.xx by VALUED_1:13;
AfT.x in L & Af.x=AT.(f.x) by A14,A16,FUNCT_1:12,def 7;
then AT.(f.xx)-AT.xx<=0 by A17,XXREAL_1:2;
then A18: AT.(f.x)<=AT.xx by XREAL_1:50;
f.x in dom AT by A14,A16,FUNCT_1:11;
then A19: AT.(f.x)=AEi.(f.v) by A13,FUNCT_1:47;
AT.x=AEi.v by A12,A13,FUNCT_1:47;
hence thesis by A18,A19;
end;
A20: P(i)c=AfT"L
proof
let x be object;
assume x in P(i);
then consider v be Element of T such that
A21: x=v and
A22: AEi.(f.v)<=AEi.v;
f.v in rng f by A8,FUNCT_1:def 3;
then A23: AEi.(f.v)=AT.(f.v) by A12,A13,FUNCT_1:47;
AEi.v=AT.v by A12,A13,FUNCT_1:47;
then Af.v<=AT.v by A14,A22,A23,FUNCT_1:12;
then Af.v-AT.v<=0 by XREAL_1:47;
then AfT.v<=0 by A11,VALUED_1:13;
then AfT.v in L by XXREAL_1:234;
hence thesis by A11,A21,FUNCT_1:def 7;
end;
L is closed by BORSUK_5:41;
then A24: AfT"L is closed by PRE_TOPC:def 6;
F.i=P(i) by A3,A9;
hence W is closed by A10,A15,A20,A24,XBOOLE_0:def 10;
end;
then A25: rng F is closed by TOPS_2:def 2;
A26: dom E=Seg len E by FINSEQ_1:def 3;
A27: conv A c=Affin A by RLAFFIN1:65;
A28: rng E=A by RLAFFIN3:def 1;
then len E=card A by FINSEQ_4:62;
then A29: dom F=dom E by A3,FINSEQ_3:29;
for S be Subset of dom F holds conv(E.:S)c=union(F.:S)
proof
let S be Subset of dom F;
set ES=E.:S;
per cases;
suppose S is empty;
then conv ES is empty;
hence thesis;
end;
suppose A30: S is non empty;
let x be object;
set fx=f.x,xES=x|--ES,fxA=fx|--A,xA=x|--A;
assume A31: x in conv ES;
A32: conv ES c=conv A by A28,RELAT_1:111,RLAFFIN1:3;
then reconsider v=x as Point of T by A7,A31;
A33: len(fxA*E)=len E by FINSEQ_2:33;
A34: len E=len(xES*E) by FINSEQ_2:33;
then reconsider fxAE=fxA*E,xESE=xES*E as Element of len E-tuples_on REAL
by A33,FINSEQ_2:92;
A35: dom fxAE=Seg len E by A33,FINSEQ_1:def 3;
A36: conv ES c=Affin ES by RLAFFIN1:65;
then A37: xA=xES by A28,A31,RELAT_1:111,RLAFFIN1:77;
A38: ES c=A by A28,RELAT_1:111;
A39: Carrier xES c=ES by RLVECT_2:def 6;
ES is affinely-independent by A28,RELAT_1:111,RLAFFIN1:43;
then sum xES=1 & Carrier xES c= A by A31,A36,A38,A39,RLAFFIN1:def 7;
then A40: Carrier fxA c=A & 1=Sum(xES*E) by A28,RLAFFIN1:30,RLVECT_2:def 6;
A41: fx in rng f by A7,A8,A31,A32,FUNCT_1:def 3;
then A42: fx in conv A by A7;
then sum fxA=1 by A27,RLAFFIN1:def 7;
then A43: Sum fxAE=Sum xESE by A28,A40,RLAFFIN1:30;
A44: dom xESE=Seg len E by A34,FINSEQ_1:def 3;
per cases by A43,RVSUM_1:83;
suppose ex j be Nat st j in Seg len E & fxAE.j<xESE.j;
then consider j be Nat such that
A45: j in Seg len E and
A46: fxAE.j<xESE.j;
A47: fxAE.j=fxA.(E.j) by A35,A45,FUNCT_1:12;
A48: xESE.j=xES.(E.j) by A44,A45,FUNCT_1:12;
then xESE.j=|--(A,E.j).x by A31,A37,RLAFFIN3:def 3;
then A49: |--(A,E.j).(f.v)<=|--(A,E.j).v by A42,A46,A47,RLAFFIN3:def 3;
A50: E.j in dom fxA by A35,A45,FUNCT_1:11;
then 0<xES.(E.j) by A7,A41,A46,A47,A48,RLAFFIN1:71;
then E.j in Carrier xES by A50,RLVECT_2:19;
then consider i be object such that
A51: i in dom E and
A52: i in S and
A53: E.i=E.j by A39,FUNCT_1:def 6;
i=j by A26,A45,A51,A53,FUNCT_1:def 4;
then A54: F.j in F.:S by A52,FUNCT_1:def 6;
P(j)=F.j by A3,A26,A29,A45;
then x in F.j by A49;
hence thesis by A54,TARSKI:def 4;
end;
suppose A55: for j be Nat st j in Seg len E holds fxAE.j<=xESE.j;
consider j be object such that
A56: j in S by A30,XBOOLE_0:def 1;
reconsider j as Nat by A56;
A57: fxAE.j<=xESE.j by A26,A29,A55,A56;
A58: P(j)=F.j by A3,A56;
xESE.j=xES.(E.j) by A26,A29,A44,A56,FUNCT_1:12;
then A59: xESE.j=|--(A,E.j).x by A31,A37,RLAFFIN3:def 3;
fxAE.j=fxA.(E.j) by A26,A29,A35,A56,FUNCT_1:12;
then |--(A,E.j).(f.v)<=|--(A,E.j).v by A42,A59,A57,RLAFFIN3:def 3;
then A60: x in F.j by A58;
F.j in F.:S by A56,FUNCT_1:def 6;
hence thesis by A60,TARSKI:def 4;
end;
end;
end;
then meet rng F is non empty by A2,A3,A25,Th22;
then consider v be object such that
A61: v in meet rng F by XBOOLE_0:def 1;
A62: v in cA by A7,A61;
then reconsider v as Element of TRn;
set fv=f.v,vA=v|--A,fvA=fv|--A;
A63: len(fvA*E)=len E by FINSEQ_2:33;
fv in rng f by A8,A61,FUNCT_1:def 3;
then A64: fv in cA by A7;
then Carrier fvA c=A & sum fvA=1 by A27,RLAFFIN1:def 7,RLVECT_2:def 6;
then A65: Carrier vA c=A & 1=Sum(fvA*E) by A28,RLAFFIN1:30,RLVECT_2:def 6;
A66: len E=len(vA*E) by FINSEQ_2:33;
then reconsider fvAE=fvA*E,vAE=vA*E as Element of len E-tuples_on REAL by A63
,FINSEQ_2:92;
A67: dom fvAE=Seg len E by A63,FINSEQ_1:def 3;
A68: dom vAE=Seg len E by A66,FINSEQ_1:def 3;
A69: for j be Nat st j in Seg len E holds fvAE.j<=vAE.j
proof
let j be Nat;
assume A70: j in Seg len E;
then F.j=P(j) & F.j in rng F by A3,A26,A29,FUNCT_1:def 3;
then v in P(j) by A61,SETFAM_1:def 1;
then A71: ex w be Element of T st w=v & |--(A,E.j).(f.w)<=|--(A,E.j).w;
A72: |--(A,E.j).v=vA.(E.j) by RLAFFIN3:def 3
.=vAE.j by A68,A70,FUNCT_1:12;
|--(A,E.j).fv=fvA.(E.j) by A64,RLAFFIN3:def 3
.=fvAE.j by A67,A70,FUNCT_1:12;
hence thesis by A71,A72;
end;
A73: Carrier vA c=A by RLVECT_2:def 6;
sum vA=1 by A27,A62,RLAFFIN1:def 7;
then A74: Sum fvAE=Sum vAE by A28,A65,RLAFFIN1:30;
A75: Carrier fvA c=A by RLVECT_2:def 6;
A76: now let w be Element of TRn;
per cases;
suppose w in A;
then consider j be object such that
A77: j in dom E and
A78: E.j=w by A28,FUNCT_1:def 3;
A79: fvAE.j=fvA.w & vAE.j=vA.w by A77,A78,FUNCT_1:13;
fvAE.j<=vAE.j & fvAE.j>=vAE.j by A26,A74,A69,A77,RVSUM_1:83;
hence vA.w=fvA.w by A79,XXREAL_0:1;
end;
suppose A80: not w in A;
then not w in Carrier vA by A73;
then A81: vA.w=0 by RLVECT_2:19;
not w in Carrier fvA by A75,A80;
hence vA.w=fvA.w by A81,RLVECT_2:19;
end;
end;
A82: Sum vA=v by A27,A62,RLAFFIN1:def 7;
Sum fvA=fv by A27,A64,RLAFFIN1:def 7;
then v=fv by A76,A82,RLVECT_2:def 9;
hence thesis by A8,A61;
end;
theorem
for A st card A = n+1
for f be continuous Function of (TOP-REAL n)|conv A,(TOP-REAL n)|conv A
holds f is with_fixpoint
proof
let A be affinely-independent Subset of TOP-REAL n such that
A1: card A=n+1;
let f be continuous Function of(TOP-REAL n)|conv A,(TOP-REAL n)|conv A;
consider x be Point of TOP-REAL n such that
A2: x in dom f & f.x=x by A1,Th23;
x is_a_fixpoint_of f by A2,ABIAN:def 3;
hence thesis by ABIAN:def 5;
end;
theorem Th25:
card A = n+1 implies ind conv A = n
proof
set TR=TOP-REAL n;
assume A1: card A=n+1;
set C=conv A;
A2: ind C>=n
proof
set E=the Enumeration of A;
assume A3: ind C<n;
A is non empty by A1;
then reconsider C as non empty Subset of TR;
ind C is natural;
then reconsider n1=n-1 as Nat by A3;
deffunc F(object)=C\conv(A\{E.$1});
reconsider c =C as Subset of the TopStruct of TR;
set TRC=TR|C;
set carr=the carrier of TRC;
A4: the TopStruct of TR=TopSpaceMetr Euclid n & the TopStruct of TRC=(the
TopStruct of TR)|c by EUCLID:def 8,PRE_TOPC:36;
consider f be FinSequence such that
A5: len f=len E & for k st k in dom f holds f.k=F(k) from FINSEQ_1:sch 2;
A6: [#]TRC=C by PRE_TOPC:def 5;
rng f c=bool carr
proof
let y be object;
assume y in rng f;
then consider x be object such that
A7: x in dom f and
A8: f.x=y by FUNCT_1:def 3;
f.x=F(x) by A5,A7;
then f.x c=C by XBOOLE_1:36;
hence thesis by A6,A8;
end;
then reconsider R=rng f as finite Subset-Family of TRC;
A9: rng E=A by RLAFFIN3:def 1;
then A10: len E=card A by FINSEQ_4:62;
A11: dom f=dom E by A5,FINSEQ_3:29;
the carrier of TRC c=union R
proof
let x be object;
assume A12: x in the carrier of TRC;
assume A13: not x in union R;
now let y be set;
assume A14: y in A;
then consider n be object such that
A15: n in dom E and
A16: E.n=y by A9,FUNCT_1:def 3;
reconsider n as Nat by A15;
f.n=F(n) by A5,A11,A15;
then F(n) in R by A11,A15,FUNCT_1:def 3;
then not x in F(n) by A13,TARSKI:def 4;
then conv(A\{E.n})c=Affin(A\{E.n}) & x in conv(A\{E.n}) by A6,A12,
RLAFFIN1:65,XBOOLE_0:def 5;
then A17: x|--A=x|--(A\{E.n}) by RLAFFIN1:77,XBOOLE_1:36;
Carrier(x|--(A\{E.n}))c=A\{E.n} & E.n in {E.n} by RLVECT_2:def 6
,TARSKI:def 1;
then not E.n in Carrier(x|--(A\{E.n})) by XBOOLE_0:def 5;
hence (x|--A).y=0 by A14,A16,A17,RLVECT_2:19;
end;
then A18: x in conv(A\A) by A6,A12,RLAFFIN1:76;
A\A={} by XBOOLE_1:37;
hence contradiction by A18;
end;
then A19: R is Cover of TRC by SETFAM_1:def 11;
now let U be Subset of TRC;
assume U in R;
then consider x be object such that
A20: x in dom f & f.x=U by FUNCT_1:def 3;
reconsider cAE=conv(A\{E.x}) as Subset of TRC by A6,RLAFFIN1:3,XBOOLE_1:36;
A\{E.x} is affinely-independent by RLAFFIN1:43,XBOOLE_1:36;
then A21: cAE is closed by TSEP_1:8;
U=cAE` by A6,A5,A20;
hence U is open by A21;
end;
then A22: ind TRC=ind C & R is open by TOPDIM_1:17,TOPS_2:def 1;
ind C<n1+1 by A3;
then ind C<=n1 by NAT_1:13;
then consider G be finite Subset-Family of TRC such that
A23: G is open and
A24: G is Cover of TRC and
A25: G is_finer_than R and
card G<=card R*(n1+1) and
A26: order G<=n1 by A4,A22,A19,TOPDIM_2:23;
defpred P[Nat,set,set] means
$3={g where g is Subset of TRC:g in G & (g c=f.($1+1) or g in $2)};
defpred P[set] means
$1 in G & $1c=f.1;
consider G0 be Subset-Family of TRC such that
A27: for x be set holds x in G0 iff x in bool carr & P[x] from SUBSET_1:sch
1;
A28: for k be Nat st 1<=k & k<len E for x be Element of bool bool carr ex y
be Element of bool bool carr st P[k,x,y]
proof
let k be Nat such that
1<=k and
k<len E;
let x be Element of bool bool carr;
set y={g where g is Subset of TRC:g in G & (g c=f.(k+1) or g in x)};
y c=bool carr
proof
let z be object;
assume z in y;
then ex g be Subset of TRC st g=z & g in G & (g c=f.(k+1) or g in x);
hence thesis;
end;
hence thesis;
end;
consider p be FinSequence of bool bool carr such that
A29: len p=len E and
A30: p/.1=G0 or len E=0 and
A31: for k be Nat st 1<=k & k<len E holds P[k,p/.k,p/.(k+1)] from NAT_2:sch
1(A28);
defpred H[Nat,object] means
($1=1 implies $2=union G0) & ($1<>1 implies $2=union(p.$1\p.($1-1)));
A32: for k be Nat st k in Seg len E ex x be object st H[k,x]
proof
let k be Nat;
k=1 or k<>1;
hence thesis;
end;
consider h be FinSequence such that
A33: dom h=Seg len E and
A34: for k be Nat st k in Seg len E holds H[k,h.k] from FINSEQ_1:sch 1(A32
);
A35: dom p=Seg len E by A29,FINSEQ_1:def 3;
rng h c=bool carr
proof
let y be object;
assume y in rng h;
then consider x be object such that
A36: x in dom h and
A37: h.x=y by FUNCT_1:def 3;
reconsider x as Nat by A36;
p.x in rng p by A35,A33,A36,FUNCT_1:def 3;
then reconsider px=p.x as Subset-Family of TRC;
y=union G0 or y=union(px\p.(x-1)) by A33,A34,A36,A37;
hence thesis;
end;
then reconsider h as FinSequence of bool carr by FINSEQ_1:def 4;
A38: A is non empty affinely-independent Subset of TOP-REAL n by A1;
A39: 1<=n+1 by NAT_1:11;
the carrier of TRC c=union rng h
proof
let x be object;
assume x in the carrier of TRC;
then x in union G by A24,SETFAM_1:45;
then consider y be set such that
A40: x in y and
A41: y in G by TARSKI:def 4;
consider z be set such that
A42: z in R and
A43: y c=z by A25,A41,SETFAM_1:def 2;
consider k be object such that
A44: k in dom f and
A45: f.k=z by A42,FUNCT_1:def 3;
reconsider k as Nat by A44;
A46: k>=1 by A44,FINSEQ_3:25;
A47: len E>=k by A5,A44,FINSEQ_3:25;
per cases by A46,XXREAL_0:1;
suppose A48: k=1 or y in G0;
A49: 1 in Seg len E by A1,A10,A39,FINSEQ_1:1;
then A50: h.1=union G0 by A34;
y in G0 by A27,A41,A43,A45,A48;
then A51: x in h.1 by A40,A50,TARSKI:def 4;
h.1 in rng h by A33,A49,FUNCT_1:def 3;
hence thesis by A51,TARSKI:def 4;
end;
suppose A52: k>1 & not y in G0;
defpred Q[Nat] means
$1>1 & $1<=len E & y c=f.$1;
A53: ex k be Nat st Q[k] by A43,A45,A47,A52;
consider m be Nat such that
A54: Q[m] & for n be Nat st Q[n] holds m<=n from NAT_1:sch 5(A53);
reconsider m1=m-1 as Element of NAT by A54,NAT_1:20;
defpred R[Nat] means
1<=$1 & $1<=m1 implies not y in p/.$1;
m1+1<=len E by A54;
then A55: m1<len E by NAT_1:13;
A56: for n be Nat st R[n] holds R[n+1]
proof
let n be Nat such that
A57: R[n];
set n1=n+1;
assume that
1<=n1 and
A58: n1<=m1;
n<m1 by A58,NAT_1:13;
then A59: n<len E by A55,XXREAL_0:2;
per cases by NAT_1:14;
suppose n=0;
hence thesis by A1,A9,A30,A52,FINSEQ_4:62;
end;
suppose A60: n>=1;
assume A61: y in p/.n1;
p/.n1={g where g is Subset of TRC:g in G & (g c=f.n1 or g in p/.n)} by
A31,A59,A60;
then ex g be Subset of TRC st y=g & g in G & (g c=f.n1 or g in p/.n) by
A61;
then Q[n1] by A55,A57,A58,A60,NAT_1:13,XXREAL_0:2;
then m<=n1 by A54;
then m1+1<=m1 by A58,XXREAL_0:2;
hence contradiction by NAT_1:13;
end;
end;
A62: R[0];
A63: for n holds R[n] from NAT_1:sch 2(A62,A56);
A64: m in dom p by A29,A54,FINSEQ_3:25;
then A65: h.m in rng h by A35,A33,FUNCT_1:def 3;
m1+1>1 by A54;
then A66: m1>=1 by NAT_1:13;
then A67: p/.m={g where g is Subset of TRC:g in G & (g c=f.(m1+1) or g in
p/.m1)} by A31,A55;
m1 in dom p by A29,A66,A55,FINSEQ_3:25;
then p.m1=p/.m1 by PARTFUN1:def 6;
then A68: not y in p.m1 by A66,A63;
p.m=p/.m by A64,PARTFUN1:def 6;
then y in p.m by A41,A54,A67;
then y in p.m\p.m1 by A68,XBOOLE_0:def 5;
then A69: x in union(p.m\p.m1) by A40,TARSKI:def 4;
h.m=union(p.m\p.m1) by A35,A34,A54,A64;
hence thesis by A69,A65,TARSKI:def 4;
end;
end;
then A70: rng h is Cover of TRC by SETFAM_1:def 11;
now let A be Subset of TRC;
assume A in rng h;
then consider k be object such that
A71: k in dom h and
A72: h.k=A by FUNCT_1:def 3;
reconsider k as Nat by A71;
A73: k>=1 by A33,A71,FINSEQ_1:1;
per cases by A73,XXREAL_0:1;
suppose A74: k=1;
A75: G0 c=G
by A27;
h.k=union G0 by A33,A34,A71,A74;
hence A is open by A23,A72,A75,TOPS_2:11,19;
end;
suppose A76: k>1;
then reconsider k1=k-1 as Element of NAT by NAT_1:20;
k1+1>1 by A76;
then A77: k1>=1 by NAT_1:13;
k1+1<=len E by A33,A71,FINSEQ_1:1;
then A78: k1<len E by NAT_1:13;
then k1 in dom p by A29,A77,FINSEQ_3:25;
then A79: p.k1=p/.k1 by PARTFUN1:def 6;
A80: P[k1,p/.k1,p/.(k1+1)] by A31,A77,A78;
p/.k c=G
proof
let x be object;
assume x in p/.k;
then ex g be Subset of TRC st x=g & g in G & (g c=f.k or g in p/.k1) by
A80;
hence thesis;
end;
then p/.k is open by A23,TOPS_2:11;
then A81: p/.k\p/.(k-1) is open by TOPS_2:15;
A82: p.k=p/.k by A35,A33,A71,PARTFUN1:def 6;
A=union(p.k\p.(k-1)) by A33,A34,A71,A72,A76;
hence A is open by A82,A81,A79,TOPS_2:19;
end;
end;
then A83: rng h is open by TOPS_2:def 1;
TRC is compact by COMPTS_1:3;
then consider gx be Subset-Family of TRC such that
gx is open and
A84: gx is Cover of TRC and
A85: clf gx is_finer_than rng h and
A86: gx is locally_finite by A4,A70,A83,PCOMPS_1:22,PCOMPS_2:3;
set cgx=clf gx;
defpred G[object,object] means
$2=union{u where u is Subset of TRC:u in cgx & u c=h.$1};
A87: for k be Nat st k in Seg len E ex x be Element of bool carr st G[k,x]
proof
let k be Nat;
set U={u where u is Subset of TRC:u in cgx & u c=h.k};
U c=bool carr
proof
let x be object;
assume x in U;
then ex u be Subset of TRC st u=x & u in cgx & u c=h.k;
hence thesis;
end;
then reconsider U as Subset-Family of TRC;
union U is Subset of TRC;
hence thesis;
end;
consider GX be FinSequence of bool carr such that
A88: dom GX=Seg len E & for k be Nat st k in Seg len E holds G[k,GX.k]
from FINSEQ_1:sch 5(A87);
A89: for i be Nat st i in dom GX holds GX.i c=h.i
proof
let i be Nat;
set U={u where u is Subset of TRC:u in cgx & u c=h.i};
now let x be set;
assume x in U;
then ex u be Subset of TRC st x=u & u in cgx & u c=h.i;
hence x c=h.i;
end;
then A90: union U c=h.i by ZFMISC_1:76;
assume i in dom GX;
hence thesis by A88,A90;
end;
A91: dom E=Seg len E by FINSEQ_1:def 3;
A92: for k be Nat st k in Seg len E holds h.k misses conv(A\{E.k})
proof
let k be Nat;
assume A93: k in Seg len E;
then A94: k>=1 by FINSEQ_1:1;
A95: H[k,h.k] by A34,A93;
assume h.k meets conv(A\{E.k});
then consider x be object such that
A96: x in h.k and
A97: x in conv(A\{E.k}) by XBOOLE_0:3;
per cases by A94,XXREAL_0:1;
suppose A98: k=1;
then consider y be set such that
A99: x in y and
A100: y in G0 by A95,A96,TARSKI:def 4;
P[y] by A27,A100;
then y c=F(k) by A5,A11,A91,A93,A98;
hence contradiction by A97,A99,XBOOLE_0:def 5;
end;
suppose A101: k>1;
then reconsider k1=k-1 as Element of NAT by NAT_1:20;
len E>=k1+1 by A93,FINSEQ_1:1;
then A102: len E>k1 by NAT_1:13;
k1+1>1 by A101;
then A103: k1>=1 by NAT_1:13;
then A104: P[k1,p/.k1,p/.(k1+1)] by A31,A102;
k1 in dom p by A29,A103,A102,FINSEQ_3:25;
then A105: p/.k1=p.k1 by PARTFUN1:def 6;
A106: p/.k=p.k by A35,A93,PARTFUN1:def 6;
consider y be set such that
A107: x in y and
A108: y in p.k\p.(k-1) by A95,A96,A101,TARSKI:def 4;
y in p.k by A108;
then consider g be Subset of TRC such that
A109: y=g and
g in G and
A110: g c=f.k or g in p.k1 by A104,A106,A105;
f.k=F(k) by A5,A11,A91,A93;
hence contradiction by A97,A107,A108,A109,A110,XBOOLE_0:def 5;
end;
end;
carr c=union rng GX
proof
let x be object;
assume A111: x in carr;
union gx=carr & union gx c=union cgx by A84,PCOMPS_1:19,SETFAM_1:45;
then consider y be set such that
A112: x in y and
A113: y in cgx by A111,TARSKI:def 4;
consider r be set such that
A114: r in rng h and
A115: y c=r by A85,A113,SETFAM_1:def 2;
consider k be object such that
A116: k in dom h and
A117: h.k=r by A114,FUNCT_1:def 3;
A118: G[k,GX.k] by A33,A88,A116;
A119: GX.k in rng GX by A33,A88,A116,FUNCT_1:def 3;
y in {u where u is Subset of TRC:u in cgx & u c=h.k} by A113,A115,A117;
then x in GX.k by A112,A118,TARSKI:def 4;
hence thesis by A119,TARSKI:def 4;
end;
then A120: rng GX is Cover of TRC by SETFAM_1:def 11;
A121: for S be Subset of dom GX holds conv(E.:S)c=union(GX.:S)
proof
let S be Subset of dom GX;
A122: rng GX=GX.:dom GX by RELAT_1:113;
A123: union rng GX=carr by A120,SETFAM_1:45;
per cases by XBOOLE_0:def 10;
suppose S=dom GX;
hence thesis by A6,A9,A91,A88,A122,A123,RELAT_1:113;
end;
suppose A124: not dom GX c=S;
set U={conv(A\{E.i}) where i is Element of NAT:i in dom E\S};
dom GX\S is non empty by A124,XBOOLE_1:37;
then A125: conv(E.:S)=meet U by A91,A88,Th12;
A126: meet U misses union(GX.:(dom E\S))
proof
assume meet U meets union(GX.:(dom E\S));
then consider x be object such that
A127: x in meet U and
A128: x in union(GX.:(dom E\S)) by XBOOLE_0:3;
consider y be set such that
A129: x in y and
A130: y in GX.:(dom E\S) by A128,TARSKI:def 4;
consider i be object such that
A131: i in dom GX and
A132: i in dom E\S and
A133: GX.i=y by A130,FUNCT_1:def 6;
reconsider i as Element of NAT by A131;
conv(A\{E.i}) in U by A132;
then A134: meet U c=conv(A\{E.i}) by SETFAM_1:7;
y c=h.i by A89,A131,A133;
then h.i meets conv(A\{E.i}) by A127,A129,A134,XBOOLE_0:3;
hence contradiction by A92,A88,A131;
end;
dom GX=dom E by A88,FINSEQ_1:def 3;
then rng GX=GX.:(S\/(dom E\S)) by A122,XBOOLE_1:45
.=GX.:S\/GX.:(dom E\S) by RELAT_1:120;
then A135: union(GX.:S)\/union(GX.:(dom E\S)) =C by A6,A123,ZFMISC_1:78;
conv(E.:S)c=C by A9,RELAT_1:111,RLAFFIN1:3;
hence thesis by A125,A135,A126,XBOOLE_1:73;
end;
end;
A136: cgx is locally_finite by A86,PCOMPS_1:18;
now let A be Subset of TRC;
assume A in rng GX;
then consider k be object such that
A137: k in dom GX & GX.k=A by FUNCT_1:def 3;
set U={u where u is Subset of TRC:u in cgx & u c=h.k};
A138: U c=cgx
proof
let x be object;
assume x in U;
then ex u be Subset of TRC st x=u & u in cgx & u c=h.k;
hence thesis;
end;
then reconsider U as Subset-Family of TRC by XBOOLE_1:1;
U is closed by A138,PCOMPS_1:11,TOPS_2:12;
then union U is closed by A136,A138,PCOMPS_1:9,21;
hence A is closed by A88,A137;
end;
then A139: rng GX is closed by TOPS_2:def 2;
len GX=card A by A10,A88,FINSEQ_1:def 3;
then meet rng GX is non empty by A139,A38,A121,Th22;
then consider I be object such that
A140: I in meet rng GX by XBOOLE_0:def 1;
defpred T[Nat,set] means
$2 in G & I in $2 & $2 in p.$1 & ($1<>1 implies not$2 in p.($1-1));
A141: for k be Nat st k in Seg len E ex x be Element of bool carr st T[k,x]
proof
let k be Nat;
assume A142: k in Seg len E;
then A143: k>=1 by FINSEQ_1:1;
A144: k<=len E by A142,FINSEQ_1:1;
A145: GX.k c=h.k & H[k,h.k] by A34,A88,A89,A142;
GX.k in rng GX by A88,A142,FUNCT_1:def 3;
then meet rng GX c=GX.k by SETFAM_1:7;
then A146: I in GX.k by A140;
per cases by A143,XXREAL_0:1;
suppose A147: k=1;
1 in dom p by A1,A10,A35,A39,FINSEQ_1:1;
then A148: p.1=G0 by A1,A9,A30,FINSEQ_4:62,PARTFUN1:def 6;
consider g be set such that
A149: I in g and
A150: g in G0 by A146,A145,A147,TARSKI:def 4;
g in G by A27,A150;
hence thesis by A147,A149,A150,A148;
end;
suppose A151: k>1;
then reconsider k1=k-1 as Nat;
A152: k1+1=k;
then A153: k1<len E by A144,NAT_1:13;
k1>=1 by A151,A152,NAT_1:13;
then A154: P[k1,p/.k1,p/.k] by A31,A153;
A155: p.k=p/.k by A35,A142,PARTFUN1:def 6;
consider g be set such that
A156: I in g and
A157: g in p.k\p.(k-1) by A146,A145,A151,TARSKI:def 4;
A158: not g in p.(k-1) by A157,XBOOLE_0:def 5;
g in p.k by A157;
then ex gg be Subset of TRC st g=gg & gg in G & (gg c=f.(k1+1) or gg in p
/.k1) by A154,A155;
hence thesis by A156,A157,A158;
end;
end;
consider t be FinSequence of bool carr such that
A159: dom t=Seg len E & for k be Nat st k in Seg len E holds T[k,t.k] from
FINSEQ_1:sch 5(A141);
A160: now let i,j be Nat;
assume that
A161: i in dom t and
A162: j in dom t and
A163: i<j;
A164: j<=len E by A159,A162,FINSEQ_1:1;
defpred P[Nat] means
i<=$1 & $1<j implies t.i in p.$1;
A165: T[i,t.i] by A159,A161;
A166: 1<=i by A159,A161,FINSEQ_1:1;
A167: for k st P[k] holds P[k+1]
proof
let k;
assume A168: P[k];
set k1=k+1;
assume that
A169: i<=k1 and
A170: k1<j;
A171: k<j by A170,NAT_1:13;
per cases by A169,NAT_1:8;
suppose i=k1;
hence thesis by A159,A161;
end;
suppose A172: i<=k;
1<=k1 & k1<=len E by A166,A164,A169,A170,XXREAL_0:2;
then A173: k1 in dom p by A35,FINSEQ_1:1;
A174: k<len E by A164,A171,XXREAL_0:2;
A175: 1<=k by A166,A172,XXREAL_0:2;
then k in dom p by A35,A174,FINSEQ_1:1;
then A176: p.k=p/.k by PARTFUN1:def 6;
P[k,p/.k,p/.k1] by A31,A175,A174;
then p.k1={g where g is Subset of TRC:g in G & (g c=f.k1 or g in p.k)}
by A173,A176,PARTFUN1:def 6;
hence thesis by A165,A168,A170,A172,NAT_1:13;
end;
end;
A177: P[0] by A165;
A178: for k holds P[k] from NAT_1:sch 2(A177,A167);
reconsider j1=j-1 as Nat by A163;
assume A179: t.i=t.j;
A180: j1+1=j;
then A181: j1<j by NAT_1:13;
A182: j<>1 by A159,A161,A163,FINSEQ_1:1;
i<=j1 by A163,A180,NAT_1:13;
then t.i in p.j1 by A181,A178;
hence contradiction by A159,A162,A179,A182;
end;
now let x1,x2 be object;
assume A183: x1 in dom t & x2 in dom t;
then reconsider i1=x1,i2=x2 as Nat;
assume A184: t.x1=t.x2;
assume x1<>x2;
then i1>i2 or i1<i2 by XXREAL_0:1;
hence contradiction by A160,A183,A184;
end;
then t is one-to-one by FUNCT_1:def 4;
then A185: card rng t=len t by FINSEQ_4:62
.=len E by A159,FINSEQ_1:def 3
.=n+1 by A1,A9,FINSEQ_4:62;
then A186: rng t is non empty;
A187: now let x be set;
assume x in rng t;
then consider i be object such that
A188: i in dom t & t.i=x by FUNCT_1:def 3;
thus I in x by A159,A188;
end;
A189: rng t c=G
proof
let y be object;
assume y in rng t;
then consider x be object such that
A190: x in dom t & t.x=y by FUNCT_1:def 3;
thus thesis by A159,A190;
end;
n<card rng t by A185,NAT_1:13;
then card Segm n in card Segm card rng t by NAT_1:41;
then n1+1 in card rng t;
then meet rng t is empty by A26,A189,TOPDIM_2:2;
hence contradiction by A186,A187,SETFAM_1:def 1;
end;
ind C<=ind TR & ind TR<=n by TOPDIM_1:20,TOPDIM_2:21;
then ind C<=n by XXREAL_0:2;
hence thesis by A2,XXREAL_0:1;
end;
theorem
ind TOP-REAL n = n
proof
set T=TOP-REAL n;
consider I be affinely-independent Subset of T such that
A1: {}T c= I & I c= [#]T & Affin I = Affin [#]T by RLAFFIN1:60;
[#]T is Affine by RUSUB_4:22;
then dim T = n & Affin [#]T = [#]T by RLAFFIN1:50,RLAFFIN3:4;
then card I = n+1 by A1,RLAFFIN3:6;
then ind conv I=n by Th25;
then ind T >= n & ind T <= n by TOPDIM_1:20,TOPDIM_2:21;
hence thesis by XXREAL_0:1;
end;