:: by Beata Madras

::

:: Received October 28, 1995

:: Copyright (c) 1995-2021 Association of Mizar Users

registration
end;

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

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;

coherence

InitSegm (A,x) is finite ;

end;
let A be non empty finite Subset of P;

let x be Element of P;

coherence

InitSegm (A,x) is finite ;

definition

let C be non empty Poset;

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

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

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

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

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

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;

existence

not for b_{1} being Element of symplexes C holds b_{1} is empty

end;
existence

not for b

proof end;

definition

let IT be SetSequence;

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

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

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

definition

let X be SetSequence;

ex b_{1} being SetSequence st

for n being Nat holds b_{1} . n = Funcs ((X . (n + 1)),(X . n))

for b_{1}, b_{2} being SetSequence st ( for n being Nat holds b_{1} . n = Funcs ((X . (n + 1)),(X . n)) ) & ( for n being Nat holds b_{2} . n = Funcs ((X . (n + 1)),(X . n)) ) holds

b_{1} = b_{2}

end;
func FuncsSeq X -> SetSequence means :Def3: :: TRIANG_1:def 3

for n being Nat holds it . n = Funcs ((X . (n + 1)),(X . n));

existence for n being Nat holds it . n = Funcs ((X . (n + 1)),(X . n));

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines FuncsSeq TRIANG_1:def 3 :

for X, b_{2} being SetSequence holds

( b_{2} = FuncsSeq X iff for n being Nat holds b_{2} . n = Funcs ((X . (n + 1)),(X . n)) );

for X, b

( b

registration

let X be lower_non-empty SetSequence;

let n be Nat;

coherence

not (FuncsSeq X) . n is empty

end;
let n be Nat;

coherence

not (FuncsSeq X) . n is empty

proof end;

definition

let n be Nat;

let f be Element of Funcs ((Seg n),(Seg (n + 1)));

coherence

f is FinSequence of REAL

end;
let f be Element of Funcs ((Seg n),(Seg (n + 1)));

coherence

f is FinSequence of REAL

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

for n being Nat

for f being Element of Funcs ((Seg n),(Seg (n + 1))) holds @ f = f;

definition

ex b_{1} being SetSequence st

for n being Nat holds b_{1} . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing }

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

b_{1} = b_{2}
end;

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 for n being Nat holds it . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines NatEmbSeq TRIANG_1:def 5 :

for b_{1} being SetSequence holds

( b_{1} = NatEmbSeq iff for n being Nat holds b_{1} . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } );

for b

( b

registration
end;

registration

let n be Nat;

coherence

for b_{1} being Element of NatEmbSeq . n holds

( b_{1} is Function-like & b_{1} is Relation-like )

end;
coherence

for b

( b

proof end;

definition
end;

definition

attr c_{1} is strict ;

struct TriangStr -> ;

aggr TriangStr(# SkeletonSeq, FacesAssign #) -> TriangStr ;

sel SkeletonSeq c_{1} -> SetSequence;

sel FacesAssign c_{1} -> ManySortedFunction of NatEmbSeq , FuncsSeq the SkeletonSeq of c_{1};

end;
struct TriangStr -> ;

aggr TriangStr(# SkeletonSeq, FacesAssign #) -> TriangStr ;

sel SkeletonSeq c

sel FacesAssign c

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

for T being TriangStr holds

( T is lower_non-empty iff the SkeletonSeq of T is lower_non-empty );

registration
end;

registration
end;

registration

let S be lower_non-empty SetSequence;

let F be ManySortedFunction of NatEmbSeq , FuncsSeq S;

coherence

TriangStr(# S,F #) is lower_non-empty ;

end;
let F be ManySortedFunction of NatEmbSeq , FuncsSeq S;

coherence

TriangStr(# S,F #) is lower_non-empty ;

definition
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) <> {} ;

ex b_{1} being Symplex of T,n st

for F, G being Function st F = the FacesAssign of T . n & G = F . f holds

b_{1} = G . x

for b_{1}, b_{2} being Symplex of T,n st ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds

b_{1} = G . x ) & ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds

b_{2} = G . x ) holds

b_{1} = b_{2}

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

it = G . x;

ex b

for F, G being Function st F = the FacesAssign of T . n & G = F . f holds

b

proof end;

uniqueness for b

b

b

b

proof 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_{5} being Symplex of T,n holds

( b_{5} = face (x,f) iff for F, G being Function st F = the FacesAssign of T . n & G = F . f holds

b_{5} = G . x );

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

( b

b

definition

let C be non empty Poset;

ex b_{1} being strict lower_non-empty TriangStr st

( the SkeletonSeq of b_{1} . 0 = {{}} & ( for n being Nat st n > 0 holds

the SkeletonSeq of b_{1} . 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_{1} . (n + 1) st s in the SkeletonSeq of b_{1} . (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 ) )

for b_{1}, b_{2} being strict lower_non-empty TriangStr st the SkeletonSeq of b_{1} . 0 = {{}} & ( for n being Nat st n > 0 holds

the SkeletonSeq of b_{1} . 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_{1} . (n + 1) st s in the SkeletonSeq of b_{1} . (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_{2} . 0 = {{}} & ( for n being Nat st n > 0 holds

the SkeletonSeq of b_{2} . 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_{2} . (n + 1) st s in the SkeletonSeq of b_{2} . (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_{1} = b_{2}

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

ex b

( the SkeletonSeq of b

the SkeletonSeq of b

for f being Face of n

for s being Element of the SkeletonSeq of b

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

the SkeletonSeq of b

for f being Face of n

for s being Element of the SkeletonSeq of b

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

the SkeletonSeq of b

for f being Face of n

for s being Element of the SkeletonSeq of b

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

proof end;

:: deftheorem defines Triang TRIANG_1:def 8 :

for C being non empty Poset

for b_{2} being strict lower_non-empty TriangStr holds

( b_{2} = Triang C iff ( the SkeletonSeq of b_{2} . 0 = {{}} & ( for n being Nat st n > 0 holds

the SkeletonSeq of b_{2} . 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_{2} . (n + 1) st s in the SkeletonSeq of b_{2} . (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 ) ) );

for C being non empty Poset

for b

( b

the SkeletonSeq of b

for f being Face of n

for s being Element of the SkeletonSeq of b

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