:: COMPL_SP semantic presentation

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)
c<sub>16</sub> 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : W <= b<sub>1</sub> } 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : s <= b<sub>1</sub> } 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW <= b<sub>1</sub> } 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : W <= b<sub>1</sub> } 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW <= b<sub>1</sub> } 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW + 1 <= b<sub>1</sub> } 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW <= b<sub>1</sub> } 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : F <= b<sub>1</sub> } 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
c<sub>16</sub> 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,c<sub>16</sub>) 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,c<sub>16</sub>) is V11() real ext-real Element of REAL
R9 is set
dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT
c<sub>16</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . c<sub>16</sub> 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW <= b<sub>1</sub> } 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : rngs <= b<sub>1</sub> } 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= s } is set
meet { (b . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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
{ H<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= TW } is set
meet { (b . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= W } is set
meet { (b . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= rngs } is set
meet { (f . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= 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)
c<sub>16</sub> 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)
c<sub>16</sub> 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 c<sub>16</sub> 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 . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= x } is set
f . x is Element of bool the carrier of D
x + 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
{ H<sub>2</sub>(b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> in x + 1 } is set
xS is set
j1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
f . j1 is Element of bool the carrier of D
{R9} is non empty trivial finite 1 -element Element of bool (bool the carrier of (TopSpaceMetr D))
{R9} \/ { (f . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= x } is non empty set
xS is set
j1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
f . j1 is Element of bool the carrier of D
meet ({R9} \/ { (f . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= x } ) is set
meet {R9} is Element of bool the carrier of (TopSpaceMetr D)
meet { (f . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= x } is set
(meet {R9}) /\ (meet { (f . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= x } ) is Element of bool the carrier of (TopSpaceMetr D)
R9 /\ (meet { (f . b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> <= x } ) is Element of bool the carrier of (TopSpaceMetr D)
s . x is Element of bool the carrier of (TopSpaceMetr D)
R9 /\ (s . x) is Element of bool the carrier of (TopSpaceMetr D)
c<sub>16</sub> . SI is set
SI is ordinal natural V11() real finite cardinal ext-real non negative set
s . SI is Element of bool the carrier of (TopSpaceMetr D)
c<sub>16</sub> . SI is Element of bool the carrier of D
x is Element of bool the carrier of (TopSpaceMetr D)
x /\ R9 is Element of bool the carrier of (TopSpaceMetr D)
rngs . SI is Element of bool the carrier of D
SI is ordinal natural V11() real finite cardinal ext-real non negative set
c<sub>16</sub> . SI is Element of bool the carrier of D
rngs . SI is Element of bool the carrier of D
(rngs . SI) /\ R9 is Element of bool the carrier of (TopSpaceMetr D)
SI 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):]
SI . 0 is Element of bool the carrier of D
s . 0 is Element of bool the carrier of (TopSpaceMetr D)
(s . 0) /\ R9 is Element of bool the carrier of (TopSpaceMetr D)
(D,SI) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
xS is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(b (#) X) . xS is V11() real ext-real Element of REAL
X . xS is V11() real ext-real Element of REAL
b * (X . xS) is V11() real ext-real Element of REAL
s . xS is Element of bool the carrier of (TopSpaceMetr D)
y is Element of bool the carrier of D
(s . xS) /\ y is Element of bool the carrier of D
SI . xS is Element of bool the carrier of D
rngs . xS is Element of bool the carrier of D
diameter (SI . xS) is V11() real ext-real Element of REAL
diameter (rngs . xS) is V11() real ext-real Element of REAL
(D,rngs) . xS is V11() real ext-real Element of REAL
(s . xS) /\ R9 is Element of bool the carrier of (TopSpaceMetr D)
(D,SI) . xS is V11() real ext-real Element of REAL
lim (D,SI) is V11() real ext-real Element of REAL
y is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
SI . y is Element of bool the carrier of D
s . y is Element of bool the carrier of (TopSpaceMetr D)
(s . y) /\ R9 is Element of bool the carrier of (TopSpaceMetr D)
y + 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
s . (y + 1) is Element of bool the carrier of (TopSpaceMetr D)
SI . (y + 1) is Element of bool the carrier of D
(s . (y + 1)) /\ R9 is Element of bool the carrier of (TopSpaceMetr D)
meet SI is Element of bool the carrier of D
y is set
R is Element of the carrier of D
xS is Element of the carrier of D
dist (R,xS) 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 . (R,xS) is V11() real ext-real Element of REAL
j1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
SI . j1 is Element of bool the carrier of D
s . j1 is Element of bool the carrier of (TopSpaceMetr D)
(s . j1) /\ R9 is Element of bool the carrier of (TopSpaceMetr D)
rngs . j1 is Element of bool the carrier of D
diameter (rngs . j1) is V11() real ext-real Element of REAL
abs (diameter (rngs . j1)) is V11() real ext-real Element of REAL
(D,rngs) . j1 is V11() real ext-real Element of REAL
((D,rngs) . j1) - 0 is V11() real ext-real Element of REAL
abs (((D,rngs) . j1) - 0) is V11() real ext-real Element of REAL
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
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
rng b is Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT
TW 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
b . f is Element of bool the carrier of D
(D,b) . f is V11() real ext-real Element of REAL
s is Element of bool the carrier of D
diameter s is V11() real ext-real Element of REAL
((D,b) . f) - 0 is V11() real ext-real Element of REAL
abs (((D,b) . f) - 0) is V11() real ext-real Element of REAL
X is Element of bool (bool the carrier of (TopSpaceMetr D))
meet X is Element of bool the carrier of (TopSpaceMetr D)
W is set
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
meet b 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 set
a is non empty Element of bool the carrier of D
D | a is non empty strict Reflexive discerning symmetric triangle Discerning SubSpace of D
the carrier of (D | a) is non empty set
bool the carrier of (D | a) is non empty set
b is Element of bool the carrier of D
X is Element of bool the carrier of (D | a)
{} (D | a) 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 | a) (D | a) Element of bool the carrier of (D | a)
{} (D | a) 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 | a) (D | a) Element of bool the carrier of (D | a)
W is set
f is Element of the carrier of (D | a)
TW is Element of the carrier of (D | a)
dist (TW,f) is V11() real ext-real Element of REAL
the distance of (D | a) is non empty Relation-like [: the carrier of (D | a), the carrier of (D | a):] -defined REAL -valued Function-like total V27([: the carrier of (D | a), the carrier of (D | a):], REAL ) Element of bool [:[: the carrier of (D | a), the carrier of (D | a):],REAL:]
[: the carrier of (D | a), the carrier of (D | a):] is non empty set
[:[: the carrier of (D | a), the carrier of (D | a):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (D | a), the carrier of (D | a):],REAL:] is non empty non trivial non finite set
the distance of (D | a) . (TW,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 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 . (s,S) is V11() real ext-real Element of REAL
diameter b is V11() real ext-real Element of REAL
(diameter b) + 0 is V11() real ext-real Element of REAL
(diameter b) + 1 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 | a) 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 | a) (D | a) Element of bool the carrier of (D | a)
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 set
a is non empty Element of bool the carrier of D
D | a is non empty strict Reflexive discerning symmetric triangle Discerning SubSpace of D
the carrier of (D | a) is non empty set
bool the carrier of (D | a) is non empty set
b is Element of bool the carrier of D
diameter b is V11() real ext-real Element of REAL
X is Element of bool the carrier of (D | a)
diameter X is V11() real ext-real Element of REAL
{} (D | a) 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 | a) (D | a) Element of bool the carrier of (D | a)
{} (D | a) 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 | a) (D | a) Element of bool the carrier of (D | a)
W is Element of the carrier of (D | a)
TW is Element of the carrier of (D | a)
dist (W,TW) is V11() real ext-real Element of REAL
the distance of (D | a) is non empty Relation-like [: the carrier of (D | a), the carrier of (D | a):] -defined REAL -valued Function-like total V27([: the carrier of (D | a), the carrier of (D | a):], REAL ) Element of bool [:[: the carrier of (D | a), the carrier of (D | a):],REAL:]
[: the carrier of (D | a), the carrier of (D | a):] is non empty set
[:[: the carrier of (D | a), the carrier of (D | a):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (D | a), the carrier of (D | a):],REAL:] is non empty non trivial non finite set
the distance of (D | a) . (W,TW) 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 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
{} (D | a) 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 | a) (D | a) Element of bool the carrier of (D | a)
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 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 Element of bool the carrier of D
D | a is non empty strict Reflexive discerning symmetric triangle Discerning SubSpace of D
the carrier of (D | a) is non empty set
[:NAT, the carrier of (D | a):] is non empty non trivial non finite set
bool [:NAT, the carrier of (D | a):] is non empty non trivial non finite set
b is non empty Relation-like NAT -defined the carrier of (D | a) -valued Function-like total V27( NAT , the carrier of (D | a)) Element of bool [:NAT, the carrier of (D | a):]
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 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 Element of bool the carrier of D
D | a is non empty strict Reflexive discerning symmetric triangle Discerning SubSpace of D
the carrier of (D | a) is non empty set
[:NAT, the carrier of (D | a):] is non empty non trivial non finite set
bool [:NAT, the carrier of (D | a):] is non empty non trivial non finite set
b is non empty Relation-like NAT -defined the carrier of (D | a) -valued Function-like total V27( NAT , the carrier of (D | a)) Element of bool [:NAT, the carrier of (D | a):]
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
b . f is Element of the carrier of (D | a)
b . s is Element of the carrier of (D | a)
dist ((b . f),(b . s)) is V11() real ext-real Element of REAL
the distance of (D | a) is non empty Relation-like [: the carrier of (D | a), the carrier of (D | a):] -defined REAL -valued Function-like total V27([: the carrier of (D | a), the carrier of (D | a):], REAL ) Element of bool [:[: the carrier of (D | a), the carrier of (D | a):],REAL:]
[: the carrier of (D | a), the carrier of (D | a):] is non empty set
[:[: the carrier of (D | a), the carrier of (D | a):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (D | a), the carrier of (D | a):],REAL:] is non empty non trivial non finite set
the distance of (D | a) . ((b . f),(b . s)) is V11() real ext-real Element of REAL
b . f is Element of the carrier of (D | a)
b . s is Element of the carrier of (D | a)
dist ((b . f),(b . s)) is V11() real ext-real Element of REAL
the distance of (D | a) . ((b . f),(b . s)) is V11() real ext-real Element of REAL
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
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
b . f is Element of the carrier of (D | a)
b . s is Element of the carrier of (D | a)
dist ((b . f),(b . s)) is V11() real ext-real Element of REAL
the distance of (D | a) is non empty Relation-like [: the carrier of (D | a), the carrier of (D | a):] -defined REAL -valued Function-like total V27([: the carrier of (D | a), the carrier of (D | a):], REAL ) Element of bool [:[: the carrier of (D | a), the carrier of (D | a):],REAL:]
[: the carrier of (D | a), the carrier of (D | a):] is non empty set
[:[: the carrier of (D | a), the carrier of (D | a):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (D | a), the carrier of (D | a):],REAL:] is non empty non trivial non finite set
the distance of (D | a) . ((b . f),(b . s)) is V11() real ext-real Element of REAL
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 . ((X . f),(X . s)) is V11() real ext-real Element of REAL
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 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)
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
b is non empty Element of bool the carrier of D
D | b is non empty strict Reflexive discerning symmetric triangle Discerning SubSpace of D
X is Element of bool the carrier of (TopSpaceMetr D)
TopSpaceMetr (D | b) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (D | b) is non empty set
Family_open_set (D | b) is Element of bool (bool the carrier of (D | b))
bool the carrier of (D | b) is non empty set
bool (bool the carrier of (D | b)) is non empty set
TopStruct(# the carrier of (D | b),(Family_open_set (D | b)) #) is non empty strict TopStruct
Cl X is closed Element of bool the carrier of (TopSpaceMetr D)
f is set
s is Element of the carrier of D
bool the carrier of (D | b) is non empty Element of bool (bool the carrier of (D | b))
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
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
cl_Ball (s,(1 / (rngs + 1))) is Element of bool the carrier of D
b /\ (cl_Ball (s,(1 / (rngs + 1)))) is Element of bool the carrier of D
F is ordinal natural V11() real finite cardinal ext-real non negative set
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
cl_Ball (s,(1 / (F + 1))) is Element of bool the carrier of D
b /\ (cl_Ball (s,(1 / (F + 1)))) is Element of bool the carrier of D
[:NAT,(bool the carrier of (D | b)):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of (D | b)):] is non empty non trivial non finite set
S is non empty Relation-like NAT -defined bool the carrier of (D | b) -valued Function-like total V27( NAT , bool the carrier of (D | b)) Element of bool [:NAT,(bool the carrier of (D | b)):]
rngs is set
dom S 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
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
Ball (s,(1 / (F + 1))) is bounded Element of bool the carrier of D
F is Element of bool the carrier of (TopSpaceMetr D)
R is set
R9 is Element of the carrier of D
dist (s,R9) 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 . (s,R9) is V11() real ext-real Element of REAL
cl_Ball (s,(1 / (F + 1))) is Element of bool the carrier of D
b /\ (cl_Ball (s,(1 / (F + 1)))) is Element of bool the carrier of D
S . rngs is set
rngs is ordinal natural V11() real finite cardinal ext-real non negative set
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
cl_Ball (s,(1 / (rngs + 1))) is Element of bool the carrier of D
the carrier of (TopSpaceMetr (D | b)) is non empty set
bool the carrier of (TopSpaceMetr (D | b)) is non empty set
S . rngs is Element of bool the carrier of (D | b)
[#] D is non empty non proper Element of bool the carrier of D
F is Element of bool the carrier of (TopSpaceMetr D)
([#] D) \ F is Element of bool the carrier of D
F ` is Element of bool the carrier of (TopSpaceMetr D)
the carrier of (TopSpaceMetr D) \ F is set
(TopSpaceMetr D) | X is strict TopSpace-like SubSpace of TopSpaceMetr D
[#] ((TopSpaceMetr D) | X) is non proper open closed Element of bool the carrier of ((TopSpaceMetr D) | X)
the carrier of ((TopSpaceMetr D) | X) is set
bool the carrier of ((TopSpaceMetr D) | X) is non empty set
F is Element of bool the carrier of (TopSpaceMetr (D | b))
F /\ ([#] ((TopSpaceMetr D) | X)) is Element of bool the carrier of ((TopSpaceMetr D) | X)
rngs is ordinal natural V11() real finite cardinal ext-real non negative set
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
cl_Ball (s,(1 / (rngs + 1))) is Element of bool the carrier of D
b /\ (cl_Ball (s,(1 / (rngs + 1)))) is Element of bool the carrier of D
S . rngs is Element of bool the carrier of (D | b)
rngs is non empty Relation-like non-empty NAT -defined bool the carrier of (D | b) -valued Function-like total V27( NAT , bool the carrier of (D | b)) (D | b) (D | b) Element of bool [:NAT,(bool the carrier of (D | b)):]
((D | b),rngs) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
R9 is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
R9 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
R9 + 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
(R9 + 1) + 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 / ((R9 + 1) + 1) is V11() real ext-real non negative Element of REAL
cl_Ball (s,(1 / ((R9 + 1) + 1))) is Element of bool the carrier of D
1 / (R9 + 1) is V11() real ext-real non negative Element of REAL
cl_Ball (s,(1 / (R9 + 1))) is Element of bool the carrier of D
SI is set
x is Element of the carrier of D
dist (s,x) is V11() real ext-real Element of REAL
the distance of D . (s,x) is V11() real ext-real Element of REAL
b /\ (cl_Ball (s,(1 / ((R9 + 1) + 1)))) is Element of bool the carrier of D
b /\ (cl_Ball (s,(1 / (R9 + 1)))) is Element of bool the carrier of D
rngs . R9 is Element of bool the carrier of (D | b)
rngs . (R9 + 1) is Element of bool the carrier of (D | b)
R is V11() real ext-real Element of REAL
R (#) R9 is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
F is V11() real ext-real Element of REAL
F (#) R9 is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
SI is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
R9 . SI is V11() real ext-real Element of REAL
SI + 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 / (SI + 1) is V11() real ext-real non negative Element of REAL
SI is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
SI + 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 / (SI + 1) is V11() real ext-real non negative Element of REAL
cl_Ball (s,(1 / (SI + 1))) is Element of bool the carrier of D
(F (#) R9) . SI is V11() real ext-real Element of REAL
R9 . SI is V11() real ext-real Element of REAL
F * (R9 . SI) is V11() real ext-real Element of REAL
(R (#) R9) . SI is V11() real ext-real Element of REAL
R * (R9 . SI) is V11() real ext-real Element of REAL
b /\ (cl_Ball (s,(1 / (SI + 1)))) is Element of bool the carrier of D
diameter (b /\ (cl_Ball (s,(1 / (SI + 1))))) is V11() real ext-real Element of REAL
diameter (cl_Ball (s,(1 / (SI + 1)))) is V11() real ext-real Element of REAL
1 + SI 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 + SI) is V11() real ext-real non negative Element of REAL
2 * H₁(SI) is V11() real ext-real non negative Element of REAL
rngs . SI is Element of bool the carrier of (D | b)
diameter (rngs . SI) is V11() real ext-real Element of REAL
((D | b),rngs) . SI is V11() real ext-real Element of REAL
lim R9 is V11() real ext-real Element of REAL
lim (R (#) R9) is V11() real ext-real Element of REAL
R * 0 is V11() real ext-real Element of REAL
lim (F (#) R9) is V11() real ext-real Element of REAL
F * 0 is V11() real ext-real Element of REAL
lim ((D | b),rngs) is V11() real ext-real Element of REAL
meet rngs is Element of bool the carrier of (D | b)
SI is set
x is Element of the carrier of D
dist (s,x) is V11() real ext-real Element of REAL
the distance of D . (s,x) is V11() real ext-real Element of REAL
y is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
y + 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 / (y + 1) is V11() real ext-real non negative Element of REAL
cl_Ball (s,(1 / (y + 1))) is Element of bool the carrier of D
rngs . y is Element of bool the carrier of (D | b)
b /\ (cl_Ball (s,(1 / (y + 1)))) is Element of bool the carrier of D
1 + y 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 + y) is V11() real ext-real non negative Element of REAL
R9 . y is V11() real ext-real Element of REAL
(R9 . y) - 0 is V11() real ext-real Element of REAL
abs ((R9 . y) - 0) is V11() real ext-real Element of REAL
rngs . 0 is Element of bool the carrier of (D | b)
0 + 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 / (0 + 1) is V11() real ext-real non negative Element of REAL
cl_Ball (s,(1 / (0 + 1))) is Element of bool the carrier of D
b /\ (cl_Ball (s,(1 / (0 + 1)))) is Element of bool the carrier of D
[:NAT, the carrier of (D | b):] is non empty non trivial non finite set
bool [:NAT, the carrier of (D | b):] is non empty non trivial non finite set
f is non empty Relation-like NAT -defined the carrier of (D | b) -valued Function-like total V27( NAT , the carrier of (D | b)) Element of bool [:NAT, the carrier of (D | b):]
[: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
s 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:]
S is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
f . S is Element of the carrier of (D | b)
s . S is Element of the carrier of D
lim s is Element of the carrier of D
S is Element of the carrier of (D | b)
rngs 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
f . F is Element of the carrier of (D | b)
dist ((f . F),S) is V11() real ext-real Element of REAL
the distance of (D | b) is non empty Relation-like [: the carrier of (D | b), the carrier of (D | b):] -defined REAL -valued Function-like total V27([: the carrier of (D | b), the carrier of (D | b):], REAL ) Element of bool [:[: the carrier of (D | b), the carrier of (D | b):],REAL:]
[: the carrier of (D | b), the carrier of (D | b):] is non empty set
[:[: the carrier of (D | b), the carrier of (D | b):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (D | b), the carrier of (D | b):],REAL:] is non empty non trivial non finite set
the distance of (D | b) . ((f . F),S) is V11() real ext-real Element of REAL
f . F is Element of the carrier of (D | b)
dist ((f . F),S) is V11() real ext-real Element of REAL
the distance of (D | b) . ((f . F),S) is V11() real ext-real Element of REAL
s . F is Element of the carrier of D
dist ((s . F),(lim 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 . ((s . F),(lim s)) is V11() real ext-real Element of REAL
D is TopStruct
the carrier of D is set
bool the carrier of D is non empty set
bool (bool the carrier of D) is non empty set
a is Element of bool (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
a is Element of bool (bool the carrier of D)
meet a is Element of bool the carrier of D
COMPLEMENT a is Element of bool (bool the carrier of D)
union (COMPLEMENT a) is Element of bool the carrier of D
(meet a) ` is Element of bool the carrier of D
the carrier of D \ (meet a) is set
[#] D is non empty non proper open closed Element of bool the carrier of D
b is Element of bool (bool the carrier of D)
COMPLEMENT b is Element of bool (bool the carrier of D)
X is set
W is Element of bool the carrier of D
W ` is Element of bool the carrier of D
the carrier of D \ W is set
(W `) ` is Element of bool the carrier of D
the carrier of D \ (W `) is set
meet (COMPLEMENT b) is Element of bool the carrier of D
union b is Element of bool the carrier of D
(union b) ` is Element of bool the carrier of D
the carrier of D \ (union b) is set
([#] D) \ ([#] D) is Element of bool the carrier of D
a is Element of bool (bool the carrier of D)
COMPLEMENT a is Element of bool (bool the carrier of D)
meet (COMPLEMENT a) is Element of bool the carrier of D
union a is Element of bool the carrier of D
(union a) ` is Element of bool the carrier of D
the carrier of D \ (union a) is set
[#] D is non empty non proper open closed Element of bool the carrier of D
([#] D) \ ([#] D) is Element of bool the carrier of D
b is set
meet b is set
X is Element of bool (bool the carrier of D)
COMPLEMENT X is Element of bool (bool the carrier of D)
W is Element of bool (bool the carrier of D)
TW is set
f is Element of bool the carrier of D
f ` is Element of bool the carrier of D
the carrier of D \ f is set
(f `) ` is Element of bool the carrier of D
the carrier of D \ (f `) is set
union W is Element of bool the carrier of D
meet X is Element of bool the carrier of D
(meet X) ` is Element of bool the carrier of D
the carrier of D \ (meet X) is set
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) (D) Element of bool [:NAT,(bool the carrier of D):]
meet a is Element of 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
dom a is V141() V142() V143() V144() V145() V146() Element of bool NAT
b is Element of bool (bool the carrier of D)
X is Element of bool the carrier of D
W is set
a . W is set
meet b 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
a . W is Element of bool the carrier of D
a is Element of bool (bool the carrier of D)
card a is ordinal cardinal set
b is Relation-like Function-like set
dom b is set
rng b 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 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):]
meet W is Element of bool the carrier of D
TW is set
f is set
dom X is V141() V142() V143() V144() V145() V146() Element of bool NAT
s is set
X . 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
X . S is Element of bool the carrier of D
{ (X . b₁) where b₁ 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 set
W . S is Element of bool the carrier of D
meet { (X . b₁) where b₁ 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 set
meet a is Element of bool the carrier of D
meet a is Element of bool the carrier of D
meet a is Element of bool the carrier of D
meet a 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 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 . b₁) where b₁ is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : W <= b₁ } 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
f is Element of bool (bool the carrier of D)
union f is Element of bool the carrier of D
Cl (union f) is closed Element of bool the carrier of D
s is set
dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT
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
s is ordinal natural V11() real finite cardinal ext-real non negative set
{ (b . b₁) where b₁ is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : s <= b₁ } 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 . TW is Element of bool the carrier of D
Cl (b . TW) is closed Element of bool the carrier of D
{ (b . b₁) where b₁ is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW <= b₁ } is set
X . TW is Element of bool the carrier of D
f is Element of bool (bool the carrier of D)
union f is Element of bool the carrier of D
Cl (union f) is closed Element of bool the carrier of D
dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT
X . W is set
W is ordinal natural V11() real finite cardinal ext-real non negative set
TW is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
{ (b . b₁) where b₁ is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW <= b₁ } is set
X . TW is Element of bool the carrier of D
X . W is Element of bool the carrier of D
f is Element of bool (bool the carrier of D)
union f is Element of bool the carrier of D
Cl (union f) is closed Element of bool the carrier of 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):]
meet W is Element of bool the carrier of D
TW is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
{ (b . b₁) where b₁ is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW <= b₁ } is set
W . TW is Element of bool the carrier of D
f is Element of bool (bool the carrier of D)
union f is Element of bool the carrier of D
Cl (union f) is closed Element of bool the carrier of 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 . b₁) where b₁ is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW + 1 <= b₁ } is set
W . (TW + 1) is Element of bool the carrier of D
s is Element of bool (bool the carrier of D)
union s is Element of bool the carrier of D
Cl (union s) is closed Element of bool the carrier of 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 bool the carrier of D
TW is non empty Element of bool (bool the carrier of D)
[:NAT,TW:] is non empty non trivial non finite set
bool [:NAT,TW:] is non empty non trivial non finite set
f is non empty Relation-like NAT -defined TW -valued Function-like total V27( NAT ,TW) Element of bool [:NAT,TW:]
f " is Relation-like Function-like set
[:TW,NAT:] is non empty non trivial non finite set
bool [:TW,NAT:] is non empty non trivial non finite set
s is Relation-like Function-like set
S is non empty Relation-like TW -defined NAT -valued Function-like total V27(TW, NAT ) Element of bool [:TW,NAT:]
rngs is set
F is Element of the carrier of D
F is Element of bool the carrier of D
{ b₁ where b₁ is Element of bool the carrier of D : ( b₁ in TW & not b₁ misses F ) } is set
{ H₁(b₁) where b₁ is Element of TW : b₁ in { b₁ where b₂ is Element of bool the carrier of D : ( b₁ in TW & not b₁ misses F ) } } is set
R9 is set
c₁₆ is Element of TW
S . c₁₆ is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
R9 is V141() V142() V143() V144() V145() V146() Element of bool NAT
c₁₆ is ordinal natural V11() real finite cardinal ext-real non negative set
c₁₆ + 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
W . (c₁₆ + 1) is Element of bool the carrier of D
{ (b . b₁) where b₁ is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : c₁₆ + 1 <= b₁ } is set
x is Element of bool (bool the carrier of D)
union x is Element of bool the carrier of D
Cl (union x) is closed Element of bool the carrier of D
clf x is Element of bool (bool the carrier of D)
union (clf x) is Element of bool the carrier of D
y is set
xS is Element of bool the carrier of D
j1 is Element of bool the carrier of D
Cl j1 is closed Element of bool the carrier of D
yS is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . yS is Element of bool the carrier of D
f . yS is Element of TW
b " is Relation-like Function-like set
(b ") . (b . yS) 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
{ (b . b₁) where b₁ is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : TW <= b₁ } is set
f is Element of bool (bool the carrier of D)
union f is Element of bool the carrier of D
Cl (union f) is closed 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
a is Element of bool (bool the carrier of D)
[:NAT,a:] is set
bool [:NAT,a:] is non empty set
b is Relation-like NAT -defined a -valued Function-like V27( NAT ,a) Element of bool [:NAT,a:]
rng b is Element of bool a
bool a 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
W 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):]
dom X is V141() V142() V143() V144() V145() V146() Element of bool NAT
X . W is set
rng X is Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
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):]
meet W 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
a is Element of bool (bool the carrier of D)
{} D is empty trivial proper ordinal natural V11() real finite V34() cardinal 0 -element open closed ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() 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
a is Element of bool the carrier of D
Der a is Element of bool the carrier of D
{ {b₁} where b₁ is Element of the carrier of D : b₁ in a } is set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
X is Element of bool (bool the carrier of D)
{ H₁(b₁) where b₁ is Element of bool the carrier of D : b₁ in X } is set
TW is set
f is Element of the carrier of D
{f} is non empty trivial finite 1 -element Element of bool the carrier of D
meet {f} is set
TW is Element of the carrier of D
f is open Element of bool the carrier of D
a /\ f is Element of bool the carrier of D
{ b₁ where b₁ is Element of bool the carrier of D : ( b₁ in X & not b₁ misses f ) } is set
{TW} is non empty trivial finite 1 -element Element of bool the carrier of D
{{TW}} is non empty trivial finite V34() 1 -element Element of bool (bool the carrier of D)
S is set
rngs is Element of bool the carrier of D
F is Element of the carrier of D
{F} is non empty trivial finite 1 -element Element of bool the carrier of D
TW is Element of bool the carrier of D
card TW is ordinal cardinal set
f is Element of the carrier of D
{f} is non empty trivial finite 1 -element Element of bool the carrier of D
D is non empty set
bool D is non empty Element of bool (bool D)
bool D is non empty set
bool (bool D) is non empty set
[:NAT,(bool D):] is non empty non trivial non finite set
bool [:NAT,(bool D):] is non empty non trivial non finite set
[:NAT,D:] is non empty non trivial non finite set
bool [:NAT,D:] is non empty non trivial non finite set
a is non empty Relation-like NAT -defined bool D -valued Function-like total V27( NAT , bool D) Element of bool [:NAT,(bool D):]
meet a is Element of bool D
b is non empty Relation-like NAT -defined D -valued Function-like total V27( NAT ,D) Element of bool [:NAT,D:]
rng b is Element of bool D
dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT
X is set
{X} is non empty trivial finite 1 -element set
b " {X} 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
TW is set
f is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . f is Element of D
a . f is Element of bool D
TW is ordinal natural V11() real finite cardinal ext-real non negative set
a . TW is Element of bool D
TW is ordinal natural V11() real finite cardinal ext-real non negative set
a . TW is Element of bool D
a . W is Element of bool D
D is non empty TopSpace-like T_0 T_1 TopStruct
the carrier of D is non empty set
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)
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) (D) Element of bool [:NAT,(bool the carrier of D):]
meet a is Element of bool the carrier of D
b is set
a . b is set
dom a 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
a . X is Element of bool the carrier of D
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
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:]
rng b is Element of bool the carrier of D
W is ordinal natural V11() real finite cardinal ext-real non negative set
b . W is Element of the carrier of D
a . W is Element of bool the carrier of D
dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT
X is Element of bool the carrier of D
Der X is Element of bool the carrier of D
W is set
TW is Element of the carrier of D
f is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
a . f is Element of bool the carrier of D
(a . f) ` is Element of bool the carrier of D
the carrier of D \ (a . f) is set
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
{ H<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b<sub>1</sub> in f + 1 } is set
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
S is Element of bool the carrier of D
{TW} is non empty trivial finite 1 -element closed Element of bool the carrier of D
S \ {TW} is Element of bool the carrier of D
((a . f) `) \ (S \ {TW}) is Element of bool the carrier of D
F is Element of bool the carrier of D
X /\ F is Element of bool the carrier of D
F is Element of the carrier of D
R is set
b . R is set
R9 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
R9 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
a . R9 is Element of bool the carrier of D
R9 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
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 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):]
meet a is Element of bool the carrier of D
b is set
a . b is set
dom a 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
a . X is Element of bool the carrier of D
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
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:]
rng b is Element of bool the carrier of D
X is Element of bool the carrier of D
{ {b₁} where b₁ is Element of the carrier of D : b₁ in X } is set
TW is Element of bool (bool the carrier of D)
f is Element of the carrier of D
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
(a . s) ` is Element of bool the carrier of D
the carrier of D \ (a . s) is set
S is Element of bool the carrier of D
{ b₁ where b₁ is Element of bool the carrier of D : ( b₁ in TW & not b₁ misses S ) } is set
{ H₂(b₁) where b₁ is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : b₁ in s } is set
F is set
R is Element of bool the carrier of D
R9 is Element of the carrier of D
{R9} is non empty trivial finite 1 -element Element of bool the carrier of D
dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT
R9 is set
b . R9 is set
c₁₆ is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
a . c₁₆ is Element of bool the carrier of D
{ H₁(b₁) where b₁ is Element of bool the carrier of D : b₁ in TW } is set
s is set
S is Element of the carrier of D
{S} is non empty trivial finite 1 -element Element of bool the carrier of D
meet {S} is set
s is ordinal natural V11() real finite cardinal ext-real non negative set
b . s is Element of the carrier of D
a . s is Element of bool the carrier of D
s is Element of bool the carrier of D
card s is ordinal cardinal set
S is Element of the carrier of D
{S} is non empty trivial finite 1 -element 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
a is Element of bool (bool the carrier of D)
a is Element of bool (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
a is Element of bool (bool the carrier of D)
a is Element of bool (bool the carrier of D)
D is non empty TopSpace-like T_0 T_1 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
a is Element of bool (bool the carrier of D)
a is Element of bool the carrier of D
Der a is Element of bool the carrier of D
a is Element of bool the carrier of D
Der a is Element of bool the carrier of D
D is non empty TopSpace-like T_0 T_1 TopStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
a is Element of bool the carrier of D
Der a is Element of bool the carrier of D
b is non empty TopSpace-like T_0 T_1 TopStruct
the carrier of b is non empty set
bool the carrier of b is non empty set
F₁() is non empty set
bool F₁() is non empty set
bool F₁() is non empty Element of bool (bool F₁())
bool (bool F₁()) is non empty set
a is Relation-like set
[:F₁(),F₁():] is non empty set
a /\ [:F₁(),F₁():] is set
bool [:F₁(),F₁():] is non empty set
a |_2 F₁() is Relation-like set
b is Relation-like F₁() -defined F₁() -valued Element of bool [:F₁(),F₁():]
RelStr(# F₁(),b #) is strict RelStr
X is non empty RelStr
the carrier of X is non empty set
[: the carrier of X,(bool F₁()):] is non empty set
bool [: the carrier of X,(bool F₁()):] is non empty set
PFuncs ( the carrier of X,(bool F₁())) is set
TW is set
f is set
s is Relation-like the carrier of X -defined bool F₁() -valued Function-like Element of bool [: the carrier of X,(bool F₁()):]
rng s is Element of bool (bool F₁())
bool (bool F₁()) is non empty set
union (rng s) is Element of bool F₁()
S is Element of F₁()
{S} is non empty trivial finite 1 -element Element of bool F₁()
(union (rng s)) \/ {S} is non empty Element of bool F₁()
rngs is Element of F₁()
F is Relation-like the carrier of X -defined bool F₁() -valued Function-like Element of bool [: the carrier of X,(bool F₁()):]
rng F is Element of bool (bool F₁())
union (rng F) is Element of bool F₁()
{rngs} is non empty trivial finite 1 -element Element of bool F₁()
(union (rng F)) \/ {rngs} is non empty Element of bool F₁()
F is Element of F₁()
s is Relation-like the carrier of X -defined bool F₁() -valued Function-like Element of bool [: the carrier of X,(bool F₁()):]
rng s is Element of bool (bool F₁())
bool (bool F₁()) is non empty set
union (rng s) is Element of bool F₁()
S is Element of F₁()
rngs is Element of F₁()
F is Relation-like the carrier of X -defined bool F₁() -valued Function-like Element of bool [: the carrier of X,(bool F₁()):]
rng F is Element of bool (bool F₁())
union (rng F) is Element of bool F₁()
{rngs} is non empty trivial finite 1 -element Element of bool F₁()
(union (rng F)) \/ {rngs} is non empty Element of bool F₁()
F is Element of F₁()
R is Element of F₁()
s is Relation-like the carrier of X -defined bool F₁() -valued Function-like Element of bool [: the carrier of X,(bool F₁()):]
rng s is Element of bool (bool F₁())
bool (bool F₁()) is non empty set
union (rng s) is Element of bool F₁()
S is Element of F₁()
rngs is Element of F₁()
[: the carrier of X,(PFuncs ( the carrier of X,(bool F₁()))):] is set
[:[: the carrier of X,(PFuncs ( the carrier of X,(bool F₁()))):],(bool F₁()):] is set
bool [:[: the carrier of X,(PFuncs ( the carrier of X,(bool F₁()))):],(bool F₁()):] is non empty set
TW is Relation-like [: the carrier of X,(PFuncs ( the carrier of X,(bool F₁()))):] -defined bool F₁() -valued Function-like total V27([: the carrier of X,(PFuncs ( the carrier of X,(bool F₁()))):], bool F₁()) Element of bool [:[: the carrier of X,(PFuncs ( the carrier of X,(bool F₁()))):],(bool F₁()):]
the InternalRel of X is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
s is non empty Relation-like the carrier of X -defined bool F₁() -valued Function-like total V27( the carrier of X, bool F₁()) Element of bool [: the carrier of X,(bool F₁()):]
bool (bool F₁()) is non empty set
rng s is Element of bool (bool F₁())
S is Element of bool (bool F₁())
union S is Element of bool F₁()
rngs is Element of bool F₁()
field b is set
F is Element of the carrier of X
s . F is set
the InternalRel of X -Seg F is set
{F} is non empty trivial finite 1 -element set
( the InternalRel of X -Seg F) \/ {F} is non empty set
s | ( the InternalRel of X -Seg F) is Relation-like the carrier of X -defined bool F₁() -valued Function-like Element of bool [: the carrier of X,(bool F₁()):]
rng (s | ( the InternalRel of X -Seg F)) is Element of bool (bool F₁())
union (rng (s | ( the InternalRel of X -Seg F))) is Element of bool F₁()
R is set
R9 is set
dom (s | ( the InternalRel of X -Seg F)) is Element of bool the carrier of X
bool the carrier of X is non empty set
R9 is set
(s | ( the InternalRel of X -Seg F)) . R9 is set
c₁₆ is Element of the carrier of X
{c₁₆} is non empty trivial finite 1 -element Element of bool the carrier of X
[c₁₆,F] is non empty Element of [: the carrier of X, the carrier of X:]
{c₁₆,F} is non empty finite set
{c₁₆} is non empty trivial finite 1 -element set
{{c₁₆,F},{c₁₆}} is non empty finite V34() set
the InternalRel of X -Seg c₁₆ is set
( the InternalRel of X -Seg c₁₆) \/ {c₁₆} is non empty set
s . c₁₆ is Element of bool F₁()
(s | ( the InternalRel of X -Seg F)) . c₁₆ is set
s . F is Element of bool F₁()
TW . (F,(s | ( the InternalRel of X -Seg F))) is set
{F} is non empty trivial finite 1 -element Element of bool the carrier of X
bool the carrier of X is non empty set
(union (rng (s | ( the InternalRel of X -Seg F)))) \/ {F} is non empty set
( the InternalRel of X -Seg F) \/ {F} is non empty set
R is Element of F₁()
R is Element of F₁()
{F} is non empty trivial finite 1 -element Element of bool the carrier of X
bool the carrier of X is non empty set
( the InternalRel of X -Seg F) \/ {F} is non empty set
R is Element of F₁()
R9 is Element of F₁()
R is Element of F₁()
F is Element of F₁()
F is set
dom s is Element of bool the carrier of X
bool the carrier of X is non empty set
R is set
s . R is set
R9 is Element of the carrier of X
s . R9 is set
R9 is Element of the carrier of X
s . R9 is set
the InternalRel of X -Seg R9 is set
s | ( the InternalRel of X -Seg R9) is Relation-like the carrier of X -defined bool F₁() -valued Function-like Element of bool [: the carrier of X,(bool F₁()):]
s . R9 is Element of bool F₁()
TW . (R9,(s | ( the InternalRel of X -Seg R9))) is set
rng (s | ( the InternalRel of X -Seg R9)) is Element of bool (bool F₁())
union (rng (s | ( the InternalRel of X -Seg R9))) is Element of bool F₁()
{R9} is non empty trivial finite 1 -element Element of bool the carrier of X
(union (rng (s | ( the InternalRel of X -Seg R9)))) \/ {R9} is non empty set
rng (s | ( the InternalRel of X -Seg R9)) is Element of bool (bool F₁())
union (rng (s | ( the InternalRel of X -Seg R9))) is Element of bool F₁()
SI is Element of F₁()
rng (s | ( the InternalRel of X -Seg R9)) is Element of bool (bool F₁())
union (rng (s | ( the InternalRel of X -Seg R9))) is Element of bool F₁()
SI is Element of F₁()
rng (s | ( the InternalRel of X -Seg R9)) is Element of bool (bool F₁())
union (rng (s | ( the InternalRel of X -Seg R9))) is Element of bool F₁()
SI is set
dom (s | ( the InternalRel of X -Seg R9)) is Element of bool the carrier of X
x is set
(s | ( the InternalRel of X -Seg R9)) . x is set
y is Element of the carrier of X
[y,R9] is non empty Element of [: the carrier of X, the carrier of X:]
{y,R9} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,R9},{y}} is non empty finite V34() set
s . y is set
s . F is set
F is Element of F₁()
F is Element of F₁()
[F,F] is non empty Element of [:F₁(),F₁():]
{F,F} is non empty finite set
{F} is non empty trivial finite 1 -element set
{{F,F},{F}} is non empty finite V34() set
s . F is set
the InternalRel of X -Seg F is set
s | ( the InternalRel of X -Seg F) is Relation-like the carrier of X -defined bool F₁() -valued Function-like Element of bool [: the carrier of X,(bool F₁()):]
dom (s | ( the InternalRel of X -Seg F)) is Element of bool the carrier of X
(s | ( the InternalRel of X -Seg F)) . F is set
rng (s | ( the InternalRel of X -Seg F)) is Element of bool (bool F₁())
s . F is set
union (rng (s | ( the InternalRel of X -Seg F))) is Element of bool F₁()
F is Element of F₁()
F is Element of F₁()
[F,F] is non empty Element of [:F₁(),F₁():]
{F,F} is non empty finite set
{F} is non empty trivial finite 1 -element set
{{F,F},{F}} is non empty finite V34() set
[F,F] is non empty Element of [:F₁(),F₁():]
{F,F} is non empty finite set
{F} is non empty trivial finite 1 -element set
{{F,F},{F}} is non empty finite V34() set
F is Element of F₁()
s . F is set
dom s is Element of bool the carrier of X
bool the carrier of X is non empty set
the InternalRel of X -Seg F is set
s | ( the InternalRel of X -Seg F) is Relation-like the carrier of X -defined bool F₁() -valued Function-like Element of bool [: the carrier of X,(bool F₁()):]
rng (s | ( the InternalRel of X -Seg F)) is Element of bool (bool F₁())
union (rng (s | ( the InternalRel of X -Seg F))) is Element of bool F₁()
F is Element of F₁()
D is non empty Reflexive symmetric MetrStruct
the carrier of D is non empty set
bool the carrier of D is non empty set
a is V11() real ext-real Element of REAL
X is Element of the carrier of D
dist (X,X) 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,X) is V11() real ext-real Element of REAL
X is Element of the carrier of D
W is Element of 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
S is Element of the carrier of D
s is Element of the carrier of D
rngs is Element of the carrier of D
F is Element of the carrier of D
dist (rngs,F) is V11() real ext-real Element of REAL
the distance of D . (rngs,F) is V11() real ext-real Element of REAL
X is Element of bool the carrier of D
W is Element of the carrier of D
TW is Element of the carrier of D
dist (W,TW) 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 . (W,TW) is V11() real ext-real Element of REAL
W is Element of the carrier of D
TW is Element of the carrier of D
Ball (TW,a) is Element of bool the carrier of 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
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
a is V11() real ext-real Element of REAL
b is Element of bool the carrier of D
a / 2 is V11() real ext-real Element of REAL
bool (bool the carrier of D) is non empty set
X is Element of bool (bool the carrier of D)
union X is Element of bool the carrier of D
bool the carrier of D is non empty Element of bool (bool the carrier of D)
W is set
TW is set
f is Element of bool the carrier of D
[:b,(bool the carrier of D):] is set
bool [:b,(bool the carrier of D):] is non empty set
W is Relation-like b -defined bool the carrier of D -valued Function-like total V27(b, bool the carrier of D) Element of bool [:b,(bool the carrier of D):]
TW is set
f is set
W . TW is set
W . f is set
rngs is Element of the carrier of D
Ball (rngs,(a / 2)) is bounded Element of bool the carrier of D
s is Element of the carrier of D
dist (s,rngs) 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 . (s,rngs) is V11() real ext-real Element of REAL
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
dist (rngs,S) is V11() real ext-real Element of REAL
the distance of D . (rngs,S) is V11() real ext-real Element of REAL
(dist (s,rngs)) + (dist (rngs,S)) is V11() real ext-real Element of REAL
(a / 2) + (a / 2) is V11() real ext-real Element of REAL
rng W is Element of bool (bool the carrier of D)
bool (bool the carrier of D) is non empty set
TW is set
dom W is Element of bool b
bool b is non empty set
f is set
W . f is set
dom W is Element of bool b
bool b is non empty set
a is V11() real ext-real Element of REAL
bool (bool the carrier of D) is non empty set
b is Element of bool the carrier of D
{ H₁(b₁) where b₁ is Element of the carrier of D : b₁ in b } is set
bool the carrier of D is non empty Element of bool (bool the carrier of D)
W is set
TW is Element of the carrier of D
Ball (TW,a) is bounded Element of bool the carrier of D
W is Element of bool (bool the carrier of D)
union W is Element of bool the carrier of D
TW is set
f is Element of the carrier of D
s is Element of the carrier of D
Ball (s,a) is bounded Element of bool the carrier of D
TW is Element of bool the carrier of D
f is Element of the carrier of D
Ball (f,a) is bounded Element of bool the carrier of 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
bool (bool the carrier of (TopSpaceMetr D)) is non empty set
b is V11() real ext-real Element of REAL
X is Element of bool the carrier of D
{ {b₁} where b₁ is Element of the carrier of (TopSpaceMetr D) : b₁ in X } is set
b / 2 is V11() real ext-real Element of REAL
W is Element of bool (bool the carrier of (TopSpaceMetr D))
TW is Element of the carrier of (TopSpaceMetr D)
f is Element of the carrier of D
Ball (f,(b / 2)) is bounded Element of bool the carrier of D
s is Element of bool the carrier of (TopSpaceMetr D)
{ b₁ where b₁ is Element of bool the carrier of (TopSpaceMetr D) : ( b₁ in W & not b₁ misses s ) } is set
dist (f,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 . (f,f) is V11() real ext-real Element of REAL
rngs is set
F is Element of bool the carrier of (TopSpaceMetr D)
F is Element of the carrier of (TopSpaceMetr D)
{F} is non empty trivial finite 1 -element Element of bool the carrier of (TopSpaceMetr D)
R is Element of the carrier of D
dist (f,R) is V11() real ext-real Element of REAL
the distance of D . (f,R) is V11() real ext-real Element of REAL
rngs is Element of the carrier of D
dist (rngs,f) is V11() real ext-real Element of REAL
the distance of D . (rngs,f) is V11() real ext-real Element of REAL
rngs is Element of the carrier of D
dist (rngs,f) is V11() real ext-real Element of REAL
the distance of D . (rngs,f) is V11() real ext-real Element of REAL
{rngs} is non empty trivial finite 1 -element bounded Element of bool the carrier of D
{{rngs}} is non empty trivial finite V34() 1 -element Element of bool (bool the carrier of D)
F is set
F is Element of bool the carrier of (TopSpaceMetr D)
R is Element of the carrier of (TopSpaceMetr D)
{R} is non empty trivial finite 1 -element Element of bool the carrier of (TopSpaceMetr D)
R9 is Element of the carrier of D
dist (f,R9) is V11() real ext-real Element of REAL
the distance of D . (f,R9) is V11() real ext-real Element of REAL
(b / 2) + (b / 2) is V11() real ext-real Element of REAL
(dist (rngs,f)) + (dist (f,R9)) is V11() real ext-real Element of REAL
dist (rngs,R9) is V11() real ext-real Element of REAL
the distance of D . (rngs,R9) is V11() real ext-real Element of REAL
rngs is Element of the carrier of D
dist (rngs,f) is V11() real ext-real Element of REAL
the distance of D . (rngs,f) is V11() real ext-real Element of REAL
D is non empty Reflexive symmetric triangle MetrStruct
TopSpaceMetr D is non empty strict TopSpace-like 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
b is V11() real ext-real Element of REAL
X is Element of bool the carrier of D
the carrier of (TopSpaceMetr D) is non empty set
bool the carrier of (TopSpaceMetr D) is non empty set
W is Element of bool the carrier of (TopSpaceMetr D)
{ {b₁} where b₁ is Element of the carrier of (TopSpaceMetr D) : b₁ in W } is set
bool (bool the carrier of (TopSpaceMetr D)) is non empty set
s is Element of bool the carrier of (TopSpaceMetr D)
f is Element of bool (bool the carrier of (TopSpaceMetr D))
card s is ordinal cardinal set
S is Element of the carrier of (TopSpaceMetr D)
{S} is non empty trivial finite 1 -element Element of bool the carrier of (TopSpaceMetr D)
{ H₁(b₁) where b₁ is Element of bool the carrier of (TopSpaceMetr D) : b₁ in f } is set
S is set
rngs is Element of the carrier of (TopSpaceMetr D)
{rngs} is non empty trivial finite 1 -element Element of bool the carrier of (TopSpaceMetr D)
meet {rngs} 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
bool the carrier of (TopSpaceMetr D) is non empty Element of bool (bool the carrier of (TopSpaceMetr D))
bool (bool the carrier of (TopSpaceMetr D)) is non empty Element of bool (bool (bool the carrier of (TopSpaceMetr D)))
bool (bool the carrier of (TopSpaceMetr D)) is non empty set
bool (bool (bool the carrier of (TopSpaceMetr D))) is non empty set
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
X + 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 / (X + 1) is V11() real ext-real non negative Element of REAL
W is Element of bool (bool the carrier of (TopSpaceMetr D))
union W is Element of bool the carrier of (TopSpaceMetr D)
TW is ordinal natural V11() real finite cardinal ext-real non negative set
f is Element of bool (bool the carrier of (TopSpaceMetr D))
union f is Element of bool the carrier of (TopSpaceMetr D)
s is Element of bool the carrier of 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
1 / (TW + 1) is V11() real ext-real non negative Element of REAL
[:NAT,(bool (bool the carrier of (TopSpaceMetr D))):] is non empty non trivial non finite set
bool [:NAT,(bool (bool the carrier of (TopSpaceMetr D))):] is non empty non trivial non finite set
b is non empty Relation-like NAT -defined bool (bool the carrier of (TopSpaceMetr D)) -valued Function-like total V27( NAT , bool (bool the carrier of (TopSpaceMetr D))) Element of bool [:NAT,(bool (bool the carrier of (TopSpaceMetr D))):]
Union b is Element of bool (bool the carrier of (TopSpaceMetr D))
dom b is V141() V142() V143() V144() V145() V146() Element of bool NAT
W is Element of bool the carrier of (TopSpaceMetr D)
TW is Element of the carrier of (TopSpaceMetr D)
f is Element of the carrier of D
s is V11() real ext-real set
Ball (f,s) is bounded Element of bool the carrier of D
S is V11() real ext-real Element of REAL
S / 2 is V11() real ext-real Element of REAL
rngs is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
1 / rngs is V11() real ext-real non negative Element of REAL
(S / 2) + (S / 2) is V11() real ext-real Element of REAL
(1 / rngs) + (1 / rngs) is V11() real ext-real non negative Element of REAL
rngs - 1 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
b . F is Element of bool (bool the carrier of (TopSpaceMetr D))
F is Element of bool (bool the carrier of (TopSpaceMetr D))
union F is Element of bool the carrier of (TopSpaceMetr D)
R is set
R9 is Element of bool the carrier of D
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
R9 is Element of the carrier of D
Ball (R9,(1 / (F + 1))) is bounded Element of bool the carrier of D
Ball (R9,(1 / rngs)) is bounded Element of bool the carrier of D
c₁₆ is Element of bool the carrier of (TopSpaceMetr D)
rng b is Element of bool (bool (bool the carrier of (TopSpaceMetr D)))
bool (bool (bool the carrier of (TopSpaceMetr D))) is non empty set
union (rng b) is Element of bool (bool the carrier of (TopSpaceMetr D))
SI is set
x is Element of the carrier of D
dist (x,R9) 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,R9) is V11() real ext-real Element of REAL
dist (R9,f) is V11() real ext-real Element of REAL
the distance of D . (R9,f) is V11() real ext-real Element of REAL
(dist (x,R9)) + (dist (R9,f)) is V11() real ext-real Element of REAL
dist (x,f) is V11() real ext-real Element of REAL
the distance of D . (x,f) is V11() real ext-real Element of REAL
Ball (f,S) is bounded Element of bool the carrier of D
{ (card b₁) where b₁ is open V113( TopSpaceMetr D) Element of bool (bool the carrier of (TopSpaceMetr D)) : verum } is set
the topology of (TopSpaceMetr D) is non empty Element of bool (bool the carrier of (TopSpaceMetr D))
TW is set
rng b is Element of bool (bool (bool the carrier of (TopSpaceMetr D)))
bool (bool (bool the carrier of (TopSpaceMetr D))) is non empty set
union (rng b) is Element of bool (bool the carrier of (TopSpaceMetr D))
f is set
S is set
b . S is Element of bool (bool the carrier of (TopSpaceMetr D))
s is Element of bool the carrier of (TopSpaceMetr D)
rngs is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
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
F is Element of the carrier of D
Ball (F,(1 / (rngs + 1))) is bounded Element of bool the carrier of D
card (Union b) is ordinal cardinal set
TW is set
f is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
b . f is Element of bool (bool the carrier of (TopSpaceMetr D))
s is Element of bool (bool the carrier of (TopSpaceMetr D))
b . TW is Element of bool (bool the carrier of (TopSpaceMetr D))
weight (TopSpaceMetr D) is ordinal cardinal set
meet { (card b₁) where b₁ is open V113( TopSpaceMetr D) Element of bool (bool the carrier of (TopSpaceMetr D)) : verum } is set
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
a is open V113(D) Element of bool (bool the carrier of D)
card a is ordinal cardinal set
b is Element of bool (bool the carrier of D)
bool the carrier of D is non empty Element of bool (bool the carrier of D)
X is set
W is Element of bool the carrier of D
TW is set
TW is set
f is Element of bool the carrier of D
s is Element of bool the carrier of D
S is set
W is Element of bool the carrier of D
{} D is empty trivial proper ordinal natural V11() real finite V34() cardinal 0 -element open closed ext-real non positive non negative V141() V142() V143() V144() V145() V146() V147() Element of bool the carrier of D
TW is Element of bool the carrier of D
f is set
W is Element of bool the carrier of D
TW is set
[:a,(bool the carrier of D):] is set
bool [:a,(bool the carrier of D):] is non empty set
X is Relation-like a -defined bool the carrier of D -valued Function-like total V27(a, bool the carrier of D) Element of bool [:a,(bool the carrier of D):]
bool (bool the carrier of D) is non empty set
rng X is Element of bool (bool the carrier of D)
{0} is non empty trivial finite V34() 1 -element V141() V142() V143() V144() V145() V146() set
(rng X) \ {0} is Element of bool (bool the carrier of D)
W is Element of bool (bool the carrier of D)
dom X is Element of bool a
bool a is non empty set
TW is set
f is set
X . f is set
s is Element of bool the carrier of D
S is set
X . s is set
S is set
union W is Element of bool the carrier of D
TW is set
f is Element of the carrier of D
s is Element of bool the carrier of D
S is Element of bool the carrier of D
X . S is set
rngs is Element of bool the carrier of D
[#] D is non empty non proper open closed Element of bool the carrier of D
card (rng X) is ordinal cardinal 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
b is Element of bool (bool the carrier of (TopSpaceMetr D))
X is Element of bool (bool the carrier of (TopSpaceMetr D))
W is Element of bool (bool the carrier of (TopSpaceMetr D))
D is set
bool D is non empty set
bool (bool D) is non empty set
a is Element of bool (bool D)
union a is Element of bool D
b is Element of bool D
{b} is non empty trivial finite 1 -element Element of bool (bool D)
INTERSECTION (a,{b}) is set
[:a,{b}:] is set
card [:a,{b}:] is ordinal cardinal set
card a is ordinal cardinal set
card (INTERSECTION (a,{b})) is ordinal cardinal set
W is set
TW is set
TW /\ b is Element of bool D
[:b,(INTERSECTION (a,{b})):] is set
bool [:b,(INTERSECTION (a,{b})):] is non empty set
W is Relation-like b -defined INTERSECTION (a,{b}) -valued Function-like V27(b, INTERSECTION (a,{b})) Element of bool [:b,(INTERSECTION (a,{b})):]
TW is set
dom W is Element of bool b
bool b is non empty set
f is set
rng W is Element of bool (INTERSECTION (a,{b}))
bool (INTERSECTION (a,{b})) is non empty set
f is set
{f} is non empty trivial finite 1 -element set
W " {f} is Element of bool b
s is set
S is set
s /\ S is set
rngs is Element of bool D
rngs /\ b is Element of bool D
F is set
W . F 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
W 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 (#) W is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
bool the carrier of D is non empty Element of bool (bool the carrier of D)
f is set
the carrier of (TopSpaceMetr D) is non empty set
bool the carrier of (TopSpaceMetr D) is non empty set
s is Element of bool the carrier of D
diameter s is V11() real ext-real Element of REAL
F is Element of bool the carrier of D
F is Element of bool the carrier of D
R is Element of bool the carrier of D
diameter R is V11() real ext-real Element of REAL
diameter F is V11() real ext-real Element of REAL
(diameter F) / 2 is V11() real ext-real Element of REAL
R9 is Element of bool the carrier of D
(diameter s) / 4 is V11() real ext-real Element of REAL
F is Element of bool (bool the carrier of D)
union F is Element of bool the carrier of D
F is Element of bool the carrier of D
F /\ s is Element of bool the carrier of D
R9 is Element of the carrier of D
Ball (R9,((diameter s) / 4)) is bounded Element of bool the carrier of D
diameter (F /\ s) is V11() real ext-real Element of REAL
diameter F is V11() real ext-real Element of REAL
2 * ((diameter s) / 4) is V11() real ext-real Element of REAL
R9 is Element of the carrier of D
Ball (R9,((diameter s) / 4)) is bounded Element of bool the carrier of D
(diameter s) / 2 is V11() real ext-real Element of REAL
R9 is Element of bool the carrier of (TopSpaceMetr D)
Cl R9 is closed Element of bool the carrier of (TopSpaceMetr D)
R9 is Element of bool the carrier of D
S is Element of bool the carrier of (TopSpaceMetr D)
c₁₆ is Element of bool the carrier of D
SI is Element of bool the carrier of D
diameter SI is V11() real ext-real Element of REAL
diameter c₁₆ is V11() real ext-real Element of REAL
(diameter c₁₆) / 2 is V11() real ext-real Element of REAL
x is Element of bool the carrier of D
1 / 2 is V11() real ext-real non negative Element of REAL
f is Element of bool (bool the carrier of D)
union f is Element of bool the carrier of D
the carrier of (TopSpaceMetr D) is non empty set
bool the carrier of (TopSpaceMetr D) is non empty set
s is Element of bool the carrier of (TopSpaceMetr D)
S is Element of bool the carrier of D
S /\ s is Element of bool the carrier of (TopSpaceMetr D)
rngs 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)
diameter rngs is V11() real ext-real Element of REAL
diameter S is V11() real ext-real Element of REAL
2 * (1 / 2) is V11() real ext-real non negative Element of REAL
R is Element of the carrier of D
Ball (R,(1 / 2)) is bounded Element of bool the carrier of D
R is Element of the carrier of D
Ball (R,(1 / 2)) is bounded Element of bool the carrier of D
F is Element of bool the carrier of D
diameter F is V11() real ext-real Element of REAL
R is Element of bool the carrier of D
R is Relation-like Function-like set
dom R is set
rng R is set
R . 0 is 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
R9 is ordinal natural V11() real finite cardinal ext-real non negative set
R9 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):]
R9 . R9 is Element of bool the carrier of D
R9 is set
dom R9 is V141() V142() V143() V144() V145() V146() Element of bool NAT
c₁₆ is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
R9 . c₁₆ is Element of bool the carrier of D
R9 . R9 is set
R9 is ordinal natural V11() real finite cardinal ext-real non negative set
R9 . R9 is Element of bool the carrier of D
(b (#) W) . 0 is V11() real ext-real Element of REAL
W . 0 is V11() real ext-real Element of REAL
b * (W . 0) is V11() real ext-real Element of REAL
R9 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):]
c₁₆ is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
c₁₆ + 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
R9 . (c₁₆ + 1) is Element of bool the carrier of D
R9 . c₁₆ is Element of bool the carrier of D
(D,R9) is non empty Relation-like NAT -defined REAL -valued Function-like total V27( NAT , REAL ) Element of bool [:NAT,REAL:]
SI is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
(b (#) W) . SI is V11() real ext-real Element of REAL
(D,R9) . SI is V11() real ext-real Element of REAL
W . SI is V11() real ext-real Element of REAL
SI + 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 (#) W) . (SI + 1) is V11() real ext-real Element of REAL
(D,R9) . (SI + 1) is V11() real ext-real Element of REAL
W . (SI + 1) is V11() real ext-real Element of REAL
1 + SI 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 + SI) is V11() real ext-real non negative Element of REAL
((D,R9) . SI) / 2 is V11() real ext-real Element of REAL
H₁(SI) / 2 is V11() real ext-real non negative Element of REAL
R9 . SI is Element of bool the carrier of D
diameter (R9 . SI) is V11() real ext-real Element of REAL
R9 . (SI + 1) is Element of bool the carrier of D
diameter (R9 . (SI + 1)) is V11() real ext-real Element of REAL
(diameter (R9 . SI)) / 2 is V11() real ext-real Element of REAL
b * (W . (SI + 1)) is V11() real ext-real Element of REAL
(SI + 1) + 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
((SI + 1) + 1) + SI 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 * (SI + 1) is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
1 / (2 * (SI + 1)) is V11() real ext-real non negative Element of REAL
1 + (SI + 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 + (SI + 1)) is V11() real ext-real non negative Element of REAL
1 + 0 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 + 0) is V11() real ext-real non negative Element of REAL
SI is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
W . SI is V11() real ext-real Element of REAL
SI + 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 / (SI + 1) is V11() real ext-real non negative Element of REAL
(D,R9) . 0 is V11() real ext-real Element of REAL
lim W is V11() real ext-real Element of REAL
lim (b (#) W) is V11() real ext-real Element of REAL
b * 0 is V11() real ext-real Element of REAL
lim (D,R9) is V11() real ext-real Element of REAL
meet R9 is Element of bool the carrier of D
SI is set
x is Element of the carrier of (TopSpaceMetr D)
xS is open Element of bool the carrier of (TopSpaceMetr D)
y is Element of the carrier of D
j1 is V11() real ext-real set
Ball (y,j1) is bounded Element of bool the carrier of D
j1 / 2 is V11() real ext-real Element of REAL
yS is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
R9 . yS is Element of bool the carrier of D
{x} is non empty trivial finite 1 -element closed Element of bool the carrier of (TopSpaceMetr D)
(R9 . yS) \ {x} is Element of bool the carrier of D
j2 is set
q is Element of the carrier of (TopSpaceMetr D)
q9 is Element of the carrier of D
dist (y,q9) 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 . (y,q9) is V11() real ext-real Element of REAL
Ball (q9,(dist (y,q9))) is bounded Element of bool the carrier of D
dist (q9,q9) is V11() real ext-real Element of REAL
the distance of D . (q9,q9) is V11() real ext-real Element of REAL
B is Element of bool the carrier of (TopSpaceMetr D)
s is set
s is Element of the carrier of D
s9 is Element of the carrier of (TopSpaceMetr D)
(b (#) W) . yS is V11() real ext-real Element of REAL
W . yS is V11() real ext-real Element of REAL
b * (W . yS) is V11() real ext-real Element of REAL
(D,R9) . yS is V11() real ext-real Element of REAL
((D,R9) . yS) - 0 is V11() real ext-real Element of REAL
abs (((D,R9) . yS) - 0) is V11() real ext-real Element of REAL
diameter (R9 . yS) is V11() real ext-real Element of REAL
dist (q9,s) is V11() real ext-real Element of REAL
the distance of D . (q9,s) is V11() real ext-real Element of REAL
(j1 / 2) + (j1 / 2) is V11() real ext-real Element of REAL
(dist (y,q9)) + (dist (q9,s)) is V11() real ext-real Element of REAL
dist (y,s) is V11() real ext-real Element of REAL
the distance of D . (y,s) is V11() real ext-real Element of REAL
s9 is Element of the carrier of (TopSpaceMetr D)
s /\ xS is Element of bool the carrier of (TopSpaceMetr D)
Der s is Element of bool the carrier of (TopSpaceMetr D)
D is set
a is MetrStruct
the carrier of a is set
b is Element of the carrier of a
{b} is non empty trivial finite 1 -element set
the carrier of a \ {b} is Element of bool the carrier of a
bool the carrier of a is non empty set
[:D,( the carrier of a \ {b}):] is set
[D,b] is non empty set
{D,b} is non empty finite set
{D} is non empty trivial finite 1 -element set
{{D,b},{D}} is non empty finite V34() set
{[D,b]} is non empty trivial finite 1 -element set
[:D,( the carrier of a \ {b}):] \/ {[D,b]} is non empty set
X is set
W is set
TW is set
[W,TW] is non empty set
{W,TW} is non empty finite set
{W} is non empty trivial finite 1 -element set
{{W,TW},{W}} is non empty finite V34() set
f is Element of the carrier of a
[W,f] is non empty set
{W,f} is non empty finite set
{{W,f},{W}} is non empty finite V34() set
W is set
TW is Element of the carrier of a
[W,TW] is non empty set
{W,TW} is non empty finite set
{W} is non empty trivial finite 1 -element set
{{W,TW},{W}} is non empty finite V34() set
D is MetrStruct
the carrier of D is set
b is set
a is Element of the carrier of D
{a} is non empty trivial finite 1 -element set
the carrier of D \ {a} is Element of bool the carrier of D
bool the carrier of D is non empty set
[:b,( the carrier of D \ {a}):] is set
[b,a] is non empty set
{b,a} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is non empty finite V34() set
{[b,a]} is non empty trivial finite 1 -element set
[:b,( the carrier of D \ {a}):] \/ {[b,a]} is non empty set
[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] is non empty set
[:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
W is set
TW is set
f is set
s is Element of the carrier of D
[f,s] is non empty set
{f,s} is non empty finite set
{f} is non empty trivial finite 1 -element set
{{f,s},{f}} is non empty finite V34() set
S is set
rngs is Element of the carrier of D
[S,rngs] is non empty set
{S,rngs} is non empty finite set
{S} is non empty trivial finite 1 -element set
{{S,rngs},{S}} is non empty finite V34() set
dist (rngs,s) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (rngs,s) is V11() real ext-real Element of REAL
F is V11() real ext-real Element of REAL
F is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
R is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
R9 is set
c₁₆ is Element of the carrier of D
[R9,c₁₆] is non empty set
{R9,c₁₆} is non empty finite set
{R9} is non empty trivial finite 1 -element set
{{R9,c₁₆},{R9}} is non empty finite V34() set
R9 is set
SI is Element of the carrier of D
[R9,SI] is non empty set
{R9,SI} is non empty finite set
{R9} is non empty trivial finite 1 -element set
{{R9,SI},{R9}} is non empty finite V34() set
dist (c₁₆,SI) is V11() real ext-real Element of REAL
the distance of D . (c₁₆,SI) is V11() real ext-real Element of REAL
dist (c₁₆,a) is V11() real ext-real Element of REAL
the distance of D . (c₁₆,a) is V11() real ext-real Element of REAL
dist (a,SI) is V11() real ext-real Element of REAL
the distance of D . (a,SI) is V11() real ext-real Element of REAL
(dist (c₁₆,a)) + (dist (a,SI)) is V11() real ext-real Element of REAL
dist (rngs,a) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (rngs,a) is V11() real ext-real Element of REAL
dist (a,s) is V11() real ext-real Element of REAL
the distance of D . (a,s) is V11() real ext-real Element of REAL
(dist (rngs,a)) + (dist (a,s)) is V11() real ext-real Element of REAL
F is V11() real ext-real Element of REAL
F is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
R is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
R9 is set
c₁₆ is Element of the carrier of D
[R9,c₁₆] is non empty set
{R9,c₁₆} is non empty finite set
{R9} is non empty trivial finite 1 -element set
{{R9,c₁₆},{R9}} is non empty finite V34() set
R9 is set
SI is Element of the carrier of D
[R9,SI] is non empty set
{R9,SI} is non empty finite set
{R9} is non empty trivial finite 1 -element set
{{R9,SI},{R9}} is non empty finite V34() set
dist (c₁₆,SI) is V11() real ext-real Element of REAL
the distance of D . (c₁₆,SI) is V11() real ext-real Element of REAL
dist (c₁₆,a) is V11() real ext-real Element of REAL
the distance of D . (c₁₆,a) is V11() real ext-real Element of REAL
dist (a,SI) is V11() real ext-real Element of REAL
the distance of D . (a,SI) is V11() real ext-real Element of REAL
(dist (c₁₆,a)) + (dist (a,SI)) is V11() real ext-real Element of REAL
F is V11() real ext-real Element of REAL
W is non empty Relation-like [:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] -defined REAL -valued Function-like total V27([:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):], REAL ) Element of bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:]
TW is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
s is set
rngs is Element of the carrier of D
[s,rngs] is non empty set
{s,rngs} is non empty finite set
{s} is non empty trivial finite 1 -element set
{{s,rngs},{s}} is non empty finite V34() set
f is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
S is set
F is Element of the carrier of D
[S,F] is non empty set
{S,F} is non empty finite set
{S} is non empty trivial finite 1 -element set
{{S,F},{S}} is non empty finite V34() set
W . (TW,f) is V11() real ext-real Element of REAL
dist (rngs,F) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (rngs,F) is V11() real ext-real Element of REAL
dist (rngs,a) is V11() real ext-real Element of REAL
the distance of D . (rngs,a) is V11() real ext-real Element of REAL
dist (a,F) is V11() real ext-real Element of REAL
the distance of D . (a,F) is V11() real ext-real Element of REAL
(dist (rngs,a)) + (dist (a,F)) is V11() real ext-real Element of REAL
W is non empty Relation-like [:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] -defined REAL -valued Function-like total V27([:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):], REAL ) Element of bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:]
TW is non empty Relation-like [:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] -defined REAL -valued Function-like total V27([:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):], REAL ) Element of bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:]
f is set
s is set
S is set
rngs is Element of the carrier of D
[S,rngs] is non empty set
{S,rngs} is non empty finite set
{S} is non empty trivial finite 1 -element set
{{S,rngs},{S}} is non empty finite V34() set
F is set
F is Element of the carrier of D
[F,F] is non empty set
{F,F} is non empty finite set
{F} is non empty trivial finite 1 -element set
{{F,F},{F}} is non empty finite V34() set
W . (f,s) is set
R is Element of the carrier of D
R9 is Element of the carrier of D
dist (R,R9) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (R,R9) is V11() real ext-real Element of REAL
TW . (f,s) is set
dist (R,a) is V11() real ext-real Element of REAL
the distance of D . (R,a) is V11() real ext-real Element of REAL
dist (a,R9) is V11() real ext-real Element of REAL
the distance of D . (a,R9) is V11() real ext-real Element of REAL
(dist (R,a)) + (dist (a,R9)) is V11() real ext-real Element of REAL
D is MetrStruct
the carrier of D is set
a is Element of the carrier of D
{a} is non empty trivial finite 1 -element set
the carrier of D \ {a} is Element of bool the carrier of D
bool the carrier of D is non empty set
b is non empty set
[:b,( the carrier of D \ {a}):] is set
[b,a] is non empty set
{b,a} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is non empty finite V34() set
{[b,a]} is non empty trivial finite 1 -element set
[:b,( the carrier of D \ {a}):] \/ {[b,a]} is non empty set
(D,a,b) is non empty Relation-like [:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] -defined REAL -valued Function-like total V27([:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):], REAL ) Element of bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:]
[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] is non empty set
[:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
X is set
f is Element of the carrier of D
[b,f] is non empty set
{b,f} is non empty finite set
{{b,f},{b}} is non empty finite V34() set
dist (f,f) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,f) is V11() real ext-real Element of REAL
(D,a,b) . ([b,f],[b,f]) is set
f is Element of the carrier of D
[X,f] is non empty set
{X,f} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,f},{X}} is non empty finite V34() set
dist (f,f) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,f) is V11() real ext-real Element of REAL
(D,a,b) . ([X,f],[X,f]) is set
f is Element of the carrier of D
dist (f,f) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,f) is V11() real ext-real Element of REAL
f is Element of the carrier of D
dist (f,f) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,f) 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 is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,s) is V11() real ext-real Element of REAL
dist (s,f) is V11() real ext-real Element of REAL
the distance of D . (s,f) is V11() real ext-real Element of REAL
f is Element of the carrier of D
s is Element of the carrier of D
[X,s] is non empty set
{X,s} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,s},{X}} is non empty finite V34() set
dist (a,a) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (a,a) is V11() real ext-real Element of REAL
dist (a,s) is V11() real ext-real Element of REAL
the distance of D . (a,s) is V11() real ext-real Element of REAL
(dist (a,a)) + (dist (a,s)) is V11() real ext-real Element of REAL
(D,a,b) . ([b,a],[X,s]) is set
(D,a,b) . ([X,s],[b,a]) is set
dist (s,a) is V11() real ext-real Element of REAL
the distance of D . (s,a) is V11() real ext-real Element of REAL
(dist (s,a)) + (dist (a,a)) is V11() real ext-real Element of REAL
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
dist (s,f) is V11() real ext-real Element of REAL
the distance of D . (s,f) is V11() real ext-real Element of REAL
f is Element of the carrier of D
s is Element of the carrier of D
[X,f] is non empty set
{X,f} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,f},{X}} is non empty finite V34() set
dist (a,a) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (a,a) is V11() real ext-real Element of REAL
dist (a,f) is V11() real ext-real Element of REAL
the distance of D . (a,f) is V11() real ext-real Element of REAL
(dist (a,a)) + (dist (a,f)) is V11() real ext-real Element of REAL
(D,a,b) . ([b,a],[X,f]) is set
(D,a,b) . ([X,f],[b,a]) is set
dist (f,a) is V11() real ext-real Element of REAL
the distance of D . (f,a) is V11() real ext-real Element of REAL
(dist (f,a)) + (dist (a,a)) is V11() real ext-real Element of REAL
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
dist (s,f) is V11() real ext-real Element of REAL
the distance of D . (s,f) is V11() real ext-real Element of REAL
f is Element of the carrier of D
s is Element of the carrier of D
[X,s] is non empty set
{X,s} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,s},{X}} is non empty finite V34() set
[X,f] is non empty set
{X,f} is non empty finite set
{{X,f},{X}} is non empty finite V34() set
dist (f,s) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,s) is V11() real ext-real Element of REAL
(D,a,b) . ([X,f],[X,s]) is set
(D,a,b) . ([X,s],[X,f]) is set
dist (s,f) is V11() real ext-real Element of REAL
the distance of D . (s,f) 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 is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,s) is V11() real ext-real Element of REAL
dist (s,f) is V11() real ext-real Element of REAL
the distance of D . (s,f) 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 is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,s) is V11() real ext-real Element of REAL
dist (s,f) is V11() real ext-real Element of REAL
the distance of D . (s,f) is V11() real ext-real Element of REAL
f is Element of the carrier of D
s is Element of the carrier of D
S is Element of the carrier of D
[b,f] is non empty set
{b,f} is non empty finite set
{{b,f},{b}} is non empty finite V34() set
[b,s] is non empty set
{b,s} is non empty finite set
{{b,s},{b}} is non empty finite V34() set
[b,S] is non empty set
{b,S} is non empty finite set
{{b,S},{b}} is non empty finite V34() set
dist (f,S) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,S) is V11() real ext-real Element of REAL
rngs is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
F is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (rngs,F) is V11() real ext-real Element of REAL
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 Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (rngs,F) is V11() real ext-real Element of REAL
(D,a,b) . (F,F) is V11() real ext-real Element of REAL
((D,a,b) . (rngs,F)) + ((D,a,b) . (F,F)) is V11() real ext-real Element of REAL
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
(dist (f,s)) + (dist (s,S)) is V11() real ext-real Element of REAL
f is Element of the carrier of D
s is Element of the carrier of D
S is Element of the carrier of D
dist (f,f) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,f) is V11() real ext-real Element of REAL
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
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
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
(dist (f,s)) + (dist (s,S)) is V11() real ext-real Element of REAL
f is Element of the carrier of D
s is Element of the carrier of D
S is Element of the carrier of D
[b,f] is non empty set
{b,f} is non empty finite set
{{b,f},{b}} is non empty finite V34() set
[X,s] is non empty set
{X,s} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,s},{X}} is non empty finite V34() set
[b,S] is non empty set
{b,S} is non empty finite set
{{b,S},{b}} is non empty finite V34() set
dist (s,S) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (s,S) is V11() real ext-real Element of REAL
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
(dist (s,S)) + (dist (f,f)) is V11() real ext-real Element of REAL
F is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
F is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (F,F) is V11() real ext-real Element of REAL
rngs is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (rngs,F) is V11() real ext-real Element of REAL
(D,a,b) . (rngs,F) is V11() real ext-real Element of REAL
((D,a,b) . (rngs,F)) + ((D,a,b) . (F,F)) is V11() real ext-real Element of REAL
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
(dist (f,f)) + (dist (f,s)) is V11() real ext-real Element of REAL
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
(dist (f,s)) + (dist (s,S)) is V11() real ext-real Element of REAL
f is Element of the carrier of D
s is Element of the carrier of D
S is Element of the carrier of D
[b,f] is non empty set
{b,f} is non empty finite set
{{b,f},{b}} is non empty finite V34() set
[X,s] is non empty set
{X,s} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,s},{X}} is non empty finite V34() set
[X,S] is non empty set
{X,S} is non empty finite set
{{X,S},{X}} is non empty finite V34() set
dist (f,f) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,f) is V11() real ext-real Element of REAL
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
(dist (f,f)) + (dist (f,s)) is V11() real ext-real Element of REAL
rngs is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
F is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (rngs,F) is V11() real ext-real Element of REAL
F is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (rngs,F) is V11() real ext-real Element of REAL
(D,a,b) . (F,F) is V11() real ext-real Element of REAL
((D,a,b) . (rngs,F)) + ((D,a,b) . (F,F)) is V11() real ext-real Element of REAL
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
(dist (f,f)) + (dist (f,S)) is V11() real ext-real Element of REAL
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
(dist (f,s)) + (dist (s,S)) is V11() real ext-real Element of REAL
f is Element of the carrier of D
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 is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (S,S) is V11() real ext-real Element of REAL
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
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
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
(dist (f,s)) + (dist (s,S)) is V11() real ext-real Element of REAL
f is Element of the carrier of D
s is Element of the carrier of D
S is Element of the carrier of D
[X,f] is non empty set
{X,f} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,f},{X}} is non empty finite V34() set
[b,s] is non empty set
{b,s} is non empty finite set
{{b,s},{b}} is non empty finite V34() set
[X,S] is non empty set
{X,S} is non empty finite set
{{X,S},{X}} is non empty finite V34() set
dist (s,s) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (s,s) is V11() real ext-real Element of REAL
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
(dist (s,s)) + (dist (s,S)) is V11() real ext-real Element of REAL
F is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
F is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (F,F) is V11() real ext-real Element of REAL
rngs is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (rngs,F) is V11() real ext-real Element of REAL
(D,a,b) . (rngs,F) is V11() real ext-real Element of REAL
((D,a,b) . (rngs,F)) + ((D,a,b) . (F,F)) is V11() real ext-real Element of REAL
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
(dist (f,s)) + (dist (s,s)) is V11() real ext-real Element of REAL
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
(dist (f,s)) + (dist (s,S)) is V11() real ext-real Element of REAL
f is Element of the carrier of D
s is Element of the carrier of D
S is Element of the carrier of D
[X,f] is non empty set
{X,f} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,f},{X}} is non empty finite V34() set
[X,s] is non empty set
{X,s} is non empty finite set
{{X,s},{X}} is non empty finite V34() set
[b,S] is non empty set
{b,S} is non empty finite set
{{b,S},{b}} is non empty finite V34() set
dist (s,S) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (s,S) is V11() real ext-real Element of REAL
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
(dist (s,S)) + (dist (S,S)) is V11() real ext-real Element of REAL
F is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
F is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (F,F) is V11() real ext-real Element of REAL
rngs is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (rngs,F) is V11() real ext-real Element of REAL
(D,a,b) . (rngs,F) is V11() real ext-real Element of REAL
((D,a,b) . (rngs,F)) + ((D,a,b) . (F,F)) is V11() real ext-real Element of REAL
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
(dist (f,S)) + (dist (S,S)) is V11() real ext-real Element of REAL
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
(dist (f,s)) + (dist (s,S)) is V11() real ext-real Element of REAL
f is Element of the carrier of D
s is Element of the carrier of D
S is Element of the carrier of D
[X,f] is non empty set
{X,f} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,f},{X}} is non empty finite V34() set
[X,s] is non empty set
{X,s} is non empty finite set
{{X,s},{X}} is non empty finite V34() set
[X,S] is non empty set
{X,S} is non empty finite set
{{X,S},{X}} is non empty finite V34() set
dist (f,S) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,S) is V11() real ext-real Element of REAL
rngs is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
F is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (rngs,F) is V11() real ext-real Element of REAL
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 Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (rngs,F) is V11() real ext-real Element of REAL
(D,a,b) . (F,F) is V11() real ext-real Element of REAL
((D,a,b) . (rngs,F)) + ((D,a,b) . (F,F)) is V11() real ext-real Element of REAL
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
(dist (f,s)) + (dist (s,S)) is V11() real ext-real Element of REAL
f is Element of the carrier of D
s 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 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,S) is V11() real ext-real Element of REAL
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
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
(dist (f,s)) + (dist (s,S)) 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 is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,S) is V11() real ext-real Element of REAL
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
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
(dist (f,s)) + (dist (s,S)) 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 is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (f,s) is V11() real ext-real Element of REAL
[b,f] is non empty set
{b,f} is non empty finite set
{{b,f},{b}} is non empty finite V34() set
[X,s] is non empty set
{X,s} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,s},{X}} is non empty finite V34() 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
(dist (f,f)) + (dist (f,s)) is V11() real ext-real Element of REAL
S is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
rngs is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (S,rngs) is V11() real ext-real Element of REAL
[X,f] is non empty set
{X,f} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,f},{X}} is non empty finite V34() set
[b,s] is non empty set
{b,s} is non empty finite set
{{b,s},{b}} is non empty finite V34() set
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
(dist (f,s)) + (dist (s,s)) is V11() real ext-real Element of REAL
S is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
rngs is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (S,rngs) is V11() real ext-real Element of REAL
[X,f] is non empty set
{X,f} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,f},{X}} is non empty finite V34() set
[X,s] is non empty set
{X,s} is non empty finite set
{{X,s},{X}} is non empty finite V34() set
S is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
rngs is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
(D,a,b) . (S,rngs) is V11() real ext-real Element of REAL
D is MetrStruct
the carrier of D is set
b is set
a is Element of the carrier of D
{a} is non empty trivial finite 1 -element set
the carrier of D \ {a} is Element of bool the carrier of D
bool the carrier of D is non empty set
[:b,( the carrier of D \ {a}):] is set
[b,a] is non empty set
{b,a} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is non empty finite V34() set
{[b,a]} is non empty trivial finite 1 -element set
[:b,( the carrier of D \ {a}):] \/ {[b,a]} is non empty set
(D,a,b) is non empty Relation-like [:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] -defined REAL -valued Function-like total V27([:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):], REAL ) Element of bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:]
[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] is non empty set
[:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
MetrStruct(# ([:b,( the carrier of D \ {a}):] \/ {[b,a]}),(D,a,b) #) is strict MetrStruct
D is MetrStruct
the carrier of D is set
a is Element of the carrier of D
b is set
(D,a,b) is strict MetrStruct
{a} is non empty trivial finite 1 -element set
the carrier of D \ {a} is Element of bool the carrier of D
bool the carrier of D is non empty set
[:b,( the carrier of D \ {a}):] is set
[b,a] is non empty set
{b,a} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is non empty finite V34() set
{[b,a]} is non empty trivial finite 1 -element set
[:b,( the carrier of D \ {a}):] \/ {[b,a]} is non empty set
(D,a,b) is non empty Relation-like [:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] -defined REAL -valued Function-like total V27([:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):], REAL ) Element of bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:]
[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] is non empty set
[:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
MetrStruct(# ([:b,( the carrier of D \ {a}):] \/ {[b,a]}),(D,a,b) #) is strict MetrStruct
D is MetrStruct
the carrier of D is set
a is Element of the carrier of D
b is set
(D,a,b) is non empty strict MetrStruct
{a} is non empty trivial finite 1 -element set
the carrier of D \ {a} is Element of bool the carrier of D
bool the carrier of D is non empty set
[:b,( the carrier of D \ {a}):] is set
[b,a] is non empty set
{b,a} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is non empty finite V34() set
{[b,a]} is non empty trivial finite 1 -element set
[:b,( the carrier of D \ {a}):] \/ {[b,a]} is non empty set
(D,a,b) is non empty Relation-like [:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] -defined REAL -valued Function-like total V27([:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):], REAL ) Element of bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:]
[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] is non empty set
[:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
MetrStruct(# ([:b,( the carrier of D \ {a}):] \/ {[b,a]}),(D,a,b) #) is strict MetrStruct
f is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
s is set
S is Element of the carrier of D
[s,S] is non empty set
{s,S} is non empty finite set
{s} is non empty trivial finite 1 -element set
{{s,S},{s}} is non empty finite V34() set
(D,a,b) . (f,f) is V11() real ext-real Element of REAL
dist (S,S) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (S,S) is V11() real ext-real Element of REAL
f is symmetric MetrStruct
the carrier of f is set
S is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
s is Element of the carrier of f
F is set
F is Element of the carrier of f
[F,F] is non empty set
{F,F} is non empty finite set
{F} is non empty trivial finite 1 -element set
{{F,F},{F}} is non empty finite V34() set
rngs is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
R is set
R9 is Element of the carrier of f
[R,R9] is non empty set
{R,R9} is non empty finite set
{R} is non empty trivial finite 1 -element set
{{R,R9},{R}} is non empty finite V34() set
(D,a,b) . (S,rngs) is V11() real ext-real Element of REAL
(D,a,b) . (rngs,S) is V11() real ext-real Element of REAL
(D,a,b) . (S,rngs) is V11() real ext-real Element of REAL
dist (F,s) is V11() real ext-real Element of REAL
the distance of f is Relation-like [: the carrier of f, the carrier of f:] -defined REAL -valued Function-like total V27([: the carrier of f, the carrier of f:], REAL ) Element of bool [:[: the carrier of f, the carrier of f:],REAL:]
[: the carrier of f, the carrier of f:] is set
[:[: the carrier of f, the carrier of f:],REAL:] is set
bool [:[: the carrier of f, the carrier of f:],REAL:] is non empty set
the distance of f . (F,s) is V11() real ext-real Element of REAL
dist (s,R9) is V11() real ext-real Element of REAL
the distance of f . (s,R9) is V11() real ext-real Element of REAL
(dist (F,s)) + (dist (s,R9)) is V11() real ext-real Element of REAL
dist (s,F) is V11() real ext-real Element of REAL
the distance of f . (s,F) is V11() real ext-real Element of REAL
(dist (s,F)) + (dist (s,R9)) is V11() real ext-real Element of REAL
dist (R9,s) is V11() real ext-real Element of REAL
the distance of f . (R9,s) is V11() real ext-real Element of REAL
(dist (s,F)) + (dist (R9,s)) is V11() real ext-real Element of REAL
(D,a,b) . (rngs,S) is V11() real ext-real Element of REAL
(D,a,b) . (S,rngs) is V11() real ext-real Element of REAL
dist (F,R9) is V11() real ext-real Element of REAL
the distance of f is Relation-like [: the carrier of f, the carrier of f:] -defined REAL -valued Function-like total V27([: the carrier of f, the carrier of f:], REAL ) Element of bool [:[: the carrier of f, the carrier of f:],REAL:]
[: the carrier of f, the carrier of f:] is set
[:[: the carrier of f, the carrier of f:],REAL:] is set
bool [:[: the carrier of f, the carrier of f:],REAL:] is non empty set
the distance of f . (F,R9) is V11() real ext-real Element of REAL
dist (R9,F) is V11() real ext-real Element of REAL
the distance of f . (R9,F) is V11() real ext-real Element of REAL
(D,a,b) . (rngs,S) is V11() real ext-real Element of REAL
(D,a,b) . (S,rngs) is V11() real ext-real Element of REAL
(D,a,b) . (rngs,S) is V11() real ext-real Element of REAL
(D,a,b) . (S,rngs) is V11() real ext-real Element of REAL
(D,a,b) . (rngs,S) is V11() real ext-real Element of REAL
f is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
rngs is set
F is Element of the carrier of D
[rngs,F] is non empty set
{rngs,F} is non empty finite set
{rngs} is non empty trivial finite 1 -element set
{{rngs,F},{rngs}} is non empty finite V34() set
s is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
F is set
R is Element of the carrier of D
[F,R] is non empty set
{F,R} is non empty finite set
{F} is non empty trivial finite 1 -element set
{{F,R},{F}} is non empty finite V34() set
S is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
R9 is set
R9 is Element of the carrier of D
[R9,R9] is non empty set
{R9,R9} is non empty finite set
{R9} is non empty trivial finite 1 -element set
{{R9,R9},{R9}} is non empty finite V34() set
dist (R,R9) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (R,R9) is V11() real ext-real Element of REAL
(D,a,b) . (s,S) is V11() real ext-real Element of REAL
dist (F,R) is V11() real ext-real Element of REAL
the distance of D . (F,R) is V11() real ext-real Element of REAL
(D,a,b) . (f,s) is V11() real ext-real Element of REAL
dist (F,R9) is V11() real ext-real Element of REAL
the distance of D . (F,R9) is V11() real ext-real Element of REAL
(D,a,b) . (f,S) is V11() real ext-real Element of REAL
((D,a,b) . (f,s)) + ((D,a,b) . (s,S)) is V11() real ext-real Element of REAL
dist (R,a) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (R,a) is V11() real ext-real Element of REAL
dist (a,R9) is V11() real ext-real Element of REAL
the distance of D . (a,R9) is V11() real ext-real Element of REAL
(dist (R,a)) + (dist (a,R9)) is V11() real ext-real Element of REAL
(D,a,b) . (s,S) is V11() real ext-real Element of REAL
dist (F,R) is V11() real ext-real Element of REAL
the distance of D . (F,R) is V11() real ext-real Element of REAL
dist (F,a) is V11() real ext-real Element of REAL
the distance of D . (F,a) is V11() real ext-real Element of REAL
dist (a,R) is V11() real ext-real Element of REAL
the distance of D . (a,R) is V11() real ext-real Element of REAL
(dist (F,a)) + (dist (a,R)) is V11() real ext-real Element of REAL
dist (R,R9) is V11() real ext-real Element of REAL
the distance of D . (R,R9) is V11() real ext-real Element of REAL
(D,a,b) . (f,s) is V11() real ext-real Element of REAL
(dist (F,R)) + (dist (R,R9)) is V11() real ext-real Element of REAL
((D,a,b) . (f,s)) + ((D,a,b) . (s,S)) is V11() real ext-real Element of REAL
dist (F,R9) is V11() real ext-real Element of REAL
the distance of D . (F,R9) is V11() real ext-real Element of REAL
(D,a,b) . (f,S) is V11() real ext-real Element of REAL
dist (F,a) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (F,a) is V11() real ext-real Element of REAL
dist (F,R) is V11() real ext-real Element of REAL
the distance of D . (F,R) is V11() real ext-real Element of REAL
dist (R,a) is V11() real ext-real Element of REAL
the distance of D . (R,a) is V11() real ext-real Element of REAL
(dist (F,R)) + (dist (R,a)) is V11() real ext-real Element of REAL
dist (a,R9) is V11() real ext-real Element of REAL
the distance of D . (a,R9) is V11() real ext-real Element of REAL
(dist (F,a)) + (dist (a,R9)) is V11() real ext-real Element of REAL
(D,a,b) . (f,S) is V11() real ext-real Element of REAL
((dist (F,R)) + (dist (R,a))) + (dist (a,R9)) is V11() real ext-real Element of REAL
(dist (R,a)) + (dist (a,R9)) is V11() real ext-real Element of REAL
(D,a,b) . (s,S) is V11() real ext-real Element of REAL
(D,a,b) . (f,s) is V11() real ext-real Element of REAL
((D,a,b) . (f,s)) + ((D,a,b) . (s,S)) is V11() real ext-real Element of REAL
dist (R,a) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (R,a) is V11() real ext-real Element of REAL
dist (a,R9) is V11() real ext-real Element of REAL
the distance of D . (a,R9) is V11() real ext-real Element of REAL
(dist (R,a)) + (dist (a,R9)) is V11() real ext-real Element of REAL
(D,a,b) . (s,S) is V11() real ext-real Element of REAL
0 + (dist (a,R9)) is V11() real ext-real Element of REAL
dist (a,R) is V11() real ext-real Element of REAL
the distance of D . (a,R) is V11() real ext-real Element of REAL
dist (F,a) is V11() real ext-real Element of REAL
the distance of D . (F,a) is V11() real ext-real Element of REAL
(dist (F,a)) + (dist (a,R)) is V11() real ext-real Element of REAL
(D,a,b) . (f,s) is V11() real ext-real Element of REAL
(dist (F,a)) + 0 is V11() real ext-real Element of REAL
(dist (F,a)) + (dist (a,R9)) is V11() real ext-real Element of REAL
(D,a,b) . (f,S) is V11() real ext-real Element of REAL
((D,a,b) . (f,s)) + ((D,a,b) . (s,S)) is V11() real ext-real Element of REAL
dist (a,R9) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (a,R9) is V11() real ext-real Element of REAL
dist (a,R) is V11() real ext-real Element of REAL
the distance of D . (a,R) is V11() real ext-real Element of REAL
dist (R,R9) is V11() real ext-real Element of REAL
the distance of D . (R,R9) is V11() real ext-real Element of REAL
(dist (a,R)) + (dist (R,R9)) is V11() real ext-real Element of REAL
dist (F,a) is V11() real ext-real Element of REAL
the distance of D . (F,a) is V11() real ext-real Element of REAL
(dist (F,a)) + (dist (a,R9)) is V11() real ext-real Element of REAL
(D,a,b) . (f,S) is V11() real ext-real Element of REAL
(dist (F,a)) + ((dist (a,R)) + (dist (R,R9))) is V11() real ext-real Element of REAL
(D,a,b) . (s,S) is V11() real ext-real Element of REAL
(dist (F,a)) + (dist (a,R)) is V11() real ext-real Element of REAL
(D,a,b) . (f,s) is V11() real ext-real Element of REAL
((D,a,b) . (f,s)) + ((D,a,b) . (s,S)) is V11() real ext-real Element of REAL
(D,a,b) . (f,S) is V11() real ext-real Element of REAL
(D,a,b) . (f,s) is V11() real ext-real Element of REAL
(D,a,b) . (s,S) is V11() real ext-real Element of REAL
((D,a,b) . (f,s)) + ((D,a,b) . (s,S)) is V11() real ext-real Element of REAL
(D,a,b) . (f,S) is V11() real ext-real Element of REAL
(D,a,b) . (f,s) is V11() real ext-real Element of REAL
(D,a,b) . (s,S) is V11() real ext-real Element of REAL
((D,a,b) . (f,s)) + ((D,a,b) . (s,S)) is V11() real ext-real Element of REAL
f is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
S is set
rngs is Element of the carrier of D
[S,rngs] is non empty set
{S,rngs} is non empty finite set
{S} is non empty trivial finite 1 -element set
{{S,rngs},{S}} is non empty finite V34() set
s is Element of [:b,( the carrier of D \ {a}):] \/ {[b,a]}
F is set
F is Element of the carrier of D
[F,F] is non empty set
{F,F} is non empty finite set
{F} is non empty trivial finite 1 -element set
{{F,F},{F}} is non empty finite V34() set
(D,a,b) . (f,s) is V11() real ext-real Element of REAL
dist (rngs,F) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (rngs,F) is V11() real ext-real Element of REAL
dist (rngs,a) is V11() real ext-real Element of REAL
the distance of D is 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 set
[:[: the carrier of D, the carrier of D:],REAL:] is set
bool [:[: the carrier of D, the carrier of D:],REAL:] is non empty set
the distance of D . (rngs,a) is V11() real ext-real Element of REAL
dist (a,F) is V11() real ext-real Element of REAL
the distance of D . (a,F) is V11() real ext-real Element of REAL
(dist (rngs,a)) + (dist (a,F)) is V11() real ext-real Element of REAL
D is Reflexive MetrStruct
the carrier of D is set
a is Element of the carrier of D
b is set
(D,a,b) is non empty strict MetrStruct
{a} is non empty trivial finite 1 -element set
the carrier of D \ {a} is Element of bool the carrier of D
bool the carrier of D is non empty set
[:b,( the carrier of D \ {a}):] is set
[b,a] is non empty set
{b,a} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is non empty finite V34() set
{[b,a]} is non empty trivial finite 1 -element set
[:b,( the carrier of D \ {a}):] \/ {[b,a]} is non empty set
(D,a,b) is non empty Relation-like [:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] -defined REAL -valued Function-like total V27([:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):], REAL ) Element of bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:]
[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] is non empty set
[:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
MetrStruct(# ([:b,( the carrier of D \ {a}):] \/ {[b,a]}),(D,a,b) #) is strict MetrStruct
D is symmetric MetrStruct
the carrier of D is set
a is Element of the carrier of D
b is set
(D,a,b) is non empty strict MetrStruct
{a} is non empty trivial finite 1 -element set
the carrier of D \ {a} is Element of bool the carrier of D
bool the carrier of D is non empty set
[:b,( the carrier of D \ {a}):] is set
[b,a] is non empty set
{b,a} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is non empty finite V34() set
{[b,a]} is non empty trivial finite 1 -element set
[:b,( the carrier of D \ {a}):] \/ {[b,a]} is non empty set
(D,a,b) is non empty Relation-like [:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] -defined REAL -valued Function-like total V27([:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):], REAL ) Element of bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:]
[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] is non empty set
[:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
MetrStruct(# ([:b,( the carrier of D \ {a}):] \/ {[b,a]}),(D,a,b) #) is strict MetrStruct
D is Reflexive symmetric triangle MetrStruct
the carrier of D is set
a is Element of the carrier of D
b is set
(D,a,b) is non empty strict Reflexive symmetric MetrStruct
{a} is non empty trivial finite 1 -element set
the carrier of D \ {a} is Element of bool the carrier of D
bool the carrier of D is non empty set
[:b,( the carrier of D \ {a}):] is set
[b,a] is non empty set
{b,a} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is non empty finite V34() set
{[b,a]} is non empty trivial finite 1 -element set
[:b,( the carrier of D \ {a}):] \/ {[b,a]} is non empty set
(D,a,b) is non empty Relation-like [:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] -defined REAL -valued Function-like total V27([:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):], REAL ) Element of bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:]
[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] is non empty set
[:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
MetrStruct(# ([:b,( the carrier of D \ {a}):] \/ {[b,a]}),(D,a,b) #) is strict MetrStruct
D is Reflexive discerning symmetric triangle MetrStruct
the carrier of D is set
a is Element of the carrier of D
b is set
(D,a,b) is non empty strict Reflexive symmetric triangle MetrStruct
{a} is non empty trivial finite 1 -element set
the carrier of D \ {a} is Element of bool the carrier of D
bool the carrier of D is non empty set
[:b,( the carrier of D \ {a}):] is set
[b,a] is non empty set
{b,a} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is non empty finite V34() set
{[b,a]} is non empty trivial finite 1 -element set
[:b,( the carrier of D \ {a}):] \/ {[b,a]} is non empty set
(D,a,b) is non empty Relation-like [:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] -defined REAL -valued Function-like total V27([:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):], REAL ) Element of bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:]
[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] is non empty set
[:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
MetrStruct(# ([:b,( the carrier of D \ {a}):] \/ {[b,a]}),(D,a,b) #) is strict MetrStruct
D is non empty Reflexive triangle MetrStruct
the carrier of D is non empty set
a is Element of the carrier of D
b is non empty set
(D,a,b) is non empty strict Reflexive MetrStruct
{a} is non empty trivial finite 1 -element set
the carrier of D \ {a} is Element of bool the carrier of D
bool the carrier of D is non empty set
[:b,( the carrier of D \ {a}):] is set
[b,a] is non empty set
{b,a} is non empty finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is non empty finite V34() set
{[b,a]} is non empty trivial finite 1 -element set
[:b,( the carrier of D \ {a}):] \/ {[b,a]} is non empty set
(D,a,b) is non empty Relation-like [:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] -defined REAL -valued Function-like total V27([:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):], REAL ) Element of bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:]
[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):] is non empty set
[:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
bool [:[:([:b,( the carrier of D \ {a}):] \/ {[b,a]}),([:b,( the carrier of D \ {a}):] \/ {[b,a]}):],REAL:] is non empty non trivial non finite set
MetrStruct(# ([:b,( the carrier of D \ {a}):] \/ {[b,a]}),(D,a,b) #) is strict MetrStruct
X 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
TW 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 (D,a,b) is non empty set
f is set
TW . f is set
[X,(TW . f)] is non empty set
{X,(TW . f)} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,(TW . f)},{X}} is non empty finite V34() set
[b,(TW . f)] is non empty set
{b,(TW . f)} is non empty finite set
{{b,(TW . f)},{b}} is non empty finite V34() set
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 Element of the carrier of D
[X,(TW . s)] is non empty set
{X,(TW . s)} is non empty finite set
{{X,(TW . s)},{X}} is non empty finite V34() set
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 Element of the carrier of D
[:NAT, the carrier of (D,a,b):] is non empty non trivial non finite set
bool [:NAT, the carrier of (D,a,b):] is non empty non trivial non finite set
f is non empty Relation-like NAT -defined the carrier of (D,a,b) -valued Function-like total V27( NAT , the carrier of (D,a,b)) Element of bool [:NAT, the carrier of (D,a,b):]
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
F 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 the carrier of (D,a,b)
f . F is Element of the carrier of (D,a,b)
dist ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
the distance of (D,a,b) is non empty Relation-like [: the carrier of (D,a,b), the carrier of (D,a,b):] -defined REAL -valued Function-like total V27([: the carrier of (D,a,b), the carrier of (D,a,b):], REAL ) Element of bool [:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:]
[: the carrier of (D,a,b), the carrier of (D,a,b):] is non empty set
[:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:] is non empty non trivial non finite set
the distance of (D,a,b) . ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
TW . rngs is Element of the carrier of D
TW . F is Element of the carrier of D
[b,(TW . F)] is non empty set
{b,(TW . F)} is non empty finite set
{{b,(TW . F)},{b}} is non empty finite V34() set
f . F is Element of the carrier of (D,a,b)
[b,(TW . rngs)] is non empty set
{b,(TW . rngs)} is non empty finite set
{{b,(TW . rngs)},{b}} is non empty finite V34() set
f . rngs is Element of the carrier of (D,a,b)
dist ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
the distance of (D,a,b) . ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
dist ((TW . rngs),(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 . rngs),(TW . F)) is V11() real ext-real Element of REAL
TW . rngs is Element of the carrier of D
TW . F is Element of the carrier of D
[b,(TW . F)] is non empty set
{b,(TW . F)} is non empty finite set
{{b,(TW . F)},{b}} is non empty finite V34() set
f . F is Element of the carrier of (D,a,b)
dist ((TW . F),(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),(TW . F)) is V11() real ext-real Element of REAL
[X,(TW . rngs)] is non empty set
{X,(TW . rngs)} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,(TW . rngs)},{X}} is non empty finite V34() set
f . rngs is Element of the carrier of (D,a,b)
dist ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
the distance of (D,a,b) . ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
dist ((TW . rngs),(TW . F)) is V11() real ext-real Element of REAL
the distance of D . ((TW . rngs),(TW . F)) is V11() real ext-real Element of REAL
(dist ((TW . rngs),(TW . F))) + (dist ((TW . F),(TW . F))) is V11() real ext-real Element of REAL
TW . rngs is Element of the carrier of D
TW . F is Element of the carrier of D
[X,(TW . F)] is non empty set
{X,(TW . F)} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,(TW . F)},{X}} is non empty finite V34() set
f . F is Element of the carrier of (D,a,b)
dist ((TW . rngs),(TW . rngs)) 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 . rngs),(TW . rngs)) is V11() real ext-real Element of REAL
[b,(TW . rngs)] is non empty set
{b,(TW . rngs)} is non empty finite set
{{b,(TW . rngs)},{b}} is non empty finite V34() set
f . rngs is Element of the carrier of (D,a,b)
dist ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
the distance of (D,a,b) . ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
dist ((TW . rngs),(TW . F)) is V11() real ext-real Element of REAL
the distance of D . ((TW . rngs),(TW . F)) is V11() real ext-real Element of REAL
(dist ((TW . rngs),(TW . rngs))) + (dist ((TW . rngs),(TW . F))) is V11() real ext-real Element of REAL
TW . rngs is Element of the carrier of D
TW . F is Element of the carrier of D
[X,(TW . F)] is non empty set
{X,(TW . F)} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,(TW . F)},{X}} is non empty finite V34() set
f . F is Element of the carrier of (D,a,b)
[X,(TW . rngs)] is non empty set
{X,(TW . rngs)} is non empty finite set
{{X,(TW . rngs)},{X}} is non empty finite V34() set
f . rngs is Element of the carrier of (D,a,b)
dist ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
the distance of (D,a,b) . ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
dist ((TW . rngs),(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 . rngs),(TW . F)) is V11() real ext-real Element of REAL
TW . rngs is Element of the carrier of D
TW . F is Element of the carrier of D
s is Element of the carrier of (D,a,b)
S is set
rngs is Element of the carrier of D
[S,rngs] is non empty set
{S,rngs} is non empty finite set
{S} is non empty trivial finite 1 -element set
{{S,rngs},{S}} is non empty finite V34() set
F 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
R is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
TW . R is Element of the carrier of D
dist ((TW . R),rngs) 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 . R),rngs) is V11() real ext-real Element of REAL
TW . R is Element of the carrier of D
f . R is Element of the carrier of (D,a,b)
dist ((f . R),s) is V11() real ext-real Element of REAL
the distance of (D,a,b) is non empty Relation-like [: the carrier of (D,a,b), the carrier of (D,a,b):] -defined REAL -valued Function-like total V27([: the carrier of (D,a,b), the carrier of (D,a,b):], REAL ) Element of bool [:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:]
[: the carrier of (D,a,b), the carrier of (D,a,b):] is non empty set
[:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:] is non empty non trivial non finite set
the distance of (D,a,b) . ((f . R),s) is V11() real ext-real Element of REAL
dist ((TW . R),rngs) is V11() real ext-real Element of REAL
the distance of D . ((TW . R),rngs) is V11() real ext-real Element of REAL
TW . R is Element of the carrier of D
f . R is Element of the carrier of (D,a,b)
dist ((f . R),s) is V11() real ext-real Element of REAL
the distance of (D,a,b) is non empty Relation-like [: the carrier of (D,a,b), the carrier of (D,a,b):] -defined REAL -valued Function-like total V27([: the carrier of (D,a,b), the carrier of (D,a,b):], REAL ) Element of bool [:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:]
[: the carrier of (D,a,b), the carrier of (D,a,b):] is non empty set
[:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:] is non empty non trivial non finite set
the distance of (D,a,b) . ((f . R),s) is V11() real ext-real Element of REAL
dist ((TW . R),(TW . R)) is V11() real ext-real Element of REAL
the distance of D . ((TW . R),(TW . R)) is V11() real ext-real Element of REAL
dist ((TW . R),rngs) is V11() real ext-real Element of REAL
the distance of D . ((TW . R),rngs) is V11() real ext-real Element of REAL
(dist ((TW . R),(TW . R))) + (dist ((TW . R),rngs)) is V11() real ext-real Element of REAL
TW . R is Element of the carrier of D
f . R is Element of the carrier of (D,a,b)
[X,(TW . R)] is non empty set
{X,(TW . R)} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,(TW . R)},{X}} is non empty finite V34() set
dist ((f . R),s) is V11() real ext-real Element of REAL
the distance of (D,a,b) is non empty Relation-like [: the carrier of (D,a,b), the carrier of (D,a,b):] -defined REAL -valued Function-like total V27([: the carrier of (D,a,b), the carrier of (D,a,b):], REAL ) Element of bool [:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:]
[: the carrier of (D,a,b), the carrier of (D,a,b):] is non empty set
[:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:] is non empty non trivial non finite set
the distance of (D,a,b) . ((f . R),s) is V11() real ext-real Element of REAL
dist ((TW . R),rngs) is V11() real ext-real Element of REAL
the distance of D . ((TW . R),rngs) is V11() real ext-real Element of REAL
TW . R is Element of the carrier of D
f . R is Element of the carrier of (D,a,b)
[X,(TW . R)] is non empty set
{X,(TW . R)} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,(TW . R)},{X}} is non empty finite V34() set
dist ((f . R),s) is V11() real ext-real Element of REAL
the distance of (D,a,b) is non empty Relation-like [: the carrier of (D,a,b), the carrier of (D,a,b):] -defined REAL -valued Function-like total V27([: the carrier of (D,a,b), the carrier of (D,a,b):], REAL ) Element of bool [:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:]
[: the carrier of (D,a,b), the carrier of (D,a,b):] is non empty set
[:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (D,a,b), the carrier of (D,a,b):],REAL:] is non empty non trivial non finite set
the distance of (D,a,b) . ((f . R),s) is V11() real ext-real Element of REAL
dist ((TW . R),a) is V11() real ext-real Element of REAL
the distance of D . ((TW . R),a) is V11() real ext-real Element of REAL
dist (a,rngs) is V11() real ext-real Element of REAL
the distance of D . (a,rngs) is V11() real ext-real Element of REAL
(dist ((TW . R),a)) + (dist (a,rngs)) is V11() real ext-real Element of REAL
dist ((TW . R),rngs) is V11() real ext-real Element of REAL
the distance of D . ((TW . R),rngs) is V11() real ext-real Element of REAL
TW . R is Element of the carrier of D
D is set
a is non empty Reflexive symmetric triangle MetrStruct
the carrier of a is non empty set
b is Element of the carrier of a
(a,b,D) is non empty strict Reflexive symmetric triangle MetrStruct
{b} is non empty trivial finite 1 -element set
the carrier of a \ {b} is Element of bool the carrier of a
bool the carrier of a is non empty set
[:D,( the carrier of a \ {b}):] is set
[D,b] is non empty set
{D,b} is non empty finite set
{D} is non empty trivial finite 1 -element set
{{D,b},{D}} is non empty finite V34() set
{[D,b]} is non empty trivial finite 1 -element set
[:D,( the carrier of a \ {b}):] \/ {[D,b]} is non empty set
(a,b,D) is non empty Relation-like [:([:D,( the carrier of a \ {b}):] \/ {[D,b]}),([:D,( the carrier of a \ {b}):] \/ {[D,b]}):] -defined REAL -valued Function-like total V27([:([:D,( the carrier of a \ {b}):] \/ {[D,b]}),([:D,( the carrier of a \ {b}):] \/ {[D,b]}):], REAL ) Element of bool [:[:([:D,( the carrier of a \ {b}):] \/ {[D,b]}),([:D,( the carrier of a \ {b}):] \/ {[D,b]}):],REAL:]
[:([:D,( the carrier of a \ {b}):] \/ {[D,b]}),([:D,( the carrier of a \ {b}):] \/ {[D,b]}):] is non empty set
[:[:([:D,( the carrier of a \ {b}):] \/ {[D,b]}),([:D,( the carrier of a \ {b}):] \/ {[D,b]}):],REAL:] is non empty non trivial non finite set
bool [:[:([:D,( the carrier of a \ {b}):] \/ {[D,b]}),([:D,( the carrier of a \ {b}):] \/ {[D,b]}):],REAL:] is non empty non trivial non finite set
MetrStruct(# ([:D,( the carrier of a \ {b}):] \/ {[D,b]}),(a,b,D) #) is strict MetrStruct
the carrier of (a,b,D) is non empty set
[:NAT, the carrier of (a,b,D):] is non empty non trivial non finite set
bool [:NAT, the carrier of (a,b,D):] is non empty non trivial non finite set
TW is non empty Relation-like NAT -defined the carrier of (a,b,D) -valued Function-like total V27( NAT , the carrier of (a,b,D)) Element of bool [:NAT, the carrier of (a,b,D):]
W is Element of the carrier of (a,b,D)
f is Element of the carrier of (a,b,D)
s is V11() real ext-real Element of REAL
W is Element of the carrier of (a,b,D)
f is V11() real ext-real Element of REAL
f 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
S is ordinal natural V11() real finite cardinal ext-real non negative set
TW . S is Element of the carrier of (a,b,D)
dist ((TW . S),W) is V11() real ext-real Element of REAL
the distance of (a,b,D) is non empty Relation-like [: the carrier of (a,b,D), the carrier of (a,b,D):] -defined REAL -valued Function-like total V27([: the carrier of (a,b,D), the carrier of (a,b,D):], REAL ) Element of bool [:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:]
[: the carrier of (a,b,D), the carrier of (a,b,D):] is non empty set
[:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:] is non empty non trivial non finite set
the distance of (a,b,D) . ((TW . S),W) is V11() real ext-real Element of REAL
rngs is set
F is Element of the carrier of a
[rngs,F] is non empty set
{rngs,F} is non empty finite set
{rngs} is non empty trivial finite 1 -element set
{{rngs,F},{rngs}} is non empty finite V34() set
F is ordinal natural V11() real finite cardinal ext-real non negative set
TW . F is Element of the carrier of (a,b,D)
R is set
R9 is Element of the carrier of a
[R,R9] is non empty set
{R,R9} is non empty finite set
{R} is non empty trivial finite 1 -element set
{{R,R9},{R}} is non empty finite V34() set
dist (b,R9) 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,R9) is V11() real ext-real Element of REAL
dist (b,b) is V11() real ext-real Element of REAL
the distance of a . (b,b) is V11() real ext-real Element of REAL
dist (F,b) is V11() real ext-real Element of REAL
the distance of a . (F,b) is V11() real ext-real Element of REAL
(dist (F,b)) + 0 is V11() real ext-real Element of REAL
f + 0 is V11() real ext-real Element of REAL
(dist (F,b)) + (dist (b,R9)) is V11() real ext-real Element of REAL
dist ((TW . S),(TW . F)) is V11() real ext-real Element of REAL
the distance of (a,b,D) . ((TW . S),(TW . F)) is V11() real ext-real Element of REAL
F is Element of the carrier of (a,b,D)
R is V11() real ext-real Element of REAL
R9 is ordinal natural V11() real finite cardinal ext-real non negative set
R9 is set
W is Element of the carrier of (a,b,D)
f is V11() real ext-real Element of REAL
D is set
a is non empty Reflexive symmetric triangle MetrStruct
the carrier of a is non empty set
b is Element of the carrier of a
(a,b,D) is non empty strict Reflexive symmetric triangle MetrStruct
{b} is non empty trivial finite 1 -element set
the carrier of a \ {b} is Element of bool the carrier of a
bool the carrier of a is non empty set
[:D,( the carrier of a \ {b}):] is set
[D,b] is non empty set
{D,b} is non empty finite set
{D} is non empty trivial finite 1 -element set
{{D,b},{D}} is non empty finite V34() set
{[D,b]} is non empty trivial finite 1 -element set
[:D,( the carrier of a \ {b}):] \/ {[D,b]} is non empty set
(a,b,D) is non empty Relation-like [:([:D,( the carrier of a \ {b}):] \/ {[D,b]}),([:D,( the carrier of a \ {b}):] \/ {[D,b]}):] -defined REAL -valued Function-like total V27([:([:D,( the carrier of a \ {b}):] \/ {[D,b]}),([:D,( the carrier of a \ {b}):] \/ {[D,b]}):], REAL ) Element of bool [:[:([:D,( the carrier of a \ {b}):] \/ {[D,b]}),([:D,( the carrier of a \ {b}):] \/ {[D,b]}):],REAL:]
[:([:D,( the carrier of a \ {b}):] \/ {[D,b]}),([:D,( the carrier of a \ {b}):] \/ {[D,b]}):] is non empty set
[:[:([:D,( the carrier of a \ {b}):] \/ {[D,b]}),([:D,( the carrier of a \ {b}):] \/ {[D,b]}):],REAL:] is non empty non trivial non finite set
bool [:[:([:D,( the carrier of a \ {b}):] \/ {[D,b]}),([:D,( the carrier of a \ {b}):] \/ {[D,b]}):],REAL:] is non empty non trivial non finite set
MetrStruct(# ([:D,( the carrier of a \ {b}):] \/ {[D,b]}),(a,b,D) #) is strict MetrStruct
the carrier of (a,b,D) is non empty set
[:NAT, the carrier of (a,b,D):] is non empty non trivial non finite set
bool [:NAT, the carrier of (a,b,D):] is non empty non trivial non finite set
TW is non empty Relation-like NAT -defined the carrier of (a,b,D) -valued Function-like total V27( NAT , the carrier of (a,b,D)) Element of bool [:NAT, the carrier of (a,b,D):]
f is set
TW . 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
TW . s is Element of the carrier of (a,b,D)
S is set
rngs is Element of the carrier of a
[S,rngs] is non empty set
{S,rngs} is non empty finite set
{S} is non empty trivial finite 1 -element set
{{S,rngs},{S}} is non empty finite V34() set
[:NAT, the carrier of a:] is non empty non trivial non finite set
bool [:NAT, the carrier of a:] is non empty non trivial non finite set
f is non empty Relation-like NAT -defined the carrier of a -valued Function-like total V27( NAT , the carrier of a) Element of bool [:NAT, the carrier of a:]
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
F 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 the carrier of a
f . F is Element of the carrier of a
dist ((f . rngs),(f . F)) 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 . ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
TW . rngs is Element of the carrier of (a,b,D)
f . rngs is Element of the carrier of a
F is set
[F,(f . rngs)] is non empty set
{F,(f . rngs)} is non empty finite set
{F} is non empty trivial finite 1 -element set
{{F,(f . rngs)},{F}} is non empty finite V34() set
TW . F is Element of the carrier of (a,b,D)
f . F is Element of the carrier of a
R is set
[R,(f . F)] is non empty set
{R,(f . F)} is non empty finite set
{R} is non empty trivial finite 1 -element set
{{R,(f . F)},{R}} is non empty finite V34() set
dist ((TW . rngs),(TW . F)) is V11() real ext-real Element of REAL
the distance of (a,b,D) is non empty Relation-like [: the carrier of (a,b,D), the carrier of (a,b,D):] -defined REAL -valued Function-like total V27([: the carrier of (a,b,D), the carrier of (a,b,D):], REAL ) Element of bool [:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:]
[: the carrier of (a,b,D), the carrier of (a,b,D):] is non empty set
[:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:] is non empty non trivial non finite set
the distance of (a,b,D) . ((TW . rngs),(TW . F)) is V11() real ext-real Element of REAL
dist ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
the distance of a . ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
dist ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
the distance of a . ((f . rngs),(f . F)) is V11() real ext-real Element of REAL
dist ((f . rngs),b) is V11() real ext-real Element of REAL
the distance of a . ((f . rngs),b) is V11() real ext-real Element of REAL
dist (b,(f . F)) is V11() real ext-real Element of REAL
the distance of a . (b,(f . F)) is V11() real ext-real Element of REAL
(dist ((f . rngs),b)) + (dist (b,(f . F))) is V11() real ext-real Element of REAL
dist ((TW . rngs),(TW . F)) is V11() real ext-real Element of REAL
the distance of (a,b,D) is non empty Relation-like [: the carrier of (a,b,D), the carrier of (a,b,D):] -defined REAL -valued Function-like total V27([: the carrier of (a,b,D), the carrier of (a,b,D):], REAL ) Element of bool [:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:]
[: the carrier of (a,b,D), the carrier of (a,b,D):] is non empty set
[:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:] is non empty non trivial non finite set
the distance of (a,b,D) . ((TW . rngs),(TW . F)) is V11() real ext-real Element of REAL
s is Element of the carrier of a
W is Element of the carrier of (a,b,D)
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
S is V11() real ext-real Element of REAL
rngs 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
TW . F is Element of the carrier of (a,b,D)
dist ((TW . F),W) is V11() real ext-real Element of REAL
the distance of (a,b,D) is non empty Relation-like [: the carrier of (a,b,D), the carrier of (a,b,D):] -defined REAL -valued Function-like total V27([: the carrier of (a,b,D), the carrier of (a,b,D):], REAL ) Element of bool [:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:]
[: the carrier of (a,b,D), the carrier of (a,b,D):] is non empty set
[:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:] is non empty non trivial non finite set
the distance of (a,b,D) . ((TW . F),W) is V11() real ext-real Element of REAL
TW . F is Element of the carrier of (a,b,D)
f . F is Element of the carrier of a
F is set
[F,(f . F)] is non empty set
{F,(f . F)} is non empty finite set
{F} is non empty trivial finite 1 -element set
{{F,(f . F)},{F}} is non empty finite V34() set
dist ((TW . F),W) is V11() real ext-real Element of REAL
the distance of (a,b,D) . ((TW . F),W) is V11() real ext-real Element of REAL
dist ((f . F),s) is V11() real ext-real Element of REAL
the distance of a . ((f . F),s) is V11() real ext-real Element of REAL
(dist ((f . F),s)) + 0 is V11() real ext-real Element of REAL
W is Element of the carrier of (a,b,D)
S is V11() real ext-real Element of REAL
rngs 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
F is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
TW . F is Element of the carrier of (a,b,D)
dist ((TW . F),W) is V11() real ext-real Element of REAL
the distance of (a,b,D) is non empty Relation-like [: the carrier of (a,b,D), the carrier of (a,b,D):] -defined REAL -valued Function-like total V27([: the carrier of (a,b,D), the carrier of (a,b,D):], REAL ) Element of bool [:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:]
[: the carrier of (a,b,D), the carrier of (a,b,D):] is non empty set
[:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:] is non empty non trivial non finite set
the distance of (a,b,D) . ((TW . F),W) is V11() real ext-real Element of REAL
TW . F is Element of the carrier of (a,b,D)
dist ((TW . F),W) is V11() real ext-real Element of REAL
the distance of (a,b,D) . ((TW . F),W) is V11() real ext-real Element of REAL
S is ordinal natural V11() real finite cardinal ext-real non negative set
rngs is set
S is ordinal natural V11() real finite cardinal ext-real non negative set
rngs is set
TW . S is Element of the carrier of (a,b,D)
[rngs,s] is non empty set
{rngs,s} is non empty finite set
{rngs} is non empty trivial finite 1 -element set
{{rngs,s},{rngs}} is non empty finite V34() set
F is ordinal natural V11() real finite cardinal ext-real non negative set
R is set
F is Element of the carrier of (a,b,D)
F is V11() real ext-real Element of REAL
R is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
max (R,S) is ordinal natural V11() real finite cardinal ext-real non negative set
R9 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
R9 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
TW . R9 is Element of the carrier of (a,b,D)
dist ((TW . R9),F) is V11() real ext-real Element of REAL
the distance of (a,b,D) is non empty Relation-like [: the carrier of (a,b,D), the carrier of (a,b,D):] -defined REAL -valued Function-like total V27([: the carrier of (a,b,D), the carrier of (a,b,D):], REAL ) Element of bool [:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:]
[: the carrier of (a,b,D), the carrier of (a,b,D):] is non empty set
[:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:] is non empty non trivial non finite set
the distance of (a,b,D) . ((TW . R9),F) is V11() real ext-real Element of REAL
TW . R9 is Element of the carrier of (a,b,D)
f . R9 is Element of the carrier of a
c₁₆ is set
[c₁₆,(f . R9)] is non empty set
{c₁₆,(f . R9)} is non empty finite set
{c₁₆} is non empty trivial finite 1 -element set
{{c₁₆,(f . R9)},{c₁₆}} is non empty finite V34() set
SI is Element of the carrier of a
[rngs,SI] is non empty set
{rngs,SI} is non empty finite set
{{rngs,SI},{rngs}} is non empty finite V34() set
dist ((TW . R9),F) is V11() real ext-real Element of REAL
the distance of (a,b,D) . ((TW . R9),F) is V11() real ext-real Element of REAL
dist ((f . R9),s) 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 . ((f . R9),s) is V11() real ext-real Element of REAL
W is Element of the carrier of (a,b,D)
F 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
R is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
TW . R is Element of the carrier of (a,b,D)
dist ((TW . R),W) is V11() real ext-real Element of REAL
the distance of (a,b,D) is non empty Relation-like [: the carrier of (a,b,D), the carrier of (a,b,D):] -defined REAL -valued Function-like total V27([: the carrier of (a,b,D), the carrier of (a,b,D):], REAL ) Element of bool [:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:]
[: the carrier of (a,b,D), the carrier of (a,b,D):] is non empty set
[:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (a,b,D), the carrier of (a,b,D):],REAL:] is non empty non trivial non finite set
the distance of (a,b,D) . ((TW . R),W) is V11() real ext-real Element of REAL
TW . R is Element of the carrier of (a,b,D)
R9 is set
R9 is Element of the carrier of a
[R9,R9] is non empty set
{R9,R9} is non empty finite set
{R9} is non empty trivial finite 1 -element set
{{R9,R9},{R9}} is non empty finite V34() set
c₁₆ is Element of the carrier of a
[rngs,c₁₆] is non empty set
{rngs,c₁₆} is non empty finite set
{rngs} is non empty trivial finite 1 -element set
{{rngs,c₁₆},{rngs}} is non empty finite V34() set
dist ((TW . R),W) is V11() real ext-real Element of REAL
the distance of (a,b,D) . ((TW . R),W) is V11() real ext-real Element of REAL
F is set
F is Element of the carrier of a
[F,F] is non empty set
{F,F} is non empty finite set
{F} is non empty trivial finite 1 -element set
{{F,F},{F}} is non empty finite V34() set
R is Element of the carrier of a
[rngs,R] is non empty set
{rngs,R} is non empty finite set
{rngs} is non empty trivial finite 1 -element set
{{rngs,R},{rngs}} is non empty finite V34() set
S is Element of the carrier of (a,b,D)
rngs is V11() real ext-real Element of REAL
D is non empty Reflexive symmetric triangle MetrStruct
the carrier of D is non empty set
a is Element of the carrier of D
b is Element of the carrier of D
dist (a,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 . (a,b) is V11() real ext-real Element of REAL
b is Element of the carrier of D
dist (a,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 . (a,b) is V11() real ext-real Element of REAL
X is non empty non trivial non finite set
(D,a,X) is non empty strict Reflexive symmetric triangle MetrStruct
{a} is non empty trivial finite 1 -element set
the carrier of D \ {a} is Element of bool the carrier of D
bool the carrier of D is non empty set
[:X,( the carrier of D \ {a}):] is set
[X,a] is non empty set
{X,a} is non empty finite set
{X} is non empty trivial finite 1 -element set
{{X,a},{X}} is non empty finite V34() set
{[X,a]} is non empty trivial finite 1 -element set
[:X,( the carrier of D \ {a}):] \/ {[X,a]} is non empty set
(D,a,X) is non empty Relation-like [:([:X,( the carrier of D \ {a}):] \/ {[X,a]}),([:X,( the carrier of D \ {a}):] \/ {[X,a]}):] -defined REAL -valued Function-like total V27([:([:X,( the carrier of D \ {a}):] \/ {[X,a]}),([:X,( the carrier of D \ {a}):] \/ {[X,a]}):], REAL ) Element of bool [:[:([:X,( the carrier of D \ {a}):] \/ {[X,a]}),([:X,( the carrier of D \ {a}):] \/ {[X,a]}):],REAL:]
[:([:X,( the carrier of D \ {a}):] \/ {[X,a]}),([:X,( the carrier of D \ {a}):] \/ {[X,a]}):] is non empty set
[:[:([:X,( the carrier of D \ {a}):] \/ {[X,a]}),([:X,( the carrier of D \ {a}):] \/ {[X,a]}):],REAL:] is non empty non trivial non finite set
bool [:[:([:X,( the carrier of D \ {a}):] \/ {[X,a]}),([:X,( the carrier of D \ {a}):] \/ {[X,a]}):],REAL:] is non empty non trivial non finite set
MetrStruct(# ([:X,( the carrier of D \ {a}):] \/ {[X,a]}),(D,a,X) #) is strict MetrStruct
the carrier of (D,a,X) is non empty set
bool the carrier of (D,a,X) is non empty Element of bool (bool the carrier of (D,a,X))
bool the carrier of (D,a,X) is non empty set
bool (bool the carrier of (D,a,X)) is non empty set
[:NAT,(bool the carrier of (D,a,X)):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of (D,a,X)):] is non empty non trivial non finite set
TopSpaceMetr (D,a,X) is non empty strict TopSpace-like TopStruct
Family_open_set (D,a,X) is Element of bool (bool the carrier of (D,a,X))
TopStruct(# the carrier of (D,a,X),(Family_open_set (D,a,X)) #) is non empty strict TopStruct
[:NAT,X:] is non empty non trivial non finite set
bool [:NAT,X:] is non empty non trivial non finite set
f is non empty Relation-like NAT -defined X -valued Function-like total V27( NAT ,X) Element of bool [:NAT,X:]
the carrier of (TopSpaceMetr (D,a,X)) is non empty set
s is set
f . s is set
[(f . s),b] is non empty set
{(f . s),b} is non empty finite set
{(f . s)} is non empty trivial finite 1 -element set
{{(f . s),b},{(f . s)}} is non empty finite V34() set
dom f is V141() V142() V143() V144() V145() V146() Element of bool NAT
rng f is Element of bool X
bool X is non empty non trivial non finite set
[:NAT, the carrier of (TopSpaceMetr (D,a,X)):] is non empty non trivial non finite set
bool [:NAT, the carrier of (TopSpaceMetr (D,a,X)):] is non empty non trivial non finite set
s is non empty Relation-like NAT -defined the carrier of (TopSpaceMetr (D,a,X)) -valued Function-like total V27( NAT , the carrier of (TopSpaceMetr (D,a,X))) Element of bool [:NAT, the carrier of (TopSpaceMetr (D,a,X)):]
bool the carrier of (TopSpaceMetr (D,a,X)) is non empty Element of bool (bool the carrier of (TopSpaceMetr (D,a,X)))
bool the carrier of (TopSpaceMetr (D,a,X)) is non empty set
bool (bool the carrier of (TopSpaceMetr (D,a,X))) is non empty set
dom s is V141() V142() V143() V144() V145() V146() Element of bool NAT
S is set
s . S is set
{(s . S)} is non empty trivial finite 1 -element set
rng s is Element of bool the carrier of (TopSpaceMetr (D,a,X))
[:NAT,(bool the carrier of (TopSpaceMetr (D,a,X))):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of (TopSpaceMetr (D,a,X))):] is non empty non trivial non finite set
S is non empty Relation-like NAT -defined bool the carrier of (TopSpaceMetr (D,a,X)) -valued Function-like total V27( NAT , bool the carrier of (TopSpaceMetr (D,a,X))) Element of bool [:NAT,(bool the carrier of (TopSpaceMetr (D,a,X))):]
rngs is set
F is set
S . rngs is set
S . F is set
s . F is set
{(s . F)} is non empty trivial finite 1 -element set
s . rngs is set
f . rngs is set
[(f . rngs),b] is non empty set
{(f . rngs),b} is non empty finite set
{(f . rngs)} is non empty trivial finite 1 -element set
{{(f . rngs),b},{(f . rngs)}} is non empty finite V34() set
{(s . rngs)} is non empty trivial finite 1 -element set
f . F is set
[(f . F),b] is non empty set
{(f . F),b} is non empty finite set
{(f . F)} is non empty trivial finite 1 -element set
{{(f . F),b},{(f . F)}} is non empty finite V34() set
rng s is Element of bool the carrier of (TopSpaceMetr (D,a,X))
rngs is Element of bool the carrier of (TopSpaceMetr (D,a,X))
{ {b₁} where b₁ is Element of the carrier of (TopSpaceMetr (D,a,X)) : b₁ in rngs } is set
2 * (dist (a,b)) is V11() real ext-real Element of REAL
rng S is Element of bool (bool the carrier of (TopSpaceMetr (D,a,X)))
bool (bool the carrier of (TopSpaceMetr (D,a,X))) is non empty set
F is Element of bool (bool the carrier of (TopSpaceMetr (D,a,X)))
R is set
dom S is V141() V142() V143() V144() V145() V146() Element of bool NAT
R9 is set
S . R9 is set
dom s is V141() V142() V143() V144() V145() V146() Element of bool NAT
s . R9 is set
{(s . R9)} is non empty trivial finite 1 -element set
R is set
dom S is V141() V142() V143() V144() V145() V146() Element of bool NAT
S . R is set
s . R is set
{(s . R)} is non empty trivial finite 1 -element set
R is non empty Relation-like non-empty NAT -defined bool the carrier of (TopSpaceMetr (D,a,X)) -valued Function-like total V27( NAT , bool the carrier of (TopSpaceMetr (D,a,X))) ( TopSpaceMetr (D,a,X)) Element of bool [:NAT,(bool the carrier of (TopSpaceMetr (D,a,X))):]
meet R is Element of bool the carrier of (TopSpaceMetr (D,a,X))
R9 is Element of the carrier of (D,a,X)
c₁₆ is Element of the carrier of (D,a,X)
dom s is V141() V142() V143() V144() V145() V146() Element of bool NAT
SI is set
s . SI is set
f . SI is set
[(f . SI),b] is non empty set
{(f . SI),b} is non empty finite set
{(f . SI)} is non empty trivial finite 1 -element set
{{(f . SI),b},{(f . SI)}} is non empty finite V34() set
x is set
s . x is set
f . x is set
[(f . x),b] is non empty set
{(f . x),b} is non empty finite set
{(f . x)} is non empty trivial finite 1 -element set
{{(f . x),b},{(f . x)}} is non empty finite V34() set
(D,a,X) . (R9,c₁₆) is set
dist (b,a) is V11() real ext-real Element of REAL
the distance of D . (b,a) is V11() real ext-real Element of REAL
(dist (b,a)) + (dist (a,b)) is V11() real ext-real Element of REAL
dist (R9,c₁₆) is V11() real ext-real Element of REAL
the distance of (D,a,X) is non empty Relation-like [: the carrier of (D,a,X), the carrier of (D,a,X):] -defined REAL -valued Function-like total V27([: the carrier of (D,a,X), the carrier of (D,a,X):], REAL ) Element of bool [:[: the carrier of (D,a,X), the carrier of (D,a,X):],REAL:]
[: the carrier of (D,a,X), the carrier of (D,a,X):] is non empty set
[:[: the carrier of (D,a,X), the carrier of (D,a,X):],REAL:] is non empty non trivial non finite set
bool [:[: the carrier of (D,a,X), the carrier of (D,a,X):],REAL:] is non empty non trivial non finite set
the distance of (D,a,X) . (R9,c₁₆) is V11() real ext-real Element of REAL
R9 is ordinal natural V11() real finite cardinal ext-real non negative set
R . R9 is Element of bool the carrier of (TopSpaceMetr (D,a,X))
{ (S . b₁) where b₁ is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT : R9 <= b₁ } is set
c₁₆ is Element of bool (bool the carrier of (TopSpaceMetr (D,a,X)))
union c₁₆ is Element of bool the carrier of (TopSpaceMetr (D,a,X))
Cl (union c₁₆) is closed Element of bool the carrier of (TopSpaceMetr (D,a,X))
x is Element of the carrier of (D,a,X)
SI is Element of bool the carrier of (D,a,X)
y is Element of the carrier of (D,a,X)
xS is set
j1 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
S . j1 is Element of bool the carrier of (TopSpaceMetr (D,a,X))
s . j1 is Element of the carrier of (TopSpaceMetr (D,a,X))
{(s . j1)} is non empty trivial finite 1 -element Element of bool the carrier of (TopSpaceMetr (D,a,X))
yS is set
j2 is ordinal natural V11() real finite cardinal ext-real non negative V139() V140() V141() V142() V143() V144() V145() V146() Element of NAT
S . j2 is Element of bool the carrier of (TopSpaceMetr (D,a,X))
s . j2 is Element of the carrier of (TopSpaceMetr (D,a,X))
{(s . j2)} is non empty trivial finite 1 -element Element of bool the carrier of (TopSpaceMetr (D,a,X))
dist (x,y) is V11() real ext-real Element of REAL
the distance of (D,a,X) . (x,y) is V11() real ext-real Element of REAL
R9 is non empty Relation-like non-empty NAT -defined bool the carrier of (D,a,X) -valued Function-like total V27( NAT , bool the carrier of (D,a,X)) Element of bool [:NAT,(bool the carrier of (D,a,X)):]
R9 . R9 is Element of bool the carrier of (D,a,X)
R9 is non empty Relation-like non-empty NAT -defined bool the carrier of (D,a,X) -valued Function-like total V27( NAT , bool the carrier of (D,a,X)) ((D,a,X)) Element of bool [:NAT,(bool the carrier of (D,a,X)):]
meet R9 is Element of bool the carrier of (D,a,X)
c₁₆ is Element of the carrier of (D,a,X)
SI is Element of the carrier of (D,a,X)
dist (c₁₆,SI) is V11() real ext-real Element of REAL
the distance of (D,a,X) . (c₁₆,SI) is V11() real ext-real Element of REAL
DiscreteSpace 2 is non empty strict Reflexive discerning symmetric triangle Discerning bounded MetrStruct
discrete_dist 2 is non empty Relation-like [:2,2:] -defined REAL -valued Function-like total V27([:2,2:], REAL ) finite Element of bool [:[:2,2:],REAL:]
MetrStruct(# 2,(discrete_dist 2) #) is strict MetrStruct
D is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of D is non empty 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)
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
a is Element of the carrier of D
b is Element of the carrier of D
dist (a,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 . (a,b) is V11() real ext-real Element of REAL
(D,a,NAT) is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
{a} is non empty trivial finite 1 -element set
the carrier of D \ {a} is Element of bool the carrier of D
[:NAT,( the carrier of D \ {a}):] is set
[NAT,a] is non empty set
{NAT,a} is non empty finite set
{NAT} is non empty trivial finite 1 -element set
{{NAT,a},{NAT}} is non empty finite V34() set
{[NAT,a]} is non empty trivial finite 1 -element set
[:NAT,( the carrier of D \ {a}):] \/ {[NAT,a]} is non empty set
(D,a,NAT) is non empty Relation-like [:([:NAT,( the carrier of D \ {a}):] \/ {[NAT,a]}),([:NAT,( the carrier of D \ {a}):] \/ {[NAT,a]}):] -defined REAL -valued Function-like total V27([:([:NAT,( the carrier of D \ {a}):] \/ {[NAT,a]}),([:NAT,( the carrier of D \ {a}):] \/ {[NAT,a]}):], REAL ) Element of bool [:[:([:NAT,( the carrier of D \ {a}):] \/ {[NAT,a]}),([:NAT,( the carrier of D \ {a}):] \/ {[NAT,a]}):],REAL:]
[:([:NAT,( the carrier of D \ {a}):] \/ {[NAT,a]}),([:NAT,( the carrier of D \ {a}):] \/ {[NAT,a]}):] is non empty set
[:[:([:NAT,( the carrier of D \ {a}):] \/ {[NAT,a]}),([:NAT,( the carrier of D \ {a}):] \/ {[NAT,a]}):],REAL:] is non empty non trivial non finite set
bool [:[:([:NAT,( the carrier of D \ {a}):] \/ {[NAT,a]}),([:NAT,( the carrier of D \ {a}):] \/ {[NAT,a]}):],REAL:] is non empty non trivial non finite set
MetrStruct(# ([:NAT,( the carrier of D \ {a}):] \/ {[NAT,a]}),(D,a,NAT) #) is strict MetrStruct
the carrier of (D,a,NAT) is non empty set
bool the carrier of (D,a,NAT) is non empty Element of bool (bool the carrier of (D,a,NAT))
bool the carrier of (D,a,NAT) is non empty set
bool (bool the carrier of (D,a,NAT)) is non empty set
[:NAT,(bool the carrier of (D,a,NAT)):] is non empty non trivial non finite set
bool [:NAT,(bool the carrier of (D,a,NAT)):] is non empty non trivial non finite set
X is non empty Relation-like non-empty NAT -defined bool the carrier of (D,a,NAT) -valued Function-like total V27( NAT , bool the carrier of (D,a,NAT)) ((D,a,NAT)) Element of bool [:NAT,(bool the carrier of (D,a,NAT)):]
meet X is Element of bool the carrier of (D,a,NAT)