:: SIMPLEX2 semantic presentation

REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V109() non bounded_below non bounded_above interval set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() left_end bounded_below Element of bool REAL
bool REAL is non empty non trivial non finite set
1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT
- 1 is non empty real V55() ext-real non positive negative set
K165(1) is real integer finite V55() ext-real non positive set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() left_end bounded_below set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite complex-membered V109() set
RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V109() set
INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V109() set
[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like non finite V93() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial Relation-like non finite V93() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:REAL,REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:REAL,REAL:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is non empty non trivial Relation-like RAT -valued non finite V93() V94() V95() set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is non empty non trivial Relation-like RAT -valued non finite V93() V94() V95() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite V93() V94() V95() set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite V93() V94() V95() set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite V93() V94() V95() V96() set
[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite V93() V94() V95() V96() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() ext-real non positive non negative V93() V94() V95() V96() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() bounded_below bounded_above real-bounded interval subset-closed set
2 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT
[:1,1:] is non empty Relation-like RAT -valued INT -valued finite V93() V94() V95() V96() set
bool [:1,1:] is non empty finite finite-membered set
[:[:1,1:],1:] is non empty Relation-like RAT -valued INT -valued finite V93() V94() V95() V96() set
bool [:[:1,1:],1:] is non empty finite finite-membered set
[:[:1,1:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[:1,1:],REAL:] is non empty non trivial non finite set
[:2,2:] is non empty Relation-like RAT -valued INT -valued finite V93() V94() V95() V96() set
[:[:2,2:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[:2,2:],REAL:] is non empty non trivial non finite set
TOP-REAL 2 is non empty TopSpace-like V126() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict V191() V192() V221() V222() finite-dimensional with_finite_small_inductive_dimension L15()
the carrier of (TOP-REAL 2) is non empty set
K523() is non empty V128() L9()
the carrier of K523() is non empty set
K528() is non empty V128() V201() V202() V203() V205() V231() V232() V233() V234() V235() V236() L9()
K529() is non empty V128() V203() V205() V234() V235() V236() M21(K528())
K530() is non empty V128() V201() V203() V205() V234() V235() V236() V237() M24(K528(),K529())
K532() is non empty V128() V201() V203() V205() L9()
K533() is non empty V128() V201() V203() V205() V237() M21(K532())
ExtREAL is non empty ext-real-membered interval set
[:NAT,REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:NAT,REAL:] is non empty non trivial non finite set
K743() is non empty strict TopSpace-like T_0 T_1 T_2 compact real-membered TopStruct
the carrier of K743() is non empty complex-membered ext-real-membered real-membered set
RealSpace is strict real-membered MetrStruct
real_dist is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:REAL,REAL:],REAL:]
MetrStruct(# REAL,real_dist #) is strict MetrStruct
R^1 is non empty strict TopSpace-like real-membered TopStruct
the carrier of R^1 is non empty complex-membered ext-real-membered real-membered set
[:COMPLEX,REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:COMPLEX,REAL:] is non empty non trivial non finite set
K844() is set
{{}} is non empty trivial functional finite finite-membered 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set
{{}} * is non empty functional FinSequence-membered FinSequenceSet of {{}}
[:({{}} *),{{}}:] is non empty Relation-like RAT -valued INT -valued V93() V94() V95() V96() set
bool [:({{}} *),{{}}:] is non empty set
PFuncs (({{}} *),{{}}) is set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() V56() ext-real non positive non negative V93() V94() V95() V96() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() bounded_below bounded_above real-bounded interval subset-closed Element of NAT
Euclid 0 is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct
REAL 0 is non empty functional FinSequence-membered FinSequenceSet of REAL
0 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist 0 is non empty Relation-like [:(REAL 0),(REAL 0):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL 0),(REAL 0):],REAL:]
[:(REAL 0),(REAL 0):] is non empty Relation-like set
[:[:(REAL 0),(REAL 0):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[:(REAL 0),(REAL 0):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL 0),(Pitag_dist 0) #) is strict MetrStruct
TopSpaceMetr (Euclid 0) is non empty trivial finite 1 -element strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 compact metrizable TopStruct
the carrier of (Euclid 0) is non empty set
Family_open_set (Euclid 0) is Element of bool (bool the carrier of (Euclid 0))
bool the carrier of (Euclid 0) is non empty set
bool (bool the carrier of (Euclid 0)) is non empty set
TopStruct(# the carrier of (Euclid 0),(Family_open_set (Euclid 0)) #) is non empty strict TopStruct
3 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT
bool the carrier of R^1 is non empty set
-infty is non empty non real ext-real non positive negative set
TOP-REAL 1 is non empty TopSpace-like V126() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict V191() V192() V221() V222() finite-dimensional with_finite_small_inductive_dimension L15()
the carrier of (TOP-REAL 1) is non empty set
[: the carrier of (TOP-REAL 1), the carrier of R^1:] is non empty Relation-like V93() V94() V95() set
bool [: the carrier of (TOP-REAL 1), the carrier of R^1:] is non empty set
+infty is non empty non real ext-real positive non negative set
union {} is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
n is non empty Reflexive discerning V181() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
the carrier of n is non empty set
Family_open_set n is Element of bool (bool the carrier of n)
bool the carrier of n is non empty set
bool (bool the carrier of n) is non empty set
TopStruct(# the carrier of n,(Family_open_set n) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr n) is non empty set
bool the carrier of (TopSpaceMetr n) is non empty set
bool (bool the carrier of (TopSpaceMetr n)) is non empty set
T is Element of bool (bool the carrier of (TopSpaceMetr n))
C is Element of bool (bool the carrier of (TopSpaceMetr n))
[#] (TopSpaceMetr n) is non empty non proper open closed Element of bool the carrier of (TopSpaceMetr n)
E is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of NAT
C is Element of the carrier of n
Ball (C,E) is bounded Element of bool the carrier of n
[#] (TopSpaceMetr n) is non empty non proper open closed Element of bool the carrier of (TopSpaceMetr n)
Funcs (([#] (TopSpaceMetr n)),REAL) is non empty functional FUNCTION_DOMAIN of [#] (TopSpaceMetr n), REAL
n1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng n1 is finite set
[: the carrier of (TopSpaceMetr n), the carrier of R^1:] is non empty Relation-like V93() V94() V95() set
bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:] is non empty set
union C is Element of bool the carrier of (TopSpaceMetr n)
len n1 is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
dom n1 is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
n1 . 1 is set
c is Element of bool the carrier of (TopSpaceMetr n)
c ` is Element of bool the carrier of (TopSpaceMetr n)
the carrier of (TopSpaceMetr n) \ c is set
(c `) ` is Element of bool the carrier of (TopSpaceMetr n)
the carrier of (TopSpaceMetr n) \ (c `) is set
TRC is non empty closed Element of bool the carrier of (TopSpaceMetr n)
dist_min TRC is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
f is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
n1 . (f + 1) is set
R is Relation-like [#] (TopSpaceMetr n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of Funcs (([#] (TopSpaceMetr n)),REAL)
G is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
G0 is Relation-like [#] (TopSpaceMetr n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of Funcs (([#] (TopSpaceMetr n)),REAL)
p is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
h is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
G is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
G0 is Element of bool the carrier of (TopSpaceMetr n)
G0 ` is Element of bool the carrier of (TopSpaceMetr n)
the carrier of (TopSpaceMetr n) \ G0 is set
(G0 `) ` is Element of bool the carrier of (TopSpaceMetr n)
the carrier of (TopSpaceMetr n) \ (G0 `) is set
p is non empty Element of bool the carrier of (TopSpaceMetr n)
dist_min p is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
h is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
h is Relation-like [#] (TopSpaceMetr n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of Funcs (([#] (TopSpaceMetr n)),REAL)
gx is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
cgx is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
p ` is Element of bool the carrier of (TopSpaceMetr n)
the carrier of (TopSpaceMetr n) \ p is set
GX is Element of the carrier of (TopSpaceMetr n)
cgx . GX is real V55() ext-real Element of the carrier of R^1
gx . GX is real V55() ext-real Element of the carrier of R^1
(dist_min p) . GX is real V55() ext-real Element of the carrier of R^1
max ((gx . GX),((dist_min p) . GX)) is real V55() ext-real set
G is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
carr is Relation-like [#] (TopSpaceMetr n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of Funcs (([#] (TopSpaceMetr n)),REAL)
f is Relation-like NAT -defined Funcs (([#] (TopSpaceMetr n)),REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs (([#] (TopSpaceMetr n)),REAL)
len f is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
f /. 1 is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)
dom f is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
f /. (len f) is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)
R is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
rng R is non empty complex-membered ext-real-membered real-membered Element of bool REAL
G is complex-membered ext-real-membered real-membered Element of bool the carrier of R^1
[#] G is complex-membered ext-real-membered real-membered Element of bool REAL
p is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
f /. p is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)
p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
f /. (p + 1) is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)
h is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
h is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
f /. h is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)
gx is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
cgx is Element of the carrier of (TopSpaceMetr n)
gx . cgx is real V55() ext-real Element of the carrier of R^1
h . cgx is real V55() ext-real Element of the carrier of R^1
p - 1 is real integer finite V55() ext-real Element of REAL
K163(p,K165(1)) is real integer finite V55() ext-real set
h is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
h + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
gx is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
n1 . (p + 1) is set
cgx is non empty Element of bool the carrier of (TopSpaceMetr n)
cgx ` is Element of bool the carrier of (TopSpaceMetr n)
the carrier of (TopSpaceMetr n) \ cgx is set
dist_min cgx is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
GX is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
f /. GX is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)
I is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
t is Element of the carrier of (TopSpaceMetr n)
I . t is real V55() ext-real Element of the carrier of R^1
h . t is real V55() ext-real Element of the carrier of R^1
gx . t is real V55() ext-real Element of the carrier of R^1
(dist_min cgx) . t is real V55() ext-real Element of the carrier of R^1
max ((gx . t),((dist_min cgx) . t)) is real V55() ext-real set
f /. {} is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)
p is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
h is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
h is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
f /. h is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)
gx is Element of the carrier of (TopSpaceMetr n)
h . gx is real V55() ext-real Element of the carrier of R^1
p . gx is real V55() ext-real Element of the carrier of R^1
dom R is non empty Element of bool the carrier of (TopSpaceMetr n)
R .: ([#] (TopSpaceMetr n)) is complex-membered ext-real-membered real-membered Element of bool the carrier of R^1
p is non empty complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded Element of bool REAL
lower_bound p is real V55() ext-real Element of REAL
inf p is real V55() ext-real set
h is set
R . h is real V55() ext-real set
gx is set
GX is set
n1 . GX is set
I is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
cgx is Element of the carrier of (TopSpaceMetr n)
(dist_min TRC) . cgx is real V55() ext-real Element of the carrier of R^1
I - 1 is real integer finite V55() ext-real Element of REAL
K163(I,K165(1)) is real integer finite V55() ext-real set
t is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
f /. t is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)
f /. I is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)
t + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
y is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
x is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
t + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
n1 . (t + 1) is set
i1 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
i2 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
n1 . I is set
i1 is non empty Element of bool the carrier of (TopSpaceMetr n)
i1 ` is Element of bool the carrier of (TopSpaceMetr n)
the carrier of (TopSpaceMetr n) \ i1 is set
dist_min i1 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
cgx is Element of the carrier of (TopSpaceMetr n)
(dist_min i1) . cgx is real V55() ext-real Element of the carrier of R^1
x . cgx is real V55() ext-real Element of the carrier of R^1
y . cgx is real V55() ext-real Element of the carrier of R^1
max ((y . cgx),((dist_min i1) . cgx)) is real V55() ext-real set
t is non empty real V55() ext-real positive non negative Element of REAL
y is Element of the carrier of n
Ball (y,t) is bounded Element of bool the carrier of n
R . y is real V55() ext-real set
x is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
x . y is real V55() ext-real set
x is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
f /. x is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)
i1 is set
i2 is Element of the carrier of n
dist (y,i2) is real V55() ext-real non negative Element of REAL
the distance of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of n, the carrier of n:],REAL:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
[:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial non finite set
the distance of n . (y,i2) is real V55() ext-real Element of REAL
(dist_min TRC) . y is real V55() ext-real set
x - 1 is real integer finite V55() ext-real Element of REAL
K163(x,K165(1)) is real integer finite V55() ext-real set
i1 is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of NAT
f /. i1 is Relation-like Function-like Element of Funcs (([#] (TopSpaceMetr n)),REAL)
i1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
i2 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
S2 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
i1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
n1 . (i1 + 1) is set
bb1 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
bb2 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
n1 . x is set
bb1 is non empty Element of bool the carrier of (TopSpaceMetr n)
bb1 ` is Element of bool the carrier of (TopSpaceMetr n)
the carrier of (TopSpaceMetr n) \ bb1 is set
dist_min bb1 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
bb2 is set
r is Element of the carrier of n
(dist_min bb1) . y is real V55() ext-real set
dist (y,r) is real V55() ext-real non negative Element of REAL
the distance of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of n, the carrier of n:],REAL:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
[:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial non finite set
the distance of n . (y,r) is real V55() ext-real Element of REAL
S2 . y is real V55() ext-real set
i2 . y is real V55() ext-real set
max ((i2 . y),((dist_min bb1) . y)) is real V55() ext-real set
r1 is non empty Relation-like the carrier of (TopSpaceMetr n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TopSpaceMetr n), the carrier of R^1:]
r1 . y is real V55() ext-real set
[#] (TopSpaceMetr n) is non empty non proper open closed Element of bool the carrier of (TopSpaceMetr n)
n is non empty Reflexive discerning V181() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
the carrier of n is non empty set
Family_open_set n is Element of bool (bool the carrier of n)
bool the carrier of n is non empty set
bool (bool the carrier of n) is non empty set
TopStruct(# the carrier of n,(Family_open_set n) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr n) is non empty set
bool the carrier of (TopSpaceMetr n) is non empty set
bool (bool the carrier of (TopSpaceMetr n)) is non empty set
T is open Element of bool (bool the carrier of (TopSpaceMetr n))
I is open Element of bool (bool the carrier of (TopSpaceMetr n))
C is non empty real V55() ext-real positive non negative (n,T)
E is Element of the carrier of n
Ball (E,C) is bounded Element of bool the carrier of n
C is Element of bool the carrier of (TopSpaceMetr n)
union T is Element of bool the carrier of (TopSpaceMetr n)
[#] (TopSpaceMetr n) is non empty non proper open closed Element of bool the carrier of (TopSpaceMetr n)
union I is Element of bool the carrier of (TopSpaceMetr n)
n is non empty Reflexive discerning V181() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
the carrier of n is non empty set
Family_open_set n is Element of bool (bool the carrier of n)
bool the carrier of n is non empty set
bool (bool the carrier of n) is non empty set
TopStruct(# the carrier of n,(Family_open_set n) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr n) is non empty set
bool the carrier of (TopSpaceMetr n) is non empty set
bool (bool the carrier of (TopSpaceMetr n)) is non empty set
T is open Element of bool (bool the carrier of (TopSpaceMetr n))
I is open Element of bool (bool the carrier of (TopSpaceMetr n))
C is non empty real V55() ext-real positive non negative (n,T)
C is Element of the carrier of n
Ball (C,C) is bounded Element of bool the carrier of n
n1 is Element of bool the carrier of (TopSpaceMetr n)
c is set
TRC is Element of bool the carrier of (TopSpaceMetr n)
carr is Element of bool the carrier of (TopSpaceMetr n)
union T is Element of bool the carrier of (TopSpaceMetr n)
[#] (TopSpaceMetr n) is non empty non proper open closed Element of bool the carrier of (TopSpaceMetr n)
union I is Element of bool the carrier of (TopSpaceMetr n)
n is non empty Reflexive discerning V181() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
the carrier of n is non empty set
Family_open_set n is Element of bool (bool the carrier of n)
bool the carrier of n is non empty set
bool (bool the carrier of n) is non empty set
TopStruct(# the carrier of n,(Family_open_set n) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr n) is non empty set
bool the carrier of (TopSpaceMetr n) is non empty set
bool (bool the carrier of (TopSpaceMetr n)) is non empty set
T is open Element of bool (bool the carrier of (TopSpaceMetr n))
I is non empty real V55() ext-real positive non negative (n,T)
C is non empty real V55() ext-real positive non negative Element of REAL
E is Element of the carrier of n
Ball (E,I) is bounded Element of bool the carrier of n
C is Element of bool the carrier of (TopSpaceMetr n)
Ball (E,C) is bounded Element of bool the carrier of n
n1 is Element of bool the carrier of (TopSpaceMetr n)
n is non empty Reflexive MetrStruct
the carrier of n is non empty set
bool the carrier of n is non empty set
T is Element of bool the carrier of n
I is non empty finite Element of bool the carrier of n
C is set
{ H₁(b₁,b₂) where b₁, b₂ is Element of the carrier of n : ( b₁ in I & b₂ in I ) } is set
C is Element of the carrier of n
dist (C,C) is real V55() ext-real Element of REAL
the distance of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of n, the carrier of n:],REAL:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
[:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial non finite set
the distance of n . (C,C) is real V55() ext-real Element of REAL
n1 is set
c is Element of the carrier of n
TRC is Element of the carrier of n
dist (c,TRC) is real V55() ext-real Element of REAL
the distance of n . (c,TRC) is real V55() ext-real Element of REAL
n1 is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
sup n1 is real V55() ext-real set
c is real V55() ext-real Element of REAL
c + 1 is real V55() ext-real Element of REAL
TRC is real V55() ext-real Element of REAL
carr is Element of the carrier of n
f is Element of the carrier of n
dist (carr,f) is real V55() ext-real Element of REAL
the distance of n . (carr,f) is real V55() ext-real Element of REAL
n is non empty Reflexive MetrStruct
the carrier of n is non empty set
bool the carrier of n is non empty set
T is non empty finite bounded Element of bool the carrier of n
diameter T is real V55() ext-real Element of REAL
the Element of T is Element of T
{ H₁(b₁,b₂) where b₁, b₂ is Element of the carrier of n : ( b₁ in T & b₂ in T ) } is set
C is set
n1 is Element of the carrier of n
c is Element of the carrier of n
dist (n1,c) is real V55() ext-real Element of REAL
the distance of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of n, the carrier of n:],REAL:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
[:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial non finite set
the distance of n . (n1,c) is real V55() ext-real Element of REAL
C is Element of the carrier of n
dist (C,C) is real V55() ext-real Element of REAL
the distance of n is non empty Relation-like [: the carrier of n, the carrier of n:] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of n, the carrier of n:],REAL:]
[: the carrier of n, the carrier of n:] is non empty Relation-like set
[:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[: the carrier of n, the carrier of n:],REAL:] is non empty non trivial non finite set
the distance of n . (C,C) is real V55() ext-real Element of REAL
C is non empty finite complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
sup C is real V55() ext-real set
n1 is real V55() ext-real Element of REAL
c is Element of the carrier of n
TRC is Element of the carrier of n
dist (c,TRC) is real V55() ext-real Element of REAL
the distance of n . (c,TRC) is real V55() ext-real Element of REAL
carr is Element of the carrier of n
f is Element of the carrier of n
dist (carr,f) is real V55() ext-real Element of REAL
the distance of n . (carr,f) is real V55() ext-real Element of REAL
n is non empty Reflexive MetrStruct
the carrier of n is non empty set
bool the carrier of n is non empty set
T is Element of bool the carrier of n
I is non void TopStruct
the carrier of I is set
bool the carrier of I is non empty set
the topology of I is open Element of bool (bool the carrier of I)
bool (bool the carrier of I) is non empty set
C is real V55() ext-real set
T is set
n is non empty Reflexive MetrStruct
the carrier of n is non empty set
the Element of the carrier of n is Element of the carrier of n
bool T is non empty set
{} T is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() ext-real non positive non negative V93() V94() V95() V96() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() bounded_below bounded_above real-bounded interval subset-closed Element of bool T
{({} T)} is non empty trivial functional finite finite-membered 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded V365(T) Element of bool (bool T)
bool (bool T) is non empty set
Complex_of {({} T)} is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements total SimplicialComplexStr of T
subset-closed_closure_of {({} T)} is non empty finite-membered non with_non-empty_elements subset-closed Element of bool (bool T)
TopStruct(# T,(subset-closed_closure_of {({} T)}) #) is strict TopStruct
C is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements total SimplicialComplexStr of T
{} n is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() ext-real non positive non negative V93() V94() V95() V96() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() bounded_below bounded_above real-bounded interval subset-closed bounded Element of bool the carrier of n
bool the carrier of n is non empty set
diameter ({} n) is real V55() ext-real Element of REAL
the topology of C is finite finite-membered V365( the carrier of C) open Element of bool (bool the carrier of C)
the carrier of C is set
bool the carrier of C is non empty set
bool (bool the carrier of C) is non empty set
E is real V55() ext-real Element of REAL
C is Element of bool the carrier of n
diameter C is real V55() ext-real Element of REAL
bool ({} T) is non empty finite finite-membered V365( {} T) Element of bool (bool ({} T))
bool ({} T) is non empty finite finite-membered set
bool (bool ({} T)) is non empty finite finite-membered set
n is non empty Reflexive MetrStruct
the set is set
the non void subset-closed finite-membered non with_non-empty_elements (n) SimplicialComplexStr of the set is non void subset-closed finite-membered non with_non-empty_elements (n) SimplicialComplexStr of the set
n is non empty Reflexive MetrStruct
T is set
I is (n) SimplicialComplexStr of T
C is subset-closed finite-membered SubSimplicialComplex of I
the topology of C is finite-membered open Element of bool (bool the carrier of C)
the carrier of C is set
bool the carrier of C is non empty set
bool (bool the carrier of C) is non empty set
the topology of I is open Element of bool (bool the carrier of I)
the carrier of I is set
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
the carrier of n is non empty set
bool the carrier of n is non empty set
E is real V55() ext-real set
C is Element of bool the carrier of n
diameter C is real V55() ext-real Element of REAL
n is non empty Reflexive MetrStruct
T is set
I is subset-closed (n) SimplicialComplexStr of T
C is real integer finite V55() ext-real set
Skeleton_of (I,C) is subset-closed finite-membered finite-degree (n) SubSimplicialComplex of I
the carrier of I is set
the topology of I is open Element of bool (bool the carrier of I)
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
C + 1 is real V55() ext-real set
K163(C,1) is real integer finite V55() ext-real set
the_subsets_with_limited_card ((C + 1), the topology of I, the carrier of I) is Element of bool (bool the carrier of I)
Complex_of (the_subsets_with_limited_card ((C + 1), the topology of I, the carrier of I)) is strict subset-closed total SimplicialComplexStr of the carrier of I
subset-closed_closure_of (the_subsets_with_limited_card ((C + 1), the topology of I, the carrier of I)) is subset-closed Element of bool (bool the carrier of I)
TopStruct(# the carrier of I,(subset-closed_closure_of (the_subsets_with_limited_card ((C + 1), the topology of I, the carrier of I))) #) is strict TopStruct
n is non empty Reflexive MetrStruct
T is TopStruct
Vertices T is Element of bool the carrier of T
the carrier of T is set
bool the carrier of T is non empty set
the carrier of n is non empty set
bool the carrier of n is non empty set
[#] n is non empty non proper Element of bool the carrier of n
(Vertices T) /\ ([#] n) is Element of bool the carrier of n
C is finite bounded Element of bool the carrier of n
diameter C is real V55() ext-real Element of REAL
the topology of T is open Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
E is Element of bool the carrier of n
diameter E is real V55() ext-real Element of REAL
C is Element of bool the carrier of T
n is non empty Reflexive MetrStruct
T is TopStruct
the topology of T is open Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[#] n is non empty non proper Element of bool the carrier of n
the carrier of n is non empty set
bool the carrier of n is non empty set
bool ([#] n) is non empty Element of bool (bool ([#] n))
bool ([#] n) is non empty set
bool (bool ([#] n)) is non empty set
{ H₁(b₁) where b₁ is Element of bool the carrier of n : S₁[b₁] } is set
C is set
E is Element of bool the carrier of n
diameter E is real V55() ext-real Element of REAL
E is set
n1 is real V55() ext-real set
c is ext-real set
C is complex-membered ext-real-membered real-membered set
TRC is Element of bool the carrier of n
diameter TRC is real V55() ext-real Element of REAL
C is Element of bool the carrier of n
diameter C is real V55() ext-real Element of REAL
sup C is ext-real set
c is real V55() ext-real Element of REAL
TRC is Element of bool the carrier of n
diameter TRC is real V55() ext-real Element of REAL
TRC is real V55() ext-real set
carr is ext-real set
f is Element of bool the carrier of n
diameter f is real V55() ext-real Element of REAL
I is real V55() ext-real Element of REAL
I is real V55() ext-real Element of REAL
C is real V55() ext-real Element of REAL
I is real V55() ext-real Element of REAL
C is real V55() ext-real Element of REAL
E is real V55() ext-real Element of REAL
C is real V55() ext-real Element of REAL
n is non empty Reflexive MetrStruct
T is TopStruct
(n,T) is real V55() ext-real Element of REAL
the topology of T is open Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[#] n is non empty non proper Element of bool the carrier of n
the carrier of n is non empty set
bool the carrier of n is non empty set
bool ([#] n) is non empty Element of bool (bool ([#] n))
bool ([#] n) is non empty set
bool (bool ([#] n)) is non empty set
I is set
C is Element of bool the carrier of n
diameter C is real V55() ext-real Element of REAL
E is real V55() ext-real set
the topology of T is open Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[#] n is non empty non proper Element of bool the carrier of n
the carrier of n is non empty set
bool the carrier of n is non empty set
bool ([#] n) is non empty Element of bool (bool ([#] n))
bool ([#] n) is non empty set
bool (bool ([#] n)) is non empty set
the topology of T is open Element of bool (bool the carrier of T)
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[#] n is non empty non proper Element of bool the carrier of n
the carrier of n is non empty set
bool the carrier of n is non empty set
bool ([#] n) is non empty Element of bool (bool ([#] n))
bool ([#] n) is non empty set
bool (bool ([#] n)) is non empty set
n is set
T is non empty Reflexive MetrStruct
I is (T) SimplicialComplexStr of n
(T,I) is real V55() ext-real Element of REAL
C is subset-closed finite-membered (T) SubSimplicialComplex of I
(T,C) is real V55() ext-real Element of REAL
the topology of C is finite-membered open Element of bool (bool the carrier of C)
the carrier of C is set
bool the carrier of C is non empty set
bool (bool the carrier of C) is non empty set
the topology of I is open Element of bool (bool the carrier of I)
the carrier of I is set
bool the carrier of I is non empty set
bool (bool the carrier of I) is non empty set
[#] T is non empty non proper Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is non empty set
bool ([#] T) is non empty Element of bool (bool ([#] T))
bool ([#] T) is non empty set
bool (bool ([#] T)) is non empty set
E is Element of bool the carrier of T
diameter E is real V55() ext-real Element of REAL
[#] T is non empty non proper Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is non empty set
bool ([#] T) is non empty Element of bool (bool ([#] T))
bool ([#] T) is non empty set
bool (bool ([#] T)) is non empty set
[#] T is non empty non proper Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is non empty set
bool ([#] T) is non empty Element of bool (bool ([#] T))
bool ([#] T) is non empty set
bool (bool ([#] T)) is non empty set
n is set
T is non empty Reflexive MetrStruct
the real V55() ext-real Element of REAL is real V55() ext-real Element of REAL
C is subset-closed (T) SimplicialComplexStr of n
(T,C) is real V55() ext-real Element of REAL
E is real integer finite V55() ext-real set
Skeleton_of (C,E) is subset-closed finite-membered finite-degree (T) SubSimplicialComplex of C
the carrier of C is set
the topology of C is open Element of bool (bool the carrier of C)
bool the carrier of C is non empty set
bool (bool the carrier of C) is non empty set
E + 1 is real V55() ext-real set
K163(E,1) is real integer finite V55() ext-real set
the_subsets_with_limited_card ((E + 1), the topology of C, the carrier of C) is Element of bool (bool the carrier of C)
Complex_of (the_subsets_with_limited_card ((E + 1), the topology of C, the carrier of C)) is strict subset-closed total SimplicialComplexStr of the carrier of C
subset-closed_closure_of (the_subsets_with_limited_card ((E + 1), the topology of C, the carrier of C)) is subset-closed Element of bool (bool the carrier of C)
TopStruct(# the carrier of C,(subset-closed_closure_of (the_subsets_with_limited_card ((E + 1), the topology of C, the carrier of C))) #) is strict TopStruct
(T,(Skeleton_of (C,E))) is real V55() ext-real Element of REAL
the topology of (Skeleton_of (C,E)) is finite-membered open Element of bool (bool the carrier of (Skeleton_of (C,E)))
the carrier of (Skeleton_of (C,E)) is set
bool the carrier of (Skeleton_of (C,E)) is non empty set
bool (bool the carrier of (Skeleton_of (C,E))) is non empty set
[#] T is non empty non proper Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is non empty set
bool ([#] T) is non empty Element of bool (bool ([#] T))
bool ([#] T) is non empty set
bool (bool ([#] T)) is non empty set
the_family_of C is Element of bool (bool the carrier of C)
n1 is Element of bool the carrier of T
E + 1 is real integer finite V55() ext-real Element of REAL
the_subsets_with_limited_card ((E + 1), the topology of C, the carrier of C) is finite-membered Element of bool (bool the carrier of C)
c is set
TRC is Element of bool the carrier of C
diameter n1 is real V55() ext-real Element of REAL
[#] T is non empty non proper Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is non empty set
bool ([#] T) is non empty Element of bool (bool ([#] T))
bool ([#] T) is non empty set
bool (bool ([#] T)) is non empty set
[#] T is non empty non proper Element of bool the carrier of T
the carrier of T is non empty set
bool the carrier of T is non empty set
bool ([#] T) is non empty Element of bool (bool ([#] T))
bool ([#] T) is non empty set
bool (bool ([#] T)) is non empty set
n is non empty Reflexive MetrStruct
T is non void subset-closed non with_non-empty_elements (n) TopStruct
(n,T) is real V55() ext-real Element of REAL
the carrier of n is non empty set
bool the carrier of n is non empty set
the carrier of T is set
bool the carrier of T is non empty set
I is real V55() ext-real Element of REAL
{} T is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() open compact ext-real non positive non negative V93() V94() V95() V96() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() bounded_below bounded_above real-bounded interval subset-closed Element of bool the carrier of T
{} n is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() ext-real non positive non negative V93() V94() V95() V96() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() bounded_below bounded_above real-bounded interval subset-closed bounded Element of bool the carrier of n
the topology of T is open Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
[#] n is non empty non proper Element of bool the carrier of n
bool ([#] n) is non empty Element of bool (bool ([#] n))
bool ([#] n) is non empty set
bool (bool ([#] n)) is non empty set
C is Element of bool the carrier of n
diameter C is real V55() ext-real Element of REAL
C is real V55() ext-real set
E is Element of bool the carrier of n
diameter E is real V55() ext-real Element of REAL
C is Element of bool the carrier of n
diameter C is real V55() ext-real Element of REAL
C is Element of bool the carrier of n
diameter C is real V55() ext-real Element of REAL
n is non empty Reflexive MetrStruct
the carrier of n is non empty set
bool the carrier of n is non empty set
T is finite bounded Element of bool the carrier of n
{T} is non empty trivial finite finite-membered 1 -element V365( the carrier of n) Element of bool (bool the carrier of n)
bool (bool the carrier of n) is non empty set
Complex_of {T} is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements total SimplicialComplexStr of the carrier of n
subset-closed_closure_of {T} is non empty finite-membered non with_non-empty_elements subset-closed Element of bool (bool the carrier of n)
TopStruct(# the carrier of n,(subset-closed_closure_of {T}) #) is non empty strict TopStruct
(n,(Complex_of {T})) is real V55() ext-real Element of REAL
diameter T is real V55() ext-real Element of REAL
C is non void subset-closed finite-membered non with_non-empty_elements (n) SimplicialComplexStr of the carrier of n
the carrier of C is set
bool the carrier of C is non empty set
the topology of C is finite-membered open Element of bool (bool the carrier of C)
bool (bool the carrier of C) is non empty set
bool T is non empty finite finite-membered V365(T) Element of bool (bool T)
bool T is non empty finite finite-membered set
bool (bool T) is non empty finite finite-membered set
C is Element of bool the carrier of n
diameter C is real V55() ext-real Element of REAL
(n,C) is real V55() ext-real Element of REAL
E is Element of bool the carrier of C
n is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
TOP-REAL n is non empty TopSpace-like V126() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict V191() V192() V221() V222() finite-dimensional with_finite_small_inductive_dimension L15()
the carrier of (TOP-REAL n) is non empty set
Euclid n is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist n is non empty Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL n),(REAL n):],REAL:]
[:(REAL n),(REAL n):] is non empty Relation-like set
[:[:(REAL n),(REAL n):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[:(REAL n),(REAL n):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
T is SimplicialComplexStr of the carrier of (TOP-REAL n)
((Euclid n),T) is real V55() ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
TOP-REAL n is non empty TopSpace-like V126() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict V191() V192() V221() V222() finite-dimensional with_finite_small_inductive_dimension L15()
the carrier of (TOP-REAL n) is non empty set
Euclid n is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist n is non empty Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL n),(REAL n):],REAL:]
[:(REAL n),(REAL n):] is non empty Relation-like set
[:[:(REAL n),(REAL n):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[:(REAL n),(REAL n):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
T is SimplicialComplexStr of the carrier of (TOP-REAL n)
bool the carrier of (TOP-REAL n) is non empty set
{} (TOP-REAL n) is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding finite-membered cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V55() open closed compact ext-real non positive non negative V93() V94() V95() V96() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V109() affinely-independent bounded_below bounded_above real-bounded interval subset-closed with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
{({} (TOP-REAL n))} is non empty trivial functional finite finite-membered 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered affinely-independent left_end right_end bounded_below bounded_above real-bounded V365( the carrier of (TOP-REAL n)) Element of bool (bool the carrier of (TOP-REAL n))
bool (bool the carrier of (TOP-REAL n)) is non empty set
Complex_of {({} (TOP-REAL n))} is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements total total affinely-independent simplex-join-closed SimplicialComplexStr of the carrier of (TOP-REAL n)
subset-closed_closure_of {({} (TOP-REAL n))} is non empty finite-membered non with_non-empty_elements subset-closed Element of bool (bool the carrier of (TOP-REAL n))
TopStruct(# the carrier of (TOP-REAL n),(subset-closed_closure_of {({} (TOP-REAL n))}) #) is non empty strict TopStruct
I is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements total affinely-independent simplex-join-closed SimplicialComplexStr of the carrier of (TOP-REAL n)
T is SimplicialComplexStr of the carrier of (TOP-REAL n)
n is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
TOP-REAL n is non empty TopSpace-like V126() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict V191() V192() V221() V222() finite-dimensional with_finite_small_inductive_dimension L15()
[#] (TOP-REAL n) is non empty non proper non proper open open closed closed convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
the carrier of (TOP-REAL n) is non empty set
bool the carrier of (TOP-REAL n) is non empty set
Euclid n is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct
REAL n is non empty functional FinSequence-membered FinSequenceSet of REAL
n -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist n is non empty Relation-like [:(REAL n),(REAL n):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL n),(REAL n):],REAL:]
[:(REAL n),(REAL n):] is non empty Relation-like set
[:[:(REAL n),(REAL n):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[:(REAL n),(REAL n):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
[#] (Euclid n) is non empty non proper Element of bool the carrier of (Euclid n)
the carrier of (Euclid n) is non empty set
bool the carrier of (Euclid n) is non empty set
the topology of (TOP-REAL n) is non empty open Element of bool (bool the carrier of (TOP-REAL n))
bool (bool the carrier of (TOP-REAL n)) is non empty set
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like V426() TopStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
Family_open_set (Euclid n) is Element of bool (bool the carrier of (Euclid n))
bool (bool the carrier of (Euclid n)) is non empty set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is non empty strict TopStruct
n is set
{n} is non empty trivial finite 1 -element set
T is set
I is set
n is non empty V126() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
bool the carrier of n is non empty set
bool (bool the carrier of n) is non empty set
BOOL the carrier of n is set
center_of_mass n is Relation-like BOOL the carrier of n -defined the carrier of n -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of n), the carrier of n:]
[:(BOOL the carrier of n), the carrier of n:] is Relation-like set
bool [:(BOOL the carrier of n), the carrier of n:] is non empty set
T is non void subset-closed finite-membered non with_non-empty_elements SimplicialComplexStr of the carrier of n
BCS T is non void subset-closed finite-membered non with_non-empty_elements SubdivisionStr of T
the carrier of (BCS T) is set
bool the carrier of (BCS T) is non empty set
I is open Element of bool the carrier of (BCS T)
E is c=-linear finite finite-membered V365( the carrier of n) Element of bool (bool the carrier of n)
(center_of_mass n) .: E is finite Element of bool the carrier of n
union E is finite Element of bool the carrier of n
{(union E)} is non empty trivial finite finite-membered 1 -element V365( the carrier of n) Element of bool (bool the carrier of n)
Complex_of {(union E)} is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements total SimplicialComplexStr of the carrier of n
subset-closed_closure_of {(union E)} is non empty finite-membered non with_non-empty_elements subset-closed Element of bool (bool the carrier of n)
TopStruct(# the carrier of n,(subset-closed_closure_of {(union E)}) #) is non empty strict TopStruct
BCS (Complex_of {(union E)}) is non void subset-closed finite-membered non with_non-empty_elements SubdivisionStr of Complex_of {(union E)}
Vertices (BCS (Complex_of {(union E)})) is Element of bool the carrier of (BCS (Complex_of {(union E)}))
the carrier of (BCS (Complex_of {(union E)})) is set
bool the carrier of (BCS (Complex_of {(union E)})) is non empty set
card (union E) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of omega
(card (union E)) - 1 is real integer finite V55() ext-real Element of REAL
K163((card (union E)),K165(1)) is real integer finite V55() ext-real set
((card (union E)) - 1) / (card (union E)) is real V55() ext-real Element of COMPLEX
K166((card (union E))) is real V55() ext-real non negative set
K164(((card (union E)) - 1),K166((card (union E)))) is real V55() ext-real set
C is Element of the carrier of n
n1 is Element of the carrier of n
C - n1 is Element of the carrier of n
- n1 is Element of the carrier of n
K323(n,C,(- n1)) is Element of the carrier of n
dom (center_of_mass n) is Element of bool (BOOL the carrier of n)
bool (BOOL the carrier of n) is non empty set
c is set
(center_of_mass n) . c is set
TRC is set
(center_of_mass n) . TRC is set
R is Element of the carrier of n
G is Element of the carrier of n
R - G is Element of the carrier of n
- G is Element of the carrier of n
K323(n,R,(- G)) is Element of the carrier of n
the topology of (Complex_of {(union E)}) is finite finite-membered V365( the carrier of (Complex_of {(union E)})) open Element of bool (bool the carrier of (Complex_of {(union E)}))
the carrier of (Complex_of {(union E)}) is set
bool the carrier of (Complex_of {(union E)}) is non empty set
bool (bool the carrier of (Complex_of {(union E)})) is non empty set
bool (union E) is non empty finite finite-membered V365( union E) Element of bool (bool (union E))
bool (union E) is non empty finite finite-membered set
bool (bool (union E)) is non empty finite finite-membered set
G0 is set
p is set
(center_of_mass n) . G0 is set
(center_of_mass n) . p is set
h is non empty finite Element of bool the carrier of n
h is non empty finite Element of bool the carrier of n
h \ h is finite Element of bool the carrier of n
{h} is non empty trivial finite finite-membered 1 -element V365( the carrier of n) Element of bool (bool the carrier of n)
{(h \ h)} is non empty trivial finite finite-membered 1 -element V365( the carrier of n) Element of bool (bool the carrier of n)
cgx is Element of bool (bool the carrier of (Complex_of {(union E)}))
GX is Element of bool (bool the carrier of (Complex_of {(union E)}))
|.(Complex_of {(union E)}).| is Element of bool the carrier of n
[#] n is non empty non proper Element of bool the carrier of n
[#] (Complex_of {(union E)}) is non proper Element of bool the carrier of (Complex_of {(union E)})
subdivision ((center_of_mass n),(Complex_of {(union E)})) is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements SimplicialComplexStr of the carrier of n
[#] (subdivision ((center_of_mass n),(Complex_of {(union E)}))) is non proper Element of bool the carrier of (subdivision ((center_of_mass n),(Complex_of {(union E)})))
the carrier of (subdivision ((center_of_mass n),(Complex_of {(union E)}))) is set
bool the carrier of (subdivision ((center_of_mass n),(Complex_of {(union E)}))) is non empty set
{R} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of n
I is Element of bool the carrier of (BCS (Complex_of {(union E)}))
(center_of_mass n) .: cgx is Element of bool the carrier of n
Im ((center_of_mass n),h) is set
t is Element of the carrier of (BCS (Complex_of {(union E)}))
x is Element of the carrier of n
i1 is Element of the carrier of n
x - i1 is Element of the carrier of n
- i1 is Element of the carrier of n
K323(n,x,(- i1)) is Element of the carrier of n
y is real V55() ext-real Element of REAL
y * (x - i1) is Element of the carrier of n
the Mult of n is non empty Relation-like [:REAL, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of n:], the carrier of n:]
[:REAL, the carrier of n:] is non empty non trivial Relation-like non finite set
[:[:REAL, the carrier of n:], the carrier of n:] is non empty non trivial Relation-like non finite set
bool [:[:REAL, the carrier of n:], the carrier of n:] is non empty non trivial non finite set
the Mult of n . (y,(x - i1)) is set
1 - 1 is real integer finite V55() ext-real Element of REAL
K163(1,K165(1)) is real integer finite V55() ext-real set
0. n is V65(n) Element of the carrier of n
the ZeroF of n is Element of the carrier of n
y is non empty finite Element of bool the carrier of n
(center_of_mass n) . y is set
rng (center_of_mass n) is Element of bool the carrier of n
x is Element of the carrier of n
{x} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of n
i1 is Element of bool the carrier of (BCS (Complex_of {(union E)}))
(center_of_mass n) .: GX is Element of bool the carrier of n
Im ((center_of_mass n),y) is set
i2 is Element of the carrier of (BCS (Complex_of {(union E)}))
card h is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of omega
1 / (card h) is real V55() ext-real non negative Element of COMPLEX
K166((card h)) is non empty real V55() ext-real positive non negative set
K164(1,K166((card h))) is real V55() ext-real non negative set
card h is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of omega
1 / (card h) is real V55() ext-real non negative Element of COMPLEX
K166((card h)) is non empty real V55() ext-real positive non negative set
K164(1,K166((card h))) is real V55() ext-real non negative set
card y is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of omega
1 / (card y) is real V55() ext-real non negative Element of COMPLEX
K166((card y)) is non empty real V55() ext-real positive non negative set
K164(1,K166((card y))) is real V55() ext-real non negative set
(card y) / (card h) is real V55() ext-real non negative Element of COMPLEX
K164((card y),K166((card h))) is real V55() ext-real non negative set
R - x is Element of the carrier of n
- x is Element of the carrier of n
K323(n,R,(- x)) is Element of the carrier of n
r is real V55() ext-real Element of REAL
r * (R - x) is Element of the carrier of n
the Mult of n is non empty Relation-like [:REAL, the carrier of n:] -defined the carrier of n -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of n:], the carrier of n:]
[:REAL, the carrier of n:] is non empty non trivial Relation-like non finite set
[:[:REAL, the carrier of n:], the carrier of n:] is non empty non trivial Relation-like non finite set
bool [:[:REAL, the carrier of n:], the carrier of n:] is non empty non trivial non finite set
the Mult of n . (r,(R - x)) is set
r21 is real V55() ext-real Element of REAL
r * r21 is real V55() ext-real Element of REAL
(card y) * 1 is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative Element of REAL
(card y) * (card h) is non empty real V55() ext-real positive non negative set
K164((card y),(card h)) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
((card y) * 1) / ((card y) * (card h)) is real V55() ext-real non negative Element of COMPLEX
K166(((card y) * (card h))) is non empty real V55() ext-real positive non negative set
K164(((card y) * 1),K166(((card y) * (card h)))) is real V55() ext-real non negative set
r2 is real V55() ext-real Element of REAL
Sum h is Element of the carrier of n
r1 is real V55() ext-real Element of REAL
r1 * (Sum h) is Element of the carrier of n
the Mult of n . (r1,(Sum h)) is set
r1 * (card h) is real V55() ext-real Element of REAL
ZeroLC n is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of n
h --> r1 is non empty Relation-like h