:: 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 -defined REAL -valued Function-like total quasi_total finite V93() V94() V95() Element of bool [:h,REAL:]
[:h,REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:h,REAL:] is non empty non trivial non finite set
(ZeroLC n) +* (h --> r1) is Relation-like Function-like V93() V94() V95() set
L1 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of h
Sum L1 is Element of the carrier of n
sum L1 is real V55() ext-real Element of REAL
Carrier L1 is Element of bool the carrier of n
1 * (card h) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative Element of REAL
1 * (card h) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative Element of REAL
(1 * (card h)) - (1 * (card h)) is real integer finite V55() ext-real Element of REAL
K165((1 * (card h))) is real integer finite V55() ext-real non positive set
K163((1 * (card h)),K165((1 * (card h)))) is real integer finite V55() ext-real set
r1 - r2 is real V55() ext-real Element of REAL
K165(r2) is real V55() ext-real set
K163(r1,K165(r2)) is real V55() ext-real set
(card h) * (card h) is non empty real V55() ext-real positive non negative set
K164((card h),(card h)) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
((card y) * 1) / ((card h) * (card h)) is real V55() ext-real non negative Element of COMPLEX
K166(((card h) * (card h))) is non empty real V55() ext-real positive non negative set
K164(((card y) * 1),K166(((card h) * (card h)))) is real V55() ext-real non negative set
r * r1 is real V55() ext-real Element of REAL
Sum y is Element of the carrier of n
r21 * (Sum y) is Element of the carrier of n
the Mult of n . (r21,(Sum y)) is set
r21 * (card y) is real V55() ext-real Element of REAL
y --> r21 is non empty Relation-like y -defined REAL -valued Function-like total quasi_total finite V93() V94() V95() Element of bool [:y,REAL:]
[:y,REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:y,REAL:] is non empty non trivial non finite set
(ZeroLC n) +* (y --> r21) is Relation-like Function-like V93() V94() V95() set
L21 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of y
Sum L21 is Element of the carrier of n
sum L21 is real V55() ext-real Element of REAL
Carrier L21 is Element of bool the carrier of n
Sum h is Element of the carrier of n
r2 * (Sum h) is Element of the carrier of n
the Mult of n . (r2,(Sum h)) is set
r2 * (card h) is real V55() ext-real Element of REAL
h --> r2 is non empty Relation-like h -defined REAL -valued Function-like total quasi_total finite V93() V94() V95() Element of bool [:h,REAL:]
[:h,REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:h,REAL:] is non empty non trivial non finite set
(ZeroLC n) +* (h --> r2) is Relation-like Function-like V93() V94() V95() set
L2 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of h
Sum L2 is Element of the carrier of n
sum L2 is real V55() ext-real Element of REAL
Carrier L2 is Element of bool the carrier of n
L1 - L2 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of n
L1 - L21 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of n
r * (L1 - L21) is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of n
v is Element of the carrier of n
(L1 - L2) . v is real V55() ext-real Element of REAL
(r * (L1 - L21)) . v is real V55() ext-real Element of REAL
dom (y --> r21) is non empty finite Element of bool y
bool y is non empty finite finite-membered set
L1 . v is real V55() ext-real Element of REAL
L2 . v is real V55() ext-real Element of REAL
(L1 . v) - (L2 . v) is real V55() ext-real Element of REAL
K165((L2 . v)) is real V55() ext-real set
K163((L1 . v),K165((L2 . v))) is real V55() ext-real set
dom (h --> r1) is non empty finite Element of bool h
bool h is non empty finite finite-membered set
dom (h --> r2) is non empty finite Element of bool h
bool h is non empty finite finite-membered set
(L1 - L21) . v is real V55() ext-real Element of REAL
r * ((L1 - L21) . v) is real V55() ext-real Element of REAL
L21 . v is real V55() ext-real Element of REAL
(L1 . v) - (L21 . v) is real V55() ext-real Element of REAL
K165((L21 . v)) is real V55() ext-real set
K163((L1 . v),K165((L21 . v))) is real V55() ext-real set
r * ((L1 . v) - (L21 . v)) is real V55() ext-real Element of REAL
(h --> r2) . v is real V55() ext-real set
(h --> r1) . v is real V55() ext-real set
(h --> r2) . v is real V55() ext-real set
- r2 is real V55() ext-real Element of REAL
(y --> r21) . v is real V55() ext-real set
- r21 is real V55() ext-real Element of REAL
r * (- r21) is real V55() ext-real Element of REAL
(card h) * (card (union E)) is real V55() ext-real non negative set
K164((card h),(card (union E))) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
(card h) * (card (union E)) is real V55() ext-real non negative set
K164((card h),(card (union E))) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
((card h) * (card (union E))) - ((card h) * (card (union E))) is real V55() ext-real set
K167(((card h) * (card (union E))),((card h) * (card (union E)))) is real V55() ext-real set
K165(((card h) * (card (union E)))) is real V55() ext-real non positive set
K163(((card h) * (card (union E))),K165(((card h) * (card (union E))))) is real V55() ext-real set
(card (union E)) * (card h) is real V55() ext-real non negative set
K164((card (union E)),(card h)) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
((card (union E)) * (card h)) - (card h) is real V55() ext-real set
K167(((card (union E)) * (card h)),(card h)) is real V55() ext-real set
K165((card h)) is real integer finite V55() ext-real non positive set
K163(((card (union E)) * (card h)),K165((card h))) is real V55() ext-real set
(card y) * (card (union E)) is real V55() ext-real non negative set
K164((card y),(card (union E))) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
((card (union E)) - 1) * (card h) is real integer finite V55() ext-real Element of REAL
Sum (r * (L1 - L21)) is Element of the carrier of n
Sum (L1 - L21) is Element of the carrier of n
r * (Sum (L1 - L21)) is Element of the carrier of n
the Mult of n . (r,(Sum (L1 - L21))) is set
n1 - C is Element of the carrier of n
- C is Element of the carrier of n
K323(n,n1,(- C)) is Element of the carrier of n
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
G0 is real V55() ext-real Element of REAL
G0 * (R - G) 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 . (G0,(R - G)) is set
G - R is Element of the carrier of n
- R is Element of the carrier of n
K323(n,G,(- R)) is Element of the carrier of n
G0 * (G - R) is Element of the carrier of n
the Mult of n . (G0,(G - R)) is set
- (G0 * (R - G)) is Element of the carrier of n
- (R - G) is Element of the carrier of n
G0 * (- (R - G)) is Element of the carrier of n
the Mult of n . (G0,(- (R - G))) is set
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
bool the carrier of (TOP-REAL n) is non empty set
T is set
I is finite compact affinely-independent with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
C is Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I
dom C 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
(dom C) \ T 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
C .: T is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (C .: T) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
{ (conv (I \ {(C . b₁)})) where b₁ 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 : b₁ in (dom C) \ T } is set
meet { (conv (I \ {(C . b₁)})) where b₁ 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 : b₁ in (dom C) \ T } is set
rng C is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
C is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
c is set
(dom C) \ c 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
card ((dom C) \ c) 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
C .: ((dom C) \ c) is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
I \ (C .: ((dom C) \ c)) is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (I \ (C .: ((dom C) \ c))) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
{ (conv (I \ {(C . b₁)})) where b₁ 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 : b₁ in (dom C) \ c } is set
meet { (conv (I \ {(C . b₁)})) where b₁ 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 : b₁ in (dom C) \ c } is set
{ H₁(b₁) where b₁ 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 : b₁ in (dom C) \ c } is set
carr is set
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} is non empty trivial 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 Element of bool NAT
C .: {f} is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
Im (C,f) is set
C . f is set
{(C . f)} is non empty trivial finite 1 -element set
R is set
{R} is non empty trivial finite 1 -element set
I \ {(C . f)} is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (I \ {(C . f)}) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
{H₁(f)} is non empty trivial finite 1 -element 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
G is set
G0 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
C . G0 is set
{(C . G0)} is non empty trivial finite 1 -element set
I \ {(C . G0)} is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (I \ {(C . G0)}) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
c \/ {f} is non empty set
(dom C) \ (c \/ {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
{ H₁(b₁) where b₁ 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 : b₁ in (dom C) \ (c \/ {f}) } is set
the epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative Element of (dom C) \ (c \/ {f}) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative Element of (dom C) \ (c \/ {f})
((dom C) \ c) \ {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
(((dom C) \ c) \ {f}) \/ {f} is non empty finite 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 bool NAT
p is 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
C . h is set
{(C . h)} is non empty trivial finite 1 -element set
I \ {(C . h)} is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (I \ {(C . h)}) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
card (((dom C) \ c) \ {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 omega
(card (((dom C) \ c) \ {f})) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
C . the epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative Element of (dom C) \ (c \/ {f}) is set
{(C . the epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative Element of (dom C) \ (c \/ {f}))} is non empty trivial finite 1 -element set
I \ {(C . the epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative Element of (dom C) \ (c \/ {f}))} is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (I \ {(C . the epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() V56() ext-real non negative Element of (dom C) \ (c \/ {f}))}) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
I \ {(C . f)} is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (I \ {(C . f)}) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
{H₁(f)} is non empty trivial finite 1 -element 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
{I} is non empty trivial finite finite-membered 1 -element affinely-independent V365( the carrier of (TOP-REAL n)) Element of bool (bool the carrier of (TOP-REAL n))
Complex_of {I} 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 ( Euclid n) (n) SimplicialComplexStr of the carrier of (TOP-REAL n)
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
subset-closed_closure_of {I} 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 {I}) #) is non empty strict TopStruct
the topology of (Complex_of {I}) is finite finite-membered V365( the carrier of (Complex_of {I})) open Element of bool (bool the carrier of (Complex_of {I}))
the carrier of (Complex_of {I}) is set
bool the carrier of (Complex_of {I}) is non empty set
bool (bool the carrier of (Complex_of {I})) is non empty set
bool I is non empty finite finite-membered V365(I) Element of bool (bool I)
bool I is non empty finite finite-membered set
bool (bool I) is non empty finite finite-membered set
{ H₁(b₁) where b₁ 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 : b₁ in (dom C) \ (c \/ {f}) } \/ {H₁(f)} is non empty set
gx is set
cgx 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
C . cgx is set
{(C . cgx)} is non empty trivial finite 1 -element set
I \ {(C . cgx)} is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (I \ {(C . cgx)}) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
C .: ((dom C) \ (c \/ {f})) is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
I \ (C .: ((dom C) \ (c \/ {f}))) is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
cgx is Element of bool the carrier of (Complex_of {I})
gx is Element of bool the carrier of (Complex_of {I})
@ gx is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (@ gx) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
@ cgx is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (@ cgx) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
(conv (@ gx)) /\ (conv (@ cgx)) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
gx /\ cgx is Element of bool the carrier of (Complex_of {I})
@ (gx /\ cgx) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (@ (gx /\ cgx)) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
(C .: ((dom C) \ (c \/ {f}))) \/ {(C . f)} is non empty finite set
((dom C) \ (c \/ {f})) \/ {f} is non empty finite 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 bool NAT
C .: (((dom C) \ (c \/ {f})) \/ {f}) is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (I \ (C .: ((dom C) \ (c \/ {f})))) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
meet { H₁(b₁) where b₁ 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 : b₁ in (dom C) \ (c \/ {f}) } is set
meet {H₁(f)} is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
(meet { H₁(b₁) where b₁ 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 : b₁ in (dom C) \ (c \/ {f}) } ) /\ (meet {H₁(f)}) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
meet ( { H₁(b₁) where b₁ 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 : b₁ in (dom C) \ (c \/ {f}) } \/ {H₁(f)}) is set
C is set
(dom C) \ C 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
card ((dom C) \ C) 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
C .: ((dom C) \ C) is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
I \ (C .: ((dom C) \ C)) is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (I \ (C .: ((dom C) \ C))) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
{ (conv (I \ {(C . b₁)})) where b₁ 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 : b₁ in (dom C) \ C } is set
meet { (conv (I \ {(C . b₁)})) where b₁ 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 : b₁ in (dom C) \ C } is set
card ((dom C) \ 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 omega
C is set
(dom C) \ C 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
card ((dom C) \ C) 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
C .: ((dom C) \ C) is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
I \ (C .: ((dom C) \ C)) is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (I \ (C .: ((dom C) \ C))) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
{ (conv (I \ {(C . b₁)})) where b₁ 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 : b₁ in (dom C) \ C } is set
meet { (conv (I \ {(C . b₁)})) where b₁ 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 : b₁ in (dom C) \ C } is set
(dom C) \ ((dom C) \ T) 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
(dom C) /\ T 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
C .: ((dom C) \ ((dom C) \ T)) is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
C .: (dom C) is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
C .: ((dom C) \ T) is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
(C .: (dom C)) \ (C .: ((dom C) \ T)) is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
I \ (C .: ((dom C) \ T)) is finite compact with_finite_small_inductive_dimension Element of bool 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()
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
the carrier of (Euclid n) is non empty set
bool the carrier of (Euclid n) is non empty set
T is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv T is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
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
I is bounded Element of bool the carrier of (Euclid n)
diameter I is real V55() ext-real Element of REAL
C is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
cl_Ball (C,(diameter I)) is Element of bool the carrier of (Euclid n)
E is set
C is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
cl_Ball (C,(diameter I)) is Element of bool the carrier of (Euclid n)
n1 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
cl_Ball (n1,(diameter I)) is closed convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
c is set
TRC is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
dist (C,TRC) is real V55() ext-real non negative Element of REAL
the distance of (Euclid n) is non empty Relation-like [: the carrier of (Euclid n), the carrier of (Euclid n):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:]
[: the carrier of (Euclid n), the carrier of (Euclid n):] is non empty Relation-like set
[:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:] is non empty non trivial non finite set
the distance of (Euclid n) . (C,TRC) is real V55() ext-real Element of REAL
dist (C,C) is real V55() ext-real non negative Element of REAL
the distance of (Euclid n) is non empty Relation-like [: the carrier of (Euclid n), the carrier of (Euclid n):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:]
[: the carrier of (Euclid n), the carrier of (Euclid n):] is non empty Relation-like set
[:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:] is non empty non trivial non finite set
the distance of (Euclid n) . (C,C) is real V55() ext-real Element of REAL
E is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
cl_Ball (E,(diameter I)) is closed convex with_finite_small_inductive_dimension Element of bool 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()
the carrier of (TOP-REAL n) is non empty set
bool the carrier of (TOP-REAL n) is non empty set
T is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv T is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
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
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
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
the carrier of (Euclid n) is non empty set
Family_open_set (Euclid n) is Element of bool (bool the carrier of (Euclid n))
bool the carrier of (Euclid n) is non empty set
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
C is Element of bool the carrier of (Euclid n)
E is bounded Element of bool the carrier of (Euclid n)
diameter E is real V55() ext-real Element of REAL
n1 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
I is Element of bool the carrier of (Euclid n)
cl_Ball (n1,(diameter E)) is Element of bool the carrier of (Euclid n)
c is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
dist (n1,c) is real V55() ext-real non negative Element of REAL
the distance of (Euclid n) is non empty Relation-like [: the carrier of (Euclid n), the carrier of (Euclid n):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:]
[: the carrier of (Euclid n), the carrier of (Euclid n):] is non empty Relation-like set
[:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:] is non empty non trivial non finite set
the distance of (Euclid n) . (n1,c) is real V55() ext-real Element of REAL
(diameter E) + 1 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
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
the carrier of (Euclid n) is non empty set
bool the carrier of (Euclid n) is non empty set
T is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv T is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
C is bounded Element of bool the carrier of (Euclid n)
I is bounded Element of bool the carrier of (Euclid n)
diameter I is real V55() ext-real Element of REAL
diameter C is real V55() ext-real Element of REAL
E is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
cl_Ball (E,(diameter I)) is Element of bool the carrier of (Euclid n)
C is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
dist (E,C) is real V55() ext-real non negative Element of REAL
the distance of (Euclid n) is non empty Relation-like [: the carrier of (Euclid n), the carrier of (Euclid n):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:]
[: the carrier of (Euclid n), the carrier of (Euclid n):] is non empty Relation-like set
[:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:] is non empty non trivial non finite set
the distance of (Euclid n) . (E,C) 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
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
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
T is ( Euclid n) (n) SimplicialComplexStr of the carrier of (TOP-REAL n)
I is SubdivisionStr of T
the carrier of (Euclid n) is non empty set
bool the carrier of (Euclid 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
C is real V55() ext-real 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
E is Element of bool the carrier of (Euclid n)
diameter E is real V55() ext-real Element of REAL
C is Element of bool the carrier of I
@ C is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
bool the carrier of (TOP-REAL n) is non empty set
conv (@ C) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
n1 is Element of bool the carrier of T
@ n1 is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (@ n1) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
[#] (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)
[#] (Euclid n) is non empty non proper Element of bool the carrier of (Euclid n)
[#] T is non proper Element of bool the carrier of T
TRC is Element of bool the carrier of (Euclid n)
diameter TRC is real V55() ext-real Element of REAL
c is Element of bool the carrier of (Euclid n)
diameter c is real V55() ext-real Element of REAL
carr is bounded Element of bool the carrier of (Euclid n)
diameter carr 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
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
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
I is non void subset-closed finite-membered finite-degree non with_non-empty_elements ( Euclid n) (n) SimplicialComplexStr of the carrier of (TOP-REAL n)
|.I.| is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
bool the carrier of (TOP-REAL n) is non empty set
[#] I is non proper Element of bool the carrier of I
the carrier of I is set
bool the carrier of I is non empty set
BCS I is non void subset-closed finite-membered non with_non-empty_elements ( Euclid n) (n) SubdivisionStr of I
(n,(BCS I)) is real V55() ext-real Element of REAL
((Euclid n),(BCS I)) is real V55() ext-real Element of REAL
degree I is real integer finite V55() ext-real set
(degree I) + 1 is real integer finite V55() ext-real Element of REAL
(degree I) / ((degree I) + 1) is real V55() ext-real Element of COMPLEX
K166(((degree I) + 1)) is real V55() ext-real set
K164((degree I),K166(((degree I) + 1))) is real V55() ext-real set
(n,I) is real V55() ext-real Element of REAL
((Euclid n),I) is real V55() ext-real Element of REAL
((degree I) / ((degree I) + 1)) * (n,I) is real V55() ext-real Element of REAL
center_of_mass (TOP-REAL n) is Relation-like BOOL the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL n) -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n):]
BOOL the carrier of (TOP-REAL n) is set
[:(BOOL the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n):] is Relation-like set
bool [:(BOOL the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n):] is non empty set
subdivision ((center_of_mass (TOP-REAL n)),I) is strict non void subset-closed finite-membered finite-degree non with_non-empty_elements SimplicialComplexStr of the carrier of (TOP-REAL n)
the carrier of (Euclid n) is non empty set
bool the carrier of (Euclid n) is non empty set
the carrier of (BCS I) is set
bool the carrier of (BCS I) is non empty set
n1 is Element of bool the carrier of (Euclid n)
diameter n1 is real V55() ext-real Element of REAL
bool (bool the carrier of I) is non empty set
carr is c=-linear finite finite-membered V365( the carrier of I) open Element of bool (bool the carrier of I)
(center_of_mass (TOP-REAL n)) .: carr is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
bool (bool the carrier of (TOP-REAL n)) is non empty set
@ carr is Element of bool (bool the carrier of (TOP-REAL n))
f is c=-linear finite finite-membered V365( the carrier of (TOP-REAL n)) Element of bool (bool the carrier of (TOP-REAL n))
union f is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
{(union f)} is non empty trivial finite finite-membered 1 -element V365( the carrier of (TOP-REAL n)) Element of bool (bool the carrier of (TOP-REAL n))
Complex_of {(union f)} is strict non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements total ( Euclid n) (n) SimplicialComplexStr of the carrier of (TOP-REAL n)
subset-closed_closure_of {(union f)} 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 {(union f)}) #) is non empty strict TopStruct
union carr is finite Element of bool the carrier of I
card (union carr) 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
c is ext-real set
(degree I) + c is ext-real set
dom (center_of_mass (TOP-REAL n)) is Element of bool (BOOL the carrier of (TOP-REAL n))
bool (BOOL the carrier of (TOP-REAL n)) is non empty set
[#] (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)
[#] (Euclid n) is non empty non proper Element of bool the carrier of (Euclid n)
TRC is open Element of bool the carrier of (BCS I)
the topology of (BCS I) is finite-membered open Element of bool (bool the carrier of (BCS I))
bool (bool the carrier of (BCS I)) is non empty set
- 1 is real integer finite V55() ext-real non positive Element of REAL
degree (BCS I) is ext-real set
- 1 is real integer finite V55() ext-real non positive Element of REAL
(- 1) + 1 is real integer finite V55() ext-real Element of REAL
G0 is Element of bool the carrier of (Euclid n)
conv (union f) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
h is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
h is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
BCS (Complex_of {(union f)}) is non void subset-closed finite-membered non with_non-empty_elements ( Euclid n) (n) SubdivisionStr of Complex_of {(union f)}
|.(BCS (Complex_of {(union f)})).| is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
|.(Complex_of {(union f)}).| is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
GX is set
(center_of_mass (TOP-REAL n)) . GX is set
card (union 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 omega
((degree I) + 1) " is real V55() ext-real Element of REAL
(card (union f)) " is real V55() ext-real non negative set
K166((card (union f))) is real V55() ext-real non negative set
diameter G0 is real V55() ext-real Element of REAL
(card (union f)) - 1 is real integer finite V55() ext-real Element of REAL
K163((card (union f)),K165(1)) is real integer finite V55() ext-real set
((card (union f)) - 1) / (card (union f)) is real V55() ext-real Element of COMPLEX
K164(((card (union f)) - 1),K166((card (union f)))) is real V55() ext-real set
(card (union f)) / (card (union f)) is real V55() ext-real non negative Element of COMPLEX
K164((card (union f)),K166((card (union f)))) is real V55() ext-real non negative set
1 / (card (union f)) is real V55() ext-real non negative Element of COMPLEX
K164(1,K166((card (union f)))) is real V55() ext-real non negative set
((card (union f)) / (card (union f))) - (1 / (card (union f))) is real V55() ext-real Element of COMPLEX
K165((1 / (card (union f)))) is real V55() ext-real non positive set
K163(((card (union f)) / (card (union f))),K165((1 / (card (union f))))) is real V55() ext-real set
1 - (1 / (card (union f))) is real V55() ext-real Element of REAL
K163(1,K165((1 / (card (union f))))) is real V55() ext-real set
p is bounded Element of bool the carrier of (Euclid n)
diameter p is real V55() ext-real Element of REAL
Vertices (BCS (Complex_of {(union f)})) is Element of bool the carrier of (BCS (Complex_of {(union f)}))
the carrier of (BCS (Complex_of {(union f)})) is set
bool the carrier of (BCS (Complex_of {(union f)})) is non empty set
gx is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
cgx is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
gx - cgx is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
- cgx is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
- cgx is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
K323((TOP-REAL n),gx,(- cgx)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
gx + (- cgx) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
gx - cgx is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
I is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
t is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
I - t is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
- t is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
- t is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
K323((TOP-REAL n),I,(- t)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
I + (- t) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
I - t is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
y is real V55() ext-real Element of REAL
y * (I - t) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
the Mult of (TOP-REAL n) is non empty Relation-like [:REAL, the carrier of (TOP-REAL n):] -defined the carrier of (TOP-REAL n) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):]
[:REAL, the carrier of (TOP-REAL n):] is non empty non trivial Relation-like non finite set
[:[:REAL, the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is non empty non trivial Relation-like non finite set
bool [:[:REAL, the carrier of (TOP-REAL n):], the carrier of (TOP-REAL n):] is non empty non trivial non finite set
the Mult of (TOP-REAL n) . (y,(I - t)) is set
y * (I - t) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
x is Element of the carrier of (BCS (Complex_of {(union f)}))
i2 is Element of bool the carrier of (BCS (Complex_of {(union f)}))
@ i2 is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (@ i2) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
i1 is Element of the carrier of (BCS (Complex_of {(union f)}))
S2 is Element of bool the carrier of (BCS (Complex_of {(union f)}))
@ S2 is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (@ S2) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
((degree I) + 1) / ((degree I) + 1) is real V55() ext-real Element of COMPLEX
K164(((degree I) + 1),K166(((degree I) + 1))) is real V55() ext-real set
1 / ((degree I) + 1) is real V55() ext-real Element of COMPLEX
K164(1,K166(((degree I) + 1))) is real V55() ext-real set
(((degree I) + 1) / ((degree I) + 1)) - (1 / ((degree I) + 1)) is real V55() ext-real Element of COMPLEX
K165((1 / ((degree I) + 1))) is real V55() ext-real set
K163((((degree I) + 1) / ((degree I) + 1)),K165((1 / ((degree I) + 1)))) is real V55() ext-real set
1 - (1 / ((degree I) + 1)) is real V55() ext-real Element of REAL
K163(1,K165((1 / ((degree I) + 1)))) is real V55() ext-real set
bb1 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
bb2 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
dist (bb1,bb2) is real V55() ext-real non negative Element of REAL
the distance of (Euclid n) is non empty Relation-like [: the carrier of (Euclid n), the carrier of (Euclid n):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:]
[: the carrier of (Euclid n), the carrier of (Euclid n):] is non empty Relation-like set
[:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:] is non empty non trivial non finite set
the distance of (Euclid n) . (bb1,bb2) is real V55() ext-real Element of REAL
dist (h,h) is real V55() ext-real non negative Element of REAL
the distance of (Euclid n) . (h,h) is real V55() ext-real Element of REAL
h - h is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
|.(h - h).| is real V55() ext-real non negative Element of REAL
K510((h - h)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
Sum K510((h - h)) is real V55() ext-real Element of REAL
sqrt (Sum K510((h - h))) is real V55() ext-real Element of REAL
|.(gx - cgx).| is real V55() ext-real non negative Element of REAL
K510((gx - cgx)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
Sum K510((gx - cgx)) is real V55() ext-real Element of REAL
sqrt (Sum K510((gx - cgx))) is real V55() ext-real Element of REAL
bb1 - bb2 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
y * (bb1 - bb2) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
|.(y * (bb1 - bb2)).| is real V55() ext-real non negative Element of REAL
K510((y * (bb1 - bb2))) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
Sum K510((y * (bb1 - bb2))) is real V55() ext-real Element of REAL
sqrt (Sum K510((y * (bb1 - bb2)))) is real V55() ext-real Element of REAL
abs y is real V55() ext-real Element of REAL
|.(bb1 - bb2).| is real V55() ext-real non negative Element of REAL
K510((bb1 - bb2)) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
Sum K510((bb1 - bb2)) is real V55() ext-real Element of REAL
sqrt (Sum K510((bb1 - bb2))) is real V55() ext-real Element of REAL
(abs y) * |.(bb1 - bb2).| is real V55() ext-real Element of REAL
y * |.(bb1 - bb2).| is real V55() ext-real Element of REAL
y * (dist (bb1,bb2)) 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
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
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
T is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
I is non void subset-closed finite-membered finite-degree non with_non-empty_elements ( Euclid n) (n) SimplicialComplexStr of the carrier of (TOP-REAL n)
|.I.| is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
bool the carrier of (TOP-REAL n) is non empty set
[#] I is non proper Element of bool the carrier of I
the carrier of I is set
bool the carrier of I is non empty set
BCS (T,I) is non void subset-closed finite-membered non with_non-empty_elements ( Euclid n) (n) SubdivisionStr of I
(n,(BCS (T,I))) is real V55() ext-real Element of REAL
((Euclid n),(BCS (T,I))) is real V55() ext-real Element of REAL
degree I is real integer finite V55() ext-real set
(degree I) + 1 is real integer finite V55() ext-real Element of REAL
(degree I) / ((degree I) + 1) is real V55() ext-real Element of COMPLEX
K166(((degree I) + 1)) is real V55() ext-real set
K164((degree I),K166(((degree I) + 1))) is real V55() ext-real set
((degree I) / ((degree I) + 1)) |^ T is real V55() ext-real set
(n,I) is real V55() ext-real Element of REAL
((Euclid n),I) is real V55() ext-real Element of REAL
(((degree I) / ((degree I) + 1)) |^ T) * (n,I) is real V55() ext-real Element of REAL
C is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
BCS (C,I) is non void subset-closed finite-membered non with_non-empty_elements ( Euclid n) (n) SubdivisionStr of I
(n,(BCS (C,I))) is real V55() ext-real Element of REAL
((Euclid n),(BCS (C,I))) is real V55() ext-real Element of REAL
((degree I) / ((degree I) + 1)) |^ C is real V55() ext-real set
(((degree I) / ((degree I) + 1)) |^ C) * (n,I) is real V55() ext-real Element of REAL
degree (BCS (C,I)) is ext-real set
C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
BCS ((C + 1),I) is non void subset-closed finite-membered non with_non-empty_elements ( Euclid n) (n) SubdivisionStr of I
(n,(BCS ((C + 1),I))) is real V55() ext-real Element of REAL
((Euclid n),(BCS ((C + 1),I))) is real V55() ext-real Element of REAL
((degree I) / ((degree I) + 1)) |^ (C + 1) is real V55() ext-real set
(((degree I) / ((degree I) + 1)) |^ (C + 1)) * (n,I) is real V55() ext-real Element of REAL
degree (BCS ((C + 1),I)) is ext-real set
center_of_mass (TOP-REAL n) is Relation-like BOOL the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL n) -valued Function-like total quasi_total Element of bool [:(BOOL the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n):]
BOOL the carrier of (TOP-REAL n) is set
[:(BOOL the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n):] is Relation-like set
bool [:(BOOL the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n):] is non empty set
- 1 is real integer finite V55() ext-real non positive Element of REAL
carr is non void subset-closed finite-membered finite-degree non with_non-empty_elements ( Euclid n) (n) SimplicialComplexStr of the carrier of (TOP-REAL n)
degree carr is real integer finite V55() ext-real set
(n,carr) is real V55() ext-real Element of REAL
((Euclid n),carr) is real V55() ext-real Element of REAL
|.carr.| is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
[#] carr is non proper Element of bool the carrier of carr
the carrier of carr is set
bool the carrier of carr is non empty set
BCS carr is non void subset-closed finite-membered non with_non-empty_elements ( Euclid n) (n) SubdivisionStr of carr
subdivision ((center_of_mass (TOP-REAL n)),carr) is strict non void subset-closed finite-membered finite-degree non with_non-empty_elements SimplicialComplexStr of the carrier of (TOP-REAL n)
(degree carr) + 1 is real integer finite V55() ext-real Element of REAL
(degree carr) / ((degree carr) + 1) is real V55() ext-real Element of COMPLEX
K166(((degree carr) + 1)) is real V55() ext-real set
K164((degree carr),K166(((degree carr) + 1))) is real V55() ext-real set
((degree carr) / ((degree carr) + 1)) * (n,carr) is real V55() ext-real Element of REAL
dom (center_of_mass (TOP-REAL n)) is Element of bool (BOOL the carrier of (TOP-REAL n))
bool (BOOL the carrier of (TOP-REAL n)) is non empty set
(- 1) + 1 is real integer finite V55() ext-real Element of REAL
(- 1) + 1 is real integer finite V55() ext-real Element of REAL
((degree carr) + 1) / ((degree carr) + 1) is real V55() ext-real Element of COMPLEX
K164(((degree carr) + 1),K166(((degree carr) + 1))) is real V55() ext-real set
1 / ((degree carr) + 1) is real V55() ext-real Element of COMPLEX
K164(1,K166(((degree carr) + 1))) is real V55() ext-real set
(((degree carr) + 1) / ((degree carr) + 1)) - (1 / ((degree carr) + 1)) is real V55() ext-real Element of COMPLEX
K165((1 / ((degree carr) + 1))) is real V55() ext-real set
K163((((degree carr) + 1) / ((degree carr) + 1)),K165((1 / ((degree carr) + 1)))) is real V55() ext-real set
1 - (1 / ((degree carr) + 1)) is real V55() ext-real Element of REAL
K163(1,K165((1 / ((degree carr) + 1)))) is real V55() ext-real set
((degree I) + 1) / ((degree I) + 1) is real V55() ext-real Element of COMPLEX
K164(((degree I) + 1),K166(((degree I) + 1))) is real V55() ext-real set
1 / ((degree I) + 1) is real V55() ext-real Element of COMPLEX
K164(1,K166(((degree I) + 1))) is real V55() ext-real set
(((degree I) + 1) / ((degree I) + 1)) - (1 / ((degree I) + 1)) is real V55() ext-real Element of COMPLEX
K165((1 / ((degree I) + 1))) is real V55() ext-real set
K163((((degree I) + 1) / ((degree I) + 1)),K165((1 / ((degree I) + 1)))) is real V55() ext-real set
1 - (1 / ((degree I) + 1)) is real V55() ext-real Element of REAL
K163(1,K165((1 / ((degree I) + 1)))) is real V55() ext-real set
((degree I) / ((degree I) + 1)) * ((((degree I) / ((degree I) + 1)) |^ C) * (n,I)) is real V55() ext-real Element of REAL
((degree I) / ((degree I) + 1)) * (((degree I) / ((degree I) + 1)) |^ C) is real V55() ext-real set
K164(((degree I) / ((degree I) + 1)),(((degree I) / ((degree I) + 1)) |^ C)) is real V55() ext-real set
(((degree I) / ((degree I) + 1)) * (((degree I) / ((degree I) + 1)) |^ C)) * (n,I) is real V55() ext-real Element of REAL
((degree I) / ((degree I) + 1)) |^ {} is real V55() ext-real set
BCS ({},I) is non void subset-closed finite-membered non with_non-empty_elements ( Euclid n) (n) SubdivisionStr of I
(n,(BCS ({},I))) is real V55() ext-real Element of REAL
((Euclid n),(BCS ({},I))) is real V55() ext-real Element of REAL
(((degree I) / ((degree I) + 1)) |^ {}) * (n,I) is real V55() ext-real Element of REAL
degree (BCS ({},I)) is ext-real set
n is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative 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
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
T is non void subset-closed finite-membered finite-degree non with_non-empty_elements ( Euclid n) (n) SimplicialComplexStr of the carrier of (TOP-REAL n)
|.T.| is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
bool the carrier of (TOP-REAL n) is non empty set
[#] T is non proper Element of bool the carrier of T
the carrier of T is set
bool the carrier of T is non empty set
degree T is real integer finite V55() ext-real set
C is real V55() ext-real set
(degree T) + 1 is real integer finite V55() ext-real Element of REAL
(degree T) / ((degree T) + 1) is real V55() ext-real Element of COMPLEX
K166(((degree T) + 1)) is real V55() ext-real set
K164((degree T),K166(((degree T) + 1))) is real V55() ext-real set
- 1 is real integer finite V55() ext-real non positive Element of REAL
BCS T is non void subset-closed finite-membered non with_non-empty_elements ( Euclid n) (n) SubdivisionStr of T
(n,(BCS T)) is real V55() ext-real Element of REAL
((Euclid n),(BCS T)) is real V55() ext-real Element of REAL
(n,T) is real V55() ext-real Element of REAL
((Euclid n),T) is real V55() ext-real Element of REAL
((degree T) / ((degree T) + 1)) * (n,T) is real V55() ext-real Element of REAL
BCS (1,T) is non void subset-closed finite-membered non with_non-empty_elements ( Euclid n) (n) SubdivisionStr of T
(n,T) is real V55() ext-real Element of REAL
((Euclid n),T) is real V55() ext-real Element of REAL
BCS ({},T) is non void subset-closed finite-membered non with_non-empty_elements ( Euclid n) (n) SubdivisionStr of T
- 1 is real integer finite V55() ext-real non positive Element of REAL
(n,T) is real V55() ext-real Element of REAL
((Euclid n),T) is real V55() ext-real Element of REAL
(- 1) + 1 is real integer finite V55() ext-real Element of REAL
C / (n,T) is real V55() ext-real Element of COMPLEX
K166((n,T)) is real V55() ext-real set
K164(C,K166((n,T))) is real V55() ext-real set
C 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
((degree T) / ((degree T) + 1)) to_power C is real V55() ext-real set
(C / (n,T)) * (n,T) is real V55() ext-real Element of REAL
BCS (C,T) is non void subset-closed finite-membered non with_non-empty_elements ( Euclid n) (n) SubdivisionStr of T
(n,(BCS (C,T))) is real V55() ext-real Element of REAL
((Euclid n),(BCS (C,T))) is real V55() ext-real Element of REAL
((degree T) / ((degree T) + 1)) |^ C is real V55() ext-real set
(((degree T) / ((degree T) + 1)) |^ C) * (n,T) is real V55() ext-real Element of REAL
- 1 is real integer finite V55() ext-real non positive Element of REAL
(n,T) is real V55() ext-real Element of REAL
((Euclid n),T) is real V55() ext-real Element of REAL
n 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
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()
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
TOP-REAL T 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),(TOP-REAL T):] is non empty strict TopSpace-like TopStruct
the carrier of [:(TOP-REAL n),(TOP-REAL T):] is non empty set
n + T is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative Element of REAL
TOP-REAL (n + T) 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 + T)) is non empty set
[: the carrier of [:(TOP-REAL n),(TOP-REAL T):], the carrier of (TOP-REAL (n + T)):] is non empty Relation-like set
bool [: the carrier of [:(TOP-REAL n),(TOP-REAL T):], the carrier of (TOP-REAL (n + T)):] is non empty set
the carrier of (TOP-REAL n) is non empty set
the carrier of (TOP-REAL T) 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 the carrier of (TOP-REAL n) is non empty set
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
the topology of (TOP-REAL T) is non empty open Element of bool (bool the carrier of (TOP-REAL T))
bool the carrier of (TOP-REAL T) is non empty set
bool (bool the carrier of (TOP-REAL T)) is non empty set
TopStruct(# the carrier of (TOP-REAL T), the topology of (TOP-REAL T) #) is non empty strict TopSpace-like V426() TopStruct
the topology of (TOP-REAL (n + T)) is non empty open Element of bool (bool the carrier of (TOP-REAL (n + T)))
bool the carrier of (TOP-REAL (n + T)) is non empty set
bool (bool the carrier of (TOP-REAL (n + T))) is non empty set
TopStruct(# the carrier of (TOP-REAL (n + T)), the topology of (TOP-REAL (n + T)) #) is non empty strict TopSpace-like V426() TopStruct
Euclid T is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct
REAL T is non empty functional FinSequence-membered FinSequenceSet of REAL
T -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist T is non empty Relation-like [:(REAL T),(REAL T):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL T),(REAL T):],REAL:]
[:(REAL T),(REAL T):] is non empty Relation-like set
[:[:(REAL T),(REAL T):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[:(REAL T),(REAL T):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL T),(Pitag_dist T) #) is strict MetrStruct
TopSpaceMetr (Euclid T) is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
the carrier of (Euclid T) is non empty set
Family_open_set (Euclid T) is Element of bool (bool the carrier of (Euclid T))
bool the carrier of (Euclid T) is non empty set
bool (bool the carrier of (Euclid T)) is non empty set
TopStruct(# the carrier of (Euclid T),(Family_open_set (Euclid T)) #) is non empty strict TopStruct
Euclid (n + T) is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct
REAL (n + T) is non empty functional FinSequence-membered FinSequenceSet of REAL
(n + T) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist (n + T) is non empty Relation-like [:(REAL (n + T)),(REAL (n + T)):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL (n + T)),(REAL (n + T)):],REAL:]
[:(REAL (n + T)),(REAL (n + T)):] is non empty Relation-like set
[:[:(REAL (n + T)),(REAL (n + T)):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[:(REAL (n + T)),(REAL (n + T)):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL (n + T)),(Pitag_dist (n + T)) #) is strict MetrStruct
TopSpaceMetr (Euclid (n + T)) is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
the carrier of (Euclid (n + T)) is non empty set
Family_open_set (Euclid (n + T)) is Element of bool (bool the carrier of (Euclid (n + T)))
bool the carrier of (Euclid (n + T)) is non empty set
bool (bool the carrier of (Euclid (n + T))) is non empty set
TopStruct(# the carrier of (Euclid (n + T)),(Family_open_set (Euclid (n + T))) #) is non empty strict TopStruct
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
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
the carrier of (Euclid n) is non empty set
Family_open_set (Euclid n) is Element of bool (bool the carrier of (Euclid n))
bool the carrier of (Euclid n) is non empty set
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
[:TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),TopStruct(# the carrier of (TOP-REAL T), the topology of (TOP-REAL T) #):] is non empty strict TopSpace-like V426() TopStruct
the carrier of [:TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),TopStruct(# the carrier of (TOP-REAL T), the topology of (TOP-REAL T) #):] is non empty set
the carrier of TopStruct(# the carrier of (TOP-REAL (n + T)), the topology of (TOP-REAL (n + T)) #) is non empty set
[: the carrier of [:TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),TopStruct(# the carrier of (TOP-REAL T), the topology of (TOP-REAL T) #):], the carrier of TopStruct(# the carrier of (TOP-REAL (n + T)), the topology of (TOP-REAL (n + T)) #):] is non empty Relation-like set
bool [: the carrier of [:TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),TopStruct(# the carrier of (TOP-REAL T), the topology of (TOP-REAL T) #):], the carrier of TopStruct(# the carrier of (TOP-REAL (n + T)), the topology of (TOP-REAL (n + T)) #):] is non empty set
TRC is non empty Relation-like the carrier of [:TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),TopStruct(# the carrier of (TOP-REAL T), the topology of (TOP-REAL T) #):] -defined the carrier of TopStruct(# the carrier of (TOP-REAL (n + T)), the topology of (TOP-REAL (n + T)) #) -valued Function-like total quasi_total Element of bool [: the carrier of [:TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),TopStruct(# the carrier of (TOP-REAL T), the topology of (TOP-REAL T) #):], the carrier of TopStruct(# the carrier of (TOP-REAL (n + T)), the topology of (TOP-REAL (n + T)) #):]
dom TRC is non empty Element of bool the carrier of [:TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),TopStruct(# the carrier of (TOP-REAL T), the topology of (TOP-REAL T) #):]
bool the carrier of [:TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),TopStruct(# the carrier of (TOP-REAL T), the topology of (TOP-REAL T) #):] is non empty set
rng TRC is non empty Element of bool the carrier of TopStruct(# the carrier of (TOP-REAL (n + T)), the topology of (TOP-REAL (n + T)) #)
bool the carrier of TopStruct(# the carrier of (TOP-REAL (n + T)), the topology of (TOP-REAL (n + T)) #) is non empty set
[#] TopStruct(# the carrier of (TOP-REAL (n + T)), the topology of (TOP-REAL (n + T)) #) is non empty non proper open closed Element of bool the carrier of TopStruct(# the carrier of (TOP-REAL (n + T)), the topology of (TOP-REAL (n + T)) #)
[#] (TOP-REAL (n + T)) 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 + T))
[#] [:(TOP-REAL n),(TOP-REAL T):] is non empty non proper open closed Element of bool the carrier of [:(TOP-REAL n),(TOP-REAL T):]
bool the carrier of [:(TOP-REAL n),(TOP-REAL T):] is non empty set
[#] (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)
[#] (TOP-REAL T) 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 T)
[:([#] (TOP-REAL n)),([#] (TOP-REAL T)):] is non empty Relation-like Element of bool the carrier of [:(TOP-REAL n),(TOP-REAL T):]
[:(TOP-REAL n),(TOP-REAL T):] | ([#] [:(TOP-REAL n),(TOP-REAL T):]) is non empty strict TopSpace-like SubSpace of [:(TOP-REAL n),(TOP-REAL T):]
(TOP-REAL n) | ([#] (TOP-REAL n)) is non empty strict TopSpace-like with_finite_small_inductive_dimension SubSpace of TOP-REAL n
(TOP-REAL T) | ([#] (TOP-REAL T)) is non empty strict TopSpace-like with_finite_small_inductive_dimension SubSpace of TOP-REAL T
[:((TOP-REAL n) | ([#] (TOP-REAL n))),((TOP-REAL T) | ([#] (TOP-REAL T))):] is non empty strict TopSpace-like TopStruct
[:TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),((TOP-REAL T) | ([#] (TOP-REAL T))):] is non empty strict TopSpace-like TopStruct
carr is non empty Relation-like the carrier of [:(TOP-REAL n),(TOP-REAL T):] -defined the carrier of (TOP-REAL (n + T)) -valued Function-like total quasi_total Element of bool [: the carrier of [:(TOP-REAL n),(TOP-REAL T):], the carrier of (TOP-REAL (n + T)):]
f is Element of bool the carrier of [:(TOP-REAL n),(TOP-REAL T):]
Cl f is closed Element of bool the carrier of [:(TOP-REAL n),(TOP-REAL T):]
carr .: (Cl f) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL (n + T))
TRC .: f is Element of bool the carrier of TopStruct(# the carrier of (TOP-REAL (n + T)), the topology of (TOP-REAL (n + T)) #)
Cl (TRC .: f) is closed Element of bool the carrier of TopStruct(# the carrier of (TOP-REAL (n + T)), the topology of (TOP-REAL (n + T)) #)
carr .: f is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL (n + T))
Cl (carr .: f) is closed with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL (n + T))
dom carr is non empty Element of bool the carrier of [:(TOP-REAL n),(TOP-REAL T):]
f is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
R is Relation-like NAT -defined REAL -valued Function-like finite T -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL T)
carr . (f,R) is set
f ^ R is Relation-like NAT -defined Function-like finite K240(n,T) -element FinSequence-like FinSubsequence-like set
K240(n,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,R] is Element of the carrier of [:(TOP-REAL n),(TOP-REAL T):]
{f,R} is non empty functional finite finite-membered set
{f} is non empty trivial functional finite finite-membered 1 -element set
{{f,R},{f}} is non empty finite finite-membered set
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
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
the carrier of (Euclid n) is non empty set
Family_open_set (Euclid n) is Element of bool (bool the carrier of (Euclid n))
bool the carrier of (Euclid n) is non empty set
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
[#] (TopSpaceMetr (Euclid n)) is non empty non proper open closed Element of bool the carrier of (TopSpaceMetr (Euclid n))
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
bool the carrier of (TopSpaceMetr (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
n 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
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()
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
TOP-REAL T 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),(TOP-REAL T):] is non empty strict TopSpace-like TopStruct
the carrier of [:(TOP-REAL n),(TOP-REAL T):] is non empty set
n + T is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative Element of REAL
TOP-REAL (n + T) 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 + T)) is non empty set
[: the carrier of [:(TOP-REAL n),(TOP-REAL T):], the carrier of (TOP-REAL (n + T)):] is non empty Relation-like set
bool [: the carrier of [:(TOP-REAL n),(TOP-REAL T):], the carrier of (TOP-REAL (n + T)):] is non empty set
the carrier of (TOP-REAL n) is non empty set
the carrier of (TOP-REAL T) 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
the carrier of (Euclid n) is non empty set
Euclid T is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct
REAL T is non empty functional FinSequence-membered FinSequenceSet of REAL
T -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist T is non empty Relation-like [:(REAL T),(REAL T):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL T),(REAL T):],REAL:]
[:(REAL T),(REAL T):] is non empty Relation-like set
[:[:(REAL T),(REAL T):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[:(REAL T),(REAL T):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL T),(Pitag_dist T) #) is strict MetrStruct
the carrier of (Euclid T) is non empty set
Euclid (n + T) is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct
REAL (n + T) is non empty functional FinSequence-membered FinSequenceSet of REAL
(n + T) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist (n + T) is non empty Relation-like [:(REAL (n + T)),(REAL (n + T)):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL (n + T)),(REAL (n + T)):],REAL:]
[:(REAL (n + T)),(REAL (n + T)):] is non empty Relation-like set
[:[:(REAL (n + T)),(REAL (n + T)):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[:(REAL (n + T)),(REAL (n + T)):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL (n + T)),(Pitag_dist (n + T)) #) is strict MetrStruct
the carrier of (Euclid (n + T)) is non empty set
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 the carrier of (Euclid n) is non empty set
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
TopSpaceMetr (Euclid T) is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
Family_open_set (Euclid T) is Element of bool (bool the carrier of (Euclid T))
bool the carrier of (Euclid T) is non empty set
bool (bool the carrier of (Euclid T)) is non empty set
TopStruct(# the carrier of (Euclid T),(Family_open_set (Euclid T)) #) is non empty strict TopStruct
I is non empty Relation-like the carrier of [:(TOP-REAL n),(TOP-REAL T):] -defined the carrier of (TOP-REAL (n + T)) -valued Function-like total quasi_total Element of bool [: the carrier of [:(TOP-REAL n),(TOP-REAL T):], the carrier of (TOP-REAL (n + T)):]
C is real V55() ext-real set
E is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
OpenHypercube (E,C) is open Element of bool the carrier of (TopSpaceMetr (Euclid n))
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
bool the carrier of (TopSpaceMetr (Euclid n)) is non empty set
C is Relation-like NAT -defined REAL -valued Function-like finite T -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid T)
E ^ C is Relation-like NAT -defined Function-like finite K240(n,T) -element FinSequence-like FinSubsequence-like set
K240(n,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
OpenHypercube (C,C) is open Element of bool the carrier of (TopSpaceMetr (Euclid T))
the carrier of (TopSpaceMetr (Euclid T)) is non empty set
bool the carrier of (TopSpaceMetr (Euclid T)) is non empty set
[:(OpenHypercube (E,C)),(OpenHypercube (C,C)):] is Relation-like Element of bool the carrier of [:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid T)):]
[:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid T)):] is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
the carrier of [:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid T)):] is non empty set
bool the carrier of [:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid T)):] is non empty set
I .: [:(OpenHypercube (E,C)),(OpenHypercube (C,C)):] is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL (n + T))
bool the carrier of (TOP-REAL (n + T)) is non empty set
n1 is Relation-like NAT -defined REAL -valued Function-like finite n + T -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid (n + T))
OpenHypercube (n1,C) is open Element of bool the carrier of (TopSpaceMetr (Euclid (n + T)))
TopSpaceMetr (Euclid (n + T)) 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 + T)) is Element of bool (bool the carrier of (Euclid (n + T)))
bool the carrier of (Euclid (n + T)) is non empty set
bool (bool the carrier of (Euclid (n + T))) is non empty set
TopStruct(# the carrier of (Euclid (n + T)),(Family_open_set (Euclid (n + T))) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr (Euclid (n + T))) is non empty set
bool the carrier of (TopSpaceMetr (Euclid (n + T))) is non empty set
Intervals (E,C) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Intervals (C,C) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Intervals (n1,C) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (Intervals (E,C)) is set
[#] (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)
bool the carrier of (TOP-REAL n) is non empty set
[#] (TopSpaceMetr (Euclid n)) is non empty non proper open closed Element of bool the carrier of (TopSpaceMetr (Euclid n))
[#] (TOP-REAL T) 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 T)
bool the carrier of (TOP-REAL T) is non empty set
[#] (TopSpaceMetr (Euclid T)) is non empty non proper open closed Element of bool the carrier of (TopSpaceMetr (Euclid T))
product (Intervals (C,C)) is set
(Intervals (E,C)) ^ (Intervals (C,C)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
[:(product (Intervals (E,C))),(product (Intervals (C,C))):] is Relation-like set
I .: [:(product (Intervals (E,C))),(product (Intervals (C,C))):] is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL (n + T))
product (Intervals (n1,C)) is set
f is set
dom I is non empty Element of bool the carrier of [:(TOP-REAL n),(TOP-REAL T):]
bool the carrier of [:(TOP-REAL n),(TOP-REAL T):] is non empty set
R is set
I . R is set
G is set
G0 is set
[G,G0] is set
{G,G0} is non empty finite set
{G} is non empty trivial finite 1 -element set
{{G,G0},{G}} is non empty finite finite-membered set
p is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
h is Relation-like NAT -defined REAL -valued Function-like finite T -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL T)
I . (p,h) is set
p ^ h is Relation-like NAT -defined Function-like finite K240(n,T) -element FinSequence-like FinSubsequence-like set
f is set
R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
R ^ G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
[R,G] is set
{R,G} is non empty functional finite finite-membered set
{R} is non empty trivial functional finite finite-membered 1 -element set
{{R,G},{R}} is non empty finite finite-membered set
[:([#] (TOP-REAL n)),([#] (TOP-REAL T)):] is non empty Relation-like Element of bool the carrier of [:(TOP-REAL n),(TOP-REAL T):]
bool the carrier of [:(TOP-REAL n),(TOP-REAL T):] is non empty set
[#] [:(TOP-REAL n),(TOP-REAL T):] is non empty non proper open closed Element of bool the carrier of [:(TOP-REAL n),(TOP-REAL T):]
dom I is non empty Element of bool the carrier of [:(TOP-REAL n),(TOP-REAL T):]
I . (R,G) is set
I . [R,G] is set
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
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
the carrier of (Euclid n) is non empty set
T is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
bool the carrier of (Euclid n) is non empty set
I is Element of bool the carrier of (Euclid n)
the Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
C is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
the real V55() ext-real set is real V55() ext-real set
E is real V55() ext-real set
OpenHypercube (C,E) is open Element of bool the carrier of (TopSpaceMetr (Euclid n))
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
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
bool the carrier of (TopSpaceMetr (Euclid n)) is non empty set
C is set
C is real V55() ext-real Element of REAL
E is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
C + 1 is real V55() ext-real Element of REAL
n1 is real V55() ext-real Element of REAL
OpenHypercube (E,n1) is open Element of bool the carrier of (TopSpaceMetr (Euclid n))
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
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
bool the carrier of (TopSpaceMetr (Euclid n)) is non empty set
Ball (E,n1) is bounded Element of bool the carrier of (Euclid n)
c is set
TRC is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
dist (E,TRC) is real V55() ext-real non negative Element of REAL
the distance of (Euclid n) is non empty Relation-like [: the carrier of (Euclid n), the carrier of (Euclid n):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:]
[: the carrier of (Euclid n), the carrier of (Euclid n):] is non empty Relation-like set
[:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:] is non empty non trivial non finite set
the distance of (Euclid n) . (E,TRC) is real V55() ext-real Element of REAL
C is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
E is real V55() ext-real set
OpenHypercube (C,E) is open Element of bool the carrier of (TopSpaceMetr (Euclid n))
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
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
bool the carrier of (TopSpaceMetr (Euclid n)) is non empty 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 Element of bool REAL
I is Element of bool the carrier of (Euclid n)
sqrt n is real V55() ext-real set
E * (sqrt n) is real V55() ext-real set
K164(E,(sqrt n)) is real V55() ext-real set
Ball (C,(E * (sqrt n))) is bounded Element of bool the carrier of (Euclid n)
I is Element of bool the carrier of (Euclid n)
bool the carrier of (TOP-REAL 1) is non empty set
T is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL 1)
I is real V55() ext-real Element of REAL
- I is real V55() ext-real Element of REAL
[.(- I),I.] is complex-membered ext-real-membered real-membered interval Element of bool REAL
E is non empty Relation-like the carrier of (TOP-REAL 1) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TOP-REAL 1), the carrier of R^1:]
rng E is non empty complex-membered ext-real-membered real-membered Element of bool REAL
[#] R^1 is non empty non proper open closed complex-membered ext-real-membered real-membered Element of bool the carrier of R^1
E /" is non empty Relation-like the carrier of R^1 -defined the carrier of (TOP-REAL 1) -valued Function-like total quasi_total Element of bool [: the carrier of R^1, the carrier of (TOP-REAL 1):]
[: the carrier of R^1, the carrier of (TOP-REAL 1):] is non empty Relation-like set
bool [: the carrier of R^1, the carrier of (TOP-REAL 1):] is non empty set
C is Relation-like Function-like one-to-one set
C " is Relation-like Function-like one-to-one set
C is complex-membered ext-real-membered real-membered Element of bool the carrier of R^1
(E /") .: C is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL 1)
C " C is set
dom E is non empty with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL 1)
[#] (TOP-REAL 1) 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 1)
n1 is set
c is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V93() V94() V95() V97() V98() V99() V100() Element of the carrier of (TOP-REAL 1)
c . 1 is real V55() ext-real set
len c 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 . 1)*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like set
|.c.| is real V55() ext-real non negative Element of REAL
K510(c) is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V93() V94() V95() V97() V98() V99() V100() FinSequence of REAL
Sum K510(c) is real V55() ext-real Element of REAL
sqrt (Sum K510(c)) is real V55() ext-real Element of REAL
abs (c . 1) is real V55() ext-real Element of REAL
Seg 1 is non empty trivial finite 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 Element of bool NAT
dom c is non empty trivial finite 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 Element of bool NAT
c /. 1 is real V55() ext-real Element of REAL
E . c is real V55() ext-real Element of the carrier of R^1
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
bool the carrier of (TOP-REAL n) is non empty set
T is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
TOP-REAL T 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 T) is non empty set
bool the carrier of (TOP-REAL T) is non empty set
T + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
TOP-REAL (T + 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 (T + 1)) is non empty set
bool the carrier of (TOP-REAL (T + 1)) is non empty set
I is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL (T + 1))
n1 is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL (T + 1))
Euclid (T + 1) is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct
REAL (T + 1) is non empty functional FinSequence-membered FinSequenceSet of REAL
(T + 1) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist (T + 1) is non empty Relation-like [:(REAL (T + 1)),(REAL (T + 1)):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL (T + 1)),(REAL (T + 1)):],REAL:]
[:(REAL (T + 1)),(REAL (T + 1)):] is non empty Relation-like set
[:[:(REAL (T + 1)),(REAL (T + 1)):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[:(REAL (T + 1)),(REAL (T + 1)):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL (T + 1)),(Pitag_dist (T + 1)) #) is strict MetrStruct
the carrier of (Euclid (T + 1)) is non empty set
c is Relation-like NAT -defined REAL -valued Function-like finite T + 1 -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid (T + 1))
TRC is real V55() ext-real set
OpenHypercube (c,TRC) is open Element of bool the carrier of (TopSpaceMetr (Euclid (T + 1)))
TopSpaceMetr (Euclid (T + 1)) is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
Family_open_set (Euclid (T + 1)) is Element of bool (bool the carrier of (Euclid (T + 1)))
bool the carrier of (Euclid (T + 1)) is non empty set
bool (bool the carrier of (Euclid (T + 1))) is non empty set
TopStruct(# the carrier of (Euclid (T + 1)),(Family_open_set (Euclid (T + 1))) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr (Euclid (T + 1))) is non empty set
bool the carrier of (TopSpaceMetr (Euclid (T + 1))) is non empty set
[:(TOP-REAL T),(TOP-REAL 1):] is non empty strict TopSpace-like TopStruct
the carrier of [:(TOP-REAL T),(TOP-REAL 1):] is non empty set
[: the carrier of [:(TOP-REAL T),(TOP-REAL 1):], the carrier of (TOP-REAL (T + 1)):] is non empty Relation-like set
bool [: the carrier of [:(TOP-REAL T),(TOP-REAL 1):], the carrier of (TOP-REAL (T + 1)):] is non empty set
carr is non empty Relation-like the carrier of [:(TOP-REAL T),(TOP-REAL 1):] -defined the carrier of (TOP-REAL (T + 1)) -valued Function-like total quasi_total Element of bool [: the carrier of [:(TOP-REAL T),(TOP-REAL 1):], the carrier of (TOP-REAL (T + 1)):]
dom carr is non empty Element of bool the carrier of [:(TOP-REAL T),(TOP-REAL 1):]
bool the carrier of [:(TOP-REAL T),(TOP-REAL 1):] is non empty set
[#] [:(TOP-REAL T),(TOP-REAL 1):] is non empty non proper open closed Element of bool the carrier of [:(TOP-REAL T),(TOP-REAL 1):]
len c 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 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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
R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len R 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 ^ R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng c is finite complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded Element of bool REAL
Euclid T is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct
REAL T is non empty functional FinSequence-membered FinSequenceSet of REAL
T -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist T is non empty Relation-like [:(REAL T),(REAL T):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL T),(REAL T):],REAL:]
[:(REAL T),(REAL T):] is non empty Relation-like set
[:[:(REAL T),(REAL T):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[:(REAL T),(REAL T):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL T),(Pitag_dist T) #) is strict MetrStruct
the carrier of (Euclid T) is non empty set
Euclid 1 is non empty strict Reflexive discerning V181() triangle V221() V222() MetrStruct
REAL 1 is non empty functional FinSequence-membered FinSequenceSet of REAL
1 -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist 1 is non empty Relation-like [:(REAL 1),(REAL 1):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[:(REAL 1),(REAL 1):],REAL:]
[:(REAL 1),(REAL 1):] is non empty Relation-like set
[:[:(REAL 1),(REAL 1):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[:(REAL 1),(REAL 1):],REAL:] is non empty non trivial non finite set
MetrStruct(# (REAL 1),(Pitag_dist 1) #) is strict MetrStruct
the carrier of (Euclid 1) is non empty set
G is Relation-like NAT -defined REAL -valued Function-like finite T -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid T)
sqrt T is real V55() ext-real set
TRC * (sqrt T) is real V55() ext-real set
K164(TRC,(sqrt T)) is real V55() ext-real set
cl_Ball (G,(TRC * (sqrt T))) is Element of bool the carrier of (Euclid T)
bool the carrier of (Euclid T) is non empty set
G0 is non empty trivial Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite 1 -element FinSequence-like FinSubsequence-like V93() V94() V95() V97() V98() V99() V100() Element of the carrier of (Euclid 1)
sqrt 1 is real V55() ext-real Element of REAL
TRC * (sqrt 1) is real V55() ext-real Element of REAL
cl_Ball (G0,(TRC * (sqrt 1))) is Element of bool the carrier of (Euclid 1)
bool the carrier of (Euclid 1) is non empty set
Ball (G0,(TRC * (sqrt 1))) is bounded Element of bool the carrier of (Euclid 1)
h is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL 1)
OpenHypercube (G0,TRC) is open Element of bool the carrier of (TopSpaceMetr (Euclid 1))
TopSpaceMetr (Euclid 1) is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
Family_open_set (Euclid 1) is Element of bool (bool the carrier of (Euclid 1))
bool (bool the carrier of (Euclid 1)) is non empty set
TopStruct(# the carrier of (Euclid 1),(Family_open_set (Euclid 1)) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr (Euclid 1)) is non empty set
bool the carrier of (TopSpaceMetr (Euclid 1)) is non empty set
Ball (G,(TRC * (sqrt T))) is bounded Element of bool the carrier of (Euclid T)
p is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL T)
OpenHypercube (G,TRC) is open Element of bool the carrier of (TopSpaceMetr (Euclid T))
TopSpaceMetr (Euclid T) is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
Family_open_set (Euclid T) is Element of bool (bool the carrier of (Euclid T))
bool (bool the carrier of (Euclid T)) is non empty set
TopStruct(# the carrier of (Euclid T),(Family_open_set (Euclid T)) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr (Euclid T)) is non empty set
bool the carrier of (TopSpaceMetr (Euclid T)) is non empty set
[:(OpenHypercube (G,TRC)),(OpenHypercube (G0,TRC)):] is Relation-like Element of bool the carrier of [:(TopSpaceMetr (Euclid T)),(TopSpaceMetr (Euclid 1)):]
[:(TopSpaceMetr (Euclid T)),(TopSpaceMetr (Euclid 1)):] is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
the carrier of [:(TopSpaceMetr (Euclid T)),(TopSpaceMetr (Euclid 1)):] is non empty set
bool the carrier of [:(TopSpaceMetr (Euclid T)),(TopSpaceMetr (Euclid 1)):] is non empty set
[:p,h:] is Relation-like Element of bool the carrier of [:(TOP-REAL T),(TOP-REAL 1):]
rng carr is non empty with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL (T + 1))
[#] (TOP-REAL (T + 1)) 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 (T + 1))
carr " n1 is Element of bool the carrier of [:(TOP-REAL T),(TOP-REAL 1):]
carr .: (carr " n1) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL (T + 1))
carr .: [:(OpenHypercube (G,TRC)),(OpenHypercube (G0,TRC)):] is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL (T + 1))
TOP-REAL {} is non empty trivial finite 1 -element TopSpace-like compact V126() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict V191() V192() V221() V222() real-membered finite-dimensional with_finite_small_inductive_dimension L15()
the carrier of (TOP-REAL {}) is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered left_end right_end bounded_below bounded_above real-bounded set
bool the carrier of (TOP-REAL {}) is non empty finite finite-membered set
T is trivial finite compact complex-membered ext-real-membered real-membered bounded_below bounded_above real-bounded with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL {})
T is with_finite_small_inductive_dimension Element of bool 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()
the carrier of (TOP-REAL n) is non empty set
bool the carrier of (TOP-REAL n) is non empty set
T is with_finite_small_inductive_dimension Element of bool 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()
the carrier of (TOP-REAL n) is non empty set
bool the carrier of (TOP-REAL n) is non empty set
T is finite compact affinely-independent with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv T is closed convex convex with_finite_small_inductive_dimension Element of bool 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()
the carrier of (TOP-REAL n) is non empty set
bool the carrier of (TOP-REAL n) is non empty set
I is non empty finite compact affinely-independent with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv I is non empty closed compact convex convex with_finite_small_inductive_dimension with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
(TOP-REAL n) | (conv I) is non empty strict TopSpace-like with_finite_small_inductive_dimension SubSpace of TOP-REAL n
the carrier of ((TOP-REAL n) | (conv I)) is non empty set
bool the carrier of ((TOP-REAL n) | (conv I)) is non empty Element of bool (bool the carrier of ((TOP-REAL n) | (conv I)))
bool the carrier of ((TOP-REAL n) | (conv I)) is non empty set
bool (bool the carrier of ((TOP-REAL n) | (conv I))) is non empty set
card I 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
E is Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I
C is Relation-like NAT -defined bool the carrier of ((TOP-REAL n) | (conv I)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool the carrier of ((TOP-REAL n) | (conv I))
len C 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
rng C is finite V365( the carrier of ((TOP-REAL n) | (conv I))) Element of bool (bool the carrier of ((TOP-REAL n) | (conv I)))
bool (bool the carrier of ((TOP-REAL n) | (conv I))) is non empty set
dom C 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
bool (dom C) is non empty finite finite-membered set
meet (rng C) is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | (conv I))
rng E is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
len 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 NAT
dom E 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
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
{I} is non empty trivial finite finite-membered 1 -element affinely-independent 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 {I} 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 ( Euclid n) (n) SimplicialComplexStr of the carrier of (TOP-REAL n)
subset-closed_closure_of {I} 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 {I}) #) is non empty strict TopStruct
E " is Relation-like Function-like one-to-one set
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
the carrier of (Euclid n) is non empty set
Family_open_set (Euclid n) is Element of bool (bool the carrier of (Euclid n))
bool the carrier of (Euclid n) is non empty set
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
the topology of (TOP-REAL n) is non empty open Element of bool (bool the carrier of (TOP-REAL n))
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like V426() TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
bool the carrier of (TopSpaceMetr (Euclid n)) is non empty set
TRC is non empty Element of bool the carrier of (TopSpaceMetr (Euclid n))
(TopSpaceMetr (Euclid n)) | TRC is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable SubSpace of TopSpaceMetr (Euclid n)
carr is non empty Element of bool the carrier of (Euclid n)
(Euclid n) | carr is non empty strict Reflexive discerning V181() triangle SubSpace of Euclid n
TopSpaceMetr ((Euclid n) | carr) is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
the carrier of ((Euclid n) | carr) is non empty set
Family_open_set ((Euclid n) | carr) is Element of bool (bool the carrier of ((Euclid n) | carr))
bool the carrier of ((Euclid n) | carr) is non empty set
bool (bool the carrier of ((Euclid n) | carr)) is non empty set
TopStruct(# the carrier of ((Euclid n) | carr),(Family_open_set ((Euclid n) | carr)) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr ((Euclid n) | carr)) is non empty set
bool the carrier of (TopSpaceMetr ((Euclid n) | carr)) is non empty set
bool (bool the carrier of (TopSpaceMetr ((Euclid n) | carr))) is non empty set
COMPLEMENT (rng C) is Element of bool (bool the carrier of ((TOP-REAL n) | (conv I)))
[#] ((TOP-REAL n) | (conv I)) is non empty non proper open closed with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | (conv I))
(meet (rng C)) ` is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | (conv I))
the carrier of ((TOP-REAL n) | (conv I)) \ (meet (rng C)) is set
f is Element of bool (bool the carrier of (TopSpaceMetr ((Euclid n) | carr)))
union f is Element of bool the carrier of (TopSpaceMetr ((Euclid n) | carr))
the non empty real V55() ext-real positive non negative ((Euclid n) | carr,f) is non empty real V55() ext-real positive non negative ((Euclid n) | carr,f)
|.(Complex_of {I}).| is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
[#] (Complex_of {I}) is non proper Element of bool the carrier of (Complex_of {I})
the carrier of (Complex_of {I}) is set
bool the carrier of (Complex_of {I}) is non empty set
G is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
BCS (G,(Complex_of {I})) is non void subset-closed finite-membered finite-degree finite-vertices locally-finite non with_non-empty_elements total affinely-independent simplex-join-closed ( Euclid n) (n) SubdivisionStr of Complex_of {I}
(n,(BCS (G,(Complex_of {I})))) is real V55() ext-real Element of REAL
((Euclid n),(BCS (G,(Complex_of {I})))) is real V55() ext-real Element of REAL
|.(BCS (G,(Complex_of {I}))).| is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
the topology of (Complex_of {I}) is finite finite-membered V365( the carrier of (Complex_of {I})) open Element of bool (bool the carrier of (Complex_of {I}))
bool (bool the carrier of (Complex_of {I})) is non empty set
bool I is non empty finite finite-membered V365(I) Element of bool (bool I)
bool I is non empty finite finite-membered set
bool (bool I) is non empty finite finite-membered set
Vertices (BCS (G,(Complex_of {I}))) is Element of bool the carrier of (BCS (G,(Complex_of {I})))
the carrier of (BCS (G,(Complex_of {I}))) is set
bool the carrier of (BCS (G,(Complex_of {I}))) is non empty set
p is set
h is Element of the carrier of (BCS (G,(Complex_of {I})))
h is Element of bool the carrier of (BCS (G,(Complex_of {I})))
@ h is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (@ h) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
gx is Element of bool the carrier of (Complex_of {I})
@ gx is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
Int (@ gx) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (@ gx) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
E " gx 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
E .: (E " gx) is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
C .: (E " gx) is finite V365( the carrier of ((TOP-REAL n) | (conv I))) Element of bool (bool the carrier of ((TOP-REAL n) | (conv I)))
union (C .: (E " gx)) is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | (conv I))
cgx is set
GX is set
C . GX is set
E . GX is set
I is set
(E ") . I is set
C . ((E ") . I) is set
t is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv t is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
y is open Element of bool the carrier of (Complex_of {I})
@ y is finite compact affinely-independent with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (@ y) is closed compact convex convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
[:(Vertices (BCS (G,(Complex_of {I})))),I:] is Relation-like set
bool [:(Vertices (BCS (G,(Complex_of {I})))),I:] is non empty set
p is Relation-like Vertices (BCS (G,(Complex_of {I}))) -defined I -valued Function-like total quasi_total Element of bool [:(Vertices (BCS (G,(Complex_of {I})))),I:]
h is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
h is Element of Vertices (BCS (G,(Complex_of {I})))
conv h is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
p . h is set
(card I) - 1 is real integer finite V55() ext-real Element of REAL
K163((card I),K165(1)) is real integer finite V55() ext-real set
h is finite open Simplex of (card I) - 1, BCS (G,(Complex_of {I}))
p .: h is finite Element of bool I
[#] (BCS (G,(Complex_of {I}))) is non proper Element of bool the carrier of (BCS (G,(Complex_of {I})))
gx is set
@ h is finite compact affinely-independent with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (@ h) is closed compact convex convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
cgx is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
h is Element of bool the carrier of (Euclid n)
GX is Element of the carrier of ((Euclid n) | carr)
Ball (GX, the non empty real V55() ext-real positive non negative ((Euclid n) | carr,f)) is bounded Element of bool the carrier of ((Euclid n) | carr)
I is Element of bool the carrier of (TopSpaceMetr ((Euclid n) | carr))
I ` is Element of bool the carrier of (TopSpaceMetr ((Euclid n) | carr))
the carrier of (TopSpaceMetr ((Euclid n) | carr)) \ I is set
t is set
C . t is set
E . t is set
dom p is Element of bool (Vertices (BCS (G,(Complex_of {I}))))
bool (Vertices (BCS (G,(Complex_of {I})))) is non empty set
y is set
p . y is set
[#] ((Euclid n) | carr) is non empty non proper Element of bool the carrier of ((Euclid n) | carr)
x is bounded Element of bool the carrier of (Euclid n)
diameter x is real V55() ext-real Element of REAL
(E ") . (p . y) is set
C . ((E ") . (p . y)) is set
i1 is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (Euclid n)
cl_Ball (cgx,(diameter x)) is Element of bool the carrier of (Euclid n)
dist (cgx,i1) is real V55() ext-real non negative Element of REAL
the distance of (Euclid n) is non empty Relation-like [: the carrier of (Euclid n), the carrier of (Euclid n):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:]
[: the carrier of (Euclid n), the carrier of (Euclid n):] is non empty Relation-like set
[:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[: the carrier of (Euclid n), the carrier of (Euclid n):],REAL:] is non empty non trivial non finite set
the distance of (Euclid n) . (cgx,i1) is real V55() ext-real Element of REAL
i2 is Element of the carrier of ((Euclid n) | carr)
dist (GX,i2) is real V55() ext-real non negative Element of REAL
the distance of ((Euclid n) | carr) is non empty Relation-like [: the carrier of ((Euclid n) | carr), the carrier of ((Euclid n) | carr):] -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [:[: the carrier of ((Euclid n) | carr), the carrier of ((Euclid n) | carr):],REAL:]
[: the carrier of ((Euclid n) | carr), the carrier of ((Euclid n) | carr):] is non empty Relation-like set
[:[: the carrier of ((Euclid n) | carr), the carrier of ((Euclid n) | carr):],REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [:[: the carrier of ((Euclid n) | carr), the carrier of ((Euclid n) | carr):],REAL:] is non empty non trivial non finite set
the distance of ((Euclid n) | carr) . (GX,i2) 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
bool the carrier of (TOP-REAL n) is non empty set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
I is finite compact affinely-independent with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
card I 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
conv I is closed compact convex convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
(TOP-REAL n) | (conv I) is strict TopSpace-like with_finite_small_inductive_dimension SubSpace of TOP-REAL n
the carrier of ((TOP-REAL n) | (conv I)) is set
[: the carrier of ((TOP-REAL n) | (conv I)), the carrier of ((TOP-REAL n) | (conv I)):] is Relation-like set
bool [: the carrier of ((TOP-REAL n) | (conv I)), the carrier of ((TOP-REAL n) | (conv I)):] is non empty set
E is Relation-like the carrier of ((TOP-REAL n) | (conv I)) -defined the carrier of ((TOP-REAL n) | (conv I)) -valued Function-like total quasi_total continuous Element of bool [: the carrier of ((TOP-REAL n) | (conv I)), the carrier of ((TOP-REAL n) | (conv I)):]
dom E is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | (conv I))
bool the carrier of ((TOP-REAL n) | (conv I)) is non empty set
C is non empty with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
(TOP-REAL n) | C is non empty strict TopSpace-like with_finite_small_inductive_dimension SubSpace of TOP-REAL n
the carrier of ((TOP-REAL n) | C) is non empty set
[: the carrier of ((TOP-REAL n) | C), the carrier of ((TOP-REAL n) | C):] is non empty Relation-like set
bool [: the carrier of ((TOP-REAL n) | C), the carrier of ((TOP-REAL n) | C):] is non empty set
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I is Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I
{ b₁ where b₁ is Element of the carrier of ((TOP-REAL n) | C) : (|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . a₁))) . (E . b₁) <= (|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . a₁))) . b₁ } is set
carr is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len carr 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 carr 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
rng carr is finite set
bool the carrier of ((TOP-REAL n) | C) is non empty Element of bool (bool the carrier of ((TOP-REAL n) | C))
bool the carrier of ((TOP-REAL n) | C) is non empty set
bool (bool the carrier of ((TOP-REAL n) | C)) is non empty set
f is set
R is set
carr . R is set
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . R is set
|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . R)) is non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TOP-REAL n), the carrier of R^1:]
[: the carrier of (TOP-REAL n), the carrier of R^1:] is non empty Relation-like V93() V94() V95() set
bool [: the carrier of (TOP-REAL n), the carrier of R^1:] is non empty set
{ b₁ where b₁ is Element of the carrier of ((TOP-REAL n) | C) : (|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . R))) . (E . b₁) <= (|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . R))) . b₁ } is set
G is set
G0 is Element of the carrier of ((TOP-REAL n) | C)
E . G0 is set
(|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . R))) . (E . G0) is real V55() ext-real set
(|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . R))) . G0 is real V55() ext-real set
[#] ((TOP-REAL n) | C) is non empty non proper open closed with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
G is real V55() ext-real set
].-infty,G.] is complex-membered ext-real-membered real-membered non left_end interval Element of bool REAL
R is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
f is Relation-like NAT -defined bool the carrier of ((TOP-REAL n) | C) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool the carrier of ((TOP-REAL n) | C)
rng f is finite V365( the carrier of ((TOP-REAL n) | C)) Element of bool (bool the carrier of ((TOP-REAL n) | C))
bool (bool the carrier of ((TOP-REAL n) | C)) is non empty set
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
p is set
f . p is set
[: the carrier of (TOP-REAL n), the carrier of R^1:] is non empty Relation-like V93() V94() V95() set
bool [: the carrier of (TOP-REAL n), the carrier of R^1:] is non empty set
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . p is set
|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . p)) is non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TOP-REAL n), the carrier of R^1:]
h is non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of R^1 -valued Function-like total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of (TOP-REAL n), the carrier of R^1:]
h | ((TOP-REAL n) | C) is non empty Relation-like the carrier of ((TOP-REAL n) | C) -defined the carrier of R^1 -valued Function-like total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of ((TOP-REAL n) | C), the carrier of R^1:]
[: the carrier of ((TOP-REAL n) | C), the carrier of R^1:] is non empty Relation-like V93() V94() V95() set
bool [: the carrier of ((TOP-REAL n) | C), the carrier of R^1:] is non empty set
c is non empty Relation-like the carrier of ((TOP-REAL n) | C) -defined the carrier of ((TOP-REAL n) | C) -valued Function-like total quasi_total continuous Element of bool [: the carrier of ((TOP-REAL n) | C), the carrier of ((TOP-REAL n) | C):]
(h | ((TOP-REAL n) | C)) * c is non empty Relation-like the carrier of ((TOP-REAL n) | C) -defined the carrier of ((TOP-REAL n) | C) -defined the carrier of R^1 -valued the carrier of R^1 -valued Function-like total total quasi_total quasi_total continuous V93() V94() V95() Element of bool [: the carrier of ((TOP-REAL n) | C), the carrier of R^1:]
((h | ((TOP-REAL n) | C)) * c) - (h | ((TOP-REAL n) | C)) is non empty Relation-like the carrier of ((TOP-REAL n) | C) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of ((TOP-REAL n) | C),REAL:]
[: the carrier of ((TOP-REAL n) | C),REAL:] is non empty non trivial Relation-like non finite V93() V94() V95() set
bool [: the carrier of ((TOP-REAL n) | C),REAL:] is non empty non trivial non finite set
dom (((h | ((TOP-REAL n) | C)) * c) - (h | ((TOP-REAL n) | C))) is non empty with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
dom (h | ((TOP-REAL n) | C)) is non empty with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
h | the carrier of ((TOP-REAL n) | C) is Relation-like the carrier of (TOP-REAL n) -defined the carrier of ((TOP-REAL n) | C) -defined the carrier of (TOP-REAL n) -defined the carrier of R^1 -valued Function-like V93() V94() V95() Element of bool [: the carrier of (TOP-REAL n), the carrier of R^1:]
dom ((h | ((TOP-REAL n) | C)) * c) is non empty with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
GX is non empty Relation-like the carrier of ((TOP-REAL n) | C) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of ((TOP-REAL n) | C), the carrier of R^1:]
G0 is complex-membered ext-real-membered real-membered Element of bool the carrier of R^1
GX " G0 is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
{ b₁ where b₁ is Element of the carrier of ((TOP-REAL n) | C) : (|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . p))) . (E . b₁) <= (|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . p))) . b₁ } is set
I is set
dom GX is non empty with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
GX . I is real V55() ext-real set
((h | ((TOP-REAL n) | C)) * c) . I is real V55() ext-real set
(h | ((TOP-REAL n) | C)) . I is real V55() ext-real set
(((h | ((TOP-REAL n) | C)) * c) . I) - ((h | ((TOP-REAL n) | C)) . I) is real V55() ext-real set
K167((((h | ((TOP-REAL n) | C)) * c) . I),((h | ((TOP-REAL n) | C)) . I)) is real V55() ext-real set
K165(((h | ((TOP-REAL n) | C)) . I)) is real V55() ext-real set
K163((((h | ((TOP-REAL n) | C)) * c) . I),K165(((h | ((TOP-REAL n) | C)) . I))) is real V55() ext-real set
E . I is set
(h | ((TOP-REAL n) | C)) . (E . I) is real V55() ext-real set
((h | ((TOP-REAL n) | C)) . (E . I)) - ((h | ((TOP-REAL n) | C)) . I) is real V55() ext-real set
K167(((h | ((TOP-REAL n) | C)) . (E . I)),((h | ((TOP-REAL n) | C)) . I)) is real V55() ext-real set
K163(((h | ((TOP-REAL n) | C)) . (E . I)),K165(((h | ((TOP-REAL n) | C)) . I))) is real V55() ext-real set
t is Element of the carrier of ((TOP-REAL n) | C)
E . t is set
h . (E . t) is real V55() ext-real set
h . t is real V55() ext-real set
I is set
t is Element of the carrier of ((TOP-REAL n) | C)
E . t is set
h . (E . t) is real V55() ext-real set
h . t is real V55() ext-real set
rng E is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | (conv I))
(h | ((TOP-REAL n) | C)) . (E . t) is real V55() ext-real set
(h | ((TOP-REAL n) | C)) . t is real V55() ext-real Element of the carrier of R^1
((h | ((TOP-REAL n) | C)) * c) . t is real V55() ext-real Element of the carrier of R^1
(((h | ((TOP-REAL n) | C)) * c) . t) - ((h | ((TOP-REAL n) | C)) . t) is real V55() ext-real set
K167((((h | ((TOP-REAL n) | C)) * c) . t),((h | ((TOP-REAL n) | C)) . t)) is real V55() ext-real set
K165(((h | ((TOP-REAL n) | C)) . t)) is real V55() ext-real set
K163((((h | ((TOP-REAL n) | C)) * c) . t),K165(((h | ((TOP-REAL n) | C)) . t))) is real V55() ext-real set
GX . t is real V55() ext-real Element of the carrier of R^1
dom the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I 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
len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I 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
Seg (len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I) is finite len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
Affin I is closed Affine with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
rng the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
bool (dom f) is non empty finite finite-membered set
R is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool (dom f)
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I .: R is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I .: R) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
f .: R is finite V365( the carrier of ((TOP-REAL n) | C)) Element of bool (bool the carrier of ((TOP-REAL n) | C))
union (f .: R) is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
G0 is set
E . G0 is set
G0 |-- ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I .: R) is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I .: R
(E . G0) |-- I is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of I
G0 |-- I is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of I
((E . G0) |-- I) * the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
len (((E . G0) |-- I) * the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I) 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
(G0 |-- ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I .: R)) * the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
len ((G0 |-- ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I .: R)) * the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I) 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
(len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
GX is Relation-like NAT -defined REAL -valued Function-like finite len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of (len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I) -tuples_on REAL
dom GX is finite len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
Affin ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I .: R) is closed Affine with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
Carrier (G0 |-- ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I .: R)) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
sum (G0 |-- ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I .: R)) is real V55() ext-real Element of REAL
Carrier ((E . G0) |-- I) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
Sum ((G0 |-- ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I .: R)) * the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I) is real V55() ext-real Element of REAL
rng E is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | (conv I))
sum ((E . G0) |-- I) is real V55() ext-real Element of REAL
Sum GX is real V55() ext-real Element of REAL
I is Relation-like NAT -defined REAL -valued Function-like finite len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of (len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I) -tuples_on REAL
Sum I is real V55() ext-real Element of REAL
dom I is finite len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
t is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
I . t is real V55() ext-real set
GX . t is real V55() ext-real set
t is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
I . t is real V55() ext-real set
GX . t is real V55() ext-real set
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . t is set
((E . G0) |-- I) . ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . t) is real V55() ext-real set
(G0 |-- ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I .: R)) . ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . t) is real V55() ext-real set
|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . t)) is non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TOP-REAL n), the carrier of R^1:]
(|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . t))) . G0 is real V55() ext-real set
cgx is Element of the carrier of ((TOP-REAL n) | C)
E . cgx is set
(|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . t))) . (E . cgx) is real V55() ext-real set
(|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . t))) . cgx is real V55() ext-real set
dom ((E . G0) |-- I) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
y is set
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . y is set
f . t is set
{ b₁ where b₁ is Element of the carrier of ((TOP-REAL n) | C) : (|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . t))) . (E . b₁) <= (|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . t))) . b₁ } is set
t is set
y is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
GX . y is real V55() ext-real set
I . y is real V55() ext-real set
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . y is set
|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . y)) is non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TOP-REAL n), the carrier of R^1:]
{ b₁ where b₁ is Element of the carrier of ((TOP-REAL n) | C) : (|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . y))) . (E . b₁) <= (|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . y))) . b₁ } is set
f . y is set
(G0 |-- ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I .: R)) . ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . y) is real V55() ext-real set
(|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . y))) . G0 is real V55() ext-real set
((E . G0) |-- I) . ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . y) is real V55() ext-real set
cgx is Element of the carrier of ((TOP-REAL n) | C)
E . cgx is set
(|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . y))) . (E . cgx) is real V55() ext-real set
(|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . y))) . cgx is real V55() ext-real set
t is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
GX . t is real V55() ext-real set
I . t is real V55() ext-real set
meet (rng f) is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
R is set
G is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
E . G is set
G |-- I is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of I
(E . G) |-- I is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of I
((E . G) |-- I) * the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
len (((E . G) |-- I) * the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I) 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
rng E is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | (conv I))
Carrier ((E . G) |-- I) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
sum ((E . G) |-- I) is real V55() ext-real Element of REAL
Carrier (G |-- I) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
Sum (((E . G) |-- I) * the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I) is real V55() ext-real Element of REAL
(G |-- I) * the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V93() V94() V95() FinSequence of REAL
len ((G |-- I) * the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I) 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
(len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
h is Relation-like NAT -defined REAL -valued Function-like finite len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of (len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I) -tuples_on REAL
dom h is finite len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
gx is Relation-like NAT -defined REAL -valued Function-like finite len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of (len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I) -tuples_on REAL
dom gx is finite len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
cgx is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
h . cgx is real V55() ext-real set
gx . cgx is real V55() ext-real set
f . cgx is set
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . cgx is set
|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . cgx)) is non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of R^1 -valued Function-like total quasi_total V93() V94() V95() Element of bool [: the carrier of (TOP-REAL n), the carrier of R^1:]
{ b₁ where b₁ is Element of the carrier of ((TOP-REAL n) | C) : (|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . cgx))) . (E . b₁) <= (|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . cgx))) . b₁ } is set
(|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . cgx))) . G is real V55() ext-real Element of the carrier of R^1
(G |-- I) . ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . cgx) is real V55() ext-real set
(|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . cgx))) . (E . G) is real V55() ext-real set
((E . G) |-- I) . ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . cgx) is real V55() ext-real set
GX is Element of the carrier of ((TOP-REAL n) | C)
E . GX is set
(|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . cgx))) . (E . GX) is real V55() ext-real set
(|-- (I,( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . cgx))) . GX is real V55() ext-real set
sum (G |-- I) is real V55() ext-real Element of REAL
Sum h is real V55() ext-real Element of REAL
Sum gx is real V55() ext-real Element of REAL
cgx is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
GX is set
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of I . GX is set
h . GX is real V55() ext-real set
((E . G) |-- I) . cgx is real V55() ext-real Element of REAL
gx . GX is real V55() ext-real set
(G |-- I) . cgx is real V55() ext-real Element of REAL
cgx is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
(G |-- I) . cgx is real V55() ext-real Element of REAL
((E . G) |-- I) . cgx is real V55() ext-real Element of REAL
cgx is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
Sum (G |-- I) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
Sum ((E . G) |-- I) is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element 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()
the carrier of (TOP-REAL n) is non empty set
bool the carrier of (TOP-REAL n) is non empty set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
T is finite compact affinely-independent with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
card 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 omega
conv T is closed compact convex convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
(TOP-REAL n) | (conv T) is strict TopSpace-like with_finite_small_inductive_dimension SubSpace of TOP-REAL n
the carrier of ((TOP-REAL n) | (conv T)) is set
[: the carrier of ((TOP-REAL n) | (conv T)), the carrier of ((TOP-REAL n) | (conv T)):] is Relation-like set
bool [: the carrier of ((TOP-REAL n) | (conv T)), the carrier of ((TOP-REAL n) | (conv T)):] is non empty set
I is Relation-like the carrier of ((TOP-REAL n) | (conv T)) -defined the carrier of ((TOP-REAL n) | (conv T)) -valued Function-like total quasi_total continuous Element of bool [: the carrier of ((TOP-REAL n) | (conv T)), the carrier of ((TOP-REAL n) | (conv T)):]
dom I is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | (conv T))
bool the carrier of ((TOP-REAL n) | (conv T)) is non empty set
C is Relation-like NAT -defined REAL -valued Function-like finite n -element FinSequence-like FinSubsequence-like V93() V94() V95() Element of the carrier of (TOP-REAL n)
I . C is set
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
bool the carrier of (TOP-REAL n) is non empty set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
T is finite compact affinely-independent with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
card 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 omega
conv T is closed compact convex convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
ind (conv T) is real integer finite V55() ext-real set
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T is Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T
C is non empty with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
ind C is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
n - 1 is real integer finite V55() ext-real Element of REAL
K163(n,K165(1)) is real integer finite V55() ext-real 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
the carrier of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty set
bool the carrier of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty set
(TOP-REAL n) | C is non empty strict TopSpace-like with_finite_small_inductive_dimension SubSpace of TOP-REAL n
the carrier of ((TOP-REAL n) | C) 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
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 V80() normal T_3 T_4 metrizable TopStruct
the carrier of (Euclid n) is non empty set
Family_open_set (Euclid n) is Element of bool (bool the carrier of (Euclid n))
bool the carrier of (Euclid n) is non empty set
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
the topology of ((TOP-REAL n) | C) is non empty open Element of bool (bool the carrier of ((TOP-REAL n) | C))
bool the carrier of ((TOP-REAL n) | C) is non empty set
bool (bool the carrier of ((TOP-REAL n) | C)) is non empty set
TopStruct(# the carrier of ((TOP-REAL n) | C), the topology of ((TOP-REAL n) | C) #) is non empty strict TopSpace-like TopStruct
c is Element of bool the carrier of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #)
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) | c is strict TopSpace-like V426() SubSpace of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #)
len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of 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 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
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
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
[#] ((TOP-REAL n) | C) is non empty non proper open closed with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
rng f is finite set
bool the carrier of ((TOP-REAL n) | C) is non empty Element of bool (bool the carrier of ((TOP-REAL n) | C))
R is set
G is set
f . G is set
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . G is set
{( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . G)} is non empty trivial finite 1 -element set
T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . G)} is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . G)}) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
C \ (conv (T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . G)})) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
rng the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
dom the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T 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
R is finite V365( the carrier of ((TOP-REAL n) | C)) Element of bool (bool the carrier of ((TOP-REAL n) | C))
union R is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
G is set
G0 is set
p is set
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . p is set
h is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
f . h is set
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . h is set
{( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . h)} is non empty trivial finite 1 -element set
T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . h)} is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . h)}) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
C \ (conv (T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . h)})) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
Affin (T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . h)}) is closed Affine with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
G |-- T is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of T
G |-- (T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . h)}) is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total V93() V94() V95() Linear_Combination of T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . h)}
Carrier (G |-- (T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . h)})) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
(G |-- T) . G0 is real V55() ext-real set
T \ T is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (T \ T) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
G is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
G0 is set
f . G0 is set
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . G0 is set
{( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . G0)} is non empty trivial finite 1 -element set
T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . G0)} is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . G0)}) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
p is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
p ` is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
the carrier of ((TOP-REAL n) | C) \ p is set
ind ((TOP-REAL n) | C) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
n1 is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
n1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
card R 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 R) * (n1 + 1) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative Element of REAL
G is finite V365( the carrier of ((TOP-REAL n) | C)) Element of bool (bool the carrier of ((TOP-REAL n) | C))
card G 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
order G is real integer finite V55() ext-real set
{ b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in G & ( b₁ c= f . (a₁ + 1) or b₁ in a₂ ) ) } is set
f . 1 is set
G0 is Element of bool (bool the carrier of ((TOP-REAL n) | C))
bool (bool the carrier of ((TOP-REAL n) | C)) is non empty set
bool (bool the carrier of ((TOP-REAL n) | C)) is non empty Element of bool (bool (bool the carrier of ((TOP-REAL n) | C)))
bool (bool (bool the carrier of ((TOP-REAL n) | C))) is non empty set
p is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
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 set
h is Element of bool (bool the carrier of ((TOP-REAL n) | C))
{ b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in G & ( b₁ c= f . (p + 1) or b₁ in h ) ) } is set
gx is set
cgx is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
p is Relation-like NAT -defined bool (bool the carrier of ((TOP-REAL n) | C)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool (bool the carrier of ((TOP-REAL n) | C))
len p 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
p /. 1 is Element of bool (bool the carrier of ((TOP-REAL n) | C))
union G0 is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
Seg (len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T) is finite len the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool NAT
h is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
p . h is set
h - 1 is real integer finite V55() ext-real Element of REAL
K163(h,K165(1)) is real integer finite V55() ext-real set
p . (h - 1) is set
(p . h) \ (p . (h - 1)) is Element of bool (p . h)
bool (p . h) is non empty set
union ((p . h) \ (p . (h - 1))) is set
h is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom h 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
dom p 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
rng h is finite set
h is set
gx is set
h . gx is set
cgx is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
p . cgx is set
rng p is finite V365( bool the carrier of ((TOP-REAL n) | C)) Element of bool (bool (bool the carrier of ((TOP-REAL n) | C)))
bool (bool (bool the carrier of ((TOP-REAL n) | C))) is non empty set
GX is Element of bool (bool the carrier of ((TOP-REAL n) | C))
cgx - 1 is real integer finite V55() ext-real Element of REAL
K163(cgx,K165(1)) is real integer finite V55() ext-real set
p . (cgx - 1) is set
GX \ (p . (cgx - 1)) is Element of bool (bool the carrier of ((TOP-REAL n) | C))
union (GX \ (p . (cgx - 1))) is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
h is Relation-like NAT -defined bool the carrier of ((TOP-REAL n) | C) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool the carrier of ((TOP-REAL n) | C)
rng h is finite V365( the carrier of ((TOP-REAL n) | C)) Element of bool (bool the carrier of ((TOP-REAL n) | C))
union (rng h) is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
gx is set
union G is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
cgx is set
GX is set
I is set
f . I is set
t is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
h . 1 is set
y is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
f . y is set
y - 1 is real integer finite V55() ext-real Element of REAL
K163(y,K165(1)) is real integer finite V55() ext-real set
x 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
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
i1 is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
p /. i1 is Element of bool (bool the carrier of ((TOP-REAL n) | C))
i1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
p /. (i1 + 1) is Element of bool (bool the carrier of ((TOP-REAL n) | C))
f . (i1 + 1) is set
{ b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in G & ( b₁ c= f . (i1 + 1) or b₁ in p /. i1 ) ) } is set
S2 is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
p /. {} is Element of bool (bool the carrier of ((TOP-REAL n) | C))
h . y is set
p /. y is Element of bool (bool the carrier of ((TOP-REAL n) | C))
f . (x + 1) is set
p /. x is Element of bool (bool the carrier of ((TOP-REAL n) | C))
{ b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in G & ( b₁ c= f . (x + 1) or b₁ in p /. x ) ) } is set
p . x is set
p . y is set
(p . y) \ (p . x) is Element of bool (p . y)
bool (p . y) is non empty set
union ((p . y) \ (p . x)) is set
gx is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
dom h 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
cgx is set
h . cgx is set
GX is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
I is set
h . GX is set
GX - 1 is real integer finite V55() ext-real Element of REAL
K163(GX,K165(1)) is real integer finite V55() ext-real set
I 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
I + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
p . I is set
p /. I is Element of bool (bool the carrier of ((TOP-REAL n) | C))
p /. (I + 1) is Element of bool (bool the carrier of ((TOP-REAL n) | C))
I + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
f . (I + 1) is set
{ b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in G & ( b₁ c= f . (I + 1) or b₁ in p /. I ) ) } is set
p /. GX is Element of bool (bool the carrier of ((TOP-REAL n) | C))
t is set
f . GX is set
y is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
p /. (GX - 1) is Element of bool (bool the carrier of ((TOP-REAL n) | C))
(p /. GX) \ (p /. (GX - 1)) is Element of bool (bool the carrier of ((TOP-REAL n) | C))
p . GX is set
p . (GX - 1) is set
(p . GX) \ (p . (GX - 1)) is Element of bool (p . GX)
bool (p . GX) is non empty set
union ((p . GX) \ (p . (GX - 1))) is set
gx is Element of bool (bool the carrier of ((TOP-REAL n) | C))
clf gx is Element of bool (bool the carrier of ((TOP-REAL n) | C))
{ b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in clf gx & b₁ c= h . a₁ ) } is set
union { b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in clf gx & b₁ c= h . a₁ ) } is set
GX is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
h . GX is set
{ b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in clf gx & b₁ c= h . GX ) } is set
union { b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in clf gx & b₁ c= h . GX ) } is set
t is set
y is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
t is Element of bool (bool the carrier of ((TOP-REAL n) | C))
union t is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
GX is Relation-like NAT -defined bool the carrier of ((TOP-REAL n) | C) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool the carrier of ((TOP-REAL n) | C)
dom GX 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
I is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
GX . I is set
h . I is set
{ b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in clf gx & b₁ c= h . I ) } is set
y is set
x is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
union { b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in clf gx & b₁ c= h . I ) } is set
I is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
h . I is set
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . I is set
{( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . I)} is non empty trivial finite 1 -element set
T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . I)} is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . I)}) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
p . I is set
I - 1 is real integer finite V55() ext-real Element of REAL
K163(I,K165(1)) is real integer finite V55() ext-real set
p . (I - 1) is set
(p . I) \ (p . (I - 1)) is Element of bool (p . I)
bool (p . I) is non empty set
union ((p . I) \ (p . (I - 1))) is set
t is set
y is set
C \ (conv (T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . I)})) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
y 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
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
p /. y is Element of bool (bool the carrier of ((TOP-REAL n) | C))
p /. (y + 1) is Element of bool (bool the carrier of ((TOP-REAL n) | C))
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
f . (y + 1) is set
{ b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in G & ( b₁ c= f . (y + 1) or b₁ in p /. y ) ) } is set
p . y is set
p /. I is Element of bool (bool the carrier of ((TOP-REAL n) | C))
x is set
f . I is set
i1 is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
C \ (conv (T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . I)})) is with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
rng GX is finite V365( the carrier of ((TOP-REAL n) | C)) Element of bool (bool the carrier of ((TOP-REAL n) | C))
union (rng GX) is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
I is set
union gx is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
union (clf gx) is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
t is set
y is set
x is set
h . x is set
GX . x is set
{ b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in clf gx & b₁ c= h . x ) } is set
union { b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in clf gx & b₁ c= h . x ) } is set
bool (dom GX) is non empty finite finite-membered set
I is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded Element of bool (dom GX)
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T .: I is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv ( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T .: I) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
GX .: I is finite V365( the carrier of ((TOP-REAL n) | C)) Element of bool (bool the carrier of ((TOP-REAL n) | C))
union (GX .: I) is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
GX .: (dom GX) is finite V365( the carrier of ((TOP-REAL n) | C)) Element of bool (bool the carrier of ((TOP-REAL n) | C))
(dom the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T) \ I 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
{ (conv (T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . b₁)})) where b₁ 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 : b₁ in (dom the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T) \ I } is set
(dom GX) \ I 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
meet { (conv (T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . b₁)})) where b₁ 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 : b₁ in (dom the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T) \ I } is set
GX .: ((dom the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T) \ I) is finite V365( the carrier of ((TOP-REAL n) | C)) Element of bool (bool the carrier of ((TOP-REAL n) | C))
union (GX .: ((dom the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T) \ I)) is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
y is set
x is set
i1 is set
GX . i1 is set
i2 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
the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . i2 is set
{( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . i2)} is non empty trivial finite 1 -element set
T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . i2)} is finite compact with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
conv (T \ {( the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T . i2)}) is convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
h . i2 is set
I \/ ((dom the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T) \ I) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below bounded_above real-bounded set
GX .: (I \/ ((dom the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T) \ I)) is finite V365( the carrier of ((TOP-REAL n) | C)) Element of bool (bool the carrier of ((TOP-REAL n) | C))
(GX .: I) \/ (GX .: ((dom the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T) \ I)) is finite V365( the carrier of ((TOP-REAL n) | C)) Element of bool (bool the carrier of ((TOP-REAL n) | C))
(union (GX .: I)) \/ (union (GX .: ((dom the Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Enumeration of T) \ I))) is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
I is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
t is set
GX . t is set
h . t is set
{ b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in clf gx & b₁ c= h . t ) } is set
x is set
i1 is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
x is Element of bool (bool the carrier of ((TOP-REAL n) | C))
union x is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
len GX 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
meet (rng GX) is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
I is set
t is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
p . t is set
t - 1 is real integer finite V55() ext-real Element of REAL
K163(t,K165(1)) is real integer finite V55() ext-real set
p . (t - 1) is set
GX . t is set
h . t is set
(p . t) \ (p . (t - 1)) is Element of bool (p . t)
bool (p . t) is non empty set
union ((p . t) \ (p . (t - 1))) is set
p . 1 is set
y is set
y is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
p /. y is Element of bool (bool the carrier of ((TOP-REAL n) | C))
p /. t is Element of bool (bool the carrier of ((TOP-REAL n) | C))
f . (y + 1) is set
{ b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in G & ( b₁ c= f . (y + 1) or b₁ in p /. y ) ) } is set
x is set
i1 is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
t is Relation-like NAT -defined bool the carrier of ((TOP-REAL n) | C) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of bool the carrier of ((TOP-REAL n) | C)
dom t 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
y is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
x is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
t . y is set
p . y is set
y - 1 is real integer finite V55() ext-real Element of REAL
K163(y,K165(1)) is real integer finite V55() ext-real set
p . (y - 1) is set
i1 is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
p . i1 is set
i1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
p . (i1 + 1) is set
p /. i1 is Element of bool (bool the carrier of ((TOP-REAL n) | C))
p /. (i1 + 1) is Element of bool (bool the carrier of ((TOP-REAL n) | C))
f . (i1 + 1) is set
{ b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in G & ( b₁ c= f . (i1 + 1) or b₁ in p /. i1 ) ) } is set
{ b₁ where b₁ is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C) : ( b₁ in G & ( b₁ c= f . (i1 + 1) or b₁ in p . i1 ) ) } is set
p . {} is 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
t . x is set
i1 is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
i1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
p . i1 is set
y is set
x is set
t . y is set
t . x is set
i1 is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
i2 is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
rng t is finite V365( the carrier of ((TOP-REAL n) | C)) Element of bool (bool the carrier of ((TOP-REAL n) | C))
card (rng 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 omega
len 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
y is set
x is set
t . x is set
y is set
x is set
t . x is set
card n 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 (card (rng 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 omega
meet (rng t) is with_finite_small_inductive_dimension Element of bool the carrier of ((TOP-REAL n) | C)
ind (TOP-REAL n) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
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()
ind (TOP-REAL n) is epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real non negative set
the carrier of (TOP-REAL n) is non empty set
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 non proper non proper open open closed closed convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
Affin ([#] (TOP-REAL n)) is non empty closed Affine with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
I is finite compact affinely-independent with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
Affin I is closed Affine with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
dim (TOP-REAL n) 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
card I 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
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural real integer finite cardinal V55() ext-real positive non negative Element of REAL
conv I is closed compact convex convex with_finite_small_inductive_dimension Element of bool the carrier of (TOP-REAL n)
ind (conv I) is real integer finite V55() ext-real set