begin
theorem
theorem
begin
:: deftheorem TRIANG_1:def 1 :
canceled;
:: deftheorem defines symplexes TRIANG_1:def 2 :
for C being non empty Poset holds symplexes C = { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ;
theorem
canceled;
theorem
canceled;
theorem Th5:
theorem
theorem Th7:
theorem
canceled;
theorem
canceled;
theorem Th10:
begin
:: deftheorem Def4 defines lower_non-empty TRIANG_1:def 3 :
for IT being SetSequence holds
( IT is lower_non-empty iff for n being Nat st not IT . n is empty holds
for m being Nat st m < n holds
not IT . m is empty );
:: deftheorem Def5 defines FuncsSeq TRIANG_1:def 4 :
for X, b2 being SetSequence holds
( b2 = FuncsSeq X iff for n being Nat holds b2 . n = Funcs (X . (n + 1)),(X . n) );
:: deftheorem defines @ TRIANG_1:def 5 :
for n being Nat
for f being Element of Funcs (Seg n),(Seg (n + 1)) holds @ f = f;
:: deftheorem Def7 defines NatEmbSeq TRIANG_1:def 6 :
for b1 being SetSequence holds
( b1 = NatEmbSeq iff for n being Nat holds b1 . n = { f where f is Element of Funcs (Seg n),(Seg (n + 1)) : @ f is increasing } );
:: deftheorem TRIANG_1:def 7 :
canceled;
:: deftheorem Def9 defines lower_non-empty TRIANG_1:def 8 :
for T being TriangStr holds
( T is lower_non-empty iff the SkeletonSeq of T is lower_non-empty );
begin
definition
let T be
lower_non-empty TriangStr ;
let n be
Nat;
let x be
Symplex of
T,
(n + 1);
let f be
Face of
n;
assume A1:
the
SkeletonSeq of
T . (n + 1) <> {}
;
func face x,
f -> Symplex of
T,
n means :
Def10:
for
F,
G being
Function st
F = the
FacesAssign of
T . n &
G = F . f holds
it = G . x;
existence
ex b1 being Symplex of T,n st
for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b1 = G . x
uniqueness
for b1, b2 being Symplex of T,n st ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b1 = G . x ) & ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b2 = G . x ) holds
b1 = b2
end;
:: deftheorem Def10 defines face TRIANG_1:def 9 :
for T being lower_non-empty TriangStr
for n being Nat
for x being Symplex of T,(n + 1)
for f being Face of n st the SkeletonSeq of T . (n + 1) <> {} holds
for b5 being Symplex of T,n holds
( b5 = face x,f iff for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b5 = G . x );
definition
let C be non
empty Poset;
func Triang C -> strict lower_non-empty TriangStr means
( the
SkeletonSeq of
it . 0 = {{} } & ( for
n being
Nat st
n > 0 holds
the
SkeletonSeq of
it . n = { (SgmX the InternalRel of C,A) where A is non empty Element of symplexes C : card A = n } ) & ( for
n being
Nat for
f being
Face of
n for
s being
Element of the
SkeletonSeq of
it . (n + 1) st
s in the
SkeletonSeq of
it . (n + 1) holds
for
A being non
empty Element of
symplexes C st
SgmX the
InternalRel of
C,
A = s holds
face s,
f = (SgmX the InternalRel of C,A) * f ) );
existence
ex b1 being strict lower_non-empty TriangStr st
( the SkeletonSeq of b1 . 0 = {{} } & ( for n being Nat st n > 0 holds
the SkeletonSeq of b1 . n = { (SgmX the InternalRel of C,A) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of b1 . (n + 1) st s in the SkeletonSeq of b1 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX the InternalRel of C,A = s holds
face s,f = (SgmX the InternalRel of C,A) * f ) )
uniqueness
for b1, b2 being strict lower_non-empty TriangStr st the SkeletonSeq of b1 . 0 = {{} } & ( for n being Nat st n > 0 holds
the SkeletonSeq of b1 . n = { (SgmX the InternalRel of C,A) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of b1 . (n + 1) st s in the SkeletonSeq of b1 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX the InternalRel of C,A = s holds
face s,f = (SgmX the InternalRel of C,A) * f ) & the SkeletonSeq of b2 . 0 = {{} } & ( for n being Nat st n > 0 holds
the SkeletonSeq of b2 . n = { (SgmX the InternalRel of C,A) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of b2 . (n + 1) st s in the SkeletonSeq of b2 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX the InternalRel of C,A = s holds
face s,f = (SgmX the InternalRel of C,A) * f ) holds
b1 = b2
end;
:: deftheorem defines Triang TRIANG_1:def 10 :
for C being non empty Poset
for b2 being strict lower_non-empty TriangStr holds
( b2 = Triang C iff ( the SkeletonSeq of b2 . 0 = {{} } & ( for n being Nat st n > 0 holds
the SkeletonSeq of b2 . n = { (SgmX the InternalRel of C,A) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of b2 . (n + 1) st s in the SkeletonSeq of b2 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX the InternalRel of C,A = s holds
face s,f = (SgmX the InternalRel of C,A) * f ) ) );