REAL is non empty non trivial non finite V141() V142() V143() V147() set
NAT is non empty non trivial ordinal non finite cardinal limit_cardinal V141() V142() V143() V144() V145() V146() V147() Element of bool REAL
bool REAL is non empty non trivial non finite set
K246() is V141() V142() V143() Element of bool REAL
omega is non empty non trivial ordinal non finite cardinal limit_cardinal V141() V142() V143() V144() V145() V146() V147() set
bool omega is non empty non trivial non finite set
1 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
[:1,1:] is non empty finite set
bool [:1,1:] is non empty finite V34() set
[:[:1,1:],1:] is non empty finite set
bool [:[:1,1:],1:] is non empty finite V34() set
[:[:1,1:],REAL:] is non empty non trivial non finite set
bool [:[:1,1:],REAL:] is non empty non trivial non finite set
[:REAL,REAL:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
2 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
[:2,2:] is non empty finite set
[:[:2,2:],REAL:] is non empty non trivial non finite set
bool [:[:2,2:],REAL:] is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite V141() V147() set
bool NAT is non empty non trivial non finite set
K314() is V137() TopStruct
the carrier of K314() is V141() V142() V143() set
RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V137() MetrStruct
real_dist is non empty Relation-like [:REAL,REAL:] -defined REAL -valued Function-like total V27([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]
MetrStruct(# REAL,real_dist #) is strict MetrStruct
K319() is non empty strict TopSpace-like V137() TopStruct
K247() is V141() V142() V143() Element of bool REAL
ExtREAL is non empty V142() set
bool ExtREAL is non empty set
the carrier of K319() is non empty V141() V142() V143() set
[:NAT,REAL:] is non empty non trivial non finite set
bool [:NAT,REAL:] is non empty non trivial non finite set
RAT is non empty non trivial non finite V141() V142() V143() V144() V147() set
INT is non empty non trivial non finite V141() V142() V143() V144() V145() V147() set
0 is empty trivial ordinal natural V11() real finite V34() cardinal 0 -element ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() set
{0,1} is non empty finite V34() V141() V142() V143() V144() V145() V146() set
bool (bool REAL) is non empty non trivial non finite set
[:COMPLEX,COMPLEX:] is non empty non trivial non finite set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
bool [:REAL,REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is non empty non trivial non finite set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is non empty non trivial non finite set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is non empty non trivial non finite set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is non empty non trivial non finite set
[:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
0 is empty trivial ordinal natural V11() real finite V34() cardinal 0 -element ext-real non positive non negative V139() V140() V141() V142() V143() V144() V145() V146() V147() Element of NAT
4 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
card 0 is empty trivial ordinal natural V11() real finite V34() cardinal 0 -element ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() set
card omega is non empty non trivial ordinal non finite cardinal set
D is non empty MetrStruct
the carrier of D is non empty set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
D is non empty Reflexive MetrStruct
the carrier of D is non empty set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
a is set
b is Element of the carrier of D
{b} is non empty trivial finite 1 -element Element of bool the carrier of D
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
X is Element of bool the carrier of D
NAT --> X is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
W is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
TW is Element of the carrier of D
f is Element of the carrier of D
dist (TW,f) is V11() real ext-real Element of REAL
the distance of D is non empty Relation-like [: the carrier of D, the carrier of D:] -defined REAL -valued Function-like total V27([: the carrier of D, the carrier of D:], REAL ) Element of bool [:[: the carrier of D, the carrier of D:],REAL:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set
the distance of D . (TW,f) is V11() real ext-real Element of REAL
TW is ordinal natural V11() real finite cardinal ext-real non negative set
f is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
W . f is Element of bool the carrier of D
W . TW is Element of bool the carrier of D
dom W is V141() V142() V143() V144() V145() V146() Element of bool NAT
TW is set
W . TW is set
D is non empty Reflexive MetrStruct
the carrier of D is non empty set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
b is set
X is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
a . X is Element of bool the carrier of D
diameter (a . X) is V11() real ext-real Element of REAL
W is ordinal natural V11() real finite cardinal ext-real non negative set
a . W is Element of bool the carrier of D
diameter (a . W) is V11() real ext-real Element of REAL
b is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
X is ordinal natural V11() real finite cardinal ext-real non negative set
b . X is V11() real ext-real Element of REAL
a . X is Element of bool the carrier of D
diameter (a . X) is V11() real ext-real Element of REAL
b is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
X is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
W is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . W is V11() real ext-real Element of REAL
a . W is Element of bool the carrier of D
diameter (a . W) is V11() real ext-real Element of REAL
X . W is V11() real ext-real Element of REAL
D is non empty Reflexive MetrStruct
the carrier of D is non empty set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) Element of bool [:NAT,(bool the carrier of D):]
(D,a) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
X is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
a . X is Element of bool the carrier of D
diameter (a . X) is V11() real ext-real Element of REAL
(D,a) . X is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive Element of REAL
D is non empty Reflexive MetrStruct
the carrier of D is non empty set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) Element of bool [:NAT,(bool the carrier of D):]
(D,a) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
(D,a) . 0 is V11() real ext-real Element of REAL
((D,a) . 0) + 1 is V11() real ext-real Element of REAL
((D,a) . 0) + 0 is V11() real ext-real Element of REAL
X is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
a . X is Element of bool the carrier of D
diameter (a . X) is V11() real ext-real Element of REAL
(D,a) . X is V11() real ext-real Element of REAL
a . 0 is Element of bool the carrier of D
diameter (a . 0) is V11() real ext-real Element of REAL
X is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
dom (D,a) is V141() V142() V143() V144() V145() V146() Element of bool NAT
W is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
a . X is Element of bool the carrier of D
diameter (a . X) is V11() real ext-real Element of REAL
(D,a) . X is V11() real ext-real Element of REAL
a . W is Element of bool the carrier of D
diameter (a . W) is V11() real ext-real Element of REAL
(D,a) . W is V11() real ext-real Element of REAL
D is non empty Reflexive MetrStruct
the carrier of D is non empty set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) Element of bool [:NAT,(bool the carrier of D):]
(D,a) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
X is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
dom (D,a) is V141() V142() V143() V144() V145() V146() Element of bool NAT
W is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
a . W is Element of bool the carrier of D
a . X is Element of bool the carrier of D
diameter (a . X) is V11() real ext-real Element of REAL
(D,a) . X is V11() real ext-real Element of REAL
diameter (a . W) is V11() real ext-real Element of REAL
(D,a) . W is V11() real ext-real Element of REAL
D is non empty Reflexive MetrStruct
the carrier of D is non empty set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
[:NAT, the carrier of D:] is non empty non trivial non finite set
bool [:NAT, the carrier of D:] is non empty non trivial non finite set
a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) Element of bool [:NAT,(bool the carrier of D):]
(D,a) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
lim (D,a) is V11() real ext-real Element of REAL
X is non empty Relation-like NAT -defined the carrier of D -valued Function-like total V27( NAT , the carrier of D) Element of bool [:NAT, the carrier of D:]
W is V11() real ext-real Element of REAL
TW is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
f is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
s is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
X . f is Element of the carrier of D
X . s is Element of the carrier of D
dist ((X . f),(X . s)) is V11() real ext-real Element of REAL
the distance of D is non empty Relation-like [: the carrier of D, the carrier of D:] -defined REAL -valued Function-like total V27([: the carrier of D, the carrier of D:], REAL ) Element of bool [:[: the carrier of D, the carrier of D:],REAL:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set
the distance of D . ((X . f),(X . s)) is V11() real ext-real Element of REAL
a . s is Element of bool the carrier of D
a . TW is Element of bool the carrier of D
X . s is Element of the carrier of D
X . f is Element of the carrier of D
a . f is Element of bool the carrier of D
(D,a) . TW is V11() real ext-real Element of REAL
((D,a) . TW) - 0 is V11() real ext-real Element of REAL
abs (((D,a) . TW) - 0) is V11() real ext-real Element of REAL
diameter (a . TW) is V11() real ext-real Element of REAL
dist ((X . f),(X . s)) is V11() real ext-real Element of REAL
the distance of D . ((X . f),(X . s)) is V11() real ext-real Element of REAL
D is V11() real ext-real Element of REAL
2 * D is V11() real ext-real Element of REAL
a is non empty Reflexive symmetric triangle MetrStruct
the carrier of a is non empty set
b is Element of the carrier of a
cl_Ball (b,D) is Element of bool the carrier of a
bool the carrier of a is non empty set
diameter (cl_Ball (b,D)) is V11() real ext-real Element of REAL
dist (b,b) is V11() real ext-real Element of REAL
the distance of a is non empty Relation-like [: the carrier of a, the carrier of a:] -defined REAL -valued Function-like total V27([: the carrier of a, the carrier of a:], REAL ) Element of bool [:[: the carrier of a, the carrier of a:],REAL:]
[: the carrier of a, the carrier of a:] is non empty set
[:[: the carrier of a, the carrier of a:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of a, the carrier of a:],REAL:] is non empty non trivial non finite set
the distance of a . (b,b) is V11() real ext-real Element of REAL
X is Element of the carrier of a
W is Element of the carrier of a
dist (X,b) is V11() real ext-real Element of REAL
the distance of a . (X,b) is V11() real ext-real Element of REAL
dist (X,W) is V11() real ext-real Element of REAL
the distance of a . (X,W) is V11() real ext-real Element of REAL
dist (b,W) is V11() real ext-real Element of REAL
the distance of a . (b,W) is V11() real ext-real Element of REAL
(dist (X,b)) + (dist (b,W)) is V11() real ext-real Element of REAL
D + D is V11() real ext-real Element of REAL
D is MetrStruct
the carrier of D is set
bool the carrier of D is non empty set
D is MetrStruct
the carrier of D is set
bool the carrier of D is non empty set
D is MetrStruct
the carrier of D is set
bool the carrier of D is non empty set
a is Element of bool the carrier of D
TopSpaceMetr D is strict TopSpace-like TopStruct
Family_open_set D is Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
TopStruct(# the carrier of D,(Family_open_set D) #) is strict TopStruct
a is Element of bool the carrier of D
[#] D is non proper Element of bool the carrier of D
a ` is Element of bool the carrier of D
the carrier of D \ a is set
Family_open_set D is Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
D is non empty MetrStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
[#] D is non empty non proper Element of bool the carrier of D
Family_open_set D is Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
{} D is empty trivial proper ordinal natural V11() real finite V34() cardinal 0 -element bounded ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() (D) (D) Element of bool the carrier of D
({} D) ` is Element of bool the carrier of D
the carrier of D \ ({} D) is set
(({} D) `) ` is Element of bool the carrier of D
the carrier of D \ (({} D) `) is set
D is MetrStruct
the carrier of D is set
bool the carrier of D is non empty set
TopSpaceMetr D is strict TopSpace-like TopStruct
Family_open_set D is Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
TopStruct(# the carrier of D,(Family_open_set D) #) is strict TopStruct
the carrier of (TopSpaceMetr D) is set
bool the carrier of (TopSpaceMetr D) is non empty set
a is Element of bool the carrier of D
b is Element of bool the carrier of (TopSpaceMetr D)
a ` is Element of bool the carrier of D
the carrier of D \ a is set
b ` is Element of bool the carrier of (TopSpaceMetr D)
the carrier of (TopSpaceMetr D) \ b is set
a ` is Element of bool the carrier of D
the carrier of D \ a is set
D is TopStruct
the carrier of D is set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
D is TopSpace-like TopStruct
the carrier of D is set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
[#] D is non proper open closed Element of bool the carrier of D
NAT --> ([#] D) is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
a is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
b is ordinal natural V11() real finite cardinal ext-real non negative set
a . b is Element of bool the carrier of D
b is ordinal natural V11() real finite cardinal ext-real non negative set
a . b is Element of bool the carrier of D
dom a is V141() V142() V143() V144() V145() V146() Element of bool NAT
b is set
a . b is set
D is TopSpace-like TopStruct
the carrier of D is set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
D is MetrStruct
the carrier of D is set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
D is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of D is non empty set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
a is set
b is Element of the carrier of D
Ball (b,1) is bounded Element of bool the carrier of D
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
NAT --> (Ball (b,1)) is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
W is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
TW is set
dom W is V141() V142() V143() V144() V145() V146() Element of bool NAT
f is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
W . f is Element of bool the carrier of D
dist (b,b) is V11() real ext-real Element of REAL
the distance of D is non empty Relation-like [: the carrier of D, the carrier of D:] -defined REAL -valued Function-like total V27([: the carrier of D, the carrier of D:], REAL ) Element of bool [:[: the carrier of D, the carrier of D:],REAL:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set
the distance of D . (b,b) is V11() real ext-real Element of REAL
W . TW is set
TW is ordinal natural V11() real finite cardinal ext-real non negative set
W . TW is Element of bool the carrier of D
Family_open_set D is Element of bool (bool the carrier of D)
TW is ordinal natural V11() real finite cardinal ext-real non negative set
W . TW is Element of bool the carrier of D
a is set
b is Element of the carrier of D
cl_Ball (b,1) is Element of bool the carrier of D
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
NAT --> (cl_Ball (b,1)) is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
W is non empty T-Sequence-like Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
TW is set
dom W is V141() V142() V143() V144() V145() V146() Element of bool NAT
f is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
W . f is Element of bool the carrier of D
dist (b,b) is V11() real ext-real Element of REAL
the distance of D is non empty Relation-like [: the carrier of D, the carrier of D:] -defined REAL -valued Function-like total V27([: the carrier of D, the carrier of D:], REAL ) Element of bool [:[: the carrier of D, the carrier of D:],REAL:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set
the distance of D . (b,b) is V11() real ext-real Element of REAL
W . TW is set
TW is ordinal natural V11() real finite cardinal ext-real non negative set
W . TW is Element of bool the carrier of D
[#] D is non empty non proper Element of bool the carrier of D
([#] D) \ (cl_Ball (b,1)) is Element of bool the carrier of D
Family_open_set D is Element of bool (bool the carrier of D)
(cl_Ball (b,1)) ` is Element of bool the carrier of D
the carrier of D \ (cl_Ball (b,1)) is set
TW is ordinal natural V11() real finite cardinal ext-real non negative set
W . TW is Element of bool the carrier of D
D is MetrStruct
the carrier of D is set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
TopSpaceMetr D is strict TopSpace-like TopStruct
Family_open_set D is Element of bool (bool the carrier of D)
TopStruct(# the carrier of D,(Family_open_set D) #) is strict TopStruct
the carrier of (TopSpaceMetr D) is set
bool the carrier of (TopSpaceMetr D) is non empty Element of bool (bool the carrier of (TopSpaceMetr D))
bool the carrier of (TopSpaceMetr D) is non empty set
bool (bool the carrier of (TopSpaceMetr D)) is non empty set
[:NAT,(bool the carrier of (TopSpaceMetr D)):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of (TopSpaceMetr D)):] is non empty non trivial non finite set
a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
b is non empty Relation-like NAT -defined bool the carrier of (TopSpaceMetr D) -valued Function-like total V27( NAT , bool the carrier of (TopSpaceMetr D)) Element of bool [:NAT,(bool the carrier of (TopSpaceMetr D)):]
X is ordinal natural V11() real finite cardinal ext-real non negative set
b . X is Element of bool the carrier of (TopSpaceMetr D)
a . X is Element of bool the carrier of D
X is ordinal natural V11() real finite cardinal ext-real non negative set
a . X is Element of bool the carrier of D
b . X is Element of bool the carrier of (TopSpaceMetr D)
X is ordinal natural V11() real finite cardinal ext-real non negative set
b . X is Element of bool the carrier of (TopSpaceMetr D)
a . X is Element of bool the carrier of D
X is ordinal natural V11() real finite cardinal ext-real non negative set
a . X is Element of bool the carrier of D
b . X is Element of bool the carrier of (TopSpaceMetr D)
D is non empty Reflexive symmetric triangle MetrStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
TopSpaceMetr D is non empty strict TopSpace-like TopStruct
Family_open_set D is Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
TopStruct(# the carrier of D,(Family_open_set D) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr D) is non empty set
bool the carrier of (TopSpaceMetr D) is non empty set
a is Element of bool the carrier of D
b is Element of bool the carrier of D
diameter a is V11() real ext-real Element of REAL
diameter b is V11() real ext-real Element of REAL
TW is Element of bool the carrier of (TopSpaceMetr D)
Cl TW is closed Element of bool the carrier of (TopSpaceMetr D)
f is Element of the carrier of D
s is Element of the carrier of D
dist (f,s) is V11() real ext-real Element of REAL
the distance of D is non empty Relation-like [: the carrier of D, the carrier of D:] -defined REAL -valued Function-like total V27([: the carrier of D, the carrier of D:], REAL ) Element of bool [:[: the carrier of D, the carrier of D:],REAL:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set
the distance of D . (f,s) is V11() real ext-real Element of REAL
(dist (f,s)) - (diameter a) is V11() real ext-real Element of REAL
((dist (f,s)) - (diameter a)) / 2 is V11() real ext-real Element of REAL
Ball (f,(((dist (f,s)) - (diameter a)) / 2)) is bounded Element of bool the carrier of D
Ball (s,(((dist (f,s)) - (diameter a)) / 2)) is bounded Element of bool the carrier of D
(diameter a) - (diameter a) is V11() real ext-real Element of REAL
0 / 2 is empty trivial ordinal natural V11() real finite V34() cardinal 0 -element ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() Element of REAL
SI is Element of bool the carrier of (TopSpaceMetr D)
c16 is Element of bool the carrier of (TopSpaceMetr D)
dist (s,s) is V11() real ext-real Element of REAL
the distance of D . (s,s) is V11() real ext-real Element of REAL
rngs is Element of the carrier of (TopSpaceMetr D)
x is set
dist (f,f) is V11() real ext-real Element of REAL
the distance of D . (f,f) is V11() real ext-real Element of REAL
S is Element of the carrier of (TopSpaceMetr D)
y is set
xS is Element of the carrier of D
dist (f,xS) is V11() real ext-real Element of REAL
the distance of D . (f,xS) is V11() real ext-real Element of REAL
j1 is Element of the carrier of D
dist (xS,j1) is V11() real ext-real Element of REAL
the distance of D . (xS,j1) is V11() real ext-real Element of REAL
(((dist (f,s)) - (diameter a)) / 2) + (diameter a) is V11() real ext-real Element of REAL
(dist (f,xS)) + (dist (xS,j1)) is V11() real ext-real Element of REAL
dist (s,j1) is V11() real ext-real Element of REAL
the distance of D . (s,j1) is V11() real ext-real Element of REAL
dist (f,j1) is V11() real ext-real Element of REAL
the distance of D . (f,j1) is V11() real ext-real Element of REAL
((((dist (f,s)) - (diameter a)) / 2) + (diameter a)) + (((dist (f,s)) - (diameter a)) / 2) is V11() real ext-real Element of REAL
dist (j1,s) is V11() real ext-real Element of REAL
the distance of D . (j1,s) is V11() real ext-real Element of REAL
(dist (f,j1)) + (dist (j1,s)) is V11() real ext-real Element of REAL
(diameter a) + 1 is V11() real ext-real Element of REAL
(diameter a) + 0 is V11() real ext-real Element of REAL
f is Element of the carrier of D
s is Element of the carrier of D
dist (f,s) is V11() real ext-real Element of REAL
the distance of D . (f,s) is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
s is Element of the carrier of D
S is Element of the carrier of D
dist (s,S) is V11() real ext-real Element of REAL
the distance of D . (s,S) is V11() real ext-real Element of REAL
0 + 0 is empty trivial ordinal natural V11() real finite V34() cardinal 0 -element ext-real non positive non negative V139() V140() V141() V142() V143() V144() V145() V146() V147() Element of NAT
D is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of D is non empty set
[:NAT, the carrier of D:] is non empty non trivial non finite set
bool [:NAT, the carrier of D:] is non empty non trivial non finite set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
TopSpaceMetr D is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
Family_open_set D is Element of bool (bool the carrier of D)
TopStruct(# the carrier of D,(Family_open_set D) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr D) is non empty set
bool the carrier of (TopSpaceMetr D) is non empty set
b is non empty Relation-like NAT -defined the carrier of D -valued Function-like total V27( NAT , the carrier of D) Element of bool [:NAT, the carrier of D:]
X is set
W is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : W <= b1 } is set
f is set
s is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . s is Element of the carrier of D
f is Element of bool the carrier of (TopSpaceMetr D)
Cl f is closed Element of bool the carrier of (TopSpaceMetr D)
s is ordinal natural V11() real finite cardinal ext-real non negative set
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : s <= b1 } is set
X is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
W is set
dom X is V141() V142() V143() V144() V145() V146() Element of bool NAT
TW is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW <= b1 } is set
X . TW is Element of bool the carrier of D
f is Element of bool the carrier of (TopSpaceMetr D)
Cl f is closed Element of bool the carrier of (TopSpaceMetr D)
b . TW is Element of the carrier of D
X . W is set
W is ordinal natural V11() real finite cardinal ext-real non negative set
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : W <= b1 } is set
X . W is Element of bool the carrier of D
TW is Element of bool the carrier of (TopSpaceMetr D)
Cl TW is closed Element of bool the carrier of (TopSpaceMetr D)
W is non empty Relation-like non-empty NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) Element of bool [:NAT,(bool the carrier of D):]
(D,W) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
lim (D,W) is V11() real ext-real Element of REAL
TW is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW <= b1 } is set
W . TW is Element of bool the carrier of D
f is Element of bool the carrier of (TopSpaceMetr D)
Cl f is closed Element of bool the carrier of (TopSpaceMetr D)
TW + 1 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW + 1 <= b1 } is set
W . (TW + 1) is Element of bool the carrier of D
s is Element of bool the carrier of (TopSpaceMetr D)
Cl s is closed Element of bool the carrier of (TopSpaceMetr D)
S is set
rngs is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . rngs is Element of the carrier of D
TW is ordinal natural V11() real finite cardinal ext-real non negative set
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW <= b1 } is set
W . TW is Element of bool the carrier of D
f is Element of bool the carrier of (TopSpaceMetr D)
Cl f is closed Element of bool the carrier of (TopSpaceMetr D)
rng b is Element of bool the carrier of D
S is set
dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT
rngs is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . rngs is Element of the carrier of D
s is Element of bool the carrier of D
TW is non empty Relation-like non-empty NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) (D) Element of bool [:NAT,(bool the carrier of D):]
(D,TW) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
s is V11() real ext-real set
S is V11() real ext-real Element of REAL
S / 2 is V11() real ext-real Element of REAL
F is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
F is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(D,TW) . F is V11() real ext-real Element of REAL
((D,TW) . F) - 0 is V11() real ext-real Element of REAL
abs (((D,TW) . F) - 0) is V11() real ext-real Element of REAL
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : F <= b1 } is set
W . F is Element of bool the carrier of D
R is Element of bool the carrier of (TopSpaceMetr D)
Cl R is closed Element of bool the carrier of (TopSpaceMetr D)
R9 is Element of the carrier of D
R9 is Element of bool the carrier of D
c16 is Element of the carrier of D
SI is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . SI is Element of the carrier of D
x is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . x is Element of the carrier of D
dist (R9,c16) is V11() real ext-real Element of REAL
the distance of D is non empty Relation-like [: the carrier of D, the carrier of D:] -defined REAL -valued Function-like total V27([: the carrier of D, the carrier of D:], REAL ) Element of bool [:[: the carrier of D, the carrier of D:],REAL:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set
the distance of D . (R9,c16) is V11() real ext-real Element of REAL
R9 is set
dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT
c16 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . c16 is Element of the carrier of D
diameter R9 is V11() real ext-real Element of REAL
diameter (W . F) is V11() real ext-real Element of REAL
b . F is Element of the carrier of D
abs (diameter (W . F)) is V11() real ext-real Element of REAL
TW is ordinal natural V11() real finite cardinal ext-real non negative set
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW <= b1 } is set
W . TW is Element of bool the carrier of D
D is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of D is non empty set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
TopSpaceMetr D is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
Family_open_set D is Element of bool (bool the carrier of D)
TopStruct(# the carrier of D,(Family_open_set D) #) is non empty strict TopStruct
b is non empty Relation-like non-empty NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) (D) Element of bool [:NAT,(bool the carrier of D):]
(D,b) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
lim (D,b) is V11() real ext-real Element of REAL
meet b is Element of bool the carrier of D
dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT
X is set
b . X is set
rng b is Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
W is set
[:NAT, the carrier of D:] is non empty non trivial non finite set
bool [:NAT, the carrier of D:] is non empty non trivial non finite set
X is non empty Relation-like NAT -defined the carrier of D -valued Function-like total V27( NAT , the carrier of D) Element of bool [:NAT, the carrier of D:]
W is ordinal natural V11() real finite cardinal ext-real non negative set
X . W is Element of the carrier of D
b . W is Element of bool the carrier of D
W is Element of the carrier of D
the carrier of (TopSpaceMetr D) is non empty set
[:NAT, the carrier of (TopSpaceMetr D):] is non empty non trivial non finite set
bool [:NAT, the carrier of (TopSpaceMetr D):] is non empty non trivial non finite set
TW is non empty Relation-like NAT -defined the carrier of (TopSpaceMetr D) -valued Function-like total V27( NAT , the carrier of (TopSpaceMetr D)) Element of bool [:NAT, the carrier of (TopSpaceMetr D):]
s is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
TW ^\ s is non empty Relation-like NAT -defined the carrier of (TopSpaceMetr D) -valued Function-like total V27( NAT , the carrier of (TopSpaceMetr D)) subsequence of TW
bool the carrier of (TopSpaceMetr D) is non empty set
b . s is Element of bool the carrier of D
rng (TW ^\ s) is Element of bool the carrier of (TopSpaceMetr D)
rngs is Element of bool the carrier of (TopSpaceMetr D)
F is set
dom (TW ^\ s) is V141() V142() V143() V144() V145() V146() Element of bool NAT
F is set
(TW ^\ s) . F is set
R is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
R + s is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . (R + s) is Element of bool the carrier of D
X . (R + s) is Element of the carrier of D
f is Element of the carrier of (TopSpaceMetr D)
Lim (TW ^\ s) is Element of bool the carrier of (TopSpaceMetr D)
[:NAT, the carrier of D:] is non empty non trivial non finite set
bool [:NAT, the carrier of D:] is non empty non trivial non finite set
b is non empty Relation-like NAT -defined the carrier of D -valued Function-like total V27( NAT , the carrier of D) Element of bool [:NAT, the carrier of D:]
the carrier of (TopSpaceMetr D) is non empty set
bool the carrier of (TopSpaceMetr D) is non empty set
X is non empty Relation-like non-empty NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) Element of bool [:NAT,(bool the carrier of D):]
(D,X) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
lim (D,X) is V11() real ext-real Element of REAL
meet X is Element of bool the carrier of D
TW is set
f is Element of the carrier of D
s is V11() real ext-real Element of REAL
S is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
rngs is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . rngs is Element of the carrier of D
dist ((b . rngs),f) is V11() real ext-real Element of REAL
the distance of D is non empty Relation-like [: the carrier of D, the carrier of D:] -defined REAL -valued Function-like total V27([: the carrier of D, the carrier of D:], REAL ) Element of bool [:[: the carrier of D, the carrier of D:],REAL:]
[: the carrier of D, the carrier of D:] is non empty set
[:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty non trivial non finite set
the distance of D . ((b . rngs),f) is V11() real ext-real Element of REAL
(D,X) . rngs is V11() real ext-real Element of REAL
((D,X) . rngs) - 0 is V11() real ext-real Element of REAL
abs (((D,X) . rngs) - 0) is V11() real ext-real Element of REAL
X . rngs is Element of bool the carrier of D
diameter (X . rngs) is V11() real ext-real Element of REAL
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : rngs <= b1 } is set
F is Element of bool the carrier of (TopSpaceMetr D)
Cl F is closed Element of bool the carrier of (TopSpaceMetr D)
b . rngs is Element of the carrier of D
dist ((b . rngs),f) is V11() real ext-real Element of REAL
the distance of D . ((b . rngs),f) is V11() real ext-real Element of REAL
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
a is non empty Relation-like non-empty NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
rng a is Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
b is Element of bool (bool the carrier of D)
X is set
W is set
dom a is V141() V142() V143() V144() V145() V146() Element of bool NAT
TW is set
a . TW is set
[:X,NAT:] is set
bool [:X,NAT:] is non empty set
W is Relation-like X -defined NAT -valued Function-like total V27(X, NAT ) Element of bool [:X,NAT:]
rng W is V141() V142() V143() V144() V145() V146() Element of bool NAT
TW is ordinal natural V11() real finite cardinal ext-real non negative set
dom a is V141() V142() V143() V144() V145() V146() Element of bool NAT
a . TW is Element of bool the carrier of D
f is set
dom W is Element of bool X
bool X is non empty set
s is set
W . s is set
S is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
a . S is Element of bool the carrier of D
meet X is set
D is non empty MetrStruct
the carrier of D is non empty set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
TopSpaceMetr D is non empty strict TopSpace-like TopStruct
Family_open_set D is Element of bool (bool the carrier of D)
TopStruct(# the carrier of D,(Family_open_set D) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr D) is non empty set
bool the carrier of (TopSpaceMetr D) is non empty set
bool (bool the carrier of (TopSpaceMetr D)) is non empty set
a is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
rng a is Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
X is Element of bool (bool the carrier of (TopSpaceMetr D))
W is Element of bool the carrier of (TopSpaceMetr D)
dom a is V141() V142() V143() V144() V145() V146() Element of bool NAT
TW is set
a . TW is set
f is ordinal natural V11() real finite cardinal ext-real non negative set
a . f is Element of bool the carrier of D
W is Element of bool the carrier of (TopSpaceMetr D)
dom a is V141() V142() V143() V144() V145() V146() Element of bool NAT
TW is set
a . TW is set
f is ordinal natural V11() real finite cardinal ext-real non negative set
a . f is Element of bool the carrier of D
D is non empty TopSpace-like TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
a is Element of bool (bool the carrier of D)
b is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
rng b is Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
X is ordinal natural V11() real finite cardinal ext-real non negative set
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= X } is set
W is set
dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT
TW is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . TW is Element of bool the carrier of D
X is set
W is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= W } is set
f is Element of bool (bool the carrier of D)
meet f is Element of bool the carrier of D
s is ordinal natural V11() real finite cardinal ext-real non negative set
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= s } is set
meet { (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= s } is set
X is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
W is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= W } is set
W + 1 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= W + 1 } is set
s is set
S is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . S is Element of bool the carrier of D
meet { (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= W } is set
X . W is Element of bool the carrier of D
b . 0 is Element of bool the carrier of D
meet { (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= W + 1 } is set
X . (W + 1) is Element of bool the carrier of D
W is ordinal natural V11() real finite cardinal ext-real non negative set
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= W } is set
W + 1 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
{ H1(b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 in W + 1 } is set
f is set
s is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . s is Element of bool the carrier of D
W is set
dom X is V141() V142() V143() V144() V145() V146() Element of bool NAT
TW is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= TW } is set
meet { (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= TW } is set
X . W is set
W is ordinal natural V11() real finite cardinal ext-real non negative set
X . W is Element of bool the carrier of D
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= W } is set
f is Element of bool (bool the carrier of D)
meet f is Element of bool the carrier of D
W is ordinal natural V11() real finite cardinal ext-real non negative set
X . W is Element of bool the carrier of D
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= W } is set
f is Element of bool (bool the carrier of D)
meet f is Element of bool the carrier of D
W is ordinal natural V11() real finite cardinal ext-real non negative set
X . W is Element of bool the carrier of D
{ (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= W } is set
meet { (b . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= W } is set
D is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
TopSpaceMetr D is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of D is non empty set
Family_open_set D is Element of bool (bool the carrier of D)
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
TopStruct(# the carrier of D,(Family_open_set D) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr D) is non empty set
bool the carrier of (TopSpaceMetr D) is non empty set
bool (bool the carrier of (TopSpaceMetr D)) is non empty set
X is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
b is V11() real ext-real Element of REAL
b (#) X is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
TW is Element of bool (bool the carrier of (TopSpaceMetr D))
meet TW is Element of bool the carrier of (TopSpaceMetr D)
f is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
X . f is V11() real ext-real Element of REAL
f + 1 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
1 / (f + 1) is V11() real ext-real non negative Element of REAL
bool the carrier of D is non empty Element of bool (bool the carrier of D)
f is set
s is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
s + 1 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
1 / (s + 1) is V11() real ext-real non negative Element of REAL
S is Element of bool the carrier of D
diameter S is V11() real ext-real Element of REAL
rngs is ordinal natural V11() real finite cardinal ext-real non negative set
F is Element of bool the carrier of D
rngs + 1 is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
1 / (rngs + 1) is V11() real ext-real non negative Element of REAL
diameter F is V11() real ext-real Element of REAL
[:NAT,(bool the carrier of D):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of D):] is non empty non trivial non finite set
f is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
rng f is Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
s is set
dom f is V141() V142() V143() V144() V145() V146() Element of bool NAT
S is set
f . S is set
rngs is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
f . rngs is Element of bool the carrier of D
bool the carrier of (TopSpaceMetr D) is non empty Element of bool (bool the carrier of (TopSpaceMetr D))
[:NAT,(bool the carrier of (TopSpaceMetr D)):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of (TopSpaceMetr D)):] is non empty non trivial non finite set
s is non empty Relation-like NAT -defined bool the carrier of (TopSpaceMetr D) -valued Function-like total V27( NAT , bool the carrier of (TopSpaceMetr D)) Element of bool [:NAT,(bool the carrier of (TopSpaceMetr D)):]
f . 0 is Element of bool the carrier of D
rngs is ordinal natural V11() real finite cardinal ext-real non negative set
{ (f . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= rngs } is set
meet { (f . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= rngs } is set
s . rngs is Element of bool the carrier of (TopSpaceMetr D)
S is non empty Relation-like non-empty NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
S . rngs is Element of bool the carrier of D
rngs is non empty Relation-like non-empty NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) (D) Element of bool [:NAT,(bool the carrier of D):]
(D,rngs) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
F is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
{ (f . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= F } is set
f . F is Element of bool the carrier of D
s . F is Element of bool the carrier of (TopSpaceMetr D)
meet { (f . b1) where b1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b1 <= F } is set
rngs . F is Element of bool the carrier of D
diameter (rngs . F) is V11() real ext-real Element of REAL
diameter (f . F) is V11() real ext-real Element of REAL
1 + F is non empty ordinal natural V11() real finite cardinal ext-real positive non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
1 / (1 + F) is V11() real ext-real non negative Element of REAL
(b (#) X) . F is V11() real ext-real Element of REAL
X . F is V11() real ext-real Element of REAL
b * (X . F) is V11() real ext-real Element of REAL
(D,rngs) . F is V11() real ext-real Element of REAL
lim X is V11() real ext-real Element of REAL
lim (b (#) X) is V11() real ext-real Element of REAL
b * 0 is V11() real ext-real Element of REAL
lim (D,rngs) is V11() real ext-real Element of REAL
meet rngs is Element of bool the carrier of D
F is set
R9 is set
R9 is Element of bool the carrier of (TopSpaceMetr D)
c16 is set
SI is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
s . SI is Element of bool the carrier of (TopSpaceMetr D)
(s . SI) /\ R9 is Element of bool the carrier of (TopSpaceMetr D)
x is ordinal natural V11() real finite cardinal ext-real non negative set
s . x is Element of bool the carrier of (TopSpaceMetr D)
(s . x) /\ R9 is Element of bool the carrier of (TopSpaceMetr D)
c16 is non empty Relation-like NAT -defined bool the carrier of D -valued Function-like total V27( NAT , bool the carrier of D) Element of bool [:NAT,(bool the carrier of D):]
SI is set
dom c16 is V141() V142() V143() V144() V145() V146() Element of bool NAT
x is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
{ (f . b1) where b1 is ordinal natural V11()