:: TRIANG_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

scheme :: TRIANG_1:sch 1
Regr1{ F1() -> Nat, P1[ set ] } :
for k being Nat st k <= F1() holds
P1[k]
provided
A1: P1[F1()] and
A2: for k being Nat st k < F1() & P1[k + 1] holds
P1[k]
proof end;

registration
let n be Nat;
cluster Seg (n + 1) -> non empty ;
coherence
not Seg (n + 1) is empty
by FINSEQ_1:6;
end;

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set holds {} |_2 A = {}
proof end;

registration
let X be set ;
cluster non empty Element of bool (Fin X);
existence
not for b1 being Subset of (Fin X) holds b1 is empty
proof end;
end;

registration
let X be non empty set ;
cluster non empty with_non-empty_elements Element of bool (Fin X);
existence
ex b1 being Subset of (Fin X) st
( not b1 is empty & b1 is with_non-empty_elements )
proof end;
end;

registration
let X be non empty set ;
let F be non empty with_non-empty_elements Subset of (Fin X);
cluster non empty Element of F;
existence
not for b1 being Element of F holds b1 is empty
proof end;
end;

registration
let X be non empty set ;
cluster with_non-empty_element Element of bool (Fin X);
existence
ex b1 being Subset of (Fin X) st b1 is with_non-empty_element
proof end;
end;

definition
let X be non empty set ;
let R be Order of X;
let A be Subset of X;
:: original: |_2
redefine func R |_2 A -> Order of A;
coherence
R |_2 A is Order of A
proof end;
end;

scheme :: TRIANG_1:sch 2
SubFinite{ F1() -> set , F2() -> Subset of F1(), P1[ set ] } :
P1[F2()]
provided
A1: F2() is finite and
A2: P1[ {} F1()] and
A3: for x being Element of F1()
for B being Subset of F1() st x in F2() & B c= F2() & P1[B] holds
P1[B \/ {x}]
proof end;

theorem :: TRIANG_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 X be non empty set ;
let F be with_non-empty_element Subset of (Fin X);
cluster non empty finite Element of F;
existence
ex b1 being Element of F st
( b1 is finite & not b1 is empty )
proof end;
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
proof end;
end;

theorem Th3: :: TRIANG_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being finite set st A c= B & card A = card B holds
A = B
proof end;

definition
let X be set ;
let A be finite Subset of X;
let R be Order of X;
assume A1: R linearly_orders A ;
canceled;
func SgmX R,A -> FinSequence of X means :Def2: :: TRIANG_1:def 2
( rng it = A & ( for n, m being Nat st n in dom it & m in dom it & n < m holds
( it /. n <> it /. m & [(it /. n),(it /. m)] in R ) ) );
existence
ex b1 being FinSequence of X st
( rng b1 = A & ( for n, m being Nat st n in dom b1 & m in dom b1 & n < m holds
( b1 /. n <> b1 /. m & [(b1 /. n),(b1 /. m)] in R ) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of X st rng b1 = A & ( for n, m being Nat st n in dom b1 & m in dom b1 & n < m holds
( b1 /. n <> b1 /. m & [(b1 /. n),(b1 /. m)] in R ) ) & rng b2 = A & ( for n, m being Nat st n in dom b2 & m in dom b2 & n < m holds
( b2 /. n <> b2 /. m & [(b2 /. n),(b2 /. m)] in R ) ) holds
b1 = b2
proof end;
end;

:: deftheorem TRIANG_1:def 1 :
canceled;

:: deftheorem Def2 defines SgmX TRIANG_1:def 2 :
for X being set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
for b4 being FinSequence of X holds
( b4 = SgmX R,A iff ( rng b4 = A & ( for n, m being Nat st n in dom b4 & m in dom b4 & n < m holds
( b4 /. n <> b4 /. m & [(b4 /. n),(b4 /. m)] in R ) ) ) );

theorem Th4: :: TRIANG_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being finite Subset of X
for R being Order of X
for f being FinSequence of X st rng f = A & ( for n, m being Nat st n in dom f & m in dom f & n < m holds
( f /. n <> f /. m & [(f /. n),(f /. m)] in R ) ) holds
f = SgmX R,A
proof end;

definition
let C be non empty Poset;
func symplexes C -> Subset of (Fin the carrier of C) equals :: TRIANG_1:def 3
{ 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 3 :
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
symplexes C is with_non-empty_element
proof end;
end;

theorem Th5: :: TRIANG_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty Poset
for x being Element of C holds {x} in symplexes C
proof end;

theorem :: TRIANG_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty Poset holds {} in symplexes C
proof end;

theorem Th7: :: TRIANG_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

registration
let X be set ;
let F be non empty Subset of (Fin X);
cluster -> finite Element of F;
coherence
for b1 being Element of F holds b1 is finite
by FINSUB_1:def 5;
end;

definition
let X be set ;
let F be non empty Subset of (Fin X);
:: original: Element
redefine mode Element of F -> Subset of X;
coherence
for b1 being Element of F holds b1 is Subset of X
proof end;
end;

theorem Th8: :: TRIANG_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
SgmX R,A is one-to-one
proof end;

theorem Th9: :: TRIANG_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
len (SgmX R,A) = Card A
proof end;

theorem Th10: :: TRIANG_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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 Element of symplexes C;
existence
not for b1 being Element of symplexes C holds b1 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 :Def4: :: TRIANG_1:def 4
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 Def4 defines lower_non-empty TRIANG_1:def 4 :
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 lower_non-empty ManySortedSet of NAT ;
existence
ex b1 being SetSequence st b1 is lower_non-empty
proof end;
end;

definition
let X be SetSequence;
func FuncsSeq X -> SetSequence means :Def5: :: TRIANG_1:def 5
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 Def5 defines FuncsSeq TRIANG_1:def 5 :
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 6
f;
coherence
f is FinSequence of REAL
proof end;
end;

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

definition
func NatEmbSeq -> SetSequence means :Def7: :: TRIANG_1:def 7
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 Def7 defines NatEmbSeq TRIANG_1:def 7 :
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 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 ;
canceled;
attr T is lower_non-empty means :Def9: :: TRIANG_1:def 9
the SkeletonSeq of T is lower_non-empty;
end;

:: deftheorem TRIANG_1:def 8 :
canceled;

:: deftheorem Def9 defines lower_non-empty TRIANG_1:def 9 :
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 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 Def9;
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 Def9;
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 :Def10: :: TRIANG_1:def 10
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 Def10 defines face TRIANG_1:def 10 :
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 11
( 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 11 :
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 ) ) );