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

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;

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 b₁ being Element of symplexes C holds b₁ is empty

proof end;

end;

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 b₁ being SetSequence st b₁ 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 b₁ being SetSequence st
for n being Nat holds b₁ . n = Funcs ((X . (n + 1)),(X . n))

proof end;

uniqueness
for b₁, b₂ being SetSequence st ( for n being Nat holds b₁ . n = Funcs ((X . (n + 1)),(X . n)) ) & ( for n being Nat holds b₂ . n = Funcs ((X . (n + 1)),(X . n)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines FuncsSeq TRIANG_1:def 3 :
for X, b₂ being SetSequence holds
( b₂ = FuncsSeq X iff for n being Nat holds b₂ . 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 b₁ being SetSequence st
for n being Nat holds b₁ . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing }

proof end;

uniqueness
for b₁, b₂ being SetSequence st ( for n being Nat holds b₁ . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ) & ( for n being Nat holds b₂ . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines NatEmbSeq TRIANG_1:def 5 :
for b₁ being SetSequence holds
( b₁ = NatEmbSeq iff for n being Nat holds b₁ . 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 b₁ being Element of NatEmbSeq . n holds
( b₁ is Function-like & b₁ is Relation-like )

proof end;

end;

definition

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

end;

definition

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

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 b₁ being TriangStr st
( b₁ is lower_non-empty & b₁ 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 ;

end;

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 b₁ being Symplex of T,n st
for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b₁ = G . x

proof end;

uniqueness
for b₁, b₂ being Symplex of T,n st ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b₁ = G . x ) & ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b₂ = G . x ) holds
b₁ = b₂

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 b₅ being Symplex of T,n holds
( b₅ = face (x,f) iff for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
b₅ = 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 b₁ being strict lower_non-empty TriangStr st
( the SkeletonSeq of b₁ . 0 = {{}} & ( for n being Nat st n > 0 holds
the SkeletonSeq of b₁ . 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 b₁ . (n + 1) st s in the SkeletonSeq of b₁ . (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 b₁, b₂ being strict lower_non-empty TriangStr st the SkeletonSeq of b₁ . 0 = {{}} & ( for n being Nat st n > 0 holds
the SkeletonSeq of b₁ . 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 b₁ . (n + 1) st s in the SkeletonSeq of b₁ . (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 b₂ . 0 = {{}} & ( for n being Nat st n > 0 holds
the SkeletonSeq of b₂ . 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 b₂ . (n + 1) st s in the SkeletonSeq of b₂ . (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
b₁ = b₂

proof end;

end;

:: deftheorem defines Triang TRIANG_1:def 8 :
for C being non empty Poset
for b₂ being strict lower_non-empty TriangStr holds
( b₂ = Triang C iff ( the SkeletonSeq of b₂ . 0 = {{}} & ( for n being Nat st n > 0 holds
the SkeletonSeq of b₂ . 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 b₂ . (n + 1) st s in the SkeletonSeq of b₂ . (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 ) ) );