:: METRIC_6 semantic presentation

REAL is non empty V45() set

COMPLEX is non empty V45() set

[:1,1:] is set
bool [:1,1:] is set
[:[:1,1:],1:] is set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is set

[:2,2:] is set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is set
RAT is non empty V45() set
INT is non empty V45() set

the carrier of X is set
V is Element of the carrier of X
y is Element of the carrier of X
dist (V,y) is V24() real ext-real Element of REAL
r is Element of the carrier of X
dist (r,y) is V24() real ext-real Element of REAL
(dist (V,y)) - (dist (r,y)) is V24() real ext-real Element of REAL
abs ((dist (V,y)) - (dist (r,y))) is V24() real ext-real Element of REAL
dist (V,r) is V24() real ext-real Element of REAL
dist (r,V) is V24() real ext-real Element of REAL
(dist (r,V)) + (dist (V,y)) is V24() real ext-real Element of REAL
(dist (r,y)) - (dist (V,y)) is V24() real ext-real Element of REAL
- (dist (V,r)) is V24() real ext-real Element of REAL
- ((dist (r,y)) - (dist (V,y))) is V24() real ext-real Element of REAL
(dist (V,r)) + (dist (r,y)) is V24() real ext-real Element of REAL
X is non empty set
[:X,X:] is set
[:[:X,X:],REAL:] is set
bool [:[:X,X:],REAL:] is set

y is Element of X
r is Element of X
V . (y,r) is V24() real ext-real Element of REAL
1 / 2 is V24() real ext-real non negative Element of REAL
V . (y,y) is V24() real ext-real Element of REAL
(1 / 2) * (V . (y,y)) is V24() real ext-real Element of REAL

1 * (V . (y,r)) is V24() real ext-real Element of REAL
(1 * (V . (y,r))) + (V . (y,r)) is V24() real ext-real Element of REAL
(1 / 2) * ((1 * (V . (y,r))) + (V . (y,r))) is V24() real ext-real Element of REAL
V . (r,y) is V24() real ext-real Element of REAL
(V . (y,r)) + (V . (r,y)) is V24() real ext-real Element of REAL
(1 / 2) * ((V . (y,r)) + (V . (r,y))) is V24() real ext-real Element of REAL
X is non empty set
[:X,X:] is set
[:[:X,X:],REAL:] is set
bool [:[:X,X:],REAL:] is set

y is Element of X
V . (y,y) is V24() real ext-real Element of REAL
y is Element of X
r is Element of X
V . (y,r) is V24() real ext-real Element of REAL
x is Element of X
s is Element of X
V . (x,s) is V24() real ext-real Element of REAL
y is Element of X
r is Element of X
V . (y,r) is V24() real ext-real Element of REAL
V . (r,y) is V24() real ext-real Element of REAL
y is Element of X
x is Element of X
V . (y,x) is V24() real ext-real Element of REAL
r is Element of X
V . (y,r) is V24() real ext-real Element of REAL
V . (r,x) is V24() real ext-real Element of REAL
(V . (y,r)) + (V . (r,x)) is V24() real ext-real Element of REAL
y is Element of X
r is Element of X
V . (y,r) is V24() real ext-real Element of REAL
x is Element of X
s is Element of X
V . (x,s) is V24() real ext-real Element of REAL
e is Element of X
e is Element of X
V . (e,e) is V24() real ext-real Element of REAL
V . (e,e) is V24() real ext-real Element of REAL
k is Element of X
n is Element of X
V . (k,n) is V24() real ext-real Element of REAL
k is Element of X
V . (k,k) is V24() real ext-real Element of REAL
V . (k,n) is V24() real ext-real Element of REAL
(V . (k,k)) + (V . (k,n)) is V24() real ext-real Element of REAL

the carrier of X is non empty set
the distance of X is Relation-like [: the carrier of X, the carrier of X:] -defined REAL -valued Function-like V29([: the carrier of X, the carrier of X:]) V30([: the carrier of X, the carrier of X:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of X, the carrier of X:],REAL:]
[: the carrier of X, the carrier of X:] is set
[:[: the carrier of X, the carrier of X:],REAL:] is set
bool [:[: the carrier of X, the carrier of X:],REAL:] is set
X is non empty set
[:X,X:] is set
[:[:X,X:],REAL:] is set
bool [:[:X,X:],REAL:] is set

y is Element of X
r is Element of X
V . (y,r) is V24() real ext-real Element of REAL
V . (r,y) is V24() real ext-real Element of REAL
V . (y,y) is V24() real ext-real Element of REAL
(V . (y,r)) + (V . (y,y)) is V24() real ext-real Element of REAL
(V . (y,r)) + 0 is V24() real ext-real Element of REAL
V . (r,r) is V24() real ext-real Element of REAL
(V . (r,y)) + (V . (r,r)) is V24() real ext-real Element of REAL
(V . (r,y)) + 0 is V24() real ext-real Element of REAL
y is Element of X
x is Element of X
V . (y,x) is V24() real ext-real Element of REAL
r is Element of X
V . (y,r) is V24() real ext-real Element of REAL
V . (r,x) is V24() real ext-real Element of REAL
(V . (y,r)) + (V . (r,x)) is V24() real ext-real Element of REAL
V . (r,y) is V24() real ext-real Element of REAL
(V . (r,y)) + (V . (r,x)) is V24() real ext-real Element of REAL
r is Element of X
x is Element of X
V . (r,x) is V24() real ext-real Element of REAL
y is Element of X
V . (r,y) is V24() real ext-real Element of REAL
V . (y,x) is V24() real ext-real Element of REAL
(V . (r,y)) + (V . (y,x)) is V24() real ext-real Element of REAL
V . (y,r) is V24() real ext-real Element of REAL
(V . (y,r)) + (V . (y,x)) is V24() real ext-real Element of REAL
r is Element of X
x is Element of X
V . (r,x) is V24() real ext-real Element of REAL
y is Element of X
V . (y,r) is V24() real ext-real Element of REAL
V . (y,x) is V24() real ext-real Element of REAL
(V . (y,r)) + (V . (y,x)) is V24() real ext-real Element of REAL
r is Element of X
x is Element of X
V . (r,x) is V24() real ext-real Element of REAL
y is Element of X
V . (y,r) is V24() real ext-real Element of REAL
V . (y,x) is V24() real ext-real Element of REAL
(V . (y,r)) + (V . (y,x)) is V24() real ext-real Element of REAL
e is Element of X
e is Element of X
V . (e,e) is V24() real ext-real Element of REAL
s is Element of X
V . (s,e) is V24() real ext-real Element of REAL
V . (s,e) is V24() real ext-real Element of REAL
(V . (s,e)) + (V . (s,e)) is V24() real ext-real Element of REAL
X is non empty set
[:X,X:] is set
[:[:X,X:],REAL:] is set
bool [:[:X,X:],REAL:] is set

r is Element of X
x is Element of X
y . (r,x) is V24() real ext-real Element of REAL
V . (r,x) is V24() real ext-real Element of REAL
1 + (V . (r,x)) is V24() real ext-real Element of REAL
(V . (r,x)) / (1 + (V . (r,x))) is V24() real ext-real Element of REAL

x is Element of X
s is Element of X
y . (x,s) is V24() real ext-real Element of REAL
r . (x,s) is V24() real ext-real Element of REAL
V . (x,s) is V24() real ext-real Element of REAL
1 + (V . (x,s)) is V24() real ext-real Element of REAL
(V . (x,s)) / (1 + (V . (x,s))) is V24() real ext-real Element of REAL
X is non empty set
[:X,X:] is set
[:[:X,X:],REAL:] is set
bool [:[:X,X:],REAL:] is set

y is Element of X
x is Element of X
(X,V) . (y,x) is V24() real ext-real Element of REAL
r is Element of X
(X,V) . (y,r) is V24() real ext-real Element of REAL
(X,V) . (r,x) is V24() real ext-real Element of REAL
((X,V) . (y,r)) + ((X,V) . (r,x)) is V24() real ext-real Element of REAL
V . (y,r) is V24() real ext-real Element of REAL
V . (y,x) is V24() real ext-real Element of REAL
V . (r,x) is V24() real ext-real Element of REAL
1 + (V . (y,r)) is V24() real ext-real Element of REAL
(V . (y,r)) / (1 + (V . (y,r))) is V24() real ext-real Element of REAL
1 + (V . (y,x)) is V24() real ext-real Element of REAL
(V . (y,x)) / (1 + (V . (y,x))) is V24() real ext-real Element of REAL
1 + (V . (r,x)) is V24() real ext-real Element of REAL
(V . (r,x)) / (1 + (V . (r,x))) is V24() real ext-real Element of REAL
(1 + (V . (y,r))) * (1 + (V . (r,x))) is V24() real ext-real Element of REAL
((V . (y,r)) / (1 + (V . (y,r)))) + ((V . (r,x)) / (1 + (V . (r,x)))) is V24() real ext-real Element of REAL
(V . (y,r)) * (1 + (V . (r,x))) is V24() real ext-real Element of REAL
(V . (r,x)) * (1 + (V . (y,r))) is V24() real ext-real Element of REAL
((V . (y,r)) * (1 + (V . (r,x)))) + ((V . (r,x)) * (1 + (V . (y,r)))) is V24() real ext-real Element of REAL
(((V . (y,r)) * (1 + (V . (r,x)))) + ((V . (r,x)) * (1 + (V . (y,r))))) / ((1 + (V . (y,r))) * (1 + (V . (r,x)))) is V24() real ext-real Element of REAL
(V . (y,r)) * 1 is V24() real ext-real Element of REAL
(V . (y,r)) * (V . (r,x)) is V24() real ext-real Element of REAL
((V . (y,r)) * 1) + ((V . (y,r)) * (V . (r,x))) is V24() real ext-real Element of REAL
(V . (r,x)) * 1 is V24() real ext-real Element of REAL
(V . (r,x)) * (V . (y,r)) is V24() real ext-real Element of REAL
((V . (r,x)) * 1) + ((V . (r,x)) * (V . (y,r))) is V24() real ext-real Element of REAL
(((V . (y,r)) * 1) + ((V . (y,r)) * (V . (r,x)))) + (((V . (r,x)) * 1) + ((V . (r,x)) * (V . (y,r)))) is V24() real ext-real Element of REAL
((((V . (y,r)) * 1) + ((V . (y,r)) * (V . (r,x)))) + (((V . (r,x)) * 1) + ((V . (r,x)) * (V . (y,r))))) / ((1 + (V . (y,r))) * (1 + (V . (r,x)))) is V24() real ext-real Element of REAL
(((V . (y,r)) / (1 + (V . (y,r)))) + ((V . (r,x)) / (1 + (V . (r,x))))) - ((V . (y,x)) / (1 + (V . (y,x)))) is V24() real ext-real Element of REAL
(V . (y,r)) + ((V . (y,r)) * (V . (r,x))) is V24() real ext-real Element of REAL
(V . (r,x)) + ((V . (r,x)) * (V . (y,r))) is V24() real ext-real Element of REAL
((V . (y,r)) + ((V . (y,r)) * (V . (r,x)))) + ((V . (r,x)) + ((V . (r,x)) * (V . (y,r)))) is V24() real ext-real Element of REAL
(((V . (y,r)) + ((V . (y,r)) * (V . (r,x)))) + ((V . (r,x)) + ((V . (r,x)) * (V . (y,r))))) * (1 + (V . (y,x))) is V24() real ext-real Element of REAL
(V . (y,x)) * ((1 + (V . (y,r))) * (1 + (V . (r,x)))) is V24() real ext-real Element of REAL
((((V . (y,r)) + ((V . (y,r)) * (V . (r,x)))) + ((V . (r,x)) + ((V . (r,x)) * (V . (y,r))))) * (1 + (V . (y,x)))) - ((V . (y,x)) * ((1 + (V . (y,r))) * (1 + (V . (r,x))))) is V24() real ext-real Element of REAL
((1 + (V . (y,r))) * (1 + (V . (r,x)))) * (1 + (V . (y,x))) is V24() real ext-real Element of REAL
(((((V . (y,r)) + ((V . (y,r)) * (V . (r,x)))) + ((V . (r,x)) + ((V . (r,x)) * (V . (y,r))))) * (1 + (V . (y,x)))) - ((V . (y,x)) * ((1 + (V . (y,r))) * (1 + (V . (r,x)))))) / (((1 + (V . (y,r))) * (1 + (V . (r,x)))) * (1 + (V . (y,x)))) is V24() real ext-real Element of REAL
(V . (y,r)) + (V . (r,x)) is V24() real ext-real Element of REAL
((V . (y,r)) + (V . (r,x))) - (V . (y,x)) is V24() real ext-real Element of REAL
(V . (r,x)) + (V . (y,r)) is V24() real ext-real Element of REAL
((V . (r,x)) + (V . (y,r))) - (V . (y,x)) is V24() real ext-real Element of REAL
((V . (r,x)) * (V . (y,r))) * (V . (y,x)) is V24() real ext-real Element of REAL
((V . (r,x)) * (V . (y,r))) + (((V . (r,x)) * (V . (y,r))) * (V . (y,x))) is V24() real ext-real Element of REAL
((V . (y,r)) * (V . (r,x))) + (((V . (r,x)) * (V . (y,r))) + (((V . (r,x)) * (V . (y,r))) * (V . (y,x)))) is V24() real ext-real Element of REAL
(((V . (r,x)) + (V . (y,r))) - (V . (y,x))) + (((V . (y,r)) * (V . (r,x))) + (((V . (r,x)) * (V . (y,r))) + (((V . (r,x)) * (V . (y,r))) * (V . (y,x))))) is V24() real ext-real Element of REAL
y is Element of X
r is Element of X
(X,V) . (y,r) is V24() real ext-real Element of REAL
V . (y,r) is V24() real ext-real Element of REAL
1 + (V . (y,r)) is V24() real ext-real Element of REAL
(V . (y,r)) / (1 + (V . (y,r))) is V24() real ext-real Element of REAL
V . (y,r) is V24() real ext-real Element of REAL
1 + (V . (y,r)) is V24() real ext-real Element of REAL
(V . (y,r)) / (1 + (V . (y,r))) is V24() real ext-real Element of REAL
y is Element of X
r is Element of X
(X,V) . (y,r) is V24() real ext-real Element of REAL
(X,V) . (r,y) is V24() real ext-real Element of REAL
V . (y,r) is V24() real ext-real Element of REAL
1 + (V . (y,r)) is V24() real ext-real Element of REAL
(V . (y,r)) / (1 + (V . (y,r))) is V24() real ext-real Element of REAL
V . (r,y) is V24() real ext-real Element of REAL
(V . (r,y)) / (1 + (V . (y,r))) is V24() real ext-real Element of REAL
1 + (V . (r,y)) is V24() real ext-real Element of REAL
(V . (r,y)) / (1 + (V . (r,y))) is V24() real ext-real Element of REAL

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is Element of the carrier of X
{V} is non empty Element of bool the carrier of X
bool the carrier of X is set

dom y is set
rng y is set
r is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
rng r is set
X is non empty MetrStruct
the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
X is non empty symmetric triangle MetrStruct
the carrier of X is non empty set
bool the carrier of X is set
V is Element of bool the carrier of X
y is Element of the carrier of X
r is V24() real ext-real Element of REAL
2 * r is V24() real ext-real Element of REAL
x is V24() real ext-real Element of REAL
s is Element of the carrier of X
Ball (s,x) is Element of bool the carrier of X
e is set
1 * r is V24() real ext-real Element of REAL
e is Element of the carrier of X
dist (s,e) is V24() real ext-real Element of REAL
the Element of the carrier of X is Element of the carrier of X
1 / 2 is V24() real ext-real non negative Element of REAL
r is V24() real ext-real non negative Element of REAL
x is Element of the carrier of X
Ball (x,r) is Element of bool the carrier of X
y is V24() real ext-real Element of REAL
r is Element of the carrier of X
Ball (r,y) is Element of bool the carrier of X
2 * y is V24() real ext-real Element of REAL
x is Element of the carrier of X
s is Element of the carrier of X
dist (x,s) is V24() real ext-real Element of REAL
dist (r,s) is V24() real ext-real Element of REAL
dist (r,x) is V24() real ext-real Element of REAL
dist (x,r) is V24() real ext-real Element of REAL
(dist (x,r)) + (dist (r,s)) is V24() real ext-real Element of REAL
y + y is V24() real ext-real Element of REAL
dist (x,s) is V24() real ext-real Element of REAL
X is non empty MetrStruct
the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set

the carrier of X is non empty set
bool the carrier of X is set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
rng V is set
y is V24() real ext-real Element of REAL
r is Element of the carrier of X
Ball (r,y) is bounded Element of bool the carrier of X
bool the carrier of X is set
x is V24() real ext-real Element of REAL
s is Element of the carrier of X
Ball (s,x) is bounded Element of bool the carrier of X

V . e is Element of the carrier of X

V . e is Element of the carrier of X
y is V24() real ext-real Element of REAL
r is Element of the carrier of X
Ball (r,y) is bounded Element of bool the carrier of X
bool the carrier of X is set
rng V is set
x is set
dom V is set
s is set
V . s is set

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is Element of the carrier of X
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
r is V24() real ext-real Element of REAL

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
y is Element of the carrier of X

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
y is Element of the carrier of X

r . x is V24() real ext-real Element of REAL
V . x is Element of the carrier of X
dist ((V . x),y) is V24() real ext-real Element of REAL

r . s is V24() real ext-real Element of REAL
V . s is Element of the carrier of X
dist ((V . s),y) is V24() real ext-real Element of REAL
x . s is V24() real ext-real Element of REAL

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

r . x is V24() real ext-real Element of REAL
V . x is Element of the carrier of X
y . x is Element of the carrier of X
dist ((V . x),(y . x)) is V24() real ext-real Element of REAL

r . s is V24() real ext-real Element of REAL
V . s is Element of the carrier of X
y . s is Element of the carrier of X
dist ((V . s),(y . s)) is V24() real ext-real Element of REAL
x . s is V24() real ext-real Element of REAL

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is Element of the carrier of X
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
lim y is Element of the carrier of X
r is V24() real ext-real Element of REAL

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is Element of the carrier of X
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
lim y is Element of the carrier of X
r is V24() real ext-real Element of REAL

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
lim V is Element of the carrier of X
y is Element of the carrier of X

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is Element of the carrier of X
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

lim (X,y,V) is V24() real ext-real Element of REAL
r is V24() real ext-real set
x is V24() real ext-real Element of REAL

(X,y,V) . e is V24() real ext-real Element of REAL
((X,y,V) . e) - 0 is V24() real ext-real Element of REAL
abs (((X,y,V) . e) - 0) is V24() real ext-real Element of REAL
y . e is Element of the carrier of X
dist ((y . e),V) is V24() real ext-real Element of REAL
r is V24() real ext-real Element of REAL

y . e is Element of the carrier of X
dist ((y . e),V) is V24() real ext-real Element of REAL
(X,y,V) . e is V24() real ext-real Element of REAL
((X,y,V) . e) - 0 is V24() real ext-real Element of REAL
abs (((X,y,V) . e) - 0) is V24() real ext-real Element of REAL
abs (dist ((y . e),V)) is V24() real ext-real Element of REAL

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is Element of the carrier of X
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
r is V24() real ext-real Element of REAL
Ball (V,r) is bounded Element of bool the carrier of X
bool the carrier of X is set

y . e is Element of the carrier of X
dist (V,(y . e)) is V24() real ext-real Element of REAL

y . e is Element of the carrier of X

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
bool the carrier of X is set
Family_open_set X is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is set
V is Element of the carrier of X
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
r is V24() real ext-real Element of REAL
Ball (V,r) is bounded Element of bool the carrier of X
r is Element of bool the carrier of X
x is V24() real ext-real Element of REAL
Ball (V,x) is bounded Element of bool the carrier of X

y . e is Element of the carrier of X

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
bool the carrier of X is set
Family_open_set X is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is set
V is Element of the carrier of X
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
r is V24() real ext-real Element of REAL
Ball (V,r) is bounded Element of bool the carrier of X
dist (V,V) is V24() real ext-real Element of REAL
r is V24() real ext-real Element of REAL
Ball (V,r) is bounded Element of bool the carrier of X

y . e is Element of the carrier of X
dist ((y . e),V) is V24() real ext-real Element of REAL

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is Element of the carrier of X
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
r is V24() real ext-real Element of REAL
Ball (V,r) is bounded Element of bool the carrier of X
bool the carrier of X is set
bool the carrier of X is set
Family_open_set X is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is set
r is Element of bool the carrier of X

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
bool the carrier of X is set
Family_open_set X is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is set
V is Element of the carrier of X
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
r is V24() real ext-real Element of REAL
Ball (V,r) is bounded Element of bool the carrier of X
r is Element of bool the carrier of X

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
bool the carrier of X is set

the carrier of x is non empty set
[:NAT, the carrier of x:] is set
bool [:NAT, the carrier of x:] is set
V is Element of the carrier of X
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
r is Element of bool the carrier of X
Family_open_set X is Element of bool (bool the carrier of X)
bool (bool the carrier of X) is set
bool the carrier of x is set
s is Element of the carrier of x
Family_open_set x is Element of bool (bool the carrier of x)
bool (bool the carrier of x) is set
e is non empty Relation-like NAT -defined the carrier of x -valued Function-like V29( NAT ) V30( NAT , the carrier of x) Element of bool [:NAT, the carrier of x:]
e is V24() real ext-real Element of REAL
Ball (s,e) is bounded Element of bool the carrier of x

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
lim V is Element of the carrier of X
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
lim y is Element of the carrier of X
dist ((lim V),(lim y)) is V24() real ext-real Element of REAL

lim (X,V,y) is V24() real ext-real Element of REAL
r is Element of the carrier of X
x is Element of the carrier of X
dist (r,x) is V24() real ext-real Element of REAL
s is V24() real ext-real set
e is V24() real ext-real Element of REAL
e / 2 is V24() real ext-real Element of REAL

(X,V,y) . n is V24() real ext-real Element of REAL
((X,V,y) . n) - (dist (r,x)) is V24() real ext-real Element of REAL
abs (((X,V,y) . n) - (dist (r,x))) is V24() real ext-real Element of REAL
V . n is Element of the carrier of X
y . n is Element of the carrier of X
dist ((V . n),(y . n)) is V24() real ext-real Element of REAL
dist (r,(y . n)) is V24() real ext-real Element of REAL
(dist ((V . n),(y . n))) - (dist (r,(y . n))) is V24() real ext-real Element of REAL
abs ((dist ((V . n),(y . n))) - (dist (r,(y . n)))) is V24() real ext-real Element of REAL
dist ((V . n),r) is V24() real ext-real Element of REAL
dist ((y . n),r) is V24() real ext-real Element of REAL
dist (x,r) is V24() real ext-real Element of REAL
(dist ((y . n),r)) - (dist (x,r)) is V24() real ext-real Element of REAL
abs ((dist ((y . n),r)) - (dist (x,r))) is V24() real ext-real Element of REAL
dist ((y . n),x) is V24() real ext-real Element of REAL
(dist ((V . n),(y . n))) - (dist ((y . n),r)) is V24() real ext-real Element of REAL
abs ((dist ((V . n),(y . n))) - (dist ((y . n),r))) is V24() real ext-real Element of REAL
(dist ((y . n),r)) - (dist (r,x)) is V24() real ext-real Element of REAL
abs ((dist ((y . n),r)) - (dist (r,x))) is V24() real ext-real Element of REAL
(abs ((dist ((V . n),(y . n))) - (dist ((y . n),r)))) + (abs ((dist ((y . n),r)) - (dist (r,x)))) is V24() real ext-real Element of REAL
(dist ((V . n),r)) + (dist ((y . n),x)) is V24() real ext-real Element of REAL
((X,V,y) . n) - (dist ((lim V),(lim y))) is V24() real ext-real Element of REAL
abs (((X,V,y) . n) - (dist ((lim V),(lim y)))) is V24() real ext-real Element of REAL
(dist ((V . n),(y . n))) - (dist (r,x)) is V24() real ext-real Element of REAL
abs ((dist ((V . n),(y . n))) - (dist (r,x))) is V24() real ext-real Element of REAL
((dist ((V . n),(y . n))) - (dist ((y . n),r))) + ((dist ((y . n),r)) - (dist (r,x))) is V24() real ext-real Element of REAL
abs (((dist ((V . n),(y . n))) - (dist ((y . n),r))) + ((dist ((y . n),r)) - (dist (r,x)))) is V24() real ext-real Element of REAL
(e / 2) + (e / 2) is V24() real ext-real Element of REAL

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is Element of the carrier of X
y is Element of the carrier of X
r is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
lim r is Element of the carrier of X

(X,r,r) . x is V24() real ext-real Element of REAL
r . x is Element of the carrier of X
dist ((r . x),(r . x)) is V24() real ext-real Element of REAL
(X,r,r) . 0 is V24() real ext-real Element of REAL
dist (V,y) is V24() real ext-real Element of REAL
lim (X,r,r) is V24() real ext-real Element of REAL

(X,r,r) . x is V24() real ext-real Element of REAL

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
y is Element of the carrier of X
r is V24() real ext-real Element of REAL

V . s is Element of the carrier of X
dist ((V . s),y) is V24() real ext-real Element of REAL
dist (y,y) is V24() real ext-real Element of REAL

V . s is Element of the carrier of X
dist ((V . s),y) is V24() real ext-real Element of REAL

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is Element of the carrier of X
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
r is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

y * x is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) subsequence of y
s is V24() real ext-real Element of REAL

r . k is Element of the carrier of X
dist ((r . k),V) is V24() real ext-real Element of REAL
dom y is set
dom x is set

dom (y * x) is set
y . (x . k) is Element of the carrier of X

r . k is Element of the carrier of X
dist ((r . k),V) is V24() real ext-real Element of REAL

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

V * r is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) subsequence of V
x is V24() real ext-real Element of REAL

y . e is Element of the carrier of X

y . k is Element of the carrier of X
dist ((y . e),(y . k)) is V24() real ext-real Element of REAL

dom V is set
dom r is set
dom (V * r) is set
V . (r . k) is Element of the carrier of X

V . (r . e) is Element of the carrier of X

y . e is Element of the carrier of X
y . k is Element of the carrier of X
dist ((y . e),(y . k)) is V24() real ext-real Element of REAL

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
lim V is Element of the carrier of X
y is Element of the carrier of X

r is V24() real ext-real set
x is V24() real ext-real Element of REAL
Ball (y,x) is bounded Element of bool the carrier of X
bool the carrier of X is set

V . s is Element of the carrier of X
(X,V,y) . s is V24() real ext-real Element of REAL
dist ((V . s),y) is V24() real ext-real Element of REAL
abs ((X,V,y) . s) is V24() real ext-real Element of REAL

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

V . s is Element of the carrier of X
V . e is Element of the carrier of X
dist ((V . s),(V . e)) is V24() real ext-real Element of REAL

y is V24() real ext-real Element of REAL

V . r is Element of the carrier of X

x is V24() real ext-real set

V . s is Element of the carrier of X
dist ((V . s),(V . r)) is V24() real ext-real Element of REAL
(X,V,(V . r)) . s is V24() real ext-real Element of REAL
abs ((X,V,(V . r)) . s) is V24() real ext-real Element of REAL
x + y is V24() real ext-real Element of REAL
s is V24() real ext-real Element of REAL
e is Element of the carrier of X
Ball (e,s) is bounded Element of bool the carrier of X
bool the carrier of X is set

V . e is Element of the carrier of X
dist ((V . e),(V . r)) is V24() real ext-real Element of REAL
dist ((V . e),e) is V24() real ext-real Element of REAL
dist ((V . e),(V . r)) is V24() real ext-real Element of REAL
dist ((V . e),e) is V24() real ext-real Element of REAL

V . e is Element of the carrier of X
s is V24() real ext-real Element of REAL
e is Element of the carrier of X
Ball (e,s) is bounded Element of bool the carrier of X
bool the carrier of X is set

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
V is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]

the carrier of X is non empty set
[:NAT, the carrier of X:] is set
bool [:NAT, the carrier of X:] is set
the Element of the carrier of X is Element of the carrier of X
{ the Element of the carrier of X} is non empty Element of bool the carrier of X
bool the carrier of X is set
y is non empty Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) Element of bool [:NAT, the carrier of X:]
rng y is set

the carrier of X is non empty set
bool the carrier of X is set
V is bounded Element of bool the carrier of X
y is Element of the carrier of X
r is V24() real ext-real Element of REAL
x is Element of the carrier of X
Ball (x,r) is bounded Element of bool the carrier of X
dist (x,y) is V24() real ext-real Element of REAL
r + (dist (x,y)) is V24() real ext-real Element of REAL
s is V24() real ext-real Element of REAL
Ball (y,s) is bounded Element of bool the carrier of X
r + 0 is V24() real ext-real Element of REAL
e is set
e is Element of the carrier of X
dist (e,x) is V24() real ext-real Element of REAL
(dist (e,x)) + (dist (x,y)) is V24() real ext-real Element of REAL
dist (e,y) is V24() real ext-real Element of REAL