:: SIMPLEX1 semantic presentation

REAL is set

- 1 is non empty V21() V29() ext-real non positive negative set
K87(1) is non empty V21() V29() V30() ext-real non positive negative finite set

RAT is set
INT is set

is Relation-like non empty non trivial non finite non empty-membered set

K469() is set

K272() is M10()

K36(K272(),) is set
K620() is TopStruct
the carrier of K620() is set

- 1 is non empty V21() V29() V30() ext-real non positive negative finite Element of REAL
+infty is non empty V29() ext-real positive non negative set
-infty is non empty V29() ext-real non positive negative set

k is set

dom V is set
(dom V) \ k is Element of bool (dom V)
bool (dom V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
V | ((dom V) \ k) is Relation-like set
card (V | ((dom V) \ k)) is epsilon-transitive epsilon-connected ordinal cardinal set

(card (V | ((dom V) \ k))) +` (Aff *` (card k)) is epsilon-transitive epsilon-connected ordinal cardinal set

dom XX is set
x is set
XX . x is set
Im (V,x) is set

dom C is set
rng C is set

dom x is set
C is set
x . C is set
XX . C is set

dom F is set
rng F is set

dom F is set
rng F is set
[:k,Aff:] is Relation-like set
X is set
A1 is set
F . A1 is set
A1 `1 is set
C . (A1 `1) is Relation-like Function-like set
A1 `2 is set
(C . (A1 `1)) . (A1 `2) is set
[(A1 `1),((C . (A1 `1)) . (A1 `2))] is V15() set
{(A1 `1),((C . (A1 `1)) . (A1 `2))} is non empty finite set
{(A1 `1)} is non empty trivial finite 1 -element set
{{(A1 `1),((C . (A1 `1)) . (A1 `2))},{(A1 `1)}} is non empty finite finite-membered with_non-empty_elements non empty-membered set
[(A1 `1),(A1 `2)] is V15() set
{(A1 `1),(A1 `2)} is non empty finite set
{{(A1 `1),(A1 `2)},{(A1 `1)}} is non empty finite finite-membered with_non-empty_elements non empty-membered set
V .: {(A1 `1)} is set
XX . (A1 `1) is set

dom S is set
rng S is set
Im (V,(A1 `1)) is set
S . (A1 `2) is set
X is set
A1 is set
S is set
[A1,S] is V15() set
{A1,S} is non empty finite set
{A1} is non empty trivial finite 1 -element set
{{A1,S},{A1}} is non empty finite finite-membered with_non-empty_elements non empty-membered set

XX . A1 is set

dom CA is set
rng CA is set
F is set
CA . F is set
[A1,F] is V15() set
{A1,F} is non empty finite set
{{A1,F},{A1}} is non empty finite finite-membered with_non-empty_elements non empty-membered set
[A1,F] `1 is set
C . ([A1,F] `1) is Relation-like Function-like set
[A1,F] `2 is set
(C . ([A1,F] `1)) . ([A1,F] `2) is set
[([A1,F] `1),((C . ([A1,F] `1)) . ([A1,F] `2))] is V15() set
{([A1,F] `1),((C . ([A1,F] `1)) . ([A1,F] `2))} is non empty finite set
{([A1,F] `1)} is non empty trivial finite 1 -element set
{{([A1,F] `1),((C . ([A1,F] `1)) . ([A1,F] `2))},{([A1,F] `1)}} is non empty finite finite-membered with_non-empty_elements non empty-membered set
Im (V,A1) is set
F . [A1,F] is set
X is set
A1 is set
F . X is set
F . A1 is set
X `1 is set

X `2 is set
(C . (X `1)) . (X `2) is set
[(X `1),((C . (X `1)) . (X `2))] is V15() set
{(X `1),((C . (X `1)) . (X `2))} is non empty finite set
{(X `1)} is non empty trivial finite 1 -element set
{{(X `1),((C . (X `1)) . (X `2))},{(X `1)}} is non empty finite finite-membered with_non-empty_elements non empty-membered set
A1 `1 is set
C . (A1 `1) is Relation-like Function-like set
A1 `2 is set
(C . (A1 `1)) . (A1 `2) is set
[(A1 `1),((C . (A1 `1)) . (A1 `2))] is V15() set
{(A1 `1),((C . (A1 `1)) . (A1 `2))} is non empty finite set
{(A1 `1)} is non empty trivial finite 1 -element set
{{(A1 `1),((C . (A1 `1)) . (A1 `2))},{(A1 `1)}} is non empty finite finite-membered with_non-empty_elements non empty-membered set
[(X `1),(X `2)] is V15() set
{(X `1),(X `2)} is non empty finite set
{{(X `1),(X `2)},{(X `1)}} is non empty finite finite-membered with_non-empty_elements non empty-membered set
Im (V,(X `1)) is set
[(A1 `1),(A1 `2)] is V15() set
{(A1 `1),(A1 `2)} is non empty finite set
{{(A1 `1),(A1 `2)},{(A1 `1)}} is non empty finite finite-membered with_non-empty_elements non empty-membered set
Im (V,(A1 `1)) is set
XX . (A1 `1) is set

dom S is set
rng S is set
XX . (X `1) is set

dom CA is set
rng CA is set
CA . (X `2) is set
S . (A1 `2) is set

[:(card k),Aff:] is Relation-like set

X is set
A1 is set
S is set
[A1,S] is V15() set
{A1,S} is non empty finite set
{A1} is non empty trivial finite 1 -element set
{{A1,S},{A1}} is non empty finite finite-membered with_non-empty_elements non empty-membered set
((dom V) \ k) \/ k is set
(dom V) \/ k is set
(V | k) \/ (V | ((dom V) \ k)) is Relation-like set
V | (dom V) is Relation-like set
XX is set
Im (V,XX) is set
x is set
[XX,x] is V15() set
{XX,x} is non empty finite set
{XX} is non empty trivial finite 1 -element set
{{XX,x},{XX}} is non empty finite finite-membered with_non-empty_elements non empty-membered set

x is set
Im (V,x) is set

C is set
[x,C] is V15() set
{x,C} is non empty finite set
{x} is non empty trivial finite 1 -element set

k is set

V is non empty finite set

[:k,V:] is Relation-like set

(card V) - 1 is V21() V29() V30() ext-real finite Element of REAL

rng XX is finite Element of bool V

Aff is non empty finite set
[:Aff,V:] is Relation-like non empty finite set

dom XX is Element of bool k

C is set
{C} is non empty trivial finite 1 -element set
x " {C} is finite Element of bool Aff

C is set
{C} is non empty trivial finite 1 -element set
x " {C} is finite Element of bool Aff

C is set
{C} is non empty trivial finite 1 -element set
x " {C} is finite Element of bool Aff

(dom XX) \ (x " {C}) is Element of bool k
x | ((dom XX) \ (x " {C})) is Relation-like Aff -defined (dom XX) \ (x " {C}) -defined Aff -defined V -valued Function-like finite Element of bool [:Aff,V:]
XX " {C} is Element of bool k

dom (x | ((dom XX) \ (x " {C}))) is finite Element of bool Aff
card (dom (x | ((dom XX) \ (x " {C})))) is V21() epsilon-transitive epsilon-connected ordinal natural V29() V30() ext-real non negative finite cardinal Element of omega

(card Aff) - (card (x " {C})) is V21() V29() ext-real set
- (card (x " {C})) is V21() V29() ext-real non positive set
K87((card (x " {C}))) is V21() V29() V30() ext-real non positive finite set
(card Aff) + (- (card (x " {C}))) is V21() V29() ext-real set
K85((card Aff),(- (card (x " {C})))) is V21() V29() ext-real set
K89((card Aff),(card (x " {C}))) is V21() V29() V30() ext-real finite set
V \ {C} is finite Element of bool V
rng (x | ((dom XX) \ (x " {C}))) is finite Element of bool V
[:(dom (x | ((dom XX) \ (x " {C})))),(V \ {C}):] is Relation-like finite set
bool [:(dom (x | ((dom XX) \ (x " {C})))),(V \ {C}):] is non empty finite finite-membered V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(card V) + (- 1) is V21() V29() V30() ext-real finite Element of REAL
1 - (card (x " {C})) is V21() V29() V30() ext-real finite Element of REAL
(card V) + (1 - (card (x " {C}))) is V21() V29() V30() ext-real finite Element of REAL
1 - (- 1) is non empty V21() V29() V30() ext-real positive non negative finite Element of REAL
CA is set
{CA} is non empty trivial finite 1 -element set
XX " {CA} is Element of bool k

S is Relation-like dom (x | ((dom XX) \ (x " {C}))) -defined V \ {C} -valued Function-like quasi_total finite Element of bool [:(dom (x | ((dom XX) \ (x " {C})))),(V \ {C}):]
rng S is finite Element of bool (V \ {C})

S " {CA} is finite Element of bool (dom (x | ((dom XX) \ (x " {C}))))
bool (dom (x | ((dom XX) \ (x " {C})))) is non empty finite finite-membered V47() subset-closed non with_non-empty_elements V290() d.union-closed set
F is set
{F} is non empty trivial finite 1 -element set
k is 1-sorted
the carrier of k is set
V is SimplicialComplexStr of the carrier of k
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
Aff is Element of bool the carrier of V
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] V is non proper Element of bool the carrier of V
k is 1-sorted
the carrier of k is set
V is SimplicialComplexStr of the carrier of k
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
Aff is Element of bool (bool the carrier of V)
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] V is non proper Element of bool the carrier of V
bool ([#] V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool ([#] V))
bool ([#] V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool ([#] V)) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of k)
k is 1-sorted
the carrier of k is set
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
V is subset-closed SimplicialComplexStr of the carrier of k
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
Aff is finite Element of bool the carrier of V
(k,V,Aff) is Element of bool the carrier of k
{(k,V,Aff)} is non empty trivial finite 1 -element Element of bool (bool the carrier of k)
bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
Complex_of {(k,V,Aff)} is strict non void subset-closed non with_non-empty_elements total SimplicialComplexStr of the carrier of k
subset-closed_closure_of {(k,V,Aff)} is non empty V47() subset-closed non with_non-empty_elements Element of bool (bool the carrier of k)
TopStruct(# the carrier of k,(subset-closed_closure_of {(k,V,Aff)}) #) is strict TopStruct
the topology of V is Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
{Aff} is non empty trivial finite finite-membered 1 -element Element of bool (bool the carrier of V)
[#] (Complex_of {(k,V,Aff)}) is non proper Element of bool the carrier of (Complex_of {(k,V,Aff)})
the carrier of (Complex_of {(k,V,Aff)}) is set
bool the carrier of (Complex_of {(k,V,Aff)}) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] V is non proper Element of bool the carrier of V
the_family_of V is V47() subset-closed Element of bool (bool the carrier of V)
the topology of (Complex_of {(k,V,Aff)}) is Element of bool (bool the carrier of (Complex_of {(k,V,Aff)}))
bool (bool the carrier of (Complex_of {(k,V,Aff)})) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
k is non empty RLSStruct
the carrier of k is non empty set
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
V is SimplicialComplexStr of the carrier of k
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
{ (conv (k,V,b1)) where b1 is Element of bool the carrier of V : not b1 is dependent } is set
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of k)
bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
F is set
XX is Element of bool the carrier of V
(k,V,XX) is Element of bool the carrier of k
conv (k,V,XX) is convex Element of bool the carrier of k
F is Element of bool (bool the carrier of k)
union F is Element of bool the carrier of k
XX is Element of bool the carrier of k
x is set
C is set
F is Element of bool the carrier of V
(k,V,F) is Element of bool the carrier of k
conv (k,V,F) is convex Element of bool the carrier of k
X is Element of bool the carrier of V
(k,V,X) is Element of bool the carrier of k
conv (k,V,X) is convex Element of bool the carrier of k
C is Element of bool the carrier of V
(k,V,C) is Element of bool the carrier of k
conv (k,V,C) is convex Element of bool the carrier of k
Aff is Element of bool the carrier of k
F is Element of bool the carrier of k
XX is set
x is Element of bool the carrier of V
(k,V,x) is Element of bool the carrier of k
conv (k,V,x) is convex Element of bool the carrier of k
x is Element of bool the carrier of V
(k,V,x) is Element of bool the carrier of k
conv (k,V,x) is convex Element of bool the carrier of k
k is non empty RLSStruct
the carrier of k is non empty set
V is SimplicialComplexStr of the carrier of k
the topology of V is Element of bool (bool the carrier of V)
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(k,V) is Element of bool the carrier of k
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
Aff is SimplicialComplexStr of the carrier of k
the topology of Aff is Element of bool (bool the carrier of Aff)
the carrier of Aff is set
bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool the carrier of Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(k,Aff) is Element of bool the carrier of k
F is set
XX is Element of bool the carrier of V
(k,V,XX) is Element of bool the carrier of k
conv (k,V,XX) is convex Element of bool the carrier of k
x is Element of bool the carrier of Aff
(k,Aff,x) is Element of bool the carrier of k
k is non empty RLSStruct
the carrier of k is non empty set
V is SimplicialComplexStr of the carrier of k
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(k,V) is Element of bool the carrier of k
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
Aff is Element of bool the carrier of V
(k,V,Aff) is Element of bool the carrier of k
conv (k,V,Aff) is convex Element of bool the carrier of k
F is set
k is set

the carrier of V is non empty set
Aff is subset-closed SimplicialComplexStr of the carrier of V
(V,Aff) is Element of bool the carrier of V
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
the carrier of Aff is set
bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
F is Element of bool the carrier of Aff
(V,Aff,F) is Element of bool the carrier of V
conv (V,Aff,F) is convex Element of bool the carrier of V
{ (Int b1) where b1 is Element of bool the carrier of V : b1 c= (V,Aff,F) } is set
union { (Int b1) where b1 is Element of bool the carrier of V : b1 c= (V,Aff,F) } is set
XX is set
x is Element of bool the carrier of V
Int x is Element of bool the carrier of V
C is Element of bool the carrier of Aff
the topology of Aff is Element of bool (bool the carrier of Aff)
bool (bool the carrier of Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
F is Element of bool the carrier of Aff
(V,Aff,F) is Element of bool the carrier of V
Int (V,Aff,F) is Element of bool the carrier of V
F is Element of bool the carrier of Aff
(V,Aff,F) is Element of bool the carrier of V
Int (V,Aff,F) is Element of bool the carrier of V
conv (V,Aff,F) is convex Element of bool the carrier of V
k is non empty RLSStruct
the carrier of k is non empty set
V is SimplicialComplexStr of the carrier of k
(k,V) is Element of bool the carrier of k
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
the topology of V is Element of bool (bool the carrier of V)
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
Aff is non empty set
F is Element of bool the carrier of V
(k,V,F) is Element of bool the carrier of k
conv (k,V,F) is convex Element of bool the carrier of k
XX is set
Aff is set
F is Element of bool the carrier of V
(k,V,F) is Element of bool the carrier of k
conv (k,V,F) is convex Element of bool the carrier of k
k is non empty RLSStruct
the carrier of k is non empty set
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
V is Element of bool the carrier of k
{V} is non empty trivial finite 1 -element Element of bool (bool the carrier of k)
bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

subset-closed_closure_of {V} is non empty V47() subset-closed non with_non-empty_elements Element of bool (bool the carrier of k)
TopStruct(# the carrier of k, #) is strict TopStruct
(k,()) is Element of bool the carrier of k
conv V is convex Element of bool the carrier of k
the carrier of () is set
bool the carrier of () is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
the topology of () is Element of bool (bool the carrier of ())
bool (bool the carrier of ()) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool V)

bool (bool V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
XX is set
x is Element of bool the carrier of ()
(k,(),x) is Element of bool the carrier of k
conv (k,(),x) is convex Element of bool the carrier of k
F is Element of bool the carrier of ()
(k,(),F) is Element of bool the carrier of k
k is non empty RLSStruct
the carrier of k is non empty set
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
V is Element of bool (bool the carrier of k)
Aff is Element of bool (bool the carrier of k)
V \/ Aff is Element of bool (bool the carrier of k)
Complex_of (V \/ Aff) is strict subset-closed total SimplicialComplexStr of the carrier of k
subset-closed_closure_of (V \/ Aff) is V47() subset-closed Element of bool (bool the carrier of k)
TopStruct(# the carrier of k,(subset-closed_closure_of (V \/ Aff)) #) is strict TopStruct
(k,(Complex_of (V \/ Aff))) is Element of bool the carrier of k

subset-closed_closure_of V is V47() subset-closed Element of bool (bool the carrier of k)
TopStruct(# the carrier of k, #) is strict TopStruct
(k,()) is Element of bool the carrier of k

subset-closed_closure_of Aff is V47() subset-closed Element of bool (bool the carrier of k)
TopStruct(# the carrier of k,() #) is strict TopStruct
(k,(Complex_of Aff)) is Element of bool the carrier of k
(k,()) \/ (k,(Complex_of Aff)) is Element of bool the carrier of k
the topology of () is Element of bool (bool the carrier of ())
the carrier of () is set
bool the carrier of () is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool the carrier of ()) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
the topology of (Complex_of Aff) is Element of bool (bool the carrier of (Complex_of Aff))
the carrier of (Complex_of Aff) is set
bool the carrier of (Complex_of Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool the carrier of (Complex_of Aff)) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
the topology of () \/ the topology of (Complex_of Aff) is set
the topology of (Complex_of (V \/ Aff)) is Element of bool (bool the carrier of (Complex_of (V \/ Aff)))
the carrier of (Complex_of (V \/ Aff)) is set
bool the carrier of (Complex_of (V \/ Aff)) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool the carrier of (Complex_of (V \/ Aff))) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
C is set
F is Element of bool the carrier of (Complex_of (V \/ Aff))
(k,(Complex_of (V \/ Aff)),F) is Element of bool the carrier of k
conv (k,(Complex_of (V \/ Aff)),F) is convex Element of bool the carrier of k
X is Element of bool the carrier of ()
(k,(),X) is Element of bool the carrier of k
X is Element of bool the carrier of (Complex_of Aff)
(k,(Complex_of Aff),X) is Element of bool the carrier of k
k is non empty RLSStruct
the carrier of k is non empty set
V is SimplicialComplexStr of the carrier of k
(k,V) is Element of bool the carrier of k
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
Aff is Element of bool the carrier of V
(k,V,Aff) is Element of bool the carrier of k
conv (k,V,Aff) is convex Element of bool the carrier of k
k is non empty RLSStruct
the carrier of k is non empty set
V is SimplicialComplexStr of the carrier of k
(k,V) is Element of bool the carrier of k
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
Aff is (k,V)
(k,Aff) is Element of bool the carrier of k
F is set
the carrier of Aff is set
bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
XX is Element of bool the carrier of Aff
(k,Aff,XX) is Element of bool the carrier of k
conv (k,Aff,XX) is convex Element of bool the carrier of k
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
x is Element of bool the carrier of V
(k,V,x) is Element of bool the carrier of k
conv (k,V,x) is convex Element of bool the carrier of k
k is non empty RLSStruct
the carrier of k is non empty set
V is non void non empty-membered SimplicialComplexStr of the carrier of k
Aff is (k,V)
(k,V) is Element of bool the carrier of k
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(k,Aff) is Element of bool the carrier of k
k is non empty RLSStruct
the carrier of k is non empty set
V is SimplicialComplexStr of the carrier of k
(k,V) is Element of bool the carrier of k
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
Aff is Element of bool the carrier of V
(k,V,Aff) is Element of bool the carrier of k
conv (k,V,Aff) is convex Element of bool the carrier of k
k is non empty RLSStruct
the carrier of k is non empty set
V is SimplicialComplexStr of the carrier of k
the carrier of V is set
the topology of V is Element of bool (bool the carrier of V)
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
Complex_of the topology of V is strict subset-closed total SimplicialComplexStr of the carrier of V
subset-closed_closure_of the topology of V is V47() subset-closed Element of bool (bool the carrier of V)
TopStruct(# the carrier of V,() #) is strict TopStruct
[#] (Complex_of the topology of V) is non proper Element of bool the carrier of (Complex_of the topology of V)
the carrier of (Complex_of the topology of V) is set
bool the carrier of (Complex_of the topology of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] V is non proper Element of bool the carrier of V
(k,V) is Element of bool the carrier of k
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
XX is SimplicialComplexStr of the carrier of k
(k,XX) is Element of bool the carrier of k
x is set
C is Element of bool the carrier of V
(k,V,C) is Element of bool the carrier of k
conv (k,V,C) is convex Element of bool the carrier of k
the carrier of XX is set
bool the carrier of XX is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
the topology of XX is Element of bool (bool the carrier of XX)
bool (bool the carrier of XX) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
F is Element of bool the carrier of XX
(k,XX,F) is Element of bool the carrier of k
the carrier of XX is set
bool the carrier of XX is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
x is Element of bool the carrier of XX
(k,XX,x) is Element of bool the carrier of k
conv (k,XX,x) is convex Element of bool the carrier of k
the topology of XX is Element of bool (bool the carrier of XX)
bool (bool the carrier of XX) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
C is set
F is Element of bool the carrier of V
(k,V,F) is Element of bool the carrier of k
conv (k,V,F) is convex Element of bool the carrier of k

the carrier of k is non empty set
V is subset-closed SimplicialComplexStr of the carrier of k
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
the topology of V is Element of bool (bool the carrier of V)
Sub_of_Fin the topology of V is finite-membered Element of bool the topology of V
bool the topology of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
F is Element of bool (bool the carrier of V)

subset-closed_closure_of F is V47() subset-closed Element of bool (bool the carrier of V)
TopStruct(# the carrier of V, #) is strict TopStruct
[#] () is non proper Element of bool the carrier of ()
the carrier of () is set
bool the carrier of () is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] V is non proper Element of bool the carrier of V
the_family_of V is V47() subset-closed Element of bool (bool the carrier of V)
x is SimplicialComplexStr of the carrier of k
the topology of x is Element of bool (bool the carrier of x)
the carrier of x is set
bool the carrier of x is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool the carrier of x) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(k,V) is Element of bool the carrier of k
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(k,x) is Element of bool the carrier of k
C is set
F is Element of bool the carrier of V
(k,V,F) is Element of bool the carrier of k
conv (k,V,F) is convex Element of bool the carrier of k
X is non empty Element of bool the carrier of k

{ (Sum b1) where b1 is Relation-like the carrier of k -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of X : b1 in ConvexComb k } is set

Sum A1 is Element of the carrier of k
Carrier A1 is finite Element of bool the carrier of k
{ b1 where b1 is Element of the carrier of k : not A1 . b1 = 0 } is set
S is non empty Element of bool the carrier of k
CA is Element of bool the carrier of x

{ (Sum b1) where b1 is Relation-like the carrier of k -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of S : b1 in ConvexComb k } is set
conv S is non empty convex Element of bool the carrier of k
(k,x,CA) is Element of bool the carrier of k
C is Element of bool the carrier of x
(k,x,C) is Element of bool the carrier of k
conv (k,x,C) is convex Element of bool the carrier of k
F is Element of bool the carrier of V
(k,V,F) is Element of bool the carrier of k
k is non empty RLSStruct
the carrier of k is non empty set
V is SimplicialComplexStr of the carrier of k
Aff is (k,V)
F is (k,Aff)
(k,F) is Element of bool the carrier of k
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(k,Aff) is Element of bool the carrier of k
(k,V) is Element of bool the carrier of k
the carrier of F is set
bool the carrier of F is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
XX is Element of bool the carrier of F
(k,F,XX) is Element of bool the carrier of k
conv (k,F,XX) is convex Element of bool the carrier of k
the carrier of Aff is set
bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
x is Element of bool the carrier of Aff
(k,Aff,x) is Element of bool the carrier of k
conv (k,Aff,x) is convex Element of bool the carrier of k
C is Element of bool the carrier of V
(k,V,C) is Element of bool the carrier of k
conv (k,V,C) is convex Element of bool the carrier of k

the carrier of k is non empty set
V is SimplicialComplexStr of the carrier of k
the carrier of V is set
the topology of V is Element of bool (bool the carrier of V)
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
Complex_of the topology of V is strict subset-closed total SimplicialComplexStr of the carrier of V
subset-closed_closure_of the topology of V is V47() subset-closed Element of bool (bool the carrier of V)
TopStruct(# the carrier of V,() #) is strict TopStruct
Aff is (k,V)
the carrier of Aff is set
bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool (bool the carrier of Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
the topology of Aff is Element of bool (bool the carrier of Aff)
Sub_of_Fin the topology of Aff is finite-membered Element of bool the topology of Aff
bool the topology of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
F is Element of bool (bool the carrier of Aff)

subset-closed_closure_of F is V47() subset-closed Element of bool (bool the carrier of Aff)
TopStruct(# the carrier of Aff, #) is strict TopStruct
XX is (k,V)

the carrier of k is non empty set

the carrier of k is non empty set
BOOL the carrier of k is set
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of k)
bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(bool the carrier of k) \ is Element of bool (bool the carrier of k)
[:(BOOL the carrier of k), the carrier of k:] is Relation-like set
bool [:(BOOL the carrier of k), the carrier of k:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
V is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k
(k,V) is Element of bool the carrier of k
[#] V is non proper Element of bool the carrier of V
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
Aff is Relation-like BOOL the carrier of k -defined the carrier of k -valued Function-like quasi_total Element of bool [:(BOOL the carrier of k), the carrier of k:]
subdivision (Aff,V) is strict non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k
bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
the carrier of (subdivision (Aff,V)) is set
bool the carrier of (subdivision (Aff,V)) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
dom Aff is Element of bool (BOOL the carrier of k)
bool (BOOL the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

x is set
C is finite non dependent Element of bool the carrier of V
(k,V,C) is Element of bool the carrier of k
conv (k,V,C) is convex Element of bool the carrier of k

{C} is non empty trivial finite finite-membered 1 -element Element of bool (bool the carrier of V)
union {C} is finite Element of bool the carrier of V
X is Element of bool the carrier of V
F is non empty Element of bool the carrier of k
Aff . F is set
Aff . C is set
Aff .: {C} is finite Element of bool the carrier of k
Im (Aff,C) is set
X is Element of the carrier of k
{X} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k
conv F is non empty convex Element of bool the carrier of k
[#] (subdivision (Aff,V)) is non proper Element of bool the carrier of (subdivision (Aff,V))
S is set
CA is set
S is c=-linear finite finite-membered simplex-like Element of bool (bool the carrier of V)
Aff .: S is finite Element of bool the carrier of k
union S is finite Element of bool the carrier of V
A1 is Element of bool the carrier of (subdivision (Aff,V))
(k,(subdivision (Aff,V)),A1) is Element of bool the carrier of k
conv (k,(subdivision (Aff,V)),A1) is convex Element of bool the carrier of k
conv {X} is non empty convex Element of bool the carrier of k
S is Element of the carrier of k
CA is Element of the carrier of k
{S} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k
F \ {S} is Element of bool the carrier of k
conv (F \ {S}) is convex Element of bool the carrier of k
F is V21() V29() ext-real Element of REAL
F * X is Element of the carrier of k
1 - F is V21() V29() ext-real Element of REAL
(1 - F) * CA is Element of the carrier of k
(F * X) + ((1 - F) * CA) is Element of the carrier of k
C \ {S} is finite non dependent Element of bool the carrier of V
(k,V,(C \ {S})) is Element of bool the carrier of k

XX is Element of bool the carrier of (subdivision (Aff,V))
XX is c=-linear finite finite-membered simplex-like Element of bool (bool the carrier of V)
Aff .: XX is finite Element of bool the carrier of k
(k,(subdivision (Aff,V)),XX) is Element of bool the carrier of k
conv (k,(subdivision (Aff,V)),XX) is convex Element of bool the carrier of k
union XX is finite Element of bool the carrier of V
XX \/ {C} is non empty finite finite-membered Element of bool (bool the carrier of V)
XXA is set
m1 is set
XXA is c=-linear finite finite-membered simplex-like Element of bool (bool the carrier of V)
Aff .: XXA is finite Element of bool the carrier of k
A1 is Element of bool the carrier of (subdivision (Aff,V))
XX \/ A1 is Element of bool the carrier of (subdivision (Aff,V))
m1 is Element of bool the carrier of (subdivision (Aff,V))
(k,(subdivision (Aff,V)),m1) is Element of bool the carrier of k
conv (k,(subdivision (Aff,V)),m1) is convex Element of bool the carrier of k
union XXA is finite Element of bool the carrier of V
(union XX) \/ C is finite Element of bool the carrier of V
XX is set
x is finite non dependent Element of bool the carrier of V
(k,V,x) is Element of bool the carrier of k
conv (k,V,x) is convex Element of bool the carrier of k

(k,(subdivision (Aff,V))) is Element of bool the carrier of k
XX is set
x is Element of bool the carrier of V
(k,V,x) is Element of bool the carrier of k
conv (k,V,x) is convex Element of bool the carrier of k
C is finite non dependent Element of bool the carrier of V

F is set
X is finite non dependent Element of bool the carrier of V
(k,V,X) is Element of bool the carrier of k
conv (k,V,X) is convex Element of bool the carrier of k

X is Element of bool the carrier of (subdivision (Aff,V))
F is c=-linear finite finite-membered simplex-like Element of bool (bool the carrier of V)
Aff .: F is finite Element of bool the carrier of k
(k,(subdivision (Aff,V)),X) is Element of bool the carrier of k
conv (k,(subdivision (Aff,V)),X) is convex Element of bool the carrier of k
union F is finite Element of bool the carrier of V
XX is Element of bool the carrier of (subdivision (Aff,V))
(k,(subdivision (Aff,V)),XX) is Element of bool the carrier of k
conv (k,(subdivision (Aff,V)),XX) is convex Element of bool the carrier of k
x is c=-linear finite finite-membered simplex-like Element of bool (bool the carrier of V)
Aff .: x is finite Element of bool the carrier of k

(k,V,({} V)) is Element of bool the carrier of k
conv (k,V,({} V)) is convex Element of bool the carrier of k
union x is finite Element of bool the carrier of V
C is finite Element of bool the carrier of V
(k,V,C) is Element of bool the carrier of k
conv (k,V,C) is convex Element of bool the carrier of k
F is set
X is set
Aff . X is set
A1 is finite non dependent Element of bool the carrier of V
Aff . A1 is set
(k,V,A1) is Element of bool the carrier of k
conv (k,V,A1) is convex Element of bool the carrier of k
XX is Element of bool the carrier of (subdivision (Aff,V))
(k,(subdivision (Aff,V)),XX) is Element of bool the carrier of k
conv (k,(subdivision (Aff,V)),XX) is convex Element of bool the carrier of k

the carrier of k is non empty set
V is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k
Aff is subset-closed finite-membered (k,V)

the carrier of k is non empty set
V is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k
(k,V) is Element of bool the carrier of k
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] V is non proper Element of bool the carrier of V
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
center_of_mass k is Relation-like BOOL the carrier of k -defined the carrier of k -valued Function-like quasi_total Element of bool [:(BOOL the carrier of k), the carrier of k:]
BOOL the carrier of k is set
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of k)
bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(bool the carrier of k) \ is Element of bool (bool the carrier of k)
[:(BOOL the carrier of k), the carrier of k:] is Relation-like set
bool [:(BOOL the carrier of k), the carrier of k:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

F is finite non dependent Element of bool the carrier of V
() . F is set
(k,V,F) is Element of bool the carrier of k
conv (k,V,F) is convex Element of bool the carrier of k

the carrier of V is non empty set
Aff is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V
(V,Aff) is Element of bool the carrier of V
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] Aff is non proper Element of bool the carrier of Aff
the carrier of Aff is set
bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
center_of_mass V is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
BOOL the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(bool the carrier of V) \ is Element of bool (bool the carrier of V)
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

subdivision (k,(),Aff) is SimplicialComplexStr of the carrier of V

subdivision (F,(),Aff) is SimplicialComplexStr of the carrier of V

subdivision ((F + 1),(),Aff) is SimplicialComplexStr of the carrier of V
XX is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)
(V,XX) is Element of bool the carrier of V
[#] XX is non proper Element of bool the carrier of XX
the carrier of XX is set
bool the carrier of XX is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
subdivision (1,(),(subdivision (F,(),Aff))) is SimplicialComplexStr of the carrier of V

(V,XX) is non void subset-closed finite-membered non with_non-empty_elements (V,XX)
subdivision ({},(),Aff) is SimplicialComplexStr of the carrier of V

the carrier of k is non empty set
V is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k
(k,V) is Element of bool the carrier of k
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] V is non proper Element of bool the carrier of V
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
({},k,V) is non void subset-closed finite-membered non with_non-empty_elements (k,V)
center_of_mass k is Relation-like BOOL the carrier of k -defined the carrier of k -valued Function-like quasi_total Element of bool [:(BOOL the carrier of k), the carrier of k:]
BOOL the carrier of k is set
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of k)
bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(bool the carrier of k) \ is Element of bool (bool the carrier of k)
[:(BOOL the carrier of k), the carrier of k:] is Relation-like set
bool [:(BOOL the carrier of k), the carrier of k:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
subdivision ({},(),V) is SimplicialComplexStr of the carrier of k

the carrier of k is non empty set
V is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k
(k,V) is Element of bool the carrier of k
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] V is non proper Element of bool the carrier of V
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(1,k,V) is non void subset-closed finite-membered non with_non-empty_elements (k,V)
(k,V) is non void subset-closed finite-membered non with_non-empty_elements (k,V)
center_of_mass k is Relation-like BOOL the carrier of k -defined the carrier of k -valued Function-like quasi_total Element of bool [:(BOOL the carrier of k), the carrier of k:]
BOOL the carrier of k is set
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of k)
bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(bool the carrier of k) \ is Element of bool (bool the carrier of k)
[:(BOOL the carrier of k), the carrier of k:] is Relation-like set
bool [:(BOOL the carrier of k), the carrier of k:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
subdivision (1,(),V) is SimplicialComplexStr of the carrier of k

the carrier of V is non empty set
Aff is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V
(V,Aff) is Element of bool the carrier of V
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] Aff is non proper Element of bool the carrier of Aff
the carrier of Aff is set
bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(k,V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)
[#] (k,V,Aff) is non proper Element of bool the carrier of (k,V,Aff)
the carrier of (k,V,Aff) is set
bool the carrier of (k,V,Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
center_of_mass V is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
BOOL the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(bool the carrier of V) \ is Element of bool (bool the carrier of V)
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
subdivision (k,(),Aff) is SimplicialComplexStr of the carrier of V

the carrier of V is non empty set
Aff is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V
(V,Aff) is Element of bool the carrier of V
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] Aff is non proper Element of bool the carrier of Aff
the carrier of Aff is set
bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(k,V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)
(V,(k,V,Aff)) is Element of bool the carrier of V

the carrier of V is non empty set
Aff is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V
(V,Aff) is Element of bool the carrier of V
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] Aff is non proper Element of bool the carrier of Aff
the carrier of Aff is set
bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
((k + 1),V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)
(k,V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)
(V,(k,V,Aff)) is non void subset-closed finite-membered non with_non-empty_elements (V,(k,V,Aff))
(V,(k,V,Aff)) is Element of bool the carrier of V
[#] (k,V,Aff) is non proper Element of bool the carrier of (k,V,Aff)
the carrier of (k,V,Aff) is set
bool the carrier of (k,V,Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
center_of_mass V is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
BOOL the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(bool the carrier of V) \ is Element of bool (bool the carrier of V)
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

subdivision ((1 + k),(),Aff) is SimplicialComplexStr of the carrier of V
subdivision (k,(),Aff) is SimplicialComplexStr of the carrier of V
subdivision (1,(),(subdivision (k,(),Aff))) is SimplicialComplexStr of the carrier of V
subdivision (1,(),(k,V,Aff)) is SimplicialComplexStr of the carrier of V
(1,V,(k,V,Aff)) is non void subset-closed finite-membered non with_non-empty_elements (V,(k,V,Aff))

the carrier of k is non empty set
V is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of k
(k,V) is Element of bool the carrier of k
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] V is non proper Element of bool the carrier of V
the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

the topology of V is Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
TopStruct(# the carrier of V, the topology of V #) is strict TopStruct
(k,V) is non void subset-closed finite-membered non with_non-empty_elements (k,V)
center_of_mass k is Relation-like BOOL the carrier of k -defined the carrier of k -valued Function-like quasi_total Element of bool [:(BOOL the carrier of k), the carrier of k:]
BOOL the carrier of k is set
bool the carrier of k is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of k)
bool (bool the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(bool the carrier of k) \ is Element of bool (bool the carrier of k)
[:(BOOL the carrier of k), the carrier of k:] is Relation-like set
bool [:(BOOL the carrier of k), the carrier of k:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

[#] (k,V) is non proper Element of bool the carrier of (k,V)
the carrier of (k,V) is set
bool the carrier of (k,V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
dom () is Element of bool (BOOL the carrier of k)
bool (BOOL the carrier of k) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
Aff is ext-real set
{} + Aff is ext-real set

() + Aff is ext-real set
the topology of (k,V) is Element of bool (bool the carrier of (k,V))
bool (bool the carrier of (k,V)) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
x is set
C is finite non dependent Element of bool the carrier of (k,V)
X is c=-linear finite finite-membered simplex-like Element of bool (bool the carrier of V)
() .: X is finite Element of bool the carrier of k
X /\ () is finite Element of bool (BOOL the carrier of k)
() .: (X /\ ()) is finite Element of bool the carrier of k
F is Element of bool the carrier of V
union X is finite Element of bool the carrier of V
A1 is finite non dependent Element of bool the carrier of V
S is set
(k,V,A1) is Element of bool the carrier of k

() + 1 is ext-real set
S is set
{S} is non empty trivial finite 1 -element set
{A1} is non empty trivial finite finite-membered 1 -element Element of bool (bool the carrier of V)
F is set
Im ((),A1) is set
() . A1 is set
{(() . A1)} is non empty trivial finite 1 -element set
CA is Element of the carrier of k
{CA} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k
Sum {CA} is Element of the carrier of k
1 / 1 is non empty V21() V29() ext-real positive non negative Element of REAL
(1 / 1) * (Sum {CA}) is Element of the carrier of k
{((1 / 1) * (Sum {CA}))} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k
{(Sum {CA})} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k
x is set
C is finite non dependent Element of bool the carrier of V
F is Element of bool the carrier of (k,V)
{C} is non empty trivial finite finite-membered 1 -element Element of bool (bool the carrier of V)
X is Element of bool the carrier of V
A1 is set
X is finite finite-membered simplex-like Element of bool (bool the carrier of V)
S is set

() + 1 is ext-real set
(k,V,C) is Element of bool the carrier of k
A1 is set
{A1} is non empty trivial finite 1 -element set
() .: X is finite Element of bool the carrier of k
Im ((),C) is set
() . C is set
{(() . C)} is non empty trivial finite 1 -element set
S is Element of the carrier of k
{S} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k
Sum {S} is Element of the carrier of k
1 / 1 is non empty V21() V29() ext-real positive non negative Element of REAL
(1 / 1) * () is Element of the carrier of k
{((1 / 1) * ())} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k
{()} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of k
F is Element of bool the carrier of (k,V)

the carrier of V is non empty set
Aff is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V
(V,Aff) is Element of bool the carrier of V
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] Aff is non proper Element of bool the carrier of Aff
the carrier of Aff is set
bool the carrier of Aff is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
degree Aff is ext-real set
the topology of Aff is Element of bool (bool the carrier of Aff)
bool (bool the carrier of Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
TopStruct(# the carrier of Aff, the topology of Aff #) is strict TopStruct
(k,V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)
BOOL the carrier of V is set
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(bool the carrier of V) \ is Element of bool (bool the carrier of V)
center_of_mass V is Relation-like BOOL the carrier of V -defined the carrier of V -valued Function-like quasi_total Element of bool [:(BOOL the carrier of V), the carrier of V:]
[:(BOOL the carrier of V), the carrier of V:] is Relation-like set
bool [:(BOOL the carrier of V), the carrier of V:] is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
dom () is Element of bool (BOOL the carrier of V)
bool (BOOL the carrier of V) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set

(F,V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)
degree (F,V,Aff) is ext-real set

((F + 1),V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)
degree ((F + 1),V,Aff) is ext-real set
subdivision ((),Aff) is strict non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V
degree (subdivision ((),Aff)) is ext-real set
(V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)
(V,(F,V,Aff)) is Element of bool the carrier of V
[#] (F,V,Aff) is non proper Element of bool the carrier of (F,V,Aff)
the carrier of (F,V,Aff) is set
bool the carrier of (F,V,Aff) is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
(V,(F,V,Aff)) is non void subset-closed finite-membered non with_non-empty_elements (V,(F,V,Aff))
({},V,Aff) is non void subset-closed finite-membered non with_non-empty_elements (V,Aff)
degree ({},V,Aff) is ext-real set

the carrier of V is non empty set
Aff is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of V
(V,Aff) is Element of bool the carrier of V
bool the carrier of V is non empty V47() subset-closed non with_non-empty_elements V290() d.union-closed set
[#] Aff is non proper Element of bool the carrier of Aff
the carrier of Aff is set
bool the carrier of Aff is non empt