:: On the concept of the triangulation
:: by Beata Madras
::
:: Received October 28, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

registration
let X be non empty set ;
let R be Order of X;
cluster RelStr(# X,R #) -> non empty ;
coherence
not RelStr(# X,R #) is empty
;
end;

theorem :: TRIANG_1:1
for A being set holds {} |_2 A = {} ;

theorem :: TRIANG_1:2
for F being non empty Poset
for A being Subset of F st A is finite & A <> {} & ( for B, C being Element of F st B in A & C in A & not B <= C holds
C <= B ) holds
ex m being Element of F st
( m in A & ( for C being Element of F st C in A holds
m <= C ) )
proof end;

registration
let P be non empty Poset;
let A be non empty finite Subset of P;
let x be Element of P;
cluster InitSegm (A,x) -> finite ;
coherence
InitSegm (A,x) is finite
;
end;

begin

definition
let C be non empty Poset;
func symplexes C -> Subset of (Fin the carrier of C) equals :: TRIANG_1:def 1
{ A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ;
coherence
{ A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } is Subset of (Fin the carrier of C)
proof end;
end;

:: deftheorem defines symplexes TRIANG_1:def 1 :
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 } ;

registration
let C be non empty Poset;
cluster symplexes C -> with_non-empty_element ;
coherence
not symplexes C is empty-membered
proof end;
end;

theorem Th3: :: TRIANG_1:3
for C being non empty Poset
for x being Element of C holds {x} in symplexes C
proof end;

theorem :: TRIANG_1:4
for C being non empty Poset holds {} in symplexes C
proof end;

theorem Th5: :: TRIANG_1:5
for C being non empty Poset
for x, s being set st x c= s & s in symplexes C holds
x in symplexes C
proof end;

theorem Th6: :: TRIANG_1:6
for n being Element of NAT
for C being non empty Poset
for A being non empty Element of symplexes C st card A = n holds
dom (SgmX ( the InternalRel of C,A)) = Seg n
proof end;

registration
let C be non empty Poset;
cluster non empty finite for Element of symplexes C;
existence
not for b1 being Element of symplexes C holds b1 is empty
proof end;
end;

begin

definition
mode SetSequence is ManySortedSet of NAT ;
end;

definition
let IT be SetSequence;
attr IT is lower_non-empty means :Def2: :: TRIANG_1:def 2
for n being Nat st not IT . n is empty holds
for m being Nat st m < n holds
not IT . m is empty ;
end;

:: deftheorem Def2 defines lower_non-empty TRIANG_1:def 2 :
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 );

registration
cluster Relation-like NAT -defined Function-like total lower_non-empty for set ;
existence
ex b1 being SetSequence st b1 is lower_non-empty
proof end;
end;

definition
let X be SetSequence;
func FuncsSeq X -> SetSequence means :Def3: :: TRIANG_1:def 3
for n being Nat holds it . n = Funcs ((X . (n + 1)),(X . n));
existence
ex b1 being SetSequence st
for n being Nat holds b1 . n = Funcs ((X . (n + 1)),(X . n))
proof end;
uniqueness
for b1, b2 being SetSequence st ( for n being Nat holds b1 . n = Funcs ((X . (n + 1)),(X . n)) ) & ( for n being Nat holds b2 . n = Funcs ((X . (n + 1)),(X . n)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines FuncsSeq TRIANG_1:def 3 :
for X, b2 being SetSequence holds
( b2 = FuncsSeq X iff for n being Nat holds b2 . n = Funcs ((X . (n + 1)),(X . n)) );

registration
let X be lower_non-empty SetSequence;
let n be Nat;
cluster (FuncsSeq X) . n -> non empty ;
coherence
not (FuncsSeq X) . n is empty
proof end;
end;

definition
let n be Nat;
let f be Element of Funcs ((Seg n),(Seg (n + 1)));
func @ f -> FinSequence of REAL equals :: TRIANG_1:def 4
f;
coherence
f is FinSequence of REAL
proof end;
end;

:: deftheorem defines @ TRIANG_1:def 4 :
for n being Nat
for f being Element of Funcs ((Seg n),(Seg (n + 1))) holds @ f = f;

definition
func NatEmbSeq -> SetSequence means :Def5: :: TRIANG_1:def 5
for n being Nat holds it . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ;
existence
ex b1 being SetSequence st
for n being Nat holds b1 . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing }
proof end;
uniqueness
for b1, b2 being SetSequence st ( for n being Nat holds b1 . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ) & ( for n being Nat holds b2 . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines NatEmbSeq TRIANG_1:def 5 :
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 } );

registration
let n be Nat;
cluster NatEmbSeq . n -> non empty ;
coherence
not NatEmbSeq . n is empty
proof end;
end;

registration
let n be Nat;
cluster -> Relation-like Function-like for Element of NatEmbSeq . n;
coherence
for b1 being Element of NatEmbSeq . n holds
( b1 is Function-like & b1 is Relation-like )
proof end;
end;

definition
let X be SetSequence;
mode triangulation of X is ManySortedFunction of NatEmbSeq , FuncsSeq X;
end;

definition
attr c1 is strict ;
struct TriangStr -> ;
aggr TriangStr(# SkeletonSeq, FacesAssign #) -> TriangStr ;
sel SkeletonSeq c1 -> SetSequence;
sel FacesAssign c1 -> ManySortedFunction of NatEmbSeq , FuncsSeq the SkeletonSeq of c1;
end;

definition
let T be TriangStr ;
attr T is lower_non-empty means :Def6: :: TRIANG_1:def 6
the SkeletonSeq of T is lower_non-empty ;
end;

:: deftheorem Def6 defines lower_non-empty TRIANG_1:def 6 :
for T being TriangStr holds
( T is lower_non-empty iff the SkeletonSeq of T is lower_non-empty );

registration
cluster strict lower_non-empty for TriangStr ;
existence
ex b1 being TriangStr st
( b1 is lower_non-empty & b1 is strict )
proof end;
end;

registration
let T be lower_non-empty TriangStr ;
cluster the SkeletonSeq of T -> lower_non-empty ;
coherence
the SkeletonSeq of T is lower_non-empty
by Def6;
end;

registration
let S be lower_non-empty SetSequence;
let F be ManySortedFunction of NatEmbSeq , FuncsSeq S;
cluster TriangStr(# S,F #) -> lower_non-empty ;
coherence
TriangStr(# S,F #) is lower_non-empty
by Def6;
end;

begin

definition
let T be TriangStr ;
let n be Nat;
mode Symplex of T,n is Element of the SkeletonSeq of T . n;
end;

definition
let n be Nat;
mode Face of n is Element of NatEmbSeq . n;
end;

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 :Def7: :: TRIANG_1:def 7
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
proof end;
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
proof end;
end;

:: deftheorem Def7 defines face TRIANG_1:def 7 :
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 :: TRIANG_1:def 8
( 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 ) )
proof end;
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
proof end;
end;

:: deftheorem defines Triang TRIANG_1:def 8 :
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 ) ) );