REAL is V126() V127() V128() V132() V304() V305() V307() set
NAT is non trivial ordinal non finite cardinal limit_cardinal V126() V127() V128() V129() V130() V131() V132() V304() Element of K19(REAL)
K19(REAL) is set
omega is non trivial ordinal non finite cardinal limit_cardinal V126() V127() V128() V129() V130() V131() V132() V304() set
K19(omega) is non trivial non finite set
K19(NAT) is non trivial non finite set
COMPLEX is V126() V132() set
RAT is V126() V127() V128() V129() V132() set
INT is V126() V127() V128() V129() V130() V132() set
K20(REAL,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is set
K282() is non empty strict L8()
the carrier of K282() is non empty set
<REAL,+> is non empty strict V107() V108() V109() V111() left-invertible right-invertible V150() left-cancelable right-cancelable V153() L8()
K783() is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20(REAL,REAL),REAL))
K20(K20(REAL,REAL),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is set
G8(REAL,K783()) is strict L8()
K288() is non empty strict V109() V111() left-cancelable right-cancelable V153() SubStr of <REAL,+>
<NAT,+> is non empty strict V107() V109() V111() left-cancelable right-cancelable V153() uniquely-decomposable SubStr of K288()
<REAL,*> is non empty strict V107() V109() V111() L8()
K785() is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20(REAL,REAL),REAL))
G8(REAL,K785()) is strict L8()
<NAT,*> is non empty strict V107() V109() V111() uniquely-decomposable SubStr of <REAL,*>
1 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT
K20(1,1) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
K19(K20(1,1)) is finite V49() set
K20(K20(1,1),1) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
K19(K20(K20(1,1),1)) is finite V49() set
K20(K20(1,1),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20(1,1),REAL)) is set
2 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT
K20(2,2) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
K20(K20(2,2),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20(2,2),REAL)) is set
TOP-REAL 2 is non empty V83() constituted-Functions constituted-FinSeqs TopSpace-like V198() V199() V200() V201() V202() V203() V204() V210() L16()
the carrier of (TOP-REAL 2) is non empty set
K589() is V241() TopStruct
the carrier of K589() is V126() V127() V128() set
RealSpace is strict V241() MetrStruct
real_dist is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20(REAL,REAL),REAL))
MetrStruct(# REAL,real_dist #) is strict MetrStruct
R^1 is non empty strict TopSpace-like V241() TopStruct
TopSpaceMetr RealSpace is strict TopSpace-like TopStruct
the carrier of RealSpace is V126() V127() V128() set
Family_open_set RealSpace is Element of K19(K19( the carrier of RealSpace))
K19( the carrier of RealSpace) is set
K19(K19( the carrier of RealSpace)) is set
TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #) is strict TopStruct
K596() is V241() SubSpace of R^1
K574(K596(),K596()) is strict TopSpace-like TopStruct
the carrier of K574(K596(),K596()) is set
K598() is non empty strict TopSpace-like V241() V243() SubSpace of R^1
the carrier of K598() is non empty V126() V127() V128() set
K19( the carrier of K598()) is set
K19(K19( the carrier of K598())) is set
K607(2) is non empty V244() SubSpace of TOP-REAL 2
K157((TOP-REAL 2)) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite 2 -element FinSequence-like FinSubsequence-like zero Element of the carrier of (TOP-REAL 2)
K606(2,K157((TOP-REAL 2)),1) is non empty strict V244() SubSpace of TOP-REAL 2
Sphere (K157((TOP-REAL 2)),1) is non empty closed V214( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
K19( the carrier of (TOP-REAL 2)) is set
(TOP-REAL 2) | (Sphere (K157((TOP-REAL 2)),1)) is strict SubSpace of TOP-REAL 2
the carrier of K607(2) is non empty set
K20( the carrier of K598(), the carrier of K607(2)) is Relation-like set
K19(K20( the carrier of K598(), the carrier of K607(2))) is set
K611() is Relation-like Function-like quasi_total quasi_total onto continuous Element of K19(K20( the carrier of K598(), the carrier of K607(2)))
K608() is Element of the carrier of K607(2)
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real V43() V44() finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() Element of NAT
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() set
|[1,0]| is Relation-like NAT -defined NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued finite 2 -element 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
<*1*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing finite 1 -element FinSequence-like FinSubsequence-like set
[1,1] is set
{1,1} is non empty finite V49() V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() set
{1} is non empty trivial finite V49() 1 -element V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() set
{{1,1},{1}} is non empty finite V49() set
{[1,1]} is Relation-like Function-like constant non empty trivial finite 1 -element set
<*0*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing finite 1 -element FinSequence-like FinSubsequence-like Function-yielding V156() V157() set
[1,0] is set
{1,0} is non empty finite V49() V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() set
{{1,0},{1}} is non empty finite V49() set
{[1,0]} is Relation-like Function-like constant non empty trivial finite 1 -element set
K142(<*1*>,<*0*>) is Relation-like NAT -defined NAT -defined Function-like non empty complex-valued ext-real-valued real-valued finite K107(1,1) -element FinSequence-like FinSubsequence-like set
K107(1,1) is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT
K610(K608()) is non empty strict SubSpace of K607(2)
the carrier of K610(K608()) is non empty set
].0,1.[ is non empty V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
R^1 ].0,1.[ is non empty V126() V127() V128() open Element of K19( the carrier of K598())
K598() | (R^1 ].0,1.[) is strict V241() SubSpace of K598()
the carrier of (K598() | (R^1 ].0,1.[)) is V126() V127() V128() set
K20( the carrier of K610(K608()), the carrier of (K598() | (R^1 ].0,1.[))) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20( the carrier of K610(K608()), the carrier of (K598() | (R^1 ].0,1.[)))) is set
K609() is Element of the carrier of K607(2)
- 1 is non empty ext-real non positive negative complex real Element of REAL
|[(- 1),0]| is Relation-like NAT -defined NAT -defined REAL -valued Function-like non empty complex-valued ext-real-valued real-valued finite 2 -element 2 -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL 2)
<*(- 1)*> is Relation-like NAT -defined Function-like one-to-one constant non empty trivial complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing finite 1 -element FinSequence-like FinSubsequence-like set
[1,(- 1)] is set
{1,(- 1)} is non empty finite V126() V127() V128() V302() V303() V304() V305() V306() set
{{1,(- 1)},{1}} is non empty finite V49() set
{[1,(- 1)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
K142(<*(- 1)*>,<*0*>) is Relation-like NAT -defined NAT -defined Function-like non empty complex-valued ext-real-valued real-valued finite K107(1,1) -element FinSequence-like FinSubsequence-like set
K610(K609()) is non empty strict SubSpace of K607(2)
the carrier of K610(K609()) is non empty set
1 / 2 is non empty ext-real positive non negative complex real Element of REAL
2 " is non empty ext-real positive non negative complex real set
1 * (2 ") is non empty ext-real positive non negative complex real set
3 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT
3 / 2 is non empty ext-real positive non negative complex real Element of REAL
3 * (2 ") is non empty ext-real positive non negative complex real set
].(1 / 2),(3 / 2).[ is non empty V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
R^1 ].(1 / 2),(3 / 2).[ is non empty V126() V127() V128() open Element of K19( the carrier of K598())
K598() | (R^1 ].(1 / 2),(3 / 2).[) is strict V241() SubSpace of K598()
the carrier of (K598() | (R^1 ].(1 / 2),(3 / 2).[)) is V126() V127() V128() set
K20( the carrier of K610(K609()), the carrier of (K598() | (R^1 ].(1 / 2),(3 / 2).[))) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20( the carrier of K610(K609()), the carrier of (K598() | (R^1 ].(1 / 2),(3 / 2).[)))) is set
K687() is set
{{}} is functional non empty trivial finite V49() 1 -element V126() V127() V128() V129() V130() V131() complex-functions-membered V302() V303() V304() V305() V306() set
{{}} * is functional non empty FinSequence-membered FinSequenceSet of {{}}
K20(({{}} *),{{}}) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(({{}} *),{{}})) is set
PFuncs (({{}} *),{{}}) is functional complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered set
K20(COMPLEX,COMPLEX) is Relation-like complex-valued set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(RAT,RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(K20(NAT,NAT),NAT)) is set
K20(COMPLEX,REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(COMPLEX,REAL)) is set
REAL 0 is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
0 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = 0 } is set
TOP-REAL 0 is non empty V83() constituted-Functions constituted-FinSeqs TopSpace-like V198() V199() V200() V201() V202() V203() V204() V210() L16()
K157((TOP-REAL 0)) is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered zero V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() Element of the carrier of (TOP-REAL 0)
the carrier of (TOP-REAL 0) is non empty set
{K157((TOP-REAL 0))} is functional non empty trivial finite V49() 1 -element V126() V127() V128() V129() V130() V131() complex-functions-membered V302() V303() V304() V305() V306() set
the carrier of R^1 is non empty V126() V127() V128() set
K19( the carrier of R^1) is set
product {} is set
n is ext-real complex real set
J is ext-real non positive complex real set
n - J is ext-real complex real set
- J is ext-real non negative complex real set
n + (- J) is ext-real complex real set
n + J is ext-real complex real set
].(n - J),(n + J).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
[.(n - J),(n + J).[ is V126() V127() V128() V303() V307() Element of K19(REAL)
].(n - J),(n + J).] is V126() V127() V128() V302() V307() Element of K19(REAL)
n is ext-real complex real set
J is non empty ext-real non positive negative complex real set
n - J is ext-real complex real set
- J is non empty ext-real positive non negative complex real set
n + (- J) is ext-real complex real set
n + J is ext-real complex real set
[.(n - J),(n + J).] is V126() V127() V128() closed V307() Element of K19(REAL)
n is ext-real non negative ordinal natural complex real finite cardinal set
J is Relation-like NAT -defined Function-like complex-valued finite n -element FinSequence-like FinSubsequence-like set
- J is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set
- 1 is non empty ext-real non positive negative complex real set
(- 1) (#) J is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set
dom (- J) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
len (- J) is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
J " is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set
dom (J ") is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
len (J ") is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
J ^2 is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set
J (#) J is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set
dom (J ^2) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
len (J ^2) is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
|.J.| is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like set
dom |.J.| is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
len |.J.| is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
PP is Relation-like NAT -defined Function-like complex-valued finite n -element FinSequence-like FinSubsequence-like set
J + PP is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set
dom (J + PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom PP is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(dom J) /\ (dom PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
len PP is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
len (J + PP) is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
J - PP is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set
- PP is Relation-like NAT -defined Function-like complex-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) PP is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set
J + (- PP) is Relation-like NAT -defined Function-like complex-valued finite n -element FinSequence-like FinSubsequence-like set
J (#) PP is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set
dom (J (#) PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom PP is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(dom J) /\ (dom PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
len PP is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
len (J (#) PP) is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
J /" PP is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set
PP " is Relation-like NAT -defined Function-like complex-valued finite n -element FinSequence-like FinSubsequence-like set
J (#) (PP ") is Relation-like NAT -defined Function-like complex-valued finite n -element FinSequence-like FinSubsequence-like set
J is ext-real non negative ordinal natural complex real finite cardinal set
PP is Relation-like NAT -defined Function-like complex-valued finite J -element FinSequence-like FinSubsequence-like set
n is complex set
n + PP is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set
dom (n + PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom PP is finite J -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
len PP is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
len (n + PP) is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
PP - n is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set
- n is complex set
(- n) + PP is Relation-like NAT -defined Function-like complex-valued finite J -element FinSequence-like FinSubsequence-like set
n (#) PP is Relation-like NAT -defined Function-like complex-valued finite FinSequence-like FinSubsequence-like set
dom (n (#) PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom PP is finite J -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
len PP is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
len (n (#) PP) is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
n is Relation-like Function-like complex-valued ext-real-valued real-valued set
{n} is functional non empty trivial finite 1 -element complex-functions-membered set
J is set
J is Relation-like Function-like complex-valued ext-real-valued real-valued set
{n,J} is functional non empty finite set
PP is set
n is ext-real non negative ordinal natural complex real finite cardinal set
C is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like set
J is set
PP is set
C +* (J,PP) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (C +* (J,PP)) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom C is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
len (C +* (J,PP)) is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
len C is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
n is ext-real non negative ordinal natural complex real finite cardinal set
J is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like set
dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
Seg 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal 0 -element {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set
len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
n is ext-real non negative ordinal natural complex real finite cardinal set
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
J is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
rng J is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)
len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
n is Relation-like Function-like complex-valued set
J is Relation-like Function-like complex-valued set
n - J is Relation-like Function-like complex-valued set
- J is Relation-like Function-like complex-valued set
(- 1) (#) J is Relation-like Function-like complex-valued set
n + (- J) is Relation-like Function-like complex-valued set
|.(n - J).| is Relation-like Function-like complex-valued ext-real-valued real-valued set
J - n is Relation-like Function-like complex-valued set
- n is Relation-like Function-like complex-valued set
(- 1) (#) n is Relation-like Function-like complex-valued set
J + (- n) is Relation-like Function-like complex-valued set
|.(J - n).| is Relation-like Function-like complex-valued ext-real-valued real-valued set
- (J - n) is Relation-like Function-like complex-valued set
(- 1) (#) (J - n) is Relation-like Function-like complex-valued set
n is ext-real non negative ordinal natural complex real finite cardinal set
J is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
J - PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
J + (- PP) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
abs (J - PP) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
absreal is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(J - PP) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set
rng (abs (J - PP)) is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)
sup (rng (abs (J - PP))) is ext-real set
{(sup (rng (abs (J - PP))))} is non empty trivial finite 1 -element V127() V302() V303() set
(abs (J - PP)) " {(sup (rng (abs (J - PP))))} is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
the ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (J - PP)) " {(sup (rng (abs (J - PP))))} is ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (J - PP)) " {(sup (rng (abs (J - PP))))}
C is ext-real non negative ordinal natural complex real finite cardinal set
T is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
E is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
T - E is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- E is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) E is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
T + (- E) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
abs (T - E) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
(T - E) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set
rng (abs (T - E)) is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)
sup (rng (abs (T - E))) is ext-real set
{(sup (rng (abs (T - E))))} is non empty trivial finite 1 -element V127() V302() V303() set
(abs (T - E)) " {(sup (rng (abs (T - E))))} is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
the ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (T - E)) " {(sup (rng (abs (T - E))))} is ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (T - E)) " {(sup (rng (abs (T - E))))}
E - T is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- T is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) T is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
E + (- T) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
abs (E - T) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
(E - T) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set
rng (abs (E - T)) is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)
sup (rng (abs (E - T))) is ext-real set
{(sup (rng (abs (E - T))))} is non empty trivial finite 1 -element V127() V302() V303() set
(abs (E - T)) " {(sup (rng (abs (E - T))))} is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
the ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (E - T)) " {(sup (rng (abs (E - T))))} is ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (E - T)) " {(sup (rng (abs (E - T))))}
n is ext-real non negative ordinal natural complex real finite cardinal set
J is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(n,J,PP) is ext-real non negative ordinal natural complex real finite cardinal set
J - PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
J + (- PP) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
abs (J - PP) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
(J - PP) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set
rng (abs (J - PP)) is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)
sup (rng (abs (J - PP))) is ext-real set
{(sup (rng (abs (J - PP))))} is non empty trivial finite 1 -element V127() V302() V303() set
(abs (J - PP)) " {(sup (rng (abs (J - PP))))} is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
the ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (J - PP)) " {(sup (rng (abs (J - PP))))} is ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (J - PP)) " {(sup (rng (abs (J - PP))))}
Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
dom (abs (J - PP)) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
n is set
J is ext-real non negative ordinal natural complex real finite cardinal set
PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite J -element FinSequence-like FinSubsequence-like set
C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite J -element FinSequence-like FinSubsequence-like set
PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite J -element FinSequence-like FinSubsequence-like FinSequence of REAL
- C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite J -element FinSequence-like FinSubsequence-like set
(- 1) (#) C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite J -element FinSequence-like FinSubsequence-like set
PP + (- C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite J -element FinSequence-like FinSubsequence-like set
abs (PP - C) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite J -element FinSequence-like FinSubsequence-like FinSequence of REAL
(PP - C) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set
(abs (PP - C)) . n is ext-real complex real set
(J,PP,C) is ext-real non negative ordinal natural complex real finite cardinal set
rng (abs (PP - C)) is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)
sup (rng (abs (PP - C))) is ext-real set
{(sup (rng (abs (PP - C))))} is non empty trivial finite 1 -element V127() V302() V303() set
(abs (PP - C)) " {(sup (rng (abs (PP - C))))} is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
the ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (PP - C)) " {(sup (rng (abs (PP - C))))} is ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (PP - C)) " {(sup (rng (abs (PP - C))))}
(abs (PP - C)) . (J,PP,C) is ext-real complex real set
dom (abs (PP - C)) is finite J -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom (PP - C) is finite J -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom PP is finite J -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom C is finite J -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(dom PP) /\ (dom C) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
Seg J is finite J -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= J ) } is set
(PP - C) . (J,PP,C) is ext-real complex real set
abs ((PP - C) . (J,PP,C)) is ext-real non negative complex real Element of REAL
Euclid 0 is non empty strict Reflexive discerning V192() triangle MetrStruct
Pitag_dist 0 is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL 0),(REAL 0)),REAL))
K20((REAL 0),(REAL 0)) is Relation-like set
K20(K20((REAL 0),(REAL 0)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL 0),(REAL 0)),REAL)) is set
MetrStruct(# (REAL 0),(Pitag_dist 0) #) is strict MetrStruct
TopSpaceMetr (Euclid 0) is non empty strict TopSpace-like TopStruct
the carrier of (Euclid 0) is non empty set
Family_open_set (Euclid 0) is Element of K19(K19( the carrier of (Euclid 0)))
K19( the carrier of (Euclid 0)) is set
K19(K19( the carrier of (Euclid 0))) is set
TopStruct(# the carrier of (Euclid 0),(Family_open_set (Euclid 0)) #) is strict TopStruct
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is Element of the carrier of (Euclid n)
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
PP is set
rng J is finite set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
{{},{{}}} is non empty finite V49() set
the topology of (TOP-REAL 0) is Element of K19(K19( the carrier of (TOP-REAL 0)))
K19( the carrier of (TOP-REAL 0)) is set
K19(K19( the carrier of (TOP-REAL 0))) is set
TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #) is strict TopStruct
n is Element of K19( the carrier of (Euclid 0))
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
PP is ext-real non positive complex real set
Ball (J,PP) is Element of K19( the carrier of (Euclid n))
K19( the carrier of (Euclid n)) is set
C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
dist (C,J) is ext-real complex real Element of REAL
the distance of (Euclid n) is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20( the carrier of (Euclid n), the carrier of (Euclid n)),REAL))
K20( the carrier of (Euclid n), the carrier of (Euclid n)) is Relation-like set
K20(K20( the carrier of (Euclid n), the carrier of (Euclid n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20( the carrier of (Euclid n), the carrier of (Euclid n)),REAL)) is set
the distance of (Euclid n) . (C,J) is ext-real complex real Element of REAL
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
PP is non empty ext-real positive non negative complex real set
Ball (J,PP) is Element of K19( the carrier of (Euclid n))
K19( the carrier of (Euclid n)) is set
n is ext-real non negative ordinal natural complex real finite cardinal set
TOP-REAL n is non empty V83() constituted-Functions constituted-FinSeqs TopSpace-like V198() V199() V200() V201() V202() V203() V204() V210() L16()
the carrier of (TOP-REAL n) is non empty set
J is ext-real non negative ordinal natural complex real finite cardinal set
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)
dom PP is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
PP /. J is ext-real complex real Element of REAL
C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)
C /. J is ext-real complex real Element of REAL
(PP /. J) - (C /. J) is ext-real complex real Element of REAL
- (C /. J) is ext-real complex real set
(PP /. J) + (- (C /. J)) is ext-real complex real set
((PP /. J) - (C /. J)) ^2 is ext-real complex real Element of REAL
((PP /. J) - (C /. J)) * ((PP /. J) - (C /. J)) is ext-real non negative complex real set
PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)
PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
PP + (- C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
sqr (PP - C) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
(PP - C) (#) (PP - C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
Sum (sqr (PP - C)) is ext-real complex real Element of REAL
E is ext-real non negative ordinal natural complex real finite cardinal set
dom (sqr (PP - C)) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(sqr (PP - C)) . E is ext-real complex real set
(PP - C) . E is ext-real complex real set
((PP - C) . E) ^2 is ext-real complex real set
((PP - C) . E) * ((PP - C) . E) is ext-real non negative complex real set
dom (PP - C) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom C is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(dom PP) /\ (dom C) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
PP . J is ext-real complex real set
C . J is ext-real complex real set
(sqr (PP - C)) . J is ext-real complex real set
(PP - C) . J is ext-real complex real set
((PP - C) . J) ^2 is ext-real complex real set
((PP - C) . J) * ((PP - C) . J) is ext-real non negative complex real set
n is ext-real non negative ordinal natural complex real finite cardinal set
TOP-REAL n is non empty V83() constituted-Functions constituted-FinSeqs TopSpace-like V198() V199() V200() V201() V202() V203() V204() V210() L16()
the carrier of (TOP-REAL n) is non empty set
J is ext-real complex real set
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)
C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)
Ball (C,J) is open Element of K19( the carrier of (TOP-REAL n))
K19( the carrier of (TOP-REAL n)) is set
PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)
PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
PP + (- C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
|.(PP - C).| is ext-real non negative complex real Element of REAL
sqr (PP - C) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
(PP - C) (#) (PP - C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
Sum (sqr (PP - C)) is ext-real complex real Element of REAL
sqrt (Sum (sqr (PP - C))) is ext-real complex real Element of REAL
(sqrt (Sum (sqr (PP - C)))) ^2 is ext-real complex real Element of REAL
(sqrt (Sum (sqr (PP - C)))) * (sqrt (Sum (sqr (PP - C)))) is ext-real non negative complex real set
J ^2 is ext-real complex real set
J * J is ext-real non negative complex real set
C - PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)
C - PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
C + (- PP) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
sqr (C - PP) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
(C - PP) (#) (C - PP) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
E is set
(PP - C) . E is ext-real complex real set
abs ((PP - C) . E) is ext-real non negative complex real Element of REAL
PP . E is ext-real complex real set
C . E is ext-real complex real set
(PP . E) - (C . E) is ext-real complex real set
- (C . E) is ext-real complex real set
(PP . E) + (- (C . E)) is ext-real complex real set
abs ((PP . E) - (C . E)) is ext-real non negative complex real Element of REAL
dom (PP - C) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom PP is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom C is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(dom PP) /\ (dom C) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
x is ext-real non negative ordinal natural complex real finite cardinal set
(PP - C) . x is ext-real complex real set
PP . x is ext-real complex real set
C . x is ext-real complex real set
(PP . x) - (C . x) is ext-real complex real set
- (C . x) is ext-real complex real set
(PP . x) + (- (C . x)) is ext-real complex real set
PP /. x is ext-real complex real Element of REAL
C /. x is ext-real complex real Element of REAL
(C . x) - (PP . x) is ext-real complex real set
- (PP . x) is ext-real complex real set
(C . x) + (- (PP . x)) is ext-real complex real set
((C . x) - (PP . x)) ^2 is ext-real complex real set
((C . x) - (PP . x)) * ((C . x) - (PP . x)) is ext-real non negative complex real set
(C /. x) - (PP /. x) is ext-real complex real Element of REAL
- (PP /. x) is ext-real complex real set
(C /. x) + (- (PP /. x)) is ext-real complex real set
((C /. x) - (PP /. x)) ^2 is ext-real complex real Element of REAL
((C /. x) - (PP /. x)) * ((C /. x) - (PP /. x)) is ext-real non negative complex real set
Sum (sqr (C - PP)) is ext-real complex real Element of REAL
(C . x) - J is ext-real complex real set
- J is ext-real complex real set
(C . x) + (- J) is ext-real complex real set
((PP . x) - (C . x)) ^2 is ext-real complex real set
((PP . x) - (C . x)) * ((PP . x) - (C . x)) is ext-real non negative complex real set
(PP /. x) - (C /. x) is ext-real complex real Element of REAL
- (C /. x) is ext-real complex real set
(PP /. x) + (- (C /. x)) is ext-real complex real set
((PP /. x) - (C /. x)) ^2 is ext-real complex real Element of REAL
((PP /. x) - (C /. x)) * ((PP /. x) - (C /. x)) is ext-real non negative complex real set
(C . x) + J is ext-real complex real set
abs (PP - C) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
(PP - C) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set
dom (abs (PP - C)) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(abs (PP - C)) . E is ext-real complex real set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is ext-real complex real set
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
Ball (C,J) is Element of K19( the carrier of (Euclid n))
K19( the carrier of (Euclid n)) is set
PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
PP + (- C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
TOP-REAL n is non empty V83() constituted-Functions constituted-FinSeqs TopSpace-like V198() V199() V200() V201() V202() V203() V204() V210() L16()
the carrier of (TOP-REAL n) is non empty set
E is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)
Ball (E,J) is open Element of K19( the carrier of (TOP-REAL n))
K19( the carrier of (TOP-REAL n)) is set
T is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)
T - E is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (TOP-REAL n)
T - E is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- E is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) E is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
T + (- E) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
x is set
(PP - C) . x is ext-real complex real set
abs ((PP - C) . x) is ext-real non negative complex real Element of REAL
i is set
PP . i is ext-real complex real set
C . i is ext-real complex real set
(PP . i) - (C . i) is ext-real complex real set
- (C . i) is ext-real complex real set
(PP . i) + (- (C . i)) is ext-real complex real set
abs ((PP . i) - (C . i)) is ext-real non negative complex real Element of REAL
n is Relation-like Function-like complex-valued ext-real-valued real-valued set
dom n is set
J is ext-real complex real set
PP is Relation-like Function-like set
dom PP is set
PP is Relation-like Function-like set
dom PP is set
C is Relation-like Function-like set
dom C is set
T is set
PP . T is set
n . T is ext-real complex real set
(n . T) - J is ext-real complex real set
- J is ext-real complex real set
(n . T) + (- J) is ext-real complex real set
(n . T) + J is ext-real complex real set
].((n . T) - J),((n . T) + J).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
C . T is set
n is ext-real complex real set
({},n) is Relation-like Function-like set
dom ({},n) is set
dom {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() Element of K19(NAT)
n is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like set
J is ext-real complex real set
(n,J) is Relation-like Function-like set
len n is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
dom (n,J) is set
Seg (len n) is finite len n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= len n ) } is set
dom n is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
PP is ext-real complex real set
(J,PP) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (J,PP) is set
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
E is set
dom (J,PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
x is Relation-like Function-like set
dom x is set
dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng i is finite set
R is set
dom i is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
V is set
i . V is set
x . V is set
(J,PP) . V is set
J . V is ext-real complex real set
(J . V) - PP is ext-real complex real set
- PP is ext-real complex real set
(J . V) + (- PP) is ext-real complex real set
(J . V) + PP is ext-real complex real set
].((J . V) - PP),((J . V) + PP).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
len J is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
len i is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is ext-real complex real set
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
(n,PP,J) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
(PP,J) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (PP,J) is set
dom (PP,J) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom PP is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
T is set
(PP,J) . T is set
PP . T is ext-real complex real set
(PP . T) - J is ext-real complex real set
- J is ext-real complex real set
(PP . T) + (- J) is ext-real complex real set
(PP . T) + J is ext-real complex real set
].((PP . T) - J),((PP . T) + J).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
(PP . T) - 0 is ext-real complex real Element of REAL
- 0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() set
(PP . T) + (- 0) is ext-real complex real set
(PP . T) + 0 is ext-real complex real Element of REAL
n is non empty ext-real positive non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
PP is ext-real non positive complex real set
(n,J,PP) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
(J,PP) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (J,PP) is set
C is set
dom (J,PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom J is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
Seg n is non empty finite n -element V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
x is set
(J,PP) . x is set
T is Relation-like Function-like complex-valued ext-real-valued real-valued set
T . x is ext-real complex real set
(T . x) - PP is ext-real complex real set
- PP is ext-real non negative complex real set
(T . x) + (- PP) is ext-real complex real set
(T . x) + PP is ext-real complex real set
].((T . x) - PP),((T . x) + PP).[ is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued open V302() V303() V304() V305() V306() V307() Element of K19(REAL)
J is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() Element of the carrier of (Euclid 0)
n is ext-real complex real set
(0,J,n) is finite Element of K19( the carrier of (TopSpaceMetr (Euclid 0)))
the carrier of (TopSpaceMetr (Euclid 0)) is non empty trivial finite 1 -element set
K19( the carrier of (TopSpaceMetr (Euclid 0))) is finite V49() set
(J,n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (J,n) is set
n is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() Element of the carrier of (Euclid 0)
J is ext-real complex real set
(0,n,J) is finite Element of K19( the carrier of (TopSpaceMetr (Euclid 0)))
the carrier of (TopSpaceMetr (Euclid 0)) is non empty trivial finite 1 -element set
K19( the carrier of (TopSpaceMetr (Euclid 0))) is finite V49() set
(n,J) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (n,J) is set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
PP is non empty ext-real positive non negative complex real set
(n,J,PP) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
(J,PP) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (J,PP) is set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is ext-real complex real set
PP is ext-real complex real set
C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
(n,C,J) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
(C,J) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (C,J) is set
(n,C,PP) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(C,PP) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (C,PP) is set
dom (C,PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom C is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom (C,J) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
T is set
C . T is ext-real complex real set
(C,J) . T is set
E is ext-real complex real set
E - J is ext-real complex real set
- J is ext-real complex real set
E + (- J) is ext-real complex real set
E + J is ext-real complex real set
].(E - J),(E + J).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
(C,PP) . T is set
E - PP is ext-real complex real set
- PP is ext-real complex real set
E + (- PP) is ext-real complex real set
E + PP is ext-real complex real set
].(E - PP),(E + PP).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is ext-real complex real set
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
(n,C,J) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
(C,J) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (C,J) is set
PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
PP + (- C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
dom PP is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
dom C is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom (PP - C) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(dom PP) /\ (dom C) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
T is set
(PP - C) . T is ext-real complex real set
abs ((PP - C) . T) is ext-real non negative complex real Element of REAL
PP . T is ext-real complex real set
C . T is ext-real complex real set
(PP . T) - (C . T) is ext-real complex real set
- (C . T) is ext-real complex real set
(PP . T) + (- (C . T)) is ext-real complex real set
abs ((PP . T) - (C . T)) is ext-real non negative complex real Element of REAL
dom (C,J) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(C,J) . T is set
(C . T) - J is ext-real complex real set
- J is ext-real complex real set
(C . T) + (- J) is ext-real complex real set
(C . T) + J is ext-real complex real set
].((C . T) - J),((C . T) + J).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
abs (PP - C) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
(PP - C) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set
dom (abs (PP - C)) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(abs (PP - C)) . T is ext-real complex real set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is ext-real complex real set
J ^2 is ext-real complex real set
J * J is ext-real non negative complex real set
n * (J ^2) is ext-real complex real set
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
(n,C,J) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
(C,J) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (C,J) is set
PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
PP + (- C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
sqr (PP - C) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
(PP - C) (#) (PP - C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
Sum (sqr (PP - C)) is ext-real complex real Element of REAL
n |-> (J ^2) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
(Seg n) --> (J ^2) is Relation-like Seg n -defined Seg n -defined Function-like constant total total quasi_total complex-valued ext-real-valued real-valued finite FinSequence-like FinSubsequence-like Element of K19(K20((Seg n),{(J ^2)}))
{(J ^2)} is non empty trivial finite 1 -element V126() V127() V128() V302() V303() V304() V305() V306() set
K20((Seg n),{(J ^2)}) is Relation-like complex-valued ext-real-valued real-valued finite set
K19(K20((Seg n),{(J ^2)})) is finite V49() set
x is ext-real non negative ordinal natural complex real finite cardinal set
dom PP is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom C is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom (PP - C) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(dom PP) /\ (dom C) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(PP - C) . x is ext-real complex real set
PP . x is ext-real complex real set
C . x is ext-real complex real set
(PP . x) - (C . x) is ext-real complex real set
- (C . x) is ext-real complex real set
(PP . x) + (- (C . x)) is ext-real complex real set
(sqr (PP - C)) . x is ext-real complex real set
((PP - C) . x) ^2 is ext-real complex real set
((PP - C) . x) * ((PP - C) . x) is ext-real non negative complex real set
(n |-> (J ^2)) . x is ext-real complex real set
abs ((PP . x) - (C . x)) is ext-real non negative complex real Element of REAL
abs ((PP - C) . x) is ext-real non negative complex real Element of REAL
(abs ((PP - C) . x)) ^2 is ext-real complex real Element of REAL
(abs ((PP - C) . x)) * (abs ((PP - C) . x)) is ext-real non negative complex real set
x is ext-real non negative ordinal natural complex real finite cardinal set
(sqr (PP - C)) . x is ext-real complex real set
(n |-> (J ^2)) . x is ext-real complex real set
x is set
i is ext-real non negative ordinal natural complex real finite cardinal set
(n |-> (J ^2)) . i is ext-real complex real set
(sqr (PP - C)) . i is ext-real complex real set
Sum (n |-> (J ^2)) is ext-real complex real set
x is ext-real non negative ordinal natural complex real finite cardinal set
(n |-> (J ^2)) . x is ext-real complex real set
(sqr (PP - C)) . x is ext-real complex real set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
sqrt n is ext-real non negative complex real set
J is ext-real complex real set
J * (sqrt n) is ext-real complex real set
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
(n,C,J) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
(C,J) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (C,J) is set
dist (PP,C) is ext-real complex real Element of REAL
the distance of (Euclid n) is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20( the carrier of (Euclid n), the carrier of (Euclid n)),REAL))
K20( the carrier of (Euclid n), the carrier of (Euclid n)) is Relation-like set
K20(K20( the carrier of (Euclid n), the carrier of (Euclid n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20( the carrier of (Euclid n), the carrier of (Euclid n)),REAL)) is set
the distance of (Euclid n) . (PP,C) is ext-real complex real Element of REAL
PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
PP + (- C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
|.(PP - C).| is ext-real non negative complex real Element of REAL
sqr (PP - C) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
(PP - C) (#) (PP - C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
Sum (sqr (PP - C)) is ext-real complex real Element of REAL
sqrt (Sum (sqr (PP - C))) is ext-real complex real Element of REAL
J ^2 is ext-real complex real set
J * J is ext-real non negative complex real set
n * (J ^2) is ext-real complex real set
sqrt (n * (J ^2)) is ext-real complex real set
sqrt (J ^2) is ext-real complex real set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
sqrt n is ext-real non negative complex real set
J is ext-real complex real set
J / (sqrt n) is ext-real complex real Element of COMPLEX
(sqrt n) " is ext-real non negative complex real set
J * ((sqrt n) ") is ext-real complex real set
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
(n,PP,(J / (sqrt n))) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
(PP,(J / (sqrt n))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (PP,(J / (sqrt n))) is set
Ball (PP,J) is Element of K19( the carrier of (Euclid n))
C is set
(J / (sqrt n)) * (sqrt n) is ext-real complex real set
T is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
dist (T,PP) is ext-real complex real Element of REAL
the distance of (Euclid n) is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20( the carrier of (Euclid n), the carrier of (Euclid n)),REAL))
K20( the carrier of (Euclid n), the carrier of (Euclid n)) is Relation-like set
K20(K20( the carrier of (Euclid n), the carrier of (Euclid n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20( the carrier of (Euclid n), the carrier of (Euclid n)),REAL)) is set
the distance of (Euclid n) . (T,PP) is ext-real complex real Element of REAL
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
sqrt n is ext-real non negative complex real set
J is ext-real complex real set
J * (sqrt n) is ext-real complex real set
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
(n,PP,J) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
(PP,J) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (PP,J) is set
Ball (PP,(J * (sqrt n))) is Element of K19( the carrier of (Euclid n))
(J * (sqrt n)) / (sqrt n) is ext-real complex real Element of COMPLEX
(sqrt n) " is ext-real non negative complex real set
(J * (sqrt n)) * ((sqrt n) ") is ext-real complex real set
(n,PP,((J * (sqrt n)) / (sqrt n))) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(PP,((J * (sqrt n)) / (sqrt n))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (PP,((J * (sqrt n)) / (sqrt n))) is set
J / (sqrt n) is ext-real complex real Element of COMPLEX
J * ((sqrt n) ") is ext-real complex real set
(J / (sqrt n)) * (sqrt n) is ext-real complex real set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is ext-real complex real set
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
Ball (C,J) is Element of K19( the carrier of (Euclid n))
K19( the carrier of (Euclid n)) is set
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
T is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
E is ext-real complex real set
Ball (PP,E) is Element of K19( the carrier of (Euclid n))
sqrt n is ext-real non negative complex real set
E / (sqrt n) is ext-real complex real Element of COMPLEX
(sqrt n) " is ext-real non negative complex real set
E * ((sqrt n) ") is ext-real complex real set
x is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
1 / x is ext-real non negative complex real Element of COMPLEX
x " is ext-real non negative complex real set
1 * (x ") is ext-real non negative complex real set
(n,PP,(E / (sqrt n))) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(PP,(E / (sqrt n))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (PP,(E / (sqrt n))) is set
i is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT
1 / i is non empty ext-real positive non negative complex real Element of COMPLEX
i " is non empty ext-real positive non negative complex real set
1 * (i ") is non empty ext-real positive non negative complex real set
(n,PP,(1 / i)) is non empty Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(PP,(1 / i)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (PP,(1 / i)) is set
1 / 1 is non empty ext-real positive non negative complex real Element of COMPLEX
1 " is non empty ext-real positive non negative complex real set
1 * (1 ") is non empty ext-real positive non negative complex real set
(n,PP,(1 / 1)) is non empty Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(PP,(1 / 1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (PP,(1 / 1)) is set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is ext-real complex real set
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
(n,C,J) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
(C,J) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (C,J) is set
PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
PP + (- C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
abs (PP - C) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
(PP - C) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set
(n,PP,C) is ext-real non negative ordinal natural complex real finite cardinal set
rng (abs (PP - C)) is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)
sup (rng (abs (PP - C))) is ext-real set
{(sup (rng (abs (PP - C))))} is non empty trivial finite 1 -element V127() V302() V303() set
(abs (PP - C)) " {(sup (rng (abs (PP - C))))} is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
the ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (PP - C)) " {(sup (rng (abs (PP - C))))} is ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (PP - C)) " {(sup (rng (abs (PP - C))))}
(abs (PP - C)) . (n,PP,C) is ext-real complex real set
(PP - C) . (n,PP,C) is ext-real complex real set
abs ((PP - C) . (n,PP,C)) is ext-real non negative complex real Element of REAL
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is ext-real complex real set
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
PP - C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) C is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
PP + (- C) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
abs (PP - C) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
(PP - C) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set
(n,PP,C) is ext-real non negative ordinal natural complex real finite cardinal set
rng (abs (PP - C)) is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)
sup (rng (abs (PP - C))) is ext-real set
{(sup (rng (abs (PP - C))))} is non empty trivial finite 1 -element V127() V302() V303() set
(abs (PP - C)) " {(sup (rng (abs (PP - C))))} is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
the ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (PP - C)) " {(sup (rng (abs (PP - C))))} is ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (PP - C)) " {(sup (rng (abs (PP - C))))}
(abs (PP - C)) . (n,PP,C) is ext-real complex real set
J - ((abs (PP - C)) . (n,PP,C)) is ext-real complex real set
- ((abs (PP - C)) . (n,PP,C)) is ext-real complex real set
J + (- ((abs (PP - C)) . (n,PP,C))) is ext-real complex real set
(n,PP,(J - ((abs (PP - C)) . (n,PP,C)))) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
(PP,(J - ((abs (PP - C)) . (n,PP,C)))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (PP,(J - ((abs (PP - C)) . (n,PP,C)))) is set
(n,C,J) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(C,J) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (C,J) is set
dom PP is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
dom C is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
i is Element of the carrier of (TopSpaceMetr (Euclid n))
R is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
dom R is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom (PP,(J - ((abs (PP - C)) . (n,PP,C)))) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom (C,J) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
V is set
(C,J) . V is set
C . V is ext-real complex real set
(C . V) - J is ext-real complex real set
- J is ext-real complex real set
(C . V) + (- J) is ext-real complex real set
(C . V) + J is ext-real complex real set
].((C . V) - J),((C . V) + J).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
(PP,(J - ((abs (PP - C)) . (n,PP,C)))) . V is set
PP . V is ext-real complex real set
(PP . V) - (J - ((abs (PP - C)) . (n,PP,C))) is ext-real complex real set
- (J - ((abs (PP - C)) . (n,PP,C))) is ext-real complex real set
(PP . V) + (- (J - ((abs (PP - C)) . (n,PP,C)))) is ext-real complex real set
(PP . V) + (J - ((abs (PP - C)) . (n,PP,C))) is ext-real complex real set
].((PP . V) - (J - ((abs (PP - C)) . (n,PP,C)))),((PP . V) + (J - ((abs (PP - C)) . (n,PP,C)))).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
R . V is ext-real complex real set
(R . V) - (PP . V) is ext-real complex real set
- (PP . V) is ext-real complex real set
(R . V) + (- (PP . V)) is ext-real complex real set
abs ((R . V) - (PP . V)) is ext-real non negative complex real Element of REAL
dom (PP - C) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(dom PP) /\ (dom C) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(PP . V) - (C . V) is ext-real complex real set
- (C . V) is ext-real complex real set
(PP . V) + (- (C . V)) is ext-real complex real set
abs ((PP . V) - (C . V)) is ext-real non negative complex real Element of REAL
(PP - C) . V is ext-real complex real set
abs ((PP - C) . V) is ext-real non negative complex real Element of REAL
(abs (PP - C)) . V is ext-real complex real set
(J - ((abs (PP - C)) . (n,PP,C))) + ((abs (PP - C)) . (n,PP,C)) is ext-real complex real set
(abs ((R . V) - (PP . V))) + (abs ((PP . V) - (C . V))) is ext-real non negative complex real Element of REAL
(R . V) - (C . V) is ext-real complex real set
(R . V) + (- (C . V)) is ext-real complex real set
abs ((R . V) - (C . V)) is ext-real non negative complex real Element of REAL
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is ext-real complex real set
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
Ball (PP,J) is Element of K19( the carrier of (Euclid n))
K19( the carrier of (Euclid n)) is set
(n,PP,J) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
(PP,J) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (PP,J) is set
C is set
dom (PP,J) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom PP is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
T is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
dom T is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
E is set
PP . E is ext-real complex real set
T . E is ext-real complex real set
(PP,J) . E is set
x is ext-real complex real Element of REAL
x - J is ext-real complex real Element of REAL
- J is ext-real complex real set
x + (- J) is ext-real complex real set
x + J is ext-real complex real Element of REAL
].(x - J),(x + J).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
T - PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) PP is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
T + (- PP) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
dom (T - PP) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(dom T) /\ (dom PP) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(T - PP) . E is ext-real complex real set
i is ext-real complex real Element of REAL
i - x is ext-real complex real Element of REAL
- x is ext-real complex real set
i + (- x) is ext-real complex real set
x + (i - x) is ext-real complex real Element of REAL
abs ((T - PP) . E) is ext-real non negative complex real Element of REAL
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
PP is ext-real complex real set
(n,J,PP) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
(J,PP) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (J,PP) is set
C is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
C - J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- J is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) J is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
C + (- J) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
abs (C - J) is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
(C - J) (#) absreal is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite set
(n,C,J) is ext-real non negative ordinal natural complex real finite cardinal set
rng (abs (C - J)) is finite V126() V127() V128() V304() V305() V306() Element of K19(REAL)
sup (rng (abs (C - J))) is ext-real set
{(sup (rng (abs (C - J))))} is non empty trivial finite 1 -element V127() V302() V303() set
(abs (C - J)) " {(sup (rng (abs (C - J))))} is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
the ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (C - J)) " {(sup (rng (abs (C - J))))} is ext-real non negative ordinal natural complex real V43() V44() finite cardinal Element of (abs (C - J)) " {(sup (rng (abs (C - J))))}
(abs (C - J)) . (n,C,J) is ext-real complex real set
PP - ((abs (C - J)) . (n,C,J)) is ext-real complex real set
- ((abs (C - J)) . (n,C,J)) is ext-real complex real set
PP + (- ((abs (C - J)) . (n,C,J))) is ext-real complex real set
E is ext-real complex real set
Ball (C,E) is Element of K19( the carrier of (Euclid n))
((abs (C - J)) . (n,C,J)) - ((abs (C - J)) . (n,C,J)) is ext-real complex real set
((abs (C - J)) . (n,C,J)) + (- ((abs (C - J)) . (n,C,J))) is ext-real complex real set
(n,C,E) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(C,E) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (C,E) is set
the topology of (TopSpaceMetr (Euclid 0)) is finite V49() Element of K19(K19( the carrier of (TopSpaceMetr (Euclid 0))))
K19(K19( the carrier of (TopSpaceMetr (Euclid 0)))) is finite V49() set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
the carrier of (Euclid n) is non empty set
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
J is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
C is ext-real complex real set
Ball (PP,C) is Element of K19( the carrier of (Euclid n))
T is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT
1 / T is non empty ext-real positive non negative complex real Element of COMPLEX
T " is non empty ext-real positive non negative complex real set
1 * (T ") is non empty ext-real positive non negative complex real set
(n,PP,(1 / T)) is non empty open Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(PP,(1 / T)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (PP,(1 / T)) is set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
the carrier of (Euclid n) is non empty set
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
J is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
PP is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
C is ext-real complex real set
(n,PP,C) is open Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(PP,C) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (PP,C) is set
Ball (PP,C) is Element of K19( the carrier of (Euclid n))
{ (a1,a2,(1 / b1)) where b1 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT : verum } is set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
{ (n,J,(1 / b1)) where b1 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT : verum } is set
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
K19(K19( the carrier of (TopSpaceMetr (Euclid n)))) is set
bool the carrier of (TopSpaceMetr (Euclid n)) is Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))
PP is set
C is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT
1 / C is non empty ext-real positive non negative complex real Element of COMPLEX
C " is non empty ext-real positive non negative complex real set
1 * (C ") is non empty ext-real positive non negative complex real set
(n,J,(1 / C)) is non empty open Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(J,(1 / C)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (J,(1 / C)) is set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
the carrier of (Euclid n) is non empty set
J is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
(n,J) is Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
K19(K19( the carrier of (TopSpaceMetr (Euclid n)))) is set
{ (n,J,(1 / b1)) where b1 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT : verum } is set
(n,J) is Element of the carrier of (TopSpaceMetr (Euclid n))
1 / 1 is non empty ext-real positive non negative complex real Element of COMPLEX
1 " is non empty ext-real positive non negative complex real set
1 * (1 ") is non empty ext-real positive non negative complex real set
(n,J,(1 / 1)) is non empty open Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(J,(1 / 1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (J,(1 / 1)) is set
C is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
T is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT
1 / T is non empty ext-real positive non negative complex real Element of COMPLEX
T " is non empty ext-real positive non negative complex real set
1 * (T ") is non empty ext-real positive non negative complex real set
(n,J,(1 / T)) is non empty open Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(J,(1 / T)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (J,(1 / T)) is set
C is set
T is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT
1 / T is non empty ext-real positive non negative complex real Element of COMPLEX
T " is non empty ext-real positive non negative complex real set
1 * (T ") is non empty ext-real positive non negative complex real set
(n,J,(1 / T)) is non empty open Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(J,(1 / T)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (J,(1 / T)) is set
Intersect (n,J) is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
C is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
T is ext-real complex real set
Ball (J,T) is Element of K19( the carrier of (Euclid n))
E is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT
1 / E is non empty ext-real positive non negative complex real Element of COMPLEX
E " is non empty ext-real positive non negative complex real set
1 * (E ") is non empty ext-real positive non negative complex real set
(n,J,(1 / E)) is non empty open Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(J,(1 / E)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (J,(1 / E)) is set
x is non empty open Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
{} --> R^1 is Relation-like non-empty empty-yielding {} -defined RAT -valued Function-like one-to-one constant functional empty total quasi_total ext-real non positive non negative ordinal T-Sequence-like natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V272() V287() TopStruct-yielding V304() V305() V306() V307() Element of K19(K20({},{R^1}))
{R^1} is non empty trivial finite 1 -element set
K20({},{R^1}) is Relation-like finite set
K19(K20({},{R^1})) is finite V49() set
Carrier ({} --> R^1) is Relation-like non-empty empty-yielding {} -defined RAT -valued Function-like one-to-one constant functional empty total ext-real non positive non negative ordinal natural complex complex-valued ext-real-valued real-valued natural-valued real finite finite-yielding V49() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V126() V127() V128() V129() V130() V131() V132() Function-yielding V156() V157() complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued V304() V305() V306() V307() set
product ({} --> R^1) is non empty constituted-Functions strict TopSpace-like TopStruct
the carrier of (product ({} --> R^1)) is non empty set
product (Carrier ({} --> R^1)) is set
{ the carrier of (TopSpaceMetr (Euclid 0))} is non empty trivial finite V49() 1 -element set
K19(K19( the carrier of (TopSpaceMetr (Euclid 0)))) is finite V49() set
n is ext-real non negative ordinal natural complex real finite cardinal set
Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
Funcs ((Seg n),REAL) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
(Seg n) --> R^1 is Relation-like Seg n -defined Seg n -defined Function-like constant total total quasi_total finite FinSequence-like FinSubsequence-like V272() V287() TopStruct-yielding Element of K19(K20((Seg n),{R^1}))
K20((Seg n),{R^1}) is Relation-like finite set
K19(K20((Seg n),{R^1})) is finite V49() set
Carrier ((Seg n) --> R^1) is Relation-like Seg n -defined Function-like total set
product (Carrier ((Seg n) --> R^1)) is set
dom (Carrier ((Seg n) --> R^1)) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19((Seg n))
K19((Seg n)) is finite V49() set
C is set
K20((Seg n),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20((Seg n),REAL)) is set
T is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued finite Element of K19(K20((Seg n),REAL))
dom T is finite set
E is set
((Seg n) --> R^1) . E is set
(Carrier ((Seg n) --> R^1)) . E is set
T . E is ext-real complex real set
x is 1-sorted
the carrier of x is set
C is set
T is Relation-like Function-like set
dom T is set
rng T is set
E is set
x is set
T . x is set
((Seg n) --> R^1) . x is set
(Carrier ((Seg n) --> R^1)) . x is set
i is 1-sorted
the carrier of i is set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
the carrier of (Euclid n) is non empty set
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
K19(K19( the carrier of (TopSpaceMetr (Euclid n)))) is set
Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
(Seg n) --> R^1 is Relation-like Seg n -defined Seg n -defined Function-like constant total total quasi_total finite FinSequence-like FinSubsequence-like V272() V287() TopStruct-yielding Element of K19(K20((Seg n),{R^1}))
K20((Seg n),{R^1}) is Relation-like finite set
K19(K20((Seg n),{R^1})) is finite V49() set
product_prebasis ((Seg n) --> R^1) is Element of K19(K19((product (Carrier ((Seg n) --> R^1)))))
Carrier ((Seg n) --> R^1) is Relation-like Seg n -defined Function-like total set
product (Carrier ((Seg n) --> R^1)) is set
K19((product (Carrier ((Seg n) --> R^1)))) is set
K19(K19((product (Carrier ((Seg n) --> R^1))))) is set
C is Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))
Funcs ((Seg n),REAL) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
dom (Carrier ((Seg n) --> R^1)) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19((Seg n))
K19((Seg n)) is finite V49() set
R is Element of the carrier of (TopSpaceMetr (Euclid n))
V is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
(n,V) is non empty open (n,V) -quasi_basis Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))
(n,V) is Element of the carrier of (TopSpaceMetr (Euclid n))
{ (n,V,(1 / b1)) where b1 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT : verum } is set
R is Relation-like the carrier of (TopSpaceMetr (Euclid n)) -defined Function-like total set
V is Element of the carrier of (TopSpaceMetr (Euclid n))
F is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
R . F is set
R . V is set
e is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
(n,e) is non empty open (n,e) -quasi_basis Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))
(n,e) is Element of the carrier of (TopSpaceMetr (Euclid n))
{ (n,e,(1 / b1)) where b1 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT : verum } is set
V is Relation-like the carrier of (TopSpaceMetr (Euclid n)) -defined Function-like total Neighborhood_System of TopSpaceMetr (Euclid n)
Union V is open quasi_basis Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))
rng V is set
union (rng V) is set
F is open quasi_basis Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))
FinMeetCl C is Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))
e is set
r is set
dom V is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
y is set
V . y is set
y is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
dom y is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
V . y is set
O is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
(n,O) is non empty open (n,O) -quasi_basis Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))
(n,O) is Element of the carrier of (TopSpaceMetr (Euclid n))
{ (n,O,(1 / b1)) where b1 is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT : verum } is set
O is non empty ext-real positive non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V302() V303() V304() V305() V306() Element of NAT
1 / O is non empty ext-real positive non negative complex real Element of COMPLEX
O " is non empty ext-real positive non negative complex real set
1 * (O ") is non empty ext-real positive non negative complex real set
(n,y,(1 / O)) is non empty open Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
(y,(1 / O)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
product (y,(1 / O)) is set
i is non empty finite set
{ H2(b1) where b1 is Element of i : S2[b1] } is set
bool the carrier of (TopSpaceMetr (Euclid n)) is Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))
a is set
N is Element of i
y . N is ext-real complex real set
(y . N) - (1 / O) is ext-real complex real set
- (1 / O) is non empty ext-real non positive negative complex real set
(y . N) + (- (1 / O)) is ext-real complex real set
(y . N) + (1 / O) is ext-real complex real set
].((y . N) - (1 / O)),((y . N) + (1 / O)).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
R^1 ].((y . N) - (1 / O)),((y . N) + (1 / O)).[ is V126() V127() V128() open Element of K19( the carrier of K598())
(Carrier ((Seg n) --> R^1)) +* (N,(R^1 ].((y . N) - (1 / O)),((y . N) + (1 / O)).[)) is Relation-like Function-like set
product ((Carrier ((Seg n) --> R^1)) +* (N,(R^1 ].((y . N) - (1 / O)),((y . N) + (1 / O)).[))) is set
q is set
dom ((Carrier ((Seg n) --> R^1)) +* (N,(R^1 ].((y . N) - (1 / O)),((y . N) + (1 / O)).[))) is set
a is Relation-like Function-like set
dom a is set
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng f is finite set
k is set
dom f is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
a is set
f . a is set
((Carrier ((Seg n) --> R^1)) +* (N,(R^1 ].((y . N) - (1 / O)),((y . N) + (1 / O)).[))) . a is set
(Carrier ((Seg n) --> R^1)) . a is set
((Seg n) --> R^1) . a is set
c26 is 1-sorted
the carrier of c26 is set
len f is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT
a is Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))
N is set
q is Element of i
y . q is ext-real complex real set
(y . q) - (1 / O) is ext-real complex real set
- (1 / O) is non empty ext-real non positive negative complex real set
(y . q) + (- (1 / O)) is ext-real complex real set
(y . q) + (1 / O) is ext-real complex real set
].((y . q) - (1 / O)),((y . q) + (1 / O)).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
R^1 ].((y . q) - (1 / O)),((y . q) + (1 / O)).[ is V126() V127() V128() open Element of K19( the carrier of K598())
(Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((y . q) - (1 / O)),((y . q) + (1 / O)).[)) is Relation-like Function-like set
product ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((y . q) - (1 / O)),((y . q) + (1 / O)).[))) is set
((Seg n) --> R^1) . q is set
N is set
y . N is ext-real complex real set
(y . N) - (1 / O) is ext-real complex real set
- (1 / O) is non empty ext-real non positive negative complex real set
(y . N) + (- (1 / O)) is ext-real complex real set
(y . N) + (1 / O) is ext-real complex real set
].((y . N) - (1 / O)),((y . N) + (1 / O)).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
R^1 ].((y . N) - (1 / O)),((y . N) + (1 / O)).[ is V126() V127() V128() open Element of K19( the carrier of K598())
(Carrier ((Seg n) --> R^1)) +* (N,(R^1 ].((y . N) - (1 / O)),((y . N) + (1 / O)).[)) is Relation-like Function-like set
product ((Carrier ((Seg n) --> R^1)) +* (N,(R^1 ].((y . N) - (1 / O)),((y . N) + (1 / O)).[))) is set
Intersect a is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
meet a is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
dom (y,(1 / O)) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
q is Element of i
y . q is ext-real complex real set
(y . q) - (1 / O) is ext-real complex real set
(y . q) + (- (1 / O)) is ext-real complex real set
(y . q) + (1 / O) is ext-real complex real set
].((y . q) - (1 / O)),((y . q) + (1 / O)).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
R^1 ].((y . q) - (1 / O)),((y . q) + (1 / O)).[ is V126() V127() V128() open Element of K19( the carrier of K598())
(Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((y . q) - (1 / O)),((y . q) + (1 / O)).[)) is Relation-like Function-like set
product ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((y . q) - (1 / O)),((y . q) + (1 / O)).[))) is set
a is set
f is Relation-like Function-like set
dom f is set
dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((y . q) - (1 / O)),((y . q) + (1 / O)).[))) is set
k is set
(y,(1 / O)) . k is set
y . k is ext-real complex real set
(y . k) - (1 / O) is ext-real complex real set
(y . k) + (- (1 / O)) is ext-real complex real set
(y . k) + (1 / O) is ext-real complex real set
].((y . k) - (1 / O)),((y . k) + (1 / O)).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
f . k is set
((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((y . q) - (1 / O)),((y . q) + (1 / O)).[))) . k is set
((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((y . q) - (1 / O)),((y . q) + (1 / O)).[))) . k is set
(Carrier ((Seg n) --> R^1)) . k is set
((Seg n) --> R^1) . k is set
a is 1-sorted
the carrier of a is set
q is set
q is Element of i
y . q is ext-real complex real set
(y . q) - (1 / O) is ext-real complex real set
(y . q) + (- (1 / O)) is ext-real complex real set
(y . q) + (1 / O) is ext-real complex real set
].((y . q) - (1 / O)),((y . q) + (1 / O)).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
R^1 ].((y . q) - (1 / O)),((y . q) + (1 / O)).[ is V126() V127() V128() open Element of K19( the carrier of K598())
(Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((y . q) - (1 / O)),((y . q) + (1 / O)).[)) is Relation-like Function-like set
product ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((y . q) - (1 / O)),((y . q) + (1 / O)).[))) is set
q is set
q is Relation-like Function-like set
dom q is set
a is set
(y,(1 / O)) . a is set
y . a is ext-real complex real set
(y . a) - (1 / O) is ext-real complex real set
(y . a) + (- (1 / O)) is ext-real complex real set
(y . a) + (1 / O) is ext-real complex real set
].((y . a) - (1 / O)),((y . a) + (1 / O)).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
R^1 ].((y . a) - (1 / O)),((y . a) + (1 / O)).[ is V126() V127() V128() open Element of K19( the carrier of K598())
(Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((y . a) - (1 / O)),((y . a) + (1 / O)).[)) is Relation-like Function-like set
product ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((y . a) - (1 / O)),((y . a) + (1 / O)).[))) is set
dom ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((y . a) - (1 / O)),((y . a) + (1 / O)).[))) is set
q . a is set
((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((y . a) - (1 / O)),((y . a) + (1 / O)).[))) . a is set
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
the carrier of (Euclid n) is non empty set
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
K19(K19( the carrier of (TopSpaceMetr (Euclid n)))) is set
Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
(Seg n) --> R^1 is Relation-like Seg n -defined Seg n -defined Function-like constant total total quasi_total finite FinSequence-like FinSubsequence-like V272() V287() TopStruct-yielding Element of K19(K20((Seg n),{R^1}))
K20((Seg n),{R^1}) is Relation-like finite set
K19(K20((Seg n),{R^1})) is finite V49() set
product_prebasis ((Seg n) --> R^1) is Element of K19(K19((product (Carrier ((Seg n) --> R^1)))))
Carrier ((Seg n) --> R^1) is Relation-like Seg n -defined Function-like total set
product (Carrier ((Seg n) --> R^1)) is set
K19((product (Carrier ((Seg n) --> R^1)))) is set
K19(K19((product (Carrier ((Seg n) --> R^1))))) is set
J is Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))
x is Element of K19( the carrier of (TopSpaceMetr (Euclid n)))
R is TopStruct
the carrier of R is set
K19( the carrier of R) is set
i is set
V is Element of K19( the carrier of R)
((Seg n) --> R^1) . i is set
(Carrier ((Seg n) --> R^1)) +* (i,V) is Relation-like Function-like set
product ((Carrier ((Seg n) --> R^1)) +* (i,V)) is set
dom (Carrier ((Seg n) --> R^1)) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19((Seg n))
K19((Seg n)) is finite V49() set
r is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
e is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
y is ext-real complex real set
Ball (e,y) is Element of K19( the carrier of (Euclid n))
F is set
e . F is ext-real complex real set
(e . F) - y is ext-real complex real set
- y is ext-real complex real set
(e . F) + (- y) is ext-real complex real set
(e . F) + y is ext-real complex real set
].((e . F) - y),((e . F) + y).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
(Carrier ((Seg n) --> R^1)) +* (F,].((e . F) - y),((e . F) + y).[) is Relation-like Function-like set
dom r is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
dom ((Carrier ((Seg n) --> R^1)) +* (F,].((e . F) - y),((e . F) + y).[)) is set
G is set
r . F is ext-real complex real set
(r . F) - (e . F) is ext-real complex real set
- (e . F) is ext-real complex real set
(r . F) + (- (e . F)) is ext-real complex real set
(e . F) + ((r . F) - (e . F)) is ext-real complex real set
dom e is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
r - e is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like FinSequence of REAL
- e is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
(- 1) (#) e is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
r + (- e) is Relation-like NAT -defined Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like set
dom (r - e) is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(dom r) /\ (dom e) is finite V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
(r - e) . F is ext-real complex real set
abs ((r - e) . F) is ext-real non negative complex real Element of REAL
r . G is ext-real complex real set
((Carrier ((Seg n) --> R^1)) +* (F,].((e . F) - y),((e . F) + y).[)) . G is set
((Carrier ((Seg n) --> R^1)) +* (F,].((e . F) - y),((e . F) + y).[)) . G is set
(Carrier ((Seg n) --> R^1)) . G is set
((Seg n) --> R^1) . G is set
r . G is ext-real complex real set
a is 1-sorted
the carrier of a is set
product ((Carrier ((Seg n) --> R^1)) +* (F,].((e . F) - y),((e . F) + y).[)) is set
e is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
dom ((Carrier ((Seg n) --> R^1)) +* (i,V)) is set
e . i is ext-real complex real set
((Carrier ((Seg n) --> R^1)) +* (i,V)) . i is set
r is ext-real complex real Element of REAL
(e . i) - r is ext-real complex real Element of REAL
- r is ext-real complex real set
(e . i) + (- r) is ext-real complex real set
(e . i) + r is ext-real complex real Element of REAL
].((e . i) - r),((e . i) + r).[ is V126() V127() V128() open V302() V303() V307() Element of K19(REAL)
Ball (e,r) is Element of K19( the carrier of (Euclid n))
y is set
(Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[) is Relation-like Function-like set
dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) is set
y is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued finite n -element FinSequence-like FinSubsequence-like Element of the carrier of (Euclid n)
product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) is set
a is set
((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a is set
((Carrier ((Seg n) --> R^1)) +* (i,V)) . a is set
((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a is set
(Carrier ((Seg n) --> R^1)) . a is set
((Carrier ((Seg n) --> R^1)) +* (i,V)) . a is set
the topology of (TopSpaceMetr (Euclid n)) is Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))
n is ext-real non negative ordinal natural complex real finite cardinal set
Euclid n is non empty constituted-Functions constituted-FinSeqs strict Reflexive discerning V192() triangle MetrStruct
REAL n is functional non empty FinSequence-membered complex-functions-membered ext-real-functions-membered real-functions-membered FinSequenceSet of REAL
n -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = n } is set
Pitag_dist n is Relation-like Function-like quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20((REAL n),(REAL n)),REAL))
K20((REAL n),(REAL n)) is Relation-like set
K20(K20((REAL n),(REAL n)),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20((REAL n),(REAL n)),REAL)) is set
MetrStruct(# (REAL n),(Pitag_dist n) #) is strict MetrStruct
TopSpaceMetr (Euclid n) is non empty strict TopSpace-like TopStruct
the carrier of (Euclid n) is non empty set
Family_open_set (Euclid n) is Element of K19(K19( the carrier of (Euclid n)))
K19( the carrier of (Euclid n)) is set
K19(K19( the carrier of (Euclid n))) is set
TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) is strict TopStruct
Seg n is finite n -element V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of K19(NAT)
{ b1 where b1 is ext-real non negative ordinal natural complex real V43() V44() finite cardinal V126() V127() V128() V129() V130() V131() V304() V305() V306() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
(Seg n) --> R^1 is Relation-like Seg n -defined Seg n -defined Function-like constant total total quasi_total finite FinSequence-like FinSubsequence-like V272() V287() TopStruct-yielding Element of K19(K20((Seg n),{R^1}))
K20((Seg n),{R^1}) is Relation-like finite set
K19(K20((Seg n),{R^1})) is finite V49() set
product ((Seg n) --> R^1) is non empty constituted-Functions strict TopSpace-like TopStruct
Funcs ((Seg n),REAL) is functional complex-functions-membered ext-real-functions-membered real-functions-membered set
Carrier ((Seg n) --> R^1) is Relation-like Seg n -defined Function-like total set
product (Carrier ((Seg n) --> R^1)) is set
the carrier of (TopSpaceMetr (Euclid n)) is non empty set
K19( the carrier of (TopSpaceMetr (Euclid n))) is set
K19(K19( the carrier of (TopSpaceMetr (Euclid n)))) is set
product_prebasis ((Seg n) --> R^1) is Element of K19(K19((product (Carrier ((Seg n) --> R^1)))))
K19((product (Carrier ((Seg n) --> R^1)))) is set
K19(K19((product (Carrier ((Seg n) --> R^1))))) is set
PP is Element of K19(K19( the carrier of (TopSpaceMetr (Euclid n))))