NAT is V45() V46() V47() V48() V49() V50() V51() Element of K6(REAL)
REAL is non empty V45() V46() V47() V51() V52() set
K6(REAL) is non empty set
COMPLEX is non empty V45() V51() V52() set
RAT is non empty V45() V46() V47() V48() V51() V52() set
INT is non empty V45() V46() V47() V48() V49() V51() V52() set
omega is V45() V46() V47() V48() V49() V50() V51() set
K6(omega) is non empty set
K6(NAT) is non empty set
K7(COMPLEX,COMPLEX) is non empty V33() set
K6(K7(COMPLEX,COMPLEX)) is non empty set
K7(COMPLEX,REAL) is non empty V33() V34() V35() set
K6(K7(COMPLEX,REAL)) is non empty set
1 is non empty set
K7(1,1) is non empty set
K6(K7(1,1)) is non empty set
K7(K7(1,1),1) is non empty set
K6(K7(K7(1,1),1)) is non empty set
K7(K7(1,1),REAL) is non empty V33() V34() V35() set
K6(K7(K7(1,1),REAL)) is non empty set
K7(REAL,REAL) is non empty V33() V34() V35() set
K7(K7(REAL,REAL),REAL) is non empty V33() V34() V35() set
K6(K7(K7(REAL,REAL),REAL)) is non empty set
2 is non empty set
K7(2,2) is non empty set
K7(K7(2,2),REAL) is non empty V33() V34() V35() set
K6(K7(K7(2,2),REAL)) is non empty set
K391() is T_0 T_1 T_2 compact V147() TopStruct
the carrier of K391() is V45() V46() V47() set
RealSpace is strict V147() MetrStruct
R^1 is non empty strict TopSpace-like V147() TopStruct
the carrier of R^1 is non empty V45() V46() V47() set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty V33() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K6(K7(REAL,REAL)) is non empty set
K7(RAT,RAT) is non empty V20( RAT ) V33() V34() V35() set
K6(K7(RAT,RAT)) is non empty set
K7(K7(RAT,RAT),RAT) is non empty V20( RAT ) V33() V34() V35() set
K6(K7(K7(RAT,RAT),RAT)) is non empty set
K7(INT,INT) is non empty V20( RAT ) V20( INT ) V33() V34() V35() set
K6(K7(INT,INT)) is non empty set
K7(K7(INT,INT),INT) is non empty V20( RAT ) V20( INT ) V33() V34() V35() set
K6(K7(K7(INT,INT),INT)) is non empty set
K7(NAT,NAT) is V20( RAT ) V20( INT ) V33() V34() V35() V36() set
K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) V33() V34() V35() V36() set
K6(K7(K7(NAT,NAT),NAT)) is non empty set
TOP-REAL 2 is V204() L16()
the carrier of (TOP-REAL 2) is set
K7( the carrier of (TOP-REAL 2),REAL) is V33() V34() V35() set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is non empty set
K6( the carrier of (TOP-REAL 2)) is non empty set
{} is set
the empty V45() V46() V47() V48() V49() V50() V51() set is empty V45() V46() V47() V48() V49() V50() V51() set
0 is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
K6( the carrier of R^1) is non empty set
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like TopStruct
n is V11() real ext-real set
P is V11() real ext-real set
max (n,P) is V11() real ext-real set
n is non empty Reflexive discerning V117() triangle MetrStruct
the carrier of n is non empty set
P is Element of the carrier of n
dist P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
(dist P) . P is V11() real ext-real set
dist (P,P) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is Element of K6( the carrier of (TopSpaceMetr n))
Q is Element of the carrier of n
dist Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
(dist Q) .: P is V45() V46() V47() Element of K6( the carrier of R^1)
dom (dist Q) is Element of K6( the carrier of (TopSpaceMetr n))
(dist Q) . Q is V11() real ext-real set
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is Element of K6( the carrier of (TopSpaceMetr n))
Q is Element of the carrier of n
dist Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
(dist Q) .: P is V45() V46() V47() Element of K6( the carrier of R^1)
R is V11() real ext-real set
dom (dist Q) is Element of K6( the carrier of (TopSpaceMetr n))
P1 is set
(dist Q) . P1 is V11() real ext-real set
Q1 is Element of the carrier of n
dist (Q,Q1) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is Element of K6( the carrier of (TopSpaceMetr n))
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
Q is set
(dist_min P) . Q is V11() real ext-real set
the carrier of n is non empty set
R is Element of the carrier of n
dist R is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
(dist R) .: P is V45() V46() V47() Element of K6( the carrier of R^1)
lower_bound ((dist R) .: P) is V11() real ext-real Element of REAL
[#] ((dist R) .: P) is V45() V46() V47() Element of K6(REAL)
lower_bound ([#] ((dist R) .: P)) is V11() real ext-real Element of REAL
Q1 is non empty V45() V46() V47() Element of K6(REAL)
lower_bound Q1 is V11() real ext-real Element of REAL
(dist_min P) . R is V11() real ext-real set
R1 is V11() real ext-real set
R1 is V11() real ext-real set
n is non empty Reflexive discerning V117() triangle MetrStruct
the carrier of n is non empty set
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is Element of the carrier of n
Q is Element of K6( the carrier of (TopSpaceMetr n))
Cl Q is Element of K6( the carrier of (TopSpaceMetr n))
R is V11() real ext-real set
Ball (P,R) is bounded Element of K6( the carrier of n)
K6( the carrier of n) is non empty set
P1 is set
Q1 is Element of the carrier of n
R1 is Element of the carrier of n
dist (P,R1) is V11() real ext-real Element of REAL
R is V11() real ext-real set
Ball (P,R) is bounded Element of K6( the carrier of n)
P1 is Element of the carrier of n
dist (P,P1) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
Q is Element of the carrier of n
(dist_min P) . Q is V11() real ext-real set
dist Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
(dist Q) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)
P1 is V11() real ext-real set
R is non empty V45() V46() V47() Element of K6(REAL)
Q1 is V11() real ext-real set
dom (dist Q) is Element of K6( the carrier of (TopSpaceMetr n))
R1 is set
(dist Q) . R1 is V11() real ext-real set
y is Element of the carrier of n
dist (Q,y) is V11() real ext-real Element of REAL
lower_bound R is V11() real ext-real Element of REAL
lower_bound ((dist Q) .: P) is V11() real ext-real Element of REAL
[#] ((dist Q) .: P) is V45() V46() V47() Element of K6(REAL)
lower_bound ([#] ((dist Q) .: P)) is V11() real ext-real Element of REAL
P1 is V11() real ext-real set
dom (dist Q) is Element of K6( the carrier of (TopSpaceMetr n))
Q1 is set
(dist Q) . Q1 is V11() real ext-real set
R1 is Element of the carrier of n
dist (Q,R1) is V11() real ext-real Element of REAL
P1 is V11() real ext-real set
Q1 is Element of the carrier of n
dist (Q,Q1) is V11() real ext-real Element of REAL
(dist Q) . Q1 is V11() real ext-real set
dom (dist Q) is Element of K6( the carrier of (TopSpaceMetr n))
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
Cl P is Element of K6( the carrier of (TopSpaceMetr n))
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
Q is Element of the carrier of n
(dist_min P) . Q is V11() real ext-real set
R is V11() real ext-real set
R is V11() real ext-real set
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty closed Element of K6( the carrier of (TopSpaceMetr n))
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
Q is Element of the carrier of n
(dist_min P) . Q is V11() real ext-real set
Cl P is Element of K6( the carrier of (TopSpaceMetr n))
n is non empty V45() V46() V47() Element of K6( the carrier of R^1)
lower_bound n is V11() real ext-real Element of REAL
P is non empty V45() V46() V47() Element of K6(REAL)
lower_bound P is V11() real ext-real Element of REAL
[#] n is V45() V46() V47() Element of K6(REAL)
lower_bound ([#] n) is V11() real ext-real Element of REAL
n is non empty V45() V46() V47() Element of K6( the carrier of R^1)
upper_bound n is V11() real ext-real Element of REAL
P is non empty V45() V46() V47() Element of K6(REAL)
upper_bound P is V11() real ext-real Element of REAL
[#] n is V45() V46() V47() Element of K6(REAL)
upper_bound ([#] n) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
Q is Element of the carrier of n
dist Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
(dist Q) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)
R is V45() V46() V47() Element of K6(REAL)
P1 is ext-real set
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
R is Element of the carrier of n
Q is Element of the carrier of n
(dist_min P) . Q is V11() real ext-real set
dist (Q,R) is V11() real ext-real Element of REAL
dist Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
dom (dist Q) is Element of K6( the carrier of (TopSpaceMetr n))
(dist Q) . R is V11() real ext-real set
(dist Q) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)
lower_bound ((dist Q) .: P) is V11() real ext-real Element of REAL
P1 is non empty V45() V46() V47() Element of K6(REAL)
lower_bound P1 is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
Q is V11() real ext-real set
R is Element of the carrier of n
(dist_min P) . R is V11() real ext-real set
dist R is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
(dist R) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)
lower_bound ((dist R) .: P) is V11() real ext-real Element of REAL
P1 is non empty V45() V46() V47() Element of K6(REAL)
lower_bound P1 is V11() real ext-real Element of REAL
Q1 is V11() real ext-real set
dom (dist R) is Element of K6( the carrier of (TopSpaceMetr n))
R1 is set
(dist R) . R1 is V11() real ext-real set
y is Element of the carrier of n
dist (R,y) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
Q is Element of the carrier of n
(dist_min P) . Q is V11() real ext-real set
R is Element of the carrier of n
dist (Q,R) is V11() real ext-real Element of REAL
(dist_min P) . R is V11() real ext-real set
(dist (Q,R)) + ((dist_min P) . R) is V11() real ext-real Element of REAL
P1 is Element of the carrier of n
dist (Q,P1) is V11() real ext-real Element of REAL
((dist_min P) . Q) - (dist (Q,R)) is V11() real ext-real Element of REAL
(dist (Q,P1)) - (dist (Q,R)) is V11() real ext-real Element of REAL
dist (R,P1) is V11() real ext-real Element of REAL
(dist (Q,R)) + (dist (R,P1)) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
K6( the carrier of n) is non empty set
P is Element of K6( the carrier of (TopSpaceMetr n))
(TopSpaceMetr n) | P is strict TopSpace-like SubSpace of TopSpaceMetr n
Q is non empty Element of K6( the carrier of n)
n | Q is non empty strict Reflexive discerning V117() triangle SubSpace of n
TopSpaceMetr (n | Q) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
R is TopSpace-like SubSpace of TopSpaceMetr n
the carrier of R is set
the carrier of (n | Q) is non empty set
[#] R is non proper closed Element of K6( the carrier of R)
K6( the carrier of R) is non empty set
n is non empty Reflexive discerning V117() triangle MetrStruct
the carrier of n is non empty set
K6( the carrier of n) is non empty set
P is Element of K6( the carrier of n)
Q is non empty Element of K6( the carrier of n)
n | Q is non empty strict Reflexive discerning V117() triangle SubSpace of n
the carrier of (n | Q) is non empty set
K6( the carrier of (n | Q)) is non empty set
R is Element of K6( the carrier of (n | Q))
P1 is V11() real ext-real Element of REAL
Q1 is Element of the carrier of n
R1 is Element of the carrier of n
dist (Q1,R1) is V11() real ext-real Element of REAL
the distance of (n | Q) is V16() V19(K7( the carrier of (n | Q), the carrier of (n | Q))) V20( REAL ) Function-like V30(K7( the carrier of (n | Q), the carrier of (n | Q)), REAL ) V33() V34() V35() Element of K6(K7(K7( the carrier of (n | Q), the carrier of (n | Q)),REAL))
K7( the carrier of (n | Q), the carrier of (n | Q)) is non empty set
K7(K7( the carrier of (n | Q), the carrier of (n | Q)),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of (n | Q), the carrier of (n | Q)),REAL)) is non empty set
y is Element of the carrier of (n | Q)
z is Element of the carrier of (n | Q)
the distance of (n | Q) . (y,z) is V11() real ext-real Element of REAL
the distance of n is V16() V19(K7( the carrier of n, the carrier of n)) V20( REAL ) Function-like V30(K7( the carrier of n, the carrier of n), REAL ) V33() V34() V35() Element of K6(K7(K7( the carrier of n, the carrier of n),REAL))
K7( the carrier of n, the carrier of n) is non empty set
K7(K7( the carrier of n, the carrier of n),REAL) is non empty V33() V34() V35() set
K6(K7(K7( the carrier of n, the carrier of n),REAL)) is non empty set
the distance of n . (Q1,R1) is V11() real ext-real Element of REAL
dist (y,z) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
the carrier of n is non empty set
K6( the carrier of n) is non empty set
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is Element of K6( the carrier of n)
Q is Element of K6( the carrier of (TopSpaceMetr n))
(TopSpaceMetr n) | Q is strict TopSpace-like SubSpace of TopSpaceMetr n
the carrier of ((TopSpaceMetr n) | Q) is set
K6( the carrier of ((TopSpaceMetr n) | Q)) is non empty set
[#] ((TopSpaceMetr n) | Q) is non proper closed Element of K6( the carrier of ((TopSpaceMetr n) | Q))
P1 is Element of K6( the carrier of ((TopSpaceMetr n) | Q))
Q1 is non empty Element of K6( the carrier of n)
n | Q1 is non empty strict Reflexive discerning V117() triangle SubSpace of n
TopSpaceMetr (n | Q1) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
[#] (n | Q1) is non empty non proper Element of K6( the carrier of (n | Q1))
the carrier of (n | Q1) is non empty set
K6( the carrier of (n | Q1)) is non empty set
{} n is empty proper V45() V46() V47() V48() V49() V50() V51() bounded Element of K6( the carrier of n)
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
Q is Element of the carrier of n
(dist_min P) . Q is V11() real ext-real set
R is set
P1 is Element of the carrier of n
dist (P1,Q) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
the carrier of n is non empty set
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
P is Element of the carrier of n
dist P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
the carrier of (TopSpaceMetr n) is non empty set
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is non empty compact Element of K6( the carrier of (TopSpaceMetr n))
dist_max P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
Q is Element of the carrier of n
dist Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() continuous Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
(dist Q) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)
R is V45() V46() V47() Element of K6(REAL)
[#] ((dist Q) .: P) is V45() V46() V47() Element of K6(REAL)
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_max P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
R is Element of the carrier of n
Q is Element of the carrier of n
dist (Q,R) is V11() real ext-real Element of REAL
(dist_max P) . Q is V11() real ext-real set
dist Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() continuous Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
(dist Q) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)
upper_bound ((dist Q) .: P) is V11() real ext-real Element of REAL
P1 is non empty V45() V46() V47() Element of K6(REAL)
upper_bound P1 is V11() real ext-real Element of REAL
dom (dist Q) is Element of K6( the carrier of (TopSpaceMetr n))
(dist Q) . R is V11() real ext-real set
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_max P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
Q is Element of the carrier of n
(dist_max P) . Q is V11() real ext-real set
R is set
P1 is Element of the carrier of n
dist (P1,Q) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
Q is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
max_dist_max (P,Q) is V11() real ext-real Element of REAL
R is Element of the carrier of n
(dist_min P) . R is V11() real ext-real set
P1 is Element of the carrier of n
dist (P1,R) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
Q is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_max P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
max_dist_max (P,Q) is V11() real ext-real Element of REAL
R is Element of the carrier of n
(dist_max P) . R is V11() real ext-real set
P1 is non empty compact Element of K6( the carrier of (TopSpaceMetr n))
dist_max P1 is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() continuous Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
(dist_max P1) .: Q is non empty V45() V46() V47() Element of K6( the carrier of R^1)
dom (dist_max P1) is Element of K6( the carrier of (TopSpaceMetr n))
(dist_max P1) . R is V11() real ext-real set
upper_bound ((dist_max P1) .: Q) is V11() real ext-real Element of REAL
max_dist_max (P1,Q) is V11() real ext-real Element of REAL
R1 is non empty V45() V46() V47() Element of K6(REAL)
upper_bound R1 is V11() real ext-real Element of REAL
[#] ((dist_max P1) .: Q) is V45() V46() V47() Element of K6(REAL)
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_max P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
Q is non empty Element of K6( the carrier of (TopSpaceMetr n))
(dist_max P) .: Q is non empty V45() V46() V47() Element of K6( the carrier of R^1)
R is V45() V46() V47() Element of K6(REAL)
the carrier of n is non empty set
K6( the carrier of n) is non empty set
max_dist_max (P,Q) is V11() real ext-real Element of REAL
Q1 is V11() real ext-real Element of REAL
R1 is ext-real set
dom (dist_max P) is Element of K6( the carrier of (TopSpaceMetr n))
y is set
(dist_max P) . y is V11() real ext-real set
P1 is non empty Element of K6( the carrier of n)
z is Element of the carrier of n
(dist_max P) . z is V11() real ext-real set
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
Q is non empty Element of K6( the carrier of (TopSpaceMetr n))
(dist_min P) .: Q is non empty V45() V46() V47() Element of K6( the carrier of R^1)
R is V45() V46() V47() Element of K6(REAL)
the carrier of n is non empty set
K6( the carrier of n) is non empty set
max_dist_max (P,Q) is V11() real ext-real Element of REAL
Q1 is V11() real ext-real Element of REAL
R1 is ext-real set
dom (dist_min P) is Element of K6( the carrier of (TopSpaceMetr n))
y is set
(dist_min P) . y is V11() real ext-real set
P1 is non empty Element of K6( the carrier of n)
z is Element of the carrier of n
(dist_min P) . z is V11() real ext-real set
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
dist_max P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
Q is Element of the carrier of n
(dist_min P) . Q is V11() real ext-real set
(dist_max P) . Q is V11() real ext-real set
R is Element of the carrier of n
dist (R,Q) is V11() real ext-real Element of REAL
dist (Q,R) is V11() real ext-real Element of REAL
{0} is V45() V46() V47() V48() V49() V50() Element of K6(REAL)
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
(dist_min P) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)
Q is set
R is set
dom (dist_min P) is Element of K6( the carrier of (TopSpaceMetr n))
P1 is set
(dist_min P) . P1 is V11() real ext-real set
R is set
dom (dist_min P) is Element of K6( the carrier of (TopSpaceMetr n))
(dist_min P) . Q is V11() real ext-real set
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
Q is non empty Element of K6( the carrier of (TopSpaceMetr n))
max_dist_min (P,Q) is V11() real ext-real Element of REAL
the carrier of n is non empty set
R is Element of the carrier of n
P1 is Element of the carrier of n
dist (R,P1) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
max_dist_min (P,P) is V11() real ext-real Element of REAL
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
(dist_min P) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)
[#] ((dist_min P) .: P) is V45() V46() V47() Element of K6(REAL)
upper_bound ((dist_min P) .: P) is V11() real ext-real Element of REAL
upper_bound {0} is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
Q is non empty Element of K6( the carrier of (TopSpaceMetr n))
min_dist_max (P,Q) is V11() real ext-real Element of REAL
the carrier of n is non empty set
R is Element of the carrier of n
P1 is Element of the carrier of n
dist (R,P1) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
Q is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_min Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
max_dist_min (Q,P) is V11() real ext-real Element of REAL
R is Element of the carrier of n
(dist_min Q) . R is V11() real ext-real set
(dist_min Q) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)
upper_bound ((dist_min Q) .: P) is V11() real ext-real Element of REAL
Q1 is non empty V45() V46() V47() Element of K6(REAL)
upper_bound Q1 is V11() real ext-real Element of REAL
dom (dist_min Q) is Element of K6( the carrier of (TopSpaceMetr n))
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is Element of K6( the carrier of (TopSpaceMetr n))
Q is Element of K6( the carrier of (TopSpaceMetr n))
max_dist_min (P,Q) is V11() real ext-real Element of REAL
max_dist_min (Q,P) is V11() real ext-real Element of REAL
max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is V11() real ext-real Element of REAL
R is V11() real ext-real Element of REAL
P1 is Element of K6( the carrier of (TopSpaceMetr n))
Q1 is Element of K6( the carrier of (TopSpaceMetr n))
max_dist_min (P1,Q1) is V11() real ext-real Element of REAL
max_dist_min (Q1,P1) is V11() real ext-real Element of REAL
max ((max_dist_min (P1,Q1)),(max_dist_min (Q1,P1))) is V11() real ext-real Element of REAL
max ((max_dist_min (Q1,P1)),(max_dist_min (P1,Q1))) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
the carrier of n is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
Q is non empty Element of K6( the carrier of (TopSpaceMetr n))
dist_min Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
(n,P,Q) is V11() real ext-real Element of REAL
max_dist_min (P,Q) is V11() real ext-real Element of REAL
max_dist_min (Q,P) is V11() real ext-real Element of REAL
max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is V11() real ext-real Element of REAL
R is Element of the carrier of n
(dist_min Q) . R is V11() real ext-real set
max ((max_dist_min (Q,P)),(max_dist_min (P,Q))) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
Q is non empty Element of K6( the carrier of (TopSpaceMetr n))
R is non empty Element of K6( the carrier of (TopSpaceMetr n))
max_dist_min (P,R) is V11() real ext-real Element of REAL
(n,P,Q) is V11() real ext-real Element of REAL
max_dist_min (P,Q) is V11() real ext-real Element of REAL
max_dist_min (Q,P) is V11() real ext-real Element of REAL
max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is V11() real ext-real Element of REAL
(n,Q,R) is V11() real ext-real Element of REAL
max_dist_min (Q,R) is V11() real ext-real Element of REAL
max_dist_min (R,Q) is V11() real ext-real Element of REAL
max ((max_dist_min (Q,R)),(max_dist_min (R,Q))) is V11() real ext-real Element of REAL
(n,P,Q) + (n,Q,R) is V11() real ext-real Element of REAL
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
(dist_min P) .: R is non empty V45() V46() V47() Element of K6( the carrier of R^1)
P1 is non empty V45() V46() V47() Element of K6(REAL)
Q1 is V11() real ext-real set
dom (dist_min P) is Element of K6( the carrier of (TopSpaceMetr n))
R1 is set
(dist_min P) . R1 is V11() real ext-real set
the carrier of n is non empty set
y is Element of the carrier of n
(dist_min P) . y is V11() real ext-real set
(n,Q,P) is V11() real ext-real Element of REAL
max ((max_dist_min (Q,P)),(max_dist_min (P,Q))) is V11() real ext-real Element of REAL
((dist_min P) . y) - (n,Q,P) is V11() real ext-real Element of REAL
z is Element of the carrier of n
dist (y,z) is V11() real ext-real Element of REAL
(dist_min P) . z is V11() real ext-real set
(dist (y,z)) + ((dist_min P) . z) is V11() real ext-real Element of REAL
(dist (y,z)) + (n,Q,P) is V11() real ext-real Element of REAL
dist_min Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
(dist_min Q) . y is V11() real ext-real set
(n,Q,P) + ((dist_min Q) . y) is V11() real ext-real Element of REAL
(n,R,Q) is V11() real ext-real Element of REAL
max ((max_dist_min (R,Q)),(max_dist_min (Q,R))) is V11() real ext-real Element of REAL
(n,Q,P) + (n,Q,R) is V11() real ext-real Element of REAL
upper_bound P1 is V11() real ext-real Element of REAL
[#] ((dist_min P) .: R) is V45() V46() V47() Element of K6(REAL)
upper_bound ([#] ((dist_min P) .: R)) is V11() real ext-real Element of REAL
upper_bound ((dist_min P) .: R) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
Q is non empty Element of K6( the carrier of (TopSpaceMetr n))
R is non empty Element of K6( the carrier of (TopSpaceMetr n))
max_dist_min (R,P) is V11() real ext-real Element of REAL
(n,P,Q) is V11() real ext-real Element of REAL
max_dist_min (P,Q) is V11() real ext-real Element of REAL
max_dist_min (Q,P) is V11() real ext-real Element of REAL
max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is V11() real ext-real Element of REAL
(n,Q,R) is V11() real ext-real Element of REAL
max_dist_min (Q,R) is V11() real ext-real Element of REAL
max_dist_min (R,Q) is V11() real ext-real Element of REAL
max ((max_dist_min (Q,R)),(max_dist_min (R,Q))) is V11() real ext-real Element of REAL
(n,P,Q) + (n,Q,R) is V11() real ext-real Element of REAL
dist_min R is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
(dist_min R) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)
P1 is non empty V45() V46() V47() Element of K6(REAL)
Q1 is V11() real ext-real set
dom (dist_min R) is Element of K6( the carrier of (TopSpaceMetr n))
R1 is set
(dist_min R) . R1 is V11() real ext-real set
the carrier of n is non empty set
y is Element of the carrier of n
(dist_min R) . y is V11() real ext-real set
((dist_min R) . y) - (n,Q,R) is V11() real ext-real Element of REAL
z is Element of the carrier of n
dist (y,z) is V11() real ext-real Element of REAL
(dist_min R) . z is V11() real ext-real set
(dist (y,z)) + ((dist_min R) . z) is V11() real ext-real Element of REAL
(dist (y,z)) + (n,Q,R) is V11() real ext-real Element of REAL
dist_min Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
(dist_min Q) . y is V11() real ext-real set
upper_bound P1 is V11() real ext-real Element of REAL
[#] ((dist_min R) .: P) is V45() V46() V47() Element of K6(REAL)
upper_bound ([#] ((dist_min R) .: P)) is V11() real ext-real Element of REAL
upper_bound ((dist_min R) .: P) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
Q is non empty Element of K6( the carrier of (TopSpaceMetr n))
(n,P,Q) is V11() real ext-real Element of REAL
max_dist_min (P,Q) is V11() real ext-real Element of REAL
max_dist_min (Q,P) is V11() real ext-real Element of REAL
max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
(n,P,P) is V11() real ext-real Element of REAL
max_dist_min (P,P) is V11() real ext-real Element of REAL
max ((max_dist_min (P,P)),(max_dist_min (P,P))) is V11() real ext-real Element of REAL
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
Q is non empty Element of K6( the carrier of (TopSpaceMetr n))
(n,P,Q) is V11() real ext-real Element of REAL
max_dist_min (P,Q) is V11() real ext-real Element of REAL
max_dist_min (Q,P) is V11() real ext-real Element of REAL
max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is V11() real ext-real Element of REAL
dist_min Q is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
K7( the carrier of (TopSpaceMetr n), the carrier of R^1) is non empty V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1)) is non empty set
(dist_min Q) .: P is non empty V45() V46() V47() Element of K6( the carrier of R^1)
upper_bound ((dist_min Q) .: P) is V11() real ext-real Element of REAL
R is non empty V45() V46() V47() Element of K6(REAL)
upper_bound R is V11() real ext-real Element of REAL
P1 is set
the carrier of n is non empty set
dom (dist_min Q) is Element of K6( the carrier of (TopSpaceMetr n))
(dist_min Q) . P1 is V11() real ext-real set
Q1 is Element of the carrier of n
P1 is set
the carrier of n is non empty set
dist_min P is V16() V19( the carrier of (TopSpaceMetr n)) V20( the carrier of R^1) Function-like V30( the carrier of (TopSpaceMetr n), the carrier of R^1) V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr n), the carrier of R^1))
(dist_min P) .: Q is non empty V45() V46() V47() Element of K6( the carrier of R^1)
upper_bound ((dist_min P) .: Q) is V11() real ext-real Element of REAL
R1 is non empty V45() V46() V47() Element of K6(REAL)
upper_bound R1 is V11() real ext-real Element of REAL
dom (dist_min P) is Element of K6( the carrier of (TopSpaceMetr n))
(dist_min P) . P1 is V11() real ext-real set
Q1 is Element of the carrier of n
n is non empty Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr n is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr n) is non empty set
K6( the carrier of (TopSpaceMetr n)) is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr n))
Q is non empty Element of K6( the carrier of (TopSpaceMetr n))
R is non empty Element of K6( the carrier of (TopSpaceMetr n))
(n,P,R) is V11() real ext-real Element of REAL
max_dist_min (P,R) is V11() real ext-real Element of REAL
max_dist_min (R,P) is V11() real ext-real Element of REAL
max ((max_dist_min (P,R)),(max_dist_min (R,P))) is V11() real ext-real Element of REAL
(n,P,Q) is V11() real ext-real Element of REAL
max_dist_min (P,Q) is V11() real ext-real Element of REAL
max_dist_min (Q,P) is V11() real ext-real Element of REAL
max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is V11() real ext-real Element of REAL
(n,Q,R) is V11() real ext-real Element of REAL
max_dist_min (Q,R) is V11() real ext-real Element of REAL
max_dist_min (R,Q) is V11() real ext-real Element of REAL
max ((max_dist_min (Q,R)),(max_dist_min (R,Q))) is V11() real ext-real Element of REAL
(n,P,Q) + (n,Q,R) is V11() real ext-real Element of REAL
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL n is non empty TopSpace-like V165() V190() V191() V192() V193() V194() V195() V196() V204() L16()
the carrier of (TOP-REAL n) is non empty set
K6( the carrier of (TOP-REAL n)) is non empty set
Euclid n is non empty strict Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid n))) is non empty set
P is Element of K6( the carrier of (TOP-REAL n))
Q is Element of K6( the carrier of (TOP-REAL n))
the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))
K6(K6( the carrier of (TOP-REAL n))) is non empty set
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct
R is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
P1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
max_dist_min (R,P1) is V11() real ext-real Element of REAL
Q1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
R1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
R is V11() real ext-real Element of REAL
max_dist_min (Q1,R1) is V11() real ext-real Element of REAL
y is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
z is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
P1 is V11() real ext-real Element of REAL
max_dist_min (y,z) is V11() real ext-real Element of REAL
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL n is non empty TopSpace-like V165() V190() V191() V192() V193() V194() V195() V196() V204() L16()
the carrier of (TOP-REAL n) is non empty set
K6( the carrier of (TOP-REAL n)) is non empty set
Euclid n is non empty strict Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid n))) is non empty set
P is Element of K6( the carrier of (TOP-REAL n))
Q is Element of K6( the carrier of (TOP-REAL n))
the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))
K6(K6( the carrier of (TOP-REAL n))) is non empty set
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct
R is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
P1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
((Euclid n),R,P1) is V11() real ext-real Element of REAL
max_dist_min (R,P1) is V11() real ext-real Element of REAL
max_dist_min (P1,R) is V11() real ext-real Element of REAL
max ((max_dist_min (R,P1)),(max_dist_min (P1,R))) is V11() real ext-real Element of REAL
Q1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
R1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
R is V11() real ext-real Element of REAL
((Euclid n),Q1,R1) is V11() real ext-real Element of REAL
max_dist_min (Q1,R1) is V11() real ext-real Element of REAL
max_dist_min (R1,Q1) is V11() real ext-real Element of REAL
max ((max_dist_min (Q1,R1)),(max_dist_min (R1,Q1))) is V11() real ext-real Element of REAL
y is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
z is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
P1 is V11() real ext-real Element of REAL
((Euclid n),y,z) is V11() real ext-real Element of REAL
max_dist_min (y,z) is V11() real ext-real Element of REAL
max_dist_min (z,y) is V11() real ext-real Element of REAL
max ((max_dist_min (y,z)),(max_dist_min (z,y))) is V11() real ext-real Element of REAL
P1 is Element of K6( the carrier of (TOP-REAL n))
R1 is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
Q1 is Element of K6( the carrier of (TOP-REAL n))
y is Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
R is V11() real ext-real Element of REAL
((Euclid n),R1,y) is V11() real ext-real Element of REAL
max_dist_min (R1,y) is V11() real ext-real Element of REAL
max_dist_min (y,R1) is V11() real ext-real Element of REAL
max ((max_dist_min (R1,y)),(max_dist_min (y,R1))) is V11() real ext-real Element of REAL
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL n is non empty TopSpace-like V165() V190() V191() V192() V193() V194() V195() V196() V204() L16()
the carrier of (TOP-REAL n) is non empty set
K6( the carrier of (TOP-REAL n)) is non empty set
P is non empty Element of K6( the carrier of (TOP-REAL n))
Q is non empty Element of K6( the carrier of (TOP-REAL n))
(n,P,Q) is V11() real ext-real Element of REAL
the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))
K6(K6( the carrier of (TOP-REAL n))) is non empty set
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct
Euclid n is non empty strict Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid n))) is non empty set
R is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
P1 is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
((Euclid n),R,P1) is V11() real ext-real Element of REAL
max_dist_min (R,P1) is V11() real ext-real Element of REAL
max_dist_min (P1,R) is V11() real ext-real Element of REAL
max ((max_dist_min (R,P1)),(max_dist_min (P1,R))) is V11() real ext-real Element of REAL
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL n is non empty TopSpace-like V165() V190() V191() V192() V193() V194() V195() V196() V204() L16()
the carrier of (TOP-REAL n) is non empty set
K6( the carrier of (TOP-REAL n)) is non empty set
P is non empty Element of K6( the carrier of (TOP-REAL n))
(n,P,P) is V11() real ext-real Element of REAL
the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))
K6(K6( the carrier of (TOP-REAL n))) is non empty set
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct
Euclid n is non empty strict Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid n))) is non empty set
Q is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
((Euclid n),Q,Q) is V11() real ext-real Element of REAL
max_dist_min (Q,Q) is V11() real ext-real Element of REAL
max ((max_dist_min (Q,Q)),(max_dist_min (Q,Q))) is V11() real ext-real Element of REAL
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL n is non empty TopSpace-like V165() V190() V191() V192() V193() V194() V195() V196() V204() L16()
the carrier of (TOP-REAL n) is non empty set
K6( the carrier of (TOP-REAL n)) is non empty set
P is non empty Element of K6( the carrier of (TOP-REAL n))
Q is non empty Element of K6( the carrier of (TOP-REAL n))
(n,P,Q) is V11() real ext-real Element of REAL
the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))
K6(K6( the carrier of (TOP-REAL n))) is non empty set
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct
Euclid n is non empty strict Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid n))) is non empty set
R is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
P1 is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
((Euclid n),R,P1) is V11() real ext-real Element of REAL
max_dist_min (R,P1) is V11() real ext-real Element of REAL
max_dist_min (P1,R) is V11() real ext-real Element of REAL
max ((max_dist_min (R,P1)),(max_dist_min (P1,R))) is V11() real ext-real Element of REAL
n is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL n is non empty TopSpace-like V165() V190() V191() V192() V193() V194() V195() V196() V204() L16()
the carrier of (TOP-REAL n) is non empty set
K6( the carrier of (TOP-REAL n)) is non empty set
P is non empty Element of K6( the carrier of (TOP-REAL n))
Q is non empty Element of K6( the carrier of (TOP-REAL n))
R is non empty Element of K6( the carrier of (TOP-REAL n))
(n,P,R) is V11() real ext-real Element of REAL
(n,P,Q) is V11() real ext-real Element of REAL
(n,Q,R) is V11() real ext-real Element of REAL
(n,P,Q) + (n,Q,R) is V11() real ext-real Element of REAL
the topology of (TOP-REAL n) is non empty Element of K6(K6( the carrier of (TOP-REAL n)))
K6(K6( the carrier of (TOP-REAL n))) is non empty set
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is non empty strict TopSpace-like TopStruct
Euclid n is non empty strict Reflexive discerning V117() triangle MetrStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like T_0 T_1 T_2 TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid n))) is non empty set
R1 is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
Q1 is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
((Euclid n),Q1,R1) is V11() real ext-real Element of REAL
max_dist_min (Q1,R1) is V11() real ext-real Element of REAL
max_dist_min (R1,Q1) is V11() real ext-real Element of REAL
max ((max_dist_min (Q1,R1)),(max_dist_min (R1,Q1))) is V11() real ext-real Element of REAL
P1 is non empty Element of K6( the carrier of (TopSpaceMetr (Euclid n)))
((Euclid n),P1,R1) is V11() real ext-real Element of REAL
max_dist_min (P1,R1) is V11() real ext-real Element of REAL
max_dist_min (R1,P1) is V11() real ext-real Element of REAL
max ((max_dist_min (P1,R1)),(max_dist_min (R1,P1))) is V11() real ext-real Element of REAL
((Euclid n),P1,Q1) is V11() real ext-real Element of REAL
max_dist_min (P1,Q1) is V11() real ext-real Element of REAL
max_dist_min (Q1,P1) is V11() real ext-real Element of REAL
max ((max_dist_min (P1,Q1)),(max_dist_min (Q1,P1))) is V11() real ext-real Element of REAL