:: NAGATA_1 semantic presentation

REAL is non empty non trivial non finite V130() V131() V132() V136() set
NAT is non empty non trivial non finite countable denumerable V130() V131() V132() V133() V134() V135() V136() Element of bool REAL
bool REAL is non empty set
K490() is V130() V131() V132() Element of bool REAL
omega is non empty non trivial non finite countable denumerable V130() V131() V132() V133() V134() V135() V136() set
bool omega is non empty set
[:NAT,REAL:] is non empty V119() V120() V121() set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
bool NAT is non empty set
K96(NAT) is V24() set
COMPLEX is non empty non trivial non finite V130() V136() set
1 is non empty ordinal natural V33() real ext-real positive non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
INT is non empty non trivial non finite V130() V131() V132() V133() V134() V136() set
[:1,1:] is RAT -valued INT -valued non empty V119() V120() V121() V122() set
RAT is non empty non trivial non finite V130() V131() V132() V133() V136() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is RAT -valued INT -valued non empty V119() V120() V121() V122() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty V119() V120() V121() set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is non empty V119() V120() V121() set
[:[:REAL,REAL:],REAL:] is non empty V119() V120() V121() set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty ordinal natural V33() real ext-real positive non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
[:2,2:] is RAT -valued INT -valued non empty V119() V120() V121() V122() set
[:[:2,2:],REAL:] is non empty V119() V120() V121() set
bool [:[:2,2:],REAL:] is non empty set
bool [:REAL,REAL:] is non empty set
K456(2) is V190() L15()
the carrier of K456(2) is set
[: the carrier of K456(2),REAL:] is V119() V120() V121() set
bool [: the carrier of K456(2),REAL:] is non empty set
bool the carrier of K456(2) is non empty set
K550() is non empty strict TopSpace-like V213() TopStruct
the carrier of K550() is non empty V130() V131() V132() set
RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V213() MetrStruct
R^1 is non empty strict TopSpace-like V213() TopStruct
K491() is V130() V131() V132() Element of bool REAL
ExtREAL is non empty V131() set
bool ExtREAL is non empty set
the carrier of R^1 is non empty V130() V131() V132() set
{} is Function-like functional empty trivial finite V45() countable FinSequence-membered V130() V131() V132() V133() V134() V135() V136() set
3 is non empty ordinal natural V33() real ext-real positive non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
0 is Function-like functional empty trivial ordinal natural V33() real ext-real non positive non negative finite V45() countable FinSequence-membered V63() V129() V130() V131() V132() V133() V134() V135() V136() Element of NAT
real_dist is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty V14([:REAL,REAL:]) quasi_total V119() V120() V121() Element of bool [:[:REAL,REAL:],REAL:]
MetrStruct(# REAL,real_dist #) is strict MetrStruct
the carrier of RealSpace is non empty V130() V131() V132() set
TopSpaceMetr RealSpace is TopStruct
Family_open_set RealSpace is Element of bool (bool the carrier of RealSpace)
bool the carrier of RealSpace is non empty set
bool (bool the carrier of RealSpace) is non empty set
TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) is non empty strict TopStruct
len omega is cardinal set
T is V33() real ext-real Element of REAL
r is V33() real ext-real Element of REAL
m is V33() real ext-real Element of REAL
T + r is V33() real ext-real Element of REAL
m + 0 is V33() real ext-real Element of REAL
r + T is V33() real ext-real Element of REAL
T is V33() real ext-real Element of REAL
a is V33() real ext-real Element of REAL
T - a is V33() real ext-real Element of REAL
abs (T - a) is V33() real ext-real Element of REAL
r is V33() real ext-real Element of REAL
T - r is V33() real ext-real Element of REAL
abs (T - r) is V33() real ext-real Element of REAL
m is V33() real ext-real Element of REAL
r - m is V33() real ext-real Element of REAL
abs (r - m) is V33() real ext-real Element of REAL
(abs (T - r)) + (abs (r - m)) is V33() real ext-real Element of REAL
m - a is V33() real ext-real Element of REAL
abs (m - a) is V33() real ext-real Element of REAL
((abs (T - r)) + (abs (r - m))) + (abs (m - a)) is V33() real ext-real Element of REAL
r - a is V33() real ext-real Element of REAL
(r - m) + (m - a) is V33() real ext-real Element of REAL
abs (r - a) is V33() real ext-real Element of REAL
(abs (r - m)) + (abs (m - a)) is V33() real ext-real Element of REAL
(abs (T - r)) + (abs (r - a)) is V33() real ext-real Element of REAL
(abs (T - r)) + ((abs (r - m)) + (abs (m - a))) is V33() real ext-real Element of REAL
(T - r) + (r - a) is V33() real ext-real Element of REAL
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{. the carrier of T,.} is non empty finite countable set
m is set
m is Element of bool (bool the carrier of T)
a is Element of the carrier of T
[#] T is non empty non proper open closed Element of bool the carrier of T
b is non empty non proper open closed Element of bool the carrier of T
c is Element of bool the carrier of T
ft is Element of bool the carrier of T
b /\ c is Element of bool the carrier of T
b /\ ft is Element of bool the carrier of T
c is Element of bool the carrier of T
ft is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of the carrier of T
[#] T is non empty non proper open closed Element of bool the carrier of T
a is Element of bool the carrier of T
b is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool the carrier of T
{m} is non empty trivial finite countable Element of bool (bool the carrier of T)
m is Element of bool the carrier of T
{m} is non empty trivial finite countable Element of bool (bool the carrier of T)
[#] T is non empty non proper open closed Element of bool the carrier of T
a is Element of the carrier of T
b is non empty non proper open closed Element of bool the carrier of T
c is Element of bool the carrier of T
ft is Element of bool the carrier of T
{c} is non empty trivial finite countable Element of bool (bool the carrier of T)
{ft} is non empty trivial finite countable Element of bool (bool the carrier of T)
c is Element of bool the carrier of T
ft is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool (bool the carrier of T)
a is Element of the carrier of T
b is open Element of bool the carrier of T
c is open Element of bool the carrier of T
ft is Element of bool the carrier of T
R is Element of bool the carrier of T
b is open Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool (bool the carrier of T)
r /\ m is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool (bool the carrier of T)
r \ m is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool (bool the carrier of T)
INTERSECTION (r,m) is set
a is Element of bool (bool the carrier of T)
b is Element of the carrier of T
c is open Element of bool the carrier of T
ft is open Element of bool the carrier of T
R is Element of bool the carrier of T
s is Element of bool the carrier of T
B is set
U is set
B /\ U is set
c /\ ft is open Element of bool the carrier of T
mfx is set
x is set
mfx /\ x is set
(c /\ ft) /\ (mfx /\ x) is Element of bool the carrier of T
(c /\ ft) /\ mfx is Element of bool the carrier of T
((c /\ ft) /\ mfx) /\ x is Element of bool the carrier of T
c /\ mfx is Element of bool the carrier of T
(c /\ mfx) /\ ft is Element of bool the carrier of T
((c /\ mfx) /\ ft) /\ x is Element of bool the carrier of T
(c /\ ft) /\ (B /\ U) is Element of bool the carrier of T
(c /\ ft) /\ B is Element of bool the carrier of T
((c /\ ft) /\ B) /\ U is Element of bool the carrier of T
c /\ B is Element of bool the carrier of T
(c /\ B) /\ ft is Element of bool the carrier of T
((c /\ B) /\ ft) /\ U is Element of bool the carrier of T
ft /\ U is Element of bool the carrier of T
(c /\ B) /\ (ft /\ U) is Element of bool the carrier of T
ft /\ x is Element of bool the carrier of T
(c /\ mfx) /\ (ft /\ x) is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool the carrier of T
a is Element of bool the carrier of T
m /\ a is Element of bool the carrier of T
{} T is Function-like functional empty trivial proper finite V45() countable FinSequence-membered open closed compact V130() V131() V132() V133() V134() V135() V136() Element of bool the carrier of T
b is Element of the carrier of T
c is open Element of bool the carrier of T
{b} is non empty trivial finite countable compact Element of bool the carrier of T
c /\ a is Element of bool the carrier of T
c /\ m is Element of bool the carrier of T
{..} is non empty trivial finite V45() countable set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of the carrier of T
a is open Element of bool the carrier of T
{a} is non empty trivial finite countable Element of bool (bool the carrier of T)
INTERSECTION ({a},r) is set
c is set
ft is set
R is set
s is set
R /\ s is set
B is set
U is set
B /\ U is set
{..} is non empty trivial finite countable set
{..} is non empty trivial finite countable set
c is set
{.c,.} is non empty finite countable set
ft is set
(INTERSECTION ({a},r)) \ {..} is Element of bool (INTERSECTION ({a},r))
bool (INTERSECTION ({a},r)) is non empty set
c is set
{.c,.} is non empty finite countable set
ft is set
{..} is non empty trivial finite countable set
{..} is non empty trivial finite countable set
{..} \/ {..} is non empty finite countable set
(INTERSECTION ({a},r)) \ {..} is Element of bool (INTERSECTION ({a},r))
bool (INTERSECTION ({a},r)) is non empty set
(INTERSECTION ({a},r)) \ {..} is Element of bool (INTERSECTION ({a},r))
bool (INTERSECTION ({a},r)) is non empty set
(INTERSECTION ({a},r)) \ {..} is Element of bool (INTERSECTION ({a},r))
bool (INTERSECTION ({a},r)) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool (bool the carrier of T)
a is Element of the carrier of T
b is open Element of bool the carrier of T
{b} is non empty trivial finite countable Element of bool (bool the carrier of T)
INTERSECTION ({b},m) is set
(INTERSECTION ({b},m)) \ {..} is Element of bool (INTERSECTION ({b},m))
bool (INTERSECTION ({b},m)) is non empty set
c is Element of bool the carrier of T
ft is Element of bool the carrier of T
b /\ ft is Element of bool the carrier of T
s is set
{..} is non empty trivial finite countable set
{(b /\ ft)} is non empty trivial finite countable Element of bool (bool the carrier of T)
b /\ c is Element of bool the carrier of T
B is set
{(b /\ c)} is non empty trivial finite countable Element of bool (bool the carrier of T)
c /\ ft is Element of bool the carrier of T
a is Element of the carrier of T
b is Element of bool the carrier of T
c is Element of bool the carrier of T
ft is Element of the carrier of T
R is Element of bool the carrier of T
s is Element of bool the carrier of T
m is Element of the carrier of T
a is Element of bool the carrier of T
b is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
r is open Element of bool the carrier of T
m is Element of bool the carrier of T
Cl m is closed Element of bool the carrier of T
r ` is closed Element of bool the carrier of T
the carrier of T \ r is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is (T) Element of bool (bool the carrier of T)
clf r is Element of bool (bool the carrier of T)
m is Element of the carrier of T
a is open Element of bool the carrier of T
b is Element of bool the carrier of T
c is Element of bool the carrier of T
ft is Element of bool the carrier of T
Cl ft is closed Element of bool the carrier of T
R is Element of bool the carrier of T
Cl R is closed Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
union r is Element of bool the carrier of T
Cl (union r) is closed Element of bool the carrier of T
m is Element of bool the carrier of T
Cl m is closed Element of bool the carrier of T
a is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of bool the carrier of T
Cl m is closed Element of bool the carrier of T
a is Element of bool the carrier of T
m /\ a is Element of bool the carrier of T
Cl (m /\ a) is closed Element of bool the carrier of T
Cl a is closed Element of bool the carrier of T
(Cl m) /\ (Cl a) is closed Element of bool the carrier of T
{} T is Function-like functional empty trivial proper finite V45() countable FinSequence-membered open closed compact V130() V131() V132() V133() V134() V135() V136() Element of bool the carrier of T
b is set
c is open Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
union r is Element of bool the carrier of T
Cl (union r) is closed Element of bool the carrier of T
clf r is Element of bool (bool the carrier of T)
union (clf r) is Element of bool the carrier of T
m is set
a is open Element of bool the carrier of T
b is set
c is set
ft is Element of bool the carrier of T
R is Element of bool the carrier of T
R is Element of bool the carrier of T
R /\ a is Element of bool the carrier of T
s is set
B is set
R /\ B is Element of bool the carrier of T
a /\ B is Element of bool the carrier of T
Cl ft is closed Element of bool the carrier of T
m is set
a is set
b is Element of bool the carrier of T
c is Element of bool the carrier of T
Cl c is closed Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Element of bool (bool the carrier of T)
m is Element of the carrier of T
a is open Element of bool the carrier of T
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of T : ( b<sub>1</sub> in r & not b<sub>1</sub> misses a ) } is set
c is open Element of bool the carrier of T
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of T : ( b<sub>1</sub> in r & not b<sub>1</sub> misses c ) } is set
ft is set
R is Element of bool the carrier of T
s is set
B is Element of bool the carrier of T
{R} is non empty trivial finite countable Element of bool (bool the carrier of T)
ft is Element of bool the carrier of T
{ft} is non empty trivial finite countable Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
r is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
m is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r . m is set
r . m is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
r is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
Union r is set
Union r is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
{..} is non empty trivial finite countable set
NAT --> {..} is Relation-like NAT -defined {..} -valued Function-like non empty non trivial V14( NAT ) quasi_total non finite Element of bool [:NAT,{..}:]
{..} is non empty trivial finite V45() countable set
[:NAT,{..}:] is non empty set
bool [:NAT,{..}:] is non empty set
m is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
a is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,m,a) is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
T is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
r is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
m is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,r,m) is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
r is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
m is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,r,m) is Element of bool (bool the carrier of T)
T is non empty non countable set
[:T,T:] is non empty set
1TopSp [:T,T:] is non empty strict TopSpace-like TopStruct
bool [:T,T:] is non empty Element of bool (bool [:T,T:])
bool [:T,T:] is non empty set
bool (bool [:T,T:]) is non empty set
[#] (bool [:T,T:]) is non empty non proper Element of bool (bool [:T,T:])
bool (bool [:T,T:]) is non empty set
TopStruct(# [:T,T:],([#] (bool [:T,T:])) #) is non empty strict TopStruct
the carrier of (1TopSp [:T,T:]) is non empty set
bool the carrier of (1TopSp [:T,T:]) is non empty set
bool (bool the carrier of (1TopSp [:T,T:])) is non empty set
{ ([:{b<sub>1</sub>},T:] \/ [:T,{b<sub>1</sub>}:]) where b<sub>1</sub> is Element of T : b<sub>1</sub> in T } is set
a is set
b is Element of T
{b} is non empty trivial finite countable Element of bool T
bool T is non empty set
[:{b},T:] is non empty set
[:T,{b}:] is non empty set
[:{b},T:] \/ [:T,{b}:] is non empty set
a is Element of bool (bool the carrier of (1TopSp [:T,T:]))
b is Element of the carrier of (1TopSp [:T,T:])
{b} is non empty trivial finite countable compact Element of bool the carrier of (1TopSp [:T,T:])
R is set
s is set
[R,s] is non empty set
{.s,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
{..} is non empty trivial finite countable set
[:{..},T:] is non empty set
[:T,{..}:] is non empty set
[:{..},T:] \/ [:T,{..}:] is non empty set
{..} is non empty trivial finite countable set
[:{..},T:] is non empty set
[:T,{..}:] is non empty set
[:{..},T:] \/ [:T,{..}:] is non empty set
{..} is non empty trivial finite countable set
ft is Element of bool the carrier of (1TopSp [:T,T:])
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of (1TopSp [:T,T:]) : ( b<sub>1</sub> in a & not b<sub>1</sub> misses ft ) } is set
{..} \/ {..} is non empty finite countable set
x is set
x is Element of bool the carrier of (1TopSp [:T,T:])
fx is set
fx is Element of T
{fx} is non empty trivial finite countable Element of bool T
bool T is non empty set
[:{fx},T:] is non empty set
[:T,{fx}:] is non empty set
[:{fx},T:] \/ [:T,{fx}:] is non empty set
b is set
c is Element of T
{c} is non empty trivial finite countable Element of bool T
bool T is non empty set
[:{c},T:] is non empty set
[:T,{c}:] is non empty set
[:{c},T:] \/ [:T,{c}:] is non empty set
len T is cardinal set
len a is cardinal set
R is Relation-like Function-like set
dom R is set
s is set
B is set
R . s is set
R . B is set
{..} is non empty trivial finite countable set
[s,s] is non empty set
{.s,.} is non empty finite countable set
{.{..},.} is non empty finite V45() countable set
[:{..},T:] is non empty set
[:T,{..}:] is non empty set
[:{..},T:] \/ [:T,{..}:] is non empty set
{..} is non empty trivial finite countable set
[:{..},T:] is non empty set
[:T,{..}:] is non empty set
[:{..},T:] \/ [:T,{..}:] is non empty set
rng R is set
s is set
B is set
R . B is set
U is Element of T
{U} is non empty trivial finite countable Element of bool T
[:{U},T:] is non empty set
[:T,{U}:] is non empty set
[:{U},T:] \/ [:T,{U}:] is non empty set
[:NAT,(bool (bool the carrier of (1TopSp [:T,T:]))):] is non empty set
bool [:NAT,(bool (bool the carrier of (1TopSp [:T,T:]))):] is non empty set
R is Relation-like NAT -defined bool (bool the carrier of (1TopSp [:T,T:])) -valued Function-like non empty V14( NAT ) quasi_total ( 1TopSp [:T,T:]) Element of bool [:NAT,(bool (bool the carrier of (1TopSp [:T,T:]))):]
((1TopSp [:T,T:]),R) is Element of bool (bool the carrier of (1TopSp [:T,T:]))
s is set
R . s is set
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
((1TopSp [:T,T:]),R,B) is Element of bool (bool the carrier of (1TopSp [:T,T:]))
R . B is set
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
((1TopSp [:T,T:]),R,B) is Element of bool (bool the carrier of (1TopSp [:T,T:]))
U is set
R . B is set
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
((1TopSp [:T,T:]),R,B) is Element of bool (bool the carrier of (1TopSp [:T,T:]))
R . B is set
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
R . B is set
U is set
[:NAT,a:] is set
bool [:NAT,a:] is non empty set
s is Relation-like NAT -defined a -valued Function-like quasi_total Element of bool [:NAT,a:]
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
R . B is set
U is Element of a
mfx is Element of a
((1TopSp [:T,T:]),R,B) is Element of bool (bool the carrier of (1TopSp [:T,T:]))
x is Element of T
{x} is non empty trivial finite countable Element of bool T
[:{x},T:] is non empty set
[:T,{x}:] is non empty set
[:{x},T:] \/ [:T,{x}:] is non empty set
x is Element of T
{x} is non empty trivial finite countable Element of bool T
[:{x},T:] is non empty set
[:T,{x}:] is non empty set
[:{x},T:] \/ [:T,{x}:] is non empty set
[x,x] is non empty Element of [:T,T:]
{.x,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
s .: NAT is Element of bool a
bool a is non empty set
B is set
U is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
((1TopSp [:T,T:]),R,U) is Element of bool (bool the carrier of (1TopSp [:T,T:]))
s . U is Element of a
R . U is set
dom s is countable V130() V131() V132() V133() V134() V135() Element of bool NAT
len NAT is cardinal set
len (s .: NAT) is cardinal set
a \ (s .: NAT) is Element of bool (bool the carrier of (1TopSp [:T,T:]))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
T is V33() real ext-real set
m is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of m is non empty set
[#] m is non empty non proper Element of bool the carrier of m
bool the carrier of m is non empty set
Family_open_set m is Element of bool (bool the carrier of m)
bool (bool the carrier of m) is non empty set
a is Element of the carrier of m
cl_Ball (a,T) is Element of bool the carrier of m
([#] m) \ (cl_Ball (a,T)) is Element of bool the carrier of m
b is Element of the carrier of m
dist (a,b) is V33() real ext-real Element of REAL
r is V33() real ext-real Element of REAL
(dist (a,b)) - r is V33() real ext-real Element of REAL
Ball (b,((dist (a,b)) - r)) is Element of bool the carrier of m
ft is set
R is Element of the carrier of m
dist (a,R) is V33() real ext-real Element of REAL
dist (b,R) is V33() real ext-real Element of REAL
((dist (a,b)) - r) + r is V33() real ext-real Element of REAL
(dist (b,R)) + (dist (a,R)) is V33() real ext-real Element of REAL
dist (R,b) is V33() real ext-real Element of REAL
(dist (a,R)) + (dist (R,b)) is V33() real ext-real Element of REAL
r + ((dist (a,b)) - r) is V33() real ext-real Element of REAL
r + 0 is V33() real ext-real Element of REAL
((dist (a,b)) - r) - 0 is V33() real ext-real Element of REAL
r - r is V33() real ext-real Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty V119() V120() V121() set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty set
the topology of T is non empty open Element of bool (bool the carrier of T)
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
r is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty V14([: the carrier of T, the carrier of T:]) quasi_total V119() V120() V121() Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
SpaceMetr ( the carrier of T,r) is strict Reflexive discerning symmetric triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of T,r)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of T,r)))
the carrier of (SpaceMetr ( the carrier of T,r)) is set
bool the carrier of (SpaceMetr ( the carrier of T,r)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of T,r))) is non empty set
a is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
TopSpaceMetr a is TopStruct
the carrier of a is non empty set
Family_open_set a is Element of bool (bool the carrier of a)
bool the carrier of a is non empty set
bool (bool the carrier of a) is non empty set
TopStruct(# the carrier of a,(Family_open_set a) #) is non empty strict TopStruct
c is Element of the carrier of T
ft is Element of bool the carrier of T
ft ` is Element of bool the carrier of T
the carrier of T \ ft is set
[#] T is non empty non proper open closed Element of bool the carrier of T
([#] T) \ ft is Element of bool the carrier of T
the carrier of (TopSpaceMetr a) is set
bool the carrier of (TopSpaceMetr a) is non empty set
[#] (TopSpaceMetr a) is non proper Element of bool the carrier of (TopSpaceMetr a)
s is Element of bool the carrier of (TopSpaceMetr a)
([#] (TopSpaceMetr a)) \ s is Element of bool the carrier of (TopSpaceMetr a)
R is Element of the carrier of a
B is Element of bool the carrier of (TopSpaceMetr a)
U is V33() real ext-real Element of REAL
Ball (R,U) is Element of bool the carrier of a
mfx is set
Cl s is Element of bool the carrier of (TopSpaceMetr a)
B is V33() real ext-real Element of REAL
Ball (R,B) is Element of bool the carrier of a
B is V33() real ext-real Element of REAL
Ball (R,B) is Element of bool the carrier of a
B / 2 is V33() real ext-real Element of REAL
(B / 2) + (B / 2) is V33() real ext-real Element of REAL
[#] a is non empty non proper Element of bool the carrier of a
cl_Ball (R,(B / 2)) is Element of bool the carrier of a
([#] a) \ (cl_Ball (R,(B / 2))) is Element of bool the carrier of a
mfx is set
x is Element of the carrier of a
dist (R,x) is V33() real ext-real Element of REAL
(B / 2) / 2 is V33() real ext-real Element of REAL
((B / 2) / 2) + ((B / 2) / 2) is V33() real ext-real Element of REAL
Ball (R,((B / 2) / 2)) is Element of bool the carrier of a
x is set
x is Element of the carrier of a
dist (R,x) is V33() real ext-real Element of REAL
fx is Element of bool the carrier of T
fx is Element of bool the carrier of T
dist (R,R) is V33() real ext-real Element of REAL
c is Element of the carrier of T
ft is Element of the carrier of T
the carrier of (TopSpaceMetr a) is set
bool the carrier of (TopSpaceMetr a) is non empty set
R is Element of the carrier of (TopSpaceMetr a)
s is Element of the carrier of (TopSpaceMetr a)
B is Element of bool the carrier of (TopSpaceMetr a)
U is Element of bool the carrier of (TopSpaceMetr a)
mfx is Element of bool the carrier of T
x is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty V119() V120() V121() set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty set
the topology of T is non empty open Element of bool (bool the carrier of T)
r is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty V14([: the carrier of T, the carrier of T:]) quasi_total V119() V120() V121() Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
SpaceMetr ( the carrier of T,r) is strict Reflexive discerning symmetric triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of T,r)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of T,r)))
the carrier of (SpaceMetr ( the carrier of T,r)) is set
bool the carrier of (SpaceMetr ( the carrier of T,r)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of T,r))) is non empty set
a is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of a is non empty set
{ (Ball (b₁,(1 / (2 |^ a₁)))) where b₁ is Element of the carrier of a : b₁ is Element of the carrier of a } is set
b is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
2 |^ b is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
1 / (2 |^ b) is V33() real ext-real non negative Element of REAL
{ (Ball (b₁,(1 / (2 |^ b)))) where b₁ is Element of the carrier of a : b₁ is Element of the carrier of a } is set
ft is set
Family_open_set a is Element of bool (bool the carrier of a)
bool the carrier of a is non empty set
bool (bool the carrier of a) is non empty set
R is Element of the carrier of a
Ball (R,(1 / (2 |^ b))) is Element of bool the carrier of a
b is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
TopSpaceMetr a is TopStruct
Family_open_set a is Element of bool (bool the carrier of a)
bool the carrier of a is non empty set
bool (bool the carrier of a) is non empty set
TopStruct(# the carrier of a,(Family_open_set a) #) is non empty strict TopStruct
[#] T is non empty non proper open closed Element of bool the carrier of T
[#] (TopSpaceMetr a) is non proper Element of bool the carrier of (TopSpaceMetr a)
the carrier of (TopSpaceMetr a) is set
bool the carrier of (TopSpaceMetr a) is non empty set
ft is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,b,ft) is Element of bool (bool the carrier of T)
union (T,b,ft) is Element of bool the carrier of T
R is set
s is Element of the carrier of a
dist (s,s) is V33() real ext-real Element of REAL
2 |^ ft is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
1 / (2 |^ ft) is V33() real ext-real non negative Element of REAL
Ball (s,(1 / (2 |^ ft))) is Element of bool the carrier of a
{ (Ball (b₁,(1 / (2 |^ ft)))) where b₁ is Element of the carrier of a : b₁ is Element of the carrier of a } is set
R is Element of bool the carrier of T
2 |^ ft is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
1 / (2 |^ ft) is V33() real ext-real non negative Element of REAL
{ (Ball (b₁,(1 / (2 |^ ft)))) where b₁ is Element of the carrier of a : b₁ is Element of the carrier of a } is set
s is Element of the carrier of a
Ball (s,(1 / (2 |^ ft))) is Element of bool the carrier of a
R is Element of bool (bool the carrier of T)
ft is set
b . ft is set
R is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,b,R) is Element of bool (bool the carrier of T)
s is Element of bool (bool the carrier of T)
ft is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
(T,ft) is Element of bool (bool the carrier of T)
R is Element of bool the carrier of T
s is Element of the carrier of T
B is Element of the carrier of a
U is V33() real ext-real Element of REAL
Ball (B,U) is Element of bool the carrier of a
mfx is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
2 |^ mfx is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
1 / (2 |^ mfx) is V33() real ext-real non negative Element of REAL
mfx + 1 is non empty ordinal natural V33() real ext-real positive non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,ft,(mfx + 1)) is Element of bool (bool the carrier of T)
b . (mfx + 1) is set
union (T,ft,(mfx + 1)) is Element of bool the carrier of T
x is Element of bool (bool the carrier of T)
x is set
(T,b,(mfx + 1)) is Element of bool (bool the carrier of T)
x is Element of bool the carrier of a
fx is Element of bool (bool the carrier of T)
fx is set
2 |^ (mfx + 1) is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
1 / (2 |^ (mfx + 1)) is V33() real ext-real non negative Element of REAL
{ (Ball (b₁,(1 / (2 |^ (mfx + 1))))) where b₁ is Element of the carrier of a : b₁ is Element of the carrier of a } is set
fx is Element of the carrier of a
Ball (fx,(1 / (2 |^ (mfx + 1)))) is Element of bool the carrier of a
dist (fx,B) is V33() real ext-real Element of REAL
r9 is Element of the carrier of a
dist (fx,r9) is V33() real ext-real Element of REAL
dist (B,r9) is V33() real ext-real Element of REAL
(dist (fx,B)) + (dist (fx,r9)) is V33() real ext-real Element of REAL
(1 / (2 |^ (mfx + 1))) + (1 / (2 |^ (mfx + 1))) is V33() real ext-real non negative Element of REAL
2 * (1 / (2 |^ (mfx + 1))) is V33() real ext-real non negative Element of REAL
(2 |^ mfx) * 2 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
1 / ((2 |^ mfx) * 2) is V33() real ext-real non negative Element of REAL
(1 / ((2 |^ mfx) * 2)) * 2 is V33() real ext-real non negative Element of REAL
R is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,ft,R) is Element of bool (bool the carrier of T)
b . R is set
s is Element of bool (bool the carrier of T)
R is set
s is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,ft,s) is Element of bool (bool the carrier of T)
b . s is set
B is Element of bool the carrier of T
U is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
r is open Element of bool the carrier of T
m is Element of bool the carrier of T
r \ m is Element of bool the carrier of T
[#] T is non empty non proper open closed Element of bool the carrier of T
([#] T) \ m is Element of bool the carrier of T
r /\ (([#] T) \ m) is Element of bool the carrier of T
m ` is Element of bool the carrier of T
the carrier of T \ m is set
r /\ (m `) is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
[:NAT,(bool the carrier of T):] is non empty set
bool [:NAT,(bool the carrier of T):] is non empty set
r is Relation-like NAT -defined bool the carrier of T -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of T):]
Union r is Element of bool the carrier of T
rng r is Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
the topology of T is non empty open Element of bool (bool the carrier of T)
m is set
dom r is countable V130() V131() V132() V133() V134() V135() Element of bool NAT
a is set
r . a is set
b is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r . b is Element of bool the carrier of T
union (rng r) is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
[:NAT,(bool the carrier of T):] is non empty set
bool [:NAT,(bool the carrier of T):] is non empty set
r is Element of bool the carrier of T
m is Element of bool the carrier of T
[#] T is non empty non proper open closed Element of bool the carrier of T
([#] T) \ m is Element of bool the carrier of T
m ` is Element of bool the carrier of T
the carrier of T \ m is set
b is Relation-like NAT -defined bool the carrier of T -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of T):]
Union b is Element of bool the carrier of T
([#] T) \ r is Element of bool the carrier of T
r ` is Element of bool the carrier of T
the carrier of T \ r is set
ft is Relation-like NAT -defined bool the carrier of T -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of T):]
Union ft is Element of bool the carrier of T
{0} is non empty trivial finite V45() countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg a₁) \/ {0} } is set
union { (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg a₁) \/ {0} } is set
R is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
ft . R is Element of bool the carrier of T
Seg R is finite R -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg R) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg R) \/ {0} } is set
union { (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg R) \/ {0} } is set
(ft . R) \ (union { (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg R) \/ {0} } ) is Element of bool the carrier of T
R is Relation-like NAT -defined bool the carrier of T -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of T):]
s is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
R . s is Element of bool the carrier of T
Seg s is finite s -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg s) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg s) \/ {0} } is set
U is set
mfx is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
b . mfx is Element of bool the carrier of T
Cl (b . mfx) is closed Element of bool the carrier of T
bool (bool the carrier of T) is non empty set
{ H₂(b₁) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg s) \/ {0} } is set
mfx is Element of bool the carrier of T
U is Element of bool (bool the carrier of T)
x is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
b . x is Element of bool the carrier of T
Cl (b . x) is closed Element of bool the carrier of T
ft . s is Element of bool the carrier of T
union U is Element of bool the carrier of T
(ft . s) \ (union U) is Element of bool the carrier of T
Union R is Element of bool the carrier of T
s is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
b . s is Element of bool the carrier of T
Cl (b . s) is closed Element of bool the carrier of T
s is set
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
ft . B is Element of bool the carrier of T
Seg B is finite B -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg B) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg B) \/ {0} } is set
union { (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg B) \/ {0} } is set
U is set
mfx is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
b . mfx is Element of bool the carrier of T
Cl (b . mfx) is closed Element of bool the carrier of T
(ft . B) \ (union { (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg B) \/ {0} } ) is Element of bool the carrier of T
R . B is Element of bool the carrier of T
{ (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg a₁) \/ {0} } is set
union { (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg a₁) \/ {0} } is set
s is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
b . s is Element of bool the carrier of T
Seg s is finite s -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg s) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg s) \/ {0} } is set
union { (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg s) \/ {0} } is set
(b . s) \ (union { (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg s) \/ {0} } ) is Element of bool the carrier of T
s is Relation-like NAT -defined bool the carrier of T -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of T):]
Union s is Element of bool the carrier of T
B is set
U is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
R . U is Element of bool the carrier of T
mfx is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
s . mfx is Element of bool the carrier of T
x is set
b . mfx is Element of bool the carrier of T
Seg mfx is finite mfx -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg mfx) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg mfx) \/ {0} } is set
union { (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg mfx) \/ {0} } is set
(b . mfx) \ (union { (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg mfx) \/ {0} } ) is Element of bool the carrier of T
Seg U is finite U -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg U) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
Cl (b . mfx) is closed Element of bool the carrier of T
{ (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg U) \/ {0} } is set
ft . U is Element of bool the carrier of T
union { (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg U) \/ {0} } is set
(ft . U) \ (union { (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg U) \/ {0} } ) is Element of bool the carrier of T
x is set
ft . U is Element of bool the carrier of T
Seg U is finite U -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg U) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg U) \/ {0} } is set
union { (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg U) \/ {0} } is set
(ft . U) \ (union { (Cl (b . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg U) \/ {0} } ) is Element of bool the carrier of T
Seg mfx is finite mfx -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg mfx) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
Cl (ft . U) is closed Element of bool the carrier of T
{ (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg mfx) \/ {0} } is set
b . mfx is Element of bool the carrier of T
union { (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg mfx) \/ {0} } is set
(b . mfx) \ (union { (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg mfx) \/ {0} } ) is Element of bool the carrier of T
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
s . B is Element of bool the carrier of T
Seg B is finite B -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg B) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg B) \/ {0} } is set
mfx is set
x is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
ft . x is Element of bool the carrier of T
Cl (ft . x) is closed Element of bool the carrier of T
bool (bool the carrier of T) is non empty set
{ H₃(b₁) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg B) \/ {0} } is set
x is Element of bool the carrier of T
mfx is Element of bool (bool the carrier of T)
x is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
ft . x is Element of bool the carrier of T
Cl (ft . x) is closed Element of bool the carrier of T
b . B is Element of bool the carrier of T
union mfx is Element of bool the carrier of T
(b . B) \ (union mfx) is Element of bool the carrier of T
B is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
ft . B is Element of bool the carrier of T
Cl (ft . B) is closed Element of bool the carrier of T
B is set
U is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
b . U is Element of bool the carrier of T
Seg U is finite U -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
(Seg U) \/ {0} is non empty finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
{ (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg U) \/ {0} } is set
union { (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg U) \/ {0} } is set
mfx is set
x is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
ft . x is Element of bool the carrier of T
Cl (ft . x) is closed Element of bool the carrier of T
(b . U) \ (union { (Cl (ft . b₁)) where b₁ is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT : b₁ in (Seg U) \/ {0} } ) is Element of bool the carrier of T
s . U is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
r is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
(T,r) is Element of bool (bool the carrier of T)
m is open Element of bool the carrier of T
a is Element of the carrier of T
b is Element of bool the carrier of T
c is Element of bool the carrier of T
Cl c is closed Element of bool the carrier of T
m ` is closed Element of bool the carrier of T
the carrier of T \ m is set
(m `) ` is open Element of bool the carrier of T
the carrier of T \ (m `) is set
b is Element of bool the carrier of T
c is Element of bool the carrier of T
ft is Element of bool the carrier of T
c ` is Element of bool the carrier of T
the carrier of T \ c is set
Cl ft is closed Element of bool the carrier of T
Cl (c `) is closed Element of bool the carrier of T
c is Element of bool the carrier of T
Cl c is closed Element of bool the carrier of T
m is Element of bool the carrier of T
a is Element of the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty set
bool [:NAT,(bool (bool the carrier of T)):] is non empty set
r is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
r is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
(T,r) is Element of bool (bool the carrier of T)
[:NAT,(bool the carrier of T):] is non empty set
bool [:NAT,(bool the carrier of T):] is non empty set
m is Element of bool the carrier of T
a is open Element of bool the carrier of T
{ b₁ where b₁ is Element of bool the carrier of T : ( b₁ in r . a₁ & Cl b₁ c= a ) } is set
union { b₁ where b₁ is Element of bool the carrier of T : ( b₁ in r . a₁ & Cl b₁ c= a ) } is set
b is set
r . b is set
{ b₁ where b₁ is Element of bool the carrier of T : ( b₁ in r . b & Cl b₁ c= a ) } is set
union { b₁ where b₁ is Element of bool the carrier of T : ( b₁ in r . b & Cl b₁ c= a ) } is set
ft is set
c is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r . c is set
{ b₁ where b₁ is Element of bool the carrier of T : ( b₁ in r . c & Cl b₁ c= a ) } is set
union { b₁ where b₁ is Element of bool the carrier of T : ( b₁ in r . c & Cl b₁ c= a ) } is set
(T,r,c) is Element of bool (bool the carrier of T)
{ b₁ where b₁ is Element of bool the carrier of T : ( b₁ in (T,r,c) & Cl b₁ c= a ) } is set
R is set
s is Element of bool the carrier of T
Cl s is closed Element of bool the carrier of T
b is Relation-like NAT -defined bool the carrier of T -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(bool the carrier of T):]
c is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,r,c) is Element of bool (bool the carrier of T)
{ b₁ where b₁ is Element of bool the carrier of T : ( b₁ in (T,r,c) & Cl b₁ c= a ) } is set
R is set
s is Element of bool the carrier of T
Cl s is closed Element of bool the carrier of T
R is Element of bool (bool the carrier of T)
s is set
B is Element of bool the carrier of T
Cl B is closed Element of bool the carrier of T
union R is Element of bool the carrier of T
Cl (union R) is closed Element of bool the carrier of T
clf R is Element of bool (bool the carrier of T)
union (clf R) is Element of bool the carrier of T
s is set
B is set
U is Element of bool the carrier of T
mfx is Element of bool the carrier of T
Cl mfx is closed Element of bool the carrier of T
x is Element of bool the carrier of T
Cl x is closed Element of bool the carrier of T
the topology of T is non empty open Element of bool (bool the carrier of T)
s is set
B is Element of bool the carrier of T
Cl B is closed Element of bool the carrier of T
b . c is Element of bool the carrier of T
Cl (b . c) is closed Element of bool the carrier of T
Union b is Element of bool the carrier of T
c is set
ft is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
b . ft is Element of bool the carrier of T
(T,r,ft) is Element of bool (bool the carrier of T)
{ b₁ where b₁ is Element of bool the carrier of T : ( b₁ in (T,r,ft) & Cl b₁ c= a ) } is set
union { b₁ where b₁ is Element of bool the carrier of T : ( b₁ in (T,r,ft) & Cl b₁ c= a ) } is set
R is set
s is Element of bool the carrier of T
Cl s is closed Element of bool the carrier of T
c is set
ft is Element of bool the carrier of T
Cl ft is closed Element of bool the carrier of T
R is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
(T,r,R) is Element of bool (bool the carrier of T)
{ b₁ where b₁ is Element of bool the carrier of T : ( b₁ in (T,r,R) & Cl b₁ c= a ) } is set
r . R is set
{ b₁ where b₁ is Element of bool the carrier of T : ( b₁ in r . R & Cl b₁ c= a ) } is set
union { b₁ where b₁ is Element of bool the carrier of T : ( b₁ in r . R & Cl b₁ c= a ) } is set
b . R is Element of bool the carrier of T
T is V33() real ext-real Element of REAL
r is V33() real ext-real Element of the carrier of RealSpace
Ball (r,T) is V130() V131() V132() Element of bool the carrier of RealSpace
m is V33() real ext-real Element of REAL
m - m is V33() real ext-real Element of REAL
abs (m - m) is V33() real ext-real Element of REAL
dist (r,r) is V33() real ext-real Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T,REAL:] is non empty V119() V120() V121() set
bool [: the carrier of T,REAL:] is non empty set
r is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
m is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
r + m is Relation-like the carrier of T -defined Function-like V14( the carrier of T) V119() V120() V121() set
r + m is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
a is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
r + m is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
b is Element of the carrier of T
a . b is V33() real ext-real Element of REAL
r . b is V33() real ext-real Element of REAL
m . b is V33() real ext-real Element of REAL
(r . b) + (m . b) is V33() real ext-real Element of REAL
dom (r + m) is Element of bool the carrier of T
bool the carrier of T is non empty set
dom r is Element of bool the carrier of T
dom m is Element of bool the carrier of T
(dom r) /\ (dom m) is Element of bool the carrier of T
the carrier of T /\ (dom m) is Element of bool the carrier of T
the carrier of T /\ the carrier of T is set
b is set
dom a is Element of bool the carrier of T
a . b is V33() real ext-real set
r . b is V33() real ext-real set
m . b is V33() real ext-real set
(r . b) + (m . b) is V33() real ext-real set
(r + m) . b is V33() real ext-real set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T,REAL:] is non empty V119() V120() V121() set
bool [: the carrier of T,REAL:] is non empty set
[:T,T:] is non empty strict TopSpace-like TopStruct
the carrier of [:T,T:] is non empty set
[: the carrier of [:T,T:],REAL:] is non empty V119() V120() V121() set
bool [: the carrier of [:T,T:],REAL:] is non empty set
r is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
[: the carrier of T, the carrier of R^1:] is non empty V119() V120() V121() set
bool [: the carrier of T, the carrier of R^1:] is non empty set
c is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty V14( the carrier of [:T,T:]) quasi_total V119() V120() V121() Element of bool [: the carrier of [:T,T:],REAL:]
[: the carrier of [:T,T:], the carrier of R^1:] is non empty V119() V120() V121() set
bool [: the carrier of [:T,T:], the carrier of R^1:] is non empty set
b is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T, the carrier of R^1:]
R is Element of the carrier of [:T,T:]
[: the carrier of T, the carrier of T:] is non empty set
s is set
B is set
[s,B] is non empty set
{.B,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
bool the carrier of R^1 is non empty set
ft is Relation-like the carrier of [:T,T:] -defined the carrier of R^1 -valued Function-like non empty V14( the carrier of [:T,T:]) quasi_total V119() V120() V121() Element of bool [: the carrier of [:T,T:], the carrier of R^1:]
ft . R is V33() real ext-real Element of the carrier of R^1
bool the carrier of [:T,T:] is non empty set
U is Element of the carrier of T
r . U is V33() real ext-real Element of REAL
mfx is Element of the carrier of T
r . mfx is V33() real ext-real Element of REAL
c . R is V33() real ext-real Element of REAL
fx is V130() V131() V132() Element of bool the carrier of R^1
fx is V33() real ext-real Element of the carrier of RealSpace
r9 is V33() real ext-real set
Ball (fx,r9) is V130() V131() V132() Element of bool the carrier of RealSpace
x is V33() real ext-real Element of the carrier of RealSpace
FGx is V33() real ext-real Element of REAL
FGx / 2 is V33() real ext-real Element of REAL
Ball (x,(FGx / 2)) is V130() V131() V132() Element of bool the carrier of RealSpace
x is V33() real ext-real Element of the carrier of RealSpace
Ball (x,(FGx / 2)) is V130() V131() V132() Element of bool the carrier of RealSpace
x is V130() V131() V132() Element of bool the carrier of R^1
bool the carrier of T is non empty set
Fx is Element of bool the carrier of T
b .: Fx is V130() V131() V132() Element of bool the carrier of R^1
x is V130() V131() V132() Element of bool the carrier of R^1
Gx is Element of bool the carrier of T
b .: Gx is V130() V131() V132() Element of bool the carrier of R^1
c . (U,mfx) is set
[U,mfx] is non empty set
{.mfx,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
c . [U,mfx] is V33() real ext-real set
b . U is V33() real ext-real Element of the carrier of R^1
b . mfx is V33() real ext-real Element of the carrier of R^1
(b . U) - (b . mfx) is V33() real ext-real set
abs ((b . U) - (b . mfx)) is V33() real ext-real Element of REAL
[:Fx,Gx:] is Element of bool the carrier of [:T,T:]
c .: [:Fx,Gx:] is V130() V131() V132() Element of bool REAL
FGx9 is set
dom c is Element of bool the carrier of [:T,T:]
xy is set
c . xy is V33() real ext-real set
x is set
y is set
[x,y] is non empty set
{.y,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
x is Element of the carrier of T
r . x is V33() real ext-real Element of REAL
y is Element of the carrier of T
r . y is V33() real ext-real Element of REAL
dom r is Element of bool the carrier of T
r .: Gx is V130() V131() V132() Element of bool REAL
fy is V33() real ext-real Element of the carrier of RealSpace
dist (fy,x) is V33() real ext-real Element of REAL
[x,y] is non empty Element of the carrier of [:T,T:]
{.y,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
c . [x,y] is V33() real ext-real Element of REAL
(r . x) - (r . y) is V33() real ext-real Element of REAL
abs ((r . x) - (r . y)) is V33() real ext-real Element of REAL
c . (x,y) is set
[x,y] is non empty set
c . [x,y] is V33() real ext-real set
(r . x) - (r . U) is V33() real ext-real Element of REAL
abs ((r . x) - (r . U)) is V33() real ext-real Element of REAL
(abs ((r . x) - (r . U))) + (c . R) is V33() real ext-real Element of REAL
(r . mfx) - (r . y) is V33() real ext-real Element of REAL
abs ((r . mfx) - (r . y)) is V33() real ext-real Element of REAL
((abs ((r . x) - (r . U))) + (c . R)) + (abs ((r . mfx) - (r . y))) is V33() real ext-real Element of REAL
dist (x,fy) is V33() real ext-real Element of REAL
((abs ((r . x) - (r . U))) + (c . R)) + (dist (x,fy)) is V33() real ext-real Element of REAL
(c . [x,y]) + 0 is V33() real ext-real Element of REAL
fx is V33() real ext-real Element of the carrier of RealSpace
dist (fx,x) is V33() real ext-real Element of REAL
(c . R) + (dist (fx,x)) is V33() real ext-real Element of REAL
((c . R) + (dist (fx,x))) + (dist (x,fy)) is V33() real ext-real Element of REAL
(r . U) - (r . x) is V33() real ext-real Element of REAL
abs ((r . U) - (r . x)) is V33() real ext-real Element of REAL
(abs ((r . U) - (r . x))) + (c . [x,y]) is V33() real ext-real Element of REAL
(r . y) - (r . mfx) is V33() real ext-real Element of REAL
abs ((r . y) - (r . mfx)) is V33() real ext-real Element of REAL
((abs ((r . U) - (r . x))) + (c . [x,y])) + (abs ((r . y) - (r . mfx))) is V33() real ext-real Element of REAL
(dist (fx,x)) + (c . [x,y]) is V33() real ext-real Element of REAL
((dist (fx,x)) + (c . [x,y])) + (abs ((r . y) - (r . mfx))) is V33() real ext-real Element of REAL
(c . [x,y]) + (dist (fx,x)) is V33() real ext-real Element of REAL
((c . [x,y]) + (dist (fx,x))) + (dist (fy,x)) is V33() real ext-real Element of REAL
r .: Fx is V130() V131() V132() Element of bool REAL
(FGx / 2) + (FGx / 2) is V33() real ext-real Element of REAL
(dist (fx,x)) + (dist (fy,x)) is V33() real ext-real Element of REAL
(c . [x,y]) + FGx is V33() real ext-real Element of REAL
(c . [x,y]) + ((dist (fx,x)) + (dist (fy,x))) is V33() real ext-real Element of REAL
- (c . [x,y]) is V33() real ext-real Element of REAL
(- (c . [x,y])) - FGx is V33() real ext-real Element of REAL
- ((- (c . [x,y])) - FGx) is V33() real ext-real Element of REAL
- (c . R) is V33() real ext-real Element of REAL
(- (c . R)) - 0 is V33() real ext-real Element of REAL
- FGx is V33() real ext-real Element of REAL
(- FGx) - (c . [x,y]) is V33() real ext-real Element of REAL
(- (c . R)) + (c . [x,y]) is V33() real ext-real Element of REAL
(- FGx) + 0 is V33() real ext-real Element of REAL
(c . R) + FGx is V33() real ext-real Element of REAL
(dist (fx,x)) + (dist (x,fy)) is V33() real ext-real Element of REAL
(c . R) + ((dist (fx,x)) + (dist (x,fy))) is V33() real ext-real Element of REAL
FGx - 0 is V33() real ext-real Element of REAL
(c . [x,y]) - (c . R) is V33() real ext-real Element of REAL
abs ((c . [x,y]) - (c . R)) is V33() real ext-real Element of REAL
Fxy1 is V33() real ext-real Element of the carrier of RealSpace
dist (fx,Fxy1) is V33() real ext-real Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T,REAL:] is non empty V119() V120() V121() set
bool [: the carrier of T,REAL:] is non empty set
r is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
m is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
(T,r,m) is Relation-like the carrier of T -defined the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) V14( the carrier of T) quasi_total quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
[: the carrier of T, the carrier of R^1:] is non empty V119() V120() V121() set
bool [: the carrier of T, the carrier of R^1:] is non empty set
b is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T, the carrier of R^1:]
a is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T, the carrier of R^1:]
bool the carrier of R^1 is non empty set
c is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T, the carrier of R^1:]
ft is Element of the carrier of T
c . ft is V33() real ext-real Element of the carrier of R^1
bool the carrier of T is non empty set
r . ft is V33() real ext-real Element of REAL
m . ft is V33() real ext-real Element of REAL
(T,r,m) . ft is V33() real ext-real Element of REAL
U is V130() V131() V132() Element of bool the carrier of R^1
B is V33() real ext-real Element of the carrier of RealSpace
mfx is V33() real ext-real set
Ball (B,mfx) is V130() V131() V132() Element of bool the carrier of RealSpace
R is V33() real ext-real Element of the carrier of RealSpace
x is V33() real ext-real Element of REAL
x / 2 is V33() real ext-real Element of REAL
Ball (R,(x / 2)) is V130() V131() V132() Element of bool the carrier of RealSpace
s is V33() real ext-real Element of the carrier of RealSpace
Ball (s,(x / 2)) is V130() V131() V132() Element of bool the carrier of RealSpace
x is V130() V131() V132() Element of bool the carrier of R^1
a . ft is V33() real ext-real Element of the carrier of R^1
fx is Element of bool the carrier of T
a .: fx is V130() V131() V132() Element of bool the carrier of R^1
fx is V130() V131() V132() Element of bool the carrier of R^1
r9 is Element of bool the carrier of T
b .: r9 is V130() V131() V132() Element of bool the carrier of R^1
fx /\ r9 is Element of bool the carrier of T
(T,r,m) .: (fx /\ r9) is V130() V131() V132() Element of bool REAL
FGx is set
dom (T,r,m) is Element of bool the carrier of T
x is set
(T,r,m) . x is V33() real ext-real set
x is Element of the carrier of T
r . x is V33() real ext-real Element of REAL
m . x is V33() real ext-real Element of REAL
(T,r,m) . x is V33() real ext-real Element of REAL
dom m is Element of bool the carrier of T
m .: r9 is V130() V131() V132() Element of bool REAL
Gx is V33() real ext-real Element of the carrier of RealSpace
dist (Gx,s) is V33() real ext-real Element of REAL
(m . x) - (m . ft) is V33() real ext-real Element of REAL
abs ((m . x) - (m . ft)) is V33() real ext-real Element of REAL
- (x / 2) is V33() real ext-real Element of REAL
dom r is Element of bool the carrier of T
r .: fx is V130() V131() V132() Element of bool REAL
Fx is V33() real ext-real Element of the carrier of RealSpace
dist (Fx,R) is V33() real ext-real Element of REAL
(r . x) - (r . ft) is V33() real ext-real Element of REAL
abs ((r . x) - (r . ft)) is V33() real ext-real Element of REAL
((r . x) - (r . ft)) + ((m . x) - (m . ft)) is V33() real ext-real Element of REAL
(- (x / 2)) + (- (x / 2)) is V33() real ext-real Element of REAL
(r . x) + (m . x) is V33() real ext-real Element of REAL
(r . ft) + (m . ft) is V33() real ext-real Element of REAL
((r . x) + (m . x)) - ((r . ft) + (m . ft)) is V33() real ext-real Element of REAL
- x is V33() real ext-real Element of REAL
(x / 2) + (x / 2) is V33() real ext-real Element of REAL
abs (((r . x) + (m . x)) - ((r . ft) + (m . ft))) is V33() real ext-real Element of REAL
((T,r,m) . x) - ((r . ft) + (m . ft)) is V33() real ext-real Element of REAL
abs (((T,r,m) . x) - ((r . ft) + (m . ft))) is V33() real ext-real Element of REAL
((T,r,m) . x) - ((T,r,m) . ft) is V33() real ext-real Element of REAL
abs (((T,r,m) . x) - ((T,r,m) . ft)) is V33() real ext-real Element of REAL
FGx9 is V33() real ext-real Element of the carrier of RealSpace
dist (B,FGx9) is V33() real ext-real Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
Funcs ( the carrier of T,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of T, REAL
[:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):] is non empty set
[:[:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):],(Funcs ( the carrier of T,REAL)):] is non empty set
bool [:[:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):],(Funcs ( the carrier of T,REAL)):] is non empty set
[: the carrier of T,REAL:] is non empty V119() V120() V121() set
bool [: the carrier of T,REAL:] is non empty set
m is Relation-like [:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):] -defined Funcs ( the carrier of T,REAL) -valued Function-like non empty V14([:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):]) quasi_total Element of bool [:[:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):],(Funcs ( the carrier of T,REAL)):]
the carrier of T --> 0 is Relation-like the carrier of T -defined NAT -valued INT -valued RAT -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() V122() Element of bool [: the carrier of T,NAT:]
[: the carrier of T,NAT:] is INT -valued RAT -valued non empty V119() V120() V121() V122() set
bool [: the carrier of T,NAT:] is non empty set
a is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
b is Relation-like the carrier of T -defined REAL -valued Function-like V14( the carrier of T) quasi_total V119() V120() V121() Element of Funcs ( the carrier of T,REAL)
c is Relation-like the carrier of T -defined REAL -valued Function-like V14( the carrier of T) quasi_total V119() V120() V121() Element of Funcs ( the carrier of T,REAL)
(T,c,b) is Relation-like the carrier of T -defined the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) V14( the carrier of T) quasi_total quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
ft is Element of the carrier of T
(T,c,b) . ft is V33() real ext-real Element of REAL
c . ft is V33() real ext-real Element of REAL
b . ft is V33() real ext-real Element of REAL
(c . ft) + (b . ft) is V33() real ext-real Element of REAL
(c . ft) + 0 is V33() real ext-real Element of REAL
m . (a,c) is set
[a,c] is non empty set
{.c,.} is functional non empty finite countable set
{..} is functional non empty trivial finite with_common_domain countable set
{.{..},.} is non empty finite V45() countable set
m . [a,c] is Relation-like Function-like set
m . (c,a) is set
[c,a] is non empty set
{.a,.} is functional non empty finite countable set
{..} is functional non empty trivial finite with_common_domain countable set
{.{..},.} is non empty finite V45() countable set
m . [c,a] is Relation-like Function-like set
a is Relation-like the carrier of T -defined REAL -valued Function-like V14( the carrier of T) quasi_total V119() V120() V121() Element of Funcs ( the carrier of T,REAL)
a is Relation-like the carrier of T -defined REAL -valued Function-like V14( the carrier of T) quasi_total V119() V120() V121() Element of Funcs ( the carrier of T,REAL)
b is Relation-like the carrier of T -defined REAL -valued Function-like V14( the carrier of T) quasi_total V119() V120() V121() Element of Funcs ( the carrier of T,REAL)
m . (a,b) is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
[a,b] is non empty set
{.b,.} is functional non empty finite countable set
{..} is functional non empty trivial finite with_common_domain countable set
{.{..},.} is non empty finite V45() countable set
m . [a,b] is Relation-like Function-like set
m . (b,a) is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
[b,a] is non empty set
{.a,.} is functional non empty finite countable set
{..} is functional non empty trivial finite with_common_domain countable set
{.{..},.} is non empty finite V45() countable set
m . [b,a] is Relation-like Function-like set
m . (a,b) is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
(T,a,b) is Relation-like the carrier of T -defined the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) V14( the carrier of T) quasi_total quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
a is Relation-like the carrier of T -defined REAL -valued Function-like V14( the carrier of T) quasi_total V119() V120() V121() Element of Funcs ( the carrier of T,REAL)
b is Relation-like the carrier of T -defined REAL -valued Function-like V14( the carrier of T) quasi_total V119() V120() V121() Element of Funcs ( the carrier of T,REAL)
c is Relation-like the carrier of T -defined REAL -valued Function-like V14( the carrier of T) quasi_total V119() V120() V121() Element of Funcs ( the carrier of T,REAL)
m . (b,c) is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
[b,c] is non empty set
{.c,.} is functional non empty finite countable set
{..} is functional non empty trivial finite with_common_domain countable set
{.{..},.} is non empty finite V45() countable set
m . [b,c] is Relation-like Function-like set
m . (a,(m . (b,c))) is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
[a,(m . (b,c))] is non empty set
{.(m . (b,c)),.} is functional non empty finite countable set
{..} is functional non empty trivial finite with_common_domain countable set
{.{..},.} is non empty finite V45() countable set
m . [a,(m . (b,c))] is Relation-like Function-like set
m . (a,b) is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
[a,b] is non empty set
{.b,.} is functional non empty finite countable set
{.{..},.} is non empty finite V45() countable set
m . [a,b] is Relation-like Function-like set
m . ((m . (a,b)),c) is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
[(m . (a,b)),c] is non empty set
{.c,.} is functional non empty finite countable set
{..} is functional non empty trivial finite with_common_domain countable set
{.{..},.} is non empty finite V45() countable set
m . [(m . (a,b)),c] is Relation-like Function-like set
m . (a,b) is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
m . (b,c) is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
ft is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
(T,ft,c) is Relation-like the carrier of T -defined the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) V14( the carrier of T) quasi_total quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
m . (ft,c) is set
[ft,c] is non empty set
{.c,.} is functional non empty finite countable set
{..} is functional non empty trivial finite with_common_domain countable set
{.{..},.} is non empty finite V45() countable set
m . [ft,c] is Relation-like Function-like set
(T,b,c) is Relation-like the carrier of T -defined the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) V14( the carrier of T) quasi_total quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
(T,a,(T,b,c)) is Relation-like the carrier of T -defined the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) V14( the carrier of T) quasi_total quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
s is Element of the carrier of T
(T,a,(T,b,c)) . s is V33() real ext-real Element of REAL
a . s is V33() real ext-real Element of REAL
(T,b,c) . s is V33() real ext-real Element of REAL
(a . s) + ((T,b,c) . s) is V33() real ext-real Element of REAL
b . s is V33() real ext-real Element of REAL
c . s is V33() real ext-real Element of REAL
(b . s) + (c . s) is V33() real ext-real Element of REAL
(a . s) + (b . s) is V33() real ext-real Element of REAL
((a . s) + (b . s)) + (c . s) is V33() real ext-real Element of REAL
(T,a,b) is Relation-like the carrier of T -defined the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) V14( the carrier of T) quasi_total quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
(T,a,b) . s is V33() real ext-real Element of REAL
((T,a,b) . s) + (c . s) is V33() real ext-real Element of REAL
(T,(T,a,b),c) is Relation-like the carrier of T -defined the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) V14( the carrier of T) quasi_total quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
(T,(T,a,b),c) . s is V33() real ext-real Element of REAL
R is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
(T,a,R) is Relation-like the carrier of T -defined the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) V14( the carrier of T) quasi_total quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
Funcs ( the carrier of T,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of T, REAL
[:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):] is non empty set
[:[:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):],(Funcs ( the carrier of T,REAL)):] is non empty set
bool [:[:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):],(Funcs ( the carrier of T,REAL)):] is non empty set
[: the carrier of T,REAL:] is non empty V119() V120() V121() set
bool [: the carrier of T,REAL:] is non empty set
r is Relation-like [:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):] -defined Funcs ( the carrier of T,REAL) -valued Function-like non empty V14([:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):]) quasi_total Element of bool [:[:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):],(Funcs ( the carrier of T,REAL)):]
a is Relation-like the carrier of T -defined REAL -valued Function-like V14( the carrier of T) quasi_total V119() V120() V121() Element of Funcs ( the carrier of T,REAL)
b is Element of the carrier of T
a . b is V33() real ext-real Element of REAL
b is Element of the carrier of T
a . b is V33() real ext-real Element of REAL
r . (a,a) is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
[a,a] is non empty set
{.a,.} is functional non empty finite countable set
{..} is functional non empty trivial finite with_common_domain countable set
{.{..},.} is non empty finite V45() countable set
r . [a,a] is Relation-like Function-like set
(T,a,a) is Relation-like the carrier of T -defined the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) V14( the carrier of T) quasi_total quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
(a . b) + (a . b) is V33() real ext-real Element of REAL
[: the carrier of T, the carrier of R^1:] is non empty V119() V120() V121() set
bool [: the carrier of T, the carrier of R^1:] is non empty set
bool the carrier of T is non empty set
b is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T, the carrier of R^1:]
c is Element of bool the carrier of T
Cl c is closed Element of bool the carrier of T
b .: (Cl c) is V130() V131() V132() Element of bool the carrier of R^1
bool the carrier of R^1 is non empty set
b .: c is V130() V131() V132() Element of bool the carrier of R^1
Cl (b .: c) is closed V130() V131() V132() Element of bool the carrier of R^1
ft is set
dom a is Element of bool the carrier of T
{} T is Function-like functional empty trivial proper finite V45() countable FinSequence-membered open closed compact V130() V131() V132() V133() V134() V135() V136() Element of bool the carrier of T
R is set
b . R is V33() real ext-real set
R is set
s is Element of the carrier of T
a . s is V33() real ext-real Element of REAL
a .: c is V130() V131() V132() Element of bool REAL
B is set
b . B is V33() real ext-real set
T is non empty set
r is non empty set
Funcs (T,r) is functional non empty FUNCTION_DOMAIN of T,r
[:T,(Funcs (T,r)):] is non empty set
bool [:T,(Funcs (T,r)):] is non empty set
[:T,r:] is non empty set
bool [:T,r:] is non empty set
m is Relation-like T -defined Funcs (T,r) -valued Function-like non empty V14(T) quasi_total Element of bool [:T,(Funcs (T,r)):]
a is Element of T
m . a is Relation-like Function-like Element of Funcs (T,r)
(m . a) . a is set
b is Relation-like T -defined r -valued Function-like non empty V14(T) quasi_total Element of bool [:T,r:]
b . a is Element of r
a is Relation-like T -defined r -valued Function-like non empty V14(T) quasi_total Element of bool [:T,r:]
b is Element of T
a . b is Element of r
m . b is Relation-like Function-like Element of Funcs (T,r)
(m . b) . b is set
a is Relation-like T -defined r -valued Function-like non empty V14(T) quasi_total Element of bool [:T,r:]
b is Relation-like T -defined r -valued Function-like non empty V14(T) quasi_total Element of bool [:T,r:]
c is Element of T
a . c is Element of r
m . c is Relation-like Function-like Element of Funcs (T,r)
(m . c) . c is set
b . c is Element of r
a is Relation-like T -defined r -valued Function-like non empty V14(T) quasi_total Element of bool [:T,r:]
b is Relation-like T -defined r -valued Function-like non empty V14(T) quasi_total Element of bool [:T,r:]
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
Funcs ( the carrier of T,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of T, REAL
[:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):] is non empty set
[:[:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):],(Funcs ( the carrier of T,REAL)):] is non empty set
bool [:[:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):],(Funcs ( the carrier of T,REAL)):] is non empty set
[: the carrier of T,REAL:] is non empty V119() V120() V121() set
bool [: the carrier of T,REAL:] is non empty set
r is Relation-like [:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):] -defined Funcs ( the carrier of T,REAL) -valued Function-like non empty V14([:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):]) quasi_total Element of bool [:[:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of T,REAL)):],(Funcs ( the carrier of T,REAL)):]
a is Relation-like NAT -defined Funcs ( the carrier of T,REAL) -valued Function-like finite countable FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of T,REAL)
len a is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
r "**" a is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
the_unity_wrt r is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
c is Relation-like the carrier of T -defined REAL -valued Function-like V14( the carrier of T) quasi_total V119() V120() V121() Element of Funcs ( the carrier of T,REAL)
b is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
1 + 0 is non empty ordinal natural V33() real ext-real positive non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
[:NAT,(Funcs ( the carrier of T,REAL)):] is non empty set
bool [:NAT,(Funcs ( the carrier of T,REAL)):] is non empty set
a . 1 is Relation-like Function-like set
c is Relation-like NAT -defined Funcs ( the carrier of T,REAL) -valued Function-like non empty V14( NAT ) quasi_total Element of bool [:NAT,(Funcs ( the carrier of T,REAL)):]
c . 1 is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
c . (len a) is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
ft is ordinal natural V33() real ext-real non negative set
c . ft is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
ft + 1 is non empty ordinal natural V33() real ext-real positive non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
c . (ft + 1) is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
R is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
R + 1 is non empty ordinal natural V33() real ext-real positive non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
R + 0 is ordinal natural V33() real ext-real non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
c . (R + 1) is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
c . R is Relation-like Function-like Element of Funcs ( the carrier of T,REAL)
a . (R + 1) is Relation-like Function-like set
r . ((c . R),(a . (R + 1))) is set
[(c . R),(a . (R + 1))] is non empty set
{.(a . (R + 1)),.} is functional non empty finite countable set
{..} is functional non empty trivial finite with_common_domain countable set
{.{..},.} is non empty finite V45() countable set
r . [(c . R),(a . (R + 1))] is Relation-like Function-like set
1 + 0 is non empty ordinal natural V33() real ext-real positive non negative V63() V129() V130() V131() V132() V133() V134() V135() Element of NAT
Seg (len a) is finite len a -element countable V130() V131() V132() V133() V134() V135() Element of bool NAT
dom a is finite countable V130() V131() V132() V133() V134() V135() Element of bool NAT
rng a is functional finite countable Element of bool (Funcs ( the carrier of T,REAL))
bool (Funcs ( the carrier of T,REAL)) is non empty set
B is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
s is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
(T,s,B) is Relation-like the carrier of T -defined the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) V14( the carrier of T) quasi_total quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
[: the carrier of T,(bool the carrier of T):] is non empty set
bool [: the carrier of T,(bool the carrier of T):] is non empty set
r is non empty TopSpace-like TopStruct
the carrier of r is non empty set
Funcs ( the carrier of T, the carrier of r) is functional non empty FUNCTION_DOMAIN of the carrier of T, the carrier of r
[: the carrier of T,(Funcs ( the carrier of T, the carrier of r)):] is non empty set
bool [: the carrier of T,(Funcs ( the carrier of T, the carrier of r)):] is non empty set
[: the carrier of T, the carrier of r:] is non empty set
bool [: the carrier of T, the carrier of r:] is non empty set
m is Relation-like the carrier of T -defined Funcs ( the carrier of T, the carrier of r) -valued Function-like non empty V14( the carrier of T) quasi_total Element of bool [: the carrier of T,(Funcs ( the carrier of T, the carrier of r)):]
( the carrier of T, the carrier of r,m) is Relation-like the carrier of T -defined the carrier of r -valued Function-like non empty V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of r:]
a is Relation-like the carrier of T -defined bool the carrier of T -valued Function-like non empty V14( the carrier of T) quasi_total Element of bool [: the carrier of T,(bool the carrier of T):]
bool the carrier of r is non empty set
b is Element of the carrier of T
( the carrier of T, the carrier of r,m) . b is Element of the carrier of r
m . b is Relation-like Function-like Element of Funcs ( the carrier of T, the carrier of r)
ft is Element of bool the carrier of r
c is Relation-like the carrier of T -defined the carrier of r -valued Function-like non empty V14( the carrier of T) quasi_total Element of bool [: the carrier of T, the carrier of r:]
c . b is Element of the carrier of r
R is Element of bool the carrier of T
c .: R is Element of bool the carrier of r
a . b is Element of bool the carrier of T
R /\ (a . b) is Element of bool the carrier of T
( the carrier of T, the carrier of r,m) .: (R /\ (a . b)) is Element of bool the carrier of r
B is set
dom ( the carrier of T, the carrier of r,m) is Element of bool the carrier of T
U is set
( the carrier of T, the carrier of r,m) . U is set
mfx is Element of the carrier of T
m . mfx is Relation-like Function-like Element of Funcs ( the carrier of T, the carrier of r)
(m . mfx) . mfx is set
c . mfx is Element of the carrier of r
dom c is Element of bool the carrier of T
T is set
[:T,REAL:] is V119() V120() V121() set
bool [:T,REAL:] is non empty set
r is V33() real ext-real Element of REAL
m is Relation-like T -defined REAL -valued Function-like V14(T) quasi_total V119() V120() V121() Element of bool [:T,REAL:]
a is set
b is Element of T
m . b is V33() real ext-real set
min (r,(m . b)) is V33() real ext-real set
a is Relation-like T -defined REAL -valued Function-like V14(T) quasi_total V119() V120() V121() Element of bool [:T,REAL:]
b is set
a . b is V33() real ext-real set
m . b is V33() real ext-real set
min (r,(m . b)) is V33() real ext-real set
c is Element of T
m . c is V33() real ext-real set
min (r,(m . c)) is V33() real ext-real set
a is Relation-like T -defined REAL -valued Function-like V14(T) quasi_total V119() V120() V121() Element of bool [:T,REAL:]
b is Relation-like T -defined REAL -valued Function-like V14(T) quasi_total V119() V120() V121() Element of bool [:T,REAL:]
c is set
a . c is V33() real ext-real set
ft is Element of T
m . ft is V33() real ext-real set
min (r,(m . ft)) is V33() real ext-real set
b . c is V33() real ext-real set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T,REAL:] is non empty V119() V120() V121() set
bool [: the carrier of T,REAL:] is non empty set
r is V33() real ext-real Element of REAL
m is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
( the carrier of T,r,m) is Relation-like the carrier of T -defined REAL -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T,REAL:]
[: the carrier of T, the carrier of R^1:] is non empty V119() V120() V121() set
bool [: the carrier of T, the carrier of R^1:] is non empty set
a is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T, the carrier of R^1:]
bool the carrier of R^1 is non empty set
b is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty V14( the carrier of T) quasi_total V119() V120() V121() Element of bool [: the carrier of T, the carrier of R^1:]
c is Element of the carrier of T
b . c is V33() real ext-real Element of the carrier of R^1
bool the carrier of T is non empty set
m . c is V33() real ext-real Element of REAL
R is V130() V131() V132() Element of bool the carrier of R^1
min (r,(m . c)) is V33() real ext-real set
ft is V33() real ext-real Element of the carrier of RealSpace
s is V33() real ext-real set
Ball (ft,s) is V130() V131() V132() Element of bool the carrier of RealSpace
B is V33() real ext-real Element of REAL
Ball (ft,B) is V130() V131() V132() Element of bool the carrier of RealSpace
dist (ft,ft) is V33() real ext-real Element of REAL
U is V130() V131() V132() Element of bool the carrier of R^1
mfx is Element of bool the carrier of T
a .: mfx is V130() V131() V132() Element of bool the carrier of R^1
( the carrier of T,r,m) .: mfx is V130() V131() V132() Element of bool REAL
x is set
dom ( the carrier of T,r,m) is Element of bool the carrier of T
x is set
( the carrier of T,r,m) . x is V33() real ext-real set
fx is Element of the carrier of T
m . fx is V33() real ext-real Element of REAL
dom m is Element of bool the carrier of T
m .: mfx is V130() V131() V132() Element of bool REAL
min (r,(m . fx)) is V33() real ext-real set
fx is V33() real ext-real Element of the carrier of RealSpace
dist (fx,ft) is V33() real ext-real Element of REAL
(m . fx) - (m . c) is V33() real ext-real Element of REAL
abs ((m . fx) - (m . c)) is V33() real ext-real Element of REAL
r - (m . c) is V33() real ext-real Element of REAL
abs (r - (m . c)) is V33() real ext-real Element of REAL
r9 is V33() real ext-real Element of the carrier of RealSpace
dist (ft,r9) is V33() real ext-real Element of REAL
min (r,(m . fx)) is V33() real ext-real set
(m . c) - r is V33() real ext-real Element of REAL
ft is V33() real ext-real Element of the carrier of RealSpace
Ball (ft,((m . c) - r)) is V130() V131() V132() Element of bool the carrier of RealSpace
dist (ft,ft) is V33() real ext-real Element of REAL
B is V130() V131() V132() Element of bool the carrier of R^1
U is Element of bool the carrier of T
a .: U is V130() V131() V132() Element of bool the carrier of R^1
( the carrier of T,r,m) .: U is V130() V131() V132() Element of bool REAL
mfx is set
dom ( the carrier of T,r,m) is Element of bool the carrier of T
x is set
( the carrier of T,r,m) . x is V33() real ext-real set
x is Element of the carrier of T
m . x is V33() real ext-real Element of REAL
dom m is Element of bool the carrier of T
m .: U is V130() V131() V132() Element of bool REAL
fx is V33() real ext-real Element of the carrier of RealSpace
dist (ft,fx) is V33() real ext-real Element of REAL
(m . c) - (m . x) is V33() real ext-real Element of REAL
abs ((m . c) - (m . x)) is V33() real ext-real Element of REAL
- (m . x) is V33() real ext-real Element of REAL
(m . c) + (- (m . x)) is V33() real ext-real Element of REAL
- r is V33() real ext-real Element of REAL
(m . c) + (- r) is V33() real ext-real Element of REAL
min (r,(m . x)) is V33() real ext-real set
min (r,(m . c)) is V33() real ext-real set
( the carrier of T,r,m) . c is V33() real ext-real Element of REAL
s is Element of bool the carrier of T
( the carrier of T,r,m) .: s is V130() V131() V132() Element of bool REAL
T is set
[:T,T:] is set
[:[:T,T:],REAL:] is V119() V120() V121() set
bool [:[:T,T:],REAL:] is non empty set
T is set
[:T,T:] is set
[:[:T,T:],REAL:] is V119() V120() V121() set
bool [:[:T,T:],REAL:] is non empty set
r is Relation-like [:T,T:] -defined REAL -valued Function-like V14([:T,T:]) quasi_total V119() V120() V121() Element of bool [:[:T,T:],REAL:]
m is Element of T
r . (m,m) is V33() real ext-real Element of REAL
[m,m] is non empty set
{.m,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [m,m] is V33() real ext-real set
a is Element of T
b is Element of T
r . (a,b) is V33() real ext-real Element of REAL
[a,b] is non empty set
{.b,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [a,b] is V33() real ext-real set
r . (b,a) is V33() real ext-real Element of REAL
[b,a] is non empty set
{.a,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [b,a] is V33() real ext-real set
c is Element of T
R is Element of T
r . (c,R) is V33() real ext-real Element of REAL
[c,R] is non empty set
{.R,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [c,R] is V33() real ext-real set
ft is Element of T
r . (c,ft) is V33() real ext-real Element of REAL
[c,ft] is non empty set
{.ft,.} is non empty finite countable set
{.{..},.} is non empty finite V45() countable set
r . [c,ft] is V33() real ext-real set
r . (ft,R) is V33() real ext-real Element of REAL
[ft,R] is non empty set
{.R,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [ft,R] is V33() real ext-real set
(r . (c,ft)) + (r . (ft,R)) is V33() real ext-real Element of REAL
T is set
[:T,T:] is set
[:[:T,T:],REAL:] is V119() V120() V121() set
bool [:[:T,T:],REAL:] is non empty set
r is Relation-like [:T,T:] -defined REAL -valued Function-like V14([:T,T:]) quasi_total V119() V120() V121() Element of bool [:[:T,T:],REAL:]
m is Element of T
r . (m,m) is V33() real ext-real Element of REAL
[m,m] is non empty set
{.m,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [m,m] is V33() real ext-real set
b is Element of T
r . (m,b) is V33() real ext-real Element of REAL
[m,b] is non empty set
{.b,.} is non empty finite countable set
{.{..},.} is non empty finite V45() countable set
r . [m,b] is V33() real ext-real set
a is Element of T
r . (m,a) is V33() real ext-real Element of REAL
[m,a] is non empty set
{.a,.} is non empty finite countable set
{.{..},.} is non empty finite V45() countable set
r . [m,a] is V33() real ext-real set
r . (b,a) is V33() real ext-real Element of REAL
[b,a] is non empty set
{.a,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [b,a] is V33() real ext-real set
(r . (m,a)) + (r . (b,a)) is V33() real ext-real Element of REAL
r . (a,b) is V33() real ext-real Element of REAL
[a,b] is non empty set
{.b,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [a,b] is V33() real ext-real set
(r . (m,a)) + (r . (a,b)) is V33() real ext-real Element of REAL
m is Element of T
a is Element of T
r . (m,a) is V33() real ext-real Element of REAL
[m,a] is non empty set
{.a,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [m,a] is V33() real ext-real set
r . (a,m) is V33() real ext-real Element of REAL
[a,m] is non empty set
{.m,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [a,m] is V33() real ext-real set
r . (a,a) is V33() real ext-real Element of REAL
[a,a] is non empty set
{.a,.} is non empty finite countable set
{.{..},.} is non empty finite V45() countable set
r . [a,a] is V33() real ext-real set
(r . (a,a)) + (r . (m,a)) is V33() real ext-real Element of REAL
r . (m,m) is V33() real ext-real Element of REAL
[m,m] is non empty set
{.m,.} is non empty finite countable set
{.{..},.} is non empty finite V45() countable set
r . [m,m] is V33() real ext-real set
(r . (m,m)) + (r . (a,m)) is V33() real ext-real Element of REAL
m is Element of T
b is Element of T
r . (m,b) is V33() real ext-real Element of REAL
[m,b] is non empty set
{.b,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [m,b] is V33() real ext-real set
a is Element of T
r . (m,a) is V33() real ext-real Element of REAL
[m,a] is non empty set
{.a,.} is non empty finite countable set
{.{..},.} is non empty finite V45() countable set
r . [m,a] is V33() real ext-real set
r . (a,b) is V33() real ext-real Element of REAL
[a,b] is non empty set
{.b,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [a,b] is V33() real ext-real set
(r . (m,a)) + (r . (a,b)) is V33() real ext-real Element of REAL
r . (b,a) is V33() real ext-real Element of REAL
[b,a] is non empty set
{.a,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [b,a] is V33() real ext-real set
(r . (m,a)) + (r . (b,a)) is V33() real ext-real Element of REAL
T is V33() real ext-real Element of REAL
r is non empty set
[:r,r:] is non empty set
[:[:r,r:],REAL:] is non empty V119() V120() V121() set
bool [:[:r,r:],REAL:] is non empty set
m is Relation-like [:r,r:] -defined REAL -valued Function-like non empty V14([:r,r:]) quasi_total V119() V120() V121() Element of bool [:[:r,r:],REAL:]
([:r,r:],T,m) is Relation-like [:r,r:] -defined REAL -valued Function-like non empty V14([:r,r:]) quasi_total V119() V120() V121() Element of bool [:[:r,r:],REAL:]
a is Element of r
b is Element of r
([:r,r:],T,m) . (a,b) is V33() real ext-real Element of REAL
[a,b] is non empty set
{.b,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
([:r,r:],T,m) . [a,b] is V33() real ext-real set
m . (a,b) is V33() real ext-real Element of REAL
m . [a,b] is V33() real ext-real set
min (T,(m . (a,b))) is V33() real ext-real set
[a,b] is non empty Element of [:r,r:]
m . [a,b] is V33() real ext-real Element of REAL
min (T,(m . [a,b])) is V33() real ext-real set
T is set
[:T,T:] is set
[:[:T,T:],REAL:] is V119() V120() V121() set
bool [:[:T,T:],REAL:] is non empty set
r is Relation-like [:T,T:] -defined REAL -valued Function-like V14([:T,T:]) quasi_total V119() V120() V121() Element of bool [:[:T,T:],REAL:]
m is Element of T
a is Element of T
r . (m,a) is V33() real ext-real Element of REAL
[m,a] is non empty set
{.a,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [m,a] is V33() real ext-real set
r . (m,m) is V33() real ext-real Element of REAL
[m,m] is non empty set
{.m,.} is non empty finite countable set
{.{..},.} is non empty finite V45() countable set
r . [m,m] is V33() real ext-real set
r . (a,m) is V33() real ext-real Element of REAL
[a,m] is non empty set
{.m,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
r . [a,m] is V33() real ext-real set
(r . (m,a)) + (r . (a,m)) is V33() real ext-real Element of REAL
(r . (m,a)) + (r . (m,a)) is V33() real ext-real Element of REAL
((r . (m,a)) + (r . (m,a))) / 2 is V33() real ext-real Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty V119() V120() V121() set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty set
r is V33() real ext-real Element of REAL
m is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty V14([: the carrier of T, the carrier of T:]) quasi_total V119() V120() V121() Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
([: the carrier of T, the carrier of T:],r,m) is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty V14([: the carrier of T, the carrier of T:]) quasi_total V119() V120() V121() Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
a is Element of the carrier of T
m . (a,a) is V33() real ext-real Element of REAL
[a,a] is non empty set
{.a,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
m . [a,a] is V33() real ext-real set
min (r,(m . (a,a))) is V33() real ext-real set
([: the carrier of T, the carrier of T:],r,m) . (a,a) is V33() real ext-real Element of REAL
([: the carrier of T, the carrier of T:],r,m) . [a,a] is V33() real ext-real set
c is Element of the carrier of T
([: the carrier of T, the carrier of T:],r,m) . (a,c) is V33() real ext-real Element of REAL
[a,c] is non empty set
{.c,.} is non empty finite countable set
{.{..},.} is non empty finite V45() countable set
([: the carrier of T, the carrier of T:],r,m) . [a,c] is V33() real ext-real set
b is Element of the carrier of T
([: the carrier of T, the carrier of T:],r,m) . (a,b) is V33() real ext-real Element of REAL
[a,b] is non empty set
{.b,.} is non empty finite countable set
{.{..},.} is non empty finite V45() countable set
([: the carrier of T, the carrier of T:],r,m) . [a,b] is V33() real ext-real set
([: the carrier of T, the carrier of T:],r,m) . (c,b) is V33() real ext-real Element of REAL
[c,b] is non empty set
{.b,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
([: the carrier of T, the carrier of T:],r,m) . [c,b] is V33() real ext-real set
(([: the carrier of T, the carrier of T:],r,m) . (a,b)) + (([: the carrier of T, the carrier of T:],r,m) . (c,b)) is V33() real ext-real Element of REAL
m . (a,c) is V33() real ext-real Element of REAL
m . [a,c] is V33() real ext-real set
min (r,(m . (a,c))) is V33() real ext-real set
m . (c,b) is V33() real ext-real Element of REAL
m . [c,b] is V33() real ext-real set
min (r,(m . (c,b))) is V33() real ext-real set
m . (a,b) is V33() real ext-real Element of REAL
m . [a,b] is V33() real ext-real set
min (r,(m . (a,b))) is V33() real ext-real set
m . (a,c) is V33() real ext-real Element of REAL
m . [a,c] is V33() real ext-real set
min (r,(m . (a,c))) is V33() real ext-real set
(m . (a,b)) + (m . (c,b)) is V33() real ext-real Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty V119() V120() V121() set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty set
r is V33() real ext-real Element of REAL
m is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty V14([: the carrier of T, the carrier of T:]) quasi_total V119() V120() V121() Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
([: the carrier of T, the carrier of T:],r,m) is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty V14([: the carrier of T, the carrier of T:]) quasi_total V119() V120() V121() Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
a is Element of the carrier of T
b is Element of the carrier of T
([: the carrier of T, the carrier of T:],r,m) . (a,b) is V33() real ext-real Element of REAL
[a,b] is non empty set
{.b,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
([: the carrier of T, the carrier of T:],r,m) . [a,b] is V33() real ext-real set
([: the carrier of T, the carrier of T:],r,m) . (b,a) is V33() real ext-real Element of REAL
[b,a] is non empty set
{.a,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
([: the carrier of T, the carrier of T:],r,m) . [b,a] is V33() real ext-real set
c is Element of the carrier of T
([: the carrier of T, the carrier of T:],r,m) . (a,c) is V33() real ext-real Element of REAL
[a,c] is non empty set
{.c,.} is non empty finite countable set
{.{..},.} is non empty finite V45() countable set
([: the carrier of T, the carrier of T:],r,m) . [a,c] is V33() real ext-real set
([: the carrier of T, the carrier of T:],r,m) . (b,c) is V33() real ext-real Element of REAL
[b,c] is non empty set
{.c,.} is non empty finite countable set
{.{..},.} is non empty finite V45() countable set
([: the carrier of T, the carrier of T:],r,m) . [b,c] is V33() real ext-real set
(([: the carrier of T, the carrier of T:],r,m) . (a,b)) + (([: the carrier of T, the carrier of T:],r,m) . (b,c)) is V33() real ext-real Element of REAL
ft is Element of the carrier of T
m . (ft,ft) is V33() real ext-real Element of REAL
[ft,ft] is non empty set
{.ft,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
m . [ft,ft] is V33() real ext-real set
R is Element of the carrier of T
s is Element of the carrier of T
m . (R,s) is V33() real ext-real Element of REAL
[R,s] is non empty set
{.s,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
m . [R,s] is V33() real ext-real set
m . (s,R) is V33() real ext-real Element of REAL
[s,R] is non empty set
{.R,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
m . [s,R] is V33() real ext-real set
B is Element of the carrier of T
mfx is Element of the carrier of T
m . (B,mfx) is V33() real ext-real Element of REAL
[B,mfx] is non empty set
{.mfx,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
m . [B,mfx] is V33() real ext-real set
U is Element of the carrier of T
m . (B,U) is V33() real ext-real Element of REAL
[B,U] is non empty set
{.U,.} is non empty finite countable set
{.{..},.} is non empty finite V45() countable set
m . [B,U] is V33() real ext-real set
m . (U,mfx) is V33() real ext-real Element of REAL
[U,mfx] is non empty set
{.mfx,.} is non empty finite countable set
{..} is non empty trivial finite countable set
{.{..},.} is non empty finite V45() countable set
m . [U,mfx] is V33() real ext-real set
(m . (B,U)) + (m . (U,mfx)) is V33() real ext-real Element of REAL
m . (a,b) is V33() real ext-real Element of REAL
m . [a,b] is V33() real ext-real set
min (r,(m . (a,b))) is V33() real ext-real set