:: Abstract Simplicial Complexes
:: by Karol P\c{a}k
::
:: Received December 18, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_1, XBOOLE_0, CARD_1, CLASSES1, COHSP_1, FINSET_1, FUNCT_1,
GROUP_4, INT_1, MATROID0, ORDERS_1, PARTFUN1, PRE_TOPC, RELAT_1, RELAT_2,
NUMBERS, SETFAM_1, SGRAPH1, SUBSET_1, TARSKI, TRIANG_1, WELLORD1,
ZFMISC_1, SIMPLEX0, XXREAL_0, NAT_1, ORDINAL1, FUNCOP_1, ARYTM_3,
RCOMP_1, STRUCT_0, GLIB_000, REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, RELAT_2, FUNCT_1,
FUNCT_2, ORDINAL1, NUMBERS, WELLORD1, ORDERS_1, FINSET_1, CARD_1,
XCMPLX_0, XREAL_0, XXREAL_0, INT_1, XXREAL_3, NAT_1, SETFAM_1, DOMAIN_1,
STRUCT_0, PRE_TOPC, TOPS_2, PENCIL_1, CLASSES1, MATROID0, RELSET_1,
COHSP_1, FUNCOP_1;
constructors SETFAM_1, XXREAL_3, REAL_1, TOPS_2, BORSUK_1, WELLORD1, BINOP_2,
CLASSES1, COH_SP, MATROID0, COHSP_1, FUNCOP_1, NAT_1;
registrations PRE_TOPC, CARD_1, COHSP_1, FIB_NUM2, FINSET_1, FUNCT_1, INT_1,
MATROID0, NAT_1, ORDINAL1, PENCIL_1, RELAT_1, SETFAM_1, SUBSET_1,
STRUCT_0, XBOOLE_0, XREAL_0, XXREAL_0, XXREAL_3, FUNCOP_1, RELSET_1;
requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
definitions CLASSES1, FINSET_1, MATROID0, ORDINAL1, SETFAM_1, TARSKI, TOPS_2,
XBOOLE_0;
equalities MATROID0, ORDINAL1, STRUCT_0, SUBSET_1, XXREAL_3;
expansions CLASSES1, FINSET_1, MATROID0, ORDINAL1, SETFAM_1, TARSKI, TOPS_2,
XBOOLE_0;
theorems CARD_1, CARD_2, CLASSES1, COHSP_1, COMBGRAS, FINSET_1, FUNCT_1,
FUNCT_2, FUNCOP_1, INT_1, MATROID0, NAT_1, ORDERS_1, ORDINAL1, PENCIL_1,
PRE_TOPC, RELAT_1, RELAT_2, SETFAM_1, STIRL2_1, SUBSET_1, WELLORD1,
WELLORD2, TARSKI, TOPS_2, XREAL_0, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0,
XXREAL_3, ZFMISC_1;
schemes CLASSES1, FRAENKEL, FUNCT_2, NAT_1;
begin :: Preliminaries
reserve x,y, X,Y,Z for set,
D for non empty set,
n,k for Nat,
i,i1,i2 for Integer;
notation let X;
antonym X is with_empty_element for X is with_non-empty_elements;
end;
registration
cluster empty -> subset-closed for set;
coherence;
cluster with_empty_element -> non empty for set;
coherence;
cluster non empty subset-closed -> with_empty_element for set;
coherence
proof
let X;
assume A1: X is non empty subset-closed;
then consider x being object such that
A2: x in X;
reconsider x as set by TARSKI:1;
{}c=x;
then {} in X by A1,A2;
hence thesis;
end;
end;
registration
let X;
cluster Sub_of_Fin X -> finite-membered;
coherence
by COHSP_1:def 3;
end;
registration
let X be subset-closed set;
cluster Sub_of_Fin X -> subset-closed;
coherence;
end;
theorem
Y is subset-closed iff for X st X in Y holds bool X c= Y
proof
thus Y is subset-closed implies for X st X in Y holds bool X c=Y;
assume A1: for X st X in Y holds bool X c=Y;
let x,y;
assume that
A2: x in Y and
A3: y c=x;
A4: y in bool x by A3;
bool x c=Y by A1,A2;
hence thesis by A4;
end;
registration
let A,B be subset-closed set;
cluster A \/ B -> subset-closed;
coherence
proof
let x,y;
assume that
A1: x in A\/B and
A2: y c=x;
x in A or x in B by A1,XBOOLE_0:def 3;
then y in A or y in B by A2,CLASSES1:def 1;
hence y in A\/B by XBOOLE_0:def 3;
end;
cluster A /\ B -> subset-closed;
coherence
proof
let x,y;
assume that
A3: x in A/\B and
A4: y c=x;
x in B by A3,XBOOLE_0:def 4;
then A5: y in B by A4,CLASSES1:def 1;
x in A by A3,XBOOLE_0:def 4;
then y in A by A4,CLASSES1:def 1;
hence y in A/\B by A5,XBOOLE_0:def 4;
end;
end;
Lm1: for X ex F be subset-closed set st F=union{bool x where x is Element of X:
x in X} & X c=F & for Y st X c=Y & Y is subset-closed holds F c=Y
proof
let X;
set B={bool x where x is Element of X:x in X};
now let a,b be set such that
A1: a in union B and
A2: b c=a;
consider y such that
A3: a in y and
A4: y in B by A1,TARSKI:def 4;
consider x be Element of X such that
A5: y=bool x and
x in X by A4;
b c=x by A2,A3,A5,XBOOLE_1:1;
hence b in union B by A4,A5,TARSKI:def 4;
end;
then reconsider U=union B as subset-closed set by CLASSES1:def 1;
take U;
thus U=union B;
thus X c=U
proof
let x be object such that
A6: x in X;
reconsider xx=x as set by TARSKI:1;
xx c=xx & bool xx in B by A6;
hence thesis by TARSKI:def 4;
end;
let Y such that
A7: X c=Y & Y is subset-closed;
let x be object;
assume x in U;
then consider y such that
A8: x in y and
A9: y in B by TARSKI:def 4;
ex x be Element of X st y=bool x & x in X by A9;
hence x in Y by A7,A8;
end;
definition
let X;
func subset-closed_closure_of X -> subset-closed set means :Def1:
X c= it & for Y st X c= Y & Y is subset-closed holds it c= Y;
existence
proof
ex F be subset-closed set st F=union{bool x where x is Element of X:x in X} &
X c=F & for Y st X c=Y & Y is subset-closed holds F c=Y by Lm1;
hence thesis;
end;
uniqueness;
end;
theorem Th2:
x in subset-closed_closure_of X iff ex y st x c= y & y in X
proof
set B={bool x1 where x1 is Element of X:x1 in X};
consider F be subset-closed set such that
A1: F=union B and
A2: X c=F & for Y st X c=Y & Y is subset-closed holds F c=Y by Lm1;
A3: F=subset-closed_closure_of X by A2,Def1;
hereby assume x in subset-closed_closure_of X;
then consider y such that
A4: x in y and
A5: y in B by A1,A3,TARSKI:def 4;
consider x1 be Element of X such that
A6: bool x1=y & x1 in X by A5;
reconsider y=x1 as set;
take y;
thus x c=y & y in X by A4,A6;
end;
given y such that
A7: x c=y and
A8: y in X;
bool y in B by A8;
hence thesis by A1,A3,A7,TARSKI:def 4;
end;
definition
let X;
let F be Subset-Family of X;
redefine func subset-closed_closure_of F -> subset-closed Subset-Family of X; :: redefines subset-closed_closure_of (SIMPLEX0, definition)
coherence
proof
set FIC=subset-closed_closure_of F;
FIC c=bool X
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in FIC;
then ex y st xx c=y & y in F by Th2;
then xx c=X by XBOOLE_1:1;
hence thesis;
end;
hence thesis;
end;
end;
registration
cluster subset-closed_closure_of {} -> empty;
coherence
proof
assume subset-closed_closure_of{} is non empty;
then consider x be object such that
A1: x in subset-closed_closure_of{};
reconsider x as set by TARSKI:1;
ex y st x c=y & y in {} by A1,Th2;
hence thesis;
end;
let X be non empty set;
cluster subset-closed_closure_of X -> non empty;
coherence
proof
ex x being object st x in X by XBOOLE_0:def 1;
hence thesis by Th2;
end;
end;
registration
let X be with_non-empty_element set;
cluster subset-closed_closure_of X -> with_non-empty_element;
coherence
proof
consider b be non empty set such that
A1: b in X by SETFAM_1:def 10;
b in subset-closed_closure_of X by A1,Th2;
hence thesis;
end;
end;
registration
let X be finite-membered set;
cluster subset-closed_closure_of X -> finite-membered;
coherence
proof
let x be set;
assume x in subset-closed_closure_of X;
then consider y such that
A1: x c=y and
A2: y in X by Th2;
y is finite by A2;
hence thesis by A1;
end;
end;
theorem Th3:
X c=Y & Y is subset-closed implies subset-closed_closure_of X c= Y
proof
assume A1: X c=Y & Y is subset-closed;
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in subset-closed_closure_of X;
then ex y st xx c=y & y in X by Th2;
hence thesis by A1;
end;
theorem Th4:
subset-closed_closure_of {X} = bool X
proof
set f=subset-closed_closure_of{X};
A1: X in {X} by TARSKI:def 1;
hereby let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in f;
then consider y such that
A2: xx c=y and
A3: y in {X} by Th2;
y=X by A3,TARSKI:def 1;
hence x in bool X by A2;
end;
let x be object;
assume x in bool X;
hence thesis by A1,Th2;
end;
theorem
subset-closed_closure_of (X\/Y) =
subset-closed_closure_of X \/ subset-closed_closure_of Y
proof
set fxy=subset-closed_closure_of(X\/Y);
set fx=subset-closed_closure_of X;
set fy=subset-closed_closure_of Y;
hereby let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in fxy;
then consider y such that
A1: xx c=y and
A2: y in X\/Y by Th2;
y in X or y in Y by A2,XBOOLE_0:def 3;
then x in fx or x in fy by A1,Th2;
hence x in fx\/fy by XBOOLE_0:def 3;
end;
let x be object;
reconsider xx=x as set by TARSKI:1;
assume A3: x in fx\/fy;
per cases by A3,XBOOLE_0:def 3;
suppose x in fx;
then consider y such that
A4: xx c=y and
A5: y in X by Th2;
y in X\/Y by A5,XBOOLE_0:def 3;
hence thesis by A4,Th2;
end;
suppose x in fy;
then consider y such that
A6: xx c=y and
A7: y in Y by Th2;
y in X\/Y by A7,XBOOLE_0:def 3;
hence thesis by A6,Th2;
end;
end;
theorem Th6:
X is_finer_than Y iff
subset-closed_closure_of X c= subset-closed_closure_of Y
proof
set fx=subset-closed_closure_of X;
set fy=subset-closed_closure_of Y;
hereby assume A1: X is_finer_than Y;
thus fx c=fy
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in fx;
then consider y such that
A2: xx c=y and
A3: y in X by Th2;
consider c be set such that
A4: c in Y and
A5: y c=c by A1,A3;
xx c=c by A2,A5;
hence thesis by A4,Th2;
end;
end;
assume A6: fx c=fy;
let x;
assume x in X;
then x in fx by Th2;
then ex y st x c=y & y in Y by A6,Th2;
hence thesis;
end;
theorem Th7:
X is subset-closed implies subset-closed_closure_of X = X
by Def1;
theorem
subset-closed_closure_of X c= X implies X is subset-closed
proof
set f=subset-closed_closure_of X;
assume A1: f c=X;
let x,y;
assume x in X & y c=x;
then y in f by Th2;
hence y in X by A1;
end;
definition
let Y,X;
let n be set;::Cardinal;
func the_subsets_with_limited_card(n,X,Y) -> Subset-Family of Y means :Def2:
for A be Subset of Y holds A in it iff A in X & card A c= n;
existence
proof
set SS={A where A is Subset of Y:A in X & card A c= n};
SS c=bool Y
proof
let x be object;
assume x in SS;
then ex A be Subset of Y st x=A & A in X & card A c= n;
hence thesis;
end;
then reconsider SS as Subset-Family of Y;
take SS;
let A be Subset of Y;
hereby assume A in SS;
then ex B be Subset of Y st B=A & B in X & card B c= n;
hence A in X & card A c= n;
end;
assume A in X & card A c= n;
hence thesis;
end;
uniqueness
proof
let S1,S2 be Subset-Family of Y;
assume that
A1: for A be Subset of Y holds A in S1 iff A in X & card A c= n and
A2: for A be Subset of Y holds A in S2 iff A in X & card A c= n;
thus S1 c=S2
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume A3: x in S1;
then x in X & card xx c= n by A1;
hence thesis by A2,A3;
end;
let x be object;
reconsider xx=x as set by TARSKI:1;
assume A4: x in S2;
then x in X & card xx c= n by A2;
hence thesis by A1,A4;
end;
end;
registration
let D;
cluster finite with_non-empty_element subset-closed
finite-membered for Subset-Family of D;
existence
proof
consider x be object such that
A1: x in D by XBOOLE_0:def 1;
{x}c=D by A1,ZFMISC_1:31;
then reconsider XX=bool{x} as Subset-Family of D by ZFMISC_1:67;
take XX;
{x} in bool{x} by ZFMISC_1:def 1;
hence thesis;
end;
end;
registration
let Y,X;
let n be finite Cardinal;
cluster the_subsets_with_limited_card(n,X,Y) -> finite-membered;
coherence
proof
let A be set;
assume A in the_subsets_with_limited_card(n,X,Y);
then card A c=card n by Def2;
hence thesis;
end;
end;
registration
let Y;
let X be subset-closed set;
let n be Cardinal;
cluster the_subsets_with_limited_card(n,X,Y) -> subset-closed;
coherence
proof
let x,y;
assume that
A1: x in the_subsets_with_limited_card(n,X,Y) and
A2: y c=x;
x in X by A1,Def2;
then A3: y in X by A2,CLASSES1:def 1;
card x c=card n & card y c=card x by A1,A2,Def2,CARD_1:11;
then A4: card y c=card n;
y c=Y by A1,A2,XBOOLE_1:1;
hence thesis by A3,A4,Def2;
end;
end;
registration
let Y;
let X be with_empty_element set;
let n be Cardinal;
cluster the_subsets_with_limited_card(n,X,Y) -> with_empty_element;
coherence
proof
A1: {}c=Y;
card{}c=card n & {} in X by SETFAM_1:def 8;
then {} in the_subsets_with_limited_card(n,X,Y) by A1,Def2;
hence thesis;
end;
end;
registration
let D;
let X be with_non-empty_element subset-closed Subset-Family of D;
let n be non empty Cardinal;
cluster the_subsets_with_limited_card(n,X,D) -> with_non-empty_element;
coherence
proof
consider x be non empty set such that
A1: x in X by SETFAM_1:def 10;
consider y be object such that
A2: y in x by XBOOLE_0:def 1;
{}c=card n;
then {} in card n by CARD_1:3;
then 1 c=card n by CARD_2:68;
then A3: card{y}c=card n by CARD_1:30;
{y}c=x by A2,ZFMISC_1:31;
then {y} in X by A1,CLASSES1:def 1;
then {y} in the_subsets_with_limited_card(n,X,D) by A3,Def2;
hence thesis;
end;
end;
notation let X;
let Y be Subset-Family of X;
let n be set;::Cardinal;
synonym the_subsets_with_limited_card(n,Y)
for the_subsets_with_limited_card(n,Y,X);
end;
theorem Th9:
X is non empty finite c=-linear implies union X in X
proof
assume X is non empty finite c=-linear;
then consider U be set such that
A1: U in X and
A2: for x st x in X holds x c=U by FINSET_1:12;
A3: union X c=U
proof
let x be object;
assume x in union X;
then consider y such that
A4: x in y and
A5: y in X by TARSKI:def 4;
y c=U by A2,A5;
hence thesis by A4;
end;
U c=union X by A1,ZFMISC_1:74;
hence thesis by A1,A3,XBOOLE_0:def 10;
end;
theorem Th10:
for X be finite c=-linear set st X is with_non-empty_elements
holds card X c= card union X
proof
let X be finite c=-linear set;
defpred P[Nat] means
for X be finite c=-linear set
st X is with_non-empty_elements & card union X=$1
holds card X c=card union X;
defpred Q[Nat] means
for n be Nat st n<=$1 holds P[n];
assume A1: X is with_non-empty_elements;
A2: for m be Nat st Q[m] holds Q[m+1]
proof
let m be Nat such that
A3: Q[m];
let n be Nat;
assume A4: n<=m+1;
let X be finite c=-linear set such that
A5: X is with_non-empty_elements and
A6: card union X=n;
reconsider u=union X as finite set by A6;
reconsider Xu=X\{u} as finite c=-linear set;
per cases by A4,NAT_1:8;
suppose n<=m;
hence thesis by A3,A5,A6;
end;
suppose A7: n=m+1;
then X is non empty by A6,ZFMISC_1:2;
then A8: X=Xu\/{u} by Th9,ZFMISC_1:116;
then u=union Xu\/union{u} by ZFMISC_1:78
.=union Xu\/u by ZFMISC_1:25;
then A9: union Xu c=u by XBOOLE_1:11;
then reconsider uXu=union Xu as finite set;
uXu<>u
proof
assume A10: uXu=u;
then Xu is non empty by A6,A7,ZFMISC_1:2;
then u in Xu by A10,Th9;
hence thesis by ZFMISC_1:56;
end;
then A11: uXu c<u by A9;
then card uXu<m+1 by A6,A7,CARD_2:48;
then card uXu<=m by NAT_1:13;
then Segm card Xu c= Segm card uXu by A3,A5;
then card Xu<=card uXu by NAT_1:39;
then card Xu<card u by A11,CARD_2:48,XXREAL_0:2;
then
A12: 1+card Xu<=card u by NAT_1:13;
not u in Xu by ZFMISC_1:56;
then
A13: 1+card Xu=card X by A8,CARD_2:41;
Segm(1+card Xu) c= Segm card u by A12,NAT_1:39;
hence thesis by A13;
end;
end;
A14: Q[0]
proof
let n be Nat;
assume A15: n<=0;
let X be finite c=-linear set such that
A16: X is with_non-empty_elements & card union X=n;
X is empty by A15,A16;
hence card X c=card union X;
end;
for n be Nat holds Q[n] from NAT_1:sch 2(A14,A2);
hence thesis by A1;
end;
theorem
X is c=-linear implies X\/{union X\/x} is c=-linear
proof
assume that
A1: X is c=-linear;
set U=union X;
set Ux=U\/x;
A2: U c=Ux by XBOOLE_1:7;
let x1,x2 be set such that
A3: x1 in X\/{Ux} & x2 in X\/{Ux};
per cases by A3,XBOOLE_0:def 3;
suppose x1 in X & x2 in X;
hence thesis by A1;
end;
suppose A4: x1 in {Ux} & x2 in {Ux};
then x1=Ux by TARSKI:def 1;
hence thesis by A4,TARSKI:def 1;
end;
suppose x1 in X & x2 in {Ux};
then x1 c=U & x2=Ux by TARSKI:def 1,ZFMISC_1:74;
then x1 c=x2 by A2;
hence thesis;
end;
suppose x2 in X & x1 in {Ux};
then x2 c=U & x1=Ux by TARSKI:def 1,ZFMISC_1:74;
then x2 c=x1 by A2;
hence thesis;
end;
end;
theorem Th12:
for X be non empty set ex Y be Subset-Family of X st
Y is with_non-empty_elements c=-linear & X in Y & card X = card Y &
for Z st Z in Y & card Z <> 1 ex x st x in Z & Z\{x} in Y
proof
let X be non empty set;
consider R be Relation such that
A1: R well_orders X by WELLORD2:17;
set RX=R|_2 X;
deffunc F(object)=X\(RX-Seg($1));
A2: for x being object st x in X holds F(x) in bool X;
consider f be Function of X,bool X such that
A3: for x being object st x in X holds f.x=F(x) from FUNCT_2:sch 2(A2);
take Y=rng f;
A4: dom f=X by FUNCT_2:def 1;
thus Y is with_non-empty_elements
proof
assume Y is with_empty_element;
then {} in Y;
then consider x being object such that
A5: x in dom f and
A6: f.x={} by FUNCT_1:def 3;
{}=F(x) by A3,A5,A6;
then X c=RX-Seg(x) by XBOOLE_1:37;
hence thesis by A4,A5,WELLORD1:1;
end;
thus Y is c=-linear
proof
let x,y;
assume that
A7: x in Y and
A8: y in Y;
consider a be object such that
A9: a in dom f & f.a=x by A7,FUNCT_1:def 3;
consider b be object such that
A10: b in dom f & f.b=y by A8,FUNCT_1:def 3;
RX-Seg(a),RX-Seg(b)are_c=-comparable by A1,WELLORD1:26,WELLORD2:16;
then RX-Seg(a)c=RX-Seg(b) or RX-Seg(b)c=RX-Seg(a);
then F(b)c=F(a) or F(a)c=F(b) by XBOOLE_1:34;
then A11: F(a),F(b)are_c=-comparable;
x=F(a) by A3,A9;
hence thesis by A3,A10,A11;
end;
A12: field RX=X by A1,WELLORD2:16;
then consider x being object such that
A13: x in X and
A14: for y being object st y in X holds[x,y] in RX
by A1,WELLORD1:7,WELLORD2:16;
A15: RX is well-ordering by A1,WELLORD2:16;
then A16: RX is well_founded by WELLORD1:def 4;
RX is antisymmetric by A15,WELLORD1:def 4;
then A17: RX is_antisymmetric_in X by A12,RELAT_2:def 12;
A18: RX-Seg(x)={}
proof
assume RX-Seg(x)<>{};
then consider y being object such that
A19: y in RX-Seg(x) by XBOOLE_0:def 1;
A20: y<>x by A19,WELLORD1:1;
A21: [y,x] in RX by A19,WELLORD1:1;
then A22: x in X by A12,RELAT_1:15;
A23: y in X by A12,A21,RELAT_1:15;
then [x,y] in RX by A14;
hence thesis by A17,A20,A21,A22,A23,RELAT_2:def 4;
end;
f.x=F(x) by A3,A13;
hence X in Y by A4,A13,A18,FUNCT_1:def 3;
now let x1,x2 be object;
reconsider R1=RX-Seg(x1),R2=RX-Seg(x2) as Subset of X by A12,WELLORD1:9;
assume that
A24: x1 in X & x2 in X and
A25: f.x1=f.x2;
R1`=f.x1 & f.x2=R2` by A3,A24;
then R1=R2 by A25,SUBSET_1:42;
then [x1,x2] in RX & [x2,x1] in RX by A12,A15,A24,WELLORD1:29;
hence x1=x2 by A17,A24,RELAT_2:def 4;
end;
then f is one-to-one by FUNCT_2:19;
then X,Y are_equipotent by A4,WELLORD2:def 4;
hence card X=card Y by CARD_1:5;
let Z;
assume that
A26: Z in Y and
A27: card Z<>1;
consider x being object such that
A28: x in dom f and
A29: f.x=Z by A26,FUNCT_1:def 3;
A30: {x}c=X by A28,ZFMISC_1:31;
reconsider x as set by TARSKI:1;
take x;
A31: not x in RX-Seg(x) by WELLORD1:1;
A32: Z=X\(RX-Seg(x)) by A3,A28,A29;
hence x in Z by A28,A31,XBOOLE_0:def 5;
RX-Seg(x)c=X by A12,WELLORD1:9;
then reconsider Rxx=RX-Seg(x)\/{x} as Subset of X by A30,XBOOLE_1:8;
X\Rxx<>{}
proof
assume X\Rxx={};
then X c=Rxx by XBOOLE_1:37;
then Z=Rxx\RX-Seg(x) by A32,XBOOLE_0:def 10
.={x}\RX-Seg(x) by XBOOLE_1:40
.={x} by A31,ZFMISC_1:59;
hence contradiction by A27,CARD_1:30;
end;
then consider a be object such that
A33: a in Rxx` and
A34: RX-Seg(a)misses Rxx` by A12,A16,WELLORD1:def 2;
A35: not a in Rxx by A33,XBOOLE_0:def 5;
x in {x} by TARSKI:def 1;
then A36: x<>a by A35,XBOOLE_0:def 3;
RX is connected by A15,WELLORD1:def 4;
then RX is_connected_in X by A12,RELAT_2:def 14;
then A37: [x,a] in RX or[a,x] in RX by A28,A33,A36,RELAT_2:def 6;
A38: not a in RX-Seg(x) by A35,XBOOLE_0:def 3;
then x in RX-Seg(a) by A36,A37,WELLORD1:1;
then A39: {x}c=RX-Seg(a) by ZFMISC_1:31;
RX-Seg(a)c=X by A12,WELLORD1:9;
then A40: RX-Seg(a)c=Rxx by A34,SUBSET_1:24;
RX-Seg(x)c=RX-Seg(a) by A12,A15,A28,A33,A37,A38,WELLORD1:1,29;
then Rxx c=RX-Seg(a) by A39,XBOOLE_1:8;
then Rxx=RX-Seg(a) by A40;
then f.a=X\Rxx by A3,A33
.=(X\RX-Seg(x))\{x} by XBOOLE_1:41
.=Z\{x} by A3,A28,A29;
hence thesis by A4,A33,FUNCT_1:def 3;
end;
theorem
for Y be Subset-Family of X st
Y is finite with_non-empty_elements c=-linear & X in Y
ex Y1 be Subset-Family of X st
Y c= Y1 & Y1 is with_non-empty_elements c=-linear & card X = card Y1 &
for Z st Z in Y1 & card Z <> 1 ex x st x in Z & Z\{x} in Y1
proof
let Y be Subset-Family of X such that
A1: Y is finite with_non-empty_elements c=-linear and
A2: X in Y;
defpred P[object,object] means
ex A being set st A = $2 &
$1 in A & $2 in Y & for y st y in Y & $1 in y holds A c= y;
A3: for x being object st x in X ex y being object st P[x,y]
proof
let x be object;
set U={A where A is Subset of X:x in A & A in Y};
A4: U c=Y
proof
let y be object;
assume y in U;
then ex A be Subset of X st y=A & x in A & A in Y;
hence thesis;
end;
then reconsider U as Subset-Family of X by XBOOLE_1:1;
assume x in X;
then X in U by A2;
then consider m be set such that
A5: m in U and
A6: for y st y in U holds m c=y by A1,A4,FINSET_1:11;
take m;
consider A be Subset of X such that
A7: m=A & x in A & A in Y by A5;
take A;
thus A = m by A7;
thus x in A & m in Y by A7;
let y;
assume y in Y & x in y;
then y in U;
hence thesis by A6,A7;
end;
consider f be Function such that
A8: dom f=X &
for x being object st x in X holds P[x,f.x] from CLASSES1:sch 1(A3);
defpred Q[object,object] means
ex D1,D2 being set st D1 = $1 & D2 = $2 &
(D2 in Y or D2 is empty) & D2 c<D1 &
(for x st x in Y & x c<D1 holds x c=D2) &
(for x st x in Y & D2 c=x & x c= D1 holds x=D1 or x=D2);
A9: for x being object st x in Y ex y being object st y in bool X & Q[x,y]
proof
let x be object;
reconsider xx = x as set by TARSKI:1;
assume A10: x in Y;
set U={A where A is Subset of X:A c<xx & A in Y};
A11: U c=Y
proof
let y be object;
assume y in U;
then ex A be Subset of X st y=A & A c<xx & A in Y;
hence thesis;
end;
then reconsider U as Subset-Family of X by XBOOLE_1:1;
take u=union U;
thus u in bool X;
A12: for y st y in Y & y c<xx holds y c=u
proof
let y;
assume that
A13: y in Y and
A14: y c<xx;
y in U by A13,A14;
hence thesis by ZFMISC_1:74;
end;
per cases;
suppose
A15: U is empty;
take xx,u;
thus xx = x & u = u;
thus (u in Y or u is empty) & u c<xx & for y st y in Y & y c<xx holds y
c=u by A1,A10,A12,A15,XBOOLE_1:61,ZFMISC_1:2;
let y;
assume that
A16: y in Y and
A17: u c=y and
A18: y c=xx;
assume y<>xx;
then y c<xx by A18;
then y c=u by A12,A16;
hence thesis by A17;
end;
suppose U is non empty;
then u in U by A1,A11,Th9;
then
A19:ex A be Subset of X st A=u & A c<xx & A in Y;
take xx,u;
thus xx = x & u = u;
thus (u in Y or u is empty) & u c<xx & for y st y in Y & y c<xx holds y
c=u by A12,A19;
let y;
assume that
A20: y in Y and
A21: u c=y and
A22: y c=xx;
assume y<>xx;
then y c<xx by A22;
then y c=u by A12,A20;
hence thesis by A21;
end;
end;
consider g be Function of Y,bool X such that
A23: for x being object st x in Y holds Q[x,g.x] from FUNCT_2:sch 1(A9);
defpred R[object,object] means
ex A being set,
h be Function of A\(g.A),bool(A\(g.A))
st A = $1 & $2=h & h is one-to-one & rng
h is with_non-empty_elements c=-linear & dom h in rng h & for Z st Z in rng h &
card Z<>1 ex x st x in Z & Z\{x} in rng h;
A24: for x being object st x in Y ex y being object st R[x,y]
proof
let y be object;
assume
A25: y in Y;
reconsider y as set by TARSKI:1;
Q[y,g.y] by A23,A25;
then g.y c<y;
then y\(g.y)<>{} by XBOOLE_1:105;
then consider Z be Subset-Family of y\(g.y) such that
A26: Z is with_non-empty_elements c=-linear & y\(g.y) in Z and
A27: card(y\g.y)=card Z and
A28: for z be set st z in Z & card z<>1 ex x st x in z & z\{x} in Z by Th12
;
y\g.y,Z are_equipotent by A27,CARD_1:5;
then consider h be Function such that
A29: h is one-to-one and
A30: dom h=y\g.y & rng h=Z by WELLORD2:def 4;
reconsider h as Function of y\g.y,bool(y\g.y) by A30,FUNCT_2:2;
take h;
thus thesis by A26,A28,A29,A30;
end;
consider h be Function such that
A31: dom h=Y &
for x being object st x in Y holds R[x,h.x] from CLASSES1:sch 1(A24);
now let x be object;
assume x in dom h;
then R[x,h.x] by A31;
hence h.x is Function;
end;
then reconsider h as Function-yielding Function by FUNCOP_1:def 6;
deffunc Z(object)=g.(f.$1)\/(h.(f.$1)).$1;
A32: for x st x in X holds x in (f.x)\(g.(f.x))
proof
let x;
assume x in X;
then
A33: P[x,f.x] by A8;
then A34: f.x in Y;
assume A35: not x in (f.x)\(g.(f.x));
x in f.x by A33;
then A36: x in g.(f.x) by A35,XBOOLE_0:def 5;
A37: Q[f.x,g.(f.x)] by A23,A34;
then g.(f.x) in Y by A36;
then A38: f.x c=g.(f.x) by A36,A33;
g.(f.x)c<f.x by A37;
hence thesis by A38,XBOOLE_0:def 8;
end;
A39: for x being object st x in X holds Z(x) in bool X
proof
let x be object;
set fx=f.x;
assume A40: x in X;
then
P[x,f.x] by A8;
then A41: fx in Y;
then R[fx,h.fx] by A31;
then consider A being set,
H be Function of fx\(g.fx),bool(fx\(g.fx)) such that
A42: h.fx=H and
H is one-to-one and
rng H is with_non-empty_elements c=-linear and
dom H in rng H and
for Z st Z in rng H & card Z<>1 ex x st x in Z & Z\{x} in rng H;
A43: x in fx\(g.fx) by A32,A40;
dom H=fx\(g.fx) by FUNCT_2:def 1;
then H.x in rng H by A43,FUNCT_1:def 3;
then H.x c=fx by XBOOLE_1:1;
then A44: H.x c=X by A41,XBOOLE_1:1;
Q[fx,g.fx] by A23,A41;
then g.fx in Y or g.fx is empty;
then Z(x)c=X by A42,A44,XBOOLE_1:8;
hence thesis;
end;
consider z be Function of X,bool X such that
A45: for x being object st x in X holds z.x=Z(x) from FUNCT_2:sch 2(A39);
A46: dom z=X by FUNCT_2:def 1;
A47: Y c=rng z
proof
let y be object;
reconsider yy=y as set by TARSKI:1;
assume A48: y in Y;
then R[y,h.y] by A31;
then consider H be Function of yy\(g.y),bool(yy\(g.y)) such that
A49: h.y=H and
H is one-to-one and
rng H is with_non-empty_elements c=-linear and
A50: dom H in rng H and
for Z st Z in rng H & card Z<>1 ex x st x in Z & Z\{x} in rng H;
consider x being object such that
A51: x in dom H and
A52: H.x=dom H by A50,FUNCT_1:def 3;
A53: dom H=yy\(g.yy) by FUNCT_2:def 1;
then A54: x in yy by A51;
then
A55: P[x,f.x] by A8,A48;
then A56: x in f.x;
Q[y,g.y] by A23,A48;
then g.y c<yy;
then A57: g.y c=yy;
A58: f.x c=yy by A48,A54,A55;
A59: f.x in Y by A55;
f.x=y
proof
assume f.x<>y;
then
A60: f.x c<yy by A58;
Q[y,g.y] by A23,A48;
then f.x c=g.y by A59,A60;
hence contradiction by A51,A56,XBOOLE_0:def 5;
end;
then z.x=g.y\/(yy\(g.y)) by A45,A48,A49,A52,A53,A54
.=y by A57,XBOOLE_1:45;
hence thesis by A46,A48,A54,FUNCT_1:def 3;
end;
A61: for Z st Z in rng z & card Z<>1 ex x st x in Z & Z\{x} in rng z
proof
let Z;
assume that
A62: Z in rng z and
A63: card Z<>1;
consider x be object such that
A64: x in dom z and
A65: z.x=Z by A62,FUNCT_1:def 3;
set fx=f.x;
P[x,fx] by A8,A64;
then
A66: fx in Y;
then R[fx,h.fx] by A31;
then consider H be Function of fx\(g.fx),bool(fx\(g.fx)) such that
A67: h.fx=H and
H is one-to-one and
rng H is with_non-empty_elements c=-linear and
dom H in rng H and
A68: for Z st Z in rng H & card Z<>1 ex x st x in Z & Z\{x} in rng H;
A69: z.x=g.fx\/H.x by A45,A64,A67;
A70: dom H=fx\(g.fx) by FUNCT_2:def 1;
x in fx\(g.fx) by A32,A64;
then A71: H.x in rng H by A70,FUNCT_1:def 3;
per cases;
suppose A72: card(H.x)=1;
then
A73: g.fx<>{} by A63,A65,A69;
Q[fx,g.fx] by A23,A66;
then A74: g.fx in Y by A73;
consider a be object such that
A75: H.x={a} by A72,CARD_2:42;
reconsider a as set by TARSKI:1;
take a;
A76: a in H.x by A75,TARSKI:def 1;
then A77: not a in g.fx by A71,XBOOLE_0:def 5;
thus a in Z by A65,A69,A76,XBOOLE_0:def 3;
Z\{a}=(g.fx\/H.x)\H.x by A45,A64,A65,A67,A75
.=g.fx\H.x by XBOOLE_1:40
.=g.fx by A75,A77,ZFMISC_1:57;
hence thesis by A47,A74;
end;
suppose card(H.x)<>1;
then consider a be set such that
A78: a in H.x and
A79: H.x\{a} in rng H by A68,A71;
A80: not a in g.fx by A71,A78,XBOOLE_0:def 5;
take a;
thus a in Z by A65,A69,A78,XBOOLE_0:def 3;
consider b be object such that
A81: b in dom H and
A82: H.b=H.x\{a} by A79,FUNCT_1:def 3;
A83: b in fx by A70,A81;
then
A84: P[b,f.b] by A8,A66;
then A85: b in f.b;
A86: f.b in Y by A84;
A87: f.b c=fx by A66,A83,A84;
fx=f.b
proof
assume fx<>f.b;
then
A88: f.b c<fx by A87;
Q[fx,g.fx] by A23,A66;
then f.b c=g.fx by A86,A88;
hence contradiction by A81,A85,XBOOLE_0:def 5;
end;
then z.b=g.fx\/(H.x\{a}) by A45,A66,A67,A82,A83
.=(g.fx\/H.x)\{a} by A80,XBOOLE_1:87,ZFMISC_1:50
.=Z\{a} by A65,A45,A64,A67;
hence thesis by A46,A66,A83,FUNCT_1:def 3;
end;
end;
A89: rng z is c=-linear
proof
let y1,y2 be set;
assume that
A90: y1 in rng z and
A91: y2 in rng z;
consider x1 be object such that
A92: x1 in dom z and
A93: z.x1=y1 by A90,FUNCT_1:def 3;
consider x2 be object such that
A94: x2 in dom z and
A95: z.x2=y2 by A91,FUNCT_1:def 3;
set fx1=f.x1,fx2=f.x2;
A96: x1 in fx1\(g.fx1) by A32,A92;
P[x1,f.x1] by A8,A92;
then
A97: fx1 in Y;
then R[fx1,h.fx1] by A31;
then consider H1 be Function of fx1\(g.fx1),bool(fx1\(g.fx1)) such that
A98: h.fx1=H1 and
H1 is one-to-one and
rng H1 is with_non-empty_elements c=-linear and
dom H1 in rng H1 and
for Z st Z in rng H1 & card Z<>1 ex x st x in Z & Z\{x} in rng H1;
A99: z.x1=g.fx1\/H1.x1 by A45,A92,A98;
dom H1=fx1\(g.fx1) by FUNCT_2:def 1;
then A100: H1.x1 in rng H1 by A96,FUNCT_1:def 3;
A101: x2 in fx2\(g.fx2) by A32,A94;
P[x2,fx2] by A8,A94;
then
A102: fx2 in Y;
then R[fx2,h.fx2] by A31;
then consider H2 be Function of fx2\(g.fx2),bool(fx2\(g.fx2)) such that
A103: h.fx2=H2 and
H2 is one-to-one and
A104: rng H2 is with_non-empty_elements c=-linear and
dom H2 in rng H2 and
for Z st Z in rng H2 & card Z<>1 ex x st x in Z & Z\{x} in rng H2;
A105: z.x2=g.fx2\/H2.x2 by A45,A94,A103;
dom H2=fx2\(g.fx2) by FUNCT_2:def 1;
then A106: H2.x2 in rng H2 by A101,FUNCT_1:def 3;
A107: fx1,fx2 are_c=-comparable by A1,A97,A102;
per cases by A107;
suppose A108: fx1=fx2;
then H1.x1,H1.x2 are_c=-comparable by A98,A100,A103,A104,A106;
then H1.x1 c=H1.x2 or H1.x2 c=H1.x1;
then z.x1 c=z.x2 or z.x2 c=z.x1 by A98,A99,A103,A105,A108,XBOOLE_1:9;
hence thesis by A93,A95;
end;
suppose fx1 c=fx2 & fx1<>fx2;
then
A109: fx1 c<fx2;
Q[fx2,g.fx2] by A23,A102;
then A110: fx1 c=g.fx2 by A97,A109;
g.fx2 c=z.x2 by A105,XBOOLE_1:7;
then A111: fx1 c=z.x2 by A110;
Q[fx1,g.fx1] by A23,A97;
then g.fx1 c<fx1;
then g.fx1 c=fx1;
then A112: g.fx1\/(fx1\(g.fx1))=fx1 by XBOOLE_1:45;
z.x1 c=g.fx1\/(fx1\(g.fx1)) by A99,A100,XBOOLE_1:9;
then z.x1 c=z.x2 by A111,A112;
hence thesis by A93,A95;
end;
suppose fx2 c=fx1 & fx1<>fx2;
then
A113: fx2 c<fx1;
Q[fx1,g.fx1] by A23,A97;
then A114: fx2 c=g.fx1 by A102,A113;
g.fx1 c=z.x1 by A99,XBOOLE_1:7;
then A115: fx2 c=z.x1 by A114;
Q[fx2,g.fx2] by A23,A102;
then g.fx2 c<fx2;
then g.fx2 c=fx2;
then A116: g.fx2\/(fx2\(g.fx2))=fx2 by XBOOLE_1:45;
z.x2 c=g.fx2\/(fx2\(g.fx2)) by A105,A106,XBOOLE_1:9;
then z.x2 c=z.x1 by A115,A116;
hence thesis by A93,A95;
end;
end;
A117: rng z is with_non-empty_elements
proof
assume rng z is non with_non-empty_elements;
then {} in rng z;
then consider x being object such that
A118: x in dom z and
A119: z.x={} by FUNCT_1:def 3;
set fx=f.x;
A120: x in fx\(g.fx) by A32,A118;
P[x,fx] by A8,A118;
then fx in Y;
then R[fx,h.fx] by A31;
then consider H be Function of fx\(g.fx),bool(fx\(g.fx)) such that
A121: h.fx=H and
H is one-to-one and
A122: rng H is with_non-empty_elements c=-linear and
dom H in rng H and
for Z st Z in rng H & card Z<>1 ex x st x in Z & Z\{x} in rng H;
dom H=fx\(g.fx) by FUNCT_2:def 1;
then A123: H.x in rng H by A120,FUNCT_1:def 3;
z.x=g.fx\/H.x by A45,A118,A121;
hence contradiction by A119,A122,A123;
end;
take rng z;
for x1,x2 be object st x1 in dom z & x2 in dom z & z.x1=z.x2 holds x1=x2
proof
let x1,x2 be object;
set f1=f.x1,f2=f.x2;
assume that
A124: x1 in dom z and
A125: x2 in dom z and
A126: z.x1=z.x2;
A127: z.x1=Z(x1) & z.x2=Z(x2) by A45,A124,A125;
P[x2,f2] by A8,A125;
then
A128: f2 in Y;
then R[f2,h.f2] by A31;
then consider H2 be Function of f2\(g.f2),bool(f2\(g.f2)) such that
A129: h.f2=H2 and
A130: H2 is one-to-one and
A131: rng H2 is with_non-empty_elements c=-linear and
dom H2 in rng H2 and
for Z st Z in rng H2 & card Z<>1 ex x st x in Z & Z\{x} in rng H2;
dom H2=f2\(g.f2) by FUNCT_2:def 1;
then A132: x2 in dom H2 by A32,A125;
then A133: H2.x2 in rng H2 by FUNCT_1:def 3;
then A134: g.f2 misses H2.x2 by XBOOLE_1:63,79;
P[x1,f1] by A8,A124;
then
A135: f1 in Y;
then R[f1,h.f1] by A31;
then consider H1 be Function of f1\(g.f1),bool(f1\(g.f1)) such that
A136: h.f1=H1 and
H1 is one-to-one and
A137: rng H1 is with_non-empty_elements c=-linear and
dom H1 in rng H1 and
for Z st Z in rng H1 & card Z<>1 ex x st x in Z & Z\{x} in rng H1;
dom H1=f1\(g.f1) by FUNCT_2:def 1;
then A138: x1 in dom H1 by A32,A124;
then A139: H1.x1 in rng H1 by FUNCT_1:def 3;
then A140: g.f1 misses H1.x1 by XBOOLE_1:63,79;
A141: f1,f2 are_c=-comparable by A1,A128,A135;
per cases by A141;
suppose A142: f1=f2;
then H1.x1=H1.x2 by A126,A127,A129,A134,A136,A140,XBOOLE_1:71;
hence thesis by A129,A130,A132,A136,A138,A142,FUNCT_1:def 4;
end;
suppose A143: f1 c=f2 & f1<>f2;
Q[f1,g.f1] by A23,A135;
then g.f1 c<f1;
then g.f1 c=f1;
then g.f1\/(f1\(g.f1))=f1 by XBOOLE_1:45;
then A144: Z(x2)c=f1 by A126,A127,A136,A139,XBOOLE_1:9;
A145: f1 c<f2 by A143;
Q[f2,g.f2] by A23,A128;
then f1 c=g.f2 by A135,A145;
then Z(x2)c=g.f2 by A144;
then H2.x2 c=g.f2 by A129,XBOOLE_1:11;
hence thesis by A131,A133,XBOOLE_1:67,79;
end;
suppose A146: f2 c=f1 & f1<>f2;
Q[f2,g.f2] by A23,A128;
then g.f2 c<f2;
then g.f2 c=f2;
then g.f2\/(f2\(g.f2))=f2 by XBOOLE_1:45;
then A147: Z(x1)c=f2 by A126,A127,A129,A133,XBOOLE_1:9;
A148: f2 c<f1 by A146;
Q[f1,g.f1] by A23,A135;
then f2 c=g.f1 by A128,A148;
then Z(x1)c=g.f1 by A147;
then H1.x1 c=g.f1 by A136,XBOOLE_1:11;
hence thesis by A137,A139,XBOOLE_1:67,79;
end;
end;
then z is one-to-one by FUNCT_1:def 4;
then X,rng z are_equipotent by A46,WELLORD2:def 4;
hence thesis by A47,A61,A89,A117,CARD_1:5;
end;
begin :: Simplicial Complexes
definition
mode SimplicialComplexStr is TopStruct;
end;
reserve K for SimplicialComplexStr;
notation let K;
let A be Subset of K;
synonym A is simplex-like for A is open;
end;
notation let K;
let S be Subset-Family of K;
synonym S is simplex-like for S is open;
end;
registration
let K;
cluster empty simplex-like for Subset-Family of K;
existence
proof
take E={}bool the carrier of K;
thus thesis;
end;
end;
theorem Th14:
for S be Subset-Family of K holds
S is simplex-like iff S c= the topology of K
proof
let S be Subset-Family of K;
hereby assume A1: S is simplex-like;
thus S c=the topology of K
proof
let x be object;
assume A2: x in S;
then reconsider A=x as Subset of K;
A is simplex-like by A1,A2;
hence thesis;
end;
end;
assume A3: S c=the topology of K;
let A be Subset of K;
assume A in S;
hence thesis by A3;
end;
definition
let K;
let v be Element of K;
attr v is vertex-like means
ex S be Subset of K st S is simplex-like & v in S;
end;
definition
let K;
func Vertices K -> Subset of K means :Def4:
for v be Element of K holds v in it iff v is vertex-like;
existence
proof
set B={v where v is Element of K:v is vertex-like};
B c=[#]K
proof
let x be object;
assume x in B;
then consider v be Element of K such that
A1: x=v and
A2: v is vertex-like;
ex S be Subset of K st S is simplex-like & v in S by A2;
hence thesis by A1;
end;
then reconsider B as Subset of K;
take B;
let v be Element of K;
hereby assume v in B;
then ex w be Element of K st v=w & w is vertex-like;
hence v is vertex-like;
end;
assume v is vertex-like;
hence thesis;
end;
uniqueness
proof
let V1,V2 be Subset of K such that
A3: for v be Element of K holds v in V1 iff v is vertex-like and
A4: for v be Element of K holds v in V2 iff v is vertex-like;
thus for x being object st x in V1 holds x in V2 by A3,A4;
let x be object;
assume A5: x in V2;
then reconsider v=x as Element of K;
v is vertex-like by A4,A5;
hence thesis by A3;
end;
end;
definition
let K be SimplicialComplexStr;
mode Vertex of K is Element of Vertices K;
end;
definition
let K be SimplicialComplexStr;
attr K is finite-vertices means :Def5:
Vertices K is finite;
end;
definition
let K;
attr K is locally-finite means
for v be Vertex of K holds
{S where S is Subset of K : S is simplex-like & v in S} is finite;
end;
definition
let K;
attr K is empty-membered means :Def7:
the topology of K is empty-membered;
attr K is with_non-empty_elements means :Def8:
the topology of K is with_non-empty_elements;
end;
notation let K;
antonym K is with_non-empty_element for K is empty-membered;
antonym K is with_empty_element for K is with_non-empty_elements;
end;
definition
let X;
mode SimplicialComplexStr of X -> SimplicialComplexStr means :Def9:
[#]it c= X;
existence
proof
take the empty TopStruct;
thus thesis;
end;
end;
definition
let X;
let KX be SimplicialComplexStr of X;
attr KX is total means
[#]KX = X;
end;
Lm2: Vertices K is empty iff K is empty-membered
proof
hereby assume A1: Vertices K is empty;
assume K is with_non-empty_element;
then the topology of K is with_non-empty_element;
then consider D such that
A2: D in the topology of K;
reconsider S=D as Subset of K by A2;
the Element of D in S;
then reconsider v=the Element of D as Element of K;
S is simplex-like by A2;
then v is vertex-like;
hence contradiction by A1,Def4;
end;
assume A3: K is empty-membered;
assume Vertices K is non empty;
then consider x being object such that
A4: x in Vertices K;
reconsider x as Element of K by A4;
x is vertex-like by A4,Def4;
then consider S be Subset of K such that
A5: S is simplex-like and
A6: x in S;
S in the topology of K by A5;
then the topology of K is with_non-empty_element by A6;
hence contradiction by A3;
end;
Lm3: for S be Subset of K st S is simplex-like & x in S holds x in Vertices K
proof
let S be Subset of K such that
A1: S is simplex-like and
A2: x in S;
reconsider v=x as Element of K by A2;
v is vertex-like by A1,A2;
hence thesis by Def4;
end;
Lm4: for A be Subset of K st A is simplex-like holds A c=Vertices K
by Lm3;
Lm5: Vertices K=union the topology of K
proof
hereby let x be object such that
A1: x in Vertices(K);
reconsider v=x as Element of K by A1;
v is vertex-like by A1,Def4;
then consider S be Subset of K such that
A2: S is simplex-like and
A3: v in S;
S in the topology of K by A2;
hence x in union the topology of K by A3,TARSKI:def 4;
end;
let x be object;
assume x in union the topology of K;
then consider y such that
A4: x in y and
A5: y in the topology of K by TARSKI:def 4;
reconsider y as Subset of K by A5;
y is simplex-like by A5;
hence thesis by A4,Lm3;
end;
Lm6: K is finite-vertices implies the topology of K is finite
proof
Vertices K=union the topology of K by Lm5;
then A1: the topology of K c=bool Vertices K by ZFMISC_1:82;
assume K is finite-vertices;
then Vertices K is finite;
hence thesis by A1;
end;
registration
cluster with_empty_element -> non void for SimplicialComplexStr;
coherence
by PENCIL_1:def 4;
cluster with_non-empty_element -> non void for SimplicialComplexStr;
coherence
by PENCIL_1:def 4;
cluster non void empty-membered -> with_empty_element for
SimplicialComplexStr;
coherence;
cluster non void subset-closed -> with_empty_element for
SimplicialComplexStr;
coherence;
cluster empty-membered-> subset-closed finite-vertices for
SimplicialComplexStr;
coherence
proof
let K;
assume A1: K is empty-membered;
then A2: the topology of K is empty-membered;
thus K is subset-closed
proof
let x,y such that
A3: x in the_family_of K and
A4: y c=x;
x is empty by A2,A3;
hence thesis by A3,A4;
end;
Vertices K is empty by A1,Lm2;
hence thesis;
end;
cluster finite-vertices-> locally-finite finite-degree for
SimplicialComplexStr;
coherence
proof
let K;
assume A5: K is finite-vertices;
then reconsider V=Vertices(K) as finite Subset of K;
thus K is locally-finite
proof
let v be Vertex of K;
A6: {S where S is Subset of K:S is simplex-like & v in S}c=the topology of K
proof
let x be object;
assume x in {S where S is Subset of K:S is simplex-like & v in S};
then ex S be Subset of K st x=S & S is simplex-like & v in S;
hence thesis;
end;
the topology of K is finite by A5,Lm6;
hence thesis by A6;
end;
thus K is finite-membered
proof
let x;
assume A7: x in the_family_of K;
then reconsider X=x as Subset of K;
X is simplex-like by A7;
then X c=V by Lm4;
hence thesis;
end;
take card V;
let A be finite Subset of K;
assume A is open;
hence thesis by Lm4,NAT_1:43;
end;
cluster locally-finite subset-closed -> finite-membered for
SimplicialComplexStr;
coherence
proof
let K be SimplicialComplexStr;
assume A8: K is locally-finite subset-closed;
the_family_of K is finite-membered
proof
let x;
assume A9: x in the_family_of K;
then reconsider A=x as Subset of K;
A10: K is non void by A9,PENCIL_1:def 4;
A11: A is simplex-like by A9;
per cases;
suppose x is empty;
hence thesis;
end;
suppose x is non empty;
then consider a be object such that
A12: a in A;
reconsider a as Element of K by A12;
a is vertex-like by A11,A12;
then reconsider a as Vertex of K by Def4;
set Aa=A\{a};
set X={S where S is Subset of K:a in S & S c=A};
defpred P[set,set] means
$1\{a}=$2;
set Z={y where y is Element of bool Aa:ex w being Subset of K st P[w,y] & w
in X};
A13: bool Aa c=Z
proof
let y be object;
assume A14: y in bool Aa;
then reconsider B=y as Subset of K by XBOOLE_1:1;
not a in B by A14,ZFMISC_1:56;
then A15: (B\/{a})\{a}=B by ZFMISC_1:117;
A16: {a}c=A by A12,ZFMISC_1:31;
Aa c=A by XBOOLE_1:36;
then B c=A by A14;
then A17: B\/{a}c=A by A16,XBOOLE_1:8;
then A18: B\/{a} is Subset of K by XBOOLE_1:1;
a in {a} by TARSKI:def 1;
then a in B\/{a} by XBOOLE_0:def 3;
then B\/{a} in X by A17,A18;
hence thesis by A14,A15,A18;
end;
set Y={S where S is Subset of K:S is simplex-like & a in S};
A19: X c=Y
proof
let y be object;
assume y in X;
then consider S be Subset of K such that
A20: y=S & a in S and
A21: S c=A;
S is simplex-like by A8,A10,A11,A21,MATROID0:1;
hence thesis by A20;
end;
Y is finite by A8;
then A22: X is finite by A19;
A23: for w be Subset of K,x,y be Element of bool Aa st P[w,x] & P[w,y]
holds x=y;
Z is finite from FRAENKEL:sch 28(A22,A23);
then A24: Aa is finite by A13;
A=Aa\/{a} by A12,ZFMISC_1:116;
hence x is finite by A24;
end;
end;
hence thesis;
end;
end;
registration
let X;
cluster empty void empty-membered strict for SimplicialComplexStr of X;
existence
proof
[#]TopStruct(# {},{}bool{} #)c=X;
then reconsider T=TopStruct(# {},{}bool{} #) as SimplicialComplexStr of X by
Def9;
take T;
thus thesis;
end;
end;
registration
let D;
cluster non empty non void total empty-membered
strict for SimplicialComplexStr of D;
existence
proof
reconsider B=bool 0 as Subset-Family of D by XBOOLE_1:2,ZFMISC_1:67;
[#]TopStruct(# D,B #)c=D;
then reconsider T=TopStruct(# D,B #) as SimplicialComplexStr of D by Def9;
take T;
[#]T=D & B is empty-membered;
hence thesis by PENCIL_1:def 4;
end;
cluster non empty total with_empty_element with_non-empty_element
finite-vertices subset-closed strict for SimplicialComplexStr of D;
existence
proof
set E=the Element of D;
reconsider B=bool{E} as Subset-Family of D by ZFMISC_1:67;
[#]TopStruct(# D,B #)c=[#]D;
then reconsider T=TopStruct(# D,B #) as SimplicialComplexStr of D by Def9;
take T;
A1: Vertices(T)c={E}
proof
let x be object such that
A2: x in Vertices(T);
reconsider v=x as Element of T by A2;
v is vertex-like by A2,Def4;
then consider S be Subset of T such that
A3: S is simplex-like and
A4: v in S;
S in B by A3;
hence thesis by A4;
end;
{E} in B by ZFMISC_1:def 1;
then B is with_non-empty_element;
then A5: [#]T=D & T is with_non-empty_element;
thus thesis by A1,A5;
end;
end;
registration
cluster non empty with_empty_element with_non-empty_element finite-vertices
subset-closed strict for SimplicialComplexStr;
existence
proof
take the non empty with_empty_element with_non-empty_element
finite-vertices subset-closed strict SimplicialComplexStr of(the non empty set
);
thus thesis;
end;
end;
registration
let K be with_non-empty_element SimplicialComplexStr;
cluster Vertices K -> non empty;
coherence by Lm2;
end;
registration
let K be finite-vertices SimplicialComplexStr;
cluster simplex-like -> finite for Subset-Family of K;
coherence
proof
let S be Subset-Family of K;
assume S is simplex-like;
then A1: S c=the topology of K by Th14;
Vertices K=union the topology of K by Lm5;
then A2: the topology of K c=bool Vertices K by ZFMISC_1:82;
Vertices K is finite by Def5;
hence thesis by A1,A2;
end;
end;
registration
let K be finite-membered SimplicialComplexStr;
cluster simplex-like -> finite-membered for Subset-Family of K;
coherence
proof
let S be Subset-Family of K;
assume A1: S is simplex-like;
let x;
assume A2: x in S;
then reconsider X=x as Subset of K;
X is simplex-like by A1,A2;
then A3: X in the topology of K;
the_family_of K is finite-membered by MATROID0:def 6;
hence thesis by A3;
end;
end;
theorem
Vertices K is empty iff K is empty-membered by Lm2;
theorem
Vertices K = union the topology of K by Lm5;
theorem
for S be Subset of K st S is simplex-like holds S c= Vertices K by Lm4;
theorem
K is finite-vertices implies the topology of K is finite by Lm6;
theorem Th19:
the topology of K is finite & K is non finite-vertices implies
K is non finite-membered
proof
defpred P[object,object] means ex D2 being set st D2 = $2 & $1 in D2;
set V=Vertices K;
assume that
A1: the topology of K is finite and
A2: K is non finite-vertices;
A3: V is infinite by A2;
A4: V=union the topology of K by Lm5;
A5: for x being object st x in V
ex y being object st y in the topology of K & P[x,y]
proof
let x be object;
assume x in V;
then ex y st x in y & y in the topology of K by A4,TARSKI:def 4;
hence thesis;
end;
consider f be Function of V,the topology of K such that
A6: for x being object st x in V holds P[x,f.x] from FUNCT_2:sch 1(A5);
the topology of K is non empty by A2,A4;
then dom f=V by FUNCT_2:def 1;
then consider x being object such that
A7: x in rng f and
A8: f"{x} is infinite by A1,A3,CARD_2:101;
x in the topology of K by A7;
then reconsider x as Subset of K;
f"{x}c=x
proof
let y be object;
assume
A9: y in f"{x};
then P[y,f.y] by A6;
then f.y in {x} & y in f.y by A9,FUNCT_1:def 7;
hence thesis by TARSKI:def 1;
end;
then x is non finite by A8;
then the_family_of K is non finite-membered by A7;
hence thesis;
end;
theorem Th20:
K is subset-closed & the topology of K is finite implies K is finite-vertices
proof
assume that
A1: K is subset-closed and
A2: the topology of K is finite;
assume K is non finite-vertices;
then K is non finite-membered by A2,Th19;
then the_family_of K is non finite-membered;
then consider x such that
A3: x in the_family_of K and
A4: x is non finite;
{x}c=the_family_of K by A3,ZFMISC_1:31;
then subset-closed_closure_of{x}c=the_family_of K by A1,Th3;
then bool x c=the_family_of K by Th4;
hence contradiction by A2,A4;
end;
begin :: The Simplicial Complex Generated on the Set
definition
let X;
let Y be Subset-Family of X;
func Complex_of Y -> strict SimplicialComplexStr of X equals
TopStruct(# X,subset-closed_closure_of Y #);
coherence
proof
[#]TopStruct(# X,subset-closed_closure_of Y #)=X;
hence thesis by Def9;
end;
end;
registration
let X;
let Y be Subset-Family of X;
cluster Complex_of Y -> total subset-closed;
coherence;
end;
registration
let X;
let Y be non empty Subset-Family of X;
cluster Complex_of Y -> with_empty_element;
coherence;
end;
registration
let X;
let Y be finite-membered Subset-Family of X;
cluster Complex_of Y -> finite-membered;
coherence;
end;
registration
let X;
let Y be finite finite-membered Subset-Family of X;
cluster Complex_of Y -> finite-vertices;
coherence
proof
set C=Complex_of Y;
reconsider Y1=Y as Subset-Family of union Y by ZFMISC_1:82;
subset-closed_closure_of Y1 c=bool union Y;
then A1: union the topology of C c=union bool union Y by ZFMISC_1:77;
union bool union Y=union Y by ZFMISC_1:81;
then Vertices C c=union Y by A1,Lm5;
hence thesis;
end;
end;
theorem
K is subset-closed implies the TopStruct of K = Complex_of the topology of K
by Th7;
definition
let X;
mode SimplicialComplex of X is finite-membered subset-closed
SimplicialComplexStr of X;
end;
definition
let K be non void SimplicialComplexStr;
mode Simplex of K is simplex-like Subset of K;
end;
registration
let K be with_empty_element SimplicialComplexStr;
cluster empty -> simplex-like for Subset of K;
coherence
proof
let S be Subset of K;
assume A1: S is empty;
the topology of K is with_empty_element by Def8;
then S in the topology of K by A1;
hence thesis;
end;
cluster empty for Simplex of K;
existence
proof
{}K is simplex-like;
hence thesis;
end;
end;
registration
let K be non void finite-membered SimplicialComplexStr;
cluster finite for Simplex of K;
existence
proof
consider S be object such that
A1: S in the topology of K by XBOOLE_0:def 1;
reconsider S as Simplex of K by A1,PRE_TOPC:def 2;
S is finite;
hence thesis;
end;
end;
begin :: The Degree of Simplicial Complexes
definition
let K;
func degree K -> ExtReal means :Def12:
(for S be finite Subset of K st S is simplex-like holds card S <= it+1) &
ex S be Subset of K st S is simplex-like & card S = it+1
if K is non void finite-degree,
it = -1 if K is void
otherwise
it = +infty;
existence
proof
now defpred P[Nat] means
for S be finite Subset of K st S is simplex-like holds card S<=$1;
assume A1: K is non void finite-degree;
then A2: the_family_of K is finite-membered by MATROID0:def 6;
A3: ex n be Nat st P[n] by A1;
consider k be Nat such that
A4: P[k] and
A5: for n be Nat st P[n] holds k<=n from NAT_1:sch 5(A3);
take D=k-1;
thus for S be finite Subset of K st S is simplex-like holds card S<=D+1 by
A4;
assume A6: for S be Subset of K st S is simplex-like holds card S<>D+1;
per cases;
suppose A7: k=0;
consider S be object such that
A8: S in the topology of K by A1,XBOOLE_0:def 1;
reconsider S as finite Subset of K by A2,A8;
A9: S is simplex-like by A8;
then card S=0 by A4,A7;
hence contradiction by A6,A7,A9;
end;
suppose k>0;
then reconsider k1=k-1 as Element of NAT by NAT_1:20;
P[k1]
proof
let S be finite Subset of K;
assume A10: S is simplex-like;
then card S<=k1+1 by A4;
then card S<k1+1 by A6,A10,XXREAL_0:1;
hence thesis by NAT_1:13;
end;
then k1+1<=k1 by A5;
hence contradiction by NAT_1:13;
end;
end;
hence thesis;
end;
uniqueness
proof
let D1,D2 be ExtReal;
now assume A11: K is non void finite-degree;
assume A12: for S be finite Subset of K st S is simplex-like holds card S<=
D1+1;
given S1 be Subset of K such that
A13: S1 is simplex-like & card S1=D1+1;
assume A14: for S be finite Subset of K st S is simplex-like holds card S<=
D2+1;
given S2 be Subset of K such that
A15: S2 is simplex-like & card S2=D2+1;
A16: D2+1<=D1+1 by A11,A12,A15;
D1+1<=D2+1 by A11,A13,A14;
hence D1=D2 by A16,XXREAL_0:1,XXREAL_3:11;
end;
hence thesis;
end;
consistency;
end;
registration
let K be finite-degree SimplicialComplexStr;
cluster degree K + 1 -> natural;
coherence
proof
per cases;
suppose K is void;
then degree K+1=-1+1 by Def12
.=0;
hence thesis;
end;
suppose K is non void;
then consider S be Subset of K such that
A1: S is simplex-like and
A2: card S=degree K+1 by Def12;
the_family_of K is finite-membered & S in the topology of K by A1,
MATROID0:def 6;
then S is finite;
hence thesis by A2;
end;
end;
cluster degree K -> integer;
coherence
proof
degree K=(degree K+1)-1 by XXREAL_3:24;
hence thesis;
end;
end;
theorem Th22:
degree K = -1 iff K is empty-membered
proof
per cases;
suppose K is void;
hence thesis by Def12;
end;
suppose A1: K is non void;
hereby assume A2: degree K=-1;
then A3: K is finite-degree by A1,Def12;
assume K is with_non-empty_element;
then the topology of K is with_non-empty_element;
then consider S be non empty set such that
A4: S in the topology of K;
reconsider S as Subset of K by A4;
A5: S is simplex-like by A4;
then reconsider S as finite Subset of K by A1,A3;
card S<=-1+1 by A1,A2,A3,A5,Def12;
then card S=0;
hence contradiction;
end;
assume A6: K is empty-membered;
then consider S be Subset of K such that
A7: S is simplex-like and
A8: card S=degree K+1 by A1,Def12;
A9: S in the topology of K by A7;
assume degree K<>-1;
then card S<>-1+1 by A8,XXREAL_3:11;
then A10: S is non empty;
the topology of K is empty-membered by A6;
hence thesis by A9,A10;
end;
end;
theorem Th23:
-1 <= degree K
proof
per cases;
suppose K is void;
hence thesis by Def12;
end;
suppose A1: K is non void finite-degree;
then reconsider d=degree K as Integer;
0=-1+1 & d+1>=0 by A1;
hence thesis by XREAL_1:6;
end;
suppose K is non void non finite-degree;
hence thesis by Def12;
end;
end;
theorem Th24:
for S be finite Subset of K st S is simplex-like holds card S <= degree K+1
proof
let S be finite Subset of K such that
A1: S is simplex-like;
S in the topology of K by A1;
then A2: K is non void by PENCIL_1:def 4;
per cases;
suppose K is finite-degree;
hence thesis by A1,A2,Def12;
end;
suppose K is non finite-degree;
then degree K=+infty by A2,Def12;
then degree K+1=+infty by XXREAL_3:def 2;
hence thesis by XXREAL_0:3;
end;
end;
theorem Th25:
K is non void or i >= -1 implies (degree K <= i iff K is finite-membered &
for S be finite Subset of K st S is simplex-like holds card S <= i+1)
proof
assume A1: K is non void or i>=-1;
per cases;
suppose A2: K is void;
then
A3: for S be finite Subset of K st S is simplex-like holds
card S<=i+1 by PENCIL_1:def 4;
K is empty-membered by A2;
hence thesis by A1,A2,A3,Th22;
end;
suppose A4: K is non void;
hereby assume A5: degree K<=i;
then A6: degree K+1<=i+1 by XXREAL_3:35;
i in REAL by XREAL_0:def 1;
then A7: degree K<>+infty by A5,XXREAL_0:9;
then K is finite-degree or K is empty-membered by Def12;
hence K is finite-membered;
let S be finite Subset of K;
assume A8: S is simplex-like;
K is non void finite-degree or K is void by A7,Def12;
then card S<=degree K+1 by A4,A8,Def12;
hence card S<=i+1 by A6,XXREAL_0:2;
end;
assume that
A9: K is finite-membered and
A10: for S be finite Subset of K st S is simplex-like holds card S<=i+1;
consider S be object such that
A11: S in the topology of K by A4,XBOOLE_0:def 1;
reconsider S as Subset of K by A11;
A12: S is simplex-like by A11;
then reconsider S as finite Subset of K by A9;
card S<=i+1 by A10,A12;
then reconsider i1=i+1 as Element of NAT by INT_1:3;
for A be finite Subset of K st A is open holds card A<=i1 by A10;
then A13: K is finite-degree by A9;
then reconsider d=degree K as Integer;
ex S1 be Subset of K st S1 is simplex-like & card S1=degree K+1 by A4,A13
,Def12;
then d+1<=i+1 by A9,A10;
hence thesis by XREAL_1:6;
end;
end;
theorem
for A be finite Subset of X holds degree Complex_of {A} = card A - 1
proof
let A be finite Subset of X;
set C=Complex_of{A};
A1: the topology of C=bool A by Th4;
then for S be finite Subset of C st S is simplex-like holds
card S<=(card A-1)+1 by NAT_1:43;
then A2: degree C<=card A-1 by Th25;
A c=A;
then reconsider A1=A as finite Simplex of C by A1,PRE_TOPC:def 2;
card A=card A-1+1 & card A1<=degree C+1 by Def12;
then card A-1<=degree C by XREAL_1:8;
hence card A-1=degree C by A2,XXREAL_0:1;
end;
begin :: Subcomplexes
definition
let X;
let KX be SimplicialComplexStr of X;
mode SubSimplicialComplex of KX -> SimplicialComplex of X means :Def13:
[#]it c= [#]KX & the topology of it c= the topology of KX;
existence
proof
set T=TopStruct(# 0,{}bool 0 #);
the_family_of T is empty & [#]T c=X;
then reconsider T=TopStruct(# 0,{}bool 0 #) as SimplicialComplex of X by Def9
,MATROID0:def 3,def 6;
take T;
thus thesis;
end;
end;
reserve KX for SimplicialComplexStr of X,
SX for SubSimplicialComplex of KX;
registration
let X,KX;
cluster empty void strict for SubSimplicialComplex of KX;
existence
proof
set C=Complex_of{}bool{};
A1: [#]C c=[#]KX & the topology of C c=the topology of KX;
[#]C c=X;
then C is SimplicialComplexStr of X by Def9;
then reconsider C as SubSimplicialComplex of KX by A1,Def13;
take C;
thus thesis;
end;
end;
registration
let X;
let KX be void SimplicialComplexStr of X;
cluster -> void for SubSimplicialComplex of KX;
coherence
proof
let S be SubSimplicialComplex of KX;
the topology of S c=the topology of KX & the topology of KX is empty by Def13
,PENCIL_1:def 4;
hence thesis;
end;
end;
registration
let D;
let KD be non void subset-closed SimplicialComplexStr of D;
cluster non void for SubSimplicialComplex of KD;
existence
proof
A1: the_family_of KD is subset-closed;
consider x being object such that
A2: x in the topology of KD by XBOOLE_0:def 1;
reconsider x as set by TARSKI:1;
per cases;
suppose x is empty;
then reconsider x as empty Subset of KD by A2;
set S=Complex_of{x};
A3: [#]S=[#]KD;
[#]KD c=D by Def9;
then reconsider S as SimplicialComplex of D by A3,Def9;
take S;
{x}c=the topology of KD by A2,ZFMISC_1:31;
then subset-closed_closure_of{x}c=the topology of KD by A1,Th3;
hence thesis by A3,Def13;
end;
suppose A4: x is non empty;
set d=the Element of x;
d in x by A4;
then reconsider dd={d} as Subset of KD by A2,ZFMISC_1:31;
set S=Complex_of{dd};
A5: [#]S=[#]KD;
[#]KD c=D by Def9;
then reconsider S as SimplicialComplex of D by A5,Def9;
take S;
dd c=x by A4,ZFMISC_1:31;
then dd in the topology of KD by A1,A2;
then {dd}c=the topology of KD by ZFMISC_1:31;
then the topology of S c=the topology of KD by A1,Th3;
hence thesis by A5,Def13;
end;
end;
end;
registration
let X;
let KX be finite-vertices SimplicialComplexStr of X;
cluster -> finite-vertices for SubSimplicialComplex of KX;
coherence
proof
let SX be SubSimplicialComplex of KX;
A1: Vertices KX is finite by Def5;
the topology of SX c=the topology of KX by Def13;
then A2: union the topology of SX c=union the topology of KX by ZFMISC_1:77;
union the topology of SX=Vertices SX & union the topology of KX=Vertices KX
by Lm5;
hence thesis by A2,A1;
end;
end;
registration
let X;
let KX be finite-degree SimplicialComplexStr of X;
cluster -> finite-degree for SubSimplicialComplex of KX;
coherence
proof
let S be SubSimplicialComplex of KX;
consider n be Nat such that
A1: for A be finite Subset of KX st A is simplex-like holds card A<=n by
MATROID0:def 7;
thus S is finite-membered;
take n;
let A be finite Subset of S;
assume A is simplex-like;
then A2: A in the topology of S;
[#]S c=[#]KX by Def13;
then reconsider A1=A as finite Subset of KX by XBOOLE_1:1;
the topology of S c=the topology of KX by Def13;
then A1 is simplex-like by A2;
hence thesis by A1;
end;
end;
theorem Th27:
for S1 be SubSimplicialComplex of SX holds S1 is SubSimplicialComplex of KX
proof
let S1 be SubSimplicialComplex of SX;
[#]SX c=[#]KX & [#]S1 c=[#]SX by Def13;
then A1: [#]S1 c=[#]KX;
the topology of SX c=the topology of KX & the topology of S1 c=the topology
of SX by Def13;
then the topology of S1 c=the topology of KX;
hence thesis by A1,Def13;
end;
theorem Th28:
for A be Subset of KX for S be finite-membered Subset-Family of A st
subset-closed_closure_of S c=the topology of KX
holds Complex_of S is strict SubSimplicialComplex of KX
proof
let A be Subset of KX;
let S be finite-membered Subset-Family of A such that
A1: subset-closed_closure_of S c=the topology of KX;
set C=Complex_of S;
[#]KX c=X by Def9;
then [#]C c=X;
then [#]C c=[#]KX & C is strict SimplicialComplexStr of X by Def9;
hence thesis by A1,Def13;
end;
theorem
for KX be subset-closed SimplicialComplexStr of X
for A be Subset of KX for S be finite-membered Subset-Family of A st
S c= the topology of KX
holds Complex_of S is strict SubSimplicialComplex of KX
proof
let KX be subset-closed SimplicialComplexStr of X;
let A be Subset of KX;
let S be finite-membered Subset-Family of A;
A1: the_family_of KX is subset-closed;
assume S c=the topology of KX;
hence thesis by A1,Th3,Th28;
end;
theorem
for Y1,Y2 be Subset-Family of X st
Y1 is finite-membered & Y1 is_finer_than Y2
holds Complex_of Y1 is SubSimplicialComplex of Complex_of Y2
proof
let Y1,Y2 be Subset-Family of X such that
A1: Y1 is finite-membered and
A2: Y1 is_finer_than Y2;
set C1=Complex_of Y1,C2=Complex_of Y2;
A3: [#]C1=X & [#]C2=X;
subset-closed_closure_of Y1 c=subset-closed_closure_of Y2 by A2,Th6;
hence thesis by A1,A3,Def13;
end;
theorem
Vertices SX c= Vertices KX
proof
let x be object;
assume A1: x in Vertices SX;
then reconsider v=x as Element of SX;
v is vertex-like by A1,Def4;
then consider S be Subset of SX such that
A2: S is simplex-like and
A3: v in S;
A4: the topology of SX c=the topology of KX by Def13;
A5: S in the topology of SX by A2;
then S in the topology of KX by A4;
then reconsider S as Subset of KX;
v in S by A3;
then reconsider v as Element of KX;
S is simplex-like by A4,A5;
then v is vertex-like by A3;
hence thesis by Def4;
end;
theorem Th32:
degree SX <= degree KX
proof
per cases;
suppose A1: SX is non finite-degree;
SX is non void
proof
assume SX is void;
then SX is empty-membered;
hence contradiction by A1;
end;
then KX is non finite-degree non void & degree SX=+infty by A1,Def12;
hence thesis by Def12;
end;
suppose SX is void;
then degree SX=-1 by Def12;
hence thesis by Th23;
end;
suppose A2: SX is non void finite-degree;
then A3: KX is non void;
per cases;
suppose KX is non finite-degree;
then degree KX=+infty by A3,Def12;
hence thesis by XXREAL_0:3;
end;
suppose A4: KX is finite-degree;
A5: the topology of SX c=the topology of KX by Def13;
consider S be Subset of SX such that
A6: S is simplex-like and
A7: card S=degree SX+1 by A2,Def12;
A8: S in the topology of SX by A6;
then S in the topology of KX by A5;
then reconsider S1=S as finite Subset of KX by A4,A7;
S1 is simplex-like by A5,A8;
then degree SX+1<=degree KX+1 by A3,A4,A7,Def12;
then A9: degree SX+1-1<=degree KX+1-1 by XXREAL_3:37;
degree SX+1-1=degree SX by XXREAL_3:24;
hence thesis by A9,XXREAL_3:24;
end;
end;
end;
definition
let X,KX,SX;
attr SX is maximal means :Def14:
for A be Subset of SX st A in the topology of KX holds A is simplex-like;
end;
theorem Th33:
SX is maximal iff bool[#]SX /\ the topology of KX c= the topology of SX
proof
hereby assume A1: SX is maximal;
thus bool[#]SX/\the topology of KX c=the topology of SX
proof
let x be object;
assume A2: x in bool[#]SX/\the topology of KX;
then reconsider A=x as Subset of SX by XBOOLE_0:def 4;
A in the topology of KX by A2,XBOOLE_0:def 4;
then A is simplex-like by A1;
hence thesis;
end;
end;
assume A3: bool[#]SX/\the topology of KX c=the topology of SX;
let A be Subset of SX;
assume A in the topology of KX;
then A in bool[#]SX/\the topology of KX by XBOOLE_0:def 4;
hence thesis by A3;
end;
registration
let X,KX;
cluster maximal strict for SubSimplicialComplex of KX;
existence
proof
set B=bool{}/\the topology of KX;
reconsider B as finite-membered subset-closed Subset-Family of{}KX by
XBOOLE_1:17,ZFMISC_1:1,33;
subset-closed_closure_of B=B by Th7;
then reconsider C=Complex_of B as strict SubSimplicialComplex of KX by Th28,
XBOOLE_1:17;
take C;
C=TopStruct(# {}KX,B #) & bool[#]C=bool{} by Th7;
hence thesis by Th33;
end;
end;
theorem Th34:
for S1 be SubSimplicialComplex of SX st SX is maximal & S1 is maximal
holds S1 is maximal SubSimplicialComplex of KX
proof
let S1 be SubSimplicialComplex of SX;
reconsider s1=S1 as SubSimplicialComplex of KX by Th27;
assume that
A1: SX is maximal and
A2: S1 is maximal;
A3: [#]S1 c=[#]SX by Def13;
now let A be Subset of s1;
reconsider a=A as Subset of SX by A3,XBOOLE_1:1;
assume A in the topology of KX;
then a is simplex-like by A1;
then a in the topology of SX;
hence A is simplex-like by A2;
end;
hence S1 is maximal SubSimplicialComplex of KX by Def14;
end;
theorem
for S1 be SubSimplicialComplex of SX st
S1 is maximal SubSimplicialComplex of KX
holds S1 is maximal
proof
let S1 be SubSimplicialComplex of SX;
assume S1 is maximal SubSimplicialComplex of KX;
then reconsider s1=S1 as maximal SubSimplicialComplex of KX;
the topology of SX c=the topology of KX by Def13;
then A1: bool[#]s1/\the topology of SX c=bool[#]s1/\the topology of KX by
XBOOLE_1:26;
bool[#]s1/\the topology of KX c=the topology of s1 by Th33;
then bool[#]S1/\the topology of SX c=the topology of S1 by A1;
hence thesis by Th33;
end;
theorem Th36:
for K1,K2 be maximal SubSimplicialComplex of KX st [#]K1 = [#]K2
holds the TopStruct of K1 = the TopStruct of K2
proof
let K1,K2 be maximal SubSimplicialComplex of KX;
assume A1: [#]K1=[#]K2;
set TOP1=the topology of K1,TOP2=the topology of K2,TOP=the topology of KX;
A2: TOP/\bool[#]K2 c=TOP2 by Th33;
TOP1 c=TOP by Def13;
then A3: TOP1 c=TOP/\bool[#]K1 by XBOOLE_1:19;
TOP2 c=TOP by Def13;
then A4: TOP2 c=TOP/\bool[#]K2 by XBOOLE_1:19;
TOP/\bool[#]K1 c=TOP1 by Th33;
then TOP1=TOP/\bool[#]K1 by A3
.=TOP2 by A1,A2,A4;
hence thesis by A1;
end;
definition
let X;
let KX be subset-closed SimplicialComplexStr of X;
let A be Subset of KX such that
A1: bool A /\ the topology of KX is finite-membered;
func KX|A -> maximal strict SubSimplicialComplex of KX means :Def15:
[#]it = A;
existence
proof
the_family_of KX is subset-closed;
then reconsider BA=bool A/\the topology of KX as finite-membered
subset-closed Subset-Family of A by A1,XBOOLE_1:17;
set KA=TopStruct(# A,BA #);
A2: [#]KA c=[#]KX & the topology of KA c=the topology of KX by XBOOLE_1:17;
A3: KA is subset-closed finite-membered;
[#]KX c=X by Def9;
then [#]KA c=X;
then KA is SimplicialComplexStr of X by Def9;
then reconsider KA as maximal strict SubSimplicialComplex of KX by A2,A3
,Def13,Th33;
take KA;
thus thesis;
end;
uniqueness by Th36;
end;
reserve SC for SimplicialComplex of X;
definition
let X,SC;
let A be Subset of SC;
redefine func SC|A means :Def16: :: redefines | (SIMPLEX0, definition)
[#]it = A;
compatibility
proof
let KA be maximal strict SubSimplicialComplex of SC;
the_family_of SC is finite-membered & bool A/\the topology of SC c=the
topology of SC by MATROID0:def 6,XBOOLE_1:17;
hence thesis by Def15;
end;
end;
theorem Th37:
for A be Subset of SC holds
the topology of SC|A = bool A /\ the topology of SC
proof
let A be Subset of SC;
A1: [#](SC|A)=A by Def16;
then A2: bool A/\the topology of SC c=the topology of SC|A by Th33;
the topology of SC|A c=the topology of SC by Def13;
then the topology of SC|A c=bool A/\the topology of SC by A1,XBOOLE_1:19;
hence thesis by A2;
end;
theorem
for A,B be Subset of SC for B1 be Subset of SC|A st B1 = B
holds SC|A|B1 = SC|B
proof
let A,B be Subset of SC;
let B1 be Subset of SC|A;
reconsider SCAB=SC|A|B1 as maximal strict SubSimplicialComplex of SC by Th34;
assume A1: B1=B;
[#]SCAB=B1 by Def16;
hence thesis by A1,Def16;
end;
theorem
SC|[#]SC = the TopStruct of SC
proof
set T=the TopStruct of SC;
A1: [#]T c=[#]SC & bool[#]T/\the topology of SC=the topology of SC by
XBOOLE_1:28;
the_family_of SC=the_family_of T & the_family_of SC is finite-membered
subset-closed by MATROID0:def 6;
then A2: T is finite-membered subset-closed;
[#]SC c=X by Def9;
then [#]T c=X;
then T is SimplicialComplexStr of X by Def9;
then reconsider T as maximal SubSimplicialComplex of SC by A1,A2,Def13,Th33;
[#]T=[#]SC;
hence thesis by Def16;
end;
theorem
for A,B be Subset of SC st A c= B holds SC|A is SubSimplicialComplex of SC|B
proof
let A,B be Subset of SC;
A1: bool A/\the topology of SC=the topology of SC|A & bool B/\the topology of
SC=the topology of SC|B by Th37;
assume A2: A c=B;
then bool A c=bool B by ZFMISC_1:67;
then A3: bool A/\the topology of SC c=bool B/\the topology of SC by
XBOOLE_1:27;
[#](SC|A)=A & [#](SC|B)=B by Def16;
hence thesis by A2,A3,A1,Def13;
end;
begin :: The Skelton of a Simplicial Complex
definition
let X,KX;
let i be dim-like number;
func Skeleton_of(KX,i) -> SimplicialComplexStr of X equals
Complex_of the_subsets_with_limited_card(Segm(i+1),the topology of KX);
coherence
proof
set C=Complex_of the_subsets_with_limited_card(Segm(i+1),the topology of KX);
[#]KX c=X by Def9;
then [#]C c=X;
hence thesis by Def9;
end;
end;
definition let n be natural Number;
redefine func -n -> integer number; :: redefines - (XXREAL_3, definition)
coherence by TARSKI:1;
end;
registration
let X,KX;
cluster Skeleton_of(KX,-1) -> empty-membered;
coherence
proof
assume Skeleton_of(KX,-1) is with_non-empty_element;
then the topology of Skeleton_of(KX,-1) is with_non-empty_element;
then consider x be non empty set such that
A1: x in the topology of Skeleton_of(KX,-1);
consider b be set such that
A2: x c=b and
A3: b in the_subsets_with_limited_card(Segm(-1+1),the topology of KX)
by A1,Th2;
card b c=card Segm(-1+1) by A3,Def2;
then card b c={};
then b is empty;
hence thesis by A2;
end;
let i be dim-like number;
cluster Skeleton_of(KX,i) -> finite-degree;
coherence
proof
reconsider i1=i+1 as Nat;
set SUB=the_subsets_with_limited_card(Segm(i+1),the topology of KX);
set C=Complex_of SUB;
now let A be finite Subset of C;
assume A is open;
then A in subset-closed_closure_of SUB;
then consider B be set such that
A4: A c=B & B in SUB by Th2;
card A c=card B & card B c= i1 by A4,Def2,CARD_1:11;
then Segm card A c= Segm i1;
hence card A<= i1 by NAT_1:39;
end;
hence thesis;
end;
end;
registration
let X;
let KX be empty-membered SimplicialComplexStr of X;
let i be dim-like number;
cluster Skeleton_of(KX,i) -> empty-membered;
coherence
proof
assume Skeleton_of(KX,i) is with_non-empty_element;
then the topology of Skeleton_of(KX,i) is with_non-empty_element;
then consider x be non empty set such that
A1: x in the topology of Skeleton_of(KX,i);
A2: the topology of KX is empty-membered by Def7;
consider y such that
A3: x c=y and
A4: y in the_subsets_with_limited_card(Segm(i+1),the topology of KX)
by A1,Th2;
y in the topology of KX by A4,Def2;
then y is empty by A2;
hence thesis by A3;
end;
end;
registration
let D;
let KD be non void subset-closed SimplicialComplexStr of D;
let i be dim-like number;
cluster Skeleton_of(KD,i) -> non void;
coherence
proof
reconsider E={} as Subset of KD by XBOOLE_1:2;
E in the topology of KD & card E c=card Segm(i+1) by PRE_TOPC:def 2;
then E in the_subsets_with_limited_card(Segm(i+1),the topology of KD)
by Def2;
hence thesis;
end;
end;
theorem
for i1,i2 being dim-like number st -1 <= i1 & i1 <= i2
holds Skeleton_of(KX,i1) is SubSimplicialComplex of Skeleton_of(KX,i2)
proof let i1,i2 be dim-like number;
assume that
-1<=i1 and
A1: i1<=i2;
reconsider I1=i1+1,I2=i2+1 as Element of NAT by INT_1:3;
the_subsets_with_limited_card(Segm(i1+1),the topology of KX)c=
the_subsets_with_limited_card(Segm(i2+1),the topology of KX)
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
I1<=I2 by A1,XREAL_1:6;
then A2: card Segm I1 c=card Segm I2 by NAT_1:40;
assume
A3: x in the_subsets_with_limited_card(Segm(i1+1),the topology of KX);
then card xx c=card I1 by Def2;
then A4: card xx c=card I2 by A2;
x in the topology of KX by A3,Def2;
hence thesis by A4,Def2;
end;
then the_subsets_with_limited_card(Segm(i1+1),the topology of KX)
is_finer_than
the_subsets_with_limited_card(Segm(i2+1),the topology of KX);
then A5: the topology of Skeleton_of(KX,i1)c=the topology of Skeleton_of(KX,
i2) by Th6;
[#]Skeleton_of(KX,i1)=[#]Skeleton_of(KX,i2);
hence thesis by A5,Def13;
end;
definition
let X;
let KX be subset-closed SimplicialComplexStr of X;
let i be dim-like number;
redefine func Skeleton_of(KX,i) -> SubSimplicialComplex of KX; :: redefines Skeleton_of (SIMPLEX0, definition)
coherence
proof
A1: the_subsets_with_limited_card(Segm(i+1),the topology of KX)c=
the topology of KX by Def2;
the_family_of KX is subset-closed;
then [#]Skeleton_of(KX,i)=[#]KX & subset-closed_closure_of
the_subsets_with_limited_card(Segm(i+1),the topology of KX)c=the topology of KX
by A1,Th3;
hence thesis by Def13;
end;
end;
theorem
for i being dim-like number
st KX is subset-closed & Skeleton_of(KX,i) is empty-membered
holds KX is empty-membered or i = -1
proof let i be dim-like number;
assume KX is subset-closed;
then A1: the_family_of KX is subset-closed;
assume A2: Skeleton_of(KX,i) is empty-membered;
assume KX is with_non-empty_element;
then the topology of KX is with_non-empty_element;
then consider x be non empty set such that
A3: x in the topology of KX;
consider y being object such that
A4: y in x by XBOOLE_0:def 1;
assume i<>-1;
then {}c=card Segm(i+1) & Segm(i+1) is non empty;
then {} in card Segm(i+1) by CARD_1:3;
then 1 c=card Segm (i+1) by CARD_2:68;
then A5: card{y}c=card Segm(i+1) by CARD_1:30;
{y}c=x by A4,ZFMISC_1:31;
then {y} in the topology of KX by A1,A3;
then {y} in the_subsets_with_limited_card(Segm(i+1),the topology of KX)
by A5,Def2;
then A6: {y} in the topology of Skeleton_of(KX,i) by Th2;
the topology of Skeleton_of(KX,i) is empty-membered by A2;
hence thesis by A6;
end;
theorem
for i being dim-like number
holds degree Skeleton_of(KX,i) <= degree KX
proof let i be dim-like number;
set S=Skeleton_of(KX,i);
per cases;
suppose KX is void or S is void;
then KX is empty-membered or S is empty-membered;
then degree Skeleton_of(KX,i)=-1 by Th22;
hence thesis by Th23;
end;
suppose A1: KX is non void finite-degree & S is non void;
then reconsider d=degree KX as Integer;
now let s be finite Subset of S;
assume s is simplex-like;
then s in subset-closed_closure_of the_subsets_with_limited_card
(Segm(i+1),the topology of KX);
then consider a be set such that
A2: s c=a and
A3: a in the_subsets_with_limited_card(Segm(i+1),the topology of KX)
by Th2;
A4: a in the topology of KX by A3,Def2;
reconsider a as finite Subset of KX by A3;
Segm card s c= Segm card a by A2,CARD_1:11;
then A5: card s<=card a by NAT_1:39;
a is simplex-like & KX is non void by A4,PENCIL_1:def 4;
then card a<=d+1 by Th25;
hence card s<=d+1 by A5,XXREAL_0:2;
end;
hence thesis by A1,Th25;
end;
suppose A6: KX is non finite-degree;
KX is non void
proof
assume KX is void;
then KX is empty-membered;
hence thesis by A6;
end;
then degree KX=+infty by A6,Def12;
hence thesis by XXREAL_0:3;
end;
end;
theorem
for i being dim-like number st -1 <= i
holds degree Skeleton_of(KX,i) <= i
proof let i be dim-like number;
set swlc=the_subsets_with_limited_card(Segm(i+1),the topology of KX);
set S=Skeleton_of(KX,i);
assume A1: -1<=i;
reconsider i1=i+1 as Element of NAT by INT_1:3;
now let A be finite Subset of S;
assume A is simplex-like;
then A in the topology of S;
then consider x such that
A2: A c=x & x in swlc by Th2;
card x c=card Segm (i+1) & card A c=card x by A2,Def2,CARD_1:11;
then A3: card A c=card Segm i1;
card Segm card A=card A;
hence card A<=i+1 by A3,NAT_1:40;
end;
hence thesis by A1,Th25;
end;
theorem
for i being dim-like number
st -1 <= i & Skeleton_of(KX,i) = the TopStruct of KX
holds degree KX <= i
proof let i be dim-like number;
assume A1: -1<=i;
per cases;
suppose KX is empty-membered;
hence thesis by A1,Th22;
end;
suppose A2: KX is with_non-empty_element;
reconsider i1=i+1 as Element of NAT by INT_1:3;
assume A3: Skeleton_of(KX,i)=the TopStruct of KX;
A4: now let S be finite Subset of KX;
assume S is simplex-like;
then S in subset-closed_closure_of the_subsets_with_limited_card(i1,the
topology of KX) by A3;
then consider y such that
A5: S c=y & y in the_subsets_with_limited_card(i1,the topology of KX)
by Th2;
card S c=card y & card y c=card i1 by A5,Def2,CARD_1:11;
then A6: card S c=card Segm i1;
card S=card Segm card S;
hence card S<=i1 by A6,NAT_1:40;
end;
for x st x in the topology of KX holds x is finite by A3;
then the_family_of KX is finite-membered;
then KX is finite-membered;
hence thesis by A2,A4,Th25;
end;
end;
theorem
for i being dim-like number
st KX is subset-closed & degree KX <= i
holds Skeleton_of(KX,i) = the TopStruct of KX
proof let i be dim-like number;
assume that
A1: KX is subset-closed and
A2: degree KX<=i;
set S=Skeleton_of(KX,i);
i in REAL by XREAL_0:def 1;
then degree KX<+infty by A2,XXREAL_0:2,9;
then A3: KX is finite-degree or KX is empty-membered by Def12;
then A4: the_family_of KX is finite-membered by MATROID0:def 6;
A5: the topology of KX c=the topology of S
proof
let x be object;
A6: degree KX+1<=i+1 by A2,XXREAL_3:36;
assume A7: x in the topology of KX;
then reconsider A=x as finite Subset of KX by A4;
A is simplex-like & KX is non void by A7,PENCIL_1:def 4;
then card A<=degree KX+1 by A3,Def12;
then card A<=i+1 & i+1 in NAT by A6,INT_1:3,XXREAL_0:2;
then card Segm card A c=card Segm(i+1) by NAT_1:40;
then A in the_subsets_with_limited_card(Segm(i+1),the topology of KX)
by A7,Def2;
hence thesis by Th2;
end;
A8: the_subsets_with_limited_card(Segm(i+1),the topology of KX)c=
the topology of KX by Def2;
the_family_of KX is subset-closed by A1;
then the topology of S c=the topology of KX by A8,Th3;
hence thesis by A5,XBOOLE_0:def 10;
end;
reserve K for non void subset-closed SimplicialComplexStr;
Lm7: -1<=i & i<=degree K implies ex S be Simplex of K st card S=i+1
proof
assume that
A1: -1<=i and
A2: i<=degree K;
-1+1<=i+1 by A1,XREAL_1:6;
then reconsider i1=i+1 as Element of NAT by INT_1:3;
per cases;
suppose A3: not K is finite-degree;
per cases by A3;
suppose not K is finite-membered;
then not the_family_of K is finite-membered;
then consider A be set such that
A4: A in the_family_of K and
A5: A is infinite;
card i1 c=card A by A5;
then consider f be Function such that
A6: f is one-to-one & dom f=i1 and
A7: rng f c=A by CARD_1:10;
rng f in the_family_of K by A4,A7,CLASSES1:def 1;
then reconsider R=rng f as Simplex of K by PRE_TOPC:def 2;
take R;
R,i1 are_equipotent by A6,WELLORD2:def 4;
hence thesis by CARD_1:def 2;
end;
suppose for n be Nat ex A be finite Subset of K st A is open & card A>n;
then consider A be finite Subset of K such that
A8: A is simplex-like and
A9: card A>i1;
card Segm i1 in card Segm card A by A9,NAT_1:41;
then card i1 c=card A by CARD_1:3;
then consider f be Function such that
A10: f is one-to-one & dom f=i1 and
A11: rng f c=A by CARD_1:10;
A in the_family_of K by A8;
then rng f in the_family_of K by A11,CLASSES1:def 1;
then reconsider R=rng f as Simplex of K by PRE_TOPC:def 2;
take R;
R,i1 are_equipotent by A10,WELLORD2:def 4;
hence thesis by CARD_1:def 2;
end;
end;
suppose A12: K is finite-degree;
then reconsider d=degree K as Integer;
consider S be Subset of K such that
A13: S is simplex-like and
A14: card S=degree K+1 by A12,Def12;
reconsider s=S as finite Subset of K by A12,A13;
i+1<=d+1 by A2,XREAL_1:6;
then Segm i1 c= Segm card s by A14,NAT_1:39;
then card i1 c=card card s;
then consider f be Function such that
A15: f is one-to-one & dom f=i1 and
A16: rng f c=S by CARD_1:10;
S in the_family_of K by A13;
then rng f in the_family_of K by A16,CLASSES1:def 1;
then reconsider R=rng f as Simplex of K by PRE_TOPC:def 2;
take R;
R,i1 are_equipotent by A15,WELLORD2:def 4;
hence thesis by CARD_1:def 2;
end;
end;
definition
let K;
let i be Real such that
A1: i is integer;
mode Simplex of i,K -> finite Simplex of K means :Def18:
card it = i+1 if -1 <= i & i <= degree K otherwise it is empty;
existence
proof
A2: now reconsider S={}K as Simplex of K;
assume A3: -1>i or i>degree K;
take S;
S is empty;
hence thesis by A3;
end;
now assume A4: -1<=i & i<=degree K;
then consider S be Simplex of K such that
A5: card S=i+1 by A1,Lm7;
take S;
reconsider i as Integer by A1;
-1 + 1 <= i+1 by A4,XXREAL_3:35;
then 0 <= i+1;
then i+1 in NAT by INT_1:3;
then S is finite by A5;
hence thesis by A4,A5;
end;
hence thesis by A2;
end;
correctness;
end;
registration
let K;
cluster -> empty for Simplex of-1,K;
coherence
proof
let S be Simplex of-1,K;
-1<=degree K by Th23;
then card S=-1+1 by Def18
.=0;
hence thesis;
end;
end;
theorem
for S be Simplex of i,K st S is non empty holds i is natural
proof
let S be Simplex of i,K;
assume S is non empty;
then -1<=i & i<>-1 by Def18;
then -1<i by XXREAL_0:1;
then i>=0 by INT_1:8;
then i in NAT by INT_1:3;
hence thesis;
end;
theorem
for S be finite Simplex of K holds S is Simplex of card S - 1,K
proof
let S be finite Simplex of K;
card S<=degree K+1 by Th24;
then card S-1<=degree K+1-1 by XXREAL_3:37;
then A1: card S-1<=degree K by XXREAL_3:24;
card S-1>=0-1 & card S=card S-1+1 by XREAL_1:6;
hence thesis by A1,Def18;
end;
theorem
for K be non void subset-closed SimplicialComplexStr of D
for S be non void SubSimplicialComplex of K
for i be Integer,A be Simplex of i,S st
A is non empty or i <= degree S or degree S = degree K
holds A is Simplex of i,K
proof
let K be non void subset-closed SimplicialComplexStr of D;
let S be non void SubSimplicialComplex of K;
let i be Integer,A be Simplex of i,S such that
A1: A is non empty or i<=degree S or degree S=degree K;
A in the topology of S & the topology of S c=the topology of K by Def13,
PRE_TOPC:def 2;
then A in the topology of K;
then reconsider B=A as Simplex of K by PRE_TOPC:def 2;
A2: degree S<=degree K by Th32;
per cases by A1;
suppose A3: A is non empty;
then A4: -1<=i by Def18;
A5: i<=degree S by A3,Def18;
-1<=i by A3,Def18;
then A6: card B=i+1 by A5,Def18;
i<=degree K by A2,A5,XXREAL_0:2;
hence thesis by A6,A4,Def18;
end;
suppose A7: i<=degree S;
then A8: i<=degree K by A2,XXREAL_0:2;
per cases;
suppose A9: -1<=i;
then card B=i+1 by A7,Def18;
hence thesis by A8,A9,Def18;
end;
suppose A10: -1>i;
then B is empty by Def18;
hence thesis by A10,Def18;
end;
end;
suppose A11: degree S=degree K;
per cases;
suppose A12: -1<=i & i<=degree S;
then card B=i+1 by Def18;
hence thesis by A11,A12,Def18;
end;
suppose A13: -1>i or i>degree S;
then B is empty by Def18;
hence thesis by A11,A13,Def18;
end;
end;
end;
definition
let K;
let i be Real such that
A1: i is integer and
A2: i <= degree K;
let S be Simplex of i,K;
mode Face of S -> Simplex of max(i-1,-1),K means :Def19:
it c= S;
existence
proof
per cases;
suppose i<0;
then i-1<0-1 by XREAL_1:8;
then reconsider F=the Simplex of-1,K as Simplex of max(i-1,-1),K
by XXREAL_0:def 10;
take F;
thus thesis;
end;
suppose A3: i>=0;
then A4: card S=i+1 by A1,A2,Def18;
then S is non empty by A3;
then consider x be object such that
A5: x in S;
reconsider I=i as Element of NAT by A1,A3,INT_1:3;
i-1<=degree K-0 by A2,XXREAL_3:37;
then A6: i-1<=degree K by XXREAL_3:4;
reconsider Sx=S\{x} as Simplex of K;
A7: card Sx=I-1+1 by A4,A5,STIRL2_1:55;
A8: i-1>=0-1 by A3,XREAL_1:6;
then max(i-1,-1)=i-1 by XXREAL_0:def 10;
then reconsider Sx as Simplex of max(i-1,-1),K by A6,A7,A8,Def18;
take Sx;
thus thesis by XBOOLE_1:36;
end;
end;
end;
theorem
for S be Simplex of n,K st n<=degree K holds
X is Face of S iff ex x st x in S & S\{x} = X
proof
let S be Simplex of n,K such that
A1: n<=degree K;
n-1<=n-0 by XREAL_1:6;
then A2: n-1<=degree K by A1,XXREAL_0:2;
reconsider N=n as Integer;
A3: n-1>=0-1 by XREAL_1:6;
then A4: max(n-1,-1)=n-1 by XXREAL_0:def 10;
A5: card S=N+1 by A1,Def18;
hereby assume X is Face of S;
then reconsider f=X as Face of S;
A6: f c=S by A1,Def19;
card f=n-1+1 by A2,A3,A4,Def18;
then card(S\f)=n+1-n by A5,A6,CARD_2:44
.=1;
then consider x being object such that
A7: S\f={x} by CARD_2:42;
reconsider x as set by TARSKI:1;
take x;
x in {x} by TARSKI:def 1;
hence x in S by A7,XBOOLE_0:def 5;
thus S\{x}=f/\S by A7,XBOOLE_1:48
.=X by A6,XBOOLE_1:28;
end;
given x such that
A8: x in S and
A9: S\{x}=X;
reconsider f=X as finite Simplex of K by A9;
card f=n-1+1 by A5,A8,A9,STIRL2_1:55;
then A10: f is Simplex of n-1,K by A2,A3,Def18;
X c=S by A9,XBOOLE_1:36;
hence thesis by A1,A4,A10,Def19;
end;
begin :: The Subdivision of a Simplicial Complex
reserve P for Function;
definition
let X,KX,P;
func subdivision(P,KX) -> strict SimplicialComplexStr of X means :Def20:
[#]it = [#]KX & for A be Subset of it holds A is simplex-like iff
ex S be c=-linear finite simplex-like Subset-Family of KX st A = P.:S;
existence
proof
defpred P[set] means
ex S be c=-linear finite simplex-like Subset-Family of KX st$1=P.:S;
set SS={A where A is Subset of KX:P[A]};
SS c=bool the carrier of KX
proof
let x be object;
assume x in SS;
then ex A be Subset of KX st x=A & P[A];
hence thesis;
end;
then reconsider SS as Subset-Family of KX;
set PP=TopStruct(# the carrier of KX,SS #);
[#]PP=[#]KX & [#]KX c=X by Def9;
then reconsider PP as strict SimplicialComplexStr of X by Def9;
take PP;
thus[#]PP=[#]KX;
let A be Subset of PP;
hereby assume A is simplex-like;
then A in SS;
then ex B be Subset of KX st B=A & P[B];
hence P[A];
end;
assume P[A];
then A in SS;
hence thesis;
end;
uniqueness
proof
let P1,P2 be strict SimplicialComplexStr of X such that
A1: [#]P1=[#]KX and
A2: for A be Subset of P1 holds A is simplex-like iff ex S be c=-linear
finite simplex-like Subset-Family of KX st A=P.:S and
A3: [#]P2=[#]KX and
A4: for A be Subset of P2 holds A is simplex-like iff ex S be c=-linear
finite simplex-like Subset-Family of KX st A=P.:S;
now let x be object;
hereby assume A5: x in the topology of P1;
then reconsider A=x as Subset of P1;
reconsider B=A as Subset of P2 by A1,A3;
A is simplex-like by A5;
then ex S be c=-linear finite simplex-like Subset-Family of KX st A=P.:S
by A2;
then B is simplex-like by A4;
hence x in the topology of P2;
end;
assume A6: x in the topology of P2;
then reconsider A=x as Subset of P2;
reconsider B=A as Subset of P1 by A1,A3;
A is simplex-like by A6;
then ex S be c=-linear finite simplex-like Subset-Family of KX st A=P.:S by
A4;
then B is simplex-like by A2;
hence x in the topology of P1;
end;
hence thesis by A1,A3,TARSKI:2;
end;
end;
registration
let X,KX,P;
cluster subdivision(P,KX)
-> with_empty_element subset-closed finite-membered;
coherence
proof
set PP=subdivision(P,KX);
set S=the empty c=-linear simplex-like Subset-Family of KX;
P.:S={}KX;
then {}PP is simplex-like by Def20;
then {} in the topology of PP;
then the topology of PP is with_empty_element;
hence PP is with_empty_element;
thus PP is subset-closed
proof
let x,y;
assume that
A1: x in the_family_of PP and
A2: y c=x;
reconsider X=x,Y=y as Subset of PP by A1,A2,XBOOLE_1:1;
X is simplex-like by A1;
then consider S be c=-linear finite simplex-like Subset-Family of KX such
that
A3: X=P.:S by Def20;
set S1={A where A is Subset of KX:A in S & P.A in Y};
S1 c=S
proof
let x be object;
assume x in S1;
then ex A be Subset of KX st A=x & A in S & P.A in Y;
hence thesis;
end;
then reconsider S1 as c=-linear finite simplex-like Subset-Family of KX
by TOPS_2:11,XBOOLE_1:1;
A4: P.:S1 c=Y
proof
let x be object;
assume x in P.:S1;
then consider y being object such that
y in dom P and
A5: y in S1 and
A6: P.y=x by FUNCT_1:def 6;
ex B be Subset of KX st y=B & B in S & P.B in Y by A5;
hence thesis by A6;
end;
Y c=P.:S1
proof
let x be object;
assume A7: x in Y;
then consider y being object such that
A8: y in dom P and
A9: y in S and
A10: P.y=x by A2,A3,FUNCT_1:def 6;
y in S1 by A7,A9,A10;
hence thesis by A8,A10,FUNCT_1:def 6;
end;
then P.:S1=Y by A4;
then Y is simplex-like by Def20;
hence thesis;
end;
let x;
assume A11: x in the_family_of PP;
then reconsider A=x as Subset of PP;
A is simplex-like by A11;
then ex S be c=-linear finite simplex-like Subset-Family of KX st A=P.:S by
Def20;
hence thesis;
end;
end;
registration
let X;
let KX be void SimplicialComplexStr of X;
let P;
cluster subdivision(P,KX) -> empty-membered;
coherence
proof
set PP=subdivision(P,KX);
assume PP is with_non-empty_element;
then the topology of PP is with_non-empty_element;
then consider x be non empty set such that
A1: x in the topology of PP;
reconsider A=x as Simplex of PP by A1,PRE_TOPC:def 2;
consider S be c=-linear finite simplex-like Subset-Family of KX such that
A2: A=P.:S by Def20;
A=P.:(S/\dom P) by A2,RELAT_1:112;
then S/\dom P is non empty;
then consider y being object such that
A3: y in S/\dom P;
A4: y in S by A3,XBOOLE_0:def 4;
reconsider y as Subset of KX by A3;
y is simplex-like by A4,TOPS_2:def 1;
then y in the topology of KX;
hence thesis by PENCIL_1:def 4;
end;
end;
theorem Th51:
degree subdivision(P,KX) <= degree KX + 1
proof
set PP=subdivision(P,KX);
per cases;
suppose KX is void;
then KX is empty-membered & degree PP=-1 by Th22;
hence thesis;
end;
suppose A1: KX is non void non finite-degree;
A2: degree PP<=+infty & degree KX+0<=degree KX+1 by XXREAL_0:3,XXREAL_3:36;
degree KX+0=degree KX & degree KX=+infty by A1,Def12,XXREAL_3:4;
hence thesis by A2,XXREAL_0:2;
end;
suppose A3: KX is non void finite-degree;
then reconsider d=degree KX as Integer;
reconsider d1=d+1 as Nat by A3;
for A be finite Subset of PP st A is simplex-like holds card A<=(d+1)+1
proof
let A be finite Subset of PP;
assume A is simplex-like;
then consider S be c=-linear finite simplex-like Subset-Family of KX such
that
A4: A=P.:S by Def20;
set Sd=S/\dom P;
A=P.:(S/\dom P) by A4,RELAT_1:112;
then Segm card A c= Segm card Sd by CARD_1:67;
then A5: card A<=card Sd by NAT_1:39;
Sd\{{}}c=S by XBOOLE_1:18,36;
then reconsider SP=Sd\{{}} as c=-linear finite simplex-like Subset-Family
of KX by TOPS_2:11;
SP\/{{}}=Sd\/{{}} by XBOOLE_1:39;
then A6: card{{}}=1 & card Sd<=card(SP\/{{}}) by CARD_1:30,NAT_1:43
,XBOOLE_1:7;
card(SP\/{{}})<=card SP+card{{}} by CARD_2:43;
then A7: card Sd<=card SP+1 by A6,XXREAL_0:2;
per cases;
suppose A8: SP is empty;
0+1<=d1+1 by XREAL_1:6;
then card Sd<=d1+1 by A6,A8,XXREAL_0:2;
hence thesis by A5,XXREAL_0:2;
end;
suppose A9: SP is non empty;
reconsider uSP=union SP as Subset of KX;
union SP in SP by A9,Th9;
then A10: uSP is simplex-like by TOPS_2:def 1;
not{} in SP by ZFMISC_1:56;
then SP is with_non-empty_elements;
then A11: card SP c=card union SP by Th10;
reconsider uSP as finite Subset of KX by A3;
card uSP<=d1 by A3,A10,Th25;
then Segm card uSP c= Segm d1 by NAT_1:39;
then Segm card SP c= Segm d1 by A11;
then card SP<=d1 by NAT_1:39;
then card SP+1<=d1+1 by XREAL_1:6;
then card Sd<=d1+1 by A7,XXREAL_0:2;
hence thesis by A5,XXREAL_0:2;
end;
end;
hence thesis by Th25;
end;
end;
theorem Th52:
dom P is with_non-empty_elements implies
degree subdivision(P,KX) <= degree KX
proof
assume A1: dom P is with_non-empty_elements;
set PP=subdivision(P,KX);
per cases;
suppose A2: KX is non finite-degree;
KX is non void
proof
assume KX is void;
then KX is empty-membered;
hence thesis by A2;
end;
then degree KX=+infty by A2,Def12;
hence thesis by XXREAL_0:3;
end;
suppose A3: KX is finite-degree;
then reconsider d=degree KX as Integer;
reconsider d1=d+1 as Nat by A3;
for A be finite Subset of PP st A is simplex-like holds card A<=d+1
proof
let A be finite Subset of PP;
assume A is simplex-like;
then consider S be c=-linear finite simplex-like Subset-Family of KX such
that
A4: A=P.:S by Def20;
A5: A=P.:(S/\dom P) by A4,RELAT_1:112;
per cases;
suppose S/\dom P is empty;
then 0<=d1 & A={} by A5;
hence thesis;
end;
suppose A6: S/\dom P is non empty;
reconsider uSP=union(S/\dom P) as Subset of KX;
A7: S/\dom P c=S by XBOOLE_1:17;
then union(S/\dom P) in S/\dom P by A6,Th9;
then union(S/\dom P) in S by XBOOLE_0:def 4;
then A8: uSP is simplex-like by TOPS_2:def 1;
then A9: uSP in the topology of KX;
the_family_of KX is finite-membered by A3,MATROID0:def 6;
then reconsider uSP as finite Subset of KX by A9;
KX is non void by A9,PENCIL_1:def 4;
then card uSP<=d+1 by A8,Th25;
then A10: Segm card uSP c= Segm d1 by NAT_1:39;
card(S/\dom P)c=card union(S/\dom P) by A1,A7,Th10;
then A11: card(S/\dom P)c=d1 by A10;
card A c=card(S/\dom P) by A5,CARD_1:67;
then Segm card A c= Segm d1 by A11;
hence thesis by NAT_1:39;
end;
end;
hence thesis by Th25;
end;
end;
registration
let X;
let KX be finite-degree SimplicialComplexStr of X;
let P;
cluster subdivision(P,KX) -> finite-degree;
coherence
proof
assume subdivision(P,KX) is non finite-degree;
then degree KX+1 in REAL & degree subdivision(P,KX)=+infty
by Def12,XREAL_0:def 1;
hence thesis by Th51,XXREAL_0:9;
end;
end;
registration
let X;
let KX be finite-vertices SimplicialComplexStr of X;
let P;
cluster subdivision(P,KX) -> finite-vertices;
coherence
proof
reconsider V=Vertices KX as finite Subset of KX by Def5;
set PP=subdivision(P,KX);
set TOP=the topology of PP;
defpred F[object,object] means
ex D2 being set st D2 = $2 & P.:D2=$1;
bool V=bool union the topology of KX by Lm5;
then A1: the topology of KX c=bool V by ZFMISC_1:82;
A2: for x being object st x in TOP
ex y being object st y in bool bool V & F[x,y]
proof
let x being object such that
A3: x in TOP;
reconsider X=x as Subset of PP by A3;
X is simplex-like by A3;
then consider S be c=-linear finite simplex-like Subset-Family of KX such
that
A4: X=P.:S by Def20;
take S;
S c=the topology of KX
proof
let y be object such that
A5: y in S;
reconsider Y=y as Subset of KX by A5;
Y is simplex-like by A5,TOPS_2:def 1;
hence thesis;
end;
then S c=bool V by A1;
hence thesis by A4;
end;
consider f be Function of TOP,bool bool V such that
A6: for x being object st x in TOP holds F[x,f.x] from FUNCT_2:sch 1(A2);
now let x1,x2 be object such that
A7: x1 in dom f and
A8: x2 in dom f & f.x1=f.x2;
A9: F[x2,f.x2] by A6,A8;
F[x1,f.x1] by A6,A7;
hence x1=P.:(f.x1)
.=x2 by A8,A9;
end;
then A10: f is one-to-one by FUNCT_1:def 4;
dom f=TOP & rng f c=bool bool V by FUNCT_2:def 1;
then card TOP c=card bool bool V by A10,CARD_1:10;
then TOP is finite;
hence thesis by Th20;
end;
end;
theorem
for KX be subset-closed SimplicialComplexStr of X
for P st dom P is with_non-empty_elements &
for n st n <= degree KX ex S be Subset of KX st
S is simplex-like & card S = n+1 & BOOL S c=dom P &
P.:BOOL S is Subset of KX & P|BOOL S is one-to-one
holds degree subdivision(P,KX) = degree KX
proof
let K be subset-closed SimplicialComplexStr of X;
let P be Function such that
A1: dom P is with_non-empty_elements and
A2: for n st n<=degree K ex S be Subset of K st S is simplex-like & card S=n
+1 & BOOL S c=dom P & P.:BOOL S is Subset of K & P|BOOL S is one-to-one;
set PP=subdivision(P,K);
A3: degree PP<=degree K by A1,Th52;
A4: for n st n<=degree K ex S be Simplex of PP st card S=n+1
proof
let n;
A5: [#]K=[#]PP by Def20;
assume n<=degree K;
then consider A be Subset of K such that
A6: A is simplex-like and
A7: card A=n+1 and
A8: BOOL A c=dom P and
A9: P.:BOOL A is Subset of K and
A10: P|BOOL A is one-to-one by A2;
A11: dom(P|BOOL A)=BOOL A by A8,RELAT_1:62;
A is non empty by A7;
then consider S be Subset-Family of A such that
A12: S is with_non-empty_elements c=-linear and
A in S and
A13: card A=card S and
for Z st Z in S & card Z<>1 ex x st x in Z & Z\{x} in S by Th12;
bool A c=bool the carrier of K by ZFMISC_1:67;
then reconsider SS=S as Subset-Family of K by XBOOLE_1:1;
A14: S c=BOOL A
proof
let x be object;
assume x in S;
then x in bool A\{{}} by A12,ZFMISC_1:56;
hence thesis by ORDERS_1:def 3;
end;
then P.:S c=P.:BOOL A by RELAT_1:123;
then reconsider PS=P.:SS as Subset of PP by A5,A9,XBOOLE_1:1;
A15: A in the_family_of K by A6;
SS is simplex-like
proof
let B be Subset of K;
assume B in SS;
then B in the_family_of K by A15,CLASSES1:def 1;
hence thesis;
end;
then SS is c=-linear finite simplex-like Subset-Family of K by A7,A12,A13;
then reconsider PS as Simplex of PP by Def20;
P.:S=(P|BOOL A).:S by A14,RELAT_1:129;
then card PS=n+1 by A7,A10,A11,A13,A14,COMBGRAS:4;
hence thesis;
end;
per cases;
suppose A16: K is empty-membered;
A17: degree PP>=-1 by Th23;
degree K=-1 by A16,Th22;
hence thesis by A3,A17,XXREAL_0:1;
end;
suppose A18: K is with_non-empty_element finite-degree;
then reconsider d=degree K,dPP=degree PP as Integer;
A19: -1<=d by Th23;
d<>-1 by A18,Th22;
then -1<d by A19,XXREAL_0:1;
then 0<=d by INT_1:8;
then reconsider d as Element of NAT by INT_1:3;
ex S be Simplex of PP st card S=d+1 by A4;
then dPP+1>=d+1 by A18,Def12;
then dPP>=d by XREAL_1:6;
hence thesis by A3,XXREAL_0:1;
end;
suppose K is non void non finite-degree;
then A20: degree K=+infty by Def12;
PP is non finite-degree
proof
assume A21: PP is finite-degree;
then reconsider d=degree PP+1 as Nat by TARSKI:1;
consider S be Subset of PP such that
A22: S is simplex-like and
A23: card S=d by A21,Def12;
reconsider S as finite Subset of PP by A22;
ex S1 be Simplex of PP st card S1=card S+1 by A4,A20,XXREAL_0:3;
then d+1<=d by A21,A23,Def12;
hence contradiction by NAT_1:13;
end;
hence thesis by A20,Def12;
end;
end;
theorem Th54:
Y c=Z implies
subdivision(P|Y,KX) is SubSimplicialComplex of subdivision(P|Z,KX)
proof
set PY=subdivision(P|Y,KX);
set PZ=subdivision(P|Z,KX);
A1: dom(P|Z)=Z/\dom P by RELAT_1:61;
assume A2: Y c=Z;
then Y/\Z=Y by XBOOLE_1:28;
then A3: dom(P|Y)=(Z/\Y)/\dom P by RELAT_1:61
.=Y/\dom(P|Z) by A1,XBOOLE_1:16;
A4: [#]PY=[#]KX by Def20;
hence [#]PY c=[#]PZ by Def20;
let x be object;
assume x in the topology of PY;
then reconsider A=x as Simplex of PY by PRE_TOPC:def 2;
[#]PZ=[#]KX by Def20;
then reconsider B=A as Subset of PZ by A4;
consider S be c=-linear finite simplex-like Subset-Family of KX such that
A5: A=(P|Y).:S by Def20;
S/\Y c=S by XBOOLE_1:17;
then reconsider SY=S/\Y as c=-linear finite simplex-like Subset-Family of KX
by TOPS_2:11;
A6: dom(P|Y)c=Y & dom(P|Y)/\S c=dom(P|Y) by RELAT_1:58,XBOOLE_1:17;
then A7: dom(P|Y)/\S c=Y;
B=(P|Y).:(dom(P|Y)/\S) by A5,RELAT_1:112
.=P.:(dom(P|Y)/\S) by A6,RELAT_1:129,XBOOLE_1:1
.=(P|Z).:(dom(P|Y)/\S) by A2,A7,RELAT_1:129,XBOOLE_1:1
.=(P|Z).:(dom(P|Z)/\SY) by A3,XBOOLE_1:16
.=(P|Z).:SY by RELAT_1:112;
then B is simplex-like by Def20;
hence thesis;
end;
theorem
dom P/\the topology of KX c= Y implies
subdivision(P|Y,KX) = subdivision(P,KX)
proof
set PX=subdivision(P|Y,KX);
set PP=subdivision(P,KX);
A1: (P|Y)|dom(P|Y)=P|(dom(P|Y)) by RELAT_1:58,74;
A2: [#]PX=[#]KX & [#]PP=[#]KX by Def20;
assume A3: dom P/\the topology of KX c=Y;
A4: the topology of PP c=the topology of PX
proof
let x be object;
assume x in the topology of PP;
then reconsider A=x as Simplex of PP by PRE_TOPC:def 2;
reconsider B=A as Subset of PX by A2;
consider S be c=-linear finite simplex-like Subset-Family of KX such that
A5: A=P.:S by Def20;
A6: S/\dom P c=Y
proof
let x be object;
assume A7: x in S/\dom P;
then reconsider A=x as Subset of KX;
x in S by A7,XBOOLE_0:def 4;
then A is simplex-like by TOPS_2:def 1;
then A8: A in the topology of KX;
x in dom P by A7,XBOOLE_0:def 4;
then A in (the topology of KX)/\dom P by A8,XBOOLE_0:def 4;
hence thesis by A3;
end;
then A9: S/\dom P/\Y=S/\dom P by XBOOLE_1:28;
B=P.:(S/\dom P) by A5,RELAT_1:112
.=(P|Y).:(S/\dom P/\Y) by A6,A9,RELAT_1:129
.=(P|Y).:(S/\(dom P/\Y)) by XBOOLE_1:16
.=(P|Y).:(S/\dom(P|Y)) by RELAT_1:61
.=(P|Y).:S by RELAT_1:112;
then B is simplex-like by Def20;
hence thesis;
end;
P|dom P=P & P|Y=(P|Y)|dom(P|Y);
then PX is SubSimplicialComplex of PP by A1,Th54,RELAT_1:60;
then the topology of PX c=the topology of PP by Def13;
hence thesis by A2,A4,XBOOLE_0:def 10;
end;
theorem Th56:
Y c= Z implies
subdivision(Y|`P,KX) is SubSimplicialComplex of subdivision(Z|`P,KX)
proof
assume A1: Y c=Z;
set PZ=subdivision(Z|`P,KX);
set PY=subdivision(Y|`P,KX);
A2: [#]PY=[#]KX by Def20;
hence [#]PY c=[#]PZ by Def20;
let x be object;
assume x in the topology of PY;
then reconsider A=x as Simplex of PY by PRE_TOPC:def 2;
consider S be c=-linear finite simplex-like Subset-Family of KX such that
A3: A=Y|`P.:S by Def20;
S/\dom(Y|`P)c=S by XBOOLE_1:17;
then reconsider Sd=S/\dom(Y|`P)
as c=-linear finite simplex-like Subset-Family of KX by TOPS_2:11;
Y|`(Z|`P)=Y|`P by A1,RELAT_1:99;
then A4: (Y|`P).:Sd c=(Z|`P).:Sd by RELAT_1:86,124;
[#]PZ=[#]KX by Def20;
then reconsider A as Subset of PZ by A2;
A5: Z|`P.:Sd c=Y|`P.:Sd
proof
let y be object;
assume y in (Z|`P).:Sd;
then consider x being object such that
A6: x in dom(Z|`P) and
A7: x in Sd and
A8: (Z|`P).x=y by FUNCT_1:def 6;
A9: x in dom(Y|`P) by A7,XBOOLE_0:def 4;
P.x=y by A6,A8,FUNCT_1:53;
then (Y|`P).x=y by A9,FUNCT_1:53;
hence thesis by A7,A9,FUNCT_1:def 6;
end;
A=Y|`P.:Sd by A3,RELAT_1:112;
then A=Z|`P.:Sd by A4,A5;
then A is simplex-like by Def20;
hence thesis;
end;
theorem
P.:(the topology of KX) c= Y implies subdivision(Y|`P,KX) = subdivision(P,KX)
proof
set PK=subdivision(P,KX);
P=rng P|`P & Y|`(rng P|`P)=(Y/\rng P)|`P by RELAT_1:96;
then reconsider PY=subdivision(Y|`P,KX) as SubSimplicialComplex of PK
by Th56,XBOOLE_1:17;
A1: [#]PY=[#]KX & [#]PK=[#]KX by Def20;
assume A2: P.:(the topology of KX)c=Y;
A3: the topology of PK c=the topology of PY
proof
let x be object;
assume x in the topology of PK;
then reconsider A=x as Simplex of PK by PRE_TOPC:def 2;
consider S be c=-linear finite simplex-like Subset-Family of KX such that
A4: A=P.:S by Def20;
reconsider A as Subset of PY by A1;
S c=the topology of KX
proof
let y be object such that
A5: y in S;
reconsider y as Subset of KX by A5;
y is simplex-like by A5,TOPS_2:def 1;
hence thesis;
end;
then A c=P.:(the topology of KX) by A4,RELAT_1:123;
then A/\Y=A by A2,XBOOLE_1:1,28;
then A=Y|`P.:S by A4,FUNCT_1:67;
then A is simplex-like by Def20;
hence thesis;
end;
the topology of PY c=the topology of PK by Def13;
hence thesis by A1,A3,XBOOLE_0:def 10;
end;
theorem Th58:
subdivision(P,SX) is SubSimplicialComplex of subdivision(P,KX)
proof
set PS=subdivision(P,SX);
set PK=subdivision(P,KX);
A1: [#]SX c=[#]KX by Def13;
A2: [#]PK=[#]KX by Def20;
hence [#]PS c=[#]PK by A1,Def20;
let x be object;
assume x in the topology of PS;
then reconsider A=x as Simplex of PS by PRE_TOPC:def 2;
[#]PS=[#]SX by Def20;
then reconsider B=A as Subset of PK by A1,A2,XBOOLE_1:1;
consider SS be c=-linear finite simplex-like Subset-Family of SX such that
A3: A=P.:SS by Def20;
bool[#]SX c=bool[#]KX by A1,ZFMISC_1:67;
then reconsider SK=SS as c=-linear finite Subset-Family of KX by XBOOLE_1:1;
SK is simplex-like
proof
let C be Subset of KX;
assume A4: C in SK;
then reconsider c =C as Subset of SX;
c is simplex-like by A4,TOPS_2:def 1;
then A5: c in the topology of SX;
the topology of SX c=the topology of KX by Def13;
hence thesis by A5;
end;
then B is simplex-like by A3,Def20;
hence thesis;
end;
theorem
for A be Subset of subdivision(P,KX) st
dom P c=the topology of SX & A = [#]SX
holds subdivision(P,SX)=subdivision(P,KX)|A
proof
set PK=subdivision(P,KX);
reconsider PS=subdivision(P,SX) as strict SubSimplicialComplex of PK by Th58;
let A be Subset of subdivision(P,KX) such that
A1: dom P c=the topology of SX and
A2: A=[#]SX;
now let a be Subset of PS;
assume a in the topology of PK;
then reconsider b=a as Simplex of PK by PRE_TOPC:def 2;
consider SS be c=-linear finite simplex-like Subset-Family of KX such that
A3: b=P.:SS by Def20;
SS/\dom P c=dom P by XBOOLE_1:17;
then A4: SS/\dom P c=the topology of SX by A1;
SS/\dom P c=SS by XBOOLE_1:17;
then reconsider Sd=SS/\dom P as c=-linear finite Subset-Family of SX by A4,
XBOOLE_1:1;
A5: Sd is simplex-like
proof
let B be Subset of SX;
assume B in Sd;
then B in dom P by XBOOLE_0:def 4;
hence thesis by A1;
end;
P.:SS=P.:Sd by RELAT_1:112;
hence a is simplex-like by A3,A5,Def20;
end;
then A6: PS is maximal;
[#]PS=[#]SX by Def20;
hence thesis by A2,A6,Def16;
end;
theorem Th60:
for K1,K2 be SimplicialComplexStr of X st
the TopStruct of K1 = the TopStruct of K2
holds subdivision(P,K1) = subdivision(P,K2)
proof
let K1,K2 be SimplicialComplexStr of X such that
A1: the TopStruct of K1=the TopStruct of K2;
set P1=subdivision(P,K1),P2=subdivision(P,K2);
A2: [#]K1=[#]P1 & [#]K2=[#]P2 by Def20;
A3: the topology of P1 c=the topology of P2
proof
let x be object;
assume A4: x in the topology of P1;
then reconsider A=x as Subset of P1;
reconsider A1=A as Subset of P2 by A1,A2;
A is simplex-like by A4;
then consider S be c=-linear finite simplex-like Subset-Family of K1 such
that
A5: A=P.:S by Def20;
reconsider S1=S as Subset-Family of K2 by A1;
S c=the topology of K1 by Th14;
then S1 is simplex-like by A1,Th14;
then A1 is simplex-like by A5,Def20;
hence thesis;
end;
the topology of P2 c=the topology of P1
proof
let x be object;
assume A6: x in the topology of P2;
then reconsider A=x as Subset of P2;
reconsider A1=A as Subset of P1 by A1,A2;
A is simplex-like by A6;
then consider S be c=-linear finite simplex-like Subset-Family of K2 such
that
A7: A=P.:S by Def20;
reconsider S1=S as Subset-Family of K1 by A1;
S c=the topology of K2 by Th14;
then S1 is simplex-like by A1,Th14;
then A1 is simplex-like by A7,Def20;
hence thesis;
end;
hence thesis by A1,A2,A3,XBOOLE_0:def 10;
end;
definition
let X,KX,P,n;
func subdivision(n,P,KX) -> SimplicialComplexStr of X means :Def21:
ex F be Function st F.0 = KX & F.n = it & dom F = NAT &
for k for KX1 be SimplicialComplexStr of X st KX1 = F.k
holds F.(k+1) = subdivision(P,KX1);
existence
proof
defpred F[object,object] means
for SX be SimplicialComplexStr of X st the topology of SX=$1 & [#]SX=[#]KX
holds the topology of subdivision(P,SX)=$2;
set BBK=bool bool[#]KX;
A1: for x being object st x in BBK ex y being object st y in BBK & F[x,y]
proof
let x be object;
assume A2: x in BBK;
per cases;
suppose ex SX be SimplicialComplexStr of X st the topology of SX=x & [#]SX=
[#]KX;
then consider SX be SimplicialComplexStr of X such that
A3: the topology of SX=x and
A4: [#]SX=[#]KX;
take T=the topology of subdivision(P,SX);
[#]subdivision(P,SX)=[#]SX by Def20;
hence T in BBK by A4;
let SX1 be SimplicialComplexStr of X such that
A5: the topology of SX1=x & [#]SX1=[#]KX;
the TopStruct of SX=the TopStruct of SX1 by A3,A4,A5;
hence thesis by Th60;
end;
suppose A6: for SX be SimplicialComplexStr of X holds the topology of SX<>x
or[#]SX<>[#]KX;
take x;
thus thesis by A2,A6;
end;
end;
consider f being Function of BBK,BBK such that
A7: for x being object st x in BBK holds F[x,f.x] from FUNCT_2:sch 1(A1);
deffunc G(set,set)=f.$2;
consider g being Function such that
A8: dom g=NAT & g.0=the topology of KX & for n being Nat holds g.(n+1)=G(n,
g.n) from NAT_1:sch 11;
defpred P[Nat] means
(ex SX be SimplicialComplexStr of X st the topology of SX=g.$1 & [#]SX=[#]KX
& ($1>0 implies SX is strict)) & for SX be SimplicialComplexStr of X st the
topology of SX=g.$1 & [#]SX=[#]KX holds g.($1+1)=
the topology of subdivision(P,SX);
g.(0+1)=f.(the topology of KX) by A8;
then A9: g.1=the topology of subdivision(P,KX) by A7;
A10: P[0 qua Nat]
proof
thus ex SX be SimplicialComplexStr of X st the topology of SX=g.0 & [#]SX=
[#]KX & (0>0 implies SX is strict) by A8;
let SX be SimplicialComplexStr of X;
assume the topology of SX=g.0 & [#]SX=[#]KX;
then the TopStruct of SX=the TopStruct of KX by A8;
hence thesis by A9,Th60;
end;
defpred H[object,object] means
for k be Nat st k=$1 holds(k=0 implies $2=KX) & (k>0 implies for SF be
Subset-Family of KX st SF=g.k holds$2=TopStruct(# the carrier of KX,SF #));
A11: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
set k1=k+1;
given SX be SimplicialComplexStr of X such that
A12: the topology of SX=g.k and
A13: [#]SX=[#]KX and
k>0 implies SX is strict;
assume for SX be SimplicialComplexStr of X st the topology of SX=g.k & [#]SX
=[#]KX holds g.k1=the topology of subdivision(P,SX);
then A14: g.k1=the topology of subdivision(P,SX) by A12,A13;
[#]subdivision(P,SX)=[#]KX by A13,Def20;
hence ex SX be SimplicialComplexStr of X st the topology of SX=g.k1 &
[#]SX=[#]KX & (k1>0 implies SX is strict) by A14;
let S1 be SimplicialComplexStr of X;
assume A15: the topology of S1=g.k1 & [#]S1=[#]KX;
g.(k1+1)=f.(g.k1) by A8;
hence thesis by A7,A15;
end;
A16: for k be Nat holds P[k] from NAT_1:sch 2(A10,A11);
A17: for x being object st x in NAT ex y being object st H[x,y]
proof
let x be object;
assume x in NAT;
then reconsider m=x as Nat;
per cases;
suppose A18: m=0;
take KX;
thus thesis by A18;
end;
suppose A19: m>0;
consider K1 be SimplicialComplexStr of X such that
A20: the topology of K1=g.m and
A21: [#]K1=[#]KX and
m>0 implies K1 is strict by A16;
reconsider TOP=the topology of K1 as Subset-Family of KX by A21;
take TopStruct(# the carrier of KX,TOP #);
thus thesis by A19,A20;
end;
end;
consider h being Function such that
A22: dom h=NAT &
for x being object st x in NAT holds H[x,h.x] from CLASSES1:sch 1(A17);
A23: h.0=KX by A22;
A24: for k be Nat for K1 be SimplicialComplexStr of X st h.k=K1 holds h.(k+1)
=subdivision(P,K1)
proof
let k be Nat;
let KK be SimplicialComplexStr of X such that
A25: h.k=KK;
P[k+1] by A16;
then consider K1 be SimplicialComplexStr of X such that
A26: the topology of K1=g.(k+1) and
A27: [#]K1=[#]KX;
reconsider TOP1=the topology of K1 as Subset-Family of KX by A27;
A28: k in NAT by ORDINAL1:def 12;
P[k] by A16;
then consider K2 be SimplicialComplexStr of X such that
A29: the topology of K2=g.k and
A30: [#]K2=[#]KX;
reconsider TOP2=the topology of K2 as Subset-Family of KX by A30;
A31: [#]subdivision(P,KK)=[#]KK by Def20;
per cases;
suppose A32: k=0;
then TOP1=the topology of subdivision(P,KK) by A8,A10,A23,A25,A26;
hence thesis by A22,A23,A25,A26,A31,A32;
end;
suppose k>0;
then A33: KK=TopStruct(# the carrier of KX,TOP2 #) by A22,A25,A28,A29;
then [#]KK=[#]KX;
then g.(k+1)=the topology of subdivision(P,KK) by A16,A29,A33;
hence thesis by A22,A31,A33;
end;
end;
per cases;
suppose A34: n=0;
take KX;
thus thesis by A22,A23,A24,A34;
end;
suppose A35: n>0;
consider K1 be SimplicialComplexStr of X such that
A36: the topology of K1=g.n and
A37: [#]K1=[#]KX and
A38: n>0 implies K1 is strict by A16;
reconsider K1 as strict SimplicialComplexStr of X by A35,A38;
take K1,h;
thus h.0=KX by A22;
n in NAT by ORDINAL1:def 12;
hence thesis by A22,A24,A35,A36,A37;
end;
end;
uniqueness
proof
let P1,P2 be SimplicialComplexStr of X;
given F1 be Function such that
A39: F1.0=KX and
A40: F1.n=P1 and
dom F1=NAT and
A41: for k for KX1 be SimplicialComplexStr of X st KX1=F1.k holds F1.(k+1)=
subdivision(P,KX1);
given F2 be Function such that
A42: F2.0=KX and
A43: F2.n=P2 and
dom F2=NAT and
A44: for k for KX1 be SimplicialComplexStr of X st KX1=F2.k holds F2.(k+1)=
subdivision(P,KX1);
defpred P[Nat] means
F1.$1=F2.$1 & ex KX1 be SimplicialComplexStr of X st KX1=F1.$1;
A45: for k st P[k] holds P[k+1]
proof
let k such that
A46: P[k];
consider KX1 be SimplicialComplexStr of X such that
A47: KX1=F1.k by A46;
F1.(k+1)=subdivision(P,KX1) by A41,A47;
hence thesis by A44,A46,A47;
end;
A48: P[0 qua Nat] by A39,A42;
for k holds P[k] from NAT_1:sch 2(A48,A45);
hence thesis by A40,A43;
end;
end;
theorem Th61:
subdivision(0,P,KX) = KX
proof
ex F be Function st F.0=KX & F.0=subdivision(0,P,KX) & dom F=NAT & for k for
KX1 be SimplicialComplexStr of X st KX1=F.k holds
F.(k+1)=subdivision(P,KX1) by Def21;
hence thesis;
end;
theorem Th62:
subdivision(1,P,KX) = subdivision(P,KX)
proof
consider F be Function such that
A1: F.0=KX and
A2: F.1=subdivision(1,P,KX) and
dom F=NAT and
A3: for k for KX1 be SimplicialComplexStr of X st KX1=F.k holds F.(k+1)=
subdivision(P,KX1) by Def21;
F.(0+1)=subdivision(P,KX) by A1,A3;
hence thesis by A2;
end;
theorem Th63:
for n,k be Element of NAT holds
subdivision(n+k,P,KX) = subdivision(n,P,subdivision(k,P,KX))
proof
let n,k be Element of NAT;
consider Fn be Function such that
A1: Fn.0=subdivision(k,P,KX) and
A2: Fn.n=subdivision(n,P,subdivision(k,P,KX)) and
dom Fn=NAT and
A3: for m be Nat for KX1 be SimplicialComplexStr of X st KX1=Fn.m holds Fn.(
m+1)=subdivision(P,KX1) by Def21;
consider Fnm be Function such that
A4: Fnm.0=KX and
A5: Fnm.(n+k)=subdivision(n+k,P,KX) and
dom Fnm=NAT and
A6: for m be Nat for KX1 be SimplicialComplexStr of X st KX1=Fnm.m holds Fnm
.(m+1)=subdivision(P,KX1) by Def21;
defpred R[Nat] means
$1<=n implies Fn.$1=Fnm.($1+k) & ex SX be SimplicialComplexStr of X st Fn.$1
=SX;
A7: for m be Nat st R[m] holds R[m+1]
proof
let m be Nat such that
A8: R[m];
assume A9: m+1<=n;
then consider SX be SimplicialComplexStr of X such that
A10: Fn.m=SX by A8,NAT_1:13;
subdivision(P,SX)=Fnm.(m+k+1) by A6,A8,A9,A10,NAT_1:13;
hence thesis by A3,A10;
end;
consider Fm be Function such that
A11: Fm.0=KX and
A12: Fm.k=subdivision(k,P,KX) and
dom Fm=NAT and
A13: for m be Nat for KX1 be SimplicialComplexStr of X st KX1=Fm.m holds Fm.
(m+1)=subdivision(P,KX1) by Def21;
defpred P[Nat] means
$1<=k implies Fm.$1=Fnm.$1 & ex SX be SimplicialComplexStr of X st Fm.$1=SX;
A14: for m be Nat st P[m] holds P[m+1]
proof
let m be Nat such that
A15: P[m];
assume A16: m+1<=k;
then consider SX be SimplicialComplexStr of X such that
A17: Fm.m=SX by A15,NAT_1:13;
subdivision(P,SX)=Fnm.(m+1) by A6,A15,A16,A17,NAT_1:13;
hence thesis by A13,A17;
end;
A18: P[0 qua Nat] by A4,A11;
for k holds P[k] from NAT_1:sch 2(A18,A14);
then A19: R[0 qua Nat] by A1,A12;
for k holds R[k] from NAT_1:sch 2(A19,A7);
hence thesis by A2,A5;
end;
theorem
[#]subdivision(n,P,KX) = [#]KX
proof
defpred P[Nat] means
[#]subdivision($1,P,KX)=[#]KX;
A1: for n st P[n] holds P[n+1]
proof
let n;
n in NAT by ORDINAL1:def 12;
then A2: subdivision(n+1,P,KX)=subdivision(1,P,subdivision(n,P,KX)) by Th63
.=subdivision(P,subdivision(n,P,KX)) by Th62;
assume[#]subdivision(n,P,KX)=[#]KX;
hence thesis by A2,Def20;
end;
A3: P[0 qua Nat] by Th61;
for n holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem
subdivision(n,P,SX) is SubSimplicialComplex of subdivision(n,P,KX)
proof
defpred P[Nat] means
subdivision($1,P,SX) is SubSimplicialComplex of subdivision($1,P,KX);
A1: for n st P[n] holds P[n+1]
proof
let n;
assume P[n];
then reconsider Pn=subdivision(n,P,SX) as
SubSimplicialComplex of subdivision(n,P,KX);
A2: n in NAT by ORDINAL1:def 12;
then A3: subdivision(n+1,P,SX)=subdivision(1,P,Pn) by Th63
.=subdivision(P,Pn) by Th62;
subdivision(n+1,P,KX)=subdivision(1,P,subdivision(n,P,KX)) by A2,Th63
.=subdivision(P,subdivision(n,P,KX)) by Th62;
hence thesis by A3,Th58;
end;
subdivision(0,P,SX)=SX by Th61;
then A4: P[0] by Th61;
for n holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;