:: Brouwer Fixed Point Theorem for Simplexes
:: by Karol P\kak
::
:: Received December 21, 2010
:: Copyright (c) 2010-2011 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, JORDAN2C,
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,
NAT_1, PRE_TOPC, NUMBERS, 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, MATROID0,
TBSP_1, MEMBERED, RLVECT_2, CONVEX1, TOPREAL9, COMPLEX1, NEWTON, POWER,
JORDAN2C, SQUARE_1, BORSUK_1, CARD_3, EUCLID_9, TMAP_1, FINSEQOP, ABIAN,
WAYBEL23, TOPDIM_1, TOPDIM_2, RLAFFIN3;
constructors ABIAN, BINOP_2, COMPTS_1, CONVEX1, EUCLID_9, FINSEQOP, FUNCSDOM,
JORDAN2C, LEXBFS, MONOID_0, NEWTON, POWER, REAL_1, RFINSEQ2, RLAFFIN1,
RLAFFIN2, RLAFFIN3, RLVECT_5, RUSUB_5, SEQ_1, SEQ_4, SIMPLEX1, SQUARE_1,
TBSP_1, TMAP_1, TOPDIM_1, TOPDIM_2, TOPREAL9, TOPS_2, WAYBEL23, WEIERSTR;
registrations ASYMPT_0, BORSUK_1, BORSUK_2, CARD_1, COMPTS_1, DILWORTH,
EUCLID, EUCLID_9, FINSEQ_1, FINSEQ_2, 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, SPRECT_1, 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;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
definitions EUCLID, METRIC_1, ORDINAL1, PCOMPS_1, RLVECT_1, SIMPLEX0,
SIMPLEX1, STRUCT_0, SUBSET_1, TARSKI, TBSP_1, XCMPLX_0, CARD_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_0, XREAL_1, XXREAL_0, XXREAL_1, XXREAL_2, XXREAL_3,
ZFMISC_1;
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;
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 3;
per cases;
suppose A7: [#]TM in G;
take R=1;
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:73;
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:60;
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:27;
then A13: g.1 in rng g by FUNCT_1:def 5;
then reconsider g1=g.1 as Subset of TM by A9;
A14: g1``<>[#]TM by A8,A9,A12,FUNCT_1:def 5;
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:11,TOPMETR:24;
A15: for n be Nat st 1<=n & n[#]TM by A8,A9,A19,FUNCT_1:def 5;
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:54;
reconsider y=h as Element of FUNCS by FUNCT_2:11,TOPMETR:24;
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:24;
n+1<=len p by A31,FINSEQ_3:27;
then A37: 1<=n1+1 & n0 by HAUSDORF:11;
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:24;
j1+1>1 by A61;
then A62: 1<=j1 & j10 by A66,HAUSDORF:11;
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 5;
then P[len p] by A11,A23,FINSEQ_3:27,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:27;
A72: k<=len p by A69,FINSEQ_3:27;
per cases by A71,XXREAL_0:1;
suppose A73: k=1;
take g1;
thus g1 in F by A4,A9,A13;
let y be set 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:24;
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:27,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:60,ZFMISC_1:95;
then G is Cover of TM by SETFAM_1:def 12;
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,XBOOLE_1:1;
end;
union F=[#]TM & union F c=union G by A2,A3,SETFAM_1:18,60;
then G is Cover of TM by SETFAM_1:def 12;
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,XBOOLE_1:1;
end;
hence thesis by A1,Def1;
end;
begin :: Bounded Simplicial Complexes
reserve n,k for Nat,
r for real number,
X for set,
M for Reflexive (non empty MetrStruct),
A for Subset of M,
K for SimplicialComplexStr;
registration let M;
cluster finite -> bounded 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 set 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 set;
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 by XREAL_0:def 1;
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 (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 number 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 Integer;
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 by SIMPLEX0:def 5;
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 5;
then A c=V by SIMPLEX0:17;
then A c=VM by XBOOLE_1:19;
hence thesis by TBSP_1:32;
end;
begin :: The Diameter of a Bounded Simplicial Complex
X: 0 in REAL by XREAL_0:def 1;
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 number 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 set;
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 set 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 number such that
A4: for A st A in the topology of K holds A is bounded & D(A)<=rr by A1
,Def2;
now let x be ext-real number;
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,XXREAL_2:16;
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 number such that
A7: for A st A in the topology of K holds diameter A<=r;
now let x be ext-real number;
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 by X;
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 number 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
number 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 set 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 number st for A st A in the topology of K holds A is bounded &
diameter A<=r by A1,Def2;
then diameter S>=0 by A3,TBSP_1:29;
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 Integer
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 Integer;
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) -> Real 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;
coherence;
compatibility
proof
let d be Real;
{}K is simplex-like;
then {}M in the topology of K by PRE_TOPC:def 5;
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 5;
hence diameter A<=d by A1,A2,Def3;
end;
let r be real number;
assume A3: for A st A is Simplex of K holds diameter A<=r;
now let A;
assume A in the topology of K;
then A is Simplex of K by PRE_TOPC:def 5;
hence diameter A<=r by A3;
end;
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 number st(for A st A is Simplex of K holds diameter A<=r)
holds r>=d;
now let A;
assume A in the topology of K;
then A is Simplex of K by PRE_TOPC:def 5;
hence diameter A<=d by A4;
end;
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 5;
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 5;
hence diameter W<=diameter S by TBSP_1:32;
end;
then A2: diameter(M,C)<=diameter S by Def4;
S c=S;
then s is simplex-like by A1,PRE_TOPC:def 5;
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 :Def5:
K is (Euclid n) bounded;
func diameter K -> Real equals
diameter(Euclid n,K);
coherence;
end;
registration
let n;
cluster bounded -> Euclid n bounded (SimplicialComplexStr of TOP-REAL n);
coherence by Def5;
cluster bounded affinely-independent simplex-join-closed non void
finite-degree total 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 by Def5;
end;
cluster finite-vertices -> bounded SimplicialComplexStr of TOP-REAL n;
coherence
proof
let K be SimplicialComplexStr of TOP-REAL n;
assume K is finite-vertices;
then K is Euclid n bounded by Th6;
hence thesis by Def5;
end;
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 & union F is Simplex of Kv
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 and
union F is Simplex of Kv;
let a1,a2 be VECTOR of V such that
A2: a1 in S and
A3: a2 in S;
consider A1 be set such that
A4: A1 in dom cM and
A5: A1 in F and
A6: cM.A1=a1 by A1,A2,FUNCT_1:def 12;
consider A2 be set such that
A7: A2 in dom cM and
A8: A2 in F and
A9: cM.A2=a2 by A1,A3,FUNCT_1:def 12;
A10: A1,A2 are_c=-comparable by A5,A8,ORDINAL1:def 9;
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:92;
A20: A1<>{} by A14,ORDERS_1:4;
then A21: uF is non empty by A19;
A22: A2 c=uF by A17,ZFMISC_1:92;
then 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:37;
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,XBOOLE_1:1;
then {A21}c=bool uF by ZFMISC_1:37;
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:117;
then aa1 is simplex-like by A23,A26,SIMPLEX0:def 20;
then A30: d1 is vertex-like by A28,SIMPLEX0:def 3;
per cases;
suppose A31: A1=A2;
reconsider Z=0 as Real by XREAL_0:def 1;
take b1=a1,b2=a1,Z;
card uF>=1 by A21,NAT_1:14;
then A32: card uF-1>=1-1 by XREAL_1:8;
a1-a2=0.V by A16,A18,A31,RLVECT_1:16;
hence thesis by A30,A32,RLVECT_1:23,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:5;
then cM.A21 in rng cM by FUNCT_1:def 5;
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:117;
then aa2 is simplex-like by A24,A26,SIMPLEX0:def 20;
then A35: d2 is vertex-like by A34,SIMPLEX0:def 3;
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 by XREAL_0:def 1;
take a1,a21,r;
A36: r*r21=(card A21*1)/(card A21*card A2) by XCMPLX_1:77
.=r2 by XCMPLX_1:92;
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 8;
A40: card A21=1 *card A2-1 *card A1 by A13,CARD_2:63;
then A41: r1-r2=(card A21*1)/(card A2*card A1) by XCMPLX_1:131
.=r*r1 by XCMPLX_1:77;
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 8;
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 8;
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:19;
A49: (L1-L2).v=L1.v-L2.v by RLVECT_2:79;
A50: dom(A1-->r1)=A1 by FUNCOP_1:19;
A51: dom(A2-->r2)=A2 by FUNCOP_1:19;
(r*(L1-L21)).v=r*((L1-L21).v) by RLVECT_2:def 13;
then A52: (r*(L1-L21)).v=r*(L1.v-L21.v) by RLVECT_2:79;
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:28;
A55: (A2-->r2).v=r2 & (A1-->r1).v=r1 by A13,A53,FUNCOP_1:13;
L1.v=(A1-->r1).v by A38,A50,A53,FUNCT_4:14;
hence thesis by A13,A41,A46,A49,A51,A52,A53,A54,A55,FUNCT_4:14;
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:28;
(A2-->r2).v=r2 by A56,FUNCOP_1:13;
then A58: (L1-L2).v=-r2 by A46,A49,A51,A56,A57,FUNCT_4:14;
A59: v in A21 by A56,XBOOLE_0:def 5;
then (A21-->r21).v=r21 by FUNCOP_1:13;
then (r*(L1-L21)).v=r*(-r21) by A43,A48,A52,A57,A59,FUNCT_4:14;
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:28;
not v in Carrier(L21) by A44,A60,XBOOLE_0:def 5;
then A62: L21.v=0 by RLVECT_2:28;
not v in Carrier(L2) by A47,A60;
hence thesis by A49,A52,A62,A61,RLVECT_2:28;
end;
end;
then A63: L1-L2=r*(L1-L21) by RLVECT_2:def 11;
card A1>=1 & card A2<=card uF by A17,NAT_1:14,44,ZFMISC_1:92;
then card A1*card uF>=1 *card A2 by XREAL_1:68;
then card A2*card uF-card A1*card uF<=card uF*card A2-card A2 by XREAL_1:15
;
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:104;
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:47
.=r*(-(b1-b2)) by RLVECT_1:39
.=r*(b2-b1) by RLVECT_1:47;
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 set 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:117;
per cases;
suppose i=0;
then consider x be set such that
A9: d\X={x} by A5,CARD_2:60;
A10: x=m by A6,A9,TARSKI:def 1;
A11: U c={C(m)}
proof
let u be set;
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:39;
E.:(d\X)={E.m} by A6,A8,A9,TARSKI:def 1;
hence thesis by A12,SETFAM_1:11;
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:140;
A15: d\X\{m}=d\Xm by XBOOLE_1:41;
A16: Um c=U
proof
let x be set;
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:54;
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 set;
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:37;
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 5;
A\E.:(d\Xm)c=A by XBOOLE_1:36;
then A1 is simplex-like by A21,PRE_TOPC:def 5;
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:153
.=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:11
.=meet(Um\/CC) by A20,SETFAM_1:10;
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:145
.=E.:d\E.:(d\X) by FUNCT_1:123
.=A\E.:(d\X) by A2,RELAT_1:146;
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: n in NAT by ORDINAL1:def 13;
A2: the TopStruct of TOP-REAL n=TopSpaceMetr Euclid n by EUCLID:def 8;
let a be bounded Subset of Euclid n
such that
A3: A=a;
let x be Point of Euclid n such that
A4: x in conv A;
A5: A c=cl_Ball(x,diameter a)
proof
let p be set;
assume A6: p in A;
then reconsider p as Point of Euclid n by A3;
reconsider pp=p as Point of TOP-REAL n by A2;
A7: cl_Ball(p,diameter a)=cl_Ball(pp,diameter a) by A1,TOPREAL9:14;
A c=cl_Ball(p,diameter a)
proof
let y be set;
assume A8: y in A;
then reconsider q=y as Point of Euclid n by A3;
dist(p,q)<=diameter a by A3,A6,A8,TBSP_1:def 10;
hence thesis by METRIC_1:13;
end;
then conv A c=cl_Ball(pp,diameter a) by A7,CONVEX1:30;
then dist(p,x)<=diameter a by A4,A7,METRIC_1:13;
hence thesis by METRIC_1:13;
end;
reconsider xx=x as Point of TOP-REAL n by A2;
cl_Ball(x,diameter a)=cl_Ball(xx,diameter a) by A1,TOPREAL9:14;
hence thesis by A5,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:def 2;
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:13;
hence dist(x,y)<=D+1 by XREAL_1:41;
end;
D>=0 by TBSP_1:29;
then cA is bounded by A1,TBSP_1:def 9;
hence conv A is Bounded by JORDAN2C:def 2;
end;
assume conv A is Bounded;
then cA is bounded by JORDAN2C:def 2;
then a is bounded by CONVEX1:41,TBSP_1:21;
hence thesis by JORDAN2C:def 2;
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:13;
end;
then A5: diameter ca<=diameter a by A1,A2,A3,TBSP_1:def 10;
diameter a<=diameter ca by A1,A2,CONVEX1:41,TBSP_1:32;
hence thesis by A5,XXREAL_0:1;
end;
end;
registration
let n;
let K be bounded SimplicialComplexStr of TOP-REAL n;
cluster -> bounded SubdivisionStr of K;
coherence
proof
let SK be SubdivisionStr of K;
consider r be real number 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 5;
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 5;
then A7: diameter B<=r by A1;
A8: B is bounded by A1,A6;
then @b is Bounded by JORDAN2C:def 2;
then conv@b is Bounded by Th14;
then reconsider cB=conv@b as bounded Subset of Euclid n by JORDAN2C:def 2;
A9: diameter cA<=diameter cB by A4,TBSP_1:32;
cA c=cB by A4;
then A10: cA is bounded by TBSP_1:21;
then A is bounded by CONVEX1:41,TBSP_1:21;
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:21,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 A2: 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 ext-real number;
assume A3: 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
A4: A=cM.:S by A2,A3,SIMPLEX0:def 20;
A5: A is bounded by A3,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 A6: union S is simplex-like by TOPS_2:def 1;
then A7: card union S<=degree K+ONE by SIMPLEX0:24;
A8: diameter K>=0 by Th7;
A9: not{} in dom cM by ORDERS_1:4;
then A10: dom cM is with_non-empty_elements by SETFAM_1:def 9;
A11: [#]T=[#]Euclid n by Lm1;
then reconsider US=Us as Subset of Euclid n;
A12: a in the topology of BK by PRE_TOPC:def 5;
per cases;
suppose K is empty-membered;
then A13: dK=-1 by SIMPLEX0:22;
then -1<=degree BK & degree BK<=-1 by A2,A10,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 by SIMPLEX0:def 7;
then A14: a={} by A12,SETFAM_1:def 11;
dK/(dK+1)=0 by A13;
hence thesis by A14,TBSP_1:def 10;
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 A15: dK>=-1+1 by INT_1:20;
then A16: dK/(dK+1)*diameter K>=0 by A8;
per cases;
suppose a is empty;
hence thesis by A16,TBSP_1:def 10;
end;
suppose A17: a is non empty;
now US is bounded;
then Us is Bounded by JORDAN2C:def 2;
then conv Us is Bounded by Th14;
then reconsider cUs=conv Us as bounded Subset of Euclid n by
JORDAN2C:def 2;
let x,y be Point of Euclid n;
assume that
A18: x in A and
A19: y in A;
reconsider X=x,Y=y as Element of T by A11;
A20: |.BCS C.|=|.C.| & |.C.|=conv Us by SIMPLEX1:8,10;
consider p be set such that
A21: p in dom cM and
A22: p in s and
cM.p=x by A4,A18,FUNCT_1:def 12;
p c=Us by A22,ZFMISC_1:92;
then A23: Us<>{} by A9,A21;
card Us<=dK+1 by A7,XXREAL_3:def 2;
then A24: (dK+1)"<=(card Us)" by A23,XREAL_1:87;
A25: diameter US<=diameter K by A6,Def4;
A26: (card Us-1)/card Us=card Us/card Us-(1/card Us)
.=1-(1/card Us) by A23,XCMPLX_1:60;
A27: diameter cUs=diameter US by Th15;
consider b1,b2 be VECTOR of T,r be Real such that
A28: b1 in Vertices BCS C and
A29: b2 in Vertices BCS C and
A30: X-Y=r*(b1-b2) and
A31: 0<=r and
A32: r<=(card Us-1)/card Us by A4,A6,A17,A18,A19,Th11;
reconsider B1=b1,B2=b2 as Element of BCS C by A28,A29;
B1 is vertex-like by A28,SIMPLEX0:def 4;
then consider S1 be Subset of BCS C such that
A33: S1 is simplex-like and
A34: B1 in S1 by SIMPLEX0:def 3;
A35: conv@S1 c=|.BCS C.| by A33,SIMPLEX1:5;
B2 is vertex-like by A29,SIMPLEX0:def 4;
then consider S2 be Subset of BCS C such that
A36: S2 is simplex-like and
A37: B2 in S2 by SIMPLEX0:def 3;
@S2 c=conv@S2 by CONVEX1:41;
then A38: B2 in conv@S2 by A37;
@S1 c=conv@S1 by CONVEX1:41;
then A39: B1 in conv@S1 by A34;
reconsider bb1=b1,bb2=b2 as Point of Euclid n by A11;
A40: b1-b2=bb1-bb2 by EUCLID:73;
dK/(dK+1)=(dK+1)/(dK+1)-(1/(dK+1))
.=1-(1/(dK+1)) by A15,XCMPLX_1:60;
then (card Us-1)/card Us<=dK/(dK+1) by A24,A26,XREAL_1:12;
then A41: dist(bb1,bb2)>=0 & r<=dK/(dK+1) by A32,XXREAL_0:2;
conv@S2 c=|.BCS C.| by A36,SIMPLEX1:5;
then dist(bb1,bb2)<=diameter US by A20,A27,A39,A38,A35,TBSP_1:def 10;
then A42: dist(bb1,bb2)<=diameter K by A25,XXREAL_0:2;
dist(x,y)=|.x-y.| by EUCLID:def 6
.=|.X-Y.| by EUCLID:73
.=|.r*(bb1-bb2).| by A30,A40,EUCLID:69
.=abs(r)*|.bb1-bb2.| by EUCLID:14
.=r*|.bb1-bb2.| by A31,ABSVALUE:def 1
.=r*dist(bb1,bb2) by EUCLID:def 6;
hence dist(x,y)<=dK/(dK+1)*diameter K by A31,A42,A41,XREAL_1:68;
end;
hence thesis by A5,A17,TBSP_1:def 10;
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:4;
then dom cM is with_non-empty_elements by SETFAM_1:def 9;
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:16;
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:20;
then ddK>0 by A14,XREAL_1:141;
then ddK|^(k+1)>0 by NEWTON:102;
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:20;
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:8;
then 1/(dK+1)<=1/(dB+1) by A15,XREAL_1:87;
then degree B/(degree B+1)<=dK/(dK+1) by A16,A17,XREAL_1:12;
then A18: degree B/(degree B+1)*diameter B<=dK/(dK+1)*((dK/(dK+1))|^k*
diameter K) by A4,A7,A15,XREAL_1:68;
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:11;
hence thesis by A1,A4,A9,A11,A12,A18,SIMPLEX1:20,XXREAL_0:2;
end;
end;
ddK|^(0 qua Nat)=1 by NEWTON:9;
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 number 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:20;
then A7: ddK>0 by A5,XREAL_1:141;
dK+1>dK by XREAL_1:31;
then A8: ddK<1 by A6,XREAL_1:191;
A9: ddK in REAL & r/diameter K in REAL by XREAL_0:def 1;
A10: diameter K>0 by A5,Th7;
then r/diameter K>0 by A2,XREAL_1:141;
then consider k be Element of NAT such that
A11: 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:21,XBOOLE_1:1;
hence thesis by JORDAN2C:def 2;
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:57;
then A11: |.v.|=abs 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 number such that
A6: A c=OpenHypercube(p,r) by A5,Th21;
A7: n in NAT by ORDINAL1:def 13;
then consider f be Function of[:TRn,TR1:],TRn1 such that
A8: f is being_homeomorphism and
A9: for fi be Element of TRn,fj be Element of TR1 holds f.(fi,fj)=fi^fj
by Th19;
A10: f is one-to-one & dom f=[#][:TRn,TR1:] by A8,TOPGRP_1:24;
len p=n1 by CARD_1:def 13;
then consider q1,q2 be FinSequence such that
A11: len q1=n and
A12: len q2=1 and
A13: p=q1^q2 by FINSEQ_2:25;
rng p c=REAL;
then A14: p is FinSequence of REAL by FINSEQ_1:def 4;
then A15: q1 is FinSequence of REAL by A13,FINSEQ_1:50;
A16: q2 is FinSequence of REAL by A13,A14,FINSEQ_1:50;
reconsider q1 as Element of Euclid n by A11,A15,TOPREAL7:17;
reconsider q2 as Element of Euclid 1 by A12,A16,TOPREAL7:17;
A17: f is continuous by A8,TOPS_2:def 5;
reconsider Bn=cl_Ball(q1,r*sqrt(n)) as Subset of TRn by TOPREAL3:13;
reconsider B1=cl_Ball(q2,r*sqrt(1)) as Subset of TR1 by TOPREAL3:13;
Ball(q2,r*sqrt(1))c=B1 & OpenHypercube(q2,r)c=Ball(q2,r*sqrt(1)) by
EUCLID_9:18,METRIC_1:15;
then A18: OpenHypercube(q2,r)c=B1 by XBOOLE_1:1;
Ball(q1,r*sqrt(n))c=Bn & OpenHypercube(q1,r)c=Ball(q1,r*sqrt(n)) by A3,
EUCLID_9:18,METRIC_1:15;
then OpenHypercube(q1,r)c=Bn by XBOOLE_1:1;
then A19: [:OpenHypercube(q1,r),OpenHypercube(q2,r):]c=[:Bn,B1:] by A18,
ZFMISC_1:119;
cl_Ball(q2,r*sqrt(1)) is bounded by TOPREAL6:67;
then B1 is Bounded by JORDAN2C:def 2;
then A20: B1 is compact by Lm4,TOPREAL6:66;
cl_Ball(q1,r*sqrt(n)) is bounded by TOPREAL6:67;
then Bn is Bounded by JORDAN2C:def 2;
then Bn is compact by A2,A7,TOPREAL6:66;
then A21: [:Bn,B1:] is compact Subset of[:TRn,TR1:] by A20,BORSUK_3:27;
rng f=[#]TRn1 by A8,TOPGRP_1:24;
then A22: f.:(f"A)=A by FUNCT_1:147;
f.:[:OpenHypercube(q1,r),OpenHypercube(q2,r):]=OpenHypercube(p,r) by A9,A11
,A13,Th20;
then A23: f"A c=[:OpenHypercube(q1,r),OpenHypercube(q2,r):] by A6,A10,A22,
FUNCT_1:157;
f"A is closed by A4,A8,TOPGRP_1:24;
then f"A is compact by A19,A21,A23,COMPTS_1:18,XBOOLE_1:1;
hence thesis by A17,A22,WEIERSTR:14;
end;
end;
A24: P[0];
for n holds P[n] from NAT_1:sch 2(A24,A1);
hence thesis;
end;
registration
let n;
cluster closed Bounded -> compact 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 13;
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:77;
then A6: dom E=dom F by A1,FINSEQ_3:31;
set En=Euclid n;
set Comp=Complex_of{A};
defpred P[set,set] 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:18;
then reconsider CrF=COMPLEMENT(rng F) as Subset-Family of TopSpaceMetr(En|ca)
by A7,PRE_TOPC:66;
CA is compact by A7,COMPTS_1:33;
then A9: TopSpaceMetr(En|ca) is compact by A8,COMPTS_1:12;
A10: (TopSpaceMetr En)|CA=TRn|cA by A7,PRE_TOPC:66;
assume meet rng F is empty;
then [#](TRn|cA)=(meet rng F)`
.=union CrF by A4,TOPS_2:12;
then A11: CrF is Cover of TopSpaceMetr(En|ca) by A8,A10,SETFAM_1:60;
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:113;
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:28;
not w in Carrier fvA by A75,A80;
hence vA.w=fvA.w by A81,RLVECT_2:28;
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 11;
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 has_a_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 set 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 set;
assume y in rng h;
then consider x be set such that
A36: x in dom h and
A37: h.x=y by FUNCT_1:def 5;
reconsider x as Nat by A36;
p.x in rng p by A35,A33,A36,FUNCT_1:def 5;
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 set;
assume x in the carrier of TRC;
then x in union G by A24,SETFAM_1:60;
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 set such that
A44: k in dom f and
A45: f.k=z by A42,FUNCT_1:def 5;
reconsider k as Nat by A44;
A46: k>=1 by A44,FINSEQ_3:27;
A47: len E>=k by A5,A44,FINSEQ_3:27;
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:3;
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 5;
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:27;
then A65: h.m in rng h by A35,A33,FUNCT_1:def 5;
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:27;
then p.m1=p/.m1 by PARTFUN1:def 8;
then A68: not y in p.m1 by A66,A63;
p.m=p/.m by A64,PARTFUN1:def 8;
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 12;
now let A be Subset of TRC;
assume A in rng h;
then consider k be set such that
A71: k in dom h and
A72: h.k=A by FUNCT_1:def 5;
reconsider k as Nat by A71;
A73: k>=1 by A33,A71,FINSEQ_1:3;
per cases by A73,XXREAL_0:1;
suppose A74: k=1;
A75: G0 c=G
proof
let x be set;
assume x in G0;
hence thesis by A27;
end;
h.k=union G0 by A33,A34,A71,A74;
hence A is open by A23,A72,A75,TOPS_2:18,26;
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:3;
then A78: k1=1 by FINSEQ_1:3;
A95: H[k,h.k] by A34,A93;
assume h.k meets conv(A\{E.k});
then consider x be set 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:3;
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:27;
then A105: p/.k1=p.k1 by PARTFUN1:def 8;
A106: p/.k=p.k by A35,A93,PARTFUN1:def 8;
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 set;
assume A111: x in carr;
union gx=carr & union gx c=union cgx by A84,PCOMPS_1:22,SETFAM_1:60;
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 set such that
A116: k in dom h and
A117: h.k=r by A114,FUNCT_1:def 5;
A118: G[k,GX.k] by A33,A88,A116;
A119: GX.k in rng GX by A33,A88,A116,FUNCT_1:def 5;
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 12;
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:146;
A123: union rng GX=carr by A120,SETFAM_1:60;
per cases by XBOOLE_0:def 10;
suppose S=dom GX;
hence thesis by A6,A9,A91,A88,A122,A123,RELAT_1:146;
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 set 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 set such that
A131: i in dom GX and
A132: i in dom E\S and
A133: GX.i=y by A130,FUNCT_1:def 12;
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:8;
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:153;
then A135: union(GX.:S)\/union(GX.:(dom E\S)) =C by A6,A123,ZFMISC_1:96;
conv(E.:S)c=C by A9,RELAT_1:144,RLAFFIN1:3;
hence thesis by A125,A135,A126,XBOOLE_1:73;
end;
end;
A136: cgx is locally_finite by A86,PCOMPS_1:21;
now let A be Subset of TRC;
assume A in rng GX;
then consider k be set such that
A137: k in dom GX & GX.k=A by FUNCT_1:def 5;
set U={u where u is Subset of TRC:u in cgx & u c=h.k};
A138: U c=cgx
proof
let x be set;
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:14,TOPS_2:19;
then union U is closed by A136,A138,PCOMPS_1:12,24;
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 set 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:3;
A144: k<=len E by A142,FINSEQ_1:3;
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 5;
then meet rng GX c=GX.k by SETFAM_1:8;
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:3;
then A148: p.1=G0 by A1,A9,A30,FINSEQ_4:77,PARTFUN1:def 8;
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 by NAT_1:20;
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 8;
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:3;
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 set;
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;