:: EUCLID_9 semantic presentation

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
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 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)
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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)
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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)
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 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)
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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)
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 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
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 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)
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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)
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 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)
{ b₁ where b₁ 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 <= b₁ & b₁ <= 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
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b₁ = 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(