:: TOPREAL7 semantic presentation

REAL is non empty V33() V166() V167() V168() V172() set
NAT is V166() V167() V168() V169() V170() V171() V172() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V33() V166() V172() set
NAT is V166() V167() V168() V169() V170() V171() V172() set
bool NAT is non empty set
I[01] is TopStruct
the carrier of I[01] is set
bool NAT is non empty set
1 is non empty V10() V11() V12() ext-real positive V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
RAT is non empty V33() V166() V167() V168() V169() V172() set
[:1,1:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V141() V142() V143() set
INT is non empty V33() V166() V167() V168() V169() V170() V172() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V141() V142() V143() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is non empty V16() complex-yielding V141() V142() set
[:[:REAL,REAL:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty V10() V11() V12() ext-real positive V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
[:2,2:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V141() V142() V143() set
[:[:2,2:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:2,2:],REAL:] is non empty set
bool [:REAL,REAL:] is non empty set
TOP-REAL 2 is non empty TopSpace-like V105() V130() V131() V132() V133() V134() V135() V136() V181() L15()
the carrier of (TOP-REAL 2) is non empty set
the carrier of (TOP-REAL 2) * is functional FinSequence-membered FinSequenceSet of the carrier of (TOP-REAL 2)
[:COMPLEX,COMPLEX:] is non empty V16() complex-yielding set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V16() complex-yielding set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:RAT,RAT:] is non empty V16() V20( RAT ) complex-yielding V141() V142() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty V16() V20( RAT ) complex-yielding V141() V142() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V141() V142() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty V16() V20( RAT ) V20( INT ) complex-yielding V141() V142() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is V16() V20( RAT ) V20( INT ) complex-yielding V141() V142() V143() set
[:[:NAT,NAT:],NAT:] is V16() V20( RAT ) V20( INT ) complex-yielding V141() V142() V143() set
bool [:[:NAT,NAT:],NAT:] is non empty set
{} is set
the empty V16() non-empty empty-yielding V20( RAT ) complex-yielding V141() V142() V143() V166() V167() V168() V169() V170() V171() V172() set is empty V16() non-empty empty-yielding V20( RAT ) complex-yielding V141() V142() V143() V166() V167() V168() V169() V170() V171() V172() set
0 is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
absreal is V16() V19( REAL ) V20( REAL ) Function-like V30( REAL , REAL ) complex-yielding V141() V142() Element of bool [:REAL,REAL:]
i is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
i + f is V11() V12() ext-real Element of REAL
j is V11() V12() ext-real Element of REAL
c₄ is V11() V12() ext-real Element of REAL
j + c₄ is V11() V12() ext-real Element of REAL
max ((i + f),(j + c₄)) is V11() V12() ext-real Element of REAL
max (i,j) is V11() V12() ext-real Element of REAL
max (f,c₄) is V11() V12() ext-real Element of REAL
(max (i,j)) + (max (f,c₄)) is V11() V12() ext-real Element of REAL
i is V11() V12() ext-real Element of REAL
j is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
j + f is V11() V12() ext-real Element of REAL
c₄ is V11() V12() ext-real Element of REAL
cij is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
cij + f is V11() V12() ext-real Element of REAL
max (i,c₄) is V11() V12() ext-real Element of REAL
max (j,cij) is V11() V12() ext-real Element of REAL
max (f,f) is V11() V12() ext-real Element of REAL
(max (j,cij)) + (max (f,f)) is V11() V12() ext-real Element of REAL
max ((j + f),(cij + f)) is V11() V12() ext-real Element of REAL
j is V16() Function-like FinSequence-like set
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
i is V16() Function-like FinSequence-like set
i ^ j is V16() Function-like FinSequence-like set
dom (i ^ j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len i) + (len j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Seg (len j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
Seg ((len i) + (len j)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
i is V10() V11() V12() ext-real V89() set
j is V16() Function-like FinSequence-like set
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
f is V16() Function-like FinSequence-like set
len f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len j) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i - (len j) is V11() V12() ext-real V89() Element of REAL
dom f is V166() V167() V168() V169() V170() V171() Element of bool NAT
((len j) + (len f)) - (len j) is V11() V12() ext-real V89() Element of REAL
(len j) - (len j) is V11() V12() ext-real V89() Element of REAL
i is V16() Function-like FinSequence-like set
j is V16() Function-like FinSequence-like set
i ^ j is V16() Function-like FinSequence-like set
f is V16() Function-like FinSequence-like set
c₄ is V16() Function-like FinSequence-like set
f ^ c₄ is V16() Function-like FinSequence-like set
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len c₄ is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
cij is V10() V11() V12() ext-real V89() set
i . cij is set
f . cij is set
dom f is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
(i ^ j) . cij is set
cij is V10() V11() V12() ext-real V89() set
j . cij is set
c₄ . cij is set
dom c₄ is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
(len i) + cij is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(i ^ j) . ((len i) + cij) is set
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
i + j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len (i + j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom (i + j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
(len i) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
f is V16() V19( NAT ) V20( REAL ) Function-like V40( len i) FinSequence-like complex-yielding V141() V142() Element of (len i) -tuples_on REAL
c₄ is V16() V19( NAT ) V20( REAL ) Function-like V40( len i) FinSequence-like complex-yielding V141() V142() Element of (len i) -tuples_on REAL
f + c₄ is V16() V19( NAT ) V20( REAL ) Function-like V40( len i) FinSequence-like complex-yielding V141() V142() Element of (len i) -tuples_on REAL
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
i - j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len (i - j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom (i - j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
(len i) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
f is V16() V19( NAT ) V20( REAL ) Function-like V40( len i) FinSequence-like complex-yielding V141() V142() Element of (len i) -tuples_on REAL
c₄ is V16() V19( NAT ) V20( REAL ) Function-like V40( len i) FinSequence-like complex-yielding V141() V142() Element of (len i) -tuples_on REAL
f - c₄ is V16() V19( NAT ) V20( REAL ) Function-like V40( len i) FinSequence-like complex-yielding V141() V142() Element of (len i) -tuples_on REAL
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
sqr i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len (sqr i) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
sqr j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
dom (sqr j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
abs i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * i is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
len (abs i) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (abs i) is V166() V167() V168() V169() V170() V171() Element of bool NAT
rng i is V166() V167() V168() Element of bool REAL
dom absreal is V166() V167() V168() Element of bool REAL
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
i ^ j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr (i ^ j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(sqr i) ^ (sqr j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * i is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
i ^ j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs (i ^ j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * (i ^ j) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
abs j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * j is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
(abs i) ^ (abs j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (i ^ j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len i) + (len j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs (i ^ j)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs i) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
f is V10() V11() V12() ext-real V89() set
(abs (i ^ j)) . f is V11() V12() ext-real Element of REAL
((abs i) ^ (abs j)) . f is V11() V12() ext-real Element of REAL
dom (i ^ j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (abs i) is V166() V167() V168() V169() V170() V171() Element of bool NAT
(i ^ j) . f is V11() V12() ext-real Element of REAL
absreal . ((i ^ j) . f) is V11() V12() ext-real Element of REAL
i . f is V11() V12() ext-real Element of REAL
absreal . (i . f) is V11() V12() ext-real Element of REAL
c₄ is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i . c₄ is V11() V12() ext-real Element of REAL
abs (i . c₄) is V11() V12() ext-real Element of REAL
(abs i) . c₄ is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
c₄ is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
c₄ - (len i) is V11() V12() ext-real V89() Element of REAL
cij is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom (abs j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
len ((abs i) ^ (abs j)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(i ^ j) . f is V11() V12() ext-real Element of REAL
absreal . ((i ^ j) . f) is V11() V12() ext-real Element of REAL
j . cij is V11() V12() ext-real Element of REAL
absreal . (j . cij) is V11() V12() ext-real Element of REAL
abs (j . cij) is V11() V12() ext-real Element of REAL
(abs j) . cij is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
len ((abs i) ^ (abs j)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i + j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr (i + j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i ^ f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len c₄ is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j ^ c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(i ^ f) + (j ^ c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr ((i ^ f) + (j ^ c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
f + c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr (f + c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(sqr (i + j)) ^ (sqr (f + c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len (i ^ f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len i) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (j ^ c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len j) + (len c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (sqr ((i ^ f) + (j ^ c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((i ^ f) + (j ^ c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (i + j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i + j)) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (f + c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i + j)) + (len (f + c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (sqr (i + j)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (sqr (i + j))) + (len (f + c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (sqr (f + c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (sqr (i + j))) + (len (sqr (f + c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((sqr (i + j)) ^ (sqr (f + c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
cij is V10() V11() V12() ext-real V89() set
(sqr ((i ^ f) + (j ^ c₄))) . cij is V11() V12() ext-real Element of REAL
((sqr (i + j)) ^ (sqr (f + c₄))) . cij is V11() V12() ext-real Element of REAL
dom (sqr ((i ^ f) + (j ^ c₄))) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom ((i ^ f) + (j ^ c₄)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (i + j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (sqr (i + j)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
((i ^ f) + (j ^ c₄)) . cij is V11() V12() ext-real Element of REAL
(((i ^ f) + (j ^ c₄)) . cij) ^2 is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
(((i ^ f) . cij) + ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
i . cij is V11() V12() ext-real Element of REAL
(i . cij) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
((i . cij) + ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
j . cij is V11() V12() ext-real Element of REAL
(i . cij) + (j . cij) is V11() V12() ext-real Element of REAL
((i . cij) + (j . cij)) ^2 is V11() V12() ext-real Element of REAL
(i + j) . cij is V11() V12() ext-real Element of REAL
((i + j) . cij) ^2 is V11() V12() ext-real Element of REAL
(sqr (i + j)) . cij is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
cij - (len i) is V11() V12() ext-real V89() Element of REAL
cij - (len (i + j)) is V11() V12() ext-real V89() Element of REAL
dom (f + c₄) is V166() V167() V168() V169() V170() V171() Element of bool NAT
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
cij - (len (sqr (i + j))) is V11() V12() ext-real V89() Element of REAL
((i ^ f) + (j ^ c₄)) . cij is V11() V12() ext-real Element of REAL
(((i ^ f) + (j ^ c₄)) . cij) ^2 is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
(((i ^ f) . cij) + ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
f . f is V11() V12() ext-real Element of REAL
(f . f) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
((f . f) + ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
c₄ . f is V11() V12() ext-real Element of REAL
(f . f) + (c₄ . f) is V11() V12() ext-real Element of REAL
((f . f) + (c₄ . f)) ^2 is V11() V12() ext-real Element of REAL
(f + c₄) . f is V11() V12() ext-real Element of REAL
((f + c₄) . f) ^2 is V11() V12() ext-real Element of REAL
(sqr (f + c₄)) . f is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i + j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs (i + j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * (i + j) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i ^ f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len c₄ is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j ^ c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(i ^ f) + (j ^ c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs ((i ^ f) + (j ^ c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * ((i ^ f) + (j ^ c₄)) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
f + c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs (f + c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * (f + c₄) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
(abs (i + j)) ^ (abs (f + c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len (i ^ f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len i) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (j ^ c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len j) + (len c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs ((i ^ f) + (j ^ c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((i ^ f) + (j ^ c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (i + j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i + j)) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (f + c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i + j)) + (len (f + c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs (i + j)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (abs (i + j))) + (len (f + c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs (f + c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (abs (i + j))) + (len (abs (f + c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((abs (i + j)) ^ (abs (f + c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
cij is V10() V11() V12() ext-real V89() set
(abs ((i ^ f) + (j ^ c₄))) . cij is V11() V12() ext-real Element of REAL
((abs (i + j)) ^ (abs (f + c₄))) . cij is V11() V12() ext-real Element of REAL
dom (abs ((i ^ f) + (j ^ c₄))) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom ((i ^ f) + (j ^ c₄)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (i + j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (abs (i + j)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
((i ^ f) + (j ^ c₄)) . f is V11() V12() ext-real Element of REAL
abs (((i ^ f) + (j ^ c₄)) . f) is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs (((i ^ f) . cij) + ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
i . cij is V11() V12() ext-real Element of REAL
(i . cij) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs ((i . cij) + ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
j . cij is V11() V12() ext-real Element of REAL
(i . cij) + (j . cij) is V11() V12() ext-real Element of REAL
abs ((i . cij) + (j . cij)) is V11() V12() ext-real Element of REAL
(i + j) . f is V11() V12() ext-real Element of REAL
abs ((i + j) . f) is V11() V12() ext-real Element of REAL
(abs (i + j)) . f is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
cij - (len i) is V11() V12() ext-real V89() Element of REAL
cij - (len (i + j)) is V11() V12() ext-real V89() Element of REAL
dom (f + c₄) is V166() V167() V168() V169() V170() V171() Element of bool NAT
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom (abs (f + c₄)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
cij - (len (abs (i + j))) is V11() V12() ext-real V89() Element of REAL
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
((i ^ f) + (j ^ c₄)) . f is V11() V12() ext-real Element of REAL
abs (((i ^ f) + (j ^ c₄)) . f) is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs (((i ^ f) . cij) + ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
f . f is V11() V12() ext-real Element of REAL
(f . f) + ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs ((f . f) + ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
c₄ . f is V11() V12() ext-real Element of REAL
(f . f) + (c₄ . f) is V11() V12() ext-real Element of REAL
abs ((f . f) + (c₄ . f)) is V11() V12() ext-real Element of REAL
(f + c₄) . f is V11() V12() ext-real Element of REAL
abs ((f + c₄) . f) is V11() V12() ext-real Element of REAL
(abs (f + c₄)) . f is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i - j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr (i - j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i ^ f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len c₄ is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j ^ c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(i ^ f) - (j ^ c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr ((i ^ f) - (j ^ c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
f - c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr (f - c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(sqr (i - j)) ^ (sqr (f - c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len (i ^ f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len i) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (j ^ c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len j) + (len c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (sqr ((i ^ f) - (j ^ c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((i ^ f) - (j ^ c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (i - j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i - j)) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (f - c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i - j)) + (len (f - c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (sqr (i - j)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (sqr (i - j))) + (len (f - c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (sqr (f - c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (sqr (i - j))) + (len (sqr (f - c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((sqr (i - j)) ^ (sqr (f - c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
cij is V10() V11() V12() ext-real V89() set
(sqr ((i ^ f) - (j ^ c₄))) . cij is V11() V12() ext-real Element of REAL
((sqr (i - j)) ^ (sqr (f - c₄))) . cij is V11() V12() ext-real Element of REAL
dom (sqr ((i ^ f) - (j ^ c₄))) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom ((i ^ f) - (j ^ c₄)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (i - j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (sqr (i - j)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
((i ^ f) - (j ^ c₄)) . cij is V11() V12() ext-real Element of REAL
(((i ^ f) - (j ^ c₄)) . cij) ^2 is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
(((i ^ f) . cij) - ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
i . cij is V11() V12() ext-real Element of REAL
(i . cij) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
((i . cij) - ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
j . cij is V11() V12() ext-real Element of REAL
(i . cij) - (j . cij) is V11() V12() ext-real Element of REAL
((i . cij) - (j . cij)) ^2 is V11() V12() ext-real Element of REAL
(i - j) . cij is V11() V12() ext-real Element of REAL
((i - j) . cij) ^2 is V11() V12() ext-real Element of REAL
(sqr (i - j)) . cij is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
cij - (len i) is V11() V12() ext-real V89() Element of REAL
cij - (len (i - j)) is V11() V12() ext-real V89() Element of REAL
dom (f - c₄) is V166() V167() V168() V169() V170() V171() Element of bool NAT
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
cij - (len (sqr (i - j))) is V11() V12() ext-real V89() Element of REAL
((i ^ f) - (j ^ c₄)) . cij is V11() V12() ext-real Element of REAL
(((i ^ f) - (j ^ c₄)) . cij) ^2 is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
(((i ^ f) . cij) - ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
f . f is V11() V12() ext-real Element of REAL
(f . f) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
((f . f) - ((j ^ c₄) . cij)) ^2 is V11() V12() ext-real Element of REAL
c₄ . f is V11() V12() ext-real Element of REAL
(f . f) - (c₄ . f) is V11() V12() ext-real Element of REAL
((f . f) - (c₄ . f)) ^2 is V11() V12() ext-real Element of REAL
(f - c₄) . f is V11() V12() ext-real Element of REAL
((f - c₄) . f) ^2 is V11() V12() ext-real Element of REAL
(sqr (f - c₄)) . f is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i - j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs (i - j) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * (i - j) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i ^ f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len c₄ is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
j ^ c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(i ^ f) - (j ^ c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs ((i ^ f) - (j ^ c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * ((i ^ f) - (j ^ c₄)) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
f - c₄ is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs (f - c₄) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * (f - c₄) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
(abs (i - j)) ^ (abs (f - c₄)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len (i ^ f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len i) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (j ^ c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len j) + (len c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs ((i ^ f) - (j ^ c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((i ^ f) - (j ^ c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (i - j) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i - j)) + (len f) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (f - c₄) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (i - j)) + (len (f - c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs (i - j)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (abs (i - j))) + (len (f - c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len (abs (f - c₄)) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
(len (abs (i - j))) + (len (abs (f - c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len ((abs (i - j)) ^ (abs (f - c₄))) is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
cij is V10() V11() V12() ext-real V89() set
(abs ((i ^ f) - (j ^ c₄))) . cij is V11() V12() ext-real Element of REAL
((abs (i - j)) ^ (abs (f - c₄))) . cij is V11() V12() ext-real Element of REAL
dom (abs ((i ^ f) - (j ^ c₄))) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom ((i ^ f) - (j ^ c₄)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom j is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (i - j) is V166() V167() V168() V169() V170() V171() Element of bool NAT
dom (abs (i - j)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
((i ^ f) - (j ^ c₄)) . f is V11() V12() ext-real Element of REAL
abs (((i ^ f) - (j ^ c₄)) . f) is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs (((i ^ f) . cij) - ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
i . cij is V11() V12() ext-real Element of REAL
(i . cij) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs ((i . cij) - ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
j . cij is V11() V12() ext-real Element of REAL
(i . cij) - (j . cij) is V11() V12() ext-real Element of REAL
abs ((i . cij) - (j . cij)) is V11() V12() ext-real Element of REAL
(i - j) . f is V11() V12() ext-real Element of REAL
abs ((i - j) . f) is V11() V12() ext-real Element of REAL
(abs (i - j)) . f is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
cij - (len i) is V11() V12() ext-real V89() Element of REAL
cij - (len (i - j)) is V11() V12() ext-real V89() Element of REAL
dom (f - c₄) is V166() V167() V168() V169() V170() V171() Element of bool NAT
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
dom (abs (f - c₄)) is V166() V167() V168() V169() V170() V171() Element of bool NAT
cij - (len (abs (i - j))) is V11() V12() ext-real V89() Element of REAL
f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
((i ^ f) - (j ^ c₄)) . f is V11() V12() ext-real Element of REAL
abs (((i ^ f) - (j ^ c₄)) . f) is V11() V12() ext-real Element of REAL
(i ^ f) . cij is V11() V12() ext-real Element of REAL
(j ^ c₄) . cij is V11() V12() ext-real Element of REAL
((i ^ f) . cij) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs (((i ^ f) . cij) - ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
f . f is V11() V12() ext-real Element of REAL
(f . f) - ((j ^ c₄) . cij) is V11() V12() ext-real Element of REAL
abs ((f . f) - ((j ^ c₄) . cij)) is V11() V12() ext-real Element of REAL
c₄ . f is V11() V12() ext-real Element of REAL
(f . f) - (c₄ . f) is V11() V12() ext-real Element of REAL
abs ((f . f) - (c₄ . f)) is V11() V12() ext-real Element of REAL
(f - c₄) . f is V11() V12() ext-real Element of REAL
abs ((f - c₄) . f) is V11() V12() ext-real Element of REAL
(abs (f - c₄)) . f is V11() V12() ext-real Element of REAL
dom i is V166() V167() V168() V169() V170() V171() Element of bool NAT
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Euclid i is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL i is non empty functional FinSequence-membered FinSequenceSet of REAL
i -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist i is V16() V19([:(REAL i),(REAL i):]) V20( REAL ) Function-like V30([:(REAL i),(REAL i):], REAL ) complex-yielding V141() V142() Element of bool [:[:(REAL i),(REAL i):],REAL:]
[:(REAL i),(REAL i):] is non empty V16() set
[:[:(REAL i),(REAL i):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:(REAL i),(REAL i):],REAL:] is non empty set
MetrStruct(# (REAL i),(Pitag_dist i) #) is strict MetrStruct
the carrier of (Euclid i) is non empty set
j is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
TOP-REAL i is non empty TopSpace-like V105() V130() V131() V132() V133() V134() V135() V136() V181() L15()
the carrier of (TOP-REAL i) is non empty set
i is non empty MetrStruct
the carrier of i is non empty set
j is non empty MetrStruct
the carrier of j is non empty set
[: the carrier of i, the carrier of j:] is non empty V16() set
the distance of i is V16() V19([: the carrier of i, the carrier of i:]) V20( REAL ) Function-like V30([: the carrier of i, the carrier of i:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of i, the carrier of i:],REAL:]
[: the carrier of i, the carrier of i:] is non empty V16() set
[:[: the carrier of i, the carrier of i:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of i, the carrier of i:],REAL:] is non empty set
the distance of j is V16() V19([: the carrier of j, the carrier of j:]) V20( REAL ) Function-like V30([: the carrier of j, the carrier of j:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of j, the carrier of j:],REAL:]
[: the carrier of j, the carrier of j:] is non empty V16() set
[:[: the carrier of j, the carrier of j:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of j, the carrier of j:],REAL:] is non empty set
c₄ is Element of [: the carrier of i, the carrier of j:]
cij is Element of [: the carrier of i, the carrier of j:]
c₄ `1 is Element of the carrier of i
c<sub>4</sub> `2 is Element of the carrier of j
cij `1 is Element of the carrier of i
cij `2 is Element of the carrier of j
the distance of i . ((c₄ `1),(cij `1)) is V11() V12() ext-real Element of REAL
[(c₄ `1),(cij `1)] is V27() set
{(c₄ `1),(cij `1)} is set
{(c₄ `1)} is set
{{(c<sub>4</sub> `1),(cij `1)},{(c<sub>4</sub> `1)}} is set
the distance of i . [(c₄ `1),(cij `1)] is V11() V12() ext-real set
the distance of j . ((c₄ `2),(cij `2)) is V11() V12() ext-real Element of REAL
[(c₄ `2),(cij `2)] is V27() set
{(c₄ `2),(cij `2)} is set
{(c₄ `2)} is set
{{(c<sub>4</sub> `2),(cij `2)},{(c<sub>4</sub> `2)}} is set
the distance of j . [(c₄ `2),(cij `2)] is V11() V12() ext-real set
max (( the distance of i . ((c₄ `1),(cij `1))),( the distance of j . ((c₄ `2),(cij `2)))) is V11() V12() ext-real Element of REAL
[(c₄ `1),(c<sub>4</sub> `2)] is V27() Element of [: the carrier of i, the carrier of j:]
{(c₄ `1),(c<sub>4</sub> `2)} is set
{{(c₄ `1),(c<sub>4</sub> `2)},{(c₄ `1)}} is set
[(cij `1),(cij `2)] is V27() Element of [: the carrier of i, the carrier of j:]
{(cij `1),(cij `2)} is set
{(cij `1)} is set
{{(cij `1),(cij `2)},{(cij `1)}} is set
[:[: the carrier of i, the carrier of j:],[: the carrier of i, the carrier of j:]:] is non empty V16() set
[:[:[: the carrier of i, the carrier of j:],[: the carrier of i, the carrier of j:]:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:[: the carrier of i, the carrier of j:],[: the carrier of i, the carrier of j:]:],REAL:] is non empty set
c<sub>4</sub> is V16() V19([:[: the carrier of i, the carrier of j:],[: the carrier of i, the carrier of j:]:]) V20( REAL ) Function-like V30([:[: the carrier of i, the carrier of j:],[: the carrier of i, the carrier of j:]:], REAL ) complex-yielding V141() V142() Element of bool [:[:[: the carrier of i, the carrier of j:],[: the carrier of i, the carrier of j:]:],REAL:]
MetrStruct(# [: the carrier of i, the carrier of j:],c<sub>4</sub> #) is strict MetrStruct
cij is strict MetrStruct
the carrier of cij is set
the distance of cij is V16() V19([: the carrier of cij, the carrier of cij:]) V20( REAL ) Function-like V30([: the carrier of cij, the carrier of cij:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of cij, the carrier of cij:],REAL:]
[: the carrier of cij, the carrier of cij:] is V16() set
[:[: the carrier of cij, the carrier of cij:],REAL:] is V16() complex-yielding V141() V142() set
bool [:[: the carrier of cij, the carrier of cij:],REAL:] is non empty set
f is Element of the carrier of cij
f is Element of the carrier of cij
the distance of cij . (f,f) is V11() V12() ext-real Element of REAL
[f,f] is V27() set
{f,f} is set
{f} is set
{{f,f},{f}} is set
the distance of cij . [f,f] is V11() V12() ext-real set
c<sub>4</sub> . (f,f) is set
c<sub>4</sub> . [f,f] is V11() V12() ext-real set
f is Element of the carrier of i
fj is Element of the carrier of j
[f,fj] is V27() Element of [: the carrier of i, the carrier of j:]
{f,fj} is set
{f} is set
{{f,fj},{f}} is set
fi is Element of the carrier of i
Fi is Element of the carrier of j
[fi,Fi] is V27() Element of [: the carrier of i, the carrier of j:]
{fi,Fi} is set
{fi} is set
{{fi,Fi},{fi}} is set
the distance of i . (f,fi) is V11() V12() ext-real Element of REAL
[f,fi] is V27() set
{f,fi} is set
{{f,fi},{f}} is set
the distance of i . [f,fi] is V11() V12() ext-real set
the distance of j . (fj,Fi) is V11() V12() ext-real Element of REAL
[fj,Fi] is V27() set
{fj,Fi} is set
{fj} is set
{{fj,Fi},{fj}} is set
the distance of j . [fj,Fi] is V11() V12() ext-real set
max (( the distance of i . (f,fi)),( the distance of j . (fj,Fi))) is V11() V12() ext-real Element of REAL
f is strict MetrStruct
the carrier of f is set
the distance of f is V16() V19([: the carrier of f, the carrier of f:]) V20( REAL ) Function-like V30([: the carrier of f, the carrier of f:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of f, the carrier of f:],REAL:]
[: the carrier of f, the carrier of f:] is V16() set
[:[: the carrier of f, the carrier of f:],REAL:] is V16() complex-yielding V141() V142() set
bool [:[: the carrier of f, the carrier of f:],REAL:] is non empty set
c<sub>4</sub> is strict MetrStruct
the carrier of c<sub>4</sub> is set
the distance of c<sub>4</sub> is V16() V19([: the carrier of c<sub>4</sub>, the carrier of c<sub>4</sub>:]) V20( REAL ) Function-like V30([: the carrier of c<sub>4</sub>, the carrier of c<sub>4</sub>:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of c<sub>4</sub>, the carrier of c<sub>4</sub>:],REAL:]
[: the carrier of c<sub>4</sub>, the carrier of c<sub>4</sub>:] is V16() set
[:[: the carrier of c<sub>4</sub>, the carrier of c<sub>4</sub>:],REAL:] is V16() complex-yielding V141() V142() set
bool [:[: the carrier of c<sub>4</sub>, the carrier of c<sub>4</sub>:],REAL:] is non empty set
f is set
f is set
the distance of f . (f,f) is set
[f,f] is V27() set
{f,f} is set
{f} is set
{{f,f},{f}} is set
the distance of f . [f,f] is V11() V12() ext-real set
the distance of c<sub>4</sub> . (f,f) is set
the distance of c<sub>4</sub> . [f,f] is V11() V12() ext-real set
fi is Element of the carrier of i
Fi is Element of the carrier of j
[fi,Fi] is V27() Element of [: the carrier of i, the carrier of j:]
{fi,Fi} is set
{fi} is set
{{fi,Fi},{fi}} is set
fj is Element of the carrier of i
Fj is Element of the carrier of j
[fj,Fj] is V27() Element of [: the carrier of i, the carrier of j:]
{fj,Fj} is set
{fj} is set
{{fj,Fj},{fj}} is set
the distance of i . (fi,fj) is V11() V12() ext-real Element of REAL
[fi,fj] is V27() set
{fi,fj} is set
{{fi,fj},{fi}} is set
the distance of i . [fi,fj] is V11() V12() ext-real set
the distance of j . (Fi,Fj) is V11() V12() ext-real Element of REAL
[Fi,Fj] is V27() set
{Fi,Fj} is set
{Fi} is set
{{Fi,Fj},{Fi}} is set
the distance of j . [Fi,Fj] is V11() V12() ext-real set
max (( the distance of i . (fi,fj)),( the distance of j . (Fi,Fj))) is V11() V12() ext-real Element of REAL
r1 is Element of the carrier of i
bb is Element of the carrier of j
[r1,bb] is V27() Element of [: the carrier of i, the carrier of j:]
{r1,bb} is set
{r1} is set
{{r1,bb},{r1}} is set
b is Element of the carrier of i
fb is Element of the carrier of j
[b,fb] is V27() Element of [: the carrier of i, the carrier of j:]
{b,fb} is set
{b} is set
{{b,fb},{b}} is set
the distance of i . (r1,b) is V11() V12() ext-real Element of REAL
[r1,b] is V27() set
{r1,b} is set
{{r1,b},{r1}} is set
the distance of i . [r1,b] is V11() V12() ext-real set
the distance of j . (bb,fb) is V11() V12() ext-real Element of REAL
[bb,fb] is V27() set
{bb,fb} is set
{bb} is set
{{bb,fb},{bb}} is set
the distance of j . [bb,fb] is V11() V12() ext-real set
max (( the distance of i . (r1,b)),( the distance of j . (bb,fb))) is V11() V12() ext-real Element of REAL
i is non empty MetrStruct
j is non empty MetrStruct
(i,j) is strict MetrStruct
the carrier of (i,j) is set
the carrier of i is non empty set
the carrier of j is non empty set
[: the carrier of i, the carrier of j:] is non empty V16() set
i is non empty MetrStruct
the carrier of i is non empty set
j is non empty MetrStruct
the carrier of j is non empty set
f is Element of the carrier of i
c<sub>4</sub> is Element of the carrier of j
[f,c<sub>4</sub>] is V27() set
{f,c<sub>4</sub>} is set
{f} is set
{{f,c<sub>4</sub>},{f}} is set
(i,j) is non empty strict MetrStruct
the carrier of (i,j) is non empty set
[f,c<sub>4</sub>] is V27() Element of [: the carrier of i, the carrier of j:]
[: the carrier of i, the carrier of j:] is non empty V16() set
i is non empty MetrStruct
j is non empty MetrStruct
(i,j) is non empty strict MetrStruct
the carrier of (i,j) is non empty set
f is Element of the carrier of (i,j)
f `1 is set
the carrier of i is non empty set
the carrier of j is non empty set
[: the carrier of i, the carrier of j:] is non empty V16() set
f `2 is set
the carrier of j is non empty set
[: the carrier of i, the carrier of j:] is non empty V16() set
i is non empty MetrStruct
the carrier of i is non empty set
j is non empty MetrStruct
the carrier of j is non empty set
(i,j) is non empty strict MetrStruct
f is Element of the carrier of i
c₄ is Element of the carrier of i
dist (f,c₄) is V11() V12() ext-real Element of REAL
the distance of i is V16() V19([: the carrier of i, the carrier of i:]) V20( REAL ) Function-like V30([: the carrier of i, the carrier of i:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of i, the carrier of i:],REAL:]
[: the carrier of i, the carrier of i:] is non empty V16() set
[:[: the carrier of i, the carrier of i:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of i, the carrier of i:],REAL:] is non empty set
the distance of i . (f,c₄) is V11() V12() ext-real Element of REAL
[f,c₄] is V27() set
{f,c₄} is set
{f} is set
{{f,c₄},{f}} is set
the distance of i . [f,c₄] is V11() V12() ext-real set
cij is Element of the carrier of j
(i,j,f,cij) is V27() Element of the carrier of (i,j)
the carrier of (i,j) is non empty set
{f,cij} is set
{{f,cij},{f}} is set
f is Element of the carrier of j
(i,j,c₄,f) is V27() Element of the carrier of (i,j)
{c₄,f} is set
{c₄} is set
{{c₄,f},{c₄}} is set
dist ((i,j,f,cij),(i,j,c₄,f)) is V11() V12() ext-real Element of REAL
the distance of (i,j) is V16() V19([: the carrier of (i,j), the carrier of (i,j):]) V20( REAL ) Function-like V30([: the carrier of (i,j), the carrier of (i,j):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:]
[: the carrier of (i,j), the carrier of (i,j):] is non empty V16() set
[:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty set
the distance of (i,j) . ((i,j,f,cij),(i,j,c₄,f)) is V11() V12() ext-real Element of REAL
[(i,j,f,cij),(i,j,c₄,f)] is V27() set
{(i,j,f,cij),(i,j,c₄,f)} is V16() set
{(i,j,f,cij)} is V16() set
{{(i,j,f,cij),(i,j,c₄,f)},{(i,j,f,cij)}} is set
the distance of (i,j) . [(i,j,f,cij),(i,j,c₄,f)] is V11() V12() ext-real set
dist (cij,f) is V11() V12() ext-real Element of REAL
the distance of j is V16() V19([: the carrier of j, the carrier of j:]) V20( REAL ) Function-like V30([: the carrier of j, the carrier of j:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of j, the carrier of j:],REAL:]
[: the carrier of j, the carrier of j:] is non empty V16() set
[:[: the carrier of j, the carrier of j:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of j, the carrier of j:],REAL:] is non empty set
the distance of j . (cij,f) is V11() V12() ext-real Element of REAL
[cij,f] is V27() set
{cij,f} is set
{cij} is set
{{cij,f},{cij}} is set
the distance of j . [cij,f] is V11() V12() ext-real set
max ((dist (f,c₄)),(dist (cij,f))) is V11() V12() ext-real Element of REAL
f is Element of the carrier of i
fi is Element of the carrier of j
(i,j,f,fi) is V27() Element of the carrier of (i,j)
{f,fi} is set
{f} is set
{{f,fi},{f}} is set
f is Element of the carrier of i
fj is Element of the carrier of j
(i,j,f,fj) is V27() Element of the carrier of (i,j)
{f,fj} is set
{f} is set
{{f,fj},{f}} is set
the distance of i . (f,f) is V11() V12() ext-real Element of REAL
[f,f] is V27() set
{f,f} is set
{{f,f},{f}} is set
the distance of i . [f,f] is V11() V12() ext-real set
the distance of j . (fi,fj) is V11() V12() ext-real Element of REAL
[fi,fj] is V27() set
{fi,fj} is set
{fi} is set
{{fi,fj},{fi}} is set
the distance of j . [fi,fj] is V11() V12() ext-real set
max (( the distance of i . (f,f)),( the distance of j . (fi,fj))) is V11() V12() ext-real Element of REAL
i is non empty MetrStruct
j is non empty MetrStruct
(i,j) is non empty strict MetrStruct
the carrier of (i,j) is non empty set
f is Element of the carrier of (i,j)
c₄ is Element of the carrier of (i,j)
dist (f,c₄) is V11() V12() ext-real Element of REAL
the distance of (i,j) is V16() V19([: the carrier of (i,j), the carrier of (i,j):]) V20( REAL ) Function-like V30([: the carrier of (i,j), the carrier of (i,j):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:]
[: the carrier of (i,j), the carrier of (i,j):] is non empty V16() set
[:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty set
the distance of (i,j) . (f,c₄) is V11() V12() ext-real Element of REAL
[f,c₄] is V27() set
{f,c₄} is set
{f} is set
{{f,c₄},{f}} is set
the distance of (i,j) . [f,c₄] is V11() V12() ext-real set
(i,j,f) is Element of the carrier of i
the carrier of i is non empty set
(i,j,c₄) is Element of the carrier of i
dist ((i,j,f),(i,j,c₄)) is V11() V12() ext-real Element of REAL
the distance of i is V16() V19([: the carrier of i, the carrier of i:]) V20( REAL ) Function-like V30([: the carrier of i, the carrier of i:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of i, the carrier of i:],REAL:]
[: the carrier of i, the carrier of i:] is non empty V16() set
[:[: the carrier of i, the carrier of i:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of i, the carrier of i:],REAL:] is non empty set
the distance of i . ((i,j,f),(i,j,c₄)) is V11() V12() ext-real Element of REAL
[(i,j,f),(i,j,c₄)] is V27() set
{(i,j,f),(i,j,c₄)} is set
{(i,j,f)} is set
{{(i,j,f),(i,j,c₄)},{(i,j,f)}} is set
the distance of i . [(i,j,f),(i,j,c₄)] is V11() V12() ext-real set
(i,j,f) is Element of the carrier of j
the carrier of j is non empty set
(i,j,c₄) is Element of the carrier of j
dist ((i,j,f),(i,j,c₄)) is V11() V12() ext-real Element of REAL
the distance of j is V16() V19([: the carrier of j, the carrier of j:]) V20( REAL ) Function-like V30([: the carrier of j, the carrier of j:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of j, the carrier of j:],REAL:]
[: the carrier of j, the carrier of j:] is non empty V16() set
[:[: the carrier of j, the carrier of j:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of j, the carrier of j:],REAL:] is non empty set
the distance of j . ((i,j,f),(i,j,c₄)) is V11() V12() ext-real Element of REAL
[(i,j,f),(i,j,c₄)] is V27() set
{(i,j,f),(i,j,c₄)} is set
{(i,j,f)} is set
{{(i,j,f),(i,j,c₄)},{(i,j,f)}} is set
the distance of j . [(i,j,f),(i,j,c₄)] is V11() V12() ext-real set
max ((dist ((i,j,f),(i,j,c₄))),(dist ((i,j,f),(i,j,c₄)))) is V11() V12() ext-real Element of REAL
cij is Element of the carrier of i
f is Element of the carrier of j
(i,j,cij,f) is V27() Element of the carrier of (i,j)
{cij,f} is set
{cij} is set
{{cij,f},{cij}} is set
f is Element of the carrier of i
f is Element of the carrier of j
(i,j,f,f) is V27() Element of the carrier of (i,j)
{f,f} is set
{f} is set
{{f,f},{f}} is set
the distance of i . (cij,f) is V11() V12() ext-real Element of REAL
[cij,f] is V27() set
{cij,f} is set
{{cij,f},{cij}} is set
the distance of i . [cij,f] is V11() V12() ext-real set
the distance of j . (f,f) is V11() V12() ext-real Element of REAL
[f,f] is V27() set
{f,f} is set
{f} is set
{{f,f},{f}} is set
the distance of j . [f,f] is V11() V12() ext-real set
max (( the distance of i . (cij,f)),( the distance of j . (f,f))) is V11() V12() ext-real Element of REAL
i is non empty Reflexive MetrStruct
j is non empty Reflexive MetrStruct
(i,j) is non empty strict MetrStruct
the carrier of (i,j) is non empty set
the distance of (i,j) is V16() V19([: the carrier of (i,j), the carrier of (i,j):]) V20( REAL ) Function-like V30([: the carrier of (i,j), the carrier of (i,j):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:]
[: the carrier of (i,j), the carrier of (i,j):] is non empty V16() set
[:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty set
f is Element of the carrier of (i,j)
the distance of (i,j) . (f,f) is V11() V12() ext-real Element of REAL
[f,f] is V27() set
{f,f} is set
{f} is set
{{f,f},{f}} is set
the distance of (i,j) . [f,f] is V11() V12() ext-real set
the carrier of i is non empty set
the carrier of j is non empty set
the distance of i is V16() V19([: the carrier of i, the carrier of i:]) V20( REAL ) Function-like V30([: the carrier of i, the carrier of i:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of i, the carrier of i:],REAL:]
[: the carrier of i, the carrier of i:] is non empty V16() set
[:[: the carrier of i, the carrier of i:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of i, the carrier of i:],REAL:] is non empty set
the distance of j is V16() V19([: the carrier of j, the carrier of j:]) V20( REAL ) Function-like V30([: the carrier of j, the carrier of j:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of j, the carrier of j:],REAL:]
[: the carrier of j, the carrier of j:] is non empty V16() set
[:[: the carrier of j, the carrier of j:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of j, the carrier of j:],REAL:] is non empty set
c₄ is Element of the carrier of i
f is Element of the carrier of j
(i,j,c₄,f) is V27() Element of the carrier of (i,j)
{c₄,f} is set
{c₄} is set
{{c₄,f},{c₄}} is set
cij is Element of the carrier of i
f is Element of the carrier of j
(i,j,cij,f) is V27() Element of the carrier of (i,j)
{cij,f} is set
{cij} is set
{{cij,f},{cij}} is set
the distance of i . (c₄,cij) is V11() V12() ext-real Element of REAL
[c₄,cij] is V27() set
{c₄,cij} is set
{{c₄,cij},{c₄}} is set
the distance of i . [c₄,cij] is V11() V12() ext-real set
the distance of j . (f,f) is V11() V12() ext-real Element of REAL
[f,f] is V27() set
{f,f} is set
{f} is set
{{f,f},{f}} is set
the distance of j . [f,f] is V11() V12() ext-real set
max (( the distance of i . (c₄,cij)),( the distance of j . (f,f))) is V11() V12() ext-real Element of REAL
the distance of i . (c₄,c₄) is V11() V12() ext-real Element of REAL
[c₄,c₄] is V27() set
{c₄,c₄} is set
{{c₄,c₄},{c₄}} is set
the distance of i . [c₄,c₄] is V11() V12() ext-real set
the distance of j . (f,f) is V11() V12() ext-real Element of REAL
[f,f] is V27() set
{f,f} is set
{{f,f},{f}} is set
the distance of j . [f,f] is V11() V12() ext-real set
i is non empty Reflexive MetrStruct
j is non empty Reflexive MetrStruct
(i,j) is non empty strict MetrStruct
i is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
j is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(i,j) is non empty strict Reflexive MetrStruct
the carrier of (i,j) is non empty set
the distance of (i,j) is V16() V19([: the carrier of (i,j), the carrier of (i,j):]) V20( REAL ) Function-like V30([: the carrier of (i,j), the carrier of (i,j):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:]
[: the carrier of (i,j), the carrier of (i,j):] is non empty V16() set
[:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty set
f is Element of the carrier of (i,j)
c₄ is Element of the carrier of (i,j)
the distance of (i,j) . (f,c₄) is V11() V12() ext-real Element of REAL
[f,c₄] is V27() set
{f,c₄} is set
{f} is set
{{f,c₄},{f}} is set
the distance of (i,j) . [f,c₄] is V11() V12() ext-real set
the carrier of i is non empty set
the distance of i is V16() V19([: the carrier of i, the carrier of i:]) V20( REAL ) Function-like V30([: the carrier of i, the carrier of i:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of i, the carrier of i:],REAL:]
[: the carrier of i, the carrier of i:] is non empty V16() set
[:[: the carrier of i, the carrier of i:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of i, the carrier of i:],REAL:] is non empty set
the carrier of j is non empty set
the distance of j is V16() V19([: the carrier of j, the carrier of j:]) V20( REAL ) Function-like V30([: the carrier of j, the carrier of j:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of j, the carrier of j:],REAL:]
[: the carrier of j, the carrier of j:] is non empty V16() set
[:[: the carrier of j, the carrier of j:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of j, the carrier of j:],REAL:] is non empty set
cij is Element of the carrier of i
f is Element of the carrier of j
(i,j,cij,f) is V27() Element of the carrier of (i,j)
{cij,f} is set
{cij} is set
{{cij,f},{cij}} is set
f is Element of the carrier of i
f is Element of the carrier of j
(i,j,f,f) is V27() Element of the carrier of (i,j)
{f,f} is set
{f} is set
{{f,f},{f}} is set
the distance of i . (cij,f) is V11() V12() ext-real Element of REAL
[cij,f] is V27() set
{cij,f} is set
{{cij,f},{cij}} is set
the distance of i . [cij,f] is V11() V12() ext-real set
the distance of j . (f,f) is V11() V12() ext-real Element of REAL
[f,f] is V27() set
{f,f} is set
{f} is set
{{f,f},{f}} is set
the distance of j . [f,f] is V11() V12() ext-real set
max (( the distance of i . (cij,f)),( the distance of j . (f,f))) is V11() V12() ext-real Element of REAL
dist (cij,f) is V11() V12() ext-real Element of REAL
dist (f,f) is V11() V12() ext-real Element of REAL
i is non empty symmetric MetrStruct
j is non empty symmetric MetrStruct
(i,j) is non empty strict MetrStruct
the carrier of (i,j) is non empty set
the distance of (i,j) is V16() V19([: the carrier of (i,j), the carrier of (i,j):]) V20( REAL ) Function-like V30([: the carrier of (i,j), the carrier of (i,j):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:]
[: the carrier of (i,j), the carrier of (i,j):] is non empty V16() set
[:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty set
f is Element of the carrier of (i,j)
c₄ is Element of the carrier of (i,j)
the distance of (i,j) . (f,c₄) is V11() V12() ext-real Element of REAL
[f,c₄] is V27() set
{f,c₄} is set
{f} is set
{{f,c₄},{f}} is set
the distance of (i,j) . [f,c₄] is V11() V12() ext-real set
the distance of (i,j) . (c₄,f) is V11() V12() ext-real Element of REAL
[c₄,f] is V27() set
{c₄,f} is set
{c₄} is set
{{c₄,f},{c₄}} is set
the distance of (i,j) . [c₄,f] is V11() V12() ext-real set
the carrier of i is non empty set
the carrier of j is non empty set
the distance of i is V16() V19([: the carrier of i, the carrier of i:]) V20( REAL ) Function-like V30([: the carrier of i, the carrier of i:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of i, the carrier of i:],REAL:]
[: the carrier of i, the carrier of i:] is non empty V16() set
[:[: the carrier of i, the carrier of i:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of i, the carrier of i:],REAL:] is non empty set
the distance of j is V16() V19([: the carrier of j, the carrier of j:]) V20( REAL ) Function-like V30([: the carrier of j, the carrier of j:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of j, the carrier of j:],REAL:]
[: the carrier of j, the carrier of j:] is non empty V16() set
[:[: the carrier of j, the carrier of j:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of j, the carrier of j:],REAL:] is non empty set
cij is Element of the carrier of i
f is Element of the carrier of j
(i,j,cij,f) is V27() Element of the carrier of (i,j)
{cij,f} is set
{cij} is set
{{cij,f},{cij}} is set
f is Element of the carrier of i
f is Element of the carrier of j
(i,j,f,f) is V27() Element of the carrier of (i,j)
{f,f} is set
{f} is set
{{f,f},{f}} is set
the distance of i . (cij,f) is V11() V12() ext-real Element of REAL
[cij,f] is V27() set
{cij,f} is set
{{cij,f},{cij}} is set
the distance of i . [cij,f] is V11() V12() ext-real set
the distance of j . (f,f) is V11() V12() ext-real Element of REAL
[f,f] is V27() set
{f,f} is set
{f} is set
{{f,f},{f}} is set
the distance of j . [f,f] is V11() V12() ext-real set
max (( the distance of i . (cij,f)),( the distance of j . (f,f))) is V11() V12() ext-real Element of REAL
fi is Element of the carrier of i
Fi is Element of the carrier of j
(i,j,fi,Fi) is V27() Element of the carrier of (i,j)
{fi,Fi} is set
{fi} is set
{{fi,Fi},{fi}} is set
fj is Element of the carrier of i
Fj is Element of the carrier of j
(i,j,fj,Fj) is V27() Element of the carrier of (i,j)
{fj,Fj} is set
{fj} is set
{{fj,Fj},{fj}} is set
the distance of i . (fi,fj) is V11() V12() ext-real Element of REAL
[fi,fj] is V27() set
{fi,fj} is set
{{fi,fj},{fi}} is set
the distance of i . [fi,fj] is V11() V12() ext-real set
the distance of j . (Fi,Fj) is V11() V12() ext-real Element of REAL
[Fi,Fj] is V27() set
{Fi,Fj} is set
{Fi} is set
{{Fi,Fj},{Fi}} is set
the distance of j . [Fi,Fj] is V11() V12() ext-real set
max (( the distance of i . (fi,fj)),( the distance of j . (Fi,Fj))) is V11() V12() ext-real Element of REAL
the distance of j . (f,f) is V11() V12() ext-real Element of REAL
[f,f] is V27() set
{f,f} is set
{f} is set
{{f,f},{f}} is set
the distance of j . [f,f] is V11() V12() ext-real set
the distance of i . (f,cij) is V11() V12() ext-real Element of REAL
[f,cij] is V27() set
{f,cij} is set
{{f,cij},{f}} is set
the distance of i . [f,cij] is V11() V12() ext-real set
i is non empty symmetric MetrStruct
j is non empty symmetric MetrStruct
(i,j) is non empty strict MetrStruct
i is non empty triangle MetrStruct
j is non empty triangle MetrStruct
(i,j) is non empty strict MetrStruct
the carrier of (i,j) is non empty set
the distance of (i,j) is V16() V19([: the carrier of (i,j), the carrier of (i,j):]) V20( REAL ) Function-like V30([: the carrier of (i,j), the carrier of (i,j):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:]
[: the carrier of (i,j), the carrier of (i,j):] is non empty V16() set
[:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty set
f is Element of the carrier of (i,j)
cij is Element of the carrier of (i,j)
the distance of (i,j) . (f,cij) is V11() V12() ext-real Element of REAL
[f,cij] is V27() set
{f,cij} is set
{f} is set
{{f,cij},{f}} is set
the distance of (i,j) . [f,cij] is V11() V12() ext-real set
c₄ is Element of the carrier of (i,j)
the distance of (i,j) . (f,c₄) is V11() V12() ext-real Element of REAL
[f,c₄] is V27() set
{f,c₄} is set
{{f,c₄},{f}} is set
the distance of (i,j) . [f,c₄] is V11() V12() ext-real set
the distance of (i,j) . (c₄,cij) is V11() V12() ext-real Element of REAL
[c₄,cij] is V27() set
{c₄,cij} is set
{c₄} is set
{{c₄,cij},{c₄}} is set
the distance of (i,j) . [c₄,cij] is V11() V12() ext-real set
( the distance of (i,j) . (f,c₄)) + ( the distance of (i,j) . (c₄,cij)) is V11() V12() ext-real Element of REAL
the carrier of i is non empty set
the carrier of j is non empty set
the distance of i is V16() V19([: the carrier of i, the carrier of i:]) V20( REAL ) Function-like V30([: the carrier of i, the carrier of i:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of i, the carrier of i:],REAL:]
[: the carrier of i, the carrier of i:] is non empty V16() set
[:[: the carrier of i, the carrier of i:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of i, the carrier of i:],REAL:] is non empty set
the distance of j is V16() V19([: the carrier of j, the carrier of j:]) V20( REAL ) Function-like V30([: the carrier of j, the carrier of j:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of j, the carrier of j:],REAL:]
[: the carrier of j, the carrier of j:] is non empty V16() set
[:[: the carrier of j, the carrier of j:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of j, the carrier of j:],REAL:] is non empty set
f is Element of the carrier of i
f is Element of the carrier of j
(i,j,f,f) is V27() Element of the carrier of (i,j)
{f,f} is set
{f} is set
{{f,f},{f}} is set
f is Element of the carrier of i
fi is Element of the carrier of j
(i,j,f,fi) is V27() Element of the carrier of (i,j)
{f,fi} is set
{f} is set
{{f,fi},{f}} is set
the distance of i . (f,f) is V11() V12() ext-real Element of REAL
[f,f] is V27() set
{f,f} is set
{{f,f},{f}} is set
the distance of i . [f,f] is V11() V12() ext-real set
the distance of j . (f,fi) is V11() V12() ext-real Element of REAL
[f,fi] is V27() set
{f,fi} is set
{f} is set
{{f,fi},{f}} is set
the distance of j . [f,fi] is V11() V12() ext-real set
max (( the distance of i . (f,f)),( the distance of j . (f,fi))) is V11() V12() ext-real Element of REAL
fj is Element of the carrier of i
Fj is Element of the carrier of j
(i,j,fj,Fj) is V27() Element of the carrier of (i,j)
{fj,Fj} is set
{fj} is set
{{fj,Fj},{fj}} is set
Fi is Element of the carrier of i
r1 is Element of the carrier of j
(i,j,Fi,r1) is V27() Element of the carrier of (i,j)
{Fi,r1} is set
{Fi} is set
{{Fi,r1},{Fi}} is set
the distance of i . (fj,Fi) is V11() V12() ext-real Element of REAL
[fj,Fi] is V27() set
{fj,Fi} is set
{{fj,Fi},{fj}} is set
the distance of i . [fj,Fi] is V11() V12() ext-real set
the distance of j . (Fj,r1) is V11() V12() ext-real Element of REAL
[Fj,r1] is V27() set
{Fj,r1} is set
{Fj} is set
{{Fj,r1},{Fj}} is set
the distance of j . [Fj,r1] is V11() V12() ext-real set
max (( the distance of i . (fj,Fi)),( the distance of j . (Fj,r1))) is V11() V12() ext-real Element of REAL
b is Element of the carrier of i
fb is Element of the carrier of j
(i,j,b,fb) is V27() Element of the carrier of (i,j)
{b,fb} is set
{b} is set
{{b,fb},{b}} is set
bb is Element of the carrier of i
fbb is Element of the carrier of j
(i,j,bb,fbb) is V27() Element of the carrier of (i,j)
{bb,fbb} is set
{bb} is set
{{bb,fbb},{bb}} is set
the distance of i . (b,bb) is V11() V12() ext-real Element of REAL
[b,bb] is V27() set
{b,bb} is set
{{b,bb},{b}} is set
the distance of i . [b,bb] is V11() V12() ext-real set
the distance of j . (fb,fbb) is V11() V12() ext-real Element of REAL
[fb,fbb] is V27() set
{fb,fbb} is set
{fb} is set
{{fb,fbb},{fb}} is set
the distance of j . [fb,fbb] is V11() V12() ext-real set
max (( the distance of i . (b,bb)),( the distance of j . (fb,fbb))) is V11() V12() ext-real Element of REAL
the distance of j . (fb,fi) is V11() V12() ext-real Element of REAL
[fb,fi] is V27() set
{fb,fi} is set
{{fb,fi},{fb}} is set
the distance of j . [fb,fi] is V11() V12() ext-real set
the distance of j . (fi,fbb) is V11() V12() ext-real Element of REAL
[fi,fbb] is V27() set
{fi,fbb} is set
{fi} is set
{{fi,fbb},{fi}} is set
the distance of j . [fi,fbb] is V11() V12() ext-real set
( the distance of j . (fb,fi)) + ( the distance of j . (fi,fbb)) is V11() V12() ext-real Element of REAL
the distance of i . (b,f) is V11() V12() ext-real Element of REAL
[b,f] is V27() set
{b,f} is set
{{b,f},{b}} is set
the distance of i . [b,f] is V11() V12() ext-real set
the distance of i . (f,bb) is V11() V12() ext-real Element of REAL
[f,bb] is V27() set
{f,bb} is set
{{f,bb},{f}} is set
the distance of i . [f,bb] is V11() V12() ext-real set
( the distance of i . (b,f)) + ( the distance of i . (f,bb)) is V11() V12() ext-real Element of REAL
i is non empty triangle MetrStruct
j is non empty triangle MetrStruct
(i,j) is non empty strict MetrStruct
i is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
j is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
(i,j) is non empty strict Reflexive symmetric triangle MetrStruct
i is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
TopSpaceMetr i is non empty strict TopSpace-like TopStruct
j is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
TopSpaceMetr j is non empty strict TopSpace-like TopStruct
[:(TopSpaceMetr i),(TopSpaceMetr j):] is strict TopSpace-like TopStruct
(i,j) is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
TopSpaceMetr (i,j) is non empty strict TopSpace-like TopStruct
the carrier of (i,j) is non empty set
Family_open_set (i,j) is Element of bool (bool the carrier of (i,j))
bool the carrier of (i,j) is non empty set
bool (bool the carrier of (i,j)) is non empty set
TopStruct(# the carrier of (i,j),(Family_open_set (i,j)) #) is strict TopStruct
the carrier of i is non empty set
Family_open_set i is Element of bool (bool the carrier of i)
bool the carrier of i is non empty set
bool (bool the carrier of i) is non empty set
TopStruct(# the carrier of i,(Family_open_set i) #) is strict TopStruct
the carrier of j is non empty set
Family_open_set j is Element of bool (bool the carrier of j)
bool the carrier of j is non empty set
bool (bool the carrier of j) is non empty set
TopStruct(# the carrier of j,(Family_open_set j) #) is strict TopStruct
the carrier of [:(TopSpaceMetr i),(TopSpaceMetr j):] is set
the carrier of (TopSpaceMetr i) is non empty set
the carrier of (TopSpaceMetr j) is non empty set
[: the carrier of (TopSpaceMetr i), the carrier of (TopSpaceMetr j):] is non empty V16() set
the carrier of (TopSpaceMetr (i,j)) is non empty set
the topology of [:(TopSpaceMetr i),(TopSpaceMetr j):] is Element of bool (bool the carrier of [:(TopSpaceMetr i),(TopSpaceMetr j):])
bool the carrier of [:(TopSpaceMetr i),(TopSpaceMetr j):] is non empty set
bool (bool the carrier of [:(TopSpaceMetr i),(TopSpaceMetr j):]) is non empty set
bool the carrier of (TopSpaceMetr i) is non empty set
bool the carrier of (TopSpaceMetr j) is non empty set
the topology of (TopSpaceMetr i) is Element of bool (bool the carrier of (TopSpaceMetr i))
bool (bool the carrier of (TopSpaceMetr i)) is non empty set
the topology of (TopSpaceMetr j) is Element of bool (bool the carrier of (TopSpaceMetr j))
bool (bool the carrier of (TopSpaceMetr j)) is non empty set
{ [:b₁,b₂:] where b₁ is Element of bool the carrier of (TopSpaceMetr i), b₂ is Element of bool the carrier of (TopSpaceMetr j) : ( b₁ in the topology of (TopSpaceMetr i) & b₂ in the topology of (TopSpaceMetr j) ) } is set
{ (union b₁) where b₁ is Element of bool (bool the carrier of [:(TopSpaceMetr i),(TopSpaceMetr j):]) : b₁ c= { [:b₁,b₂:] where b₂ is Element of bool the carrier of (TopSpaceMetr i), b₃ is Element of bool the carrier of (TopSpaceMetr j) : ( b₁ in the topology of (TopSpaceMetr i) & b₂ in the topology of (TopSpaceMetr j) ) } } is set
the topology of (TopSpaceMetr (i,j)) is Element of bool (bool the carrier of (TopSpaceMetr (i,j)))
bool the carrier of (TopSpaceMetr (i,j)) is non empty set
bool (bool the carrier of (TopSpaceMetr (i,j))) is non empty set
cij is set
f is Element of bool (bool the carrier of [:(TopSpaceMetr i),(TopSpaceMetr j):])
union f is set
f is Element of the carrier of (i,j)
f is set
fi is Element of bool the carrier of (TopSpaceMetr i)
fj is Element of bool the carrier of (TopSpaceMetr j)
[:fi,fj:] is V16() Element of bool the carrier of [:(TopSpaceMetr i),(TopSpaceMetr j):]
Fi is set
Fj is set
[Fi,Fj] is V27() set
{Fi,Fj} is set
{Fi} is set
{{Fi,Fj},{Fi}} is set
r1 is Element of the carrier of j
b is V11() V12() ext-real Element of REAL
Ball (r1,b) is Element of bool the carrier of j
bb is Element of the carrier of i
fb is V11() V12() ext-real Element of REAL
Ball (bb,fb) is Element of bool the carrier of i
min (fb,b) is V11() V12() ext-real Element of REAL
fbb is V11() V12() ext-real Element of REAL
Ball (f,fbb) is Element of bool the carrier of (i,j)
fxx is set
b1 is Element of the carrier of (i,j)
dist (b1,f) is V11() V12() ext-real Element of REAL
the distance of (i,j) is V16() V19([: the carrier of (i,j), the carrier of (i,j):]) V20( REAL ) Function-like V30([: the carrier of (i,j), the carrier of (i,j):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:]
[: the carrier of (i,j), the carrier of (i,j):] is non empty V16() set
[:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty set
the distance of (i,j) . (b1,f) is V11() V12() ext-real Element of REAL
[b1,f] is V27() set
{b1,f} is set
{b1} is set
{{b1,f},{b1}} is set
the distance of (i,j) . [b1,f] is V11() V12() ext-real set
the distance of i is V16() V19([: the carrier of i, the carrier of i:]) V20( REAL ) Function-like V30([: the carrier of i, the carrier of i:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of i, the carrier of i:],REAL:]
[: the carrier of i, the carrier of i:] is non empty V16() set
[:[: the carrier of i, the carrier of i:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of i, the carrier of i:],REAL:] is non empty set
the distance of j is V16() V19([: the carrier of j, the carrier of j:]) V20( REAL ) Function-like V30([: the carrier of j, the carrier of j:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of j, the carrier of j:],REAL:]
[: the carrier of j, the carrier of j:] is non empty V16() set
[:[: the carrier of j, the carrier of j:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of j, the carrier of j:],REAL:] is non empty set
x1 is Element of the carrier of i
x2 is Element of the carrier of j
(i,j,x1,x2) is V27() Element of the carrier of (i,j)
{x1,x2} is set
{x1} is set
{{x1,x2},{x1}} is set
b2 is Element of the carrier of i
x2i is Element of the carrier of j
(i,j,b2,x2i) is V27() Element of the carrier of (i,j)
{b2,x2i} is set
{b2} is set
{{b2,x2i},{b2}} is set
the distance of i . (x1,b2) is V11() V12() ext-real Element of REAL
[x1,b2] is V27() set
{x1,b2} is set
{{x1,b2},{x1}} is set
the distance of i . [x1,b2] is V11() V12() ext-real set
the distance of j . (x2,x2i) is V11() V12() ext-real Element of REAL
[x2,x2i] is V27() set
{x2,x2i} is set
{x2} is set
{{x2,x2i},{x2}} is set
the distance of j . [x2,x2i] is V11() V12() ext-real set
max (( the distance of i . (x1,b2)),( the distance of j . (x2,x2i))) is V11() V12() ext-real Element of REAL
the distance of j . (x2,r1) is V11() V12() ext-real Element of REAL
[x2,r1] is V27() set
{x2,r1} is set
{{x2,r1},{x2}} is set
the distance of j . [x2,r1] is V11() V12() ext-real set
dist (x2,r1) is V11() V12() ext-real Element of REAL
the distance of i . (x1,bb) is V11() V12() ext-real Element of REAL
[x1,bb] is V27() set
{x1,bb} is set
{{x1,bb},{x1}} is set
the distance of i . [x1,bb] is V11() V12() ext-real set
dist (x1,bb) is V11() V12() ext-real Element of REAL
cij is set
f is Element of bool the carrier of [:(TopSpaceMetr i),(TopSpaceMetr j):]
Base-Appr f is Element of bool (bool the carrier of [:(TopSpaceMetr i),(TopSpaceMetr j):])
{ [:b₁,b₂:] where b₁ is Element of bool the carrier of (TopSpaceMetr i), b₂ is Element of bool the carrier of (TopSpaceMetr j) : ( [:b₁,b₂:] c= f & b₁ is open & b₂ is open ) } is set
union (Base-Appr f) is set
f is set
f is Element of the carrier of (i,j)
fi is V11() V12() ext-real Element of REAL
Ball (f,fi) is Element of bool the carrier of (i,j)
[: the carrier of i, the carrier of j:] is non empty V16() set
fj is set
Fi is set
[fj,Fi] is V27() set
{fj,Fi} is set
{fj} is set
{{fj,Fi},{fj}} is set
Fj is Element of the carrier of j
Ball (Fj,fi) is Element of bool the carrier of j
r1 is Element of the carrier of i
Ball (r1,fi) is Element of bool the carrier of i
bb is Element of bool the carrier of (TopSpaceMetr i)
b is Element of bool the carrier of (TopSpaceMetr j)
[:bb,b:] is V16() Element of bool the carrier of [:(TopSpaceMetr i),(TopSpaceMetr j):]
fb is set
fbb is set
fxx is set
[fbb,fxx] is V27() set
{fbb,fxx} is set
{fbb} is set
{{fbb,fxx},{fbb}} is set
x1 is Element of the carrier of i
b1 is Element of the carrier of j
(i,j,x1,b1) is V27() Element of the carrier of (i,j)
{x1,b1} is set
{x1} is set
{{x1,b1},{x1}} is set
the distance of (i,j) is V16() V19([: the carrier of (i,j), the carrier of (i,j):]) V20( REAL ) Function-like V30([: the carrier of (i,j), the carrier of (i,j):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:]
[: the carrier of (i,j), the carrier of (i,j):] is non empty V16() set
[:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of (i,j), the carrier of (i,j):],REAL:] is non empty set
the distance of (i,j) . (f,(i,j,x1,b1)) is V11() V12() ext-real Element of REAL
[f,(i,j,x1,b1)] is V27() set
{f,(i,j,x1,b1)} is set
{f} is set
{{f,(i,j,x1,b1)},{f}} is set
the distance of (i,j) . [f,(i,j,x1,b1)] is V11() V12() ext-real set
the distance of i is V16() V19([: the carrier of i, the carrier of i:]) V20( REAL ) Function-like V30([: the carrier of i, the carrier of i:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of i, the carrier of i:],REAL:]
[: the carrier of i, the carrier of i:] is non empty V16() set
[:[: the carrier of i, the carrier of i:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of i, the carrier of i:],REAL:] is non empty set
the distance of j is V16() V19([: the carrier of j, the carrier of j:]) V20( REAL ) Function-like V30([: the carrier of j, the carrier of j:], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of j, the carrier of j:],REAL:]
[: the carrier of j, the carrier of j:] is non empty V16() set
[:[: the carrier of j, the carrier of j:],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of j, the carrier of j:],REAL:] is non empty set
b2 is Element of the carrier of i
x2i is Element of the carrier of j
(i,j,b2,x2i) is V27() Element of the carrier of (i,j)
{b2,x2i} is set
{b2} is set
{{b2,x2i},{b2}} is set
x2 is Element of the carrier of i
b2i is Element of the carrier of j
(i,j,x2,b2i) is V27() Element of the carrier of (i,j)
{x2,b2i} is set
{x2} is set
{{x2,b2i},{x2}} is set
the distance of i . (b2,x2) is V11() V12() ext-real Element of REAL
[b2,x2] is V27() set
{b2,x2} is set
{{b2,x2},{b2}} is set
the distance of i . [b2,x2] is V11() V12() ext-real set
the distance of j . (x2i,b2i) is V11() V12() ext-real Element of REAL
[x2i,b2i] is V27() set
{x2i,b2i} is set
{x2i} is set
{{x2i,b2i},{x2i}} is set
the distance of j . [x2i,b2i] is V11() V12() ext-real set
max (( the distance of i . (b2,x2)),( the distance of j . (x2i,b2i))) is V11() V12() ext-real Element of REAL
dist (x2i,b2i) is V11() V12() ext-real Element of REAL
dist (b2,x2) is V11() V12() ext-real Element of REAL
dist (f,(i,j,x1,b1)) is V11() V12() ext-real Element of REAL
f is set
f is Element of bool the carrier of (TopSpaceMetr i)
fi is Element of bool the carrier of (TopSpaceMetr j)
[:f,fi:] is V16() Element of bool the carrier of [:(TopSpaceMetr i),(TopSpaceMetr j):]
i is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of i is non empty set
TopSpaceMetr i is non empty strict TopSpace-like TopStruct
j is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of j is non empty set
TopSpaceMetr j is non empty strict TopSpace-like TopStruct
Family_open_set i is Element of bool (bool the carrier of i)
bool the carrier of i is non empty set
bool (bool the carrier of i) is non empty set
Family_open_set j is Element of bool (bool the carrier of j)
bool the carrier of j is non empty set
bool (bool the carrier of j) is non empty set
f is set
c₄ is Element of the carrier of j
cij is Element of the carrier of i
f is V11() V12() ext-real Element of REAL
Ball (cij,f) is Element of bool the carrier of i
f is V11() V12() ext-real Element of REAL
Ball (c₄,f) is Element of bool the carrier of j
f is set
c₄ is Element of the carrier of i
cij is Element of the carrier of j
f is V11() V12() ext-real Element of REAL
Ball (cij,f) is Element of bool the carrier of j
f is V11() V12() ext-real Element of REAL
Ball (c₄,f) is Element of bool the carrier of i
TopStruct(# the carrier of i,(Family_open_set i) #) is strict TopStruct
i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Euclid i is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL i is non empty functional FinSequence-membered FinSequenceSet of REAL
i -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist i is V16() V19([:(REAL i),(REAL i):]) V20( REAL ) Function-like V30([:(REAL i),(REAL i):], REAL ) complex-yielding V141() V142() Element of bool [:[:(REAL i),(REAL i):],REAL:]
[:(REAL i),(REAL i):] is non empty V16() set
[:[:(REAL i),(REAL i):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:(REAL i),(REAL i):],REAL:] is non empty set
MetrStruct(# (REAL i),(Pitag_dist i) #) is strict MetrStruct
TopSpaceMetr (Euclid i) is non empty strict TopSpace-like TopStruct
j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Euclid j is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL j is non empty functional FinSequence-membered FinSequenceSet of REAL
j -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist j is V16() V19([:(REAL j),(REAL j):]) V20( REAL ) Function-like V30([:(REAL j),(REAL j):], REAL ) complex-yielding V141() V142() Element of bool [:[:(REAL j),(REAL j):],REAL:]
[:(REAL j),(REAL j):] is non empty V16() set
[:[:(REAL j),(REAL j):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:(REAL j),(REAL j):],REAL:] is non empty set
MetrStruct(# (REAL j),(Pitag_dist j) #) is strict MetrStruct
TopSpaceMetr (Euclid j) is non empty strict TopSpace-like TopStruct
[:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] is strict TopSpace-like TopStruct
the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] is set
i + j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Euclid (i + j) is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL (i + j) is non empty functional FinSequence-membered FinSequenceSet of REAL
(i + j) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist (i + j) is V16() V19([:(REAL (i + j)),(REAL (i + j)):]) V20( REAL ) Function-like V30([:(REAL (i + j)),(REAL (i + j)):], REAL ) complex-yielding V141() V142() Element of bool [:[:(REAL (i + j)),(REAL (i + j)):],REAL:]
[:(REAL (i + j)),(REAL (i + j)):] is non empty V16() set
[:[:(REAL (i + j)),(REAL (i + j)):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:(REAL (i + j)),(REAL (i + j)):],REAL:] is non empty set
MetrStruct(# (REAL (i + j)),(Pitag_dist (i + j)) #) is strict MetrStruct
TopSpaceMetr (Euclid (i + j)) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid (i + j))) is non empty set
[: the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], the carrier of (TopSpaceMetr (Euclid (i + j))):] is V16() set
bool [: the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], the carrier of (TopSpaceMetr (Euclid (i + j))):] is non empty set
the carrier of (Euclid i) is non empty set
the carrier of (Euclid j) is non empty set
the carrier of (Euclid (i + j)) is non empty set
((Euclid i),(Euclid j)) is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
TopSpaceMetr ((Euclid i),(Euclid j)) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr ((Euclid i),(Euclid j))) is non empty set
the carrier of ((Euclid i),(Euclid j)) is non empty set
f is Element of the carrier of (Euclid i)
f is Element of the carrier of (Euclid j)
f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
fi is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
f ^ fi is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
fj is Element of the carrier of (Euclid (i + j))
[: the carrier of (Euclid i), the carrier of (Euclid j):] is non empty V16() set
[:[: the carrier of (Euclid i), the carrier of (Euclid j):], the carrier of (Euclid (i + j)):] is non empty V16() set
bool [:[: the carrier of (Euclid i), the carrier of (Euclid j):], the carrier of (Euclid (i + j)):] is non empty set
f is V16() V19([: the carrier of (Euclid i), the carrier of (Euclid j):]) V20( the carrier of (Euclid (i + j))) Function-like V30([: the carrier of (Euclid i), the carrier of (Euclid j):], the carrier of (Euclid (i + j))) Element of bool [:[: the carrier of (Euclid i), the carrier of (Euclid j):], the carrier of (Euclid (i + j)):]
[: the carrier of (TopSpaceMetr ((Euclid i),(Euclid j))), the carrier of (TopSpaceMetr (Euclid (i + j))):] is non empty V16() set
bool [: the carrier of (TopSpaceMetr ((Euclid i),(Euclid j))), the carrier of (TopSpaceMetr (Euclid (i + j))):] is non empty set
f is V16() V19( the carrier of (TopSpaceMetr ((Euclid i),(Euclid j)))) V20( the carrier of (TopSpaceMetr (Euclid (i + j)))) Function-like V30( the carrier of (TopSpaceMetr ((Euclid i),(Euclid j))), the carrier of (TopSpaceMetr (Euclid (i + j)))) Element of bool [: the carrier of (TopSpaceMetr ((Euclid i),(Euclid j))), the carrier of (TopSpaceMetr (Euclid (i + j))):]
f is V16() V19( the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):]) V20( the carrier of (TopSpaceMetr (Euclid (i + j)))) Function-like V30( the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], the carrier of (TopSpaceMetr (Euclid (i + j)))) Element of bool [: the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], the carrier of (TopSpaceMetr (Euclid (i + j))):]
dom f is Element of bool the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):]
bool the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] is non empty set
[#] [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] is non proper Element of bool the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):]
rng f is Element of bool the carrier of (TopSpaceMetr (Euclid (i + j)))
bool the carrier of (TopSpaceMetr (Euclid (i + j))) is non empty set
[#] (TopSpaceMetr (Euclid (i + j))) is non empty non proper Element of bool the carrier of (TopSpaceMetr (Euclid (i + j)))
f " is V16() V19( the carrier of (TopSpaceMetr (Euclid (i + j)))) V20( the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):]) Function-like V30( the carrier of (TopSpaceMetr (Euclid (i + j))), the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):]) Element of bool [: the carrier of (TopSpaceMetr (Euclid (i + j))), the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):]:]
[: the carrier of (TopSpaceMetr (Euclid (i + j))), the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):]:] is V16() set
bool [: the carrier of (TopSpaceMetr (Euclid (i + j))), the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):]:] is non empty set
fi is set
fj is V16() V19( NAT ) V20( REAL ) Function-like V40(i + j) FinSequence-like complex-yielding V141() V142() Element of REAL (i + j)
len fj is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Fi is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len Fi is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Fj is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len Fj is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Fi ^ Fj is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
[:NAT,REAL:] is V16() complex-yielding V141() V142() set
bool [:NAT,REAL:] is non empty set
[Fi,Fj] is V27() Element of [:(bool [:NAT,REAL:]),(bool [:NAT,REAL:]):]
[:(bool [:NAT,REAL:]),(bool [:NAT,REAL:]):] is non empty V16() set
{Fi,Fj} is set
{Fi} is set
{{Fi,Fj},{Fi}} is set
f . (Fi,Fj) is set
[Fi,Fj] is V27() set
f . [Fi,Fj] is set
r1 is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
b is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
r1 ^ b is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
fi is set
proj1 f is set
fj is set
f . fi is set
f . fj is set
Fi is set
Fj is set
[Fi,Fj] is V27() set
{Fi,Fj} is set
{Fi} is set
{{Fi,Fj},{Fi}} is set
r1 is set
b is set
[r1,b] is V27() set
{r1,b} is set
{r1} is set
{{r1,b},{r1}} is set
f . (Fi,Fj) is set
f . [Fi,Fj] is set
bb is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
fb is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
bb ^ fb is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
f . (r1,b) is set
f . [r1,b] is set
fbb is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
fxx is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
fbb ^ fxx is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len fb is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len fxx is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len bb is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len fbb is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
bool the carrier of (TopSpaceMetr ((Euclid i),(Euclid j))) is non empty set
fi is Element of bool the carrier of (TopSpaceMetr ((Euclid i),(Euclid j)))
(f ") " fi is Element of bool the carrier of (TopSpaceMetr (Euclid (i + j)))
the topology of (TopSpaceMetr ((Euclid i),(Euclid j))) is Element of bool (bool the carrier of (TopSpaceMetr ((Euclid i),(Euclid j))))
bool (bool the carrier of (TopSpaceMetr ((Euclid i),(Euclid j)))) is non empty set
Family_open_set ((Euclid i),(Euclid j)) is Element of bool (bool the carrier of ((Euclid i),(Euclid j)))
bool the carrier of ((Euclid i),(Euclid j)) is non empty set
bool (bool the carrier of ((Euclid i),(Euclid j))) is non empty set
f .: fi is Element of bool the carrier of (TopSpaceMetr (Euclid (i + j)))
fj is Element of the carrier of (Euclid (i + j))
Fi is set
f . Fi is set
Fj is Element of the carrier of ((Euclid i),(Euclid j))
r1 is V11() V12() ext-real Element of REAL
Ball (Fj,r1) is Element of bool the carrier of ((Euclid i),(Euclid j))
Ball (fj,r1) is Element of bool the carrier of (Euclid (i + j))
bool the carrier of (Euclid (i + j)) is non empty set
b is set
bb is Element of the carrier of (Euclid (i + j))
dist (bb,fj) is V11() V12() ext-real Element of REAL
the distance of (Euclid (i + j)) is V16() V19([: the carrier of (Euclid (i + j)), the carrier of (Euclid (i + j)):]) V20( REAL ) Function-like V30([: the carrier of (Euclid (i + j)), the carrier of (Euclid (i + j)):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of (Euclid (i + j)), the carrier of (Euclid (i + j)):],REAL:]
[: the carrier of (Euclid (i + j)), the carrier of (Euclid (i + j)):] is non empty V16() set
[:[: the carrier of (Euclid (i + j)), the carrier of (Euclid (i + j)):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of (Euclid (i + j)), the carrier of (Euclid (i + j)):],REAL:] is non empty set
the distance of (Euclid (i + j)) . (bb,fj) is V11() V12() ext-real Element of REAL
[bb,fj] is V27() set
{bb,fj} is set
{bb} is set
{{bb,fj},{bb}} is set
the distance of (Euclid (i + j)) . [bb,fj] is V11() V12() ext-real set
fb is V16() V19( NAT ) V20( REAL ) Function-like V40(i + j) FinSequence-like complex-yielding V141() V142() Element of REAL (i + j)
fbb is V16() V19( NAT ) V20( REAL ) Function-like V40(i + j) FinSequence-like complex-yielding V141() V142() Element of REAL (i + j)
fb - fbb is V16() V19( NAT ) V20( REAL ) Function-like V40(i + j) FinSequence-like complex-yielding V141() V142() Element of REAL (i + j)
|.(fb - fbb).| is V11() V12() ext-real non negative Element of REAL
sqr (fb - fbb) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
Sum (sqr (fb - fbb)) is V11() V12() ext-real Element of REAL
sqrt (Sum (sqr (fb - fbb))) is V11() V12() ext-real Element of REAL
abs (fb - fbb) is V16() V19( NAT ) V20( REAL ) Function-like V40(i + j) FinSequence-like complex-yielding V141() V142() Element of (i + j) -tuples_on REAL
absreal * (fb - fbb) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
sqr (abs (fb - fbb)) is V16() V19( NAT ) V20( REAL ) Function-like V40(i + j) FinSequence-like complex-yielding V141() V142() Element of (i + j) -tuples_on REAL
Sum (sqr (abs (fb - fbb))) is V11() V12() ext-real Element of REAL
sqrt (Sum (sqr (abs (fb - fbb)))) is V11() V12() ext-real Element of REAL
fxx is V16() V19( NAT ) V20( REAL ) Function-like V40(i + j) FinSequence-like complex-yielding V141() V142() Element of REAL (i + j)
len fxx is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
b1 is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len b1 is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
x1 is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len x1 is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
b1 ^ x1 is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
x2 is Element of the carrier of (Euclid i)
b2 is Element of the carrier of (Euclid j)
f . (x2,b2) is set
[x2,b2] is V27() set
{x2,b2} is set
{x2} is set
{{x2,b2},{x2}} is set
f . [x2,b2] is set
x2i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
b2i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
x2i ^ b2i is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
((Euclid i),(Euclid j),Fj) is Element of the carrier of (Euclid i)
dist (x2,((Euclid i),(Euclid j),Fj)) is V11() V12() ext-real Element of REAL
the distance of (Euclid i) is V16() V19([: the carrier of (Euclid i), the carrier of (Euclid i):]) V20( REAL ) Function-like V30([: the carrier of (Euclid i), the carrier of (Euclid i):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of (Euclid i), the carrier of (Euclid i):],REAL:]
[: the carrier of (Euclid i), the carrier of (Euclid i):] is non empty V16() set
[:[: the carrier of (Euclid i), the carrier of (Euclid i):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of (Euclid i), the carrier of (Euclid i):],REAL:] is non empty set
the distance of (Euclid i) . (x2,((Euclid i),(Euclid j),Fj)) is V11() V12() ext-real Element of REAL
[x2,((Euclid i),(Euclid j),Fj)] is V27() set
{x2,((Euclid i),(Euclid j),Fj)} is set
{{x2,((Euclid i),(Euclid j),Fj)},{x2}} is set
the distance of (Euclid i) . [x2,((Euclid i),(Euclid j),Fj)] is V11() V12() ext-real set
((Euclid i),(Euclid j),Fj) is Element of the carrier of (Euclid j)
dist (b2,((Euclid i),(Euclid j),Fj)) is V11() V12() ext-real Element of REAL
the distance of (Euclid j) is V16() V19([: the carrier of (Euclid j), the carrier of (Euclid j):]) V20( REAL ) Function-like V30([: the carrier of (Euclid j), the carrier of (Euclid j):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of (Euclid j), the carrier of (Euclid j):],REAL:]
[: the carrier of (Euclid j), the carrier of (Euclid j):] is non empty V16() set
[:[: the carrier of (Euclid j), the carrier of (Euclid j):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of (Euclid j), the carrier of (Euclid j):],REAL:] is non empty set
the distance of (Euclid j) . (b2,((Euclid i),(Euclid j),Fj)) is V11() V12() ext-real Element of REAL
[b2,((Euclid i),(Euclid j),Fj)] is V27() set
{b2,((Euclid i),(Euclid j),Fj)} is set
{b2} is set
{{b2,((Euclid i),(Euclid j),Fj)},{b2}} is set
the distance of (Euclid j) . [b2,((Euclid i),(Euclid j),Fj)] is V11() V12() ext-real set
max ((dist (x2,((Euclid i),(Euclid j),Fj))),(dist (b2,((Euclid i),(Euclid j),Fj)))) is V11() V12() ext-real Element of REAL
b1f is set
b2f is set
[b1f,b2f] is V27() set
{b1f,b2f} is set
{b1f} is set
{{b1f,b2f},{b1f}} is set
x2f is Element of the carrier of (Euclid i)
x1f is Element of the carrier of (Euclid j)
f . (x2f,x1f) is set
[x2f,x1f] is V27() set
{x2f,x1f} is set
{x2f} is set
{{x2f,x1f},{x2f}} is set
f . [x2f,x1f] is set
fi is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
fj is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
fi ^ fj is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len fi is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len fj is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len x2i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len b2i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
x2i - fi is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs (x2i - fi) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * (x2i - fi) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
b2i - fj is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
abs (b2i - fj) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
absreal * (b2i - fj) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
(abs (x2i - fi)) ^ (abs (b2i - fj)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr ((abs (x2i - fi)) ^ (abs (b2i - fj))) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
Sum (sqr ((abs (x2i - fi)) ^ (abs (b2i - fj)))) is V11() V12() ext-real Element of REAL
sqrt (Sum (sqr ((abs (x2i - fi)) ^ (abs (b2i - fj))))) is V11() V12() ext-real Element of REAL
sqr (abs (x2i - fi)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr (abs (b2i - fj)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
(sqr (abs (x2i - fi))) ^ (sqr (abs (b2i - fj))) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
Sum ((sqr (abs (x2i - fi))) ^ (sqr (abs (b2i - fj)))) is V11() V12() ext-real Element of REAL
sqrt (Sum ((sqr (abs (x2i - fi))) ^ (sqr (abs (b2i - fj))))) is V11() V12() ext-real Element of REAL
Sum (sqr (abs (x2i - fi))) is V11() V12() ext-real Element of REAL
Sum (sqr (abs (b2i - fj))) is V11() V12() ext-real Element of REAL
(Sum (sqr (abs (x2i - fi)))) + (Sum (sqr (abs (b2i - fj)))) is V11() V12() ext-real Element of REAL
sqrt ((Sum (sqr (abs (x2i - fi)))) + (Sum (sqr (abs (b2i - fj))))) is V11() V12() ext-real Element of REAL
a22 is V16() V19( NAT ) V20( REAL ) Function-like V40(j) FinSequence-like complex-yielding V141() V142() Element of REAL j
hh2 is V16() V19( NAT ) V20( REAL ) Function-like V40(j) FinSequence-like complex-yielding V141() V142() Element of REAL j
hh2 - a22 is V16() V19( NAT ) V20( REAL ) Function-like V40(j) FinSequence-like complex-yielding V141() V142() Element of REAL j
abs (hh2 - a22) is V16() V19( NAT ) V20( REAL ) Function-like V40(j) FinSequence-like complex-yielding V141() V142() Element of j -tuples_on REAL
absreal * (hh2 - a22) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
sqr (abs (hh2 - a22)) is V16() V19( NAT ) V20( REAL ) Function-like V40(j) FinSequence-like complex-yielding V141() V142() Element of j -tuples_on REAL
Sum (sqr (abs (hh2 - a22))) is V11() V12() ext-real Element of REAL
(Sum (sqr (abs (hh2 - a22)))) + 0 is V11() V12() ext-real Element of REAL
sqrt (Sum (sqr (abs (hh2 - a22)))) is V11() V12() ext-real Element of REAL
|.(hh2 - a22).| is V11() V12() ext-real non negative Element of REAL
sqr (hh2 - a22) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
Sum (sqr (hh2 - a22)) is V11() V12() ext-real Element of REAL
sqrt (Sum (sqr (hh2 - a22))) is V11() V12() ext-real Element of REAL
(Pitag_dist j) . (hh2,a22) is V11() V12() ext-real Element of REAL
[hh2,a22] is V27() set
{hh2,a22} is set
{hh2} is set
{{hh2,a22},{hh2}} is set
(Pitag_dist j) . [hh2,a22] is V11() V12() ext-real set
x1i is V16() V19( NAT ) V20( REAL ) Function-like V40(i) FinSequence-like complex-yielding V141() V142() Element of REAL i
b1i is V16() V19( NAT ) V20( REAL ) Function-like V40(i) FinSequence-like complex-yielding V141() V142() Element of REAL i
b1i - x1i is V16() V19( NAT ) V20( REAL ) Function-like V40(i) FinSequence-like complex-yielding V141() V142() Element of REAL i
abs (b1i - x1i) is V16() V19( NAT ) V20( REAL ) Function-like V40(i) FinSequence-like complex-yielding V141() V142() Element of i -tuples_on REAL
absreal * (b1i - x1i) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
sqr (abs (b1i - x1i)) is V16() V19( NAT ) V20( REAL ) Function-like V40(i) FinSequence-like complex-yielding V141() V142() Element of i -tuples_on REAL
Sum (sqr (abs (b1i - x1i))) is V11() V12() ext-real Element of REAL
(Sum (sqr (abs (b1i - x1i)))) + 0 is V11() V12() ext-real Element of REAL
sqrt (Sum (sqr (abs (b1i - x1i)))) is V11() V12() ext-real Element of REAL
|.(b1i - x1i).| is V11() V12() ext-real non negative Element of REAL
sqr (b1i - x1i) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
Sum (sqr (b1i - x1i)) is V11() V12() ext-real Element of REAL
sqrt (Sum (sqr (b1i - x1i))) is V11() V12() ext-real Element of REAL
(Pitag_dist i) . (b1i,x1i) is V11() V12() ext-real Element of REAL
[b1i,x1i] is V27() set
{b1i,x1i} is set
{b1i} is set
{{b1i,x1i},{b1i}} is set
(Pitag_dist i) . [b1i,x1i] is V11() V12() ext-real set
((Euclid i),(Euclid j),x2,b2) is V27() Element of the carrier of ((Euclid i),(Euclid j))
((Euclid i),(Euclid j),((Euclid i),(Euclid j),Fj),((Euclid i),(Euclid j),Fj)) is V27() Element of the carrier of ((Euclid i),(Euclid j))
{((Euclid i),(Euclid j),Fj),((Euclid i),(Euclid j),Fj)} is set
{((Euclid i),(Euclid j),Fj)} is set
{{((Euclid i),(Euclid j),Fj),((Euclid i),(Euclid j),Fj)},{((Euclid i),(Euclid j),Fj)}} is set
dist (((Euclid i),(Euclid j),x2,b2),((Euclid i),(Euclid j),((Euclid i),(Euclid j),Fj),((Euclid i),(Euclid j),Fj))) is V11() V12() ext-real Element of REAL
the distance of ((Euclid i),(Euclid j)) is V16() V19([: the carrier of ((Euclid i),(Euclid j)), the carrier of ((Euclid i),(Euclid j)):]) V20( REAL ) Function-like V30([: the carrier of ((Euclid i),(Euclid j)), the carrier of ((Euclid i),(Euclid j)):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of ((Euclid i),(Euclid j)), the carrier of ((Euclid i),(Euclid j)):],REAL:]
[: the carrier of ((Euclid i),(Euclid j)), the carrier of ((Euclid i),(Euclid j)):] is non empty V16() set
[:[: the carrier of ((Euclid i),(Euclid j)), the carrier of ((Euclid i),(Euclid j)):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of ((Euclid i),(Euclid j)), the carrier of ((Euclid i),(Euclid j)):],REAL:] is non empty set
the distance of ((Euclid i),(Euclid j)) . (((Euclid i),(Euclid j),x2,b2),((Euclid i),(Euclid j),((Euclid i),(Euclid j),Fj),((Euclid i),(Euclid j),Fj))) is V11() V12() ext-real Element of REAL
[((Euclid i),(Euclid j),x2,b2),((Euclid i),(Euclid j),((Euclid i),(Euclid j),Fj),((Euclid i),(Euclid j),Fj))] is V27() set
{((Euclid i),(Euclid j),x2,b2),((Euclid i),(Euclid j),((Euclid i),(Euclid j),Fj),((Euclid i),(Euclid j),Fj))} is V16() set
{((Euclid i),(Euclid j),x2,b2)} is V16() set
{{((Euclid i),(Euclid j),x2,b2),((Euclid i),(Euclid j),((Euclid i),(Euclid j),Fj),((Euclid i),(Euclid j),Fj))},{((Euclid i),(Euclid j),x2,b2)}} is set
the distance of ((Euclid i),(Euclid j)) . [((Euclid i),(Euclid j),x2,b2),((Euclid i),(Euclid j),((Euclid i),(Euclid j),Fj),((Euclid i),(Euclid j),Fj))] is V11() V12() ext-real set
dist (((Euclid i),(Euclid j),x2,b2),Fj) is V11() V12() ext-real Element of REAL
the distance of ((Euclid i),(Euclid j)) . (((Euclid i),(Euclid j),x2,b2),Fj) is V11() V12() ext-real Element of REAL
[((Euclid i),(Euclid j),x2,b2),Fj] is V27() set
{((Euclid i),(Euclid j),x2,b2),Fj} is set
{{((Euclid i),(Euclid j),x2,b2),Fj},{((Euclid i),(Euclid j),x2,b2)}} is set
the distance of ((Euclid i),(Euclid j)) . [((Euclid i),(Euclid j),x2,b2),Fj] is V11() V12() ext-real set
[:NAT,REAL:] is V16() complex-yielding V141() V142() set
bool [:NAT,REAL:] is non empty set
[x2i,b2i] is V27() Element of [:(bool [:NAT,REAL:]),(bool [:NAT,REAL:]):]
[:(bool [:NAT,REAL:]),(bool [:NAT,REAL:]):] is non empty V16() set
{x2i,b2i} is set
{x2i} is set
{{x2i,b2i},{x2i}} is set
bool the carrier of (Euclid (i + j)) is non empty set
Family_open_set (Euclid (i + j)) is Element of bool (bool the carrier of (Euclid (i + j)))
bool (bool the carrier of (Euclid (i + j))) is non empty set
the topology of (TopSpaceMetr (Euclid (i + j))) is Element of bool (bool the carrier of (TopSpaceMetr (Euclid (i + j))))
bool (bool the carrier of (TopSpaceMetr (Euclid (i + j)))) is non empty set
fi is Element of bool the carrier of (TopSpaceMetr (Euclid (i + j)))
f " fi is Element of bool the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):]
the topology of (TopSpaceMetr (Euclid (i + j))) is Element of bool (bool the carrier of (TopSpaceMetr (Euclid (i + j))))
bool (bool the carrier of (TopSpaceMetr (Euclid (i + j)))) is non empty set
Family_open_set (Euclid (i + j)) is Element of bool (bool the carrier of (Euclid (i + j)))
bool the carrier of (Euclid (i + j)) is non empty set
bool (bool the carrier of (Euclid (i + j))) is non empty set
fj is Element of the carrier of ((Euclid i),(Euclid j))
f . fj is set
Fi is Element of the carrier of (Euclid (i + j))
Fj is V11() V12() ext-real Element of REAL
Ball (Fi,Fj) is Element of bool the carrier of (Euclid (i + j))
Fj / 2 is V11() V12() ext-real Element of REAL
r1 is V11() V12() ext-real Element of REAL
Ball (fj,r1) is Element of bool the carrier of ((Euclid i),(Euclid j))
bool the carrier of ((Euclid i),(Euclid j)) is non empty set
b is set
bb is Element of the carrier of ((Euclid i),(Euclid j))
dist (bb,fj) is V11() V12() ext-real Element of REAL
the distance of ((Euclid i),(Euclid j)) is V16() V19([: the carrier of ((Euclid i),(Euclid j)), the carrier of ((Euclid i),(Euclid j)):]) V20( REAL ) Function-like V30([: the carrier of ((Euclid i),(Euclid j)), the carrier of ((Euclid i),(Euclid j)):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of ((Euclid i),(Euclid j)), the carrier of ((Euclid i),(Euclid j)):],REAL:]
[: the carrier of ((Euclid i),(Euclid j)), the carrier of ((Euclid i),(Euclid j)):] is non empty V16() set
[:[: the carrier of ((Euclid i),(Euclid j)), the carrier of ((Euclid i),(Euclid j)):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of ((Euclid i),(Euclid j)), the carrier of ((Euclid i),(Euclid j)):],REAL:] is non empty set
the distance of ((Euclid i),(Euclid j)) . (bb,fj) is V11() V12() ext-real Element of REAL
[bb,fj] is V27() set
{bb,fj} is set
{bb} is set
{{bb,fj},{bb}} is set
the distance of ((Euclid i),(Euclid j)) . [bb,fj] is V11() V12() ext-real set
f . bb is set
f . b is set
fb is Element of the carrier of (Euclid (i + j))
the distance of (Euclid i) is V16() V19([: the carrier of (Euclid i), the carrier of (Euclid i):]) V20( REAL ) Function-like V30([: the carrier of (Euclid i), the carrier of (Euclid i):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of (Euclid i), the carrier of (Euclid i):],REAL:]
[: the carrier of (Euclid i), the carrier of (Euclid i):] is non empty V16() set
[:[: the carrier of (Euclid i), the carrier of (Euclid i):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of (Euclid i), the carrier of (Euclid i):],REAL:] is non empty set
the distance of (Euclid j) is V16() V19([: the carrier of (Euclid j), the carrier of (Euclid j):]) V20( REAL ) Function-like V30([: the carrier of (Euclid j), the carrier of (Euclid j):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of (Euclid j), the carrier of (Euclid j):],REAL:]
[: the carrier of (Euclid j), the carrier of (Euclid j):] is non empty V16() set
[:[: the carrier of (Euclid j), the carrier of (Euclid j):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of (Euclid j), the carrier of (Euclid j):],REAL:] is non empty set
b1 is Element of the carrier of (Euclid i)
b2 is Element of the carrier of (Euclid j)
((Euclid i),(Euclid j),b1,b2) is V27() Element of the carrier of ((Euclid i),(Euclid j))
{b1,b2} is set
{b1} is set
{{b1,b2},{b1}} is set
x1 is Element of the carrier of (Euclid i)
x2 is Element of the carrier of (Euclid j)
((Euclid i),(Euclid j),x1,x2) is V27() Element of the carrier of ((Euclid i),(Euclid j))
{x1,x2} is set
{x1} is set
{{x1,x2},{x1}} is set
the distance of (Euclid i) . (b1,x1) is V11() V12() ext-real Element of REAL
[b1,x1] is V27() set
{b1,x1} is set
{{b1,x1},{b1}} is set
the distance of (Euclid i) . [b1,x1] is V11() V12() ext-real set
the distance of (Euclid j) . (b2,x2) is V11() V12() ext-real Element of REAL
[b2,x2] is V27() set
{b2,x2} is set
{b2} is set
{{b2,x2},{b2}} is set
the distance of (Euclid j) . [b2,x2] is V11() V12() ext-real set
max (( the distance of (Euclid i) . (b1,x1)),( the distance of (Euclid j) . (b2,x2))) is V11() V12() ext-real Element of REAL
dist (((Euclid i),(Euclid j),b1,b2),((Euclid i),(Euclid j),x1,x2)) is V11() V12() ext-real Element of REAL
the distance of ((Euclid i),(Euclid j)) . (((Euclid i),(Euclid j),b1,b2),((Euclid i),(Euclid j),x1,x2)) is V11() V12() ext-real Element of REAL
[((Euclid i),(Euclid j),b1,b2),((Euclid i),(Euclid j),x1,x2)] is V27() set
{((Euclid i),(Euclid j),b1,b2),((Euclid i),(Euclid j),x1,x2)} is V16() set
{((Euclid i),(Euclid j),b1,b2)} is V16() set
{{((Euclid i),(Euclid j),b1,b2),((Euclid i),(Euclid j),x1,x2)},{((Euclid i),(Euclid j),b1,b2)}} is set
the distance of ((Euclid i),(Euclid j)) . [((Euclid i),(Euclid j),b1,b2),((Euclid i),(Euclid j),x1,x2)] is V11() V12() ext-real set
dist (b1,x1) is V11() V12() ext-real Element of REAL
dist (b2,x2) is V11() V12() ext-real Element of REAL
max ((dist (b1,x1)),(dist (b2,x2))) is V11() V12() ext-real Element of REAL
f . (b1,b2) is set
[b1,b2] is V27() set
f . [b1,b2] is set
b1f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
b2f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
b1f ^ b2f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len b1f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len b2f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
r1 + r1 is V11() V12() ext-real Element of REAL
b1i is V16() V19( NAT ) V20( REAL ) Function-like V40(i) FinSequence-like complex-yielding V141() V142() Element of REAL i
x1i is V16() V19( NAT ) V20( REAL ) Function-like V40(i) FinSequence-like complex-yielding V141() V142() Element of REAL i
(Pitag_dist i) . (b1i,x1i) is V11() V12() ext-real Element of REAL
[b1i,x1i] is V27() set
{b1i,x1i} is set
{b1i} is set
{{b1i,x1i},{b1i}} is set
(Pitag_dist i) . [b1i,x1i] is V11() V12() ext-real set
b2i is V16() V19( NAT ) V20( REAL ) Function-like V40(j) FinSequence-like complex-yielding V141() V142() Element of REAL j
x2i is V16() V19( NAT ) V20( REAL ) Function-like V40(j) FinSequence-like complex-yielding V141() V142() Element of REAL j
(Pitag_dist j) . (b2i,x2i) is V11() V12() ext-real Element of REAL
[b2i,x2i] is V27() set
{b2i,x2i} is set
{b2i} is set
{{b2i,x2i},{b2i}} is set
(Pitag_dist j) . [b2i,x2i] is V11() V12() ext-real set
((Pitag_dist i) . (b1i,x1i)) + ((Pitag_dist j) . (b2i,x2i)) is V11() V12() ext-real Element of REAL
b1i - x1i is V16() V19( NAT ) V20( REAL ) Function-like V40(i) FinSequence-like complex-yielding V141() V142() Element of REAL i
sqr (b1i - x1i) is V16() V19( NAT ) V20( REAL ) Function-like V40(i) FinSequence-like complex-yielding V141() V142() Element of i -tuples_on REAL
Sum (sqr (b1i - x1i)) is V11() V12() ext-real Element of REAL
b2i - x2i is V16() V19( NAT ) V20( REAL ) Function-like V40(j) FinSequence-like complex-yielding V141() V142() Element of REAL j
sqr (b2i - x2i) is V16() V19( NAT ) V20( REAL ) Function-like V40(j) FinSequence-like complex-yielding V141() V142() Element of j -tuples_on REAL
Sum (sqr (b2i - x2i)) is V11() V12() ext-real Element of REAL
(Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i))) is V11() V12() ext-real Element of REAL
sqrt ((Sum (sqr (b1i - x1i))) + (Sum (sqr (b2i - x2i)))) is V11() V12() ext-real Element of REAL
|.(b1i - x1i).| is V11() V12() ext-real non negative Element of REAL
sqr (b1i - x1i) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
Sum (sqr (b1i - x1i)) is V11() V12() ext-real Element of REAL
sqrt (Sum (sqr (b1i - x1i))) is V11() V12() ext-real Element of REAL
sqrt (Sum (sqr (b2i - x2i))) is V11() V12() ext-real Element of REAL
|.(b1i - x1i).| + (sqrt (Sum (sqr (b2i - x2i)))) is V11() V12() ext-real Element of REAL
|.(b2i - x2i).| is V11() V12() ext-real non negative Element of REAL
sqr (b2i - x2i) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
Sum (sqr (b2i - x2i)) is V11() V12() ext-real Element of REAL
sqrt (Sum (sqr (b2i - x2i))) is V11() V12() ext-real Element of REAL
((Pitag_dist i) . (b1i,x1i)) + |.(b2i - x2i).| is V11() V12() ext-real Element of REAL
f . (x1,x2) is set
[x1,x2] is V27() set
f . [x1,x2] is set
x1f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
x2f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
x1f ^ x2f is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
len x1f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
len x2f is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
fbb is V16() V19( NAT ) V20( REAL ) Function-like V40(i + j) FinSequence-like complex-yielding V141() V142() Element of REAL (i + j)
fxx is V16() V19( NAT ) V20( REAL ) Function-like V40(i + j) FinSequence-like complex-yielding V141() V142() Element of REAL (i + j)
(Pitag_dist (i + j)) . (fbb,fxx) is V11() V12() ext-real Element of REAL
[fbb,fxx] is V27() set
{fbb,fxx} is set
{fbb} is set
{{fbb,fxx},{fbb}} is set
(Pitag_dist (i + j)) . [fbb,fxx] is V11() V12() ext-real set
fbb - fxx is V16() V19( NAT ) V20( REAL ) Function-like V40(i + j) FinSequence-like complex-yielding V141() V142() Element of REAL (i + j)
|.(fbb - fxx).| is V11() V12() ext-real non negative Element of REAL
sqr (fbb - fxx) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
Sum (sqr (fbb - fxx)) is V11() V12() ext-real Element of REAL
sqrt (Sum (sqr (fbb - fxx))) is V11() V12() ext-real Element of REAL
abs (fbb - fxx) is V16() V19( NAT ) V20( REAL ) Function-like V40(i + j) FinSequence-like complex-yielding V141() V142() Element of (i + j) -tuples_on REAL
absreal * (fbb - fxx) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
sqr (abs (fbb - fxx)) is V16() V19( NAT ) V20( REAL ) Function-like V40(i + j) FinSequence-like complex-yielding V141() V142() Element of (i + j) -tuples_on REAL
Sum (sqr (abs (fbb - fxx))) is V11() V12() ext-real Element of REAL
sqrt (Sum (sqr (abs (fbb - fxx)))) is V11() V12() ext-real Element of REAL
abs (b1i - x1i) is V16() V19( NAT ) V20( REAL ) Function-like V40(i) FinSequence-like complex-yielding V141() V142() Element of i -tuples_on REAL
absreal * (b1i - x1i) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
abs (b2i - x2i) is V16() V19( NAT ) V20( REAL ) Function-like V40(j) FinSequence-like complex-yielding V141() V142() Element of j -tuples_on REAL
absreal * (b2i - x2i) is V16() V19( NAT ) V20( REAL ) complex-yielding V141() V142() set
(abs (b1i - x1i)) ^ (abs (b2i - x2i)) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
sqr ((abs (b1i - x1i)) ^ (abs (b2i - x2i))) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
Sum (sqr ((abs (b1i - x1i)) ^ (abs (b2i - x2i)))) is V11() V12() ext-real Element of REAL
sqrt (Sum (sqr ((abs (b1i - x1i)) ^ (abs (b2i - x2i))))) is V11() V12() ext-real Element of REAL
sqr (abs (b1i - x1i)) is V16() V19( NAT ) V20( REAL ) Function-like V40(i) FinSequence-like complex-yielding V141() V142() Element of i -tuples_on REAL
sqr (abs (b2i - x2i)) is V16() V19( NAT ) V20( REAL ) Function-like V40(j) FinSequence-like complex-yielding V141() V142() Element of j -tuples_on REAL
(sqr (abs (b1i - x1i))) ^ (sqr (abs (b2i - x2i))) is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
Sum ((sqr (abs (b1i - x1i))) ^ (sqr (abs (b2i - x2i)))) is V11() V12() ext-real Element of REAL
sqrt (Sum ((sqr (abs (b1i - x1i))) ^ (sqr (abs (b2i - x2i))))) is V11() V12() ext-real Element of REAL
Sum (sqr (abs (b1i - x1i))) is V11() V12() ext-real Element of REAL
Sum (sqr (abs (b2i - x2i))) is V11() V12() ext-real Element of REAL
(Sum (sqr (abs (b1i - x1i)))) + (Sum (sqr (abs (b2i - x2i)))) is V11() V12() ext-real Element of REAL
sqrt ((Sum (sqr (abs (b1i - x1i)))) + (Sum (sqr (abs (b2i - x2i))))) is V11() V12() ext-real Element of REAL
(Sum (sqr (abs (b1i - x1i)))) + (Sum (sqr (b2i - x2i))) is V11() V12() ext-real Element of REAL
sqrt ((Sum (sqr (abs (b1i - x1i)))) + (Sum (sqr (b2i - x2i)))) is V11() V12() ext-real Element of REAL
dist (fb,Fi) is V11() V12() ext-real Element of REAL
the distance of (Euclid (i + j)) is V16() V19([: the carrier of (Euclid (i + j)), the carrier of (Euclid (i + j)):]) V20( REAL ) Function-like V30([: the carrier of (Euclid (i + j)), the carrier of (Euclid (i + j)):], REAL ) complex-yielding V141() V142() Element of bool [:[: the carrier of (Euclid (i + j)), the carrier of (Euclid (i + j)):],REAL:]
[: the carrier of (Euclid (i + j)), the carrier of (Euclid (i + j)):] is non empty V16() set
[:[: the carrier of (Euclid (i + j)), the carrier of (Euclid (i + j)):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[: the carrier of (Euclid (i + j)), the carrier of (Euclid (i + j)):],REAL:] is non empty set
the distance of (Euclid (i + j)) . (fb,Fi) is V11() V12() ext-real Element of REAL
[fb,Fi] is V27() set
{fb,Fi} is set
{fb} is set
{{fb,Fi},{fb}} is set
the distance of (Euclid (i + j)) . [fb,Fi] is V11() V12() ext-real set
bool the carrier of ((Euclid i),(Euclid j)) is non empty set
Family_open_set ((Euclid i),(Euclid j)) is Element of bool (bool the carrier of ((Euclid i),(Euclid j)))
bool (bool the carrier of ((Euclid i),(Euclid j))) is non empty set
the topology of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] is Element of bool (bool the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):])
bool (bool the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):]) is non empty set
[#] (TopSpaceMetr ((Euclid i),(Euclid j))) is non empty non proper Element of bool the carrier of (TopSpaceMetr ((Euclid i),(Euclid j)))
fi is V16() Function-like FinSequence-like set
fj is V16() Function-like FinSequence-like set
[fi,fj] is V27() set
{fi,fj} is set
{fi} is set
{{fi,fj},{fi}} is set
f . (fi,fj) is set
f . [fi,fj] is set
fi ^ fj is V16() Function-like FinSequence-like set
Fi is Element of the carrier of (Euclid i)
Fj is Element of the carrier of (Euclid j)
f . (Fi,Fj) is set
[Fi,Fj] is V27() set
{Fi,Fj} is set
{Fi} is set
{{Fi,Fj},{Fi}} is set
f . [Fi,Fj] is set
r1 is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
b is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
r1 ^ b is V16() V19( NAT ) V20( REAL ) Function-like FinSequence-like complex-yielding V141() V142() FinSequence of REAL
i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Euclid i is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL i is non empty functional FinSequence-membered FinSequenceSet of REAL
i -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist i is V16() V19([:(REAL i),(REAL i):]) V20( REAL ) Function-like V30([:(REAL i),(REAL i):], REAL ) complex-yielding V141() V142() Element of bool [:[:(REAL i),(REAL i):],REAL:]
[:(REAL i),(REAL i):] is non empty V16() set
[:[:(REAL i),(REAL i):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:(REAL i),(REAL i):],REAL:] is non empty set
MetrStruct(# (REAL i),(Pitag_dist i) #) is strict MetrStruct
TopSpaceMetr (Euclid i) is non empty strict TopSpace-like TopStruct
j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Euclid j is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL j is non empty functional FinSequence-membered FinSequenceSet of REAL
j -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist j is V16() V19([:(REAL j),(REAL j):]) V20( REAL ) Function-like V30([:(REAL j),(REAL j):], REAL ) complex-yielding V141() V142() Element of bool [:[:(REAL j),(REAL j):],REAL:]
[:(REAL j),(REAL j):] is non empty V16() set
[:[:(REAL j),(REAL j):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:(REAL j),(REAL j):],REAL:] is non empty set
MetrStruct(# (REAL j),(Pitag_dist j) #) is strict MetrStruct
TopSpaceMetr (Euclid j) is non empty strict TopSpace-like TopStruct
[:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] is strict TopSpace-like TopStruct
i + j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Euclid (i + j) is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL (i + j) is non empty functional FinSequence-membered FinSequenceSet of REAL
(i + j) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist (i + j) is V16() V19([:(REAL (i + j)),(REAL (i + j)):]) V20( REAL ) Function-like V30([:(REAL (i + j)),(REAL (i + j)):], REAL ) complex-yielding V141() V142() Element of bool [:[:(REAL (i + j)),(REAL (i + j)):],REAL:]
[:(REAL (i + j)),(REAL (i + j)):] is non empty V16() set
[:[:(REAL (i + j)),(REAL (i + j)):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:(REAL (i + j)),(REAL (i + j)):],REAL:] is non empty set
MetrStruct(# (REAL (i + j)),(Pitag_dist (i + j)) #) is strict MetrStruct
TopSpaceMetr (Euclid (i + j)) is non empty strict TopSpace-like TopStruct
the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] is set
the carrier of (TopSpaceMetr (Euclid (i + j))) is non empty set
[: the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], the carrier of (TopSpaceMetr (Euclid (i + j))):] is V16() set
bool [: the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], the carrier of (TopSpaceMetr (Euclid (i + j))):] is non empty set
f is V16() V19( the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):]) V20( the carrier of (TopSpaceMetr (Euclid (i + j)))) Function-like V30( the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], the carrier of (TopSpaceMetr (Euclid (i + j)))) Element of bool [: the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], the carrier of (TopSpaceMetr (Euclid (i + j))):]
dom f is Element of bool the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):]
bool the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] is non empty set
i is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Euclid i is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL i is non empty functional FinSequence-membered FinSequenceSet of REAL
i -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist i is V16() V19([:(REAL i),(REAL i):]) V20( REAL ) Function-like V30([:(REAL i),(REAL i):], REAL ) complex-yielding V141() V142() Element of bool [:[:(REAL i),(REAL i):],REAL:]
[:(REAL i),(REAL i):] is non empty V16() set
[:[:(REAL i),(REAL i):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:(REAL i),(REAL i):],REAL:] is non empty set
MetrStruct(# (REAL i),(Pitag_dist i) #) is strict MetrStruct
TopSpaceMetr (Euclid i) is non empty strict TopSpace-like TopStruct
j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Euclid j is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL j is non empty functional FinSequence-membered FinSequenceSet of REAL
j -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist j is V16() V19([:(REAL j),(REAL j):]) V20( REAL ) Function-like V30([:(REAL j),(REAL j):], REAL ) complex-yielding V141() V142() Element of bool [:[:(REAL j),(REAL j):],REAL:]
[:(REAL j),(REAL j):] is non empty V16() set
[:[:(REAL j),(REAL j):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:(REAL j),(REAL j):],REAL:] is non empty set
MetrStruct(# (REAL j),(Pitag_dist j) #) is strict MetrStruct
TopSpaceMetr (Euclid j) is non empty strict TopSpace-like TopStruct
[:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] is strict TopSpace-like TopStruct
the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):] is set
i + j is V10() V11() V12() ext-real V89() V150() V166() V167() V168() V169() V170() V171() Element of NAT
Euclid (i + j) is non empty strict Reflexive discerning symmetric triangle Discerning MetrStruct
REAL (i + j) is non empty functional FinSequence-membered FinSequenceSet of REAL
(i + j) -tuples_on REAL is non empty functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist (i + j) is V16() V19([:(REAL (i + j)),(REAL (i + j)):]) V20( REAL ) Function-like V30([:(REAL (i + j)),(REAL (i + j)):], REAL ) complex-yielding V141() V142() Element of bool [:[:(REAL (i + j)),(REAL (i + j)):],REAL:]
[:(REAL (i + j)),(REAL (i + j)):] is non empty V16() set
[:[:(REAL (i + j)),(REAL (i + j)):],REAL:] is non empty V16() complex-yielding V141() V142() set
bool [:[:(REAL (i + j)),(REAL (i + j)):],REAL:] is non empty set
MetrStruct(# (REAL (i + j)),(Pitag_dist (i + j)) #) is strict MetrStruct
TopSpaceMetr (Euclid (i + j)) is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr (Euclid (i + j))) is non empty set
[: the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], the carrier of (TopSpaceMetr (Euclid (i + j))):] is V16() set
bool [: the carrier of [:(TopSpaceMetr (Euclid i)),(TopSpaceMetr (Euclid j)):], the carrier of (TopSpaceMetr (Euclid (i + j))):] is non empty set