REAL is complex-membered ext-real-membered real-membered V105() V108() V109() V111() set
NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V105() V108() Element of bool REAL
bool REAL is non empty set
COMPLEX is complex-membered V105() set
omega is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V105() V108() set
bool omega is non empty set
I[01] is non empty strict TopSpace-like TopStruct
the carrier of I[01] is non empty set
1 is non empty natural V14() real ext-real positive complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V106() V108() Element of NAT
[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty natural V14() real ext-real positive complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V106() V108() Element of NAT
[:2,2:] is non empty set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is non empty set
{} is empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V105() V108() V111() set
0 is empty natural V14() real ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V105() V108() V111() Element of NAT
RealSpace is non empty strict Reflexive discerning V122() triangle Discerning MetrStruct
real_dist is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like V36([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]
MetrStruct(# REAL,real_dist #) is strict MetrStruct
TopSpaceMetr RealSpace is non empty strict TopSpace-like TopStruct
the carrier of RealSpace is non empty set
Family_open_set RealSpace is Element of bool (bool the carrier of RealSpace)
bool the carrier of RealSpace is non empty set
bool (bool the carrier of RealSpace) is non empty set
TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr RealSpace) is non empty set
bool the carrier of (TopSpaceMetr RealSpace) is non empty set
[.0,1.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
x is TopStruct
the carrier of x is set
bool the carrier of x is non empty set
bool (bool the carrier of x) is non empty set
R is Element of bool (bool the carrier of T)
union R is set
e is Element of bool (bool the carrier of x)
union e is set
T is non empty TopSpace-like TopStruct
R is non empty TopSpace-like SubSpace of T
the carrier of R is non empty set
bool the carrier of R is non empty set
x is Element of the carrier of R
e is Element of the carrier of R
the carrier of T is non empty set
bool the carrier of T is non empty set
B is Element of the carrier of T
A is Element of the carrier of T
B2 is Element of bool the carrier of T
r is Element of bool the carrier of T
[#] R is non empty non proper open closed dense non boundary Element of bool the carrier of R
B2 /\ ([#] R) is Element of bool the carrier of R
r /\ ([#] R) is Element of bool the carrier of R
the topology of T is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
d is Element of bool the carrier of R
the topology of R is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
W9 is Element of bool the carrier of R
B2 /\ r is Element of bool the carrier of T
W9 /\ d is Element of bool the carrier of R
B2 /\ (r /\ ([#] R)) is Element of bool the carrier of R
(B2 /\ (r /\ ([#] R))) /\ ([#] R) is Element of bool the carrier of R
{} /\ ([#] R) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V108() Element of bool the carrier of R
T is TopSpace-like TopStruct
R is TopSpace-like SubSpace of T
the carrier of R is set
x is TopSpace-like SubSpace of T
the carrier of x is set
bool the carrier of R is non empty set
the topology of R is non empty Element of bool (bool the carrier of R)
bool (bool the carrier of R) is non empty set
bool the carrier of x is non empty set
the topology of x is non empty Element of bool (bool the carrier of x)
bool (bool the carrier of x) is non empty set
[#] R is non proper open closed dense Element of bool the carrier of R
e is Element of bool the carrier of R
the carrier of T is set
bool the carrier of T is non empty set
the topology of T is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
B is Element of bool the carrier of T
B /\ ([#] R) is Element of bool the carrier of R
[#] x is non proper open closed dense Element of bool the carrier of x
B /\ ([#] x) is Element of bool the carrier of x
A is Element of bool the carrier of x
([#] x) /\ ([#] R) is Element of bool the carrier of R
B /\ (([#] x) /\ ([#] R)) is Element of bool the carrier of R
A /\ ([#] R) is Element of bool the carrier of R
B is Element of bool the carrier of x
B /\ ([#] R) is Element of bool the carrier of R
the carrier of T is set
bool the carrier of T is non empty set
the topology of T is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
[#] x is non proper open closed dense Element of bool the carrier of x
A is Element of bool the carrier of T
A /\ ([#] x) is Element of bool the carrier of x
([#] x) /\ ([#] R) is Element of bool the carrier of R
A /\ (([#] x) /\ ([#] R)) is Element of bool the carrier of R
A /\ ([#] R) is Element of bool the carrier of R
[#] x is non proper open closed dense Element of bool the carrier of x
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
R is Element of bool the carrier of T
T | R is strict TopSpace-like SubSpace of T
x is Element of bool the carrier of T
R \/ x is Element of bool the carrier of T
T | (R \/ x) is strict TopSpace-like SubSpace of T
T | x is strict TopSpace-like SubSpace of T
[#] (T | R) is non proper open closed dense Element of bool the carrier of (T | R)
the carrier of (T | R) is set
bool the carrier of (T | R) is non empty set
[#] (T | (R \/ x)) is non proper open closed dense Element of bool the carrier of (T | (R \/ x))
the carrier of (T | (R \/ x)) is set
bool the carrier of (T | (R \/ x)) is non empty set
[#] (T | x) is non proper open closed dense Element of bool the carrier of (T | x)
the carrier of (T | x) is set
bool the carrier of (T | x) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
R is Element of the carrier of T
x is non empty Element of bool the carrier of T
T | x is non empty strict TopSpace-like SubSpace of T
the carrier of (T | x) is non empty set
bool the carrier of (T | x) is non empty set
e is a_neighborhood of R
e /\ x is Element of bool the carrier of T
B is Element of the carrier of (T | x)
A is Element of bool the carrier of (T | x)
Int e is open Element of bool the carrier of T
B2 is Element of bool the carrier of T
B2 /\ x is Element of bool the carrier of T
r is Element of bool the carrier of (T | x)
[#] (T | x) is non empty non proper open closed dense non boundary Element of bool the carrier of (T | x)
B2 /\ ([#] (T | x)) is Element of bool the carrier of (T | x)
Int A is open Element of bool the carrier of (T | x)
T is TopSpace-like TopStruct
the carrier of T is set
R is TopSpace-like TopStruct
the carrier of R is set
[: the carrier of T, the carrier of R:] is set
bool [: the carrier of T, the carrier of R:] is non empty set
bool the carrier of R is non empty set
x is Relation-like the carrier of T -defined the carrier of R -valued Function-like V36( the carrier of T, the carrier of R) Element of bool [: the carrier of T, the carrier of R:]
e is Element of bool the carrier of R
R | e is strict TopSpace-like SubSpace of R
the carrier of (R | e) is set
[: the carrier of T, the carrier of (R | e):] is set
bool [: the carrier of T, the carrier of (R | e):] is non empty set
[#] (R | e) is non proper open closed dense Element of bool the carrier of (R | e)
bool the carrier of (R | e) is non empty set
B is Relation-like the carrier of T -defined the carrier of (R | e) -valued Function-like V36( the carrier of T, the carrier of (R | e)) Element of bool [: the carrier of T, the carrier of (R | e):]
rng x is Element of bool the carrier of R
A is Element of bool the carrier of (R | e)
B " A is Element of bool the carrier of T
bool the carrier of T is non empty set
B2 is Element of bool the carrier of R
B2 /\ ([#] (R | e)) is Element of bool the carrier of (R | e)
B2 /\ e is Element of bool the carrier of R
x " (B2 /\ e) is Element of bool the carrier of T
x " B2 is Element of bool the carrier of T
x " e is Element of bool the carrier of T
(x " B2) /\ (x " e) is Element of bool the carrier of T
(rng x) /\ e is Element of bool the carrier of R
x " ((rng x) /\ e) is Element of bool the carrier of T
(x " B2) /\ (x " ((rng x) /\ e)) is Element of bool the carrier of T
x " (rng x) is Element of bool the carrier of T
(x " B2) /\ (x " (rng x)) is Element of bool the carrier of T
dom x is Element of bool the carrier of T
(x " B2) /\ (dom x) is Element of bool the carrier of T
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
R is non empty TopStruct
the carrier of R is non empty set
[: the carrier of T, the carrier of R:] is set
bool [: the carrier of T, the carrier of R:] is non empty set
x is Element of bool the carrier of T
T | x is strict SubSpace of T
the carrier of (T | x) is set
[: the carrier of (T | x), the carrier of R:] is set
bool [: the carrier of (T | x), the carrier of R:] is non empty set
e is Relation-like the carrier of T -defined the carrier of R -valued Function-like V36( the carrier of T, the carrier of R) Element of bool [: the carrier of T, the carrier of R:]
e | x is Relation-like the carrier of T -defined the carrier of R -valued Element of bool [: the carrier of T, the carrier of R:]
B is Relation-like the carrier of (T | x) -defined the carrier of R -valued Function-like V36( the carrier of (T | x), the carrier of R) Element of bool [: the carrier of (T | x), the carrier of R:]
[#] R is non empty non proper dense Element of bool the carrier of R
bool the carrier of R is non empty set
A is Element of bool the carrier of R
B " A is Element of bool the carrier of (T | x)
bool the carrier of (T | x) is non empty set
[#] (T | x) is non proper dense Element of bool the carrier of (T | x)
e " A is Element of bool the carrier of T
([#] (T | x)) /\ (e " A) is Element of bool the carrier of T
T is Reflexive discerning V122() triangle MetrStruct
the carrier of T is set
the distance of T is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like V36([: the carrier of T, the carrier of T:], REAL ) Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
[: the carrier of T, the carrier of T:] is set
[:[: the carrier of T, the carrier of T:],REAL:] is set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty set
MetrStruct(# the carrier of T, the distance of T #) is strict MetrStruct
the carrier of MetrStruct(# the carrier of T, the distance of T #) is set
R is Element of the carrier of MetrStruct(# the carrier of T, the distance of T #)
x is Element of the carrier of MetrStruct(# the carrier of T, the distance of T #)
e is Element of the carrier of MetrStruct(# the carrier of T, the distance of T #)
dist (R,e) is V14() real ext-real Element of REAL
the distance of MetrStruct(# the carrier of T, the distance of T #) is Relation-like [: the carrier of MetrStruct(# the carrier of T, the distance of T #), the carrier of MetrStruct(# the carrier of T, the distance of T #):] -defined REAL -valued Function-like V36([: the carrier of MetrStruct(# the carrier of T, the distance of T #), the carrier of MetrStruct(# the carrier of T, the distance of T #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# the carrier of T, the distance of T #), the carrier of MetrStruct(# the carrier of T, the distance of T #):],REAL:]
[: the carrier of MetrStruct(# the carrier of T, the distance of T #), the carrier of MetrStruct(# the carrier of T, the distance of T #):] is set
[:[: the carrier of MetrStruct(# the carrier of T, the distance of T #), the carrier of MetrStruct(# the carrier of T, the distance of T #):],REAL:] is set
bool [:[: the carrier of MetrStruct(# the carrier of T, the distance of T #), the carrier of MetrStruct(# the carrier of T, the distance of T #):],REAL:] is non empty set
the distance of MetrStruct(# the carrier of T, the distance of T #) . (R,e) is V14() real ext-real Element of REAL
[R,e] is set
{R,e} is non empty set
{R} is non empty set
{{R,e},{R}} is non empty set
the distance of MetrStruct(# the carrier of T, the distance of T #) . [R,e] is set
the distance of T . (R,e) is set
the distance of T . [R,e] is set
B is Element of the carrier of T
B2 is Element of the carrier of T
dist (B,B2) is V14() real ext-real Element of REAL
the distance of T . (B,B2) is V14() real ext-real Element of REAL
[B,B2] is set
{B,B2} is non empty set
{B} is non empty set
{{B,B2},{B}} is non empty set
the distance of T . [B,B2] is set
dist (R,x) is V14() real ext-real Element of REAL
the distance of MetrStruct(# the carrier of T, the distance of T #) . (R,x) is V14() real ext-real Element of REAL
[R,x] is set
{R,x} is non empty set
{{R,x},{R}} is non empty set
the distance of MetrStruct(# the carrier of T, the distance of T #) . [R,x] is set
the distance of T . (R,x) is set
the distance of T . [R,x] is set
A is Element of the carrier of T
dist (B,A) is V14() real ext-real Element of REAL
the distance of T . (B,A) is V14() real ext-real Element of REAL
[B,A] is set
{B,A} is non empty set
{{B,A},{B}} is non empty set
the distance of T . [B,A] is set
dist (x,R) is V14() real ext-real Element of REAL
the distance of MetrStruct(# the carrier of T, the distance of T #) . (x,R) is V14() real ext-real Element of REAL
[x,R] is set
{x,R} is non empty set
{x} is non empty set
{{x,R},{x}} is non empty set
the distance of MetrStruct(# the carrier of T, the distance of T #) . [x,R] is set
the distance of T . (x,R) is set
the distance of T . [x,R] is set
dist (A,B) is V14() real ext-real Element of REAL
the distance of T . (A,B) is V14() real ext-real Element of REAL
[A,B] is set
{A,B} is non empty set
{A} is non empty set
{{A,B},{A}} is non empty set
the distance of T . [A,B] is set
dist (x,e) is V14() real ext-real Element of REAL
the distance of MetrStruct(# the carrier of T, the distance of T #) . (x,e) is V14() real ext-real Element of REAL
[x,e] is set
{x,e} is non empty set
{{x,e},{x}} is non empty set
the distance of MetrStruct(# the carrier of T, the distance of T #) . [x,e] is set
the distance of T . (x,e) is set
the distance of T . [x,e] is set
dist (A,B2) is V14() real ext-real Element of REAL
the distance of T . (A,B2) is V14() real ext-real Element of REAL
[A,B2] is set
{A,B2} is non empty set
{{A,B2},{A}} is non empty set
the distance of T . [A,B2] is set
(dist (R,x)) + (dist (x,e)) is V14() real ext-real Element of REAL
T is Reflexive discerning V122() triangle MetrStruct
the carrier of T is set
the distance of T is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like V36([: the carrier of T, the carrier of T:], REAL ) Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
[: the carrier of T, the carrier of T:] is set
[:[: the carrier of T, the carrier of T:],REAL:] is set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty set
MetrStruct(# the carrier of T, the distance of T #) is strict MetrStruct
R is Reflexive discerning V122() triangle MetrStruct
the carrier of R is set
the distance of R is Relation-like [: the carrier of R, the carrier of R:] -defined REAL -valued Function-like V36([: the carrier of R, the carrier of R:], REAL ) Element of bool [:[: the carrier of R, the carrier of R:],REAL:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:],REAL:] is set
bool [:[: the carrier of R, the carrier of R:],REAL:] is non empty set
x is Element of the carrier of R
e is Element of the carrier of R
the distance of R . (x,e) is V14() real ext-real Element of REAL
[x,e] is set
{x,e} is non empty set
{x} is non empty set
{{x,e},{x}} is non empty set
the distance of R . [x,e] is set
the distance of T . (x,e) is set
the distance of T . [x,e] is set
T is Reflexive discerning V122() triangle MetrStruct
the carrier of T is set
the distance of T is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like V36([: the carrier of T, the carrier of T:], REAL ) Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
[: the carrier of T, the carrier of T:] is set
[:[: the carrier of T, the carrier of T:],REAL:] is set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty set
MetrStruct(# the carrier of T, the distance of T #) is strict MetrStruct
R is Reflexive discerning V122() triangle MetrStruct
the carrier of R is set
the distance of R is Relation-like [: the carrier of R, the carrier of R:] -defined REAL -valued Function-like V36([: the carrier of R, the carrier of R:], REAL ) Element of bool [:[: the carrier of R, the carrier of R:],REAL:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:],REAL:] is set
bool [:[: the carrier of R, the carrier of R:],REAL:] is non empty set
x is Element of the carrier of R
e is Element of the carrier of R
the distance of R . (x,e) is V14() real ext-real Element of REAL
[x,e] is set
{x,e} is non empty set
{x} is non empty set
{{x,e},{x}} is non empty set
the distance of R . [x,e] is set
the distance of T . (x,e) is set
the distance of T . [x,e] is set
T is non empty Reflexive discerning V122() triangle Discerning MetrStruct
the carrier of T is non empty set
the distance of T is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like V36([: the carrier of T, the carrier of T:], REAL ) Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty set
MetrStruct(# the carrier of T, the distance of T #) is non empty strict MetrStruct
R is Reflexive discerning V122() triangle MetrStruct
the carrier of R is set
the distance of R is Relation-like [: the carrier of R, the carrier of R:] -defined REAL -valued Function-like V36([: the carrier of R, the carrier of R:], REAL ) Element of bool [:[: the carrier of R, the carrier of R:],REAL:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:],REAL:] is set
bool [:[: the carrier of R, the carrier of R:],REAL:] is non empty set
x is Element of the carrier of R
e is Element of the carrier of R
the distance of R . (x,e) is V14() real ext-real Element of REAL
[x,e] is set
{x,e} is non empty set
{x} is non empty set
{{x,e},{x}} is non empty set
the distance of R . [x,e] is set
the distance of T . (x,e) is set
the distance of T . [x,e] is set
T is non empty Reflexive discerning V122() triangle Discerning MetrStruct
the carrier of T is non empty set
R is non empty Reflexive discerning V122() triangle Discerning (T)
the carrier of R is non empty set
x is Element of the carrier of R
T is V14() real ext-real set
R is Reflexive discerning V122() triangle MetrStruct
the carrier of R is set
x is Reflexive discerning V122() triangle (R)
the carrier of x is set
e is Element of the carrier of R
Ball (e,T) is Element of bool the carrier of R
bool the carrier of R is non empty set
(Ball (e,T)) /\ the carrier of x is Element of bool the carrier of R
B is Element of the carrier of x
Ball (B,T) is Element of bool the carrier of x
bool the carrier of x is non empty set
A is set
B2 is Element of the carrier of x
dist (B,B2) is V14() real ext-real Element of REAL
the distance of x is Relation-like [: the carrier of x, the carrier of x:] -defined REAL -valued Function-like V36([: the carrier of x, the carrier of x:], REAL ) Element of bool [:[: the carrier of x, the carrier of x:],REAL:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:],REAL:] is set
bool [:[: the carrier of x, the carrier of x:],REAL:] is non empty set
the distance of x . (B,B2) is V14() real ext-real Element of REAL
[B,B2] is set
{B,B2} is non empty set
{B} is non empty set
{{B,B2},{B}} is non empty set
the distance of x . [B,B2] is set
the distance of R is Relation-like [: the carrier of R, the carrier of R:] -defined REAL -valued Function-like V36([: the carrier of R, the carrier of R:], REAL ) Element of bool [:[: the carrier of R, the carrier of R:],REAL:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:],REAL:] is set
bool [:[: the carrier of R, the carrier of R:],REAL:] is non empty set
r is Element of the carrier of R
the distance of R . (e,r) is V14() real ext-real Element of REAL
[e,r] is set
{e,r} is non empty set
{e} is non empty set
{{e,r},{e}} is non empty set
the distance of R . [e,r] is set
dist (e,r) is V14() real ext-real Element of REAL
A is set
B2 is Element of the carrier of x
r is Element of the carrier of R
dist (e,r) is V14() real ext-real Element of REAL
the distance of R . (e,r) is V14() real ext-real Element of REAL
[e,r] is set
{e,r} is non empty set
{{e,r},{e}} is non empty set
the distance of R . [e,r] is set
the distance of x . (B,B2) is V14() real ext-real Element of REAL
[B,B2] is set
{B,B2} is non empty set
{{B,B2},{B}} is non empty set
the distance of x . [B,B2] is set
dist (B,B2) is V14() real ext-real Element of REAL
T is non empty Reflexive discerning V122() triangle Discerning MetrStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
R is non empty Element of bool the carrier of T
the distance of T is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like V36([: the carrier of T, the carrier of T:], REAL ) Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty set
the distance of T || R is Relation-like Function-like set
[:R,R:] is non empty set
the distance of T | [:R,R:] is Relation-like set
dom ( the distance of T || R) is set
dom the distance of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
bool [: the carrier of T, the carrier of T:] is non empty set
(dom the distance of T) /\ [:R,R:] is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
[: the carrier of T, the carrier of T:] /\ [:R,R:] is set
the carrier of T /\ R is Element of bool the carrier of T
[:( the carrier of T /\ R),( the carrier of T /\ R):] is set
[:( the carrier of T /\ R),R:] is set
the distance of T | [:R,R:] is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
rng ( the distance of T || R) is set
x is non empty set
[:x,x:] is non empty set
[:[:x,x:],REAL:] is set
bool [:[:x,x:],REAL:] is non empty set
B is Relation-like [:x,x:] -defined REAL -valued Function-like V36([:x,x:], REAL ) Element of bool [:[:x,x:],REAL:]
MetrStruct(# x,B #) is non empty strict MetrStruct
the carrier of MetrStruct(# x,B #) is non empty set
B2 is Element of the carrier of MetrStruct(# x,B #)
r is Element of the carrier of MetrStruct(# x,B #)
dist (B2,r) is V14() real ext-real Element of REAL
the distance of MetrStruct(# x,B #) is Relation-like [: the carrier of MetrStruct(# x,B #), the carrier of MetrStruct(# x,B #):] -defined REAL -valued Function-like V36([: the carrier of MetrStruct(# x,B #), the carrier of MetrStruct(# x,B #):], REAL ) Element of bool [:[: the carrier of MetrStruct(# x,B #), the carrier of MetrStruct(# x,B #):],REAL:]
[: the carrier of MetrStruct(# x,B #), the carrier of MetrStruct(# x,B #):] is non empty set
[:[: the carrier of MetrStruct(# x,B #), the carrier of MetrStruct(# x,B #):],REAL:] is set
bool [:[: the carrier of MetrStruct(# x,B #), the carrier of MetrStruct(# x,B #):],REAL:] is non empty set
the distance of MetrStruct(# x,B #) . (B2,r) is V14() real ext-real Element of REAL
[B2,r] is set
{B2,r} is non empty set
{B2} is non empty set
{{B2,r},{B2}} is non empty set
the distance of MetrStruct(# x,B #) . [B2,r] is set
[B2,r] is Element of [: the carrier of MetrStruct(# x,B #), the carrier of MetrStruct(# x,B #):]
the distance of T . [B2,r] is set
the distance of T . (B2,r) is set
the distance of T . [B2,r] is set
B2 is Element of the carrier of MetrStruct(# x,B #)
r is Element of the carrier of MetrStruct(# x,B #)
W9 is Element of the carrier of MetrStruct(# x,B #)
dist (B2,W9) is V14() real ext-real Element of REAL
the distance of MetrStruct(# x,B #) . (B2,W9) is V14() real ext-real Element of REAL
[B2,W9] is set
{B2,W9} is non empty set
{B2} is non empty set
{{B2,W9},{B2}} is non empty set
the distance of MetrStruct(# x,B #) . [B2,W9] is set
the distance of T . (B2,W9) is set
the distance of T . [B2,W9] is set
d is Element of the carrier of T
H is Element of the carrier of T
dist (d,H) is V14() real ext-real Element of REAL
the distance of T . (d,H) is V14() real ext-real Element of REAL
[d,H] is set
{d,H} is non empty set
{d} is non empty set
{{d,H},{d}} is non empty set
the distance of T . [d,H] is set
dist (B2,r) is V14() real ext-real Element of REAL
the distance of MetrStruct(# x,B #) . (B2,r) is V14() real ext-real Element of REAL
[B2,r] is set
{B2,r} is non empty set
{{B2,r},{B2}} is non empty set
the distance of MetrStruct(# x,B #) . [B2,r] is set
the distance of T . (B2,r) is set
the distance of T . [B2,r] is set
H is Element of the carrier of T
dist (d,H) is V14() real ext-real Element of REAL
the distance of T . (d,H) is V14() real ext-real Element of REAL
[d,H] is set
{d,H} is non empty set
{{d,H},{d}} is non empty set
the distance of T . [d,H] is set
dist (r,W9) is V14() real ext-real Element of REAL
the distance of MetrStruct(# x,B #) . (r,W9) is V14() real ext-real Element of REAL
[r,W9] is set
{r,W9} is non empty set
{r} is non empty set
{{r,W9},{r}} is non empty set
the distance of MetrStruct(# x,B #) . [r,W9] is set
the distance of T . (r,W9) is set
the distance of T . [r,W9] is set
dist (H,H) is V14() real ext-real Element of REAL
the distance of T . (H,H) is V14() real ext-real Element of REAL
[H,H] is set
{H,H} is non empty set
{H} is non empty set
{{H,H},{H}} is non empty set
the distance of T . [H,H] is set
dist (H,d) is V14() real ext-real Element of REAL
the distance of T . (H,d) is V14() real ext-real Element of REAL
[H,d] is set
{H,d} is non empty set
{{H,d},{H}} is non empty set
the distance of T . [H,d] is set
dist (r,B2) is V14() real ext-real Element of REAL
the distance of MetrStruct(# x,B #) . (r,B2) is V14() real ext-real Element of REAL
[r,B2] is set
{r,B2} is non empty set
{{r,B2},{r}} is non empty set
the distance of MetrStruct(# x,B #) . [r,B2] is set
(dist (B2,r)) + (dist (r,W9)) is V14() real ext-real Element of REAL
B2 is Reflexive discerning V122() triangle MetrStruct
the carrier of B2 is set
the distance of B2 is Relation-like [: the carrier of B2, the carrier of B2:] -defined REAL -valued Function-like V36([: the carrier of B2, the carrier of B2:], REAL ) Element of bool [:[: the carrier of B2, the carrier of B2:],REAL:]
[: the carrier of B2, the carrier of B2:] is set
[:[: the carrier of B2, the carrier of B2:],REAL:] is set
bool [:[: the carrier of B2, the carrier of B2:],REAL:] is non empty set
r is Element of the carrier of B2
W9 is Element of the carrier of B2
the distance of B2 . (r,W9) is V14() real ext-real Element of REAL
[r,W9] is set
{r,W9} is non empty set
{r} is non empty set
{{r,W9},{r}} is non empty set
the distance of B2 . [r,W9] is set
dist (r,W9) is V14() real ext-real Element of REAL
the distance of T . (r,W9) is set
the distance of T . [r,W9] is set
r is strict Reflexive discerning V122() triangle (T)
the carrier of r is set
x is strict Reflexive discerning V122() triangle (T)
the carrier of x is set
e is strict Reflexive discerning V122() triangle (T)
the carrier of e is set
the distance of x is Relation-like [: the carrier of x, the carrier of x:] -defined REAL -valued Function-like V36([: the carrier of x, the carrier of x:], REAL ) Element of bool [:[: the carrier of x, the carrier of x:],REAL:]
[: the carrier of x, the carrier of x:] is set
[:[: the carrier of x, the carrier of x:],REAL:] is set
bool [:[: the carrier of x, the carrier of x:],REAL:] is non empty set
B is Element of R
A is Element of R
the distance of x . (B,A) is set
[B,A] is set
{B,A} is non empty set
{B} is non empty set
{{B,A},{B}} is non empty set
the distance of x . [B,A] is set
the distance of T is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like V36([: the carrier of T, the carrier of T:], REAL ) Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty set
the distance of T . (B,A) is V14() real ext-real Element of REAL
the distance of T . [B,A] is set
the distance of e is Relation-like [: the carrier of e, the carrier of e:] -defined REAL -valued Function-like V36([: the carrier of e, the carrier of e:], REAL ) Element of bool [:[: the carrier of e, the carrier of e:],REAL:]
[: the carrier of e, the carrier of e:] is set
[:[: the carrier of e, the carrier of e:],REAL:] is set
bool [:[: the carrier of e, the carrier of e:],REAL:] is non empty set
the distance of e . (B,A) is set
the distance of e . [B,A] is set
T is non empty Reflexive discerning V122() triangle Discerning MetrStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
R is non empty Element of bool the carrier of T
(T,R) is strict Reflexive discerning V122() triangle (T)
T is V14() real ext-real set
R is V14() real ext-real set
[.T,R.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL
x is Element of bool the carrier of RealSpace
e is non empty Element of bool the carrier of RealSpace
(RealSpace,e) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )
B is non empty Element of bool the carrier of RealSpace
(RealSpace,B) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )
x is Element of bool the carrier of RealSpace
B is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )
A is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )
e is non empty Element of bool the carrier of RealSpace
(RealSpace,e) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )
T is V14() real ext-real set
R is V14() real ext-real set
(T,R) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )
the carrier of (T,R) is non empty set
[.T,R.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL
x is non empty Element of bool the carrier of RealSpace
(RealSpace,x) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )
the carrier of (RealSpace,x) is non empty set
T is MetrStruct
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
x is V14() real ext-real set
T is Element of the carrier of RealSpace
e is V14() real ext-real set
R is Element of the carrier of RealSpace
dist (T,R) is V14() real ext-real Element of REAL
the distance of RealSpace is Relation-like [: the carrier of RealSpace, the carrier of RealSpace:] -defined REAL -valued Function-like V36([: the carrier of RealSpace, the carrier of RealSpace:], REAL ) Element of bool [:[: the carrier of RealSpace, the carrier of RealSpace:],REAL:]
[: the carrier of RealSpace, the carrier of RealSpace:] is non empty set
[:[: the carrier of RealSpace, the carrier of RealSpace:],REAL:] is set
bool [:[: the carrier of RealSpace, the carrier of RealSpace:],REAL:] is non empty set
the distance of RealSpace . (T,R) is V14() real ext-real Element of REAL
[T,R] is set
{T,R} is non empty set
{T} is non empty set
{{T,R},{T}} is non empty set
the distance of RealSpace . [T,R] is set
x - e is V14() real ext-real set
abs (x - e) is V14() real ext-real Element of REAL
T is MetrStruct
the carrier of T is set
TopSpaceMetr T is strict TopSpace-like TopStruct
Family_open_set T is Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T,(Family_open_set T) #) is strict TopStruct
the carrier of (TopSpaceMetr T) is set
R is MetrStruct
TopSpaceMetr R is strict TopSpace-like TopStruct
the carrier of R is set
Family_open_set R is Element of bool (bool the carrier of R)
bool the carrier of R is non empty set
bool (bool the carrier of R) is non empty set
TopStruct(# the carrier of R,(Family_open_set R) #) is strict TopStruct
the topology of (TopSpaceMetr R) is non empty Element of bool (bool the carrier of (TopSpaceMetr R))
the carrier of (TopSpaceMetr R) is set
bool the carrier of (TopSpaceMetr R) is non empty set
bool (bool the carrier of (TopSpaceMetr R)) is non empty set
T is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr T is non empty strict TopSpace-like TopStruct
the carrier of T is non empty set
Family_open_set T is Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T,(Family_open_set T) #) is non empty strict TopStruct
R is non empty Reflexive discerning V122() triangle Discerning (T)
TopSpaceMetr R is non empty strict TopSpace-like TopStruct
the carrier of R is non empty set
Family_open_set R is Element of bool (bool the carrier of R)
bool the carrier of R is non empty set
bool (bool the carrier of R) is non empty set
TopStruct(# the carrier of R,(Family_open_set R) #) is non empty strict TopStruct
[#] (TopSpaceMetr R) is non empty non proper open closed dense non boundary Element of bool the carrier of (TopSpaceMetr R)
the carrier of (TopSpaceMetr R) is non empty set
bool the carrier of (TopSpaceMetr R) is non empty set
[#] (TopSpaceMetr T) is non empty non proper open closed dense non boundary Element of bool the carrier of (TopSpaceMetr T)
the carrier of (TopSpaceMetr T) is non empty set
bool the carrier of (TopSpaceMetr T) is non empty set
the topology of (TopSpaceMetr R) is non empty Element of bool (bool the carrier of (TopSpaceMetr R))
bool (bool the carrier of (TopSpaceMetr R)) is non empty set
the topology of (TopSpaceMetr T) is non empty Element of bool (bool the carrier of (TopSpaceMetr T))
bool (bool the carrier of (TopSpaceMetr T)) is non empty set
B is Element of bool the carrier of (TopSpaceMetr R)
{ (Ball (b1,b2)) where b1 is Element of the carrier of T, b2 is V14() real ext-real Element of REAL : ( b1 in B & not b2 <= 0 & (Ball (b1,b2)) /\ the carrier of R c= B ) } is set
B2 is set
r is Element of the carrier of T
W9 is V14() real ext-real Element of REAL
Ball (r,W9) is Element of bool the carrier of T
(Ball (r,W9)) /\ the carrier of R is Element of bool the carrier of T
union { (Ball (b1,b2)) where b1 is Element of the carrier of T, b2 is V14() real ext-real Element of REAL : ( b1 in B & not b2 <= 0 & (Ball (b1,b2)) /\ the carrier of R c= B ) } is set
B2 is Element of bool the carrier of T
r is Element of bool the carrier of (TopSpaceMetr T)
r /\ ([#] (TopSpaceMetr R)) is Element of bool the carrier of (TopSpaceMetr R)
d is set
H is Element of the carrier of R
W9 is Element of bool the carrier of R
W99 is V14() real ext-real Element of REAL
Ball (H,W99) is Element of bool the carrier of R
H is Element of the carrier of T
Ball (H,W99) is Element of bool the carrier of T
(Ball (H,W99)) /\ the carrier of R is Element of bool the carrier of T
W9 is Element of the carrier of T
d is set
H is Element of the carrier of T
H is V14() real ext-real Element of REAL
Ball (H,H) is Element of bool the carrier of T
(Ball (H,H)) /\ the carrier of R is Element of bool the carrier of T
W99 is V14() real ext-real Element of REAL
Ball (W9,W99) is Element of bool the carrier of T
W9 is set
d is set
H is Element of the carrier of T
H is V14() real ext-real Element of REAL
Ball (H,H) is Element of bool the carrier of T
(Ball (H,H)) /\ the carrier of R is Element of bool the carrier of T
B2 is Element of bool the carrier of (TopSpaceMetr T)
B2 /\ ([#] (TopSpaceMetr R)) is Element of bool the carrier of (TopSpaceMetr R)
A is Element of bool the carrier of R
W9 is Element of the carrier of R
d is Element of the carrier of T
r is Element of bool the carrier of T
H is V14() real ext-real Element of REAL
Ball (d,H) is Element of bool the carrier of T
Ball (W9,H) is Element of bool the carrier of R
(Ball (d,H)) /\ the carrier of R is Element of bool the carrier of T
B2 /\ the carrier of R is Element of bool the carrier of (TopSpaceMetr T)
B2 /\ the carrier of (TopSpaceMetr R) is Element of bool the carrier of (TopSpaceMetr T)
T is V14() real ext-real set
R is triangle MetrStruct
the carrier of R is set
TopSpaceMetr R is strict TopSpace-like TopStruct
Family_open_set R is Element of bool (bool the carrier of R)
bool the carrier of R is non empty set
bool (bool the carrier of R) is non empty set
TopStruct(# the carrier of R,(Family_open_set R) #) is strict TopStruct
the carrier of (TopSpaceMetr R) is set
bool the carrier of (TopSpaceMetr R) is non empty set
x is Element of the carrier of R
Ball (x,T) is Element of bool the carrier of R
e is Element of bool the carrier of (TopSpaceMetr R)
T is non empty Reflexive discerning V122() triangle Discerning MetrStruct
TopSpaceMetr T is non empty strict TopSpace-like TopStruct
the carrier of T is non empty set
Family_open_set T is Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopStruct(# the carrier of T,(Family_open_set T) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr T) is non empty set
bool the carrier of (TopSpaceMetr T) is non empty set
R is Element of bool the carrier of (TopSpaceMetr T)
the topology of (TopSpaceMetr T) is non empty Element of bool (bool the carrier of (TopSpaceMetr T))
bool (bool the carrier of (TopSpaceMetr T)) is non empty set
x is Element of bool the carrier of T
e is Element of the carrier of T
B is V14() real ext-real Element of REAL
Ball (e,B) is Element of bool the carrier of T
e is Element of the carrier of T
B is V14() real ext-real set
Ball (e,B) is Element of bool the carrier of T
A is V14() real ext-real Element of REAL
Ball (e,A) is Element of bool the carrier of T
x is Element of bool the carrier of T
the topology of (TopSpaceMetr T) is non empty Element of bool (bool the carrier of (TopSpaceMetr T))
bool (bool the carrier of (TopSpaceMetr T)) is non empty set
T is non empty Reflexive discerning V122() triangle Discerning MetrStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
TopSpaceMetr T is non empty strict TopSpace-like TopStruct
Family_open_set T is Element of bool (bool the carrier of T)
TopStruct(# the carrier of T,(Family_open_set T) #) is non empty strict TopStruct
x is Element of bool (bool the carrier of T)
the carrier of (TopSpaceMetr T) is non empty set
bool the carrier of (TopSpaceMetr T) is non empty set
bool (bool the carrier of (TopSpaceMetr T)) is non empty set
e is Element of bool (bool the carrier of (TopSpaceMetr T))
B is Element of bool the carrier of (TopSpaceMetr T)
A is Element of bool the carrier of T
B2 is Element of the carrier of T
r is V14() real ext-real Element of REAL
Ball (B2,r) is Element of bool the carrier of T
union x is set
union e is set
B is Element of bool (bool the carrier of (TopSpaceMetr T))
A is Element of bool (bool the carrier of T)
union B is set
union A is set
TopSpaceMetr T is non empty strict TopSpace-like TopStruct
Family_open_set T is Element of bool (bool the carrier of T)
TopStruct(# the carrier of T,(Family_open_set T) #) is non empty strict TopStruct
the carrier of (TopSpaceMetr T) is non empty set
bool the carrier of (TopSpaceMetr T) is non empty set
bool (bool the carrier of (TopSpaceMetr T)) is non empty set
x is Element of bool (bool the carrier of (TopSpaceMetr T))
{ (Ball (b1,b2)) where b1 is Element of the carrier of T, b2 is V14() real ext-real Element of REAL : ex b3 being Element of bool the carrier of (TopSpaceMetr T) st
( b3 in x & Ball (b1,b2) c= b3 ) } is set
B is set
A is Element of the carrier of T
B2 is V14() real ext-real Element of REAL
Ball (A,B2) is Element of bool the carrier of T
r is Element of bool the carrier of (TopSpaceMetr T)
B is Element of bool (bool the carrier of T)
union B is set
A is set
union x is set
B2 is Element of the carrier of T
r is set
W9 is Element of bool the carrier of (TopSpaceMetr T)
d is V14() real ext-real set
Ball (B2,d) is Element of bool the carrier of T
H is V14() real ext-real Element of REAL
Ball (B2,H) is Element of bool the carrier of T
B2 is set
r is Element of the carrier of T
W9 is V14() real ext-real Element of REAL
Ball (r,W9) is Element of bool the carrier of T
d is Element of bool the carrier of (TopSpaceMetr T)
B2 is Element of bool (bool the carrier of T)
A is non empty Element of bool (bool the carrier of (TopSpaceMetr T))
r is set
W9 is Element of the carrier of T
d is V14() real ext-real Element of REAL
Ball (W9,d) is Element of bool the carrier of T
H is Element of bool the carrier of (TopSpaceMetr T)
H is Element of bool the carrier of (TopSpaceMetr T)
[:B2,A:] is set
bool [:B2,A:] is non empty set
r is Relation-like B2 -defined A -valued Function-like V36(B2,A) Element of bool [:B2,A:]
rng r is Element of bool A
bool A is non empty set
W9 is Element of bool (bool the carrier of (TopSpaceMetr T))
d is Element of bool (bool the carrier of (TopSpaceMetr T))
union d is set
union B2 is set
H is set
H is set
r . H is set
dom r is Element of bool B2
bool B2 is non empty set
dom r is Element of bool B2
bool B2 is non empty set
() is TopSpace-like TopStruct
the carrier of () is non empty set
T is V14() real ext-real set
R is V14() real ext-real set
(T,R) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )
TopSpaceMetr (T,R) is non empty strict TopSpace-like TopStruct
the carrier of (T,R) is non empty set
Family_open_set (T,R) is Element of bool (bool the carrier of (T,R))
bool the carrier of (T,R) is non empty set
bool (bool the carrier of (T,R)) is non empty set
TopStruct(# the carrier of (T,R),(Family_open_set (T,R)) #) is non empty strict TopStruct
T is V14() real ext-real set
R is V14() real ext-real set
(T,R) is non empty strict TopSpace-like SubSpace of ()
(T,R) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )
TopSpaceMetr (T,R) is non empty strict TopSpace-like TopStruct
the carrier of (T,R) is non empty set
Family_open_set (T,R) is Element of bool (bool the carrier of (T,R))
bool the carrier of (T,R) is non empty set
bool (bool the carrier of (T,R)) is non empty set
TopStruct(# the carrier of (T,R),(Family_open_set (T,R)) #) is non empty strict TopStruct
the carrier of (T,R) is non empty set
[.T,R.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL
bool the carrier of () is non empty set
T is V14() real ext-real set
R is V14() real ext-real set
[.T,R.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL
(T,R) is non empty strict TopSpace-like SubSpace of ()
(T,R) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )
TopSpaceMetr (T,R) is non empty strict TopSpace-like TopStruct
the carrier of (T,R) is non empty set
Family_open_set (T,R) is Element of bool (bool the carrier of (T,R))
bool the carrier of (T,R) is non empty set
bool (bool the carrier of (T,R)) is non empty set
TopStruct(# the carrier of (T,R),(Family_open_set (T,R)) #) is non empty strict TopStruct
x is Element of bool the carrier of ()
() | x is strict TopSpace-like SubSpace of ()
[#] (T,R) is non empty non proper open closed dense non boundary Element of bool the carrier of (T,R)
the carrier of (T,R) is non empty set
bool the carrier of (T,R) is non empty set
(0,1) is non empty strict TopSpace-like SubSpace of ()
(0,1) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )
TopSpaceMetr (0,1) is non empty strict TopSpace-like TopStruct
the carrier of (0,1) is non empty set
Family_open_set (0,1) is Element of bool (bool the carrier of (0,1))
bool the carrier of (0,1) is non empty set
bool (bool the carrier of (0,1)) is non empty set
TopStruct(# the carrier of (0,1),(Family_open_set (0,1)) #) is non empty strict TopStruct
T is Element of bool the carrier of ()
x is Element of bool the carrier of (TopSpaceMetr RealSpace)
(TopSpaceMetr RealSpace) | x is strict TopSpace-like SubSpace of TopSpaceMetr RealSpace
T is V14() real ext-real set
R is V14() real ext-real set
x is V14() real ext-real set
T + x is V14() real ext-real set
(T + x) - x is V14() real ext-real set
R - x is V14() real ext-real set
[: the carrier of (), the carrier of ():] is non empty set
bool [: the carrier of (), the carrier of ():] is non empty set
T is Relation-like the carrier of () -defined the carrier of () -valued Function-like V36( the carrier of (), the carrier of ()) Element of bool [: the carrier of (), the carrier of ():]
R is V14() real ext-real Element of REAL
x is V14() real ext-real Element of REAL
e is Element of the carrier of ()
T . e is Element of the carrier of ()
B is a_neighborhood of T . e
Int B is open Element of bool the carrier of ()
B2 is Element of bool the carrier of ()
A is Element of the carrier of RealSpace
r is V14() real ext-real set
Ball (A,r) is Element of bool the carrier of RealSpace
[#] () is non empty non proper open closed dense non boundary Element of bool the carrier of ()
Int ([#] ()) is open Element of bool the carrier of ()
{x} is non empty complex-membered ext-real-membered real-membered set
dom T is Element of bool the carrier of ()
d is a_neighborhood of e
H is set
T . 0 is set
0 * 0 is V14() real ext-real Element of REAL
(0 * 0) + x is V14() real ext-real Element of REAL
H is set
T . H is set
W99 is V14() real ext-real Element of REAL
0 * W99 is V14() real ext-real Element of REAL
(0 * W99) + x is V14() real ext-real Element of REAL
T .: d is Element of bool the carrier of ()
H is V14() real ext-real Element of REAL
0 * H is V14() real ext-real Element of REAL
(0 * H) + x is V14() real ext-real Element of REAL
abs R is V14() real ext-real Element of REAL
2 * (abs R) is V14() real ext-real Element of REAL
r / (2 * (abs R)) is V14() real ext-real Element of COMPLEX
W9 is Element of the carrier of RealSpace
Ball (W9,(r / (2 * (abs R)))) is Element of bool the carrier of RealSpace
H is Element of bool the carrier of ()
Int H is open Element of bool the carrier of ()
H is a_neighborhood of e
T .: H is Element of bool the carrier of ()
y is set
dom T is Element of bool the carrier of ()
x is set
T . x is set
x9 is Element of the carrier of RealSpace
y9 is V14() real ext-real Element of REAL
dist (W9,x9) is V14() real ext-real Element of REAL
the distance of RealSpace is Relation-like [: the carrier of RealSpace, the carrier of RealSpace:] -defined REAL -valued Function-like V36([: the carrier of RealSpace, the carrier of RealSpace:], REAL ) Element of bool [:[: the carrier of RealSpace, the carrier of RealSpace:],REAL:]
[: the carrier of RealSpace, the carrier of RealSpace:] is non empty set
[:[: the carrier of RealSpace, the carrier of RealSpace:],REAL:] is set
bool [:[: the carrier of RealSpace, the carrier of RealSpace:],REAL:] is non empty set
the distance of RealSpace . (W9,x9) is V14() real ext-real Element of REAL
[W9,x9] is set
{W9,x9} is non empty set
{W9} is non empty set
{{W9,x9},{W9}} is non empty set
the distance of RealSpace . [W9,x9] is set
W99 is V14() real ext-real Element of REAL
x99 is V14() real ext-real Element of REAL
W99 - x99 is V14() real ext-real Element of REAL
abs (W99 - x99) is V14() real ext-real Element of REAL
(abs R) * (r / (2 * (abs R))) is V14() real ext-real Element of REAL
(abs R) * (abs (W99 - x99)) is V14() real ext-real Element of REAL
R * (W99 - x99) is V14() real ext-real Element of REAL
abs (R * (W99 - x99)) is V14() real ext-real Element of REAL
R * W99 is V14() real ext-real Element of REAL
(R * W99) + x is V14() real ext-real Element of REAL
R * x99 is V14() real ext-real Element of REAL
(R * x99) + x is V14() real ext-real Element of REAL
((R * W99) + x) - ((R * x99) + x) is V14() real ext-real Element of REAL
abs (((R * W99) + x) - ((R * x99) + x)) is V14() real ext-real Element of REAL
Y9 is V14() real ext-real Element of REAL
Y9 - ((R * x99) + x) is V14() real ext-real Element of REAL
abs (Y9 - ((R * x99) + x)) is V14() real ext-real Element of REAL
Y9 - y9 is V14() real ext-real Element of REAL
abs (Y9 - y9) is V14() real ext-real Element of REAL
r / 2 is V14() real ext-real Element of COMPLEX
(r / 2) + (r / 2) is V14() real ext-real Element of COMPLEX
yy is Element of the carrier of RealSpace
dist (A,yy) is V14() real ext-real Element of REAL
the distance of RealSpace . (A,yy) is V14() real ext-real Element of REAL
[A,yy] is set
{A,yy} is non empty set
{A} is non empty set
{{A,yy},{A}} is non empty set
the distance of RealSpace . [A,yy] is set
W9 is a_neighborhood of e
T .: W9 is Element of bool the carrier of ()
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
R is Element of bool the carrier of T
x is Element of bool the carrier of T
T | R is strict TopSpace-like SubSpace of T
T | x is strict TopSpace-like SubSpace of T
R \/ x is Element of bool the carrier of T
x is V14() real ext-real set
e is V14() real ext-real set
(x,e) is non empty strict TopSpace-like SubSpace of ()
(x,e) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )
TopSpaceMetr (x,e) is non empty strict TopSpace-like TopStruct
the carrier of (x,e) is non empty set
Family_open_set (x,e) is Element of bool (bool the carrier of (x,e))
bool the carrier of (x,e) is non empty set
bool (bool the carrier of (x,e)) is non empty set
TopStruct(# the carrier of (x,e),(Family_open_set (x,e)) #) is non empty strict TopStruct
the carrier of (x,e) is non empty set
bool the carrier of (x,e) is non empty set
T is V14() real ext-real set
R is V14() real ext-real set
[.T,R.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL
(T,R) is non empty strict TopSpace-like SubSpace of ()
(T,R) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )
TopSpaceMetr (T,R) is non empty strict TopSpace-like TopStruct
the carrier of (T,R) is non empty set
Family_open_set (T,R) is Element of bool (bool the carrier of (T,R))
bool the carrier of (T,R) is non empty set
bool (bool the carrier of (T,R)) is non empty set
TopStruct(# the carrier of (T,R),(Family_open_set (T,R)) #) is non empty strict TopStruct
B is Element of bool the carrier of (x,e)
(x,e) | B is strict TopSpace-like SubSpace of (x,e)
[.x,e.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL
B2 is non empty Element of bool the carrier of ()
() | B2 is non empty strict TopSpace-like SubSpace of ()
A is non empty Element of bool the carrier of ()
() | A is non empty strict TopSpace-like SubSpace of ()
() is non empty strict TopSpace-like SubSpace of ()
the carrier of () is non empty set
bool the carrier of () is non empty set
T is V14() real ext-real set
R is V14() real ext-real set
x is Element of bool the carrier of ()
[.T,R.] is complex-membered ext-real-membered real-membered V111() Element of bool REAL
(T,R) is non empty strict TopSpace-like SubSpace of ()
(T,R) is non empty strict Reflexive discerning V122() triangle Discerning ( RealSpace )
TopSpaceMetr (T,R) is non empty strict TopSpace-like TopStruct
the carrier of (T,R) is non empty set
Family_open_set (T,R) is Element of bool (bool the carrier of (T,R))
bool the carrier of (T,R) is non empty set
bool (bool the carrier of (T,R)) is non empty set
TopStruct(# the carrier of (T,R),(Family_open_set (T,R)) #) is non empty strict TopStruct
() | x is strict TopSpace-like SubSpace of ()
T is () 1-sorted
the carrier of T is set
T is set
T is () TopStruct
R is SubSpace of T
x is set
the carrier of R is set
the carrier of T is complex-membered ext-real-membered real-membered set