:: Abstract Simplicial Complexes
:: by Karol P\c{a}k
::
:: Received December 18, 2009
:: Copyright (c) 2009-2011 Association of Mizar Users

begin

notation

let X be set ;
antonym with_empty_element X for with_non-empty_elements ;

end;

registration

cluster empty -> finite-membered set ;
coherence
for b₁ being set st b₁ is empty holds
b₁ is finite-membered

proof end;

let X be finite set ;
cluster {X} -> finite-membered ;
coherence
{X} is finite-membered

proof end;

cluster bool X -> finite-membered ;
coherence
bool X is finite-membered

proof end;

let Y be finite set ;
cluster {X,Y} -> finite-membered ;
coherence
{X,Y} is finite-membered

proof end;

end;

registration

let X be finite-membered set ;
cluster -> finite-membered Element of bool X;
coherence
for b₁ being Subset of X holds b₁ is finite-membered

proof end;

let Y be finite-membered set ;
cluster X \/ Y -> finite-membered ;
coherence
X \/ Y is finite-membered

proof end;

end;

registration

let X be finite finite-membered set ;
cluster union X -> finite ;
coherence
union X is finite

proof end;

end;

registration

cluster empty -> subset-closed set ;
coherence
for b₁ being set st b₁ is empty holds
b₁ is subset-closed

proof end;

cluster with_empty_element -> non empty set ;
coherence
for b₁ being set st b₁ is with_empty_element holds
not b₁ is empty by SETFAM_1:def 9;
cluster non empty subset-closed -> with_empty_element set ;
coherence
for b₁ being set st not b₁ is empty & b₁ is subset-closed holds
b₁ is with_empty_element

proof end;

end;

registration

let X be set ;
cluster Sub_of_Fin X -> finite-membered ;
coherence
Sub_of_Fin X is finite-membered

proof end;

end;

registration

let X be subset-closed set ;
cluster Sub_of_Fin X -> subset-closed ;
coherence
Sub_of_Fin X is subset-closed

proof end;

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 ;
cluster A \/ B -> subset-closed ;
coherence
A \/ B is subset-closed

proof end;

cluster A /\ B -> subset-closed ;
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 b₁ being subset-closed set st
( X c= b₁ & ( for Y being set st X c= Y & Y is subset-closed holds
b₁ c= Y ) )

proof end;

uniqueness
for b₁, b₂ being subset-closed set st X c= b₁ & ( for Y being set st X c= Y & Y is subset-closed holds
b₁ c= Y ) & X c= b₂ & ( for Y being set st X c= Y & Y is subset-closed holds
b₂ c= Y ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines subset-closed_closure_of SIMPLEX0:def 1 :
for X being set
for b₂ being subset-closed set holds
( b₂ = subset-closed_closure_of X iff ( X c= b₂ & ( for Y being set st X c= Y & Y is subset-closed holds
b₂ 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
subset-closed_closure_of F is subset-closed Subset-Family of X

proof end;

end;

registration

cluster subset-closed_closure_of {} -> empty subset-closed ;
coherence
subset-closed_closure_of {} is empty

proof end;

let X be non empty set ;
cluster subset-closed_closure_of X -> non empty subset-closed ;
coherence
not subset-closed_closure_of X is empty

proof end;

end;

registration

let X be with_non-empty_element set ;
cluster subset-closed_closure_of X -> with_non-empty_element subset-closed ;
coherence
not subset-closed_closure_of X is empty-membered

proof end;

end;

registration

let X be finite-membered set ;
cluster subset-closed_closure_of X -> subset-closed finite-membered ;
coherence
subset-closed_closure_of X is finite-membered

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) = (subset-closed_closure_of X) \/ (subset-closed_closure_of 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

proof end;

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= card n ) );
existence
ex b₁ being Subset-Family of Y st
for A being Subset of Y holds
( A in b₁ iff ( A in X & card A c= card n ) )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of Y st ( for A being Subset of Y holds
( A in b₁ iff ( A in X & card A c= card n ) ) ) & ( for A being Subset of Y holds
( A in b₂ iff ( A in X & card A c= card n ) ) ) holds
b₁ = b₂

proof end;

end;

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

registration

let D be non empty set ;
cluster with_non-empty_element finite subset-closed finite-membered Element of bool (bool D);
existence
ex b₁ being Subset-Family of D st
( b₁ is finite & not b₁ is empty-membered & b₁ is subset-closed & b₁ is finite-membered )

proof end;

end;

registration

let Y, X be set ;
let n be finite set ;
cluster the_subsets_with_limited_card (n,X,Y) -> finite-membered ;
coherence
the_subsets_with_limited_card (n,X,Y) is finite-membered

proof end;

end;

registration

let Y be set ;
let X be subset-closed set ;
let n be set ;
cluster the_subsets_with_limited_card (n,X,Y) -> subset-closed ;
coherence
the_subsets_with_limited_card (n,X,Y) is subset-closed

proof end;

end;

registration

let Y be set ;
let X be with_empty_element set ;
let n be set ;
cluster the_subsets_with_limited_card (n,X,Y) -> with_empty_element ;
coherence
the_subsets_with_limited_card (n,X,Y) is with_empty_element

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 set ;
cluster the_subsets_with_limited_card (n,X,D) -> with_non-empty_element ;
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 not X is with_empty_element holds
card X c= card (union X)

proof end;

theorem :: SIMPLEX0:11

for X, x being set st X is c=-linear holds
X \/ {((union 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
( not Y is with_empty_element & 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 & not Y is with_empty_element & Y is c=-linear & X in Y holds
ex Y1 being Subset-Family of X st
( Y c= Y1 & not Y1 is with_empty_element & 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;

begin

definition

mode SimplicialComplexStr is TopStruct ;

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 Element of bool (bool the carrier of K);
existence
ex b₁ being Subset-Family of K st
( b₁ is empty & b₁ 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 :Def3: :: SIMPLEX0:def 3
ex S being Subset of K st
( S is simplex-like & v in S );

end;

:: deftheorem Def3 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 b₁ being Subset of K st
for v being Element of K holds
( v in b₁ iff v is vertex-like )

proof end;

uniqueness
for b₁, b₂ being Subset of K st ( for v being Element of K holds
( v in b₁ iff v is vertex-like ) ) & ( for v being Element of K holds
( v in b₂ iff v is vertex-like ) ) holds
b₁ = b₂

proof end;

end;

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

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: :: 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 :Def6: :: 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 Def6 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
not the topology of K is with_empty_element ;

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 not the topology of K is with_empty_element );

notation

let K be SimplicialComplexStr;
antonym with_non-empty_element K for empty-membered ;
antonym with_empty_element K for with_non-empty_elements ;

end;

definition

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

proof end;

end;

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

definition

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

end;

:: deftheorem Def10 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

proof end;

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

cluster with_empty_element -> non void TopStruct ;
coherence
for b₁ being SimplicialComplexStr st not b₁ is with_non-empty_elements holds
not b₁ is void

proof end;

cluster with_non-empty_element -> non void TopStruct ;
coherence
for b₁ being SimplicialComplexStr st not b₁ is empty-membered holds
not b₁ is void

proof end;

cluster non void empty-membered -> with_empty_element TopStruct ;
coherence
for b₁ being SimplicialComplexStr st not b₁ is void & b₁ is empty-membered holds
not b₁ is with_non-empty_elements

proof end;

cluster non void subset-closed -> with_empty_element TopStruct ;
coherence
for b₁ being SimplicialComplexStr st not b₁ is void & b₁ is subset-closed holds
not b₁ is with_non-empty_elements

proof end;

cluster empty-membered -> subset-closed finite-vertices TopStruct ;
coherence
for b₁ being SimplicialComplexStr st b₁ is empty-membered holds
( b₁ is subset-closed & b₁ is finite-vertices )

proof end;

cluster finite-vertices -> finite-degree locally-finite TopStruct ;
coherence
for b₁ being SimplicialComplexStr st b₁ is finite-vertices holds
( b₁ is locally-finite & b₁ is finite-degree )

proof end;

cluster subset-closed locally-finite -> finite-membered TopStruct ;
coherence
for b₁ being SimplicialComplexStr st b₁ is locally-finite & b₁ is subset-closed holds
b₁ is finite-membered

proof end;

end;

registration

let X be set ;
cluster empty strict void empty-membered SimplicialComplexStr of X;
existence
ex b₁ being SimplicialComplexStr of X st
( b₁ is empty & b₁ is void & b₁ is empty-membered & b₁ is strict )

proof end;

end;

registration

let D be non empty set ;
cluster non empty strict non void empty-membered total SimplicialComplexStr of D;
existence
ex b₁ being SimplicialComplexStr of D st
( not b₁ is empty & not b₁ is void & b₁ is total & b₁ is empty-membered & b₁ is strict )

proof end;

cluster non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element total SimplicialComplexStr of D;
existence
ex b₁ being SimplicialComplexStr of D st
( not b₁ is empty & b₁ is total & not b₁ is with_non-empty_elements & not b₁ is empty-membered & b₁ is finite-vertices & b₁ is subset-closed & b₁ is strict )

proof end;

end;

registration

cluster non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element TopStruct ;
existence
ex b₁ being SimplicialComplexStr st
( not b₁ is empty & not b₁ is with_non-empty_elements & not b₁ is empty-membered & b₁ is finite-vertices & b₁ is subset-closed & b₁ 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 Element of bool (bool the carrier of K);
coherence
for b₁ being Subset-Family of K st b₁ is simplex-like holds
b₁ is finite

proof end;

end;

registration

let K be finite-membered SimplicialComplexStr;
cluster simplex-like -> finite-membered Element of bool (bool the carrier of K);
coherence
for b₁ being Subset-Family of K st b₁ is simplex-like holds
b₁ 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;

begin

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,(subset-closed_closure_of Y) #);
coherence
TopStruct(# X,(subset-closed_closure_of Y) #) 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,(subset-closed_closure_of Y) #);

registration

let X be set ;
let Y be Subset-Family of X;
cluster Complex_of Y -> strict subset-closed total ;
coherence
( Complex_of Y is total & Complex_of Y is subset-closed )

proof end;

end;

registration

let X be set ;
let Y be non empty Subset-Family of X;
cluster Complex_of Y -> strict with_empty_element ;
coherence
not Complex_of Y is with_non-empty_elements by Def8;

end;

registration

let X be set ;
let Y be finite-membered Subset-Family of X;
cluster Complex_of Y -> strict finite-membered ;
coherence
Complex_of Y is finite-membered

proof end;

end;

registration

let X be set ;
let Y be finite finite-membered Subset-Family of X;
cluster Complex_of Y -> strict finite-vertices ;
coherence
Complex_of Y is finite-vertices

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

proof end;

definition

let X be set ;
mode SimplicialComplex of X is subset-closed finite-membered 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 Element of bool the carrier of K;
coherence
for b₁ being Subset of K st b₁ is empty holds
b₁ is simplex-like

proof end;

cluster empty simplex-like Element of bool the carrier of K;
existence
ex b₁ being Simplex of K st b₁ is empty

proof end;

end;

registration

let K be non void finite-membered SimplicialComplexStr;
cluster finite simplex-like Element of bool the carrier of K;
existence
ex b₁ being Simplex of K st b₁ is finite

proof end;

end;

begin

definition

let K be SimplicialComplexStr;
func degree K -> ext-real number 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 b₁ being ext-real number st
( ( for S being finite Subset of K st S is simplex-like holds
card S <= b₁ + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b₁ + 1 ) ) ) & ( K is void implies ex b₁ being ext-real number st b₁ = - 1 ) & ( ( K is void or not K is finite-degree ) & not K is void implies ex b₁ being ext-real number st b₁ = +infty ) )

proof end;

uniqueness
for b₁, b₂ being ext-real number holds
( ( not K is void & K is finite-degree & ( for S being finite Subset of K st S is simplex-like holds
card S <= b₁ + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b₁ + 1 ) & ( for S being finite Subset of K st S is simplex-like holds
card S <= b₂ + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b₂ + 1 ) implies b₁ = b₂ ) & ( K is void & b₁ = - 1 & b₂ = - 1 implies b₁ = b₂ ) & ( ( K is void or not K is finite-degree ) & not K is void & b₁ = +infty & b₂ = +infty implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being ext-real number 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 <= b₁ + 1 ) & ex S being Subset of K st
( S is simplex-like & card S = b₁ + 1 ) ) iff b₁ = - 1 ) ;

end;

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

registration

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

proof end;

cluster degree K -> ext-real integer ;
coherence
degree K is integer

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 <= (degree K) + 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 (Complex_of {A}) = (card A) - 1

proof end;

begin

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 b₁ being SimplicialComplex of X st
( [#] b₁ c= [#] KX & the topology of b₁ 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 b₃ being SimplicialComplex of X holds
( b₃ is SubSimplicialComplex of KX iff ( [#] b₃ c= [#] KX & the topology of b₃ c= the topology of KX ) );

registration

let X be set ;
let KX be SimplicialComplexStr of X;
cluster empty strict void subset-closed finite-membered SubSimplicialComplex of KX;
existence
ex b₁ being SubSimplicialComplex of KX st
( b₁ is empty & b₁ is void & b₁ is strict )

proof end;

end;

registration

let X be set ;
let KX be void SimplicialComplexStr of X;
cluster -> void SubSimplicialComplex of KX;
coherence
for b₁ being SubSimplicialComplex of KX holds b₁ is void

proof end;

end;

registration

let D be non empty set ;
let KD be non void subset-closed SimplicialComplexStr of D;
cluster non void subset-closed finite-membered SubSimplicialComplex of KD;
existence
not for b₁ being SubSimplicialComplex of KD holds b₁ is void

proof end;

end;

registration

let X be set ;
let KX be finite-vertices SimplicialComplexStr of X;
cluster -> finite-vertices SubSimplicialComplex of KX;
coherence
for b₁ being SubSimplicialComplex of KX holds b₁ is finite-vertices

proof end;

end;

registration

let X be set ;
let KX be finite-degree SimplicialComplexStr of X;
cluster -> finite-degree SubSimplicialComplex of KX;
coherence
for b₁ being SubSimplicialComplex of KX holds b₁ 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;
cluster strict subset-closed finite-membered maximal SubSimplicialComplex of KX;
existence
ex b₁ being SubSimplicialComplex of KX st
( b₁ is maximal & b₁ 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 b₁ being strict maximal SubSimplicialComplex of KX st [#] b₁ = A

proof end;

uniqueness
for b₁, b₂ being strict maximal SubSimplicialComplex of KX st [#] b₁ = A & [#] b₂ = A holds
b₁ = b₂ 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 b₄ being strict maximal SubSimplicialComplex of KX holds
( b₄ = KX | A iff [#] b₄ = 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 b₁ being strict maximal SubSimplicialComplex of SC holds
( b₁ = SC | A iff [#] b₁ = 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 b₄ being strict maximal SubSimplicialComplex of SC holds
( b₄ = SC | A iff [#] b₄ = 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;

registration

cluster integer -> finite set ;
coherence
for b₁ being Integer holds b₁ is finite

proof end;

end;

begin

definition

let X be set ;
let KX be SimplicialComplexStr of X;
let i be real number ;
func Skeleton_of (KX,i) -> SimplicialComplexStr of X equals :: SIMPLEX0:def 17
Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX));
coherence
Complex_of (the_subsets_with_limited_card ((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 real number holds Skeleton_of (KX,i) = Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX));

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 Integer;
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 Integer;
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 Integer;
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 i1, i2 being Integer
for KX being SimplicialComplexStr of X 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 Integer;
:: 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 i being Integer
for KX being SimplicialComplexStr of X 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 i being Integer
for KX being SimplicialComplexStr of X holds degree (Skeleton_of (KX,i)) <= degree KX

proof end;

theorem :: SIMPLEX0:44

for X being set
for i being Integer
for KX being SimplicialComplexStr of X st - 1 <= i holds
degree (Skeleton_of (KX,i)) <= i

proof end;

theorem :: SIMPLEX0:45

for X being set
for i being Integer
for KX being SimplicialComplexStr of X 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 i being Integer
for KX being SimplicialComplexStr of X 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 number ;
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 b₁ being finite Simplex of K st card b₁ = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b₁ being finite Simplex of K st b₁ is empty ) )

proof end;

correctness
consistency
for b₁ 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 number st i is integer holds
for b₃ being finite Simplex of K holds
( ( - 1 <= i & i <= degree K implies ( b₃ is Simplex of i,K iff card b₃ = i + 1 ) ) & ( ( not - 1 <= i or not i <= degree K ) implies ( b₃ is Simplex of i,K iff b₃ is empty ) ) );

registration

let K be non void subset-closed SimplicialComplexStr;
cluster -> empty Simplex of - 1,K;
coherence
for b₁ being Simplex of - 1,K holds b₁ 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 number ;
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 b₁ being Simplex of max ((i - 1),(- 1)),K st b₁ c= S

proof end;

end;

:: deftheorem Def19 defines Face SIMPLEX0:def 19 :
for K being non void subset-closed SimplicialComplexStr
for i being real number st i is integer & i <= degree K holds
for S being Simplex of i,K
for b₄ being Simplex of max ((i - 1),(- 1)),K holds
( b₄ is Face of S iff b₄ 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;

begin

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 b₁ being strict SimplicialComplexStr of X st
( [#] b₁ = [#] KX & ( for A being Subset of b₁ 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 b₁, b₂ being strict SimplicialComplexStr of X st [#] b₁ = [#] KX & ( for A being Subset of b₁ holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) & [#] b₂ = [#] KX & ( for A being Subset of b₂ holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) holds
b₁ = b₂

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 b₄ being strict SimplicialComplexStr of X holds
( b₄ = subdivision (P,KX) iff ( [#] b₄ = [#] KX & ( for A being Subset of b₄ 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;
cluster subdivision (P,KX) -> strict subset-closed finite-membered with_empty_element ;
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;
cluster subdivision (P,KX) -> strict empty-membered ;
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 not dom P is with_empty_element 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;
cluster subdivision (P,KX) -> strict finite-degree ;
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;
cluster subdivision (P,KX) -> strict finite-vertices ;
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 not dom P is with_empty_element & ( 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 b₁ being SimplicialComplexStr of X ex F being Function st
( F . 0 = KX & F . n = b₁ & 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 b₁, b₂ being SimplicialComplexStr of X st ex F being Function st
( F . 0 = KX & F . n = b₁ & 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 = b₂ & 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
b₁ = b₂

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 b₅ being SimplicialComplexStr of X holds
( b₅ = subdivision (n,P,KX) iff ex F being Function st
( F . 0 = KX & F . n = b₅ & 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;