TRIANG_1: On the concept of the triangulation

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

scheme :: TRIANG_1:sch 1
Regr1{ F₁() -> Nat, P₁[ set ] } :

for k being Element of NAT st k <= F₁() holds
P₁[k]

provided

A1: P₁[F₁()] and
A2: for k being Element of NAT st k < F₁() & P₁[k + 1] holds
P₁[k]

proof end;

registration

let n be Nat;
cluster Seg (n + 1) -> non empty ;
coherence ;

end;

registration

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

end;

theorem :: TRIANG_1:1

for A being set holds {} |_2 A = {} ;

registration

let X be set ;
cluster non empty Element of bool (Fin X);
existence

proof end;

end;

registration

let X be non empty set ;
cluster non empty with_non-empty_elements Element of bool (Fin X);
existence

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

proof end;

end;

registration

let X be non empty set ;
cluster with_non-empty_element Element of bool (Fin X);
existence

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

proof end;

end;

scheme :: TRIANG_1:sch 2
SubFinite{ F₁() -> set , F₂() -> Subset of F₁(), P₁[ set ] } :

P₁[F₂()]

provided

A1: F₂() is finite and
A2: P₁[ {} F₁()] and
A3: for x being Element of F₁()
for B being Subset of F₁() st x in F₂() & B c= F₂() & P₁[B] holds
P₁[B \/ {x}]

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

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

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 ;

end;

theorem Th3: :: TRIANG_1:3

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

proof end;

uniqueness

proof end;

end;

:: deftheorem TRIANG_1:def 1 :

:: deftheorem Def2 defines SgmX TRIANG_1:def 2 :

theorem Th4: :: TRIANG_1:4

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

proof end;

end;

:: deftheorem defines symplexes TRIANG_1:def 3 :

registration

let C be non empty Poset;
cluster symplexes C -> with_non-empty_element ;
coherence

proof end;

end;

theorem Th5: :: TRIANG_1:5

for C being non empty Poset
for x being Element of C holds {x} in symplexes C

proof end;

theorem :: TRIANG_1:6

for C being non empty Poset holds {} in symplexes C

proof end;

theorem Th7: :: TRIANG_1:7

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 ;

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

proof end;

end;

theorem Th8: :: TRIANG_1:8

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

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

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 Element of symplexes C;
existence

proof end;

end;

definition

mode SetSequence is ManySortedSet of ;

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 :

registration

cluster lower_non-empty set ;
existence

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines FuncsSeq TRIANG_1:def 5 :

registration

let X be lower_non-empty SetSequence;
let n be Nat;
cluster (FuncsSeq X) . n -> non empty ;
coherence

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

proof end;

end;

:: deftheorem defines @ TRIANG_1:def 6 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines NatEmbSeq TRIANG_1:def 7 :

registration

let n be Nat;
cluster NatEmbSeq . n -> non empty ;
coherence

proof end;

end;

registration

let n be Nat;
cluster -> Relation-like Function-like Element of NatEmbSeq . n;
coherence

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

:: deftheorem Def9 defines lower_non-empty TRIANG_1:def 9 :

registration

cluster strict lower_non-empty TriangStr ;
existence

proof end;

end;

registration

let T be lower_non-empty TriangStr ;
cluster the SkeletonSeq of T -> lower_non-empty ;
coherence 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 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines face TRIANG_1:def 10 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines Triang TRIANG_1:def 11 :