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

notation

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

end;

registration

cluster empty -> subset-closed for set ;

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

cluster with_empty_element -> non empty for set ;

coherence
for b₁ being set st b₁ is with_empty_element holds
not b₁ is empty ;

cluster non empty subset-closed -> with_empty_element for 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 by COHSP_1:def 3;

end;

registration

let X be subset-closed set ;

cluster Sub_of_Fin X -> subset-closed ;

coherence
Sub_of_Fin X is subset-closed ;

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₂ ;

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 -> finite-membered subset-closed ;

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

registration

let D be non empty set ;

cluster with_non-empty_element finite finite-membered subset-closed for Element of bool (bool D);

existence
ex b₁ being Subset-Family of D st
( b₁ is finite & b₁ is with_non-empty_element & b₁ is subset-closed & b₁ is finite-membered )

proof end;

end;

registration

let Y, X be set ;
let n be finite Cardinal;

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 Cardinal;

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 Cardinal;

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 Cardinal;

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 X is with_non-empty_elements 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
( 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

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 for 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 :: 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 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 :: 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

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

cluster with_empty_element -> non void for TopStruct ;

coherence
for b₁ being SimplicialComplexStr st b₁ is with_empty_element holds
not b₁ is void by PENCIL_1:def 4;

cluster with_non-empty_element -> non void for TopStruct ;

coherence
for b₁ being SimplicialComplexStr st b₁ is with_non-empty_element holds
not b₁ is void by PENCIL_1:def 4;

cluster non void empty-membered -> with_empty_element for TopStruct ;

coherence
for b₁ being SimplicialComplexStr st not b₁ is void & b₁ is empty-membered holds
b₁ is with_empty_element ;

cluster non void subset-closed -> with_empty_element for TopStruct ;

coherence
for b₁ being SimplicialComplexStr st not b₁ is void & b₁ is subset-closed holds
b₁ is with_empty_element ;

cluster empty-membered -> subset-closed finite-vertices for 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 for 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 for 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 for 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 for 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 for SimplicialComplexStr of D;

existence
ex b₁ being SimplicialComplexStr of D st
( not b₁ is empty & b₁ is total & b₁ is with_empty_element & b₁ is with_non-empty_element & 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 for TopStruct ;

existence
ex b₁ being SimplicialComplexStr st
( not b₁ is empty & b₁ is with_empty_element & b₁ is with_non-empty_element & 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 for 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 for 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;

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 ) ;

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 ;

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 ;

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 by Th7;

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 for 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 for 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 for Element of bool the carrier of K;

existence
ex b₁ being Simplex of K st b₁ 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 b₁ being ExtReal 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 ExtReal st b₁ = - 1 ) & ( ( K is void or not K is finite-degree ) & not K is void implies ex b₁ being ExtReal st b₁ = +infty ) )

proof end;

uniqueness
for b₁, b₂ 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 <= 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 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 <= 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 ExtReal 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 -> 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;

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 for 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 for 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 for 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 for 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 for 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 for 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;

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
- n is integer number 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 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 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 for 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;
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 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;

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 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;

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 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 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;