:: by Karol P\c{a}k

::

:: Received December 18, 2009

:: Copyright (c) 2009-2012 Association of Mizar Users

begin

registration

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is subset-closed

for b_{1} being set st b_{1} is with_empty_element holds

not b_{1} is empty
by SETFAM_1:def 8;

coherence

for b_{1} being set st not b_{1} is empty & b_{1} is subset-closed holds

b_{1} is with_empty_element

end;
for b

b

proof end;

coherence for b

not b

coherence

for b

b

proof end;

registration

let A, B be subset-closed set ;

coherence

A \/ B is subset-closed

A /\ B is subset-closed

end;
coherence

A \/ B is subset-closed

proof end;

coherence A /\ B is subset-closed

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

ex b_{1} being subset-closed set st

( X c= b_{1} & ( for Y being set st X c= Y & Y is subset-closed holds

b_{1} c= Y ) )

for b_{1}, b_{2} being subset-closed set st X c= b_{1} & ( for Y being set st X c= Y & Y is subset-closed holds

b_{1} c= Y ) & X c= b_{2} & ( for Y being set st X c= Y & Y is subset-closed holds

b_{2} c= Y ) holds

b_{1} = b_{2}

end;
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 ( X c= it & ( for Y being set st X c= Y & Y is subset-closed holds

it c= Y ) );

ex b

( X c= b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines subset-closed_closure_of SIMPLEX0:def 1 :

for X being set

for b_{2} being subset-closed set holds

( b_{2} = subset-closed_closure_of X iff ( X c= b_{2} & ( for Y being set st X c= Y & Y is subset-closed holds

b_{2} c= Y ) ) );

for X being set

for b

( b

b

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

( 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

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

registration

coherence

subset-closed_closure_of {} is empty

coherence

not subset-closed_closure_of X is empty

end;
subset-closed_closure_of {} is empty

proof end;

let X be non empty set ;coherence

not subset-closed_closure_of X is empty

proof end;

registration

let X be with_non-empty_element set ;

coherence

not subset-closed_closure_of X is empty-membered

end;
coherence

not subset-closed_closure_of X is empty-membered

proof end;

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

( X is_finer_than Y iff subset-closed_closure_of X c= subset-closed_closure_of Y )

proof end;

definition

let Y, X, n be set ;

ex b_{1} being Subset-Family of Y st

for A being Subset of Y holds

( A in b_{1} iff ( A in X & card A c= card n ) )

for b_{1}, b_{2} being Subset-Family of Y st ( for A being Subset of Y holds

( A in b_{1} iff ( A in X & card A c= card n ) ) ) & ( for A being Subset of Y holds

( A in b_{2} iff ( A in X & card A c= card n ) ) ) holds

b_{1} = b_{2}

end;
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 for A being Subset of Y holds

( A in it iff ( A in X & card A c= card n ) );

ex b

for A being Subset of Y holds

( A in b

proof end;

uniqueness for b

( A in b

( A in b

b

proof end;

:: deftheorem Def2 defines the_subsets_with_limited_card SIMPLEX0:def 2 :

for Y, X, n being set

for b_{4} being Subset-Family of Y holds

( b_{4} = the_subsets_with_limited_card (n,X,Y) iff for A being Subset of Y holds

( A in b_{4} iff ( A in X & card A c= card n ) ) );

for Y, X, n being set

for b

( b

( A in b

registration

let D be non empty set ;

existence

ex b_{1} being Subset-Family of D st

( b_{1} is finite & b_{1} is with_non-empty_element & b_{1} is subset-closed & b_{1} is finite-membered )

end;
existence

ex b

( b

proof end;

registration

let Y, X be set ;

let n be finite set ;

coherence

the_subsets_with_limited_card (n,X,Y) is finite-membered

end;
let n be finite set ;

coherence

the_subsets_with_limited_card (n,X,Y) is finite-membered

proof end;

registration

let Y be set ;

let X be subset-closed set ;

let n be set ;

coherence

the_subsets_with_limited_card (n,X,Y) is subset-closed

end;
let X be subset-closed set ;

let n be set ;

coherence

the_subsets_with_limited_card (n,X,Y) is subset-closed

proof end;

registration

let Y be set ;

let X be with_empty_element set ;

let n be set ;

coherence

the_subsets_with_limited_card (n,X,Y) is with_empty_element

end;
let X be with_empty_element set ;

let n be set ;

coherence

the_subsets_with_limited_card (n,X,Y) is with_empty_element

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

coherence

not the_subsets_with_limited_card (n,X,D) is empty-membered

end;
let X be with_non-empty_element subset-closed Subset-Family of D;

let n be non empty set ;

coherence

not the_subsets_with_limited_card (n,X,D) is empty-membered

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

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

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

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;

begin

notation
end;

registration

let K be SimplicialComplexStr;

existence

ex b_{1} being Subset-Family of K st

( b_{1} is empty & b_{1} is simplex-like )

end;
existence

ex b

( b

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

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;

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

ex S being Subset of K st

( S is simplex-like & v in S );

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

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;

ex b_{1} being Subset of K st

for v being Element of K holds

( v in b_{1} iff v is vertex-like )

for b_{1}, b_{2} being Subset of K st ( for v being Element of K holds

( v in b_{1} iff v is vertex-like ) ) & ( for v being Element of K holds

( v in b_{2} iff v is vertex-like ) ) holds

b_{1} = b_{2}

end;
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 for v being Element of K holds

( v in it iff v is vertex-like );

ex b

for v being Element of K holds

( v in b

proof end;

uniqueness for b

( v in b

( v in b

b

proof end;

:: deftheorem Def4 defines Vertices SIMPLEX0:def 4 :

for K being SimplicialComplexStr

for b_{2} being Subset of K holds

( b_{2} = Vertices K iff for v being Element of K holds

( v in b_{2} iff v is vertex-like ) );

for K being SimplicialComplexStr

for b

( b

( v in b

:: deftheorem Def5 defines finite-vertices SIMPLEX0:def 5 :

for K being SimplicialComplexStr holds

( K is finite-vertices iff Vertices K is finite );

for K being SimplicialComplexStr holds

( K is finite-vertices iff Vertices K is finite );

definition

let K be SimplicialComplexStr;

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

for v being Vertex of K holds { S where S is Subset of K : ( S is simplex-like & v in S ) } is finite ;

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

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;

end;
attr K is with_non-empty_elements means :Def8: :: SIMPLEX0:def 8

the topology of K is with_non-empty_elements ;

the topology of K is with_non-empty_elements ;

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

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

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;
antonym with_non-empty_element K for empty-membered ;

antonym with_empty_element K for with_non-empty_elements ;

definition
end;

:: deftheorem Def9 defines SimplicialComplexStr SIMPLEX0:def 9 :

for X being set

for b_{2} being SimplicialComplexStr holds

( b_{2} is SimplicialComplexStr of X iff [#] b_{2} c= X );

for X being set

for b

( b

:: deftheorem Def10 defines total SIMPLEX0:def 10 :

for X being set

for KX being SimplicialComplexStr of X holds

( KX is total iff [#] KX = X );

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

coherence

for b_{1} being SimplicialComplexStr st b_{1} is with_empty_element holds

not b_{1} is void

for b_{1} being SimplicialComplexStr st b_{1} is with_non-empty_element holds

not b_{1} is void

for b_{1} being SimplicialComplexStr st not b_{1} is void & b_{1} is empty-membered holds

b_{1} is with_empty_element

for b_{1} being SimplicialComplexStr st not b_{1} is void & b_{1} is subset-closed holds

b_{1} is with_empty_element

for b_{1} being SimplicialComplexStr st b_{1} is empty-membered holds

( b_{1} is subset-closed & b_{1} is finite-vertices )

for b_{1} being SimplicialComplexStr st b_{1} is finite-vertices holds

( b_{1} is locally-finite & b_{1} is finite-degree )

for b_{1} being SimplicialComplexStr st b_{1} is locally-finite & b_{1} is subset-closed holds

b_{1} is finite-membered

end;
for b

not b

proof end;

coherence for b

not b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

( b

proof end;

coherence for b

( b

proof end;

coherence for b

b

proof end;

registration

let X be set ;

existence

ex b_{1} being SimplicialComplexStr of X st

( b_{1} is empty & b_{1} is void & b_{1} is empty-membered & b_{1} is strict )

end;
existence

ex b

( b

proof end;

registration

let D be non empty set ;

existence

ex b_{1} being SimplicialComplexStr of D st

( not b_{1} is empty & not b_{1} is void & b_{1} is total & b_{1} is empty-membered & b_{1} is strict )

ex b_{1} being SimplicialComplexStr of D st

( not b_{1} is empty & b_{1} is total & b_{1} is with_empty_element & b_{1} is with_non-empty_element & b_{1} is finite-vertices & b_{1} is subset-closed & b_{1} is strict )

end;
existence

ex b

( not b

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

( not b

proof end;

registration

ex b_{1} being SimplicialComplexStr st

( not b_{1} is empty & b_{1} is with_empty_element & b_{1} is with_non-empty_element & b_{1} is finite-vertices & b_{1} is subset-closed & b_{1} is strict )
end;

cluster non empty strict subset-closed finite-vertices with_non-empty_element with_empty_element for TopStruct ;

existence ex b

( not b

proof end;

registration
end;

registration

let K be finite-vertices SimplicialComplexStr;

coherence

for b_{1} being Subset-Family of K st b_{1} is simplex-like holds

b_{1} is finite

end;
coherence

for b

b

proof end;

registration

let K be finite-membered SimplicialComplexStr;

coherence

for b_{1} being Subset-Family of K st b_{1} is simplex-like holds

b_{1} is finite-membered

end;
coherence

for b

b

proof end;

theorem :: SIMPLEX0:15

theorem :: SIMPLEX0:16

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;

for S being Subset of K st S is simplex-like holds

S c= Vertices K by Lm4;

theorem :: SIMPLEX0:18

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

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

K is finite-vertices

proof end;

begin

definition

let X be set ;

let Y be Subset-Family of X;

TopStruct(# X,(subset-closed_closure_of Y) #) is strict SimplicialComplexStr of X

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

TopStruct(# X,(subset-closed_closure_of Y) #) is strict SimplicialComplexStr of X

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

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;

coherence

( Complex_of Y is total & Complex_of Y is subset-closed )

end;
let Y be Subset-Family of X;

coherence

( Complex_of Y is total & Complex_of Y is subset-closed )

proof end;

registration

let X be set ;

let Y be non empty Subset-Family of X;

coherence

not Complex_of Y is with_non-empty_elements by Def8;

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

coherence

not Complex_of Y is with_non-empty_elements by Def8;

registration

let X be set ;

let Y be finite-membered Subset-Family of X;

coherence

Complex_of Y is finite-membered

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

coherence

Complex_of Y is finite-membered

proof end;

registration

let X be set ;

let Y be finite finite-membered Subset-Family of X;

coherence

Complex_of Y is finite-vertices

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

coherence

Complex_of Y is finite-vertices

proof 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

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;
mode SimplicialComplex of X is subset-closed finite-membered SimplicialComplexStr of X;

definition
end;

registration

let K be with_empty_element SimplicialComplexStr;

coherence

for b_{1} being Subset of K st b_{1} is empty holds

b_{1} is simplex-like

ex b_{1} being Simplex of K st b_{1} is empty

end;
coherence

for b

b

proof end;

existence ex b

proof end;

registration

let K be non void finite-membered SimplicialComplexStr;

existence

ex b_{1} being Simplex of K st b_{1} is finite

end;
existence

ex b

proof end;

begin

definition

let K be SimplicialComplexStr;

( ( not K is void & K is finite-degree implies ex b_{1} being ext-real number st

( ( for S being finite Subset of K st S is simplex-like holds

card S <= b_{1} + 1 ) & ex S being Subset of K st

( S is simplex-like & card S = b_{1} + 1 ) ) ) & ( K is void implies ex b_{1} being ext-real number st b_{1} = - 1 ) & ( ( K is void or not K is finite-degree ) & not K is void implies ex b_{1} being ext-real number st b_{1} = +infty ) )

for b_{1}, b_{2} 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} + 1 ) & ex S being Subset of K st

( S is simplex-like & card S = b_{1} + 1 ) & ( for S being finite Subset of K st S is simplex-like holds

card S <= b_{2} + 1 ) & ex S being Subset of K st

( S is simplex-like & card S = b_{2} + 1 ) implies b_{1} = b_{2} ) & ( K is void & b_{1} = - 1 & b_{2} = - 1 implies b_{1} = b_{2} ) & ( ( K is void or not K is finite-degree ) & not K is void & b_{1} = +infty & b_{2} = +infty implies b_{1} = b_{2} ) )

for b_{1} 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} + 1 ) & ex S being Subset of K st

( S is simplex-like & card S = b_{1} + 1 ) ) iff b_{1} = - 1 )
;

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

( ( not K is void & K is finite-degree implies ex b

( ( for S being finite Subset of K st S is simplex-like holds

card S <= b

( S is simplex-like & card S = b

proof end;

uniqueness for b

( ( not K is void & K is finite-degree & ( for S being finite Subset of K st S is simplex-like holds

card S <= b

( S is simplex-like & card S = b

card S <= b

( S is simplex-like & card S = b

proof end;

consistency for b

( ( ( for S being finite Subset of K st S is simplex-like holds

card S <= b

( S is simplex-like & card S = b

:: deftheorem Def12 defines degree SIMPLEX0:def 12 :

for K being SimplicialComplexStr

for b_{2} being ext-real number holds

( ( not K is void & K is finite-degree implies ( b_{2} = degree K iff ( ( for S being finite Subset of K st S is simplex-like holds

card S <= b_{2} + 1 ) & ex S being Subset of K st

( S is simplex-like & card S = b_{2} + 1 ) ) ) ) & ( K is void implies ( b_{2} = degree K iff b_{2} = - 1 ) ) & ( ( K is void or not K is finite-degree ) & not K is void implies ( b_{2} = degree K iff b_{2} = +infty ) ) );

for K being SimplicialComplexStr

for b

( ( not K is void & K is finite-degree implies ( b

card S <= b

( S is simplex-like & card S = b

registration

let K be finite-degree SimplicialComplexStr;

coherence

(degree K) + 1 is natural

degree K is integer

end;
coherence

(degree K) + 1 is natural

proof end;

coherence degree K is integer

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

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

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;

begin

definition

let X be set ;

let KX be SimplicialComplexStr of X;

ex b_{1} being SimplicialComplex of X st

( [#] b_{1} c= [#] KX & the topology of b_{1} c= the topology of KX )

end;
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 ( [#] it c= [#] KX & the topology of it c= the topology of KX );

ex b

( [#] b

proof end;

:: deftheorem Def13 defines SubSimplicialComplex SIMPLEX0:def 13 :

for X being set

for KX being SimplicialComplexStr of X

for b_{3} being SimplicialComplex of X holds

( b_{3} is SubSimplicialComplex of KX iff ( [#] b_{3} c= [#] KX & the topology of b_{3} c= the topology of KX ) );

for X being set

for KX being SimplicialComplexStr of X

for b

( b

registration

let X be set ;

let KX be SimplicialComplexStr of X;

existence

ex b_{1} being SubSimplicialComplex of KX st

( b_{1} is empty & b_{1} is void & b_{1} is strict )

end;
let KX be SimplicialComplexStr of X;

existence

ex b

( b

proof end;

registration

let X be set ;

let KX be void SimplicialComplexStr of X;

coherence

for b_{1} being SubSimplicialComplex of KX holds b_{1} is void

end;
let KX be void SimplicialComplexStr of X;

coherence

for b

proof end;

registration

let D be non empty set ;

let KD be non void subset-closed SimplicialComplexStr of D;

existence

not for b_{1} being SubSimplicialComplex of KD holds b_{1} is void

end;
let KD be non void subset-closed SimplicialComplexStr of D;

existence

not for b

proof end;

registration

let X be set ;

let KX be finite-vertices SimplicialComplexStr of X;

coherence

for b_{1} being SubSimplicialComplex of KX holds b_{1} is finite-vertices

end;
let KX be finite-vertices SimplicialComplexStr of X;

coherence

for b

proof end;

registration

let X be set ;

let KX be finite-degree SimplicialComplexStr of X;

coherence

for b_{1} being SubSimplicialComplex of KX holds b_{1} is finite-degree

end;
let KX be finite-degree SimplicialComplexStr of X;

coherence

for b

proof 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

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

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

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

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

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

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;

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

for A being Subset of SX st A in the topology of KX holds

A is simplex-like ;

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

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 )

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 b_{1} being SubSimplicialComplex of KX st

( b_{1} is maximal & b_{1} is strict )

end;
let KX be SimplicialComplexStr of X;

existence

ex b

( b

proof 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

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

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

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 ;

ex b_{1} being strict maximal SubSimplicialComplex of KX st [#] b_{1} = A

for b_{1}, b_{2} being strict maximal SubSimplicialComplex of KX st [#] b_{1} = A & [#] b_{2} = A holds

b_{1} = b_{2}
by Th36;

end;
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 [#] it = A;

ex b

proof end;

uniqueness for b

b

:: 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_{4} being strict maximal SubSimplicialComplex of KX holds

( b_{4} = KX | A iff [#] b_{4} = A );

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

( b

definition

let X be set ;

let SC be SimplicialComplex of X;

let A be Subset of SC;

compatibility

for b_{1} being strict maximal SubSimplicialComplex of SC holds

( b_{1} = SC | A iff [#] b_{1} = A )

end;
let SC be SimplicialComplex of X;

let A be Subset of SC;

compatibility

for b

( b

proof 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_{4} being strict maximal SubSimplicialComplex of SC holds

( b_{4} = SC | A iff [#] b_{4} = A );

for X being set

for SC being SimplicialComplex of X

for A being Subset of SC

for b

( b

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

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

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

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

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;

begin

definition

let X be set ;

let KX be SimplicialComplexStr of X;

let i be real number ;

Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX)) is SimplicialComplexStr of X

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

Complex_of (the_subsets_with_limited_card ((i + 1), the topology of KX)) is SimplicialComplexStr of X

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

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;

coherence

Skeleton_of (KX,(- 1)) is empty-membered

coherence

Skeleton_of (KX,i) is finite-degree

end;
let KX be SimplicialComplexStr of X;

coherence

Skeleton_of (KX,(- 1)) is empty-membered

proof end;

let i be Integer;coherence

Skeleton_of (KX,i) is finite-degree

proof end;

registration

let X be set ;

let KX be empty-membered SimplicialComplexStr of X;

let i be Integer;

coherence

Skeleton_of (KX,i) is empty-membered

end;
let KX be empty-membered SimplicialComplexStr of X;

let i be Integer;

coherence

Skeleton_of (KX,i) is empty-membered

proof end;

registration

let D be non empty set ;

let KD be non void subset-closed SimplicialComplexStr of D;

let i be Integer;

coherence

not Skeleton_of (KD,i) is void

end;
let KD be non void subset-closed SimplicialComplexStr of D;

let i be Integer;

coherence

not Skeleton_of (KD,i) is void

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

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

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

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

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

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

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

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

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 B1: i is integer ;

( ( - 1 <= i & i <= degree K implies ex b_{1} being finite Simplex of K st card b_{1} = i + 1 ) & ( ( not - 1 <= i or not i <= degree K ) implies ex b_{1} being finite Simplex of K st b_{1} is empty ) )

consistency

for b_{1} being finite Simplex of K holds verum;

;

end;
let i be real number ;

assume B1: 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 card it = i + 1 if ( - 1 <= i & i <= degree K )

otherwise it is empty ;

( ( - 1 <= i & i <= degree K implies ex b

proof end;

correctness consistency

for b

;

:: 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_{3} being finite Simplex of K holds

( ( - 1 <= i & i <= degree K implies ( b_{3} is Simplex of i,K iff card b_{3} = i + 1 ) ) & ( ( not - 1 <= i or not i <= degree K ) implies ( b_{3} is Simplex of i,K iff b_{3} is empty ) ) );

for K being non void subset-closed SimplicialComplexStr

for i being real number st i is integer holds

for b

( ( - 1 <= i & i <= degree K implies ( b

registration

let K be non void subset-closed SimplicialComplexStr;

coherence

for b_{1} being Simplex of - 1,K holds b_{1} is empty

end;
coherence

for b

proof 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

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

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

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

B1: i is integer and

B2: i <= degree K ;

let S be Simplex of i,K;

existence

ex b_{1} being Simplex of max ((i - 1),(- 1)),K st b_{1} c= S

end;
let i be real number ;

assume that

B1: i is integer and

B2: i <= degree K ;

let S be Simplex of i,K;

existence

ex b

proof 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_{4} being Simplex of max ((i - 1),(- 1)),K holds

( b_{4} is Face of S iff b_{4} c= S );

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

( b

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

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;

ex b_{1} being strict SimplicialComplexStr of X st

( [#] b_{1} = [#] KX & ( for A being Subset of b_{1} holds

( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) )

for b_{1}, b_{2} being strict SimplicialComplexStr of X st [#] b_{1} = [#] KX & ( for A being Subset of b_{1} holds

( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) & [#] b_{2} = [#] KX & ( for A being Subset of b_{2} holds

( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) holds

b_{1} = b_{2}

end;
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 ( [#] 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 ) ) );

ex b

( [#] b

( 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

( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) & [#] b

( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) holds

b

proof end;

:: deftheorem Def20 defines subdivision SIMPLEX0:def 20 :

for X being set

for KX being SimplicialComplexStr of X

for P being Function

for b_{4} being strict SimplicialComplexStr of X holds

( b_{4} = subdivision (P,KX) iff ( [#] b_{4} = [#] KX & ( for A being Subset of b_{4} holds

( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) ) );

for X being set

for KX being SimplicialComplexStr of X

for P being Function

for b

( b

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

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

registration

let X be set ;

let KX be void SimplicialComplexStr of X;

let P be Function;

coherence

subdivision (P,KX) is empty-membered

end;
let KX be void SimplicialComplexStr of X;

let P be Function;

coherence

subdivision (P,KX) is empty-membered

proof 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

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

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

end;
let KX be finite-degree SimplicialComplexStr of X;

let P be Function;

coherence

subdivision (P,KX) is finite-degree

proof 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

end;
let KX be finite-vertices SimplicialComplexStr of X;

let P be Function;

coherence

subdivision (P,KX) is finite-vertices

proof 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

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)

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)

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)

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)

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)

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

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)

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;

ex b_{1} being SimplicialComplexStr of X ex F being Function st

( F . 0 = KX & F . n = b_{1} & dom F = NAT & ( for k being Nat

for KX1 being SimplicialComplexStr of X st KX1 = F . k holds

F . (k + 1) = subdivision (P,KX1) ) )

for b_{1}, b_{2} being SimplicialComplexStr of X st ex F being Function st

( F . 0 = KX & F . n = b_{1} & 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_{2} & 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_{1} = b_{2}

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

ex b

( F . 0 = KX & F . n = b

for KX1 being SimplicialComplexStr of X st KX1 = F . k holds

F . (k + 1) = subdivision (P,KX1) ) )

proof end;

uniqueness for b

( F . 0 = KX & F . n = b

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

for KX1 being SimplicialComplexStr of X st KX1 = F . k holds

F . (k + 1) = subdivision (P,KX1) ) ) holds

b

proof 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_{5} being SimplicialComplexStr of X holds

( b_{5} = subdivision (n,P,KX) iff ex F being Function st

( F . 0 = KX & F . n = b_{5} & dom F = NAT & ( for k being Nat

for KX1 being SimplicialComplexStr of X st KX1 = F . k holds

F . (k + 1) = subdivision (P,KX1) ) ) );

for X being set

for KX being SimplicialComplexStr of X

for P being Function

for n being Nat

for b

( b

( F . 0 = KX & F . n = b

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

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)

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

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

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)

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;