:: Abstract Simplicial Complexes
:: by Karol P\c{a}k
::
:: Copyright (c) 2009-2019 Association of Mizar Users

notation end;

registration
coherence
for b1 being set st b1 is empty holds
b1 is subset-closed
;
cluster with_empty_element -> non empty for set ;
coherence
for b1 being set st b1 is with_empty_element holds
not b1 is empty
;
coherence
for b1 being set st not b1 is empty & b1 is subset-closed holds
b1 is with_empty_element
proof end;
end;

registration
let X be set ;
coherence by COHSP_1:def 3;
end;

registration
let X be subset-closed set ;
coherence ;
end;

theorem :: SIMPLEX0:1
for Y being set holds
( Y is subset-closed iff for X being set st X in Y holds
bool X c= Y )
proof end;

registration
let A, B be subset-closed set ;
coherence
A \/ B is subset-closed
proof end;
coherence
A /\ B is subset-closed
proof end;
end;

Lm1: for X being set ex F being subset-closed set st
( F = union { (bool x) where x is Element of X : x in X } & X c= F & ( for Y being set st X c= Y & Y is subset-closed holds
F c= Y ) )

proof end;

definition
let X be set ;
func subset-closed_closure_of X -> subset-closed set means :Def1: :: SIMPLEX0:def 1
( X c= it & ( for Y being set st X c= Y & Y is subset-closed holds
it c= Y ) );
existence
ex b1 being subset-closed set st
( X c= b1 & ( for Y being set st X c= Y & Y is subset-closed holds
b1 c= Y ) )
proof end;
uniqueness
for b1, b2 being subset-closed set st X c= b1 & ( for Y being set st X c= Y & Y is subset-closed holds
b1 c= Y ) & X c= b2 & ( for Y being set st X c= Y & Y is subset-closed holds
b2 c= Y ) holds
b1 = b2
;
end;

:: deftheorem Def1 defines subset-closed_closure_of SIMPLEX0:def 1 :
for X being set
for b2 being subset-closed set holds
( b2 = subset-closed_closure_of X iff ( X c= b2 & ( for Y being set st X c= Y & Y is subset-closed holds
b2 c= Y ) ) );

theorem Th2: :: SIMPLEX0:2
for x, X being set holds
( x in subset-closed_closure_of X iff ex y being set st
( x c= y & y in X ) )
proof end;

definition
let X be set ;
let F be Subset-Family of X;
:: original: subset-closed_closure_of
redefine func subset-closed_closure_of F -> subset-closed Subset-Family of X;
coherence
proof end;
end;

registration
coherence
proof end;
let X be non empty set ;
coherence
proof end;
end;

registration
let X be with_non-empty_element set ;
coherence
proof end;
end;

registration
let X be finite-membered set ;
coherence
proof end;
end;

theorem Th3: :: SIMPLEX0:3
for X, Y being set st X c= Y & Y is subset-closed holds
subset-closed_closure_of X c= Y
proof end;

theorem Th4: :: SIMPLEX0:4
for X being set holds subset-closed_closure_of {X} = bool X
proof end;

theorem :: SIMPLEX0:5
for X, Y being set holds subset-closed_closure_of (X \/ Y) = \/
proof end;

theorem Th6: :: SIMPLEX0:6
for X, Y being set holds
( X is_finer_than Y iff subset-closed_closure_of X c= subset-closed_closure_of Y )
proof end;

theorem Th7: :: SIMPLEX0:7
for X being set st X is subset-closed holds
subset-closed_closure_of X = X by Def1;

theorem :: SIMPLEX0:8
for X being set st subset-closed_closure_of X c= X holds
X is subset-closed
proof end;

definition
let Y, X, n be set ;
func the_subsets_with_limited_card (n,X,Y) -> Subset-Family of Y means :Def2: :: SIMPLEX0:def 2
for A being Subset of Y holds
( A in it iff ( A in X & card A c= n ) );
existence
ex b1 being Subset-Family of Y st
for A being Subset of Y holds
( A in b1 iff ( A in X & card A c= n ) )
proof end;
uniqueness
for b1, b2 being Subset-Family of Y st ( for A being Subset of Y holds
( A in b1 iff ( A in X & card A c= n ) ) ) & ( for A being Subset of Y holds
( A in b2 iff ( A in X & card A c= n ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines the_subsets_with_limited_card SIMPLEX0:def 2 :
for Y, X, n being set
for b4 being Subset-Family of Y holds
( b4 = the_subsets_with_limited_card (n,X,Y) iff for A being Subset of Y holds
( A in b4 iff ( A in X & card A c= n ) ) );

registration
let D be non empty set ;
existence
ex b1 being Subset-Family of D st
( b1 is finite & b1 is with_non-empty_element & b1 is subset-closed & b1 is finite-membered )
proof end;
end;

registration
let Y, X be set ;
let n be finite Cardinal;
coherence
proof end;
end;

registration
let Y be set ;
let X be subset-closed set ;
let n be Cardinal;
coherence
proof end;
end;

registration
let Y be set ;
let X be with_empty_element set ;
let n be Cardinal;
coherence
proof end;
end;

registration
let D be non empty set ;
let X be with_non-empty_element subset-closed Subset-Family of D;
let n be non empty Cardinal;
coherence
not the_subsets_with_limited_card (n,X,D) is empty-membered
proof end;
end;

notation
let X be set ;
let Y be Subset-Family of X;
let n be set ;
synonym the_subsets_with_limited_card (n,Y) for the_subsets_with_limited_card (n,Y,X);
end;

theorem Th9: :: SIMPLEX0:9
for X being set st not X is empty & X is finite & X is c=-linear holds
union X in X
proof end;

theorem Th10: :: SIMPLEX0:10
for X being c=-linear finite set st X is with_non-empty_elements holds
card X c= card ()
proof end;

theorem :: SIMPLEX0:11
for x, X being set st X is c=-linear holds
X \/ {(() \/ x)} is c=-linear
proof end;

theorem Th12: :: SIMPLEX0:12
for X being non empty set ex Y being Subset-Family of X st
( Y is with_non-empty_elements & Y is c=-linear & X in Y & card X = card Y & ( for Z being set st Z in Y & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y ) ) )
proof end;

theorem :: SIMPLEX0:13
for X being set
for Y being Subset-Family of X st Y is finite & Y is with_non-empty_elements & Y is c=-linear & X in Y holds
ex Y1 being Subset-Family of X st
( Y c= Y1 & Y1 is with_non-empty_elements & Y1 is c=-linear & card X = card Y1 & ( for Z being set st Z in Y1 & card Z <> 1 holds
ex x being set st
( x in Z & Z \ {x} in Y1 ) ) )
proof end;

definition end;

notation
let K be SimplicialComplexStr;
let A be Subset of K;
synonym simplex-like A for open ;
end;

notation
let K be SimplicialComplexStr;
let S be Subset-Family of K;
synonym simplex-like S for open ;
end;

registration
let K be SimplicialComplexStr;
cluster empty simplex-like for Element of bool (bool the carrier of K);
existence
ex b1 being Subset-Family of K st
( b1 is empty & b1 is simplex-like )
proof end;
end;

theorem Th14: :: SIMPLEX0:14
for K being SimplicialComplexStr
for S being Subset-Family of K holds
( S is simplex-like iff S c= the topology of K )
proof end;

definition
let K be SimplicialComplexStr;
let v be Element of K;
attr v is vertex-like means :: SIMPLEX0:def 3
ex S being Subset of K st
( S is simplex-like & v in S );
end;

:: deftheorem defines vertex-like SIMPLEX0:def 3 :
for K being SimplicialComplexStr
for v being Element of K holds
( v is vertex-like iff ex S being Subset of K st
( S is simplex-like & v in S ) );

definition
let K be SimplicialComplexStr;
func Vertices K -> Subset of K means :Def4: :: SIMPLEX0:def 4
for v being Element of K holds
( v in it iff v is vertex-like );
existence
ex b1 being Subset of K st
for v being Element of K holds
( v in b1 iff v is vertex-like )
proof end;
uniqueness
for b1, b2 being Subset of K st ( for v being Element of K holds
( v in b1 iff v is vertex-like ) ) & ( for v being Element of K holds
( v in b2 iff v is vertex-like ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Vertices SIMPLEX0:def 4 :
for K being SimplicialComplexStr
for b2 being Subset of K holds
( b2 = Vertices K iff for v being Element of K holds
( v in b2 iff v is vertex-like ) );

definition end;

definition
let K be SimplicialComplexStr;
attr K is finite-vertices means :Def5: :: SIMPLEX0:def 5
Vertices K is finite ;
end;

:: deftheorem Def5 defines finite-vertices SIMPLEX0:def 5 :
for K being SimplicialComplexStr holds
( K is finite-vertices iff Vertices K is finite );

definition
let K be SimplicialComplexStr;
attr K is locally-finite means :: SIMPLEX0:def 6
for v being Vertex of K holds { S where S is Subset of K : ( S is simplex-like & v in S ) } is finite ;
end;

:: deftheorem defines locally-finite SIMPLEX0:def 6 :
for K being SimplicialComplexStr holds
( K is locally-finite iff for v being Vertex of K holds { S where S is Subset of K : ( S is simplex-like & v in S ) } is finite );

definition
let K be SimplicialComplexStr;
attr K is empty-membered means :Def7: :: SIMPLEX0:def 7
the topology of K is empty-membered ;
attr K is with_non-empty_elements means :Def8: :: SIMPLEX0:def 8
the topology of K is with_non-empty_elements ;
end;

:: deftheorem Def7 defines empty-membered SIMPLEX0:def 7 :
for K being SimplicialComplexStr holds
( K is empty-membered iff the topology of K is empty-membered );

:: deftheorem Def8 defines with_non-empty_elements SIMPLEX0:def 8 :
for K being SimplicialComplexStr holds
( K is with_non-empty_elements iff the topology of K is with_non-empty_elements );

notation end;

definition
let X be set ;
mode SimplicialComplexStr of X -> SimplicialComplexStr means :Def9: :: SIMPLEX0:def 9
[#] it c= X;
existence
ex b1 being SimplicialComplexStr st [#] b1 c= X
proof end;
end;

:: deftheorem Def9 defines SimplicialComplexStr SIMPLEX0:def 9 :
for X being set
for b2 being SimplicialComplexStr holds
( b2 is SimplicialComplexStr of X iff [#] b2 c= X );

definition
let X be set ;
let KX be SimplicialComplexStr of X;
attr KX is total means :: SIMPLEX0:def 10
[#] KX = X;
end;

:: deftheorem defines total SIMPLEX0:def 10 :
for X being set
for KX being SimplicialComplexStr of X holds
( KX is total iff [#] KX = X );

Lm2: for K being SimplicialComplexStr holds
( Vertices K is empty iff K is empty-membered )

proof end;

Lm3: for x being set
for K being SimplicialComplexStr
for S being Subset of K st S is simplex-like & x in S holds
x in Vertices K

proof end;

Lm4: for K being SimplicialComplexStr
for A being Subset of K st A is simplex-like holds
A c= Vertices K

by Lm3;

Lm5: for K being SimplicialComplexStr holds Vertices K = union the topology of K
proof end;

Lm6: for K being SimplicialComplexStr st K is finite-vertices holds
the topology of K is finite

proof end;

registration
coherence
for b1 being SimplicialComplexStr st b1 is with_empty_element holds
not b1 is void
by PENCIL_1:def 4;
coherence
for b1 being SimplicialComplexStr st b1 is with_non-empty_element holds
not b1 is void
by PENCIL_1:def 4;
coherence
for b1 being SimplicialComplexStr st not b1 is void & b1 is empty-membered holds
b1 is with_empty_element
;
coherence
for b1 being SimplicialComplexStr st not b1 is void & b1 is subset-closed holds
b1 is with_empty_element
;
coherence
for b1 being SimplicialComplexStr st b1 is empty-membered holds
( b1 is subset-closed & b1 is finite-vertices )
proof end;
coherence
for b1 being SimplicialComplexStr st b1 is finite-vertices holds
( b1 is locally-finite & b1 is finite-degree )
proof end;
coherence
for b1 being SimplicialComplexStr st b1 is locally-finite & b1 is subset-closed holds
b1 is finite-membered
proof end;
end;

registration
let X be set ;
existence
ex b1 being SimplicialComplexStr of X st
( b1 is empty & b1 is void & b1 is empty-membered & b1 is strict )
proof end;
end;

registration
let D be non empty set ;
existence
ex b1 being SimplicialComplexStr of D st
( not b1 is empty & not b1 is void & b1 is total & b1 is empty-membered & b1 is strict )
proof end;
existence
ex b1 being SimplicialComplexStr of D st
( not b1 is empty & b1 is total & b1 is with_empty_element & b1 is with_non-empty_element & b1 is finite-vertices & b1 is subset-closed & b1 is strict )
proof end;
end;

registration
existence
ex b1 being SimplicialComplexStr st
( not b1 is empty & b1 is with_empty_element & b1 is with_non-empty_element & b1 is finite-vertices & b1 is subset-closed & b1 is strict )
proof end;
end;

registration
let K be with_non-empty_element SimplicialComplexStr;
cluster Vertices K -> non empty ;
coherence
not Vertices K is empty
by Lm2;
end;

registration
let K be finite-vertices SimplicialComplexStr;
cluster simplex-like -> finite for Element of bool (bool the carrier of K);
coherence
for b1 being Subset-Family of K st b1 is simplex-like holds
b1 is finite
proof end;
end;

registration
let K be finite-membered SimplicialComplexStr;
cluster simplex-like -> finite-membered for Element of bool (bool the carrier of K);
coherence
for b1 being Subset-Family of K st b1 is simplex-like holds
b1 is finite-membered
proof end;
end;

theorem :: SIMPLEX0:15
for K being SimplicialComplexStr holds
( Vertices K is empty iff K is empty-membered ) by Lm2;

theorem :: SIMPLEX0:16
for K being SimplicialComplexStr holds Vertices K = union the topology of K by Lm5;

theorem :: SIMPLEX0:17
for K being SimplicialComplexStr
for S being Subset of K st S is simplex-like holds
S c= Vertices K by Lm4;

theorem :: SIMPLEX0:18
for K being SimplicialComplexStr st K is finite-vertices holds
the topology of K is finite by Lm6;

theorem Th19: :: SIMPLEX0:19
for K being SimplicialComplexStr st the topology of K is finite & not K is finite-vertices holds
not K is finite-membered
proof end;

theorem Th20: :: SIMPLEX0:20
for K being SimplicialComplexStr st K is subset-closed & the topology of K is finite holds
K is finite-vertices
proof end;

definition
let X be set ;
let Y be Subset-Family of X;
func Complex_of Y -> strict SimplicialComplexStr of X equals :: SIMPLEX0:def 11
TopStruct(# X, #);
coherence
TopStruct(# X, #) is strict SimplicialComplexStr of X
proof end;
end;

:: deftheorem defines Complex_of SIMPLEX0:def 11 :
for X being set
for Y being Subset-Family of X holds Complex_of Y = TopStruct(# X, #);

registration
let X be set ;
let Y be Subset-Family of X;
coherence ;
end;

registration
let X be set ;
let Y be non empty Subset-Family of X;
coherence ;
end;

registration
let X be set ;
let Y be finite-membered Subset-Family of X;
coherence ;
end;

registration
let X be set ;
let Y be finite finite-membered Subset-Family of X;
coherence
proof end;
end;

theorem :: SIMPLEX0:21
for K being SimplicialComplexStr st K is subset-closed holds
TopStruct(# the carrier of K, the topology of K #) = Complex_of the topology of K by Th7;

definition 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 Element of bool the carrier of K;
coherence
for b1 being Subset of K st b1 is empty holds
b1 is simplex-like
proof end;
cluster empty simplex-like for Element of bool the carrier of K;
existence
ex b1 being Simplex of K st b1 is empty
proof end;
end;

registration
let K be non void finite-membered SimplicialComplexStr;
cluster finite simplex-like for Element of bool the carrier of K;
existence
ex b1 being Simplex of K st b1 is finite
proof end;
end;

definition
let K be SimplicialComplexStr;
func degree K -> ExtReal means :Def12: :: SIMPLEX0:def 12
( ( for S being finite Subset of K st S is simplex-like holds
card S <= it + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = it + 1 ) ) if ( not K is void & K is finite-degree )
it = - 1 if K is void
otherwise it = +infty ;
existence
( ( not K is void & K is finite-degree implies ex b1 being ExtReal st
( ( for S being finite Subset of K st S is simplex-like holds
card S <= b1 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b1 + 1 ) ) ) & ( K is void implies ex b1 being ExtReal st b1 = - 1 ) & ( ( K is void or not K is finite-degree ) & not K is void implies ex b1 being ExtReal st b1 = +infty ) )
proof end;
uniqueness
for b1, b2 being ExtReal holds
( ( not K is void & K is finite-degree & ( for S being finite Subset of K st S is simplex-like holds
card S <= b1 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b1 + 1 ) & ( for S being finite Subset of K st S is simplex-like holds
card S <= b2 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b2 + 1 ) implies b1 = b2 ) & ( K is void & b1 = - 1 & b2 = - 1 implies b1 = b2 ) & ( ( K is void or not K is finite-degree ) & not K is void & b1 = +infty & b2 = +infty implies b1 = b2 ) )
proof end;
consistency
for b1 being ExtReal st not K is void & K is finite-degree & K is void holds
( ( ( for S being finite Subset of K st S is simplex-like holds
card S <= b1 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b1 + 1 ) ) iff b1 = - 1 )
;
end;

:: deftheorem Def12 defines degree SIMPLEX0:def 12 :
for K being SimplicialComplexStr
for b2 being ExtReal holds
( ( not K is void & K is finite-degree implies ( b2 = degree K iff ( ( for S being finite Subset of K st S is simplex-like holds
card S <= b2 + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b2 + 1 ) ) ) ) & ( K is void implies ( b2 = degree K iff b2 = - 1 ) ) & ( ( K is void or not K is finite-degree ) & not K is void implies ( b2 = degree K iff b2 = +infty ) ) );

registration
let K be finite-degree SimplicialComplexStr;
cluster () + 1 -> natural ;
coherence
() + 1 is natural
proof end;
coherence
proof end;
end;

theorem Th22: :: SIMPLEX0:22
for K being SimplicialComplexStr holds
( degree K = - 1 iff K is empty-membered )
proof end;

theorem Th23: :: SIMPLEX0:23
for K being SimplicialComplexStr holds - 1 <= degree K
proof end;

theorem Th24: :: SIMPLEX0:24
for K being SimplicialComplexStr
for S being finite Subset of K st S is simplex-like holds
card S <= () + 1
proof end;

theorem Th25: :: SIMPLEX0:25
for i being Integer
for K being SimplicialComplexStr st ( not K is void or i >= - 1 ) holds
( degree K <= i iff ( K is finite-membered & ( for S being finite Subset of K st S is simplex-like holds
card S <= i + 1 ) ) )
proof end;

theorem :: SIMPLEX0:26
for X being set
for A being finite Subset of X holds degree () = (card A) - 1
proof end;

definition
let X be set ;
let KX be SimplicialComplexStr of X;
mode SubSimplicialComplex of KX -> SimplicialComplex of X means :Def13: :: SIMPLEX0:def 13
( [#] it c= [#] KX & the topology of it c= the topology of KX );
existence
ex b1 being SimplicialComplex of X st
( [#] b1 c= [#] KX & the topology of b1 c= the topology of KX )
proof end;
end;

:: deftheorem Def13 defines SubSimplicialComplex SIMPLEX0:def 13 :
for X being set
for KX being SimplicialComplexStr of X
for b3 being SimplicialComplex of X holds
( b3 is SubSimplicialComplex of KX iff ( [#] b3 c= [#] KX & the topology of b3 c= the topology of KX ) );

registration
let X be set ;
let KX be SimplicialComplexStr of X;
existence
ex b1 being SubSimplicialComplex of KX st
( b1 is empty & b1 is void & b1 is strict )
proof end;
end;

registration
let X be set ;
let KX be void SimplicialComplexStr of X;
cluster -> void for SubSimplicialComplex of KX;
coherence
for b1 being SubSimplicialComplex of KX holds b1 is void
proof end;
end;

registration
let D be non empty set ;
let KD be non void subset-closed SimplicialComplexStr of D;
existence
not for b1 being SubSimplicialComplex of KD holds b1 is void
proof end;
end;

registration
let X be set ;
let KX be finite-vertices SimplicialComplexStr of X;
coherence
for b1 being SubSimplicialComplex of KX holds b1 is finite-vertices
proof end;
end;

registration
let X be set ;
let KX be finite-degree SimplicialComplexStr of X;
cluster -> finite-degree for SubSimplicialComplex of KX;
coherence
for b1 being SubSimplicialComplex of KX holds b1 is finite-degree
proof end;
end;

theorem Th27: :: SIMPLEX0:27
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX holds S1 is SubSimplicialComplex of KX
proof end;

theorem Th28: :: SIMPLEX0:28
for X being set
for KX being SimplicialComplexStr of X
for A being Subset of KX
for S being 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 end;

theorem :: SIMPLEX0:29
for X being set
for KX being subset-closed SimplicialComplexStr of X
for A being Subset of KX
for S being finite-membered Subset-Family of A st S c= the topology of KX holds
Complex_of S is strict SubSimplicialComplex of KX
proof end;

theorem :: SIMPLEX0:30
for X being set
for Y1, Y2 being 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 end;

theorem :: SIMPLEX0:31
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds Vertices SX c= Vertices KX
proof end;

theorem Th32: :: SIMPLEX0:32
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds degree SX <= degree KX
proof end;

definition
let X be set ;
let KX be SimplicialComplexStr of X;
let SX be SubSimplicialComplex of KX;
attr SX is maximal means :Def14: :: SIMPLEX0:def 14
for A being Subset of SX st A in the topology of KX holds
A is simplex-like ;
end;

:: deftheorem Def14 defines maximal SIMPLEX0:def 14 :
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds
( SX is maximal iff for A being Subset of SX st A in the topology of KX holds
A is simplex-like );

theorem Th33: :: SIMPLEX0:33
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX holds
( SX is maximal iff (bool ([#] SX)) /\ the topology of KX c= the topology of SX )
proof end;

registration
let X be set ;
let KX be SimplicialComplexStr of X;
existence
ex b1 being SubSimplicialComplex of KX st
( b1 is maximal & b1 is strict )
proof end;
end;

theorem Th34: :: SIMPLEX0:34
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX st SX is maximal & S1 is maximal holds
S1 is maximal SubSimplicialComplex of KX
proof end;

theorem :: SIMPLEX0:35
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for S1 being SubSimplicialComplex of SX st S1 is maximal SubSimplicialComplex of KX holds
S1 is maximal
proof end;

theorem Th36: :: SIMPLEX0:36
for X being set
for KX being SimplicialComplexStr of X
for K1, K2 being maximal SubSimplicialComplex of KX st [#] K1 = [#] K2 holds
TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #)
proof end;

definition
let X be set ;
let KX be subset-closed SimplicialComplexStr of X;
let A be Subset of KX;
assume A1: (bool A) /\ the topology of KX is finite-membered ;
func KX | A -> strict maximal SubSimplicialComplex of KX means :Def15: :: SIMPLEX0:def 15
[#] it = A;
existence
ex b1 being strict maximal SubSimplicialComplex of KX st [#] b1 = A
proof end;
uniqueness
for b1, b2 being strict maximal SubSimplicialComplex of KX st [#] b1 = A & [#] b2 = A holds
b1 = b2
by Th36;
end;

:: deftheorem Def15 defines | SIMPLEX0:def 15 :
for X being set
for KX being subset-closed SimplicialComplexStr of X
for A being Subset of KX st (bool A) /\ the topology of KX is finite-membered holds
for b4 being strict maximal SubSimplicialComplex of KX holds
( b4 = KX | A iff [#] b4 = A );

definition
let X be set ;
let SC be SimplicialComplex of X;
let A be Subset of SC;
redefine func SC | A means :Def16: :: SIMPLEX0:def 16
[#] it = A;
compatibility
for b1 being strict maximal SubSimplicialComplex of SC holds
( b1 = SC | A iff [#] b1 = A )
proof end;
end;

:: deftheorem Def16 defines | SIMPLEX0:def 16 :
for X being set
for SC being SimplicialComplex of X
for A being Subset of SC
for b4 being strict maximal SubSimplicialComplex of SC holds
( b4 = SC | A iff [#] b4 = A );

theorem Th37: :: SIMPLEX0:37
for X being set
for SC being SimplicialComplex of X
for A being Subset of SC holds the topology of (SC | A) = (bool A) /\ the topology of SC
proof end;

theorem :: SIMPLEX0:38
for X being set
for SC being SimplicialComplex of X
for A, B being Subset of SC
for B1 being Subset of (SC | A) st B1 = B holds
(SC | A) | B1 = SC | B
proof end;

theorem :: SIMPLEX0:39
for X being set
for SC being SimplicialComplex of X holds SC | ([#] SC) = TopStruct(# the carrier of SC, the topology of SC #)
proof end;

theorem :: SIMPLEX0:40
for X being set
for SC being SimplicialComplex of X
for A, B being Subset of SC st A c= B holds
SC | A is SubSimplicialComplex of SC | B
proof end;

definition
let X be set ;
let KX be SimplicialComplexStr of X;
let i be dim-like number ;
func Skeleton_of (KX,i) -> SimplicialComplexStr of X equals :: SIMPLEX0:def 17
Complex_of (the_subsets_with_limited_card ((Segm (i + 1)), the topology of KX));
coherence
Complex_of (the_subsets_with_limited_card ((Segm (i + 1)), the topology of KX)) is SimplicialComplexStr of X
proof end;
end;

:: deftheorem defines Skeleton_of SIMPLEX0:def 17 :
for X being set
for KX being SimplicialComplexStr of X
for i being dim-like number holds Skeleton_of (KX,i) = Complex_of (the_subsets_with_limited_card ((Segm (i + 1)), the topology of KX));

definition
let n be natural Number ;
:: original: -
redefine func - n -> integer number ;
coherence by TARSKI:1;
end;

registration
let X be set ;
let KX be SimplicialComplexStr of X;
cluster Skeleton_of (KX,(- 1)) -> empty-membered ;
coherence
Skeleton_of (KX,(- 1)) is empty-membered
proof end;
let i be dim-like number ;
cluster Skeleton_of (KX,i) -> finite-degree ;
coherence
Skeleton_of (KX,i) is finite-degree
proof end;
end;

registration
let X be set ;
let KX be empty-membered SimplicialComplexStr of X;
let i be dim-like number ;
cluster Skeleton_of (KX,i) -> empty-membered ;
coherence
Skeleton_of (KX,i) is empty-membered
proof end;
end;

registration
let D be non empty set ;
let KD be non void subset-closed SimplicialComplexStr of D;
let i be dim-like number ;
cluster Skeleton_of (KD,i) -> non void ;
coherence
not Skeleton_of (KD,i) is void
proof end;
end;

theorem :: SIMPLEX0:41
for X being set
for KX being SimplicialComplexStr of X
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 end;

definition
let X be set ;
let KX be subset-closed SimplicialComplexStr of X;
let i be dim-like number ;
:: original: Skeleton_of
redefine func Skeleton_of (KX,i) -> SubSimplicialComplex of KX;
coherence
Skeleton_of (KX,i) is SubSimplicialComplex of KX
proof end;
end;

theorem :: SIMPLEX0:42
for X being set
for KX being SimplicialComplexStr of X
for i being dim-like number st KX is subset-closed & Skeleton_of (KX,i) is empty-membered & not KX is empty-membered holds
i = - 1
proof end;

theorem :: SIMPLEX0:43
for X being set
for KX being SimplicialComplexStr of X
for i being dim-like number holds degree (Skeleton_of (KX,i)) <= degree KX
proof end;

theorem :: SIMPLEX0:44
for X being set
for KX being SimplicialComplexStr of X
for i being dim-like number st - 1 <= i holds
degree (Skeleton_of (KX,i)) <= i
proof end;

theorem :: SIMPLEX0:45
for X being set
for KX being SimplicialComplexStr of X
for i being dim-like number st - 1 <= i & Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #) holds
degree KX <= i
proof end;

theorem :: SIMPLEX0:46
for X being set
for KX being SimplicialComplexStr of X
for i being dim-like number st KX is subset-closed & degree KX <= i holds
Skeleton_of (KX,i) = TopStruct(# the carrier of KX, the topology of KX #)
proof end;

Lm7: for i being Integer
for K being non void subset-closed SimplicialComplexStr st - 1 <= i & i <= degree K holds
ex S being Simplex of K st card S = i + 1

proof end;

definition
let K be non void subset-closed SimplicialComplexStr;
let i be Real;
assume A1: i is integer ;
mode Simplex of i,K -> finite Simplex of K means :Def18: :: SIMPLEX0:def 18
card it = i + 1 if ( - 1 <= i & i <= degree K )
otherwise it is empty ;
existence
( ( - 1 <= i & i <= degree K implies ex b1 being finite Simplex of K st card b1 = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b1 being finite Simplex of K st b1 is empty ) )
proof end;
correctness
consistency
for b1 being finite Simplex of K holds verum
;
;
end;

:: deftheorem Def18 defines Simplex SIMPLEX0:def 18 :
for K being non void subset-closed SimplicialComplexStr
for i being Real st i is integer holds
for b3 being finite Simplex of K holds
( ( - 1 <= i & i <= degree K implies ( b3 is Simplex of i,K iff card b3 = i + 1 ) ) & ( ( not - 1 <= i or not i <= degree K ) implies ( b3 is Simplex of i,K iff b3 is empty ) ) );

registration
let K be non void subset-closed SimplicialComplexStr;
cluster -> empty for Simplex of - 1,K;
coherence
for b1 being Simplex of - 1,K holds b1 is empty
proof end;
end;

theorem :: SIMPLEX0:47
for i being Integer
for K being non void subset-closed SimplicialComplexStr
for S being Simplex of i,K st not S is empty holds
i is natural
proof end;

theorem :: SIMPLEX0:48
for K being non void subset-closed SimplicialComplexStr
for S being finite Simplex of K holds S is Simplex of (card S) - 1,K
proof end;

theorem :: SIMPLEX0:49
for D being non empty set
for K being non void subset-closed SimplicialComplexStr of D
for S being non void SubSimplicialComplex of K
for i being Integer
for A being Simplex of i,S st ( not A is empty or i <= degree S or degree S = degree K ) holds
A is Simplex of i,K
proof end;

definition
let K be non void subset-closed SimplicialComplexStr;
let i be Real;
assume 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: :: SIMPLEX0:def 19
it c= S;
existence
ex b1 being Simplex of max ((i - 1),(- 1)),K st b1 c= S
proof end;
end;

:: deftheorem Def19 defines Face SIMPLEX0:def 19 :
for K being non void subset-closed SimplicialComplexStr
for i being Real st i is integer & i <= degree K holds
for S being Simplex of i,K
for b4 being Simplex of max ((i - 1),(- 1)),K holds
( b4 is Face of S iff b4 c= S );

theorem :: SIMPLEX0:50
for X being set
for n being Nat
for K being non void subset-closed SimplicialComplexStr
for S being Simplex of n,K st n <= degree K holds
( X is Face of S iff ex x being set st
( x in S & S \ {x} = X ) )
proof end;

definition
let X be set ;
let KX be SimplicialComplexStr of X;
let P be Function;
func subdivision (P,KX) -> strict SimplicialComplexStr of X means :Def20: :: SIMPLEX0:def 20
( [#] it = [#] KX & ( for A being Subset of it holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) );
existence
ex b1 being strict SimplicialComplexStr of X st
( [#] b1 = [#] KX & ( for A being Subset of b1 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) )
proof end;
uniqueness
for b1, b2 being strict SimplicialComplexStr of X st [#] b1 = [#] KX & ( for A being Subset of b1 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) & [#] b2 = [#] KX & ( for A being Subset of b2 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines subdivision SIMPLEX0:def 20 :
for X being set
for KX being SimplicialComplexStr of X
for P being Function
for b4 being strict SimplicialComplexStr of X holds
( b4 = subdivision (P,KX) iff ( [#] b4 = [#] KX & ( for A being Subset of b4 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) ) );

registration
let X be set ;
let KX be SimplicialComplexStr of X;
let P be Function;
coherence
( not subdivision (P,KX) is with_non-empty_elements & subdivision (P,KX) is subset-closed & subdivision (P,KX) is finite-membered )
proof end;
end;

registration
let X be set ;
let KX be void SimplicialComplexStr of X;
let P be Function;
coherence
subdivision (P,KX) is empty-membered
proof end;
end;

theorem Th51: :: SIMPLEX0:51
for X being set
for KX being SimplicialComplexStr of X
for P being Function holds degree (subdivision (P,KX)) <= (degree KX) + 1
proof end;

theorem Th52: :: SIMPLEX0:52
for X being set
for KX being SimplicialComplexStr of X
for P being Function st dom P is with_non-empty_elements holds
degree (subdivision (P,KX)) <= degree KX
proof end;

registration
let X be set ;
let KX be finite-degree SimplicialComplexStr of X;
let P be Function;
coherence
subdivision (P,KX) is finite-degree
proof end;
end;

registration
let X be set ;
let KX be finite-vertices SimplicialComplexStr of X;
let P be Function;
coherence
subdivision (P,KX) is finite-vertices
proof end;
end;

theorem :: SIMPLEX0:53
for X being set
for KX being subset-closed SimplicialComplexStr of X
for P being Function st dom P is with_non-empty_elements & ( for n being Nat st n <= degree KX holds
ex S being 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 end;

theorem Th54: :: SIMPLEX0:54
for X, Y, Z being set
for KX being SimplicialComplexStr of X
for P being Function st Y c= Z holds
subdivision ((P | Y),KX) is SubSimplicialComplex of subdivision ((P | Z),KX)
proof end;

theorem :: SIMPLEX0:55
for X, Y being set
for KX being SimplicialComplexStr of X
for P being Function st (dom P) /\ the topology of KX c= Y holds
subdivision ((P | Y),KX) = subdivision (P,KX)
proof end;

theorem Th56: :: SIMPLEX0:56
for X, Y, Z being set
for KX being SimplicialComplexStr of X
for P being Function st Y c= Z holds
subdivision ((Y | P),KX) is SubSimplicialComplex of subdivision ((Z | P),KX)
proof end;

theorem :: SIMPLEX0:57
for X, Y being set
for KX being SimplicialComplexStr of X
for P being Function st P .: the topology of KX c= Y holds
subdivision ((Y |` P),KX) = subdivision (P,KX)
proof end;

theorem Th58: :: SIMPLEX0:58
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function holds subdivision (P,SX) is SubSimplicialComplex of subdivision (P,KX)
proof end;

theorem :: SIMPLEX0:59
for X being set
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function
for A being Subset of (subdivision (P,KX)) st dom P c= the topology of SX & A = [#] SX holds
subdivision (P,SX) = (subdivision (P,KX)) | A
proof end;

theorem Th60: :: SIMPLEX0:60
for X being set
for P being Function
for K1, K2 being SimplicialComplexStr of X st TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) holds
subdivision (P,K1) = subdivision (P,K2)
proof end;

definition
let X be set ;
let KX be SimplicialComplexStr of X;
let P be Function;
let n be Nat;
func subdivision (n,P,KX) -> SimplicialComplexStr of X means :Def21: :: SIMPLEX0:def 21
ex F being Function st
( F . 0 = KX & F . n = it & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) );
existence
ex b1 being SimplicialComplexStr of X ex F being Function st
( F . 0 = KX & F . n = b1 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) )
proof end;
uniqueness
for b1, b2 being SimplicialComplexStr of X st ex F being Function st
( F . 0 = KX & F . n = b1 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) & ex F being Function st
( F . 0 = KX & F . n = b2 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines subdivision SIMPLEX0:def 21 :
for X being set
for KX being SimplicialComplexStr of X
for P being Function
for n being Nat
for b5 being SimplicialComplexStr of X holds
( b5 = subdivision (n,P,KX) iff ex F being Function st
( F . 0 = KX & F . n = b5 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) );

theorem Th61: :: SIMPLEX0:61
for X being set
for KX being SimplicialComplexStr of X
for P being Function holds subdivision (0,P,KX) = KX
proof end;

theorem Th62: :: SIMPLEX0:62
for X being set
for KX being SimplicialComplexStr of X
for P being Function holds subdivision (1,P,KX) = subdivision (P,KX)
proof end;

theorem Th63: :: SIMPLEX0:63
for X being set
for KX being SimplicialComplexStr of X
for P being Function
for n, k being Element of NAT holds subdivision ((n + k),P,KX) = subdivision (n,P,(subdivision (k,P,KX)))
proof end;

theorem :: SIMPLEX0:64
for X being set
for n being Nat
for KX being SimplicialComplexStr of X
for P being Function holds [#] (subdivision (n,P,KX)) = [#] KX
proof end;

theorem :: SIMPLEX0:65
for X being set
for n being Nat
for KX being SimplicialComplexStr of X
for SX being SubSimplicialComplex of KX
for P being Function holds subdivision (n,P,SX) is SubSimplicialComplex of subdivision (n,P,KX)
proof end;