REAL is V45() V46() V47() V51() set
NAT is V45() V46() V47() V48() V49() V50() V51() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V45() V51() set
RAT is V45() V46() V47() V48() V51() set
INT is V45() V46() V47() V48() V49() V51() set
omega is V45() V46() V47() V48() V49() V50() V51() set
K6(omega) is set
K6(NAT) is set
K7(COMPLEX,COMPLEX) is V33() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(COMPLEX,REAL) is V33() V34() V35() set
K6(K7(COMPLEX,REAL)) is set
1 is non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
K7(1,1) is V20( RAT ) V20( INT ) V33() V34() V35() V36() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V20( RAT ) V20( INT ) V33() V34() V35() V36() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V33() V34() V35() set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is V33() V34() V35() set
K7(K7(REAL,REAL),REAL) is V33() V34() V35() set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty natural V11() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
K7(2,2) is V20( RAT ) V20( INT ) V33() V34() V35() V36() set
K7(K7(2,2),REAL) is V33() V34() V35() set
K6(K7(K7(2,2),REAL)) is set
K6(K7(REAL,REAL)) is set
K386() is non empty V142() L10()
the carrier of K386() is non empty set
K391() is non empty V142() V164() V165() V166() V168() V194() V195() V196() V197() V198() V199() L10()
K392() is non empty V142() V166() V168() V197() V198() V199() M16(K391())
K393() is non empty V142() V164() V166() V168() V197() V198() V199() V200() M19(K391(),K392())
K395() is non empty V142() V164() V166() V168() L10()
K396() is non empty V142() V164() V166() V168() V200() M16(K395())
K479() is V220() TopStruct
the carrier of K479() is V45() V46() V47() set
RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V220() MetrStruct
K484() is non empty strict TopSpace-like T_2 V220() TopStruct
the carrier of K484() is non empty V45() V46() V47() set
TOP-REAL 2 is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
NonZero (TOP-REAL 2) is Element of K6( the carrier of (TOP-REAL 2))
K6( the carrier of (TOP-REAL 2)) is set
[#] (TOP-REAL 2) is non empty non proper non proper open open connected a_component V260( TOP-REAL 2) Element of K6( the carrier of (TOP-REAL 2))
K292((TOP-REAL 2)) is V16() Function-like V33() V34() V35() V69(2) V70() V83( TOP-REAL 2) Element of the carrier of (TOP-REAL 2)
the ZeroF of (TOP-REAL 2) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
{K292((TOP-REAL 2))} is non empty functional V52() set
([#] (TOP-REAL 2)) \ {K292((TOP-REAL 2))} is Element of K6( the carrier of (TOP-REAL 2))
K7((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2))) is set
K6(K7((NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)))) is set
K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)) is set
K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2))) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V33() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is V20( RAT ) V33() V34() V35() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V20( RAT ) V33() V34() V35() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V20( RAT ) V20( INT ) V33() V34() V35() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V20( RAT ) V20( INT ) V33() V34() V35() set
K6(K7(K7(INT,INT),INT)) is 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 set
{} is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() set
the empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() set is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() set
union {} is V52() set
0 is empty natural V11() real ext-real non positive non negative Function-like functional V43() V44() V45() V46() V47() V48() V49() V50() V51() V52() V56() Element of NAT
|[0,0]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K6( the carrier of K484()) is set
A is set
B is non empty set
K7(A,B) is set
K6(K7(A,B)) is set
P is V16() V19(A) V20(B) Function-like V26(A) quasi_total Element of K6(K7(A,B))
rng P is Element of K6(B)
K6(B) is set
p is Element of B
A is set
B is non empty set
K7(A,B) is set
K6(K7(A,B)) is set
P is V16() V19(A) V20(B) Function-like V26(A) quasi_total Element of K6(K7(A,B))
p is Element of B
q is set
P . q is set
A is set
K6(A) is set
B is non empty set
K7(A,B) is set
K6(K7(A,B)) is set
P is V16() V19(A) V20(B) Function-like V26(A) quasi_total Element of K6(K7(A,B))
p is Element of K6(A)
P .: p is Element of K6(B)
K6(B) is set
(P .: p) ` is Element of K6(B)
B \ (P .: p) is set
p ` is Element of K6(A)
A \ p is set
P .: (p `) is Element of K6(B)
q is set
a is Element of B
r is set
P . r is set
r is Element of A
A is set
K6(A) is set
B is non empty set
K7(A,B) is set
K6(K7(A,B)) is set
P is V16() V19(A) V20(B) Function-like V26(A) quasi_total Element of K6(K7(A,B))
p is Element of K6(A)
p ` is Element of K6(A)
A \ p is set
P .: (p `) is Element of K6(B)
K6(B) is set
P .: p is Element of K6(B)
(P .: p) ` is Element of K6(B)
B \ (P .: p) is set
q is set
a is Element of B
r is set
P . r is set
r is set
P . r is set
A is set
K6(A) is set
B is non empty set
K7(A,B) is set
K6(K7(A,B)) is set
P is V16() V19(A) V20(B) Function-like V26(A) quasi_total Element of K6(K7(A,B))
p is Element of K6(A)
P .: p is Element of K6(B)
K6(B) is set
(P .: p) ` is Element of K6(B)
B \ (P .: p) is set
p ` is Element of K6(A)
A \ p is set
P .: (p `) is Element of K6(B)
A is TopSpace-like TopStruct
the carrier of A is set
K6( the carrier of A) is set
{} A is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact Element of K6( the carrier of A)
B is Element of K6( the carrier of A)
A | ({} A) is empty V81() V82() {} -element strict T_2 compact SubSpace of A
the carrier of (A | ({} A)) is empty V2() Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() set
K6( the carrier of (A | ({} A))) is V52() V56() set
P is functional V45() V46() V47() V48() V49() V50() V52() V56() Element of K6( the carrier of (A | ({} A)))
p is functional V45() V46() V47() V48() V49() V50() V52() V56() Element of K6( the carrier of (A | ({} A)))
A is non empty TopSpace-like TopStruct
the carrier of A is non empty set
K6( the carrier of A) is set
B is Element of K6( the carrier of A)
P is Element of K6( the carrier of A)
p is Element of K6( the carrier of A)
{} A is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact Element of K6( the carrier of A)
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
Euclid A is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL A is non empty V72() M12( REAL )
K257(A,REAL) is V72() M12( REAL )
Pitag_dist A is V16() V19(K7((REAL A),(REAL A))) V20( REAL ) Function-like quasi_total V33() V34() V35() Element of K6(K7(K7((REAL A),(REAL A)),REAL))
K7((REAL A),(REAL A)) is set
K7(K7((REAL A),(REAL A)),REAL) is V33() V34() V35() set
K6(K7(K7((REAL A),(REAL A)),REAL)) is set
MetrStruct(# (REAL A),(Pitag_dist A) #) is strict MetrStruct
the carrier of (Euclid A) is non empty set
K6( the carrier of (Euclid A)) is set
P is Element of K6( the carrier of (Euclid A))
P ` is Element of K6( the carrier of (Euclid A))
the carrier of (Euclid A) \ P is set
P \/ (P `) is Element of K6( the carrier of (Euclid A))
[#] (Euclid A) is non empty non proper Element of K6( the carrier of (Euclid A))
B is Element of K6( the carrier of (Euclid A))
A is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
TopSpaceMetr A is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr A) is non empty set
K6( the carrier of (TopSpaceMetr A)) is set
B is non empty Element of K6( the carrier of (TopSpaceMetr A))
dist_min B is non empty V16() V19( the carrier of (TopSpaceMetr A)) V20( the carrier of K484()) Function-like V26( the carrier of (TopSpaceMetr A)) quasi_total V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr A), the carrier of K484()))
K7( the carrier of (TopSpaceMetr A), the carrier of K484()) is V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr A), the carrier of K484())) is set
P is Element of the carrier of (TopSpaceMetr A)
(dist_min B) . P is V11() real ext-real Element of the carrier of K484()
the carrier of A is non empty set
Family_open_set A is Element of K6(K6( the carrier of A))
K6( the carrier of A) is set
K6(K6( the carrier of A)) is set
TopStruct(# the carrier of A,(Family_open_set A) #) is strict TopStruct
p is Element of the carrier of A
dist p is non empty V16() V19( the carrier of (TopSpaceMetr A)) V20( the carrier of K484()) Function-like V26( the carrier of (TopSpaceMetr A)) quasi_total V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr A), the carrier of K484()))
(dist p) .: B is V45() V46() V47() Element of K6( the carrier of K484())
[#] ((dist p) .: B) is V45() V46() V47() Element of K6(REAL)
a is V11() real ext-real set
dom (dist p) is Element of K6( the carrier of (TopSpaceMetr A))
r is set
(dist p) . r is V11() real ext-real set
r is Element of the carrier of A
dist (p,r) is V11() real ext-real Element of REAL
dom (dist p) is Element of K6( the carrier of (TopSpaceMetr A))
lower_bound ([#] ((dist p) .: B)) is V11() real ext-real Element of REAL
lower_bound ((dist p) .: B) is V11() real ext-real Element of REAL
A is V11() real ext-real Element of REAL
B is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
TopSpaceMetr B is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr B) is non empty set
K6( the carrier of (TopSpaceMetr B)) is set
the carrier of B is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr B))
dist_min P is non empty V16() V19( the carrier of (TopSpaceMetr B)) V20( the carrier of K484()) Function-like V26( the carrier of (TopSpaceMetr B)) quasi_total V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr B), the carrier of K484()))
K7( the carrier of (TopSpaceMetr B), the carrier of K484()) is V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr B), the carrier of K484())) is set
p is Element of the carrier of B
(dist_min P) . p is V11() real ext-real set
dist p is non empty V16() V19( the carrier of (TopSpaceMetr B)) V20( the carrier of K484()) Function-like V26( the carrier of (TopSpaceMetr B)) quasi_total V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr B), the carrier of K484()))
(dist p) .: P is V45() V46() V47() Element of K6( the carrier of K484())
[#] ((dist p) .: P) is V45() V46() V47() Element of K6(REAL)
Family_open_set B is Element of K6(K6( the carrier of B))
K6( the carrier of B) is set
K6(K6( the carrier of B)) is set
TopStruct(# the carrier of B,(Family_open_set B) #) is strict TopStruct
a is V11() real ext-real set
dom (dist p) is Element of K6( the carrier of (TopSpaceMetr B))
r is set
(dist p) . r is V11() real ext-real set
r is Element of the carrier of B
dist (p,r) is V11() real ext-real Element of REAL
dom (dist p) is Element of K6( the carrier of (TopSpaceMetr B))
lower_bound ([#] ((dist p) .: P)) is V11() real ext-real Element of REAL
lower_bound ((dist p) .: P) is V11() real ext-real Element of REAL
A is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
TopSpaceMetr A is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr A) is non empty set
K6( the carrier of (TopSpaceMetr A)) is set
B is non empty Element of K6( the carrier of (TopSpaceMetr A))
P is non empty Element of K6( the carrier of (TopSpaceMetr A))
min_dist_min (B,P) is V11() real ext-real Element of REAL
dist_min B is non empty V16() V19( the carrier of (TopSpaceMetr A)) V20( the carrier of K484()) Function-like V26( the carrier of (TopSpaceMetr A)) quasi_total V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr A), the carrier of K484()))
K7( the carrier of (TopSpaceMetr A), the carrier of K484()) is V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr A), the carrier of K484())) is set
(dist_min B) .: P is V45() V46() V47() Element of K6( the carrier of K484())
[#] ((dist_min B) .: P) is V45() V46() V47() Element of K6(REAL)
q is V11() real ext-real set
dom (dist_min B) is Element of K6( the carrier of (TopSpaceMetr A))
a is set
(dist_min B) . a is V11() real ext-real set
r is Element of the carrier of (TopSpaceMetr A)
(dist_min B) . r is V11() real ext-real Element of the carrier of K484()
dom (dist_min B) is Element of K6( the carrier of (TopSpaceMetr A))
lower_bound ([#] ((dist_min B) .: P)) is V11() real ext-real Element of REAL
lower_bound ((dist_min B) .: P) is V11() real ext-real Element of REAL
A is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
TopSpaceMetr A is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr A) is non empty set
K6( the carrier of (TopSpaceMetr A)) is set
B is compact Element of K6( the carrier of (TopSpaceMetr A))
P is compact Element of K6( the carrier of (TopSpaceMetr A))
min_dist_min (B,P) is V11() real ext-real Element of REAL
p is set
the carrier of A is non empty set
Family_open_set A is Element of K6(K6( the carrier of A))
K6( the carrier of A) is set
K6(K6( the carrier of A)) is set
TopStruct(# the carrier of A,(Family_open_set A) #) is strict TopStruct
q is Element of the carrier of A
dist (q,q) is V11() real ext-real Element of REAL
A is V11() real ext-real Element of REAL
B is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
TopSpaceMetr B is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr B) is non empty set
K6( the carrier of (TopSpaceMetr B)) is set
the carrier of B is non empty set
P is non empty Element of K6( the carrier of (TopSpaceMetr B))
p is non empty Element of K6( the carrier of (TopSpaceMetr B))
min_dist_min (P,p) is V11() real ext-real Element of REAL
dist_min P is non empty V16() V19( the carrier of (TopSpaceMetr B)) V20( the carrier of K484()) Function-like V26( the carrier of (TopSpaceMetr B)) quasi_total V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr B), the carrier of K484()))
K7( the carrier of (TopSpaceMetr B), the carrier of K484()) is V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr B), the carrier of K484())) is set
(dist_min P) .: p is V45() V46() V47() Element of K6( the carrier of K484())
[#] ((dist_min P) .: p) is V45() V46() V47() Element of K6(REAL)
a is V11() real ext-real set
dom (dist_min P) is Element of K6( the carrier of (TopSpaceMetr B))
r is set
(dist_min P) . r is V11() real ext-real set
r is Element of the carrier of (TopSpaceMetr B)
s is Element of the carrier of B
q9 is Element of the carrier of B
dist (s,q9) is V11() real ext-real Element of REAL
dom (dist_min P) is Element of K6( the carrier of (TopSpaceMetr B))
lower_bound ([#] ((dist_min P) .: p)) is V11() real ext-real Element of REAL
lower_bound ((dist_min P) .: p) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
P is Element of K6( the carrier of (TOP-REAL A))
P ` is Element of K6( the carrier of (TOP-REAL A))
the carrier of (TOP-REAL A) \ P is set
B is Element of K6( the carrier of (TOP-REAL A))
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
{} (TOP-REAL A) is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact bounded Element of K6( the carrier of (TOP-REAL A))
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
BDD ({} (TOP-REAL A)) is Element of K6( the carrier of (TOP-REAL A))
{ b1 where b1 is Element of K6( the carrier of (TOP-REAL A)) : b1 is_inside_component_of {} (TOP-REAL A) } is set
[#] (TOP-REAL A) is non empty non proper non proper open open connected a_component V260( TOP-REAL A) Element of K6( the carrier of (TOP-REAL A))
the topology of (TOP-REAL A) is Element of K6(K6( the carrier of (TOP-REAL A)))
K6(K6( the carrier of (TOP-REAL A))) is set
TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is strict TopStruct
[#] TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is non proper Element of K6( the carrier of TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #))
the carrier of TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is set
K6( the carrier of TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #)) is set
(TOP-REAL A) | ([#] (TOP-REAL A)) is strict SubSpace of TOP-REAL A
P is set
p is Element of K6( the carrier of (TOP-REAL A))
({} (TOP-REAL A)) ` is closed Element of K6( the carrier of (TOP-REAL A))
the carrier of (TOP-REAL A) \ ({} (TOP-REAL A)) is set
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
[#] (TOP-REAL A) is non empty non proper non proper open open connected a_component V260( TOP-REAL A) Element of K6( the carrier of (TOP-REAL A))
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
BDD ([#] (TOP-REAL A)) is Element of K6( the carrier of (TOP-REAL A))
{} (TOP-REAL A) is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact bounded Element of K6( the carrier of (TOP-REAL A))
([#] (TOP-REAL A)) ` is closed Element of K6( the carrier of (TOP-REAL A))
the carrier of (TOP-REAL A) \ ([#] (TOP-REAL A)) is set
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
{} (TOP-REAL A) is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact bounded Element of K6( the carrier of (TOP-REAL A))
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
UBD ({} (TOP-REAL A)) is Element of K6( the carrier of (TOP-REAL A))
[#] (TOP-REAL A) is non empty non proper non proper open open connected a_component V260( TOP-REAL A) Element of K6( the carrier of (TOP-REAL A))
{ b1 where b1 is Element of K6( the carrier of (TOP-REAL A)) : b1 is_outside_component_of {} (TOP-REAL A) } is set
the topology of (TOP-REAL A) is Element of K6(K6( the carrier of (TOP-REAL A)))
K6(K6( the carrier of (TOP-REAL A))) is set
TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is strict TopStruct
[#] TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is non proper Element of K6( the carrier of TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #))
the carrier of TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is set
K6( the carrier of TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #)) is set
(TOP-REAL A) | ([#] (TOP-REAL A)) is strict SubSpace of TOP-REAL A
({} (TOP-REAL A)) ` is closed Element of K6( the carrier of (TOP-REAL A))
the carrier of (TOP-REAL A) \ ({} (TOP-REAL A)) is set
union { b1 where b1 is Element of K6( the carrier of (TOP-REAL A)) : b1 is_outside_component_of {} (TOP-REAL A) } is set
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
[#] (TOP-REAL A) is non empty non proper non proper open open connected a_component V260( TOP-REAL A) Element of K6( the carrier of (TOP-REAL A))
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
UBD ([#] (TOP-REAL A)) is Element of K6( the carrier of (TOP-REAL A))
{} (TOP-REAL A) is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact bounded Element of K6( the carrier of (TOP-REAL A))
([#] (TOP-REAL A)) ` is closed Element of K6( the carrier of (TOP-REAL A))
the carrier of (TOP-REAL A) \ ([#] (TOP-REAL A)) is set
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
B is connected Element of K6( the carrier of (TOP-REAL A))
P is Element of K6( the carrier of (TOP-REAL A))
UBD P is Element of K6( the carrier of (TOP-REAL A))
BDD P is Element of K6( the carrier of (TOP-REAL A))
[#] (TOP-REAL A) is non empty non proper non proper open open connected a_component V260( TOP-REAL A) Element of K6( the carrier of (TOP-REAL A))
[#] (TOP-REAL A) is non empty non proper non proper open open connected a_component V260( TOP-REAL A) Element of K6( the carrier of (TOP-REAL A))
P ` is Element of K6( the carrier of (TOP-REAL A))
the carrier of (TOP-REAL A) \ P is set
(P `) ` is Element of K6( the carrier of (TOP-REAL A))
the carrier of (TOP-REAL A) \ (P `) is set
{} (TOP-REAL A) is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact bounded Element of K6( the carrier of (TOP-REAL A))
p is Element of K6( the carrier of (TOP-REAL A))
[#] (TOP-REAL A) is non empty non proper non proper open open connected a_component V260( TOP-REAL A) Element of K6( the carrier of (TOP-REAL A))
Euclid 2 is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL 2 is non empty V72() M12( REAL )
K257(2,REAL) is V72() M12( REAL )
Pitag_dist 2 is V16() V19(K7((REAL 2),(REAL 2))) V20( REAL ) Function-like quasi_total V33() V34() V35() Element of K6(K7(K7((REAL 2),(REAL 2)),REAL))
K7((REAL 2),(REAL 2)) is set
K7(K7((REAL 2),(REAL 2)),REAL) is V33() V34() V35() set
K6(K7(K7((REAL 2),(REAL 2)),REAL)) is set
MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct
the carrier of (Euclid 2) is non empty set
A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
dist (|[0,0]|,A) is V11() real ext-real Element of REAL
B is V11() real ext-real Element of REAL
B * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(A,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist (|[0,0]|,(B * A)) is V11() real ext-real Element of REAL
abs B is V11() real ext-real Element of REAL
(abs B) * (dist (|[0,0]|,A)) is V11() real ext-real Element of REAL
B ^2 is V11() real ext-real Element of REAL
K37(B,B) is V11() real ext-real set
A `1 is V11() real ext-real Element of REAL
(A `1) ^2 is V11() real ext-real Element of REAL
K37((A `1),(A `1)) is V11() real ext-real set
A `2 is V11() real ext-real Element of REAL
(A `2) ^2 is V11() real ext-real Element of REAL
K37((A `2),(A `2)) is V11() real ext-real set
|[0,0]| `1 is V11() real ext-real Element of REAL
|[0,0]| `2 is V11() real ext-real Element of REAL
0 - (A `1) is V11() real ext-real Element of REAL
(0 - (A `1)) ^2 is V11() real ext-real Element of REAL
K37((0 - (A `1)),(0 - (A `1))) is V11() real ext-real set
0 - (A `2) is V11() real ext-real Element of REAL
(0 - (A `2)) ^2 is V11() real ext-real Element of REAL
K37((0 - (A `2)),(0 - (A `2))) is V11() real ext-real set
((0 - (A `1)) ^2) + ((0 - (A `2)) ^2) is V11() real ext-real Element of REAL
sqrt (((0 - (A `1)) ^2) + ((0 - (A `2)) ^2)) is V11() real ext-real Element of REAL
((A `1) ^2) + ((A `2) ^2) is V11() real ext-real Element of REAL
sqrt (((A `1) ^2) + ((A `2) ^2)) is V11() real ext-real Element of REAL
(B * A) `1 is V11() real ext-real Element of REAL
0 - ((B * A) `1) is V11() real ext-real Element of REAL
(0 - ((B * A) `1)) ^2 is V11() real ext-real Element of REAL
K37((0 - ((B * A) `1)),(0 - ((B * A) `1))) is V11() real ext-real set
(B * A) `2 is V11() real ext-real Element of REAL
0 - ((B * A) `2) is V11() real ext-real Element of REAL
(0 - ((B * A) `2)) ^2 is V11() real ext-real Element of REAL
K37((0 - ((B * A) `2)),(0 - ((B * A) `2))) is V11() real ext-real set
((0 - ((B * A) `1)) ^2) + ((0 - ((B * A) `2)) ^2) is V11() real ext-real Element of REAL
sqrt (((0 - ((B * A) `1)) ^2) + ((0 - ((B * A) `2)) ^2)) is V11() real ext-real Element of REAL
((B * A) `1) ^2 is V11() real ext-real Element of REAL
K37(((B * A) `1),((B * A) `1)) is V11() real ext-real set
- ((B * A) `2) is V11() real ext-real Element of REAL
(- ((B * A) `2)) ^2 is V11() real ext-real Element of REAL
K37((- ((B * A) `2)),(- ((B * A) `2))) is V11() real ext-real set
(((B * A) `1) ^2) + ((- ((B * A) `2)) ^2) is V11() real ext-real Element of REAL
sqrt ((((B * A) `1) ^2) + ((- ((B * A) `2)) ^2)) is V11() real ext-real Element of REAL
B * (A `1) is V11() real ext-real Element of REAL
(B * (A `1)) ^2 is V11() real ext-real Element of REAL
K37((B * (A `1)),(B * (A `1))) is V11() real ext-real set
((B * A) `2) ^2 is V11() real ext-real Element of REAL
K37(((B * A) `2),((B * A) `2)) is V11() real ext-real set
((B * (A `1)) ^2) + (((B * A) `2) ^2) is V11() real ext-real Element of REAL
sqrt (((B * (A `1)) ^2) + (((B * A) `2) ^2)) is V11() real ext-real Element of REAL
(B ^2) * ((A `1) ^2) is V11() real ext-real Element of REAL
B * (A `2) is V11() real ext-real Element of REAL
(B * (A `2)) ^2 is V11() real ext-real Element of REAL
K37((B * (A `2)),(B * (A `2))) is V11() real ext-real set
((B ^2) * ((A `1) ^2)) + ((B * (A `2)) ^2) is V11() real ext-real Element of REAL
sqrt (((B ^2) * ((A `1) ^2)) + ((B * (A `2)) ^2)) is V11() real ext-real Element of REAL
(B ^2) * (((A `1) ^2) + ((A `2) ^2)) is V11() real ext-real Element of REAL
sqrt ((B ^2) * (((A `1) ^2) + ((A `2) ^2))) is V11() real ext-real Element of REAL
sqrt (B ^2) is V11() real ext-real Element of REAL
(sqrt (B ^2)) * (sqrt (((A `1) ^2) + ((A `2) ^2))) is V11() real ext-real Element of REAL
A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
A + B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365(A,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
P is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
P + B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365(P,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist ((A + B),(P + B)) is V11() real ext-real Element of REAL
dist (A,P) is V11() real ext-real Element of REAL
(A + B) `1 is V11() real ext-real Element of REAL
(P + B) `1 is V11() real ext-real Element of REAL
((A + B) `1) - ((P + B) `1) is V11() real ext-real Element of REAL
A `1 is V11() real ext-real Element of REAL
B `1 is V11() real ext-real Element of REAL
(A `1) + (B `1) is V11() real ext-real Element of REAL
((A `1) + (B `1)) - ((P + B) `1) is V11() real ext-real Element of REAL
P `1 is V11() real ext-real Element of REAL
(P `1) + (B `1) is V11() real ext-real Element of REAL
((A `1) + (B `1)) - ((P `1) + (B `1)) is V11() real ext-real Element of REAL
(A `1) - (P `1) is V11() real ext-real Element of REAL
((A `1) - (P `1)) + 0 is V11() real ext-real Element of REAL
(A + B) `2 is V11() real ext-real Element of REAL
(P + B) `2 is V11() real ext-real Element of REAL
((A + B) `2) - ((P + B) `2) is V11() real ext-real Element of REAL
A `2 is V11() real ext-real Element of REAL
B `2 is V11() real ext-real Element of REAL
(A `2) + (B `2) is V11() real ext-real Element of REAL
((A `2) + (B `2)) - ((P + B) `2) is V11() real ext-real Element of REAL
P `2 is V11() real ext-real Element of REAL
(P `2) + (B `2) is V11() real ext-real Element of REAL
((A `2) + (B `2)) - ((P `2) + (B `2)) is V11() real ext-real Element of REAL
(A `2) - (P `2) is V11() real ext-real Element of REAL
((A `2) - (P `2)) + 0 is V11() real ext-real Element of REAL
(((A + B) `1) - ((P + B) `1)) ^2 is V11() real ext-real Element of REAL
K37((((A + B) `1) - ((P + B) `1)),(((A + B) `1) - ((P + B) `1))) is V11() real ext-real set
(((A + B) `2) - ((P + B) `2)) ^2 is V11() real ext-real Element of REAL
K37((((A + B) `2) - ((P + B) `2)),(((A + B) `2) - ((P + B) `2))) is V11() real ext-real set
((((A + B) `1) - ((P + B) `1)) ^2) + ((((A + B) `2) - ((P + B) `2)) ^2) is V11() real ext-real Element of REAL
sqrt (((((A + B) `1) - ((P + B) `1)) ^2) + ((((A + B) `2) - ((P + B) `2)) ^2)) is V11() real ext-real Element of REAL
A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
dist (A,B) is V11() real ext-real Element of REAL
P is Element of the carrier of (Euclid 2)
p is Element of the carrier of (Euclid 2)
dist (P,p) is V11() real ext-real Element of REAL
A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
A - B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(A,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
P is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
P - B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(P,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist ((A - B),(P - B)) is V11() real ext-real Element of REAL
dist (A,P) is V11() real ext-real Element of REAL
- B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K367(B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
A + (- B) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365(A,(- B)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
P + (- B) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365(P,(- B)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
- A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K367(A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
dist (A,B) is V11() real ext-real Element of REAL
- B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K367(B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist ((- A),(- B)) is V11() real ext-real Element of REAL
B - B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(B,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
A - B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(A,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist ((B - B),(A - B)) is V11() real ext-real Element of REAL
A + (- B) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365(A,(- B)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist ((B - B),(A + (- B))) is V11() real ext-real Element of REAL
dist (|[0,0]|,(A + (- B))) is V11() real ext-real Element of REAL
A - A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(A,A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist ((A - A),(A + (- B))) is V11() real ext-real Element of REAL
A + (- A) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365(A,(- A)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist ((A + (- A)),(A + (- B))) is V11() real ext-real Element of REAL
A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
A - B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(A,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
P is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
A - P is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(A,P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist ((A - B),(A - P)) is V11() real ext-real Element of REAL
dist (B,P) is V11() real ext-real Element of REAL
- (A - B) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K367((A - B)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
B - A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(B,A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
- (A - P) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K367((A - P)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
P - A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(P,A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist ((B - A),(P - A)) is V11() real ext-real Element of REAL
A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
dist (A,B) is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
P * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(A,P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
P * B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(B,P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist ((P * A),(P * B)) is V11() real ext-real Element of REAL
abs P is V11() real ext-real Element of REAL
(abs P) * (dist (A,B)) is V11() real ext-real Element of REAL
(P * A) - (P * A) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369((P * A),(P * A)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
(P * A) - (P * B) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369((P * A),(P * B)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist (((P * A) - (P * A)),((P * A) - (P * B))) is V11() real ext-real Element of REAL
dist (|[0,0]|,((P * A) - (P * B))) is V11() real ext-real Element of REAL
A - B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(A,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
P * (A - B) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371((A - B),P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist (|[0,0]|,(P * (A - B))) is V11() real ext-real Element of REAL
dist (|[0,0]|,(A - B)) is V11() real ext-real Element of REAL
(abs P) * (dist (|[0,0]|,(A - B))) is V11() real ext-real Element of REAL
A - A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(A,A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist ((A - A),(A - B)) is V11() real ext-real Element of REAL
(abs P) * (dist ((A - A),(A - B))) is V11() real ext-real Element of REAL
A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
dist (A,B) is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
P * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(A,P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
1 - P is V11() real ext-real Element of REAL
(1 - P) * B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(B,(1 - P)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
(P * A) + ((1 - P) * B) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365((P * A),((1 - P) * B)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist (A,((P * A) + ((1 - P) * B))) is V11() real ext-real Element of REAL
(1 - P) * (dist (A,B)) is V11() real ext-real Element of REAL
1 + P is V11() real ext-real Element of REAL
1 + 1 is non empty V11() real ext-real positive non negative Element of REAL
1 - 1 is V11() real ext-real Element of REAL
abs (1 - P) is V11() real ext-real Element of REAL
P + (1 - P) is V11() real ext-real Element of REAL
(P + (1 - P)) * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(A,(P + (1 - P))) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist (((P + (1 - P)) * A),((P * A) + ((1 - P) * B))) is V11() real ext-real Element of REAL
(1 - P) * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(A,(1 - P)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
(P * A) + ((1 - P) * A) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365((P * A),((1 - P) * A)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist (((P * A) + ((1 - P) * A)),((P * A) + ((1 - P) * B))) is V11() real ext-real Element of REAL
dist (((1 - P) * A),((1 - P) * B)) is V11() real ext-real Element of REAL
A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
dist (B,A) is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
P * B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(B,P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
1 - P is V11() real ext-real Element of REAL
(1 - P) * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(A,(1 - P)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
(P * B) + ((1 - P) * A) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365((P * B),((1 - P) * A)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist (A,((P * B) + ((1 - P) * A))) is V11() real ext-real Element of REAL
P * (dist (B,A)) is V11() real ext-real Element of REAL
abs P is V11() real ext-real Element of REAL
P + (1 - P) is V11() real ext-real Element of REAL
(P + (1 - P)) * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(A,(P + (1 - P))) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist (((P * B) + ((1 - P) * A)),((P + (1 - P)) * A)) is V11() real ext-real Element of REAL
P * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(A,P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
(P * A) + ((1 - P) * A) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365((P * A),((1 - P) * A)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist (((P * A) + ((1 - P) * A)),((P * B) + ((1 - P) * A))) is V11() real ext-real Element of REAL
dist ((P * A),(P * B)) is V11() real ext-real Element of REAL
A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
dist (B,A) is V11() real ext-real Element of REAL
P is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
LSeg (B,P) is connected Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * B) + (b1 * P)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
dist (A,P) is V11() real ext-real Element of REAL
(dist (B,A)) + (dist (A,P)) is V11() real ext-real Element of REAL
dist (B,P) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
1 - p is V11() real ext-real Element of REAL
(1 - p) * B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(B,(1 - p)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
p * P is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(P,p) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
((1 - p) * B) + (p * P) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365(((1 - p) * B),(p * P)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
p * (dist (B,P)) is V11() real ext-real Element of REAL
dist (P,A) is V11() real ext-real Element of REAL
(1 - p) * (dist (B,P)) is V11() real ext-real Element of REAL
A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
P is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
LSeg (B,P) is connected Element of K6( the carrier of (TOP-REAL 2))
{ (((1 - b1) * B) + (b1 * P)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
dist (B,P) is V11() real ext-real Element of REAL
dist (A,P) is V11() real ext-real Element of REAL
dist (B,A) is V11() real ext-real Element of REAL
(dist (B,A)) + (dist (A,P)) is V11() real ext-real Element of REAL
A is V11() real ext-real Element of REAL
{ b1 where b1 is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2) : not A <= |.b1.| } is set
B is Element of the carrier of (Euclid 2)
Ball (B,A) is Element of K6( the carrier of (Euclid 2))
K6( the carrier of (Euclid 2)) is set
{ b1 where b1 is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2) : not A <= |.(|[0,0]| - b1).| } is set
q is set
a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
|[0,0]| - a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(|[0,0]|,a) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
|.(|[0,0]| - a).| is V11() real ext-real non negative Element of REAL
K373((|[0,0]| - a)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
K379(K373((|[0,0]| - a))) is V11() real ext-real Element of REAL
sqrt K379(K373((|[0,0]| - a))) is V11() real ext-real Element of REAL
a - |[0,0]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(a,|[0,0]|) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
|.(a - |[0,0]|).| is V11() real ext-real non negative Element of REAL
K373((a - |[0,0]|)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
K379(K373((a - |[0,0]|))) is V11() real ext-real Element of REAL
sqrt K379(K373((a - |[0,0]|))) is V11() real ext-real Element of REAL
|.a.| is V11() real ext-real non negative Element of REAL
K373(a) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
K379(K373(a)) is V11() real ext-real Element of REAL
sqrt K379(K373(a)) is V11() real ext-real Element of REAL
q is set
a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
|.a.| is V11() real ext-real non negative Element of REAL
K373(a) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
K379(K373(a)) is V11() real ext-real Element of REAL
sqrt K379(K373(a)) is V11() real ext-real Element of REAL
|[0,0]| - a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(|[0,0]|,a) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
|.(|[0,0]| - a).| is V11() real ext-real non negative Element of REAL
K373((|[0,0]| - a)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
K379(K373((|[0,0]| - a))) is V11() real ext-real Element of REAL
sqrt K379(K373((|[0,0]| - a))) is V11() real ext-real Element of REAL
a - |[0,0]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K369(a,|[0,0]|) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
|.(a - |[0,0]|).| is V11() real ext-real non negative Element of REAL
K373((a - |[0,0]|)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
K379(K373((a - |[0,0]|))) is V11() real ext-real Element of REAL
sqrt K379(K373((a - |[0,0]|))) is V11() real ext-real Element of REAL
A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
B is V11() real ext-real Element of REAL
B * A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(A,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
P is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
AffineMap (B,P,B,p) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total V94( TOP-REAL 2, TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
(AffineMap (B,P,B,p)) . A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
|[P,p]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(B * A) + |[P,p]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365((B * A),|[P,p]|) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
A `1 is V11() real ext-real Element of REAL
B * (A `1) is V11() real ext-real Element of REAL
(B * (A `1)) + P is V11() real ext-real Element of REAL
A `2 is V11() real ext-real Element of REAL
B * (A `2) is V11() real ext-real Element of REAL
(B * (A `2)) + p is V11() real ext-real Element of REAL
|[((B * (A `1)) + P),((B * (A `2)) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(B * A) `1 is V11() real ext-real Element of REAL
((B * A) `1) + P is V11() real ext-real Element of REAL
|[(((B * A) `1) + P),((B * (A `2)) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(B * A) `2 is V11() real ext-real Element of REAL
((B * A) `2) + p is V11() real ext-real Element of REAL
|[(((B * A) `1) + P),(((B * A) `2) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
|[((B * A) `1),((B * A) `2)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
|[((B * A) `1),((B * A) `2)]| + |[P,p]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365(|[((B * A) `1),((B * A) `2)]|,|[P,p]|) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
A `1 is V11() real ext-real Element of REAL
A `2 is V11() real ext-real Element of REAL
B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
P is V11() real ext-real Element of REAL
AffineMap (P,(A `1),P,(A `2)) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total V94( TOP-REAL 2, TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
(AffineMap (P,(A `1),P,(A `2))) . B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
P * B is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(B,P) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
(P * B) + A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365((P * B),A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
|[(A `1),(A `2)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(P * B) + |[(A `1),(A `2)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365((P * B),|[(A `1),(A `2)]|) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
id (REAL 2) is non empty V16() V19( REAL 2) V20( REAL 2) Function-like one-to-one V26( REAL 2) quasi_total Element of K6(K7((REAL 2),(REAL 2)))
K6(K7((REAL 2),(REAL 2))) is set
A is V11() real ext-real Element of REAL
1 / A is V11() real ext-real Element of REAL
B is V11() real ext-real Element of REAL
1 / B is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
P / A is V11() real ext-real Element of REAL
- (P / A) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
p / B is V11() real ext-real Element of REAL
- (p / B) is V11() real ext-real Element of REAL
AffineMap ((1 / A),(- (P / A)),(1 / B),(- (p / B))) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total V94( TOP-REAL 2, TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
AffineMap (A,P,B,p) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total V94( TOP-REAL 2, TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
(AffineMap (A,P,B,p)) * (AffineMap ((1 / A),(- (P / A)),(1 / B),(- (p / B)))) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
a `1 is V11() real ext-real Element of REAL
(1 / A) * (a `1) is V11() real ext-real Element of REAL
((1 / A) * (a `1)) - (P / A) is V11() real ext-real Element of REAL
a `2 is V11() real ext-real Element of REAL
(1 / B) * (a `2) is V11() real ext-real Element of REAL
((1 / B) * (a `2)) - (p / B) is V11() real ext-real Element of REAL
|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `2 is V11() real ext-real Element of REAL
A * (1 / A) is V11() real ext-real Element of REAL
((AffineMap (A,P,B,p)) * (AffineMap ((1 / A),(- (P / A)),(1 / B),(- (p / B))))) . a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(AffineMap ((1 / A),(- (P / A)),(1 / B),(- (p / B)))) . a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(AffineMap (A,P,B,p)) . ((AffineMap ((1 / A),(- (P / A)),(1 / B),(- (p / B)))) . a) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
((1 / A) * (a `1)) + (- (P / A)) is V11() real ext-real Element of REAL
((1 / B) * (a `2)) + (- (p / B)) is V11() real ext-real Element of REAL
|[(((1 / A) * (a `1)) + (- (P / A))),(((1 / B) * (a `2)) + (- (p / B)))]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(AffineMap (A,P,B,p)) . |[(((1 / A) * (a `1)) + (- (P / A))),(((1 / B) * (a `2)) + (- (p / B)))]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `1 is V11() real ext-real Element of REAL
A * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `1) is V11() real ext-real Element of REAL
(A * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `1)) + P is V11() real ext-real Element of REAL
B * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `2) is V11() real ext-real Element of REAL
(B * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `2)) + p is V11() real ext-real Element of REAL
|[((A * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `1)) + P),((B * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `2)) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
A * (((1 / A) * (a `1)) - (P / A)) is V11() real ext-real Element of REAL
(A * (((1 / A) * (a `1)) - (P / A))) + P is V11() real ext-real Element of REAL
|[((A * (((1 / A) * (a `1)) - (P / A))) + P),((B * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `2)) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(A * (1 / A)) * (a `1) is V11() real ext-real Element of REAL
A * (P / A) is V11() real ext-real Element of REAL
((A * (1 / A)) * (a `1)) - (A * (P / A)) is V11() real ext-real Element of REAL
(((A * (1 / A)) * (a `1)) - (A * (P / A))) + P is V11() real ext-real Element of REAL
|[((((A * (1 / A)) * (a `1)) - (A * (P / A))) + P),((B * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `2)) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
1 * (a `1) is V11() real ext-real Element of REAL
1 * P is V11() real ext-real Element of REAL
(1 * (a `1)) - (1 * P) is V11() real ext-real Element of REAL
((1 * (a `1)) - (1 * P)) + P is V11() real ext-real Element of REAL
|[(((1 * (a `1)) - (1 * P)) + P),((B * (|[(((1 / A) * (a `1)) - (P / A)),(((1 / B) * (a `2)) - (p / B))]| `2)) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
B * ((1 / B) * (a `2)) is V11() real ext-real Element of REAL
B * (p / B) is V11() real ext-real Element of REAL
(B * ((1 / B) * (a `2))) - (B * (p / B)) is V11() real ext-real Element of REAL
((B * ((1 / B) * (a `2))) - (B * (p / B))) + p is V11() real ext-real Element of REAL
|[(a `1),(((B * ((1 / B) * (a `2))) - (B * (p / B))) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
B * (1 / B) is V11() real ext-real Element of REAL
(B * (1 / B)) * (a `2) is V11() real ext-real Element of REAL
((B * (1 / B)) * (a `2)) - p is V11() real ext-real Element of REAL
(((B * (1 / B)) * (a `2)) - p) + p is V11() real ext-real Element of REAL
|[(a `1),((((B * (1 / B)) * (a `2)) - p) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
1 * (a `2) is V11() real ext-real Element of REAL
1 * p is V11() real ext-real Element of REAL
(1 * (a `2)) - (1 * p) is V11() real ext-real Element of REAL
((1 * (a `2)) - (1 * p)) + p is V11() real ext-real Element of REAL
|[(a `1),(((1 * (a `2)) - (1 * p)) + p)]| is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
q is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
q . a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
A `1 is V11() real ext-real Element of REAL
A `2 is V11() real ext-real Element of REAL
B is V11() real ext-real Element of REAL
AffineMap (B,(A `1),B,(A `2)) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total V94( TOP-REAL 2, TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
P is Element of the carrier of (Euclid 2)
Ball (P,1) is Element of K6( the carrier of (Euclid 2))
K6( the carrier of (Euclid 2)) is set
(AffineMap (B,(A `1),B,(A `2))) .: (Ball (P,1)) is Element of K6( the carrier of (TOP-REAL 2))
p is Element of the carrier of (Euclid 2)
Ball (p,B) is Element of K6( the carrier of (Euclid 2))
a is Element of K6( the carrier of (TOP-REAL 2))
q is Element of K6( the carrier of (TOP-REAL 2))
(AffineMap (B,(A `1),B,(A `2))) .: q is Element of K6( the carrier of (TOP-REAL 2))
r is set
r is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
1 / B is V11() real ext-real Element of REAL
(A `1) / B is V11() real ext-real Element of REAL
- ((A `1) / B) is V11() real ext-real Element of REAL
(A `2) / B is V11() real ext-real Element of REAL
- ((A `2) / B) is V11() real ext-real Element of REAL
AffineMap ((1 / B),(- ((A `1) / B)),(1 / B),(- ((A `2) / B))) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total V94( TOP-REAL 2, TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
(AffineMap ((1 / B),(- ((A `1) / B)),(1 / B),(- ((A `2) / B)))) . r is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
B * ((AffineMap ((1 / B),(- ((A `1) / B)),(1 / B),(- ((A `2) / B)))) . r) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(((AffineMap ((1 / B),(- ((A `1) / B)),(1 / B),(- ((A `2) / B)))) . r),B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
(B * ((AffineMap ((1 / B),(- ((A `1) / B)),(1 / B),(- ((A `2) / B)))) . r)) + A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365((B * ((AffineMap ((1 / B),(- ((A `1) / B)),(1 / B),(- ((A `2) / B)))) . r)),A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist (A,((B * ((AffineMap ((1 / B),(- ((A `1) / B)),(1 / B),(- ((A `2) / B)))) . r)) + A)) is V11() real ext-real Element of REAL
X is Element of the carrier of (Euclid 2)
z2 is Element of the carrier of (Euclid 2)
dist (X,z2) is V11() real ext-real Element of REAL
dist (|[0,0]|,((AffineMap ((1 / B),(- ((A `1) / B)),(1 / B),(- ((A `2) / B)))) . r)) is V11() real ext-real Element of REAL
z3 is Element of the carrier of (Euclid 2)
z4 is Element of the carrier of (Euclid 2)
dist (z3,z4) is V11() real ext-real Element of REAL
(AffineMap (B,(A `1),B,(A `2))) . ((AffineMap ((1 / B),(- ((A `1) / B)),(1 / B),(- ((A `2) / B)))) . r) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(AffineMap (B,(A `1),B,(A `2))) * (AffineMap ((1 / B),(- ((A `1) / B)),(1 / B),(- ((A `2) / B)))) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
((AffineMap (B,(A `1),B,(A `2))) * (AffineMap ((1 / B),(- ((A `1) / B)),(1 / B),(- ((A `2) / B))))) . r is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(id (REAL 2)) . r is set
s is Element of the carrier of (Euclid 2)
dist (p,s) is V11() real ext-real Element of REAL
|[0,0]| + A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365(|[0,0]|,A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist ((|[0,0]| + A),((B * ((AffineMap ((1 / B),(- ((A `1) / B)),(1 / B),(- ((A `2) / B)))) . r)) + A)) is V11() real ext-real Element of REAL
dist (|[0,0]|,(B * ((AffineMap ((1 / B),(- ((A `1) / B)),(1 / B),(- ((A `2) / B)))) . r))) is V11() real ext-real Element of REAL
abs B is V11() real ext-real Element of REAL
(abs B) * (dist (|[0,0]|,((AffineMap ((1 / B),(- ((A `1) / B)),(1 / B),(- ((A `2) / B)))) . r))) is V11() real ext-real Element of REAL
dist (P,z4) is V11() real ext-real Element of REAL
B * (dist (P,z4)) is V11() real ext-real Element of REAL
1 * B is V11() real ext-real Element of REAL
id (TOP-REAL 2) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
id the carrier of (TOP-REAL 2) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like one-to-one V26( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
(id (TOP-REAL 2)) . r is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
r is set
r is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
s is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(AffineMap (B,(A `1),B,(A `2))) . s is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
X is Element of the carrier of (Euclid 2)
dist (P,X) is V11() real ext-real Element of REAL
dist (|[0,0]|,s) is V11() real ext-real Element of REAL
B * s is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(s,B) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
(B * s) + A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365((B * s),A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist (A,((B * s) + A)) is V11() real ext-real Element of REAL
q9 is Element of the carrier of (Euclid 2)
dist (p,q9) is V11() real ext-real Element of REAL
|[0,0]| + A is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365(|[0,0]|,A) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
dist ((|[0,0]| + A),((B * s) + A)) is V11() real ext-real Element of REAL
dist (|[0,0]|,(B * s)) is V11() real ext-real Element of REAL
abs B is V11() real ext-real Element of REAL
(abs B) * (dist (|[0,0]|,s)) is V11() real ext-real Element of REAL
B * (dist (P,X)) is V11() real ext-real Element of REAL
z2 is Element of the carrier of (Euclid 2)
z3 is Element of the carrier of (Euclid 2)
dist (z2,z3) is V11() real ext-real Element of REAL
z2 is Element of the carrier of (Euclid 2)
z3 is Element of the carrier of (Euclid 2)
dist (z2,z3) is V11() real ext-real Element of REAL
A is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
B is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
AffineMap (A,B,P,p) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total V94( TOP-REAL 2, TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
rng (AffineMap (A,B,P,p)) is Element of K6( the carrier of (TOP-REAL 2))
q is set
1 / A is V11() real ext-real Element of REAL
B / A is V11() real ext-real Element of REAL
- (B / A) is V11() real ext-real Element of REAL
1 / P is V11() real ext-real Element of REAL
p / P is V11() real ext-real Element of REAL
- (p / P) is V11() real ext-real Element of REAL
AffineMap ((1 / A),(- (B / A)),(1 / P),(- (p / P))) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total V94( TOP-REAL 2, TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(AffineMap ((1 / A),(- (B / A)),(1 / P),(- (p / P)))) . a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(AffineMap (A,B,P,p)) . ((AffineMap ((1 / A),(- (B / A)),(1 / P),(- (p / P)))) . a) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(AffineMap (A,B,P,p)) * (AffineMap ((1 / A),(- (B / A)),(1 / P),(- (p / P)))) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
((AffineMap (A,B,P,p)) * (AffineMap ((1 / A),(- (B / A)),(1 / P),(- (p / P))))) . a is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(id (REAL 2)) . a is set
A is V11() real ext-real Element of REAL
B is Element of the carrier of (Euclid 2)
Ball (B,A) is Element of K6( the carrier of (Euclid 2))
K6( the carrier of (Euclid 2)) is set
(Ball (B,A)) ` is Element of K6( the carrier of (Euclid 2))
the carrier of (Euclid 2) \ (Ball (B,A)) is set
{} (TOP-REAL 2) is empty Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V56() open connected compact bounded Element of K6( the carrier of (TOP-REAL 2))
q is Element of the carrier of (Euclid 2)
Ball (q,1) is Element of K6( the carrier of (Euclid 2))
a is Element of K6( the carrier of (TOP-REAL 2))
p is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
p `1 is V11() real ext-real Element of REAL
p `2 is V11() real ext-real Element of REAL
AffineMap (A,(p `1),A,(p `2)) is non empty V16() V19( the carrier of (TOP-REAL 2)) V20( the carrier of (TOP-REAL 2)) Function-like V26( the carrier of (TOP-REAL 2)) quasi_total V94( TOP-REAL 2, TOP-REAL 2) Element of K6(K7( the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2)))
r is Element of K6( the carrier of (TOP-REAL 2))
(AffineMap (A,(p `1),A,(p `2))) .: r is Element of K6( the carrier of (TOP-REAL 2))
a ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ a is set
r ` is Element of K6( the carrier of (TOP-REAL 2))
the carrier of (TOP-REAL 2) \ r is set
s is Element of K6( the carrier of (TOP-REAL 2))
(REAL 2) \ (Ball (q,1)) is Element of K6((REAL 2))
K6((REAL 2)) is set
{ b1 where b1 is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2) : not 1 <= |.b1.| } is set
(REAL 2) \ { b1 where b1 is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2) : not 1 <= |.b1.| } is Element of K6((REAL 2))
r is Element of K6( the carrier of (TOP-REAL 2))
(AffineMap (A,(p `1),A,(p `2))) .: s is Element of K6( the carrier of (TOP-REAL 2))
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
Euclid A is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL A is non empty V72() M12( REAL )
K257(A,REAL) is V72() M12( REAL )
Pitag_dist A is V16() V19(K7((REAL A),(REAL A))) V20( REAL ) Function-like quasi_total V33() V34() V35() Element of K6(K7(K7((REAL A),(REAL A)),REAL))
K7((REAL A),(REAL A)) is set
K7(K7((REAL A),(REAL A)),REAL) is V33() V34() V35() set
K6(K7(K7((REAL A),(REAL A)),REAL)) is set
MetrStruct(# (REAL A),(Pitag_dist A) #) is strict MetrStruct
TopSpaceMetr (Euclid A) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid A)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid A))) is set
B is Element of K6( the carrier of (TOP-REAL A))
P is Element of K6( the carrier of (TOP-REAL A))
the topology of (TOP-REAL A) is Element of K6(K6( the carrier of (TOP-REAL A)))
K6(K6( the carrier of (TOP-REAL A))) is set
TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is strict TopStruct
p is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
q is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
min_dist_min (p,q) is V11() real ext-real Element of REAL
a is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
r is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
p is V11() real ext-real Element of REAL
min_dist_min (a,r) is V11() real ext-real Element of REAL
r is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
s is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
q is V11() real ext-real Element of REAL
min_dist_min (r,s) is V11() real ext-real Element of REAL
A is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
TopSpaceMetr A is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr A) is non empty set
K6( the carrier of (TopSpaceMetr A)) is set
p is non empty compact Element of K6( the carrier of (TopSpaceMetr A))
q is non empty compact Element of K6( the carrier of (TopSpaceMetr A))
min_dist_min (p,q) is V11() real ext-real Element of REAL
min_dist_min (q,p) is V11() real ext-real Element of REAL
the carrier of A is non empty set
a is Element of the carrier of A
r is Element of the carrier of A
dist (a,r) is V11() real ext-real Element of REAL
r is Element of the carrier of A
s is Element of the carrier of A
dist (r,s) is V11() real ext-real Element of REAL
p is non empty compact Element of K6( the carrier of (TopSpaceMetr A))
q is non empty compact Element of K6( the carrier of (TopSpaceMetr A))
max_dist_max (p,q) is V11() real ext-real Element of REAL
max_dist_max (q,p) is V11() real ext-real Element of REAL
the carrier of A is non empty set
a is Element of the carrier of A
r is Element of the carrier of A
dist (a,r) is V11() real ext-real Element of REAL
r is Element of the carrier of A
s is Element of the carrier of A
dist (r,s) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
p is non empty compact bounded Element of K6( the carrier of (TOP-REAL A))
q is non empty compact bounded Element of K6( the carrier of (TOP-REAL A))
(A,p,q) is V11() real ext-real Element of REAL
(A,q,p) is V11() real ext-real Element of REAL
Euclid A is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL A is non empty V72() M12( REAL )
K257(A,REAL) is V72() M12( REAL )
Pitag_dist A is V16() V19(K7((REAL A),(REAL A))) V20( REAL ) Function-like quasi_total V33() V34() V35() Element of K6(K7(K7((REAL A),(REAL A)),REAL))
K7((REAL A),(REAL A)) is set
K7(K7((REAL A),(REAL A)),REAL) is V33() V34() V35() set
K6(K7(K7((REAL A),(REAL A)),REAL)) is set
MetrStruct(# (REAL A),(Pitag_dist A) #) is strict MetrStruct
TopSpaceMetr (Euclid A) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid A)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid A))) is set
a is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
r is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
min_dist_min (a,r) is V11() real ext-real Element of REAL
the topology of (TOP-REAL A) is Element of K6(K6( the carrier of (TOP-REAL A)))
K6(K6( the carrier of (TOP-REAL A))) is set
TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is strict TopStruct
s is non empty compact Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
r is non empty compact Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
((Euclid A),s,r) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
B is non empty Element of K6( the carrier of (TOP-REAL A))
P is non empty Element of K6( the carrier of (TOP-REAL A))
(A,B,P) is V11() real ext-real Element of REAL
Euclid A is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL A is non empty V72() M12( REAL )
K257(A,REAL) is V72() M12( REAL )
Pitag_dist A is V16() V19(K7((REAL A),(REAL A))) V20( REAL ) Function-like quasi_total V33() V34() V35() Element of K6(K7(K7((REAL A),(REAL A)),REAL))
K7((REAL A),(REAL A)) is set
K7(K7((REAL A),(REAL A)),REAL) is V33() V34() V35() set
K6(K7(K7((REAL A),(REAL A)),REAL)) is set
MetrStruct(# (REAL A),(Pitag_dist A) #) is strict MetrStruct
TopSpaceMetr (Euclid A) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid A)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid A))) is set
p is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
q is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
min_dist_min (p,q) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
B is compact bounded Element of K6( the carrier of (TOP-REAL A))
P is compact bounded Element of K6( the carrier of (TOP-REAL A))
(A,B,P) is V11() real ext-real Element of REAL
Euclid A is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL A is non empty V72() M12( REAL )
K257(A,REAL) is V72() M12( REAL )
Pitag_dist A is V16() V19(K7((REAL A),(REAL A))) V20( REAL ) Function-like quasi_total V33() V34() V35() Element of K6(K7(K7((REAL A),(REAL A)),REAL))
K7((REAL A),(REAL A)) is set
K7(K7((REAL A),(REAL A)),REAL) is V33() V34() V35() set
K6(K7(K7((REAL A),(REAL A)),REAL)) is set
MetrStruct(# (REAL A),(Pitag_dist A) #) is strict MetrStruct
TopSpaceMetr (Euclid A) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid A)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid A))) is set
p is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
q is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
min_dist_min (p,q) is V11() real ext-real Element of REAL
the topology of (TOP-REAL A) is Element of K6(K6( the carrier of (TOP-REAL A)))
K6(K6( the carrier of (TOP-REAL A))) is set
TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is strict TopStruct
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
B is V11() real ext-real Element of REAL
P is non empty Element of K6( the carrier of (TOP-REAL A))
p is non empty Element of K6( the carrier of (TOP-REAL A))
(A,P,p) is V11() real ext-real Element of REAL
Euclid A is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL A is non empty V72() M12( REAL )
K257(A,REAL) is V72() M12( REAL )
Pitag_dist A is V16() V19(K7((REAL A),(REAL A))) V20( REAL ) Function-like quasi_total V33() V34() V35() Element of K6(K7(K7((REAL A),(REAL A)),REAL))
K7((REAL A),(REAL A)) is set
K7(K7((REAL A),(REAL A)),REAL) is V33() V34() V35() set
K6(K7(K7((REAL A),(REAL A)),REAL)) is set
MetrStruct(# (REAL A),(Pitag_dist A) #) is strict MetrStruct
the carrier of (Euclid A) is non empty set
q is Element of the carrier of (Euclid A)
a is Element of the carrier of (Euclid A)
dist (q,a) is V11() real ext-real Element of REAL
r is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
r is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
dist (r,r) is V11() real ext-real Element of REAL
s is Element of the carrier of (Euclid A)
q9 is Element of the carrier of (Euclid A)
dist (s,q9) is V11() real ext-real Element of REAL
TopSpaceMetr (Euclid A) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid A)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid A))) is set
q is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
a is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
min_dist_min (q,a) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
B is Element of K6( the carrier of (TOP-REAL A))
p is non empty Element of K6( the carrier of (TOP-REAL A))
P is non empty Element of K6( the carrier of (TOP-REAL A))
(A,P,B) is V11() real ext-real Element of REAL
(A,P,p) is V11() real ext-real Element of REAL
Euclid A is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL A is non empty V72() M12( REAL )
K257(A,REAL) is V72() M12( REAL )
Pitag_dist A is V16() V19(K7((REAL A),(REAL A))) V20( REAL ) Function-like quasi_total V33() V34() V35() Element of K6(K7(K7((REAL A),(REAL A)),REAL))
K7((REAL A),(REAL A)) is set
K7(K7((REAL A),(REAL A)),REAL) is V33() V34() V35() set
K6(K7(K7((REAL A),(REAL A)),REAL)) is set
MetrStruct(# (REAL A),(Pitag_dist A) #) is strict MetrStruct
TopSpaceMetr (Euclid A) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid A)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid A))) is set
q is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
a is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
min_dist_min (q,a) is V11() real ext-real Element of REAL
K7( the carrier of (TopSpaceMetr (Euclid A)),REAL) is V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr (Euclid A)),REAL)) is set
dist_min q is non empty V16() V19( the carrier of (TopSpaceMetr (Euclid A))) V20( the carrier of K484()) Function-like V26( the carrier of (TopSpaceMetr (Euclid A))) quasi_total V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr (Euclid A)), the carrier of K484()))
K7( the carrier of (TopSpaceMetr (Euclid A)), the carrier of K484()) is V33() V34() V35() set
K6(K7( the carrier of (TopSpaceMetr (Euclid A)), the carrier of K484())) is set
r is V16() V19( the carrier of (TopSpaceMetr (Euclid A))) V20( REAL ) Function-like quasi_total V33() V34() V35() Element of K6(K7( the carrier of (TopSpaceMetr (Euclid A)),REAL))
r .: a is V45() V46() V47() Element of K6(REAL)
r is V45() V46() V47() Element of K6(REAL)
s is ext-real set
q9 is Element of the carrier of (TopSpaceMetr (Euclid A))
r . q9 is V11() real ext-real Element of REAL
lower_bound r is V11() real ext-real Element of REAL
(dist_min q) .: a is V45() V46() V47() Element of K6( the carrier of K484())
[#] ((dist_min q) .: a) is V45() V46() V47() Element of K6(REAL)
lower_bound ([#] ((dist_min q) .: a)) is V11() real ext-real Element of REAL
lower_bound ((dist_min q) .: a) is V11() real ext-real Element of REAL
s is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
q9 is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
min_dist_min (s,q9) is V11() real ext-real Element of REAL
dom r is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
r .: q9 is V45() V46() V47() Element of K6(REAL)
X is non empty V45() V46() V47() Element of K6(REAL)
lower_bound X is V11() real ext-real Element of REAL
(dist_min q) .: q9 is V45() V46() V47() Element of K6( the carrier of K484())
[#] ((dist_min q) .: q9) is V45() V46() V47() Element of K6(REAL)
lower_bound ([#] ((dist_min q) .: q9)) is V11() real ext-real Element of REAL
lower_bound ((dist_min q) .: q9) is V11() real ext-real Element of REAL
min_dist_min (q,q9) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
B is non empty compact bounded Element of K6( the carrier of (TOP-REAL A))
P is non empty compact bounded Element of K6( the carrier of (TOP-REAL A))
(A,B,P) is V11() real ext-real Element of REAL
Euclid A is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL A is non empty V72() M12( REAL )
K257(A,REAL) is V72() M12( REAL )
Pitag_dist A is V16() V19(K7((REAL A),(REAL A))) V20( REAL ) Function-like quasi_total V33() V34() V35() Element of K6(K7(K7((REAL A),(REAL A)),REAL))
K7((REAL A),(REAL A)) is set
K7(K7((REAL A),(REAL A)),REAL) is V33() V34() V35() set
K6(K7(K7((REAL A),(REAL A)),REAL)) is set
MetrStruct(# (REAL A),(Pitag_dist A) #) is strict MetrStruct
TopSpaceMetr (Euclid A) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid A)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid A))) is set
p is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
q is Element of K6( the carrier of (TopSpaceMetr (Euclid A)))
min_dist_min (p,q) is V11() real ext-real Element of REAL
the topology of (TOP-REAL A) is Element of K6(K6( the carrier of (TOP-REAL A)))
K6(K6( the carrier of (TOP-REAL A))) is set
TopStruct(# the carrier of (TOP-REAL A), the topology of (TOP-REAL A) #) is strict TopStruct
the carrier of (Euclid A) is non empty set
a is Element of the carrier of (Euclid A)
r is Element of the carrier of (Euclid A)
dist (a,r) is V11() real ext-real Element of REAL
r is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
s is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
dist (r,s) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
B is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
{B} is non empty functional V52() compact bounded Element of K6( the carrier of (TOP-REAL A))
K6( the carrier of (TOP-REAL A)) is set
P is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
{P} is non empty functional V52() compact bounded Element of K6( the carrier of (TOP-REAL A))
(A,{B},{P}) is V11() real ext-real Element of REAL
dist (B,P) is V11() real ext-real Element of REAL
p is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
q is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
dist (p,q) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
B is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
{B} is non empty functional V52() compact bounded Element of K6( the carrier of (TOP-REAL A))
P is Element of K6( the carrier of (TOP-REAL A))
(A,{B},P) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
P is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
B is non empty Element of K6( the carrier of (TOP-REAL A))
(A,P,B) is V11() real ext-real Element of REAL
{P} is non empty functional V52() compact bounded Element of K6( the carrier of (TOP-REAL A))
(A,{P},B) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
P is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
B is compact bounded Element of K6( the carrier of (TOP-REAL A))
(A,P,B) is V11() real ext-real Element of REAL
{P} is non empty functional V52() compact bounded Element of K6( the carrier of (TOP-REAL A))
(A,{P},B) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
B is non empty compact bounded Element of K6( the carrier of (TOP-REAL A))
P is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
(A,P,B) is V11() real ext-real Element of REAL
{P} is non empty functional V52() compact bounded Element of K6( the carrier of (TOP-REAL A))
(A,{P},B) is V11() real ext-real Element of REAL
(A,B,{P}) is V11() real ext-real Element of REAL
p is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
q is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
dist (p,q) is V11() real ext-real Element of REAL
dist (P,p) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
B is non empty Element of K6( the carrier of (TOP-REAL A))
P is Element of K6( the carrier of (TOP-REAL A))
p is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
(A,p,P) is V11() real ext-real Element of REAL
{p} is non empty functional V52() compact bounded Element of K6( the carrier of (TOP-REAL A))
(A,{p},P) is V11() real ext-real Element of REAL
(A,p,B) is V11() real ext-real Element of REAL
(A,{p},B) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
B is V11() real ext-real Element of REAL
P is non empty Element of K6( the carrier of (TOP-REAL A))
p is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
(A,p,P) is V11() real ext-real Element of REAL
{p} is non empty functional V52() compact bounded Element of K6( the carrier of (TOP-REAL A))
(A,{p},P) is V11() real ext-real Element of REAL
q is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
a is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
dist (q,a) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
B is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
P is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
{P} is non empty functional V52() compact bounded Element of K6( the carrier of (TOP-REAL A))
K6( the carrier of (TOP-REAL A)) is set
(A,B,{P}) is V11() real ext-real Element of REAL
{B} is non empty functional V52() compact bounded Element of K6( the carrier of (TOP-REAL A))
(A,{B},{P}) is V11() real ext-real Element of REAL
dist (B,P) is V11() real ext-real Element of REAL
A is natural V11() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() Element of NAT
TOP-REAL A is non empty TopSpace-like V140() V184() V185() V225() V226() V227() V228() V229() V230() V231() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL A) is non empty set
K6( the carrier of (TOP-REAL A)) is set
B is non empty Element of K6( the carrier of (TOP-REAL A))
p is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
P is V16() Function-like V33() V34() V35() V69(A) V70() Element of the carrier of (TOP-REAL A)
(A,P,B) is V11() real ext-real Element of REAL
{P} is non empty functional V52() compact bounded Element of K6( the carrier of (TOP-REAL A))
(A,{P},B) is V11() real ext-real Element of REAL
dist (P,p) is V11() real ext-real Element of REAL
{p} is non empty functional V52() compact bounded Element of K6( the carrier of (TOP-REAL A))
(A,P,{p}) is V11() real ext-real Element of REAL
(A,{P},{p}) is V11() real ext-real Element of REAL
A is non empty compact bounded Element of K6( the carrier of (TOP-REAL 2))
B is open Element of K6( the carrier of (TOP-REAL 2))
the topology of (TOP-REAL 2) is Element of K6(K6( the carrier of (TOP-REAL 2)))
K6(K6( the carrier of (TOP-REAL 2))) is set
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is strict TopStruct
TopSpaceMetr (Euclid 2) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid 2)) is non empty set
K6( the carrier of (TopSpaceMetr (Euclid 2))) is set
p is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
(2,p,A) is V11() real ext-real Element of REAL
{p} is non empty functional V52() compact bounded Element of K6( the carrier of (TOP-REAL 2))
(2,{p},A) is V11() real ext-real Element of REAL
(2,p,B) is V11() real ext-real Element of REAL
(2,{p},B) is V11() real ext-real Element of REAL
q is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
dist (p,q) is V11() real ext-real Element of REAL
a is Element of the carrier of (Euclid 2)
P is open Element of K6( the carrier of (TopSpaceMetr (Euclid 2)))
r is V11() real ext-real set
Ball (a,r) is Element of K6( the carrier of (Euclid 2))
K6( the carrier of (Euclid 2)) is set
r is V11() real ext-real Element of REAL
2 * (dist (p,q)) is V11() real ext-real Element of REAL
r / (2 * (dist (p,q))) is V11() real ext-real Element of REAL
1 - (r / (2 * (dist (p,q)))) is V11() real ext-real Element of REAL
(1 - (r / (2 * (dist (p,q))))) * q is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(q,(1 - (r / (2 * (dist (p,q)))))) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
(r / (2 * (dist (p,q)))) * p is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K371(p,(r / (2 * (dist (p,q))))) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p) is V16() Function-like V33() V34() V35() V69(2) V70() Element of the carrier of (TOP-REAL 2)
K365(((1 - (r / (2 * (dist (p,q))))) * q),((r / (2 * (dist (p,q)))) * p)) is V16() V19( NAT ) V20( REAL ) Function-like V33() V34() V35() V70() M11( REAL )
1 - 0 is non empty V11() real ext-real positive non negative Element of REAL
dist (q,(((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p))) is V11() real ext-real Element of REAL
1 * r is V11() real ext-real Element of REAL
(1 * r) / (2 * (dist (p,q))) is V11() real ext-real Element of REAL
((1 * r) / (2 * (dist (p,q)))) * (dist (p,q)) is V11() real ext-real Element of REAL
r / 2 is V11() real ext-real Element of REAL
(dist (p,q)) / 1 is V11() real ext-real Element of REAL
(r / 2) / ((dist (p,q)) / 1) is V11() real ext-real Element of REAL
((r / 2) / ((dist (p,q)) / 1)) * (dist (p,q)) is V11() real ext-real Element of REAL
r / 1 is V11() real ext-real Element of REAL
Ball (a,r) is Element of K6( the carrier of (Euclid 2))
X is Element of the carrier of (Euclid 2)
z2 is Element of the carrier of (Euclid 2)
dist (X,z2) is V11() real ext-real Element of REAL
X is Element of the carrier of (Euclid 2)
z2 is Element of the carrier of (Euclid 2)
dist (X,z2) is V11() real ext-real Element of REAL
dist (p,(((1 - (r / (2 * (dist (p,q))))) * q) + ((r / (2 * (dist (p,q)))) * p))) is V11() real ext-real Element of REAL
(1 - (r / (2 * (dist (p,q))))) * (dist (p,q)) is V11() real ext-real Element of REAL