:: Brouwer Fixed Point Theorem for Simplexes
:: by Karol P\kak
::
:: Received December 21, 2010
:: Copyright (c) 2010-2018 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_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, CARD_1, 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[#]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 & n0;
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 & n0 by HAUSDORF:9;
then (dist_min g19).x>0 by JORDAN1K:9;
hence 01;
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 & j10 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;
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 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=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 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:
(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 k0;
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.| by FINSEQ_1:40;
then A11: |.v.|=|.v1.| by TOPREALC:18;
|.v.|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;
rng p c=REAL;
then A13: p is FinSequence of REAL by FINSEQ_1:def 4;
then A14: q1 is FinSequence of REAL by A12,FINSEQ_1:36;
A15: q2 is FinSequence of REAL by A12,A13,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)=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 C1 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=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=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=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: i1 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= n & ind T <= n by TOPDIM_1:20,TOPDIM_2:21;
hence thesis by XXREAL_0:1;
end;