:: 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 &amp; A <> {} &amp; ( for B, C being Element of F st B in A &amp; C in A &amp; not B <= C holds
C <= B ) holds
ex m being Element of F st
( m in A &amp; ( for C being Element of F st C in A holds
m <= C ) )
proofend;

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

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

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

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

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

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

begin

definition
mode SetSequence is ManySortedSet of NAT ;
end;

definition
let IT be SetSequence;
attrIT 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
proofend;
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))
proofend;
uniqueness
 for b1, b2 being SetSequence st ( for n being Nat holds b1 . n = Funcs ((X . (n + 1)),(X . n)) ) &amp; ( for n being Nat holds b2 . n = Funcs ((X . (n + 1)),(X . n)) ) holds
b1 = b2
proofend;
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
proofend;
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
proofend;
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  }
proofend;
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  }  ) &amp; ( 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
proofend;
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;
clusterNatEmbSeq . n ->  non empty ;
coherence
 not NatEmbSeq . n is empty
proofend;
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 &amp; b1 is Relation-like )
proofend;
end;

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

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

definition
let T be TriangStr ;
attrT 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 &amp; b1 is strict )
proofend;
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 &amp; 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 &amp; G = F . f holds
b1 = G . x
proofend;
uniqueness
 for b1, b2 being Symplex of T,n st ( for F, G being Function st F = the FacesAssign of T . n &amp; G = F . f holds
b1 = G . x ) &amp; ( for F, G being Function st F = the FacesAssign of T . n &amp; G = F . f holds
b2 = G . x ) holds
b1 = b2
proofend;
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 &amp; 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 = {{}} &amp; ( 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  }  ) &amp; ( 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 = {{}} &amp; ( 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  }  ) &amp; ( 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 ) )
proofend;
uniqueness
 for b1, b2 being strict lower_non-empty TriangStr st the SkeletonSeq of b1 . 0 = {{}} &amp; ( 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  }  ) &amp; ( 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 ) &amp; the SkeletonSeq of b2 . 0 = {{}} &amp; ( 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  }  ) &amp; ( 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
proofend;
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 = {{}} &amp; ( 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  }  ) &amp; ( 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 ) ) );