:: TRIANG_1 semantic presentation

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

for b₁ being Nat st b₁ <= F₁() holds
P₁[b₁]

provided

E1: P₁[F₁()] and
E2: for b₁ being Nat st b₁ < F₁() & P₁[b₁ + 1] holds
P₁[b₁]

proof end;

registration

let c₁ be Nat;
cluster Seg (a₁ + 1) -> non empty ;
coherence by FINSEQ_1:6;

end;

registration

let c₁ be non empty set ;
let c₂ be Order of c₁;
cluster RelStr(# a₁,a₂ #) -> non empty ;
coherence ;

end;

theorem Th1: :: TRIANG_1:1

for b₁ being set holds {} |_2 b₁ = {}

proof end;

registration

let c₁ be set ;
cluster non empty Element of bool (Fin a₁);
existence

proof end;

end;

registration

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

proof end;

end;

registration

let c₁ be non empty set ;
let c₂ be non empty with_non-empty_elements Subset of (Fin c₁);
cluster non empty Element of a₂;
existence

proof end;

end;

registration

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

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be Order of c₁;
let c₃ be Subset of c₁;
redefine func |_2 as c₂ |_2 c₃ -> Order of a₃;
coherence

proof end;

end;

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

P₁[F₂()]

provided

E1: F₂() is finite and
E2: P₁[ {} F₁()] and
E3: for b₁ being Element of F₁()
for b₂ being Subset of F₁() st b₁ in F₂() & b₂ c= F₂() & P₁[b₂] holds
P₁[b₂ \/ {b₁}]

proof end;

theorem Th2: :: TRIANG_1:2

for b₁ being non empty Poset
for b₂ being Subset of b₁ st b₂ is finite & b₂ <> {} & ( for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ & not b₃ <= b₄ holds
b₄ <= b₃ ) holds
ex b₃ being Element of b₁ st
( b₃ in b₂ & ( for b₄ being Element of b₁ st b₄ in b₂ holds
b₃ <= b₄ ) )

proof end;

registration

let c₁ be non empty set ;
let c₂ be with_non-empty_element Subset of (Fin c₁);
cluster non empty finite Element of a₂;
existence

proof end;

end;

registration

let c₁ be non empty Poset;
let c₂ be non empty finite Subset of c₁;
let c₃ be Element of c₁;
cluster InitSegm a₂,a₃ -> finite ;
coherence

proof end;

end;

theorem Th3: :: TRIANG_1:3

for b₁, b₂ being finite set st b₁ c= b₂ & card b₁ = card b₂ holds
b₁ = b₂

proof end;

definition

let c₁ be set ;
let c₂ be finite Subset of c₁;
let c₃ be Order of c₁;
assume E2: c₃ linearly_orders c₂ ;
canceled;
func SgmX c₃,c₂ -> FinSequence of a₁ means :Def2: :: TRIANG_1:def 2
( rng a₄ = a₂ & ( for b₁, b₂ being Nat st b₁ in dom a₄ & b₂ in dom a₄ & b₁ < b₂ holds
( a₄ /. b₁ <> a₄ /. b₂ & [(a₄ /. b₁),(a₄ /. b₂)] in a₃ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 TRIANG_1:def 1 :

:: deftheorem Def2 defines SgmX TRIANG_1:def 2 :

theorem Th4: :: TRIANG_1:4

for b₁ being set
for b₂ being finite Subset of b₁
for b₃ being Order of b₁
for b₄ being FinSequence of b₁ st rng b₄ = b₂ & ( for b₅, b₆ being Nat st b₅ in dom b₄ & b₆ in dom b₄ & b₅ < b₆ holds
( b₄ /. b₅ <> b₄ /. b₆ & [(b₄ /. b₅),(b₄ /. b₆)] in b₃ ) ) holds
b₄ = SgmX b₃,b₂

proof end;

definition

let c₁ be non empty Poset;
func symplexes c₁ -> Subset of (Fin the carrier of a₁) equals :: TRIANG_1:def 3
{ b₁ where B is Element of Fin the carrier of a₁ : the InternalRel of a₁ linearly_orders b₁ } ;
coherence

proof end;

end;

:: deftheorem Def3 defines symplexes TRIANG_1:def 3 :

registration

let c₁ be non empty Poset;
cluster symplexes a₁ -> with_non-empty_element ;
coherence

proof end;

end;

theorem Th5: :: TRIANG_1:5

for b₁ being non empty Poset
for b₂ being Element of b₁ holds {b₂} in symplexes b₁

proof end;

theorem Th6: :: TRIANG_1:6

for b₁ being non empty Poset holds {} in symplexes b₁

proof end;

theorem Th7: :: TRIANG_1:7

for b₁ being non empty Poset
for b₂, b₃ being set st b₂ c= b₃ & b₃ in symplexes b₁ holds
b₂ in symplexes b₁

proof end;

registration

let c₁ be set ;
let c₂ be non empty Subset of (Fin c₁);
cluster -> finite Element of a₂;
coherence by FINSUB_1:def 5;

end;

definition

let c₁ be set ;
let c₂ be non empty Subset of (Fin c₁);
redefine mode Element as Element of c₂ -> Subset of a₁;
coherence

proof end;

end;

theorem Th8: :: TRIANG_1:8

for b₁ being set
for b₂ being finite Subset of b₁
for b₃ being Order of b₁ st b₃ linearly_orders b₂ holds
SgmX b₃,b₂ is one-to-one

proof end;

theorem Th9: :: TRIANG_1:9

for b₁ being set
for b₂ being finite Subset of b₁
for b₃ being Order of b₁ st b₃ linearly_orders b₂ holds
len (SgmX b₃,b₂) = Card b₂

proof end;

theorem Th10: :: TRIANG_1:10

for b₁ being Nat
for b₂ being non empty Poset
for b₃ being non empty Element of symplexes b₂ st Card b₃ = b₁ holds
dom (SgmX the InternalRel of b₂,b₃) = Seg b₁

proof end;

registration

let c₁ be non empty Poset;
cluster non empty finite Element of symplexes a₁;
existence

proof end;

end;

definition

mode SetSequence is ManySortedSet of NAT ;

end;

definition

let c₁ be SetSequence;
attr a₁ is lower_non-empty means :Def4: :: TRIANG_1:def 4
for b₁ being Nat st not a₁ . b₁ is empty holds
for b₂ being Nat st b₂ < b₁ holds
not a₁ . b₂ is empty;

end;

:: deftheorem Def4 defines lower_non-empty TRIANG_1:def 4 :

registration

cluster lower_non-empty ManySortedSet of NAT ;
existence

proof end;

end;

definition

let c₁ be SetSequence;
func FuncsSeq c₁ -> SetSequence means :Def5: :: TRIANG_1:def 5
for b₁ being Nat holds a₂ . b₁ = Funcs (a₁ . (b₁ + 1)),(a₁ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines FuncsSeq TRIANG_1:def 5 :

registration

let c₁ be lower_non-empty SetSequence;
let c₂ be Nat;
cluster (FuncsSeq a₁) . a₂ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be Nat;
let c₂ be Element of Funcs (Seg c₁),(Seg (c₁ + 1));
func @ c₂ -> FinSequence of REAL equals :: TRIANG_1:def 6
a₂;
coherence

proof end;

end;

:: deftheorem Def6 defines @ TRIANG_1:def 6 :

definition

func NatEmbSeq -> SetSequence means :Def7: :: TRIANG_1:def 7
for b₁ being Nat holds a₁ . b₁ = { b₂ where B is Element of Funcs (Seg b₁),(Seg (b₁ + 1)) : @ b₂ is increasing } ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines NatEmbSeq TRIANG_1:def 7 :

registration

let c₁ be Nat;
cluster NatEmbSeq . a₁ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be Nat;
cluster -> Relation-like Function-like Element of NatEmbSeq . a₁;
coherence

proof end;

end;

definition

let c₁ be SetSequence;
mode triangulation of a₁ is ManySortedFunction of NatEmbSeq , FuncsSeq a₁;

end;

definition

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

end;

definition

let c₁ be TriangStr ;
canceled;
attr a₁ is lower_non-empty means :Def9: :: TRIANG_1:def 9
the SkeletonSeq of a₁ is lower_non-empty;

end;

:: deftheorem Def8 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 c₁ be lower_non-empty TriangStr ;
cluster the SkeletonSeq of a₁ -> lower_non-empty ;
coherence by Def9;

end;

registration

let c₁ be lower_non-empty SetSequence;
let c₂ be ManySortedFunction of NatEmbSeq , FuncsSeq c₁;
cluster TriangStr(# a₁,a₂ #) -> lower_non-empty ;
coherence by Def9;

end;

definition

let c₁ be TriangStr ;
let c₂ be Nat;
mode Symplex of a₁,a₂ is Element of the SkeletonSeq of a₁ . a₂;

end;

definition

let c₁ be Nat;
mode Face of a₁ is Element of NatEmbSeq . a₁;

end;

definition

let c₁ be lower_non-empty TriangStr ;
let c₂ be Nat;
let c₃ be Symplex of c₁,(c₂ + 1);
let c₄ be Face of c₂;
assume E13: the SkeletonSeq of c₁ . (c₂ + 1) <> {} ;
func face c₃,c₄ -> Symplex of a₁,a₂ means :Def10: :: TRIANG_1:def 10
for b₁, b₂ being Function st b₁ = the FacesAssign of a₁ . a₂ & b₂ = b₁ . a₄ holds
a₅ = b₂ . a₃;
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 a₂ . 0 = {{} } & ( for b₁ being Nat st b₁ > 0 holds
the SkeletonSeq of a₂ . b₁ = { (SgmX the InternalRel of a₁,b₂) where B is non empty Element of symplexes a₁ : Card b₂ = b₁ } ) & ( for b₁ being Nat
for b₂ being Face of b₁
for b₃ being Element of the SkeletonSeq of a₂ . (b₁ + 1) st b₃ in the SkeletonSeq of a₂ . (b₁ + 1) holds
for b₄ being non empty Element of symplexes a₁ st SgmX the InternalRel of a₁,b₄ = b₃ holds
face b₃,b₂ = (SgmX the InternalRel of a₁,b₄) * b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines Triang TRIANG_1:def 11 :