REAL is non empty non trivial non finite V76() V77() V78() V82() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() Element of bool REAL
bool REAL is non empty non trivial non finite set
{} is set
the Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V35() real ext-real non positive non negative finite V49() cardinal {} -element FinSequence-membered V76() V77() V78() V79() V80() V81() V82() set is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V35() real ext-real non positive non negative finite V49() cardinal {} -element FinSequence-membered V76() V77() V78() V79() V80() V81() V82() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
{{},1} is finite set
COMPLEX is non empty non trivial non finite V76() V82() set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() set
bool omega is non empty non trivial non finite set
[:NAT,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty non trivial non finite set
bool (bool REAL) is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K115(NAT) is V26() set
RAT is non empty non trivial non finite V76() V77() V78() V79() V82() set
INT is non empty non trivial non finite V76() V77() V78() V79() V80() V82() set
[:1,1:] is RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set
bool [:1,1:] is non empty finite V49() set
[:[:1,1:],1:] is RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set
bool [:[:1,1:],1:] is non empty finite V49() set
[:[:1,1:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:1,1:],REAL:] is non empty non trivial non finite set
[:REAL,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
[:[:REAL,REAL:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
[:2,2:] is RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set
[:[:2,2:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:2,2:],REAL:] is non empty non trivial non finite set
K546() is non empty strict TopSpace-like V162() TopStruct
the carrier of K546() is non empty V76() V77() V78() set
RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V162() MetrStruct
R^1 is non empty strict TopSpace-like T_0 T_1 T_2 V162() TopStruct
K553() is non empty strict TopSpace-like V162() SubSpace of R^1
[:COMPLEX,COMPLEX:] is non empty non trivial non finite complex-valued set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:COMPLEX,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:COMPLEX,REAL:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite complex-valued set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
bool [:REAL,REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is RAT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is RAT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
K680(2) is V222() L15()
the carrier of K680(2) is set
[: the carrier of K680(2),REAL:] is complex-valued ext-real-valued real-valued set
bool [: the carrier of K680(2),REAL:] is non empty set
bool the carrier of K680(2) is non empty set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
real_dist is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
MetrStruct(# REAL,real_dist #) is strict MetrStruct
the carrier of RealSpace is non empty V76() V77() V78() set
TopSpaceMetr RealSpace is TopStruct
the carrier of R^1 is non empty V76() V77() V78() set
dom {} is set
rng {} is set
4 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
T is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
T + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
Bn is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
0 * 2 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(0 * 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
1 * ((0 * 2) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
Bn mod 2 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set
2 * bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * bbcT) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 |^ 0 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 * PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * PM) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 |^ 0) * ((2 * PM) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
Bn mod 2 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set
2 * bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * bbcT) + 0 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
PM + PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
FB is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 |^ FB is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
TPM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 * TPM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * TPM) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 |^ FB) * ((2 * TPM) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 * (2 |^ FB) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * (2 |^ FB)) * ((2 * TPM) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
FB + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 |^ (FB + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 |^ (FB + 1)) * ((2 * TPM) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
Bn mod 2 is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 |^ bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 * PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * PM) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 |^ bbcT) * ((2 * PM) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
T is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
Bn is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
T is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 |^ T is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
Bn is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 * Bn is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * Bn) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 |^ T) * ((2 * Bn) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
((2 |^ T) * ((2 * Bn) + 1)) - 1 is V35() real ext-real Element of REAL
T is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]
Bn is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 |^ Bn is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
[Bn,bbcT] is Element of [:NAT,NAT:]
{Bn,bbcT} is finite V49() V76() V77() V78() V79() V80() V81() set
{Bn} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() set
{{Bn,bbcT},{Bn}} is finite V49() set
T . [Bn,bbcT] is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 * bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * bbcT) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 |^ Bn) * ((2 * bbcT) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
((2 |^ Bn) * ((2 * bbcT) + 1)) - 1 is V35() real ext-real Element of REAL
T . (Bn,bbcT) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
[Bn,bbcT] is set
T . [Bn,bbcT] is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set
In ((((2 |^ Bn) * ((2 * bbcT) + 1)) - 1),NAT) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
T is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]
Bn is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]
bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
[bbcT,PM] is Element of [:NAT,NAT:]
{bbcT,PM} is finite V49() V76() V77() V78() V79() V80() V81() set
{bbcT} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() set
{{bbcT,PM},{bbcT}} is finite V49() set
T . [bbcT,PM] is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 |^ bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 * PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * PM) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 |^ bbcT) * ((2 * PM) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
((2 |^ bbcT) * ((2 * PM) + 1)) - 1 is V35() real ext-real Element of REAL
T . (bbcT,PM) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
[bbcT,PM] is set
T . [bbcT,PM] is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set
Bn . (bbcT,PM) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
Bn . [bbcT,PM] is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set
() is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]
T is set
Bn is set
() . T is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal Element of REAL
() . Bn is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal Element of REAL
bbcT is set
PM is set
[bbcT,PM] is set
{bbcT,PM} is finite set
{bbcT} is non empty trivial finite 1 -element set
{{bbcT,PM},{bbcT}} is finite V49() set
FB is set
TPM is set
[FB,TPM] is set
{FB,TPM} is finite set
{FB} is non empty trivial finite 1 -element set
{{FB,TPM},{FB}} is finite V49() set
UX is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 |^ UX is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 * k is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * k) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 |^ UX) * ((2 * k) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
((2 |^ UX) * ((2 * k) + 1)) - 1 is V35() real ext-real Element of REAL
Un is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 |^ Un is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
UXk is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 * UXk is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * UXk) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 |^ Un) * ((2 * UXk) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
((2 |^ Un) * ((2 * UXk) + 1)) - 1 is V35() real ext-real Element of REAL
T is set
Bn is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
Bn + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 |^ bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
2 * PM is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 * PM) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
(2 |^ bbcT) * ((2 * PM) + 1) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
Bn - 0 is V35() real ext-real Element of REAL
((2 |^ bbcT) * ((2 * PM) + 1)) - 1 is V35() real ext-real Element of REAL
dom () is Relation-like NAT -defined NAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
[bbcT,PM] is Element of [:NAT,NAT:]
{bbcT,PM} is finite V49() V76() V77() V78() V79() V80() V81() set
{bbcT} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() set
{{bbcT,PM},{bbcT}} is finite V49() set
() . [bbcT,PM] is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of NAT
rng () is V76() V77() V78() V79() V80() V81() Element of bool NAT
T is set
[:T,T:] is set
[:[:T,T:],REAL:] is complex-valued ext-real-valued real-valued set
bool [:[:T,T:],REAL:] is non empty set
[:T,REAL:] is complex-valued ext-real-valued real-valued set
bool [:T,REAL:] is non empty set
Bn is Relation-like [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]
bbcT is Element of T
PM is set
Bn . (bbcT,PM) is set
[bbcT,PM] is set
{bbcT,PM} is finite set
{bbcT} is non empty trivial finite 1 -element set
{{bbcT,PM},{bbcT}} is finite V49() set
Bn . [bbcT,PM] is V35() real ext-real set
Bn . [bbcT,PM] is V35() real ext-real Element of REAL
PM is Relation-like T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
FB is Element of T
[bbcT,FB] is set
{bbcT,FB} is finite set
{bbcT} is non empty trivial finite 1 -element set
{{bbcT,FB},{bbcT}} is finite V49() set
dom Bn is Relation-like T -defined T -valued Element of bool [:T,T:]
bool [:T,T:] is non empty set
Bn . [bbcT,FB] is V35() real ext-real Element of REAL
dom PM is Element of bool T
bool T is non empty set
Bn . (bbcT,FB) is V35() real ext-real Element of REAL
Bn . [bbcT,FB] is V35() real ext-real set
PM . FB is V35() real ext-real Element of REAL
FB is Element of T
PM . FB is V35() real ext-real Element of REAL
Bn . (bbcT,FB) is V35() real ext-real Element of REAL
[bbcT,FB] is set
{bbcT,FB} is finite set
{bbcT} is non empty trivial finite 1 -element set
{{bbcT,FB},{bbcT}} is finite V49() set
Bn . [bbcT,FB] is V35() real ext-real set
PM is Relation-like T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
FB is Relation-like T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
TPM is Element of T
PM . TPM is V35() real ext-real Element of REAL
Bn . (bbcT,TPM) is V35() real ext-real Element of REAL
[bbcT,TPM] is set
{bbcT,TPM} is finite set
{bbcT} is non empty trivial finite 1 -element set
{{bbcT,TPM},{bbcT}} is finite V49() set
Bn . [bbcT,TPM] is V35() real ext-real set
FB . TPM is V35() real ext-real Element of 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
Bn is non empty TopSpace-like TopStruct
[:T,Bn:] is non empty strict TopSpace-like TopStruct
the carrier of [:T,Bn:] is non empty set
bool the carrier of [:T,Bn:] is non empty set
the carrier of Bn is non empty set
bool the carrier of Bn is non empty set
[: the carrier of T, the carrier of Bn:] is non empty set
pr1 ( the carrier of T, the carrier of Bn) is Relation-like [: the carrier of T, the carrier of Bn:] -defined the carrier of T -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of T, the carrier of Bn:], the carrier of T:]
[:[: the carrier of T, the carrier of Bn:], the carrier of T:] is non empty set
bool [:[: the carrier of T, the carrier of Bn:], the carrier of T:] is non empty set
pr2 ( the carrier of T, the carrier of Bn) is Relation-like [: the carrier of T, the carrier of Bn:] -defined the carrier of Bn -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of T, the carrier of Bn:], the carrier of Bn:]
[:[: the carrier of T, the carrier of Bn:], the carrier of Bn:] is non empty set
bool [:[: the carrier of T, the carrier of Bn:], the carrier of Bn:] is non empty set
FB is Element of bool the carrier of [:T,Bn:]
bool (bool the carrier of [:T,Bn:]) is non empty set
TPM is Element of bool (bool the carrier of [:T,Bn:])
union TPM is Element of bool the carrier of [:T,Bn:]
Un is Element of the carrier of T
{Un} is non empty trivial finite 1 -element Element of bool the carrier of T
[:{Un}, the carrier of Bn:] is non empty set
FB /\ [:{Un}, the carrier of Bn:] is Element of bool the carrier of [:T,Bn:]
(pr2 ( the carrier of T, the carrier of Bn)) .: (FB /\ [:{Un}, the carrier of Bn:]) is Element of bool the carrier of Bn
UX is Element of the carrier of Bn
{UX} is non empty trivial finite 1 -element Element of bool the carrier of Bn
[: the carrier of T,{UX}:] is non empty set
FB /\ [: the carrier of T,{UX}:] is Element of bool the carrier of [:T,Bn:]
(pr1 ( the carrier of T, the carrier of Bn)) .: (FB /\ [: the carrier of T,{UX}:]) is Element of bool the carrier of T
UXk is Element of bool the carrier of T
k is Element of bool the carrier of Bn
UXk9 is set
dom (pr1 ( the carrier of T, the carrier of Bn)) is Relation-like the carrier of T -defined the carrier of Bn -valued Element of bool [: the carrier of T, the carrier of Bn:]
bool [: the carrier of T, the carrier of Bn:] is non empty set
nm is set
(pr1 ( the carrier of T, the carrier of Bn)) . nm is set
n is set
m is Element of bool the carrier of T
Unn is Element of bool the carrier of Bn
[:m,Unn:] is Element of bool the carrier of [:T,Bn:]
B is set
B1 is set
[B,B1] is set
{B,B1} is finite set
{B} is non empty trivial finite 1 -element set
{{B,B1},{B}} is finite V49() set
k is set
[k,UX] is set
{k,UX} is finite set
{k} is non empty trivial finite 1 -element set
{{k,UX},{k}} is finite V49() set
(pr1 ( the carrier of T, the carrier of Bn)) . (k,UX) is set
(pr1 ( the carrier of T, the carrier of Bn)) . [k,UX] is set
(pr1 ( the carrier of T, the carrier of Bn)) . (B,B1) is set
(pr1 ( the carrier of T, the carrier of Bn)) . [B,B1] is set
nm is Element of bool the carrier of T
n is Element of bool the carrier of T
UXk9 is set
dom (pr2 ( the carrier of T, the carrier of Bn)) is Relation-like the carrier of T -defined the carrier of Bn -valued Element of bool [: the carrier of T, the carrier of Bn:]
bool [: the carrier of T, the carrier of Bn:] is non empty set
nm is set
(pr2 ( the carrier of T, the carrier of Bn)) . nm is set
n is set
m is set
Unn is set
[m,Unn] is set
{m,Unn} is finite set
{m} is non empty trivial finite 1 -element set
{{m,Unn},{m}} is finite V49() set
(pr2 ( the carrier of T, the carrier of Bn)) . (m,Unn) is set
(pr2 ( the carrier of T, the carrier of Bn)) . [m,Unn] is set
B is Element of bool the carrier of T
B1 is Element of bool the carrier of Bn
[:B,B1:] is Element of bool the carrier of [:T,Bn:]
k is set
[Un,k] is set
{Un,k} is finite set
{Un} is non empty trivial finite 1 -element set
{{Un,k},{Un}} is finite V49() set
(pr2 ( the carrier of T, the carrier of Bn)) . (Un,k) is set
(pr2 ( the carrier of T, the carrier of Bn)) . [Un,k] is set
nm is Element of bool the carrier of Bn
n is Element of bool the carrier of Bn
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 non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite 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 non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of [:T,T:],REAL:] is non empty non trivial non finite set
bbcT is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
[: the carrier of [:T,T:], the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set
bool [: the carrier of [:T,T:], the carrier of R^1:] is non empty set
PM is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
TPM is Element of the carrier of T
( the carrier of T,bbcT,TPM) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
[: the carrier of T, the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set
bool [: the carrier of T, the carrier of R^1:] is non empty set
FB is Relation-like the carrier of [:T,T:] -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:], the carrier of R^1:]
bool the carrier of R^1 is non empty set
Un is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T, the carrier of R^1:]
UX is Element of the carrier of T
Un . UX is V35() real ext-real Element of the carrier of R^1
bool the carrier of T is non empty set
[TPM,UX] is Element of [: the carrier of T, the carrier of T:]
{TPM,UX} is finite set
{TPM} is non empty trivial finite 1 -element set
{{TPM,UX},{TPM}} is finite V49() set
pr2 ( the carrier of T, the carrier of T) is Relation-like [: the carrier of T, the carrier of T:] -defined the carrier of T -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of T, the carrier of T:], the carrier of T:]
[:[: the carrier of T, the carrier of T:], the carrier of T:] is non empty set
bool [:[: the carrier of T, the carrier of T:], the carrier of T:] is non empty set
dom (pr2 ( the carrier of T, the carrier of T)) is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
bool [: the carrier of T, the carrier of T:] is non empty set
UXk is Element of the carrier of [:T,T:]
bbcT . (TPM,UX) is V35() real ext-real Element of REAL
[TPM,UX] is set
bbcT . [TPM,UX] is V35() real ext-real set
k is V76() V77() V78() Element of bool the carrier of R^1
bool the carrier of [:T,T:] is non empty set
UXk9 is Element of bool the carrier of [:T,T:]
FB .: UXk9 is V76() V77() V78() Element of bool the carrier of R^1
{TPM} is non empty trivial finite 1 -element Element of bool the carrier of T
[:{TPM}, the carrier of T:] is non empty set
UXk9 /\ [:{TPM}, the carrier of T:] is Element of bool the carrier of [:T,T:]
(pr2 ( the carrier of T, the carrier of T)) .: (UXk9 /\ [:{TPM}, the carrier of T:]) is Element of bool the carrier of T
(pr2 ( the carrier of T, the carrier of T)) . (TPM,UX) is Element of the carrier of T
(pr2 ( the carrier of T, the carrier of T)) . [TPM,UX] is set
Un .: ((pr2 ( the carrier of T, the carrier of T)) .: (UXk9 /\ [:{TPM}, the carrier of T:])) is V76() V77() V78() Element of bool the carrier of R^1
n is set
dom Un is Element of bool the carrier of T
m is set
Un . m is V35() real ext-real Element of REAL
Unn is Element of the carrier of T
B is set
(pr2 ( the carrier of T, the carrier of T)) . B is set
B1 is set
k is set
[B1,k] is set
{B1,k} is finite set
{B1} is non empty trivial finite 1 -element set
{{B1,k},{B1}} is finite V49() set
q is Element of the carrier of T
s is Element of the carrier of T
[q,s] is Element of [: the carrier of T, the carrier of T:]
{q,s} is finite set
{q} is non empty trivial finite 1 -element set
{{q,s},{q}} is finite V49() set
(pr2 ( the carrier of T, the carrier of T)) . (q,s) is Element of the carrier of T
[q,s] is set
(pr2 ( the carrier of T, the carrier of T)) . [q,s] is set
bbcT . (q,s) is V35() real ext-real Element of REAL
bbcT . [q,s] is V35() real ext-real set
dom FB is Element of bool the carrier of [:T,T:]
T is non empty set
[:T,T:] is non empty set
[:[:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:T,T:],REAL:] is non empty non trivial non finite set
bool T is non empty set
[:T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:T,REAL:] is non empty non trivial non finite set
Bn is Relation-like [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]
bbcT is Element of bool T
PM is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
FB is Element of T
PM . FB is V35() real ext-real Element of REAL
(T,Bn,FB) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
(T,Bn,FB) .: bbcT is V76() V77() V78() Element of bool REAL
lower_bound ((T,Bn,FB) .: bbcT) is V35() real ext-real Element of REAL
PM is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
FB is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
TPM is Element of T
PM . TPM is V35() real ext-real Element of REAL
(T,Bn,TPM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
(T,Bn,TPM) .: bbcT is V76() V77() V78() Element of bool REAL
lower_bound ((T,Bn,TPM) .: bbcT) is V35() real ext-real Element of REAL
FB . TPM is V35() real ext-real Element of REAL
T is non empty set
[:T,T:] is non empty set
[:[:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:T,T:],REAL:] is non empty non trivial non finite set
bool T is non empty set
Bn is Relation-like [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]
PM is Element of T
(T,Bn,PM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
[:T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:T,REAL:] is non empty non trivial non finite set
bbcT is non empty Element of bool T
(T,Bn,PM) .: bbcT is V76() V77() V78() Element of bool REAL
FB is ext-real set
dom (T,Bn,PM) is Element of bool T
TPM is set
(T,Bn,PM) . TPM is V35() real ext-real Element of REAL
Un is Element of T
Bn . (PM,Un) is V35() real ext-real Element of REAL
[PM,Un] is set
{PM,Un} is finite set
{PM} is non empty trivial finite 1 -element set
{{PM,Un},{PM}} is finite V49() set
Bn . [PM,Un] is V35() real ext-real set
dom (T,Bn,PM) is Element of bool T
bbcT is set
dom Bn is Relation-like T -defined T -valued Element of bool [:T,T:]
bool [:T,T:] is non empty set
PM is set
FB is set
[PM,FB] is set
{PM,FB} is finite set
{PM} is non empty trivial finite 1 -element set
{{PM,FB},{PM}} is finite V49() set
TPM is Element of T
Un is Element of T
Bn . (TPM,Un) is V35() real ext-real Element of REAL
[TPM,Un] is set
{TPM,Un} is finite set
{TPM} is non empty trivial finite 1 -element set
{{TPM,Un},{TPM}} is finite V49() set
Bn . [TPM,Un] is V35() real ext-real set
- 1 is V35() real ext-real non positive Element of REAL
Bn . bbcT is V35() real ext-real Element of REAL
PM is Element of T
(T,Bn,PM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
bbcT is non empty Element of bool T
(T,Bn,PM) .: bbcT is V76() V77() V78() Element of bool REAL
TPM is Element of T
(T,Bn,TPM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
FB is non empty Element of bool T
(T,Bn,TPM) .: FB is V76() V77() V78() Element of bool REAL
T is non empty set
[:T,T:] is non empty set
[:[:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:T,T:],REAL:] is non empty non trivial non finite set
bool T is non empty set
Bn is Relation-like [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]
bbcT is non empty Element of bool T
(T,Bn,bbcT) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
[:T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:T,REAL:] is non empty non trivial non finite set
PM is Element of T
(T,Bn,bbcT) . PM is V35() real ext-real Element of REAL
FB is V35() real ext-real set
(T,Bn,PM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
(T,Bn,PM) .: bbcT is V76() V77() V78() Element of bool REAL
dom (T,Bn,PM) is Element of bool T
TPM is set
(T,Bn,PM) . TPM is V35() real ext-real Element of REAL
Bn . (PM,TPM) is set
[PM,TPM] is set
{PM,TPM} is finite set
{PM} is non empty trivial finite 1 -element set
{{PM,TPM},{PM}} is finite V49() set
Bn . [PM,TPM] is V35() real ext-real set
lower_bound ((T,Bn,PM) .: bbcT) is V35() real ext-real Element of REAL
T is non empty set
[:T,T:] is non empty set
[:[:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:T,T:],REAL:] is non empty non trivial non finite set
bool T is non empty set
Bn is Relation-like [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]
bbcT is Element of bool T
(T,Bn,bbcT) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
[:T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:T,REAL:] is non empty non trivial non finite set
PM is Element of T
(T,Bn,bbcT) . PM is V35() real ext-real Element of REAL
(T,Bn,PM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
FB is non empty Element of bool T
(T,Bn,PM) .: FB is V76() V77() V78() Element of bool REAL
Bn . (PM,PM) is V35() real ext-real Element of REAL
[PM,PM] is set
{PM,PM} is finite set
{PM} is non empty trivial finite 1 -element set
{{PM,PM},{PM}} is finite V49() set
Bn . [PM,PM] is V35() real ext-real set
dom (T,Bn,PM) is Element of bool T
(T,Bn,PM) . PM is V35() real ext-real Element of REAL
lower_bound ((T,Bn,PM) .: FB) is V35() real ext-real Element of REAL
(T,Bn,FB) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
(T,Bn,FB) . PM is V35() 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 non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set
bool the carrier of T is non empty set
Bn is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
bbcT is Element of the carrier of T
PM is Element of the carrier of T
Bn . (bbcT,PM) is V35() real ext-real Element of REAL
[bbcT,PM] is set
{bbcT,PM} is finite set
{bbcT} is non empty trivial finite 1 -element set
{{bbcT,PM},{bbcT}} is finite V49() set
Bn . [bbcT,PM] is V35() real ext-real set
FB is non empty Element of bool the carrier of T
( the carrier of T,Bn,FB) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
( the carrier of T,Bn,FB) . bbcT is V35() real ext-real Element of REAL
( the carrier of T,Bn,FB) . PM is V35() real ext-real Element of REAL
(( the carrier of T,Bn,FB) . bbcT) - (( the carrier of T,Bn,FB) . PM) is V35() real ext-real Element of REAL
abs ((( the carrier of T,Bn,FB) . bbcT) - (( the carrier of T,Bn,FB) . PM)) is V35() real ext-real Element of REAL
TPM is Element of the carrier of T
Un is Element of the carrier of T
Bn . (TPM,Un) is V35() real ext-real Element of REAL
[TPM,Un] is set
{TPM,Un} is finite set
{TPM} is non empty trivial finite 1 -element set
{{TPM,Un},{TPM}} is finite V49() set
Bn . [TPM,Un] is V35() real ext-real set
- (Bn . (TPM,Un)) is V35() real ext-real Element of REAL
( the carrier of T,Bn,FB) . Un is V35() real ext-real Element of REAL
( the carrier of T,Bn,FB) . TPM is V35() real ext-real Element of REAL
(( the carrier of T,Bn,FB) . Un) - (( the carrier of T,Bn,FB) . TPM) is V35() real ext-real Element of REAL
( the carrier of T,Bn,TPM) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
( the carrier of T,Bn,TPM) .: FB is V76() V77() V78() Element of bool REAL
( the carrier of T,Bn,Un) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
( the carrier of T,Bn,Un) .: FB is V76() V77() V78() Element of bool REAL
lower_bound (( the carrier of T,Bn,TPM) .: FB) is V35() real ext-real Element of REAL
(lower_bound (( the carrier of T,Bn,TPM) .: FB)) - (Bn . (TPM,Un)) is V35() real ext-real Element of REAL
UX is V35() real ext-real set
dom ( the carrier of T,Bn,Un) is Element of bool the carrier of T
UXk is set
( the carrier of T,Bn,Un) . UXk is V35() real ext-real Element of REAL
k is Element of the carrier of T
( the carrier of T,Bn,TPM) . k is V35() real ext-real Element of REAL
Bn . (TPM,k) is V35() real ext-real Element of REAL
[TPM,k] is set
{TPM,k} is finite set
{{TPM,k},{TPM}} is finite V49() set
Bn . [TPM,k] is V35() real ext-real set
Bn . (Un,k) is V35() real ext-real Element of REAL
[Un,k] is set
{Un,k} is finite set
{Un} is non empty trivial finite 1 -element set
{{Un,k},{Un}} is finite V49() set
Bn . [Un,k] is V35() real ext-real set
(Bn . (TPM,Un)) + (Bn . (Un,k)) is V35() real ext-real Element of REAL
dom ( the carrier of T,Bn,TPM) is Element of bool the carrier of T
(lower_bound (( the carrier of T,Bn,TPM) .: FB)) + 0 is V35() real ext-real Element of REAL
(Bn . (Un,k)) - 0 is V35() real ext-real Element of REAL
lower_bound (( the carrier of T,Bn,Un) .: FB) is V35() real ext-real Element of REAL
(lower_bound (( the carrier of T,Bn,Un) .: FB)) - 0 is V35() real ext-real Element of REAL
0 - (Bn . (TPM,Un)) is V35() real ext-real Element of REAL
(lower_bound (( the carrier of T,Bn,Un) .: FB)) - (lower_bound (( the carrier of T,Bn,TPM) .: FB)) is V35() real ext-real Element of REAL
- (Bn . (bbcT,PM)) is V35() real ext-real Element of REAL
(( the carrier of T,Bn,FB) . PM) - (( the carrier of T,Bn,FB) . bbcT) is V35() real ext-real Element of REAL
- ((( the carrier of T,Bn,FB) . bbcT) - (( the carrier of T,Bn,FB) . PM)) is V35() real ext-real Element of REAL
Bn . (PM,bbcT) is V35() real ext-real Element of REAL
[PM,bbcT] is set
{PM,bbcT} is finite set
{PM} is non empty trivial finite 1 -element set
{{PM,bbcT},{PM}} is finite V49() set
Bn . [PM,bbcT] is V35() real ext-real set
- (Bn . (PM,bbcT)) is V35() 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 non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set
bool the carrier of T is non empty set
Bn is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
bbcT is non empty Element of bool the carrier of T
( the carrier of T,Bn,bbcT) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
[: the carrier of T, the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set
bool [: the carrier of T, the carrier of R^1:] is non empty set
FB is Element of the carrier of T
( the carrier of T,Bn,FB) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
bool the carrier of R^1 is non empty set
PM is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T, the carrier of R^1:]
PM . FB is V35() real ext-real Element of the carrier of R^1
PM . FB is V35() real ext-real Element of REAL
TPM is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T, the carrier of R^1:]
TPM . FB is V35() real ext-real Element of REAL
UXk is V76() V77() V78() Element of bool the carrier of R^1
Un is V35() real ext-real Element of the carrier of RealSpace
k is V35() real ext-real set
Ball (Un,k) is V76() V77() V78() Element of bool the carrier of RealSpace
bool the carrier of RealSpace is non empty set
UX is V35() real ext-real Element of the carrier of RealSpace
Ball (UX,k) is V76() V77() V78() Element of bool the carrier of RealSpace
TPM . FB is V35() real ext-real Element of the carrier of R^1
(TPM . FB) - (TPM . FB) is V35() real ext-real set
abs ((TPM . FB) - (TPM . FB)) is V35() real ext-real Element of REAL
dist (UX,UX) is V35() real ext-real Element of REAL
UXk9 is V76() V77() V78() Element of bool the carrier of R^1
nm is Element of bool the carrier of T
TPM .: nm is V76() V77() V78() Element of bool the carrier of R^1
PM .: nm is V76() V77() V78() Element of bool the carrier of R^1
n is set
dom PM is Element of bool the carrier of T
m is set
PM . m is V35() real ext-real Element of REAL
Unn is Element of the carrier of T
PM . Unn is V35() real ext-real Element of REAL
TPM . Unn is V35() real ext-real Element of REAL
Bn . (FB,Unn) is V35() real ext-real Element of REAL
[FB,Unn] is set
{FB,Unn} is finite set
{FB} is non empty trivial finite 1 -element set
{{FB,Unn},{FB}} is finite V49() set
Bn . [FB,Unn] is V35() real ext-real set
TPM . Unn is V35() real ext-real Element of the carrier of R^1
Bn . (FB,FB) is V35() real ext-real Element of REAL
[FB,FB] is set
{FB,FB} is finite set
{{FB,FB},{FB}} is finite V49() set
Bn . [FB,FB] is V35() real ext-real set
B1 is V35() real ext-real Element of the carrier of RealSpace
dist (UX,B1) is V35() real ext-real Element of REAL
0 - (TPM . Unn) is V35() real ext-real Element of REAL
abs (0 - (TPM . Unn)) is V35() real ext-real Element of REAL
dom TPM is Element of bool the carrier of T
- (0 - (TPM . Unn)) is V35() real ext-real Element of REAL
abs (- (0 - (TPM . Unn))) is V35() real ext-real Element of REAL
( the carrier of T,Bn,bbcT) . FB is V35() real ext-real Element of REAL
( the carrier of T,Bn,bbcT) . Unn is V35() real ext-real Element of REAL
(( the carrier of T,Bn,bbcT) . FB) - (( the carrier of T,Bn,bbcT) . Unn) is V35() real ext-real Element of REAL
abs ((( the carrier of T,Bn,bbcT) . FB) - (( the carrier of T,Bn,bbcT) . Unn)) is V35() real ext-real Element of REAL
B is V35() real ext-real Element of the carrier of RealSpace
dist (Un,B) is V35() real ext-real Element of REAL
T is set
[:T,T:] is set
[:[:T,T:],REAL:] is complex-valued ext-real-valued real-valued set
bool [:[:T,T:],REAL:] is non empty set
Bn is Relation-like [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]
bbcT is Element of T
Bn . (bbcT,bbcT) is V35() real ext-real Element of REAL
[bbcT,bbcT] is set
{bbcT,bbcT} is finite set
{bbcT} is non empty trivial finite 1 -element set
{{bbcT,bbcT},{bbcT}} is finite V49() set
Bn . [bbcT,bbcT] is V35() real ext-real set
PM is Element of T
FB is Element of T
Bn . (PM,FB) is V35() real ext-real Element of REAL
[PM,FB] is set
{PM,FB} is finite set
{PM} is non empty trivial finite 1 -element set
{{PM,FB},{PM}} is finite V49() set
Bn . [PM,FB] is V35() real ext-real set
Bn . (FB,PM) is V35() real ext-real Element of REAL
[FB,PM] is set
{FB,PM} is finite set
{FB} is non empty trivial finite 1 -element set
{{FB,PM},{FB}} is finite V49() set
Bn . [FB,PM] is V35() real ext-real set
TPM is Element of T
UX is Element of T
Bn . (TPM,UX) is V35() real ext-real Element of REAL
[TPM,UX] is set
{TPM,UX} is finite set
{TPM} is non empty trivial finite 1 -element set
{{TPM,UX},{TPM}} is finite V49() set
Bn . [TPM,UX] is V35() real ext-real set
Un is Element of T
Bn . (TPM,Un) is V35() real ext-real Element of REAL
[TPM,Un] is set
{TPM,Un} is finite set
{{TPM,Un},{TPM}} is finite V49() set
Bn . [TPM,Un] is V35() real ext-real set
Bn . (Un,UX) is V35() real ext-real Element of REAL
[Un,UX] is set
{Un,UX} is finite set
{Un} is non empty trivial finite 1 -element set
{{Un,UX},{Un}} is finite V49() set
Bn . [Un,UX] is V35() real ext-real set
(Bn . (TPM,Un)) + (Bn . (Un,UX)) is V35() 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 non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set
bool the carrier of T is non empty set
Bn is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
SpaceMetr ( the carrier of T,Bn) is strict Reflexive discerning symmetric triangle MetrStruct
PM is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of PM is non empty set
FB is Element of the carrier of PM
TPM is Element of the carrier of PM
Bn . (FB,TPM) is set
[FB,TPM] is set
{FB,TPM} is finite set
{FB} is non empty trivial finite 1 -element set
{{FB,TPM},{FB}} is finite V49() set
Bn . [FB,TPM] is V35() real ext-real set
dist (FB,TPM) is V35() real ext-real Element of REAL
MetrStruct(# the carrier of T,Bn #) is strict MetrStruct
Family_open_set PM is Element of bool (bool the carrier of PM)
bool the carrier of PM is non empty set
bool (bool the carrier of PM) is non empty set
the topology of T is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
FB is set
TPM is Element of bool the carrier of T
TPM ` is Element of bool the carrier of T
the carrier of T \ TPM is set
[#] T is non empty non proper open closed Element of bool the carrier of T
([#] T) ` is open closed Element of bool the carrier of T
the carrier of T \ ([#] T) is set
TPM is Element of bool the carrier of T
TPM ` is Element of bool the carrier of T
the carrier of T \ TPM is set
Un is set
UX is Element of the carrier of PM
UXk is V35() real ext-real Element of REAL
Ball (UX,UXk) is Element of bool the carrier of PM
UXk9 is Element of bool the carrier of T
UXk9 ` is Element of bool the carrier of T
the carrier of T \ UXk9 is set
( the carrier of T,Bn,(UXk9 `)) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
{ b1 where b1 is Element of the carrier of T : ( the carrier of T,Bn,(UXk9 `)) . b1 = 0 } is set
n is set
n is set
m is set
( the carrier of T,Bn,(UXk9 `)) . m is V35() real ext-real Element of REAL
m is set
Unn is Element of the carrier of T
( the carrier of T,Bn,(UXk9 `)) . Unn is V35() real ext-real Element of REAL
( the carrier of T,Bn,Unn) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
( the carrier of T,Bn,Unn) .: (UXk9 `) is V76() V77() V78() Element of bool REAL
B is Element of the carrier of PM
B1 is V35() real ext-real Element of REAL
Ball (B,B1) is Element of bool the carrier of PM
lower_bound (( the carrier of T,Bn,Unn) .: (UXk9 `)) is V35() real ext-real Element of REAL
0 + B1 is V35() real ext-real Element of REAL
k is V35() real ext-real set
dom ( the carrier of T,Bn,Unn) is Element of bool the carrier of T
q is set
( the carrier of T,Bn,Unn) . q is V35() real ext-real Element of REAL
s is Element of the carrier of T
Bn . (Unn,s) is V35() real ext-real Element of REAL
[Unn,s] is set
{Unn,s} is finite set
{Unn} is non empty trivial finite 1 -element set
{{Unn,s},{Unn}} is finite V49() set
Bn . [Unn,s] is V35() real ext-real set
b is Element of the carrier of PM
dist (B,b) is V35() real ext-real Element of REAL
Cl (UXk9 `) is closed Element of bool the carrier of T
k is Element of the carrier of T
Bn . (k,k) is V35() real ext-real Element of REAL
[k,k] is set
{k,k} is finite set
{k} is non empty trivial finite 1 -element set
{{k,k},{k}} is finite V49() set
Bn . [k,k] is V35() real ext-real set
dist (UX,UX) is V35() real ext-real Element of REAL
UX is Element of bool the carrier of T
UXk is Element of bool the carrier of T
TPM is Element of bool the carrier of T
TPM ` is Element of bool the carrier of T
the carrier of T \ TPM is set
FB is set
TPM is Element of bool the carrier of T
TPM ` is Element of bool the carrier of T
the carrier of T \ TPM is set
[#] T is non empty non proper open closed Element of bool the carrier of T
([#] T) ` is open closed Element of bool the carrier of T
the carrier of T \ ([#] T) is set
TPM is Element of bool the carrier of T
TPM ` is Element of bool the carrier of T
the carrier of T \ TPM is set
Un is Element of bool the carrier of PM
UX is Element of the carrier of PM
( the carrier of T,Bn,(TPM `)) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
UXk is Element of the carrier of T
( the carrier of T,Bn,(TPM `)) . UXk is V35() real ext-real Element of REAL
k is V35() real ext-real Element of REAL
Ball (UX,k) is Element of bool the carrier of PM
( the carrier of T,Bn,UXk) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
( the carrier of T,Bn,UXk) .: (TPM `) is V76() V77() V78() Element of bool REAL
UXk9 is set
nm is Element of the carrier of PM
dist (UX,nm) is V35() real ext-real Element of REAL
dom ( the carrier of T,Bn,UXk) is Element of bool the carrier of T
n is Element of the carrier of T
( the carrier of T,Bn,UXk) . n is V35() real ext-real Element of REAL
lower_bound (( the carrier of T,Bn,UXk) .: (TPM `)) is V35() real ext-real Element of REAL
Bn . (UXk,n) is V35() real ext-real Element of REAL
[UXk,n] is set
{UXk,n} is finite set
{UXk} is non empty trivial finite 1 -element set