:: FCONT_3 semantic presentation

REAL is non empty V48() V84() V85() V86() V90() V97() V98() V100() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V48() V84() V90() set
omega is non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() set
K19(omega) is set
K20(NAT,REAL) is V1() V33() V34() V35() set
K19(K20(NAT,REAL)) is set
K19(K19(REAL)) is set
K20(REAL,REAL) is V1() V33() V34() V35() set
K19(K20(REAL,REAL)) is set
RAT is non empty V48() V84() V85() V86() V87() V90() set
INT is non empty V48() V84() V85() V86() V87() V88() V90() set
K20(COMPLEX,COMPLEX) is V1() V33() set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is V1() V33() set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(K20(REAL,REAL),REAL) is V1() V33() V34() V35() set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is V1() V5( RAT ) V33() V34() V35() set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is V1() V5( RAT ) V33() V34() V35() set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is V1() V5( RAT ) V5( INT ) V33() V34() V35() set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is V1() V5( RAT ) V5( INT ) V33() V34() V35() set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is V1() V5( RAT ) V5( INT ) V33() V34() V35() V36() set
K20(K20(NAT,NAT),NAT) is V1() V5( RAT ) V5( INT ) V33() V34() V35() V36() set
K19(K20(K20(NAT,NAT),NAT)) is set
K19(NAT) is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V82() V83() V84() V85() V86() V87() V88() V89() V95() V97() Element of NAT
{} is set
the V1() non-empty empty-yielding V5( RAT ) empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() V35() V36() V84() V85() V86() V87() V88() V89() V90() V97() V100() set is V1() non-empty empty-yielding V5( RAT ) empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() V35() V36() V84() V85() V86() V87() V88() V89() V90() V97() V100() set
0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V82() V83() V84() V85() V86() V87() V88() V89() V95() V97() Element of NAT
-infty is non empty non real ext-real non positive negative set
+infty is non empty non real ext-real positive non negative set
K195(-infty,+infty) is V95() V96() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= -infty & not +infty <= b₁ ) } is set
[#] REAL is V84() V85() V86() Element of K19(REAL)
f is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng f is non empty V84() V85() V86() set
lim f is V22() real ext-real Element of REAL
f is V84() V85() V86() Element of K19(REAL)
L is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng L is non empty V84() V85() V86() set
lim L is V22() real ext-real Element of REAL
rng L is non empty V84() V85() V86() Element of K19(REAL)
([#] REAL) ` is V84() V85() V86() Element of K19(REAL)
REAL \ ([#] REAL) is V84() V85() V86() set
{} REAL is V84() V85() V86() Element of K19(REAL)
f is V84() V85() V86() Element of K19(REAL)
f ` is V84() V85() V86() Element of K19(REAL)
REAL \ f is V84() V85() V86() set
f is V22() real ext-real set
right_closed_halfline f is V84() V85() V86() Element of K19(REAL)
K193(f,+infty) is V96() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f <= b₁ & not +infty <= b₁ ) } is set
NAT --> f is V1() V4( NAT ) V5({f}) Function-like constant non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,{f}))
{f} is V84() V85() V86() set
K20(NAT,{f}) is V1() V33() V34() V35() set
K19(K20(NAT,{f})) is set
r1 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng r1 is non empty V84() V85() V86() set
lim r1 is V22() real ext-real Element of REAL
rng r1 is non empty V84() V85() V86() Element of K19(REAL)
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT
r1 . x0 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : f <= b₁ } is set
L is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
L . x0 is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
lim L is V22() real ext-real Element of REAL
L . 0 is V22() real ext-real Element of REAL
left_closed_halfline f is V84() V85() V86() Element of K19(REAL)
K194(-infty,f) is V95() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= -infty & b₁ <= f ) } is set
NAT --> f is V1() V4( NAT ) V5({f}) Function-like constant non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,{f}))
{f} is V84() V85() V86() set
K20(NAT,{f}) is V1() V33() V34() V35() set
K19(K20(NAT,{f})) is set
r1 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng r1 is non empty V84() V85() V86() set
lim r1 is V22() real ext-real Element of REAL
rng r1 is non empty V84() V85() V86() Element of K19(REAL)
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT
r1 . x0 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : b₁ <= f } is set
L is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
L . x0 is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
lim L is V22() real ext-real Element of REAL
L . 0 is V22() real ext-real Element of REAL
right_open_halfline f is V84() V85() V86() Element of K19(REAL)
K195(f,+infty) is V95() V96() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= f & not +infty <= b₁ ) } is set
(right_open_halfline f) ` is V84() V85() V86() Element of K19(REAL)
REAL \ (right_open_halfline f) is V84() V85() V86() set
halfline f is V84() V85() V86() Element of K19(REAL)
K195(-infty,f) is V95() V96() V100() set
{ b<sub>1</sub> where b<sub>1</sub> is V22() real ext-real Element of REAL : ( not b<sub>1</sub> <= -infty & not f <= b<sub>1</sub> ) } is set
(halfline f) ` is V84() V85() V86() Element of K19(REAL)
REAL \ (halfline f) is V84() V85() V86() set
f is V22() real ext-real Element of REAL
L is V22() real ext-real Element of REAL
f - L is V22() real ext-real Element of REAL
abs (f - L) is V22() real ext-real Element of REAL
r1 is V22() real ext-real set
L - r1 is V22() real ext-real Element of REAL
L + r1 is V22() real ext-real Element of REAL
].(L - r1),(L + r1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= L - r1 & not L + r1 <= b₁ ) } is set
(L + r1) - L is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
L - f is V22() real ext-real Element of REAL
- (f - L) is V22() real ext-real Element of REAL
abs (- (f - L)) is V22() real ext-real Element of REAL
L - (L - r1) is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
L is V22() real ext-real Element of REAL
f - L is V22() real ext-real Element of REAL
r1 is V22() real ext-real set
L - r1 is V22() real ext-real Element of REAL
L + r1 is V22() real ext-real Element of REAL
].(L - r1),(L + r1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= L - r1 & not L + r1 <= b₁ ) } is set
- r1 is V22() real ext-real set
].(- r1),r1.[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= - r1 & not r1 <= b₁ ) } is set
abs (f - L) is V22() real ext-real Element of REAL
(f - L) - 0 is V22() real ext-real Element of REAL
abs ((f - L) - 0) is V22() real ext-real Element of REAL
0 - r1 is V22() real ext-real Element of REAL
0 + r1 is V22() real ext-real Element of REAL
].(0 - r1),(0 + r1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= 0 - r1 & not 0 + r1 <= b₁ ) } is set
f is V22() real ext-real Element of REAL
L is V22() real ext-real Element of REAL
r1 is V22() real ext-real Element of REAL
L + r1 is V22() real ext-real Element of REAL
abs r1 is V22() real ext-real Element of REAL
x0 is V22() real ext-real set
L - x0 is V22() real ext-real Element of REAL
L + x0 is V22() real ext-real Element of REAL
].(L - x0),(L + x0).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= L - x0 & not L + x0 <= b₁ ) } is set
f - L is V22() real ext-real Element of REAL
abs (f - L) is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
L is V22() real ext-real Element of REAL
f - L is V22() real ext-real Element of REAL
r1 is V22() real ext-real set
- r1 is V22() real ext-real set
].(- r1),r1.[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= - r1 & not r1 <= b₁ ) } is set
L - r1 is V22() real ext-real Element of REAL
L + r1 is V22() real ext-real Element of REAL
].(L - r1),(L + r1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= L - r1 & not L + r1 <= b₁ ) } is set
abs (f - L) is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
L + (f - L) is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
L is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim L is V22() real ext-real Element of REAL
r1 is V22() real ext-real set
x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
NAT --> r1 is V1() V4( NAT ) V5({r1}) Function-like constant non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,{r1}))
{r1} is V84() V85() V86() set
K20(NAT,{r1}) is V1() V33() V34() V35() set
K19(K20(NAT,{r1})) is set
N is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
N - x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT
(N - x0) . r is V22() real ext-real Element of REAL
N . r is V22() real ext-real Element of REAL
x0 . r is V22() real ext-real Element of REAL
(N . r) - (x0 . r) is V22() real ext-real Element of REAL
r1 - (x0 . r) is V22() real ext-real Element of REAL
r + 1 is V22() real ext-real Element of REAL
f / (r + 1) is V22() real ext-real Element of REAL
r1 - (f / (r + 1)) is V22() real ext-real Element of REAL
L . r is V22() real ext-real Element of REAL
lim N is V22() real ext-real Element of REAL
N . 0 is V22() real ext-real Element of REAL
lim x0 is V22() real ext-real Element of REAL
r1 - 0 is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
L is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
lim L is V22() real ext-real Element of REAL
r1 is V22() real ext-real set
x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
NAT --> r1 is V1() V4( NAT ) V5({r1}) Function-like constant non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,{r1}))
{r1} is V84() V85() V86() set
K20(NAT,{r1}) is V1() V33() V34() V35() set
K19(K20(NAT,{r1})) is set
N is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
N + x0 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT
(N + x0) . r is V22() real ext-real Element of REAL
N . r is V22() real ext-real Element of REAL
x0 . r is V22() real ext-real Element of REAL
(N . r) + (x0 . r) is V22() real ext-real Element of REAL
r1 + (x0 . r) is V22() real ext-real Element of REAL
r + 1 is V22() real ext-real Element of REAL
f / (r + 1) is V22() real ext-real Element of REAL
r1 + (f / (r + 1)) is V22() real ext-real Element of REAL
L . r is V22() real ext-real Element of REAL
lim N is V22() real ext-real Element of REAL
N . 0 is V22() real ext-real Element of REAL
lim x0 is V22() real ext-real Element of REAL
r1 + 0 is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
L is V22() real ext-real set
r1 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
r1 . f is V22() real ext-real Element of REAL
dom r1 is V84() V85() V86() Element of K19(REAL)
x0 is open V84() V85() V86() Neighbourhood of f
N is V22() real ext-real set
f - N is V22() real ext-real Element of REAL
f + N is V22() real ext-real Element of REAL
].(f - N),(f + N).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= f - N & not f + N <= b₁ ) } is set
r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT
r + 1 is V22() real ext-real Element of REAL
N / (r + 1) is V22() real ext-real Element of REAL
f - (N / (r + 1)) is V22() real ext-real Element of REAL
f + (N / (r + 1)) is V22() real ext-real Element of REAL
].(f - (N / (r + 1))),(f + (N / (r + 1))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= f - (N / (r + 1)) & not f + (N / (r + 1)) <= b₁ ) } is set
r is open V84() V85() V86() Neighbourhood of f
fp is set
fm is V22() real ext-real Element of REAL
0 + 1 is V22() real ext-real Element of REAL
N / 1 is V22() real ext-real Element of REAL
fp is V22() real ext-real Element of REAL
r1 . fp is V22() real ext-real Element of REAL
fm is V22() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
rng r is non empty V84() V85() V86() Element of K19(REAL)
r is set
fp is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT
r . fp is V22() real ext-real Element of REAL
r is V22() real ext-real set
fp is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT
fm is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT
r1 /* r is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
(r1 /* r) . fm is V22() real ext-real Element of REAL
((r1 /* r) . fm) - L is V22() real ext-real Element of REAL
abs (((r1 /* r) . fm) - L) is V22() real ext-real Element of REAL
r . fm is V22() real ext-real Element of REAL
r1 . (r . fm) is V22() real ext-real Element of REAL
(r1 . (r . fm)) - L is V22() real ext-real Element of REAL
abs ((r1 . (r . fm)) - L) is V22() real ext-real Element of REAL
L - L is V22() real ext-real set
abs (L - L) is V22() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
fp is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total V33() V34() V35() Element of K19(K20(NAT,REAL))
fm is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() Element of NAT
r . fm is V22() real ext-real Element of REAL
fm + 1 is V22() real ext-real Element of REAL
N / (fm + 1) is V22() real ext-real Element of REAL
f - (N / (fm + 1)) is V22() real ext-real Element of REAL
f + (N / (fm + 1)) is V22() real ext-real Element of REAL
r . fm is V22() real ext-real Element of REAL
fp . fm is V22() real ext-real Element of REAL
lim fp is V22() real ext-real Element of REAL
lim r is V22() real ext-real Element of REAL
lim r is V22() real ext-real Element of REAL
lim (r1 /* r) is V22() real ext-real Element of REAL
f is set
L is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (L | f) is Element of K19(f)
K19(f) is set
r1 is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
(L | f) . r1 is V22() real ext-real Element of REAL
(L | f) . x0 is V22() real ext-real Element of REAL
dom L is V84() V85() V86() Element of K19(REAL)
f /\ (dom L) is V84() V85() V86() Element of K19(REAL)
L . x0 is V22() real ext-real Element of REAL
L . r1 is V22() real ext-real Element of REAL
L . r1 is V22() real ext-real Element of REAL
L . x0 is V22() real ext-real Element of REAL
dom (L | f) is Element of K19(f)
K19(f) is set
r1 is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
(L | f) . r1 is V22() real ext-real Element of REAL
(L | f) . x0 is V22() real ext-real Element of REAL
dom L is V84() V85() V86() Element of K19(REAL)
f /\ (dom L) is V84() V85() V86() Element of K19(REAL)
L . r1 is V22() real ext-real Element of REAL
L . x0 is V22() real ext-real Element of REAL
L . x0 is V22() real ext-real Element of REAL
L . r1 is V22() real ext-real Element of REAL
f is set
L is V1() V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
(L | f) " is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L .: f is V84() V85() V86() Element of K19(REAL)
((L | f) ") | (L .: f) is V1() V4( REAL ) V4(L .: f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom ((L | f) ") is V84() V85() V86() Element of K19(REAL)
(L .: f) /\ (dom ((L | f) ")) is V84() V85() V86() Element of K19(REAL)
r1 is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
((L | f) ") . x0 is V22() real ext-real Element of REAL
((L | f) ") . r1 is V22() real ext-real Element of REAL
rng (L | f) is V84() V85() V86() Element of K19(REAL)
(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
(L | f) . (((L | f) ") . x0) is V22() real ext-real Element of REAL
dom (L | f) is Element of K19(f)
K19(f) is set
dom ((L | f) | f) is Element of K19(f)
f /\ (dom (L | f)) is Element of K19(f)
(L | f) . (((L | f) ") . r1) is V22() real ext-real Element of REAL
(L | f) . (((L | f) ") . x0) is V22() real ext-real Element of REAL
f is set
L is V1() V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
(L | f) " is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L .: f is V84() V85() V86() Element of K19(REAL)
((L | f) ") | (L .: f) is V1() V4( REAL ) V4(L .: f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom ((L | f) ") is V84() V85() V86() Element of K19(REAL)
(L .: f) /\ (dom ((L | f) ")) is V84() V85() V86() Element of K19(REAL)
r1 is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
((L | f) ") . r1 is V22() real ext-real Element of REAL
((L | f) ") . x0 is V22() real ext-real Element of REAL
rng (L | f) is V84() V85() V86() Element of K19(REAL)
(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
(L | f) . (((L | f) ") . x0) is V22() real ext-real Element of REAL
dom (L | f) is Element of K19(f)
K19(f) is set
dom ((L | f) | f) is Element of K19(f)
f /\ (dom (L | f)) is Element of K19(f)
(L | f) . (((L | f) ") . r1) is V22() real ext-real Element of REAL
(L | f) . (((L | f) ") . x0) is V22() real ext-real Element of REAL
f is set
L is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom L is V84() V85() V86() Element of K19(REAL)
L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L .: f is V84() V85() V86() Element of K19(REAL)
r1 is V22() real ext-real Element of REAL
halfline r1 is open V84() V85() V86() Element of K19(REAL)
K195(-infty,r1) is V95() V96() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= -infty & not r1 <= b₁ ) } is set
(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (L | f) is Element of K19(f)
K19(f) is set
N is V22() real ext-real set
(L | f) .: f is V84() V85() V86() Element of K19(REAL)
(dom L) /\ f is V84() V85() V86() Element of K19(REAL)
(L | f) . N is V22() real ext-real Element of REAL
r is open V84() V85() V86() Neighbourhood of (L | f) . N
r is open V84() V85() V86() Neighbourhood of (L | f) . N
fp is open V84() V85() V86() Neighbourhood of (L | f) . N
fm is V22() real ext-real set
((L | f) . N) - fm is V22() real ext-real Element of REAL
((L | f) . N) + fm is V22() real ext-real Element of REAL
].(((L | f) . N) - fm),(((L | f) . N) + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . N) - fm & not ((L | f) . N) + fm <= b₁ ) } is set
R is V22() real ext-real Element of REAL
R / 2 is V22() real ext-real Element of REAL
((L | f) . N) + (R / 2) is V22() real ext-real Element of REAL
(((L | f) . N) + (R / 2)) + (R / 2) is V22() real ext-real Element of REAL
((L | f) . N) + R is V22() real ext-real Element of REAL
(((L | f) . N) + R) - R is V22() real ext-real Element of REAL
((L | f) . N) - R is V22() real ext-real Element of REAL
].(((L | f) . N) - R),(((L | f) . N) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . N) - R & not ((L | f) . N) + R <= b₁ ) } is set
N1 is V22() real ext-real Element of REAL
(L | f) . N1 is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
((L | f) . N) - (R / 2) is V22() real ext-real Element of REAL
(((L | f) . N) - R) + (R / 2) is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
(L | f) . r2 is V22() real ext-real Element of REAL
N1 - N is V22() real ext-real Element of REAL
N - r2 is V22() real ext-real Element of REAL
min ((N - r2),(N1 - N)) is V22() real ext-real set
N - (min ((N - r2),(N1 - N))) is V22() real ext-real set
N + (min ((N - r2),(N1 - N))) is V22() real ext-real set
].(N - (min ((N - r2),(N1 - N)))),(N + (min ((N - r2),(N1 - N)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= N - (min ((N - r2),(N1 - N))) & not N + (min ((N - r2),(N1 - N))) <= b₁ ) } is set
r2 is open V84() V85() V86() Neighbourhood of N
N is V22() real ext-real set
s is open V84() V85() V86() Neighbourhood of N
(min ((N - r2),(N1 - N))) + N is V22() real ext-real set
x is V22() real ext-real Element of REAL
((min ((N - r2),(N1 - N))) + N) - N is V22() real ext-real set
N - N is V22() real ext-real set
- (N - N) is V22() real ext-real set
- (N - r2) is V22() real ext-real Element of REAL
N - N is V22() real ext-real set
(N - N) + N is V22() real ext-real set
r2 - N is V22() real ext-real Element of REAL
(r2 - N) + N is V22() real ext-real Element of REAL
(L | f) . N is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
(N1 - N) + N is V22() real ext-real Element of REAL
[.(((L | f) . N) - (R / 2)),(((L | f) . N) + (R / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( ((L | f) . N) - (R / 2) <= b₁ & b₁ <= ((L | f) . N) + (R / 2) ) } is set
(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (L | f) is Element of K19(f)
K19(f) is set
N is V22() real ext-real set
(L | f) .: f is V84() V85() V86() Element of K19(REAL)
(dom L) /\ f is V84() V85() V86() Element of K19(REAL)
(L | f) . N is V22() real ext-real Element of REAL
r is open V84() V85() V86() Neighbourhood of (L | f) . N
r is open V84() V85() V86() Neighbourhood of (L | f) . N
fp is open V84() V85() V86() Neighbourhood of (L | f) . N
fm is V22() real ext-real set
((L | f) . N) - fm is V22() real ext-real Element of REAL
((L | f) . N) + fm is V22() real ext-real Element of REAL
].(((L | f) . N) - fm),(((L | f) . N) + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . N) - fm & not ((L | f) . N) + fm <= b₁ ) } is set
R is V22() real ext-real Element of REAL
R / 2 is V22() real ext-real Element of REAL
((L | f) . N) + (R / 2) is V22() real ext-real Element of REAL
(((L | f) . N) + (R / 2)) + (R / 2) is V22() real ext-real Element of REAL
((L | f) . N) + R is V22() real ext-real Element of REAL
(((L | f) . N) + R) - R is V22() real ext-real Element of REAL
((L | f) . N) - R is V22() real ext-real Element of REAL
].(((L | f) . N) - R),(((L | f) . N) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . N) - R & not ((L | f) . N) + R <= b₁ ) } is set
N1 is V22() real ext-real Element of REAL
(L | f) . N1 is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
((L | f) . N) - (R / 2) is V22() real ext-real Element of REAL
(((L | f) . N) - R) + (R / 2) is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
(L | f) . r2 is V22() real ext-real Element of REAL
N - N1 is V22() real ext-real Element of REAL
r2 - N is V22() real ext-real Element of REAL
min ((r2 - N),(N - N1)) is V22() real ext-real set
N - (min ((r2 - N),(N - N1))) is V22() real ext-real set
N + (min ((r2 - N),(N - N1))) is V22() real ext-real set
].(N - (min ((r2 - N),(N - N1)))),(N + (min ((r2 - N),(N - N1)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= N - (min ((r2 - N),(N - N1))) & not N + (min ((r2 - N),(N - N1))) <= b₁ ) } is set
r2 is open V84() V85() V86() Neighbourhood of N
N is V22() real ext-real set
s is open V84() V85() V86() Neighbourhood of N
(min ((r2 - N),(N - N1))) + N is V22() real ext-real set
x is V22() real ext-real Element of REAL
((min ((r2 - N),(N - N1))) + N) - N is V22() real ext-real set
N - N is V22() real ext-real set
N - N is V22() real ext-real set
x is V22() real ext-real Element of REAL
(r2 - N) + N is V22() real ext-real Element of REAL
(N - N) + N is V22() real ext-real set
(L | f) . N is V22() real ext-real Element of REAL
- (N - N) is V22() real ext-real set
- (N - N1) is V22() real ext-real Element of REAL
N1 - N is V22() real ext-real Element of REAL
(N1 - N) + N is V22() real ext-real Element of REAL
[.(((L | f) . N) - (R / 2)),(((L | f) . N) + (R / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( ((L | f) . N) - (R / 2) <= b₁ & b₁ <= ((L | f) . N) + (R / 2) ) } is set
f is set
L is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom L is V84() V85() V86() Element of K19(REAL)
L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L .: f is V84() V85() V86() Element of K19(REAL)
r1 is V22() real ext-real Element of REAL
right_open_halfline r1 is open V84() V85() V86() Element of K19(REAL)
K195(r1,+infty) is V95() V96() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 & not +infty <= b₁ ) } is set
(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (L | f) is Element of K19(f)
K19(f) is set
N is V22() real ext-real set
(L | f) .: f is V84() V85() V86() Element of K19(REAL)
(dom L) /\ f is V84() V85() V86() Element of K19(REAL)
(L | f) . N is V22() real ext-real Element of REAL
r is open V84() V85() V86() Neighbourhood of (L | f) . N
r is open V84() V85() V86() Neighbourhood of (L | f) . N
fp is open V84() V85() V86() Neighbourhood of (L | f) . N
fm is V22() real ext-real set
((L | f) . N) - fm is V22() real ext-real Element of REAL
((L | f) . N) + fm is V22() real ext-real Element of REAL
].(((L | f) . N) - fm),(((L | f) . N) + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . N) - fm & not ((L | f) . N) + fm <= b₁ ) } is set
R is V22() real ext-real Element of REAL
R / 2 is V22() real ext-real Element of REAL
((L | f) . N) + (R / 2) is V22() real ext-real Element of REAL
(((L | f) . N) + (R / 2)) + (R / 2) is V22() real ext-real Element of REAL
((L | f) . N) + R is V22() real ext-real Element of REAL
(((L | f) . N) + R) - R is V22() real ext-real Element of REAL
((L | f) . N) - R is V22() real ext-real Element of REAL
].(((L | f) . N) - R),(((L | f) . N) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . N) - R & not ((L | f) . N) + R <= b₁ ) } is set
N1 is V22() real ext-real Element of REAL
(L | f) . N1 is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
((L | f) . N) - (R / 2) is V22() real ext-real Element of REAL
(((L | f) . N) - R) + (R / 2) is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
(L | f) . r2 is V22() real ext-real Element of REAL
N1 - N is V22() real ext-real Element of REAL
N - r2 is V22() real ext-real Element of REAL
min ((N - r2),(N1 - N)) is V22() real ext-real set
N - (min ((N - r2),(N1 - N))) is V22() real ext-real set
N + (min ((N - r2),(N1 - N))) is V22() real ext-real set
].(N - (min ((N - r2),(N1 - N)))),(N + (min ((N - r2),(N1 - N)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= N - (min ((N - r2),(N1 - N))) & not N + (min ((N - r2),(N1 - N))) <= b₁ ) } is set
r2 is open V84() V85() V86() Neighbourhood of N
N is V22() real ext-real set
s is open V84() V85() V86() Neighbourhood of N
(min ((N - r2),(N1 - N))) + N is V22() real ext-real set
x is V22() real ext-real Element of REAL
((min ((N - r2),(N1 - N))) + N) - N is V22() real ext-real set
N - N is V22() real ext-real set
- (N - N) is V22() real ext-real set
- (N - r2) is V22() real ext-real Element of REAL
N - N is V22() real ext-real set
(N - N) + N is V22() real ext-real set
r2 - N is V22() real ext-real Element of REAL
(r2 - N) + N is V22() real ext-real Element of REAL
(L | f) . N is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
(N1 - N) + N is V22() real ext-real Element of REAL
[.(((L | f) . N) - (R / 2)),(((L | f) . N) + (R / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( ((L | f) . N) - (R / 2) <= b₁ & b₁ <= ((L | f) . N) + (R / 2) ) } is set
(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (L | f) is Element of K19(f)
K19(f) is set
N is V22() real ext-real set
(L | f) .: f is V84() V85() V86() Element of K19(REAL)
(dom L) /\ f is V84() V85() V86() Element of K19(REAL)
(L | f) . N is V22() real ext-real Element of REAL
r is open V84() V85() V86() Neighbourhood of (L | f) . N
r is open V84() V85() V86() Neighbourhood of (L | f) . N
fp is open V84() V85() V86() Neighbourhood of (L | f) . N
fm is V22() real ext-real set
((L | f) . N) - fm is V22() real ext-real Element of REAL
((L | f) . N) + fm is V22() real ext-real Element of REAL
].(((L | f) . N) - fm),(((L | f) . N) + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . N) - fm & not ((L | f) . N) + fm <= b₁ ) } is set
R is V22() real ext-real Element of REAL
R / 2 is V22() real ext-real Element of REAL
((L | f) . N) + (R / 2) is V22() real ext-real Element of REAL
(((L | f) . N) + (R / 2)) + (R / 2) is V22() real ext-real Element of REAL
((L | f) . N) + R is V22() real ext-real Element of REAL
(((L | f) . N) + R) - R is V22() real ext-real Element of REAL
((L | f) . N) - R is V22() real ext-real Element of REAL
].(((L | f) . N) - R),(((L | f) . N) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . N) - R & not ((L | f) . N) + R <= b₁ ) } is set
N1 is V22() real ext-real Element of REAL
(L | f) . N1 is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
((L | f) . N) - (R / 2) is V22() real ext-real Element of REAL
(((L | f) . N) - R) + (R / 2) is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
(L | f) . r2 is V22() real ext-real Element of REAL
N - N1 is V22() real ext-real Element of REAL
r2 - N is V22() real ext-real Element of REAL
min ((r2 - N),(N - N1)) is V22() real ext-real set
N - (min ((r2 - N),(N - N1))) is V22() real ext-real set
N + (min ((r2 - N),(N - N1))) is V22() real ext-real set
].(N - (min ((r2 - N),(N - N1)))),(N + (min ((r2 - N),(N - N1)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= N - (min ((r2 - N),(N - N1))) & not N + (min ((r2 - N),(N - N1))) <= b₁ ) } is set
r2 is open V84() V85() V86() Neighbourhood of N
N is V22() real ext-real set
s is open V84() V85() V86() Neighbourhood of N
(min ((r2 - N),(N - N1))) + N is V22() real ext-real set
x is V22() real ext-real Element of REAL
((min ((r2 - N),(N - N1))) + N) - N is V22() real ext-real set
N - N is V22() real ext-real set
N - N is V22() real ext-real set
x is V22() real ext-real Element of REAL
(r2 - N) + N is V22() real ext-real Element of REAL
(N - N) + N is V22() real ext-real set
(L | f) . N is V22() real ext-real Element of REAL
- (N - N) is V22() real ext-real set
- (N - N1) is V22() real ext-real Element of REAL
N1 - N is V22() real ext-real Element of REAL
(N1 - N) + N is V22() real ext-real Element of REAL
[.(((L | f) . N) - (R / 2)),(((L | f) . N) + (R / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( ((L | f) . N) - (R / 2) <= b₁ & b₁ <= ((L | f) . N) + (R / 2) ) } is set
f is set
L is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom L is V84() V85() V86() Element of K19(REAL)
L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L .: f is V84() V85() V86() Element of K19(REAL)
r1 is V22() real ext-real Element of REAL
left_closed_halfline r1 is closed V84() V85() V86() Element of K19(REAL)
K194(-infty,r1) is V95() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= -infty & b₁ <= r1 ) } is set
halfline r1 is open V84() V85() V86() Element of K19(REAL)
K195(-infty,r1) is V95() V96() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= -infty & not r1 <= b₁ ) } is set
dom (L | f) is Element of K19(f)
K19(f) is set
r is V22() real ext-real set
(L | f) .: f is V84() V85() V86() Element of K19(REAL)
(dom L) /\ f is V84() V85() V86() Element of K19(REAL)
(L | f) . r is V22() real ext-real Element of REAL
{r1} is V84() V85() V86() set
{r1} \/ (halfline r1) is V84() V85() V86() set
(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
fp is open V84() V85() V86() Neighbourhood of (L | f) . r
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fm is open V84() V85() V86() Neighbourhood of (L | f) . r
R is V22() real ext-real set
((L | f) . r) - R is V22() real ext-real Element of REAL
((L | f) . r) + R is V22() real ext-real Element of REAL
].(((L | f) . r) - R),(((L | f) . r) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r) - R & not ((L | f) . r) + R <= b₁ ) } is set
N1 is V22() real ext-real Element of REAL
N1 / 2 is V22() real ext-real Element of REAL
((L | f) . r) + (N1 / 2) is V22() real ext-real Element of REAL
(((L | f) . r) + (N1 / 2)) + (N1 / 2) is V22() real ext-real Element of REAL
((L | f) . r) + N1 is V22() real ext-real Element of REAL
(((L | f) . r) + N1) - N1 is V22() real ext-real Element of REAL
((L | f) . r) - N1 is V22() real ext-real Element of REAL
].(((L | f) . r) - N1),(((L | f) . r) + N1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r) - N1 & not ((L | f) . r) + N1 <= b₁ ) } is set
x is V22() real ext-real Element of REAL
(L | f) . x is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
((L | f) . r) - (N1 / 2) is V22() real ext-real Element of REAL
(((L | f) . r) - N1) + (N1 / 2) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
(L | f) . s is V22() real ext-real Element of REAL
x - r is V22() real ext-real Element of REAL
r - s is V22() real ext-real Element of REAL
min ((r - s),(x - r)) is V22() real ext-real set
r - (min ((r - s),(x - r))) is V22() real ext-real set
r + (min ((r - s),(x - r))) is V22() real ext-real set
].(r - (min ((r - s),(x - r)))),(r + (min ((r - s),(x - r)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - (min ((r - s),(x - r))) & not r + (min ((r - s),(x - r))) <= b₁ ) } is set
s is open V84() V85() V86() Neighbourhood of r
x is V22() real ext-real set
N is open V84() V85() V86() Neighbourhood of r
(min ((r - s),(x - r))) + x is V22() real ext-real set
c₂₀ is V22() real ext-real Element of REAL
((min ((r - s),(x - r))) + x) - x is V22() real ext-real set
r - x is V22() real ext-real set
- (r - x) is V22() real ext-real set
- (r - s) is V22() real ext-real Element of REAL
x - r is V22() real ext-real set
(x - r) + r is V22() real ext-real set
s - r is V22() real ext-real Element of REAL
(s - r) + r is V22() real ext-real Element of REAL
(L | f) . x is V22() real ext-real Element of REAL
c₂₀ is V22() real ext-real Element of REAL
(x - r) + r is V22() real ext-real Element of REAL
[.(((L | f) . r) - (N1 / 2)),(((L | f) . r) + (N1 / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( ((L | f) . r) - (N1 / 2) <= b₁ & b₁ <= ((L | f) . r) + (N1 / 2) ) } is set
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fp is V22() real ext-real set
r1 - fp is V22() real ext-real Element of REAL
r1 + fp is V22() real ext-real Element of REAL
].(r1 - fp),(r1 + fp).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 - fp & not r1 + fp <= b₁ ) } is set
fm is V22() real ext-real Element of REAL
fm / 2 is V22() real ext-real Element of REAL
r1 + (fm / 2) is V22() real ext-real Element of REAL
r1 - (fm / 2) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : not r1 <= b₁ } is set
N1 is V22() real ext-real Element of REAL
(L | f) . N1 is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
r - N1 is V22() real ext-real Element of REAL
r - (r - N1) is V22() real ext-real Element of REAL
r + (r - N1) is V22() real ext-real Element of REAL
].(r - (r - N1)),(r + (r - N1)).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - (r - N1) & not r + (r - N1) <= b₁ ) } is set
N1 is open V84() V85() V86() Neighbourhood of r
r2 is V22() real ext-real set
x is open V84() V85() V86() Neighbourhood of r
r1 - fm is V22() real ext-real Element of REAL
(L | f) . r2 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : b₁ <= r1 } is set
s is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
[.(r1 - (fm / 2)),(r1 + (fm / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( r1 - (fm / 2) <= b₁ & b₁ <= r1 + (fm / 2) ) } is set
r1 + fm is V22() real ext-real Element of REAL
].(r1 - fm),(r1 + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 - fm & not r1 + fm <= b₁ ) } is set
r is open V84() V85() V86() Neighbourhood of (L | f) . r
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fp is open V84() V85() V86() Neighbourhood of r
(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
fp is open V84() V85() V86() Neighbourhood of (L | f) . r
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fm is open V84() V85() V86() Neighbourhood of (L | f) . r
R is V22() real ext-real set
((L | f) . r) - R is V22() real ext-real Element of REAL
((L | f) . r) + R is V22() real ext-real Element of REAL
].(((L | f) . r) - R),(((L | f) . r) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r) - R & not ((L | f) . r) + R <= b₁ ) } is set
N1 is V22() real ext-real Element of REAL
N1 / 2 is V22() real ext-real Element of REAL
((L | f) . r) + (N1 / 2) is V22() real ext-real Element of REAL
(((L | f) . r) + (N1 / 2)) + (N1 / 2) is V22() real ext-real Element of REAL
((L | f) . r) + N1 is V22() real ext-real Element of REAL
(((L | f) . r) + N1) - N1 is V22() real ext-real Element of REAL
((L | f) . r) - N1 is V22() real ext-real Element of REAL
].(((L | f) . r) - N1),(((L | f) . r) + N1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r) - N1 & not ((L | f) . r) + N1 <= b₁ ) } is set
x is V22() real ext-real Element of REAL
(L | f) . x is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
((L | f) . r) - (N1 / 2) is V22() real ext-real Element of REAL
(((L | f) . r) - N1) + (N1 / 2) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
(L | f) . s is V22() real ext-real Element of REAL
r - x is V22() real ext-real Element of REAL
s - r is V22() real ext-real Element of REAL
min ((s - r),(r - x)) is V22() real ext-real set
r - (min ((s - r),(r - x))) is V22() real ext-real set
r + (min ((s - r),(r - x))) is V22() real ext-real set
].(r - (min ((s - r),(r - x)))),(r + (min ((s - r),(r - x)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - (min ((s - r),(r - x))) & not r + (min ((s - r),(r - x))) <= b₁ ) } is set
s is open V84() V85() V86() Neighbourhood of r
x is V22() real ext-real set
N is open V84() V85() V86() Neighbourhood of r
(min ((s - r),(r - x))) + x is V22() real ext-real set
c₂₀ is V22() real ext-real Element of REAL
((min ((s - r),(r - x))) + x) - x is V22() real ext-real set
r - x is V22() real ext-real set
x - r is V22() real ext-real set
c₂₀ is V22() real ext-real Element of REAL
(s - r) + r is V22() real ext-real Element of REAL
(x - r) + r is V22() real ext-real set
(L | f) . x is V22() real ext-real Element of REAL
- (r - x) is V22() real ext-real set
- (r - x) is V22() real ext-real Element of REAL
x - r is V22() real ext-real Element of REAL
(x - r) + r is V22() real ext-real Element of REAL
[.(((L | f) . r) - (N1 / 2)),(((L | f) . r) + (N1 / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( ((L | f) . r) - (N1 / 2) <= b₁ & b₁ <= ((L | f) . r) + (N1 / 2) ) } is set
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fp is V22() real ext-real set
r1 - fp is V22() real ext-real Element of REAL
r1 + fp is V22() real ext-real Element of REAL
].(r1 - fp),(r1 + fp).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 - fp & not r1 + fp <= b₁ ) } is set
fm is V22() real ext-real Element of REAL
fm / 2 is V22() real ext-real Element of REAL
r1 + (fm / 2) is V22() real ext-real Element of REAL
r1 - (fm / 2) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : not r1 <= b₁ } is set
N1 is V22() real ext-real Element of REAL
(L | f) . N1 is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
N1 - r is V22() real ext-real Element of REAL
r - (N1 - r) is V22() real ext-real Element of REAL
r + (N1 - r) is V22() real ext-real Element of REAL
].(r - (N1 - r)),(r + (N1 - r)).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - (N1 - r) & not r + (N1 - r) <= b₁ ) } is set
N1 is open V84() V85() V86() Neighbourhood of r
r2 is V22() real ext-real set
x is open V84() V85() V86() Neighbourhood of r
r1 - fm is V22() real ext-real Element of REAL
(L | f) . r2 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : b₁ <= r1 } is set
s is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
[.(r1 - (fm / 2)),(r1 + (fm / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( r1 - (fm / 2) <= b₁ & b₁ <= r1 + (fm / 2) ) } is set
r1 + fm is V22() real ext-real Element of REAL
].(r1 - fm),(r1 + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 - fm & not r1 + fm <= b₁ ) } is set
r is open V84() V85() V86() Neighbourhood of (L | f) . r
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fp is open V84() V85() V86() Neighbourhood of r
r is open V84() V85() V86() Neighbourhood of (L | f) . r
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fp is open V84() V85() V86() Neighbourhood of r
f is set
L is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom L is V84() V85() V86() Element of K19(REAL)
L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L .: f is V84() V85() V86() Element of K19(REAL)
r1 is V22() real ext-real Element of REAL
right_closed_halfline r1 is closed V84() V85() V86() Element of K19(REAL)
K193(r1,+infty) is V96() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( r1 <= b₁ & not +infty <= b₁ ) } is set
right_open_halfline r1 is open V84() V85() V86() Element of K19(REAL)
K195(r1,+infty) is V95() V96() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 & not +infty <= b₁ ) } is set
dom (L | f) is Element of K19(f)
K19(f) is set
r is V22() real ext-real set
(L | f) .: f is V84() V85() V86() Element of K19(REAL)
(dom L) /\ f is V84() V85() V86() Element of K19(REAL)
(L | f) . r is V22() real ext-real Element of REAL
{r1} is V84() V85() V86() set
{r1} \/ (right_open_halfline r1) is V84() V85() V86() set
(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
fp is open V84() V85() V86() Neighbourhood of (L | f) . r
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fm is open V84() V85() V86() Neighbourhood of (L | f) . r
R is V22() real ext-real set
((L | f) . r) - R is V22() real ext-real Element of REAL
((L | f) . r) + R is V22() real ext-real Element of REAL
].(((L | f) . r) - R),(((L | f) . r) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r) - R & not ((L | f) . r) + R <= b₁ ) } is set
N1 is V22() real ext-real Element of REAL
N1 / 2 is V22() real ext-real Element of REAL
((L | f) . r) + (N1 / 2) is V22() real ext-real Element of REAL
(((L | f) . r) + (N1 / 2)) + (N1 / 2) is V22() real ext-real Element of REAL
((L | f) . r) + N1 is V22() real ext-real Element of REAL
(((L | f) . r) + N1) - N1 is V22() real ext-real Element of REAL
((L | f) . r) - N1 is V22() real ext-real Element of REAL
].(((L | f) . r) - N1),(((L | f) . r) + N1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r) - N1 & not ((L | f) . r) + N1 <= b₁ ) } is set
x is V22() real ext-real Element of REAL
(L | f) . x is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
((L | f) . r) - (N1 / 2) is V22() real ext-real Element of REAL
(((L | f) . r) - N1) + (N1 / 2) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
(L | f) . s is V22() real ext-real Element of REAL
x - r is V22() real ext-real Element of REAL
r - s is V22() real ext-real Element of REAL
min ((r - s),(x - r)) is V22() real ext-real set
r - (min ((r - s),(x - r))) is V22() real ext-real set
r + (min ((r - s),(x - r))) is V22() real ext-real set
].(r - (min ((r - s),(x - r)))),(r + (min ((r - s),(x - r)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - (min ((r - s),(x - r))) & not r + (min ((r - s),(x - r))) <= b₁ ) } is set
s is open V84() V85() V86() Neighbourhood of r
x is V22() real ext-real set
N is open V84() V85() V86() Neighbourhood of r
(min ((r - s),(x - r))) + x is V22() real ext-real set
c₂₀ is V22() real ext-real Element of REAL
((min ((r - s),(x - r))) + x) - x is V22() real ext-real set
r - x is V22() real ext-real set
- (r - x) is V22() real ext-real set
- (r - s) is V22() real ext-real Element of REAL
x - r is V22() real ext-real set
(x - r) + r is V22() real ext-real set
s - r is V22() real ext-real Element of REAL
(s - r) + r is V22() real ext-real Element of REAL
(L | f) . x is V22() real ext-real Element of REAL
c₂₀ is V22() real ext-real Element of REAL
(x - r) + r is V22() real ext-real Element of REAL
[.(((L | f) . r) - (N1 / 2)),(((L | f) . r) + (N1 / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( ((L | f) . r) - (N1 / 2) <= b₁ & b₁ <= ((L | f) . r) + (N1 / 2) ) } is set
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fp is V22() real ext-real set
r1 - fp is V22() real ext-real Element of REAL
r1 + fp is V22() real ext-real Element of REAL
].(r1 - fp),(r1 + fp).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 - fp & not r1 + fp <= b₁ ) } is set
fm is V22() real ext-real Element of REAL
fm / 2 is V22() real ext-real Element of REAL
r1 - (fm / 2) is V22() real ext-real Element of REAL
r1 + (fm / 2) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : not b₁ <= r1 } is set
N1 is V22() real ext-real Element of REAL
(L | f) . N1 is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
N1 - r is V22() real ext-real Element of REAL
r - (N1 - r) is V22() real ext-real Element of REAL
r + (N1 - r) is V22() real ext-real Element of REAL
].(r - (N1 - r)),(r + (N1 - r)).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - (N1 - r) & not r + (N1 - r) <= b₁ ) } is set
N1 is open V84() V85() V86() Neighbourhood of r
r2 is V22() real ext-real set
x is open V84() V85() V86() Neighbourhood of r
(L | f) . r2 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : r1 <= b₁ } is set
s is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
[.(r1 - (fm / 2)),(r1 + (fm / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( r1 - (fm / 2) <= b₁ & b₁ <= r1 + (fm / 2) ) } is set
r1 - fm is V22() real ext-real Element of REAL
r1 + fm is V22() real ext-real Element of REAL
].(r1 - fm),(r1 + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 - fm & not r1 + fm <= b₁ ) } is set
r is open V84() V85() V86() Neighbourhood of (L | f) . r
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fp is open V84() V85() V86() Neighbourhood of r
(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
fp is open V84() V85() V86() Neighbourhood of (L | f) . r
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fm is open V84() V85() V86() Neighbourhood of (L | f) . r
R is V22() real ext-real set
((L | f) . r) - R is V22() real ext-real Element of REAL
((L | f) . r) + R is V22() real ext-real Element of REAL
].(((L | f) . r) - R),(((L | f) . r) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r) - R & not ((L | f) . r) + R <= b₁ ) } is set
N1 is V22() real ext-real Element of REAL
N1 / 2 is V22() real ext-real Element of REAL
((L | f) . r) + (N1 / 2) is V22() real ext-real Element of REAL
(((L | f) . r) + (N1 / 2)) + (N1 / 2) is V22() real ext-real Element of REAL
((L | f) . r) + N1 is V22() real ext-real Element of REAL
(((L | f) . r) + N1) - N1 is V22() real ext-real Element of REAL
((L | f) . r) - N1 is V22() real ext-real Element of REAL
].(((L | f) . r) - N1),(((L | f) . r) + N1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r) - N1 & not ((L | f) . r) + N1 <= b₁ ) } is set
x is V22() real ext-real Element of REAL
(L | f) . x is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
((L | f) . r) - (N1 / 2) is V22() real ext-real Element of REAL
(((L | f) . r) - N1) + (N1 / 2) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
(L | f) . s is V22() real ext-real Element of REAL
r - x is V22() real ext-real Element of REAL
s - r is V22() real ext-real Element of REAL
min ((s - r),(r - x)) is V22() real ext-real set
r - (min ((s - r),(r - x))) is V22() real ext-real set
r + (min ((s - r),(r - x))) is V22() real ext-real set
].(r - (min ((s - r),(r - x)))),(r + (min ((s - r),(r - x)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - (min ((s - r),(r - x))) & not r + (min ((s - r),(r - x))) <= b₁ ) } is set
s is open V84() V85() V86() Neighbourhood of r
x is V22() real ext-real set
N is open V84() V85() V86() Neighbourhood of r
(min ((s - r),(r - x))) + x is V22() real ext-real set
c₂₀ is V22() real ext-real Element of REAL
((min ((s - r),(r - x))) + x) - x is V22() real ext-real set
r - x is V22() real ext-real set
x - r is V22() real ext-real set
c₂₀ is V22() real ext-real Element of REAL
(s - r) + r is V22() real ext-real Element of REAL
(x - r) + r is V22() real ext-real set
(L | f) . x is V22() real ext-real Element of REAL
- (r - x) is V22() real ext-real set
- (r - x) is V22() real ext-real Element of REAL
x - r is V22() real ext-real Element of REAL
(x - r) + r is V22() real ext-real Element of REAL
[.(((L | f) . r) - (N1 / 2)),(((L | f) . r) + (N1 / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( ((L | f) . r) - (N1 / 2) <= b₁ & b₁ <= ((L | f) . r) + (N1 / 2) ) } is set
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fp is V22() real ext-real set
r1 - fp is V22() real ext-real Element of REAL
r1 + fp is V22() real ext-real Element of REAL
].(r1 - fp),(r1 + fp).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 - fp & not r1 + fp <= b₁ ) } is set
fm is V22() real ext-real Element of REAL
fm / 2 is V22() real ext-real Element of REAL
r1 - (fm / 2) is V22() real ext-real Element of REAL
r1 + (fm / 2) is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : not b₁ <= r1 } is set
N1 is V22() real ext-real Element of REAL
(L | f) . N1 is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
r - N1 is V22() real ext-real Element of REAL
r - (r - N1) is V22() real ext-real Element of REAL
r + (r - N1) is V22() real ext-real Element of REAL
].(r - (r - N1)),(r + (r - N1)).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - (r - N1) & not r + (r - N1) <= b₁ ) } is set
N1 is open V84() V85() V86() Neighbourhood of r
r2 is V22() real ext-real set
x is open V84() V85() V86() Neighbourhood of r
(L | f) . r2 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : r1 <= b₁ } is set
s is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
[.(r1 - (fm / 2)),(r1 + (fm / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( r1 - (fm / 2) <= b₁ & b₁ <= r1 + (fm / 2) ) } is set
r1 - fm is V22() real ext-real Element of REAL
r1 + fm is V22() real ext-real Element of REAL
].(r1 - fm),(r1 + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 - fm & not r1 + fm <= b₁ ) } is set
r is open V84() V85() V86() Neighbourhood of (L | f) . r
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fp is open V84() V85() V86() Neighbourhood of r
r is open V84() V85() V86() Neighbourhood of (L | f) . r
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fp is open V84() V85() V86() Neighbourhood of r
f is set
L is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom L is V84() V85() V86() Element of K19(REAL)
L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L .: f is V84() V85() V86() Element of K19(REAL)
r1 is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
].r1,x0.[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 & not x0 <= b₁ ) } is set
(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (L | f) is Element of K19(f)
K19(f) is set
r is V22() real ext-real set
(L | f) .: f is V84() V85() V86() Element of K19(REAL)
(dom L) /\ f is V84() V85() V86() Element of K19(REAL)
(L | f) . r is V22() real ext-real Element of REAL
fp is open V84() V85() V86() Neighbourhood of (L | f) . r
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fm is open V84() V85() V86() Neighbourhood of (L | f) . r
R is V22() real ext-real set
((L | f) . r) - R is V22() real ext-real Element of REAL
((L | f) . r) + R is V22() real ext-real Element of REAL
].(((L | f) . r) - R),(((L | f) . r) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r) - R & not ((L | f) . r) + R <= b₁ ) } is set
N1 is V22() real ext-real Element of REAL
N1 / 2 is V22() real ext-real Element of REAL
((L | f) . r) + (N1 / 2) is V22() real ext-real Element of REAL
(((L | f) . r) + (N1 / 2)) + (N1 / 2) is V22() real ext-real Element of REAL
((L | f) . r) + N1 is V22() real ext-real Element of REAL
(((L | f) . r) + N1) - N1 is V22() real ext-real Element of REAL
((L | f) . r) - N1 is V22() real ext-real Element of REAL
].(((L | f) . r) - N1),(((L | f) . r) + N1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r) - N1 & not ((L | f) . r) + N1 <= b₁ ) } is set
x is V22() real ext-real Element of REAL
(L | f) . x is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
((L | f) . r) - (N1 / 2) is V22() real ext-real Element of REAL
(((L | f) . r) - N1) + (N1 / 2) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
(L | f) . s is V22() real ext-real Element of REAL
x - r is V22() real ext-real Element of REAL
r - s is V22() real ext-real Element of REAL
min ((r - s),(x - r)) is V22() real ext-real set
r - (min ((r - s),(x - r))) is V22() real ext-real set
r + (min ((r - s),(x - r))) is V22() real ext-real set
].(r - (min ((r - s),(x - r)))),(r + (min ((r - s),(x - r)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - (min ((r - s),(x - r))) & not r + (min ((r - s),(x - r))) <= b₁ ) } is set
s is open V84() V85() V86() Neighbourhood of r
x is V22() real ext-real set
N is open V84() V85() V86() Neighbourhood of r
(min ((r - s),(x - r))) + x is V22() real ext-real set
c₂₀ is V22() real ext-real Element of REAL
((min ((r - s),(x - r))) + x) - x is V22() real ext-real set
r - x is V22() real ext-real set
- (r - x) is V22() real ext-real set
- (r - s) is V22() real ext-real Element of REAL
x - r is V22() real ext-real set
(x - r) + r is V22() real ext-real set
s - r is V22() real ext-real Element of REAL
(s - r) + r is V22() real ext-real Element of REAL
(L | f) . x is V22() real ext-real Element of REAL
c₂₀ is V22() real ext-real Element of REAL
(x - r) + r is V22() real ext-real Element of REAL
[.(((L | f) . r) - (N1 / 2)),(((L | f) . r) + (N1 / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( ((L | f) . r) - (N1 / 2) <= b₁ & b₁ <= ((L | f) . r) + (N1 / 2) ) } is set
(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (L | f) is Element of K19(f)
K19(f) is set
r is V22() real ext-real set
(L | f) .: f is V84() V85() V86() Element of K19(REAL)
(dom L) /\ f is V84() V85() V86() Element of K19(REAL)
(L | f) . r is V22() real ext-real Element of REAL
fp is open V84() V85() V86() Neighbourhood of (L | f) . r
r is open V84() V85() V86() Neighbourhood of (L | f) . r
fm is open V84() V85() V86() Neighbourhood of (L | f) . r
R is V22() real ext-real set
((L | f) . r) - R is V22() real ext-real Element of REAL
((L | f) . r) + R is V22() real ext-real Element of REAL
].(((L | f) . r) - R),(((L | f) . r) + R).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r) - R & not ((L | f) . r) + R <= b₁ ) } is set
N1 is V22() real ext-real Element of REAL
N1 / 2 is V22() real ext-real Element of REAL
((L | f) . r) + (N1 / 2) is V22() real ext-real Element of REAL
(((L | f) . r) + (N1 / 2)) + (N1 / 2) is V22() real ext-real Element of REAL
((L | f) . r) + N1 is V22() real ext-real Element of REAL
(((L | f) . r) + N1) - N1 is V22() real ext-real Element of REAL
((L | f) . r) - N1 is V22() real ext-real Element of REAL
].(((L | f) . r) - N1),(((L | f) . r) + N1).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r) - N1 & not ((L | f) . r) + N1 <= b₁ ) } is set
x is V22() real ext-real Element of REAL
(L | f) . x is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
((L | f) . r) - (N1 / 2) is V22() real ext-real Element of REAL
(((L | f) . r) - N1) + (N1 / 2) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
(L | f) . s is V22() real ext-real Element of REAL
r - x is V22() real ext-real Element of REAL
s - r is V22() real ext-real Element of REAL
min ((s - r),(r - x)) is V22() real ext-real set
r - (min ((s - r),(r - x))) is V22() real ext-real set
r + (min ((s - r),(r - x))) is V22() real ext-real set
].(r - (min ((s - r),(r - x)))),(r + (min ((s - r),(r - x)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - (min ((s - r),(r - x))) & not r + (min ((s - r),(r - x))) <= b₁ ) } is set
s is open V84() V85() V86() Neighbourhood of r
x is V22() real ext-real set
N is open V84() V85() V86() Neighbourhood of r
(min ((s - r),(r - x))) + x is V22() real ext-real set
c₂₀ is V22() real ext-real Element of REAL
((min ((s - r),(r - x))) + x) - x is V22() real ext-real set
r - x is V22() real ext-real set
x - r is V22() real ext-real set
c₂₀ is V22() real ext-real Element of REAL
(s - r) + r is V22() real ext-real Element of REAL
(x - r) + r is V22() real ext-real set
(L | f) . x is V22() real ext-real Element of REAL
- (r - x) is V22() real ext-real set
- (r - x) is V22() real ext-real Element of REAL
x - r is V22() real ext-real Element of REAL
(x - r) + r is V22() real ext-real Element of REAL
[.(((L | f) . r) - (N1 / 2)),(((L | f) . r) + (N1 / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( ((L | f) . r) - (N1 / 2) <= b₁ & b₁ <= ((L | f) . r) + (N1 / 2) ) } is set
f is set
L is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom L is V84() V85() V86() Element of K19(REAL)
L | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L .: f is V84() V85() V86() Element of K19(REAL)
(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (L | f) is Element of K19(f)
K19(f) is set
r1 is V22() real ext-real set
(L | f) .: f is V84() V85() V86() Element of K19(REAL)
(dom L) /\ f is V84() V85() V86() Element of K19(REAL)
(L | f) . r1 is V22() real ext-real Element of REAL
x0 is open V84() V85() V86() Neighbourhood of (L | f) . r1
N is V22() real ext-real set
((L | f) . r1) - N is V22() real ext-real Element of REAL
((L | f) . r1) + N is V22() real ext-real Element of REAL
].(((L | f) . r1) - N),(((L | f) . r1) + N).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r1) - N & not ((L | f) . r1) + N <= b₁ ) } is set
r is V22() real ext-real Element of REAL
r / 2 is V22() real ext-real Element of REAL
((L | f) . r1) + (r / 2) is V22() real ext-real Element of REAL
((L | f) . r1) - (r / 2) is V22() real ext-real Element of REAL
fp is V22() real ext-real Element of REAL
(L | f) . fp is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
R is V22() real ext-real Element of REAL
(L | f) . R is V22() real ext-real Element of REAL
R - r1 is V22() real ext-real Element of REAL
r1 - fp is V22() real ext-real Element of REAL
min ((r1 - fp),(R - r1)) is V22() real ext-real set
r1 - (min ((r1 - fp),(R - r1))) is V22() real ext-real set
r1 + (min ((r1 - fp),(R - r1))) is V22() real ext-real set
].(r1 - (min ((r1 - fp),(R - r1)))),(r1 + (min ((r1 - fp),(R - r1)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 - (min ((r1 - fp),(R - r1))) & not r1 + (min ((r1 - fp),(R - r1))) <= b₁ ) } is set
N1 is open V84() V85() V86() Neighbourhood of r1
r2 is V22() real ext-real set
x is open V84() V85() V86() Neighbourhood of r1
(((L | f) . r1) + (r / 2)) + (r / 2) is V22() real ext-real Element of REAL
((L | f) . r1) + r is V22() real ext-real Element of REAL
(((L | f) . r1) + r) - r is V22() real ext-real Element of REAL
((L | f) . r1) - r is V22() real ext-real Element of REAL
].(((L | f) . r1) - r),(((L | f) . r1) + r).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r1) - r & not ((L | f) . r1) + r <= b₁ ) } is set
(((L | f) . r1) - r) + (r / 2) is V22() real ext-real Element of REAL
[.(((L | f) . r1) - (r / 2)),(((L | f) . r1) + (r / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( ((L | f) . r1) - (r / 2) <= b₁ & b₁ <= ((L | f) . r1) + (r / 2) ) } is set
(min ((r1 - fp),(R - r1))) + r2 is V22() real ext-real set
s is V22() real ext-real Element of REAL
((min ((r1 - fp),(R - r1))) + r2) - r2 is V22() real ext-real set
r1 - r2 is V22() real ext-real set
- (r1 - r2) is V22() real ext-real set
- (r1 - fp) is V22() real ext-real Element of REAL
r2 - r1 is V22() real ext-real set
(r2 - r1) + r1 is V22() real ext-real set
fp - r1 is V22() real ext-real Element of REAL
(fp - r1) + r1 is V22() real ext-real Element of REAL
(L | f) . r2 is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
(R - r1) + r1 is V22() real ext-real Element of REAL
(L | f) | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom (L | f) is Element of K19(f)
K19(f) is set
r1 is V22() real ext-real set
(L | f) .: f is V84() V85() V86() Element of K19(REAL)
(dom L) /\ f is V84() V85() V86() Element of K19(REAL)
(L | f) . r1 is V22() real ext-real Element of REAL
x0 is open V84() V85() V86() Neighbourhood of (L | f) . r1
N is V22() real ext-real set
((L | f) . r1) - N is V22() real ext-real Element of REAL
((L | f) . r1) + N is V22() real ext-real Element of REAL
].(((L | f) . r1) - N),(((L | f) . r1) + N).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r1) - N & not ((L | f) . r1) + N <= b₁ ) } is set
r is V22() real ext-real Element of REAL
r / 2 is V22() real ext-real Element of REAL
((L | f) . r1) + (r / 2) is V22() real ext-real Element of REAL
((L | f) . r1) - (r / 2) is V22() real ext-real Element of REAL
fp is V22() real ext-real Element of REAL
(L | f) . fp is V22() real ext-real Element of REAL
f /\ (dom (L | f)) is Element of K19(f)
R is V22() real ext-real Element of REAL
(L | f) . R is V22() real ext-real Element of REAL
r1 - R is V22() real ext-real Element of REAL
fp - r1 is V22() real ext-real Element of REAL
min ((fp - r1),(r1 - R)) is V22() real ext-real set
r1 - (min ((fp - r1),(r1 - R))) is V22() real ext-real set
r1 + (min ((fp - r1),(r1 - R))) is V22() real ext-real set
].(r1 - (min ((fp - r1),(r1 - R)))),(r1 + (min ((fp - r1),(r1 - R)))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 - (min ((fp - r1),(r1 - R))) & not r1 + (min ((fp - r1),(r1 - R))) <= b₁ ) } is set
N1 is open V84() V85() V86() Neighbourhood of r1
r2 is V22() real ext-real set
x is open V84() V85() V86() Neighbourhood of r1
(((L | f) . r1) + (r / 2)) + (r / 2) is V22() real ext-real Element of REAL
((L | f) . r1) + r is V22() real ext-real Element of REAL
(((L | f) . r1) + r) - r is V22() real ext-real Element of REAL
((L | f) . r1) - r is V22() real ext-real Element of REAL
].(((L | f) . r1) - r),(((L | f) . r1) + r).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= ((L | f) . r1) - r & not ((L | f) . r1) + r <= b₁ ) } is set
(((L | f) . r1) - r) + (r / 2) is V22() real ext-real Element of REAL
[.(((L | f) . r1) - (r / 2)),(((L | f) . r1) + (r / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( ((L | f) . r1) - (r / 2) <= b₁ & b₁ <= ((L | f) . r1) + (r / 2) ) } is set
(min ((fp - r1),(r1 - R))) + r2 is V22() real ext-real set
s is V22() real ext-real Element of REAL
((min ((fp - r1),(r1 - R))) + r2) - r2 is V22() real ext-real set
r1 - r2 is V22() real ext-real set
r2 - r1 is V22() real ext-real set
s is V22() real ext-real Element of REAL
(fp - r1) + r1 is V22() real ext-real Element of REAL
(r2 - r1) + r1 is V22() real ext-real set
(L | f) . r2 is V22() real ext-real Element of REAL
- (r1 - r2) is V22() real ext-real set
- (r1 - R) is V22() real ext-real Element of REAL
R - r1 is V22() real ext-real Element of REAL
(R - r1) + r1 is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
L is V22() real ext-real Element of REAL
].f,L.[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= f & not L <= b₁ ) } is set
r1 is V1() V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
r1 | ].f,L.[ is V1() V4( REAL ) V4(].f,L.[) V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
dom r1 is V84() V85() V86() Element of K19(REAL)
(r1 | ].f,L.[) " is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
r1 .: ].f,L.[ is V84() V85() V86() Element of K19(REAL)
((r1 | ].f,L.[) ") | (r1 .: ].f,L.[) is V1() V4( REAL ) V4(r1 .: ].f,L.[) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
r1 . N is V22() real ext-real Element of REAL
(dom r1) /\ ].f,L.[ is V84() V85() V86() Element of K19(REAL)
dom (r1 | ].f,L.[) is V84() V85() V86() Element of K19(REAL)
(r1 | ].f,L.[) . N is V22() real ext-real Element of REAL
rng (r1 | ].f,L.[) is V84() V85() V86() Element of K19(REAL)
dom ((r1 | ].f,L.[) ") is V84() V85() V86() Element of K19(REAL)
((r1 | ].f,L.[) ") .: (r1 .: ].f,L.[) is V84() V85() V86() Element of K19(REAL)
((r1 | ].f,L.[) ") .: (rng (r1 | ].f,L.[)) is V84() V85() V86() Element of K19(REAL)
((r1 | ].f,L.[) ") .: (dom ((r1 | ].f,L.[) ")) is V84() V85() V86() Element of K19(REAL)
rng ((r1 | ].f,L.[) ") is V84() V85() V86() Element of K19(REAL)
x0 is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
r1 . N is V22() real ext-real Element of REAL
(dom r1) /\ ].f,L.[ is V84() V85() V86() Element of K19(REAL)
dom (r1 | ].f,L.[) is V84() V85() V86() Element of K19(REAL)
(r1 | ].f,L.[) . N is V22() real ext-real Element of REAL
rng (r1 | ].f,L.[) is V84() V85() V86() Element of K19(REAL)
dom ((r1 | ].f,L.[) ") is V84() V85() V86() Element of K19(REAL)
((r1 | ].f,L.[) ") .: (r1 .: ].f,L.[) is V84() V85() V86() Element of K19(REAL)
((r1 | ].f,L.[) ") .: (rng (r1 | ].f,L.[)) is V84() V85() V86() Element of K19(REAL)
((r1 | ].f,L.[) ") .: (dom ((r1 | ].f,L.[) ")) is V84() V85() V86() Element of K19(REAL)
rng ((r1 | ].f,L.[) ") is V84() V85() V86() Element of K19(REAL)
f is V22() real ext-real Element of REAL
halfline f is open V84() V85() V86() Element of K19(REAL)
K195(-infty,f) is V95() V96() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= -infty & not f <= b₁ ) } is set
L is V1() V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
L | (halfline f) is V1() V4( REAL ) V4( halfline f) V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
dom L is V84() V85() V86() Element of K19(REAL)
(L | (halfline f)) " is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L .: (halfline f) is V84() V85() V86() Element of K19(REAL)
((L | (halfline f)) ") | (L .: (halfline f)) is V1() V4( REAL ) V4(L .: (halfline f)) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
L . N is V22() real ext-real Element of REAL
(dom L) /\ (halfline f) is V84() V85() V86() Element of K19(REAL)
dom (L | (halfline f)) is V84() V85() V86() Element of K19(REAL)
(L | (halfline f)) . N is V22() real ext-real Element of REAL
rng (L | (halfline f)) is V84() V85() V86() Element of K19(REAL)
dom ((L | (halfline f)) ") is V84() V85() V86() Element of K19(REAL)
((L | (halfline f)) ") .: (L .: (halfline f)) is V84() V85() V86() Element of K19(REAL)
((L | (halfline f)) ") .: (rng (L | (halfline f))) is V84() V85() V86() Element of K19(REAL)
((L | (halfline f)) ") .: (dom ((L | (halfline f)) ")) is V84() V85() V86() Element of K19(REAL)
rng ((L | (halfline f)) ") is V84() V85() V86() Element of K19(REAL)
x0 is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
L . N is V22() real ext-real Element of REAL
(dom L) /\ (halfline f) is V84() V85() V86() Element of K19(REAL)
dom (L | (halfline f)) is V84() V85() V86() Element of K19(REAL)
(L | (halfline f)) . N is V22() real ext-real Element of REAL
rng (L | (halfline f)) is V84() V85() V86() Element of K19(REAL)
dom ((L | (halfline f)) ") is V84() V85() V86() Element of K19(REAL)
((L | (halfline f)) ") .: (L .: (halfline f)) is V84() V85() V86() Element of K19(REAL)
((L | (halfline f)) ") .: (rng (L | (halfline f))) is V84() V85() V86() Element of K19(REAL)
((L | (halfline f)) ") .: (dom ((L | (halfline f)) ")) is V84() V85() V86() Element of K19(REAL)
rng ((L | (halfline f)) ") is V84() V85() V86() Element of K19(REAL)
f is V22() real ext-real Element of REAL
right_open_halfline f is open V84() V85() V86() Element of K19(REAL)
K195(f,+infty) is V95() V96() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= f & not +infty <= b₁ ) } is set
L is V1() V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
L | (right_open_halfline f) is V1() V4( REAL ) V4( right_open_halfline f) V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
dom L is V84() V85() V86() Element of K19(REAL)
(L | (right_open_halfline f)) " is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L .: (right_open_halfline f) is V84() V85() V86() Element of K19(REAL)
((L | (right_open_halfline f)) ") | (L .: (right_open_halfline f)) is V1() V4( REAL ) V4(L .: (right_open_halfline f)) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
L . N is V22() real ext-real Element of REAL
(dom L) /\ (right_open_halfline f) is V84() V85() V86() Element of K19(REAL)
dom (L | (right_open_halfline f)) is V84() V85() V86() Element of K19(REAL)
(L | (right_open_halfline f)) . N is V22() real ext-real Element of REAL
rng (L | (right_open_halfline f)) is V84() V85() V86() Element of K19(REAL)
dom ((L | (right_open_halfline f)) ") is V84() V85() V86() Element of K19(REAL)
((L | (right_open_halfline f)) ") .: (L .: (right_open_halfline f)) is V84() V85() V86() Element of K19(REAL)
((L | (right_open_halfline f)) ") .: (rng (L | (right_open_halfline f))) is V84() V85() V86() Element of K19(REAL)
((L | (right_open_halfline f)) ") .: (dom ((L | (right_open_halfline f)) ")) is V84() V85() V86() Element of K19(REAL)
rng ((L | (right_open_halfline f)) ") is V84() V85() V86() Element of K19(REAL)
x0 is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
L . N is V22() real ext-real Element of REAL
(dom L) /\ (right_open_halfline f) is V84() V85() V86() Element of K19(REAL)
dom (L | (right_open_halfline f)) is V84() V85() V86() Element of K19(REAL)
(L | (right_open_halfline f)) . N is V22() real ext-real Element of REAL
rng (L | (right_open_halfline f)) is V84() V85() V86() Element of K19(REAL)
dom ((L | (right_open_halfline f)) ") is V84() V85() V86() Element of K19(REAL)
((L | (right_open_halfline f)) ") .: (L .: (right_open_halfline f)) is V84() V85() V86() Element of K19(REAL)
((L | (right_open_halfline f)) ") .: (rng (L | (right_open_halfline f))) is V84() V85() V86() Element of K19(REAL)
((L | (right_open_halfline f)) ") .: (dom ((L | (right_open_halfline f)) ")) is V84() V85() V86() Element of K19(REAL)
rng ((L | (right_open_halfline f)) ") is V84() V85() V86() Element of K19(REAL)
f is V22() real ext-real Element of REAL
left_closed_halfline f is closed V84() V85() V86() Element of K19(REAL)
K194(-infty,f) is V95() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= -infty & b₁ <= f ) } is set
L is V1() V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
L | (left_closed_halfline f) is V1() V4( REAL ) V4( left_closed_halfline f) V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
dom L is V84() V85() V86() Element of K19(REAL)
(L | (left_closed_halfline f)) " is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L .: (left_closed_halfline f) is V84() V85() V86() Element of K19(REAL)
((L | (left_closed_halfline f)) ") | (L .: (left_closed_halfline f)) is V1() V4( REAL ) V4(L .: (left_closed_halfline f)) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
L . N is V22() real ext-real Element of REAL
(dom L) /\ (left_closed_halfline f) is V84() V85() V86() Element of K19(REAL)
dom (L | (left_closed_halfline f)) is V84() V85() V86() Element of K19(REAL)
(L | (left_closed_halfline f)) . N is V22() real ext-real Element of REAL
rng (L | (left_closed_halfline f)) is V84() V85() V86() Element of K19(REAL)
dom ((L | (left_closed_halfline f)) ") is V84() V85() V86() Element of K19(REAL)
((L | (left_closed_halfline f)) ") .: (L .: (left_closed_halfline f)) is V84() V85() V86() Element of K19(REAL)
((L | (left_closed_halfline f)) ") .: (rng (L | (left_closed_halfline f))) is V84() V85() V86() Element of K19(REAL)
((L | (left_closed_halfline f)) ") .: (dom ((L | (left_closed_halfline f)) ")) is V84() V85() V86() Element of K19(REAL)
rng ((L | (left_closed_halfline f)) ") is V84() V85() V86() Element of K19(REAL)
x0 is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
L . N is V22() real ext-real Element of REAL
(dom L) /\ (left_closed_halfline f) is V84() V85() V86() Element of K19(REAL)
dom (L | (left_closed_halfline f)) is V84() V85() V86() Element of K19(REAL)
(L | (left_closed_halfline f)) . N is V22() real ext-real Element of REAL
rng (L | (left_closed_halfline f)) is V84() V85() V86() Element of K19(REAL)
dom ((L | (left_closed_halfline f)) ") is V84() V85() V86() Element of K19(REAL)
((L | (left_closed_halfline f)) ") .: (L .: (left_closed_halfline f)) is V84() V85() V86() Element of K19(REAL)
((L | (left_closed_halfline f)) ") .: (rng (L | (left_closed_halfline f))) is V84() V85() V86() Element of K19(REAL)
((L | (left_closed_halfline f)) ") .: (dom ((L | (left_closed_halfline f)) ")) is V84() V85() V86() Element of K19(REAL)
rng ((L | (left_closed_halfline f)) ") is V84() V85() V86() Element of K19(REAL)
f is V22() real ext-real Element of REAL
right_closed_halfline f is closed V84() V85() V86() Element of K19(REAL)
K193(f,+infty) is V96() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f <= b₁ & not +infty <= b₁ ) } is set
L is V1() V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
L | (right_closed_halfline f) is V1() V4( REAL ) V4( right_closed_halfline f) V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
dom L is V84() V85() V86() Element of K19(REAL)
(L | (right_closed_halfline f)) " is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L .: (right_closed_halfline f) is V84() V85() V86() Element of K19(REAL)
((L | (right_closed_halfline f)) ") | (L .: (right_closed_halfline f)) is V1() V4( REAL ) V4(L .: (right_closed_halfline f)) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
x0 is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
L . N is V22() real ext-real Element of REAL
(dom L) /\ (right_closed_halfline f) is V84() V85() V86() Element of K19(REAL)
dom (L | (right_closed_halfline f)) is V84() V85() V86() Element of K19(REAL)
(L | (right_closed_halfline f)) . N is V22() real ext-real Element of REAL
rng (L | (right_closed_halfline f)) is V84() V85() V86() Element of K19(REAL)
dom ((L | (right_closed_halfline f)) ") is V84() V85() V86() Element of K19(REAL)
((L | (right_closed_halfline f)) ") .: (L .: (right_closed_halfline f)) is V84() V85() V86() Element of K19(REAL)
((L | (right_closed_halfline f)) ") .: (rng (L | (right_closed_halfline f))) is V84() V85() V86() Element of K19(REAL)
((L | (right_closed_halfline f)) ") .: (dom ((L | (right_closed_halfline f)) ")) is V84() V85() V86() Element of K19(REAL)
rng ((L | (right_closed_halfline f)) ") is V84() V85() V86() Element of K19(REAL)
x0 is V22() real ext-real Element of REAL
N is V22() real ext-real Element of REAL
L . N is V22() real ext-real Element of REAL
(dom L) /\ (right_closed_halfline f) is V84() V85() V86() Element of K19(REAL)
dom (L | (right_closed_halfline f)) is V84() V85() V86() Element of K19(REAL)
(L | (right_closed_halfline f)) . N is V22() real ext-real Element of REAL
rng (L | (right_closed_halfline f)) is V84() V85() V86() Element of K19(REAL)
dom ((L | (right_closed_halfline f)) ") is V84() V85() V86() Element of K19(REAL)
((L | (right_closed_halfline f)) ") .: (L .: (right_closed_halfline f)) is V84() V85() V86() Element of K19(REAL)
((L | (right_closed_halfline f)) ") .: (rng (L | (right_closed_halfline f))) is V84() V85() V86() Element of K19(REAL)
((L | (right_closed_halfline f)) ") .: (dom ((L | (right_closed_halfline f)) ")) is V84() V85() V86() Element of K19(REAL)
rng ((L | (right_closed_halfline f)) ") is V84() V85() V86() Element of K19(REAL)
L is V1() V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
L | ([#] REAL) is V1() V4( REAL ) V4( [#] REAL) V4( REAL ) V5( REAL ) Function-like one-to-one V33() V34() V35() Element of K19(K20(REAL,REAL))
L " is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
rng L is V84() V85() V86() Element of K19(REAL)
(L ") | (rng L) is V1() V4( REAL ) V4( rng L) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom L is V84() V85() V86() Element of K19(REAL)
r1 is V22() real ext-real Element of REAL
L .: ([#] REAL) is V84() V85() V86() Element of K19(REAL)
x0 is V22() real ext-real Element of REAL
L . x0 is V22() real ext-real Element of REAL
(dom L) /\ ([#] REAL) is V84() V85() V86() Element of K19(REAL)
dom (L | ([#] REAL)) is V84() V85() V86() Element of K19(([#] REAL))
K19(([#] REAL)) is set
(L | ([#] REAL)) . x0 is V22() real ext-real Element of REAL
rng (L | ([#] REAL)) is V84() V85() V86() Element of K19(REAL)
(L | ([#] REAL)) " is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom ((L | ([#] REAL)) ") is V84() V85() V86() Element of K19(REAL)
((L | ([#] REAL)) ") .: (L .: ([#] REAL)) is V84() V85() V86() Element of K19(REAL)
((L | ([#] REAL)) ") .: (rng (L | ([#] REAL))) is V84() V85() V86() Element of K19(REAL)
((L | ([#] REAL)) ") .: (dom ((L | ([#] REAL)) ")) is V84() V85() V86() Element of K19(REAL)
rng ((L | ([#] REAL)) ") is V84() V85() V86() Element of K19(REAL)
((L | ([#] REAL)) ") | (L .: ([#] REAL)) is V1() V4( REAL ) V4(L .: ([#] REAL)) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((L | ([#] REAL)) ") | (rng L) is V1() V4( REAL ) V4( rng L) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
r1 is V22() real ext-real Element of REAL
L .: ([#] REAL) is V84() V85() V86() Element of K19(REAL)
x0 is V22() real ext-real Element of REAL
L . x0 is V22() real ext-real Element of REAL
(dom L) /\ ([#] REAL) is V84() V85() V86() Element of K19(REAL)
dom (L | ([#] REAL)) is V84() V85() V86() Element of K19(([#] REAL))
K19(([#] REAL)) is set
(L | ([#] REAL)) . x0 is V22() real ext-real Element of REAL
rng (L | ([#] REAL)) is V84() V85() V86() Element of K19(REAL)
(L | ([#] REAL)) " is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom ((L | ([#] REAL)) ") is V84() V85() V86() Element of K19(REAL)
((L | ([#] REAL)) ") .: (L .: ([#] REAL)) is V84() V85() V86() Element of K19(REAL)
((L | ([#] REAL)) ") .: (rng (L | ([#] REAL))) is V84() V85() V86() Element of K19(REAL)
((L | ([#] REAL)) ") .: (dom ((L | ([#] REAL)) ")) is V84() V85() V86() Element of K19(REAL)
rng ((L | ([#] REAL)) ") is V84() V85() V86() Element of K19(REAL)
((L | ([#] REAL)) ") | (L .: ([#] REAL)) is V1() V4( REAL ) V4(L .: ([#] REAL)) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
((L | ([#] REAL)) ") | (rng L) is V1() V4( REAL ) V4( rng L) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
f is V22() real ext-real Element of REAL
L is V22() real ext-real Element of REAL
].f,L.[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= f & not L <= b₁ ) } is set
r1 is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom r1 is V84() V85() V86() Element of K19(REAL)
r1 | ].f,L.[ is V1() V4( REAL ) V4(].f,L.[) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
rng (r1 | ].f,L.[) is V84() V85() V86() Element of K19(REAL)
x0 is V22() real ext-real set
dom (r1 | ].f,L.[) is V84() V85() V86() Element of K19(REAL)
r is V22() real ext-real Element of REAL
(r1 | ].f,L.[) . r is V22() real ext-real Element of REAL
r1 . r is V22() real ext-real Element of REAL
(dom r1) /\ ].f,L.[ is V84() V85() V86() Element of K19(REAL)
r is open V84() V85() V86() Neighbourhood of r
fp is V22() real ext-real set
r - fp is V22() real ext-real Element of REAL
r + fp is V22() real ext-real Element of REAL
].(r - fp),(r + fp).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - fp & not r + fp <= b₁ ) } is set
fm is V22() real ext-real Element of REAL
fm / 2 is V22() real ext-real Element of REAL
r - 0 is V22() real ext-real Element of REAL
r - (fm / 2) is V22() real ext-real Element of REAL
r - fm is V22() real ext-real Element of REAL
r + (fm / 2) is V22() real ext-real Element of REAL
r1 . (r + (fm / 2)) is V22() real ext-real Element of REAL
r1 . (r - (fm / 2)) is V22() real ext-real Element of REAL
r + fm is V22() real ext-real Element of REAL
].(r - fm),(r + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - fm & not r + fm <= b₁ ) } is set
].f,L.[ /\ (dom r1) is V84() V85() V86() Element of K19(REAL)
[.(r - (fm / 2)),(r + (fm / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( r - (fm / 2) <= b₁ & b₁ <= r + (fm / 2) ) } is set
r1 | [.(r - (fm / 2)),(r + (fm / 2)).] is V1() V4( REAL ) V4([.(r - (fm / 2)),(r + (fm / 2)).]) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(r1 . r) - (r1 . (r - (fm / 2))) is V22() real ext-real Element of REAL
(r1 . (r + (fm / 2))) - (r1 . r) is V22() real ext-real Element of REAL
min (((r1 . r) - (r1 . (r - (fm / 2)))),((r1 . (r + (fm / 2))) - (r1 . r))) is V22() real ext-real set
x0 - (min (((r1 . r) - (r1 . (r - (fm / 2)))),((r1 . (r + (fm / 2))) - (r1 . r)))) is V22() real ext-real set
x0 + (min (((r1 . r) - (r1 . (r - (fm / 2)))),((r1 . (r + (fm / 2))) - (r1 . r)))) is V22() real ext-real set
].(x0 - (min (((r1 . r) - (r1 . (r - (fm / 2)))),((r1 . (r + (fm / 2))) - (r1 . r))))),(x0 + (min (((r1 . r) - (r1 . (r - (fm / 2)))),((r1 . (r + (fm / 2))) - (r1 . r))))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= x0 - (min (((r1 . r) - (r1 . (r - (fm / 2)))),((r1 . (r + (fm / 2))) - (r1 . r)))) & not x0 + (min (((r1 . r) - (r1 . (r - (fm / 2)))),((r1 . (r + (fm / 2))) - (r1 . r)))) <= b₁ ) } is set
x is open V84() V85() V86() Neighbourhood of x0
[.(r1 . (r + (fm / 2))),(r1 . (r - (fm / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( r1 . (r + (fm / 2)) <= b₁ & b₁ <= r1 . (r - (fm / 2)) ) } is set
[.(r1 . (r - (fm / 2))),(r1 . (r + (fm / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( r1 . (r - (fm / 2)) <= b₁ & b₁ <= r1 . (r + (fm / 2)) ) } is set
[.(r1 . (r - (fm / 2))),(r1 . (r + (fm / 2))).] \/ [.(r1 . (r + (fm / 2))),(r1 . (r - (fm / 2))).] is V84() V85() V86() Element of K19(REAL)
r2 is open V84() V85() V86() Neighbourhood of x0
s is set
].(r1 . (r - (fm / 2))),(r1 . (r + (fm / 2))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 . (r - (fm / 2)) & not r1 . (r + (fm / 2)) <= b₁ ) } is set
(r1 . r) - (min (((r1 . r) - (r1 . (r - (fm / 2)))),((r1 . (r + (fm / 2))) - (r1 . r)))) is V22() real ext-real Element of REAL
(r1 . r) + (min (((r1 . r) - (r1 . (r - (fm / 2)))),((r1 . (r + (fm / 2))) - (r1 . r)))) is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
(r1 . r) + ((r1 . (r + (fm / 2))) - (r1 . r)) is V22() real ext-real Element of REAL
(r1 . r) - ((r1 . r) - (r1 . (r - (fm / 2)))) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
r1 . s is V22() real ext-real Element of REAL
(r1 | ].f,L.[) . s is V22() real ext-real Element of REAL
(r1 . (r - (fm / 2))) - (r1 . r) is V22() real ext-real Element of REAL
(r1 . r) - (r1 . (r + (fm / 2))) is V22() real ext-real Element of REAL
min (((r1 . (r - (fm / 2))) - (r1 . r)),((r1 . r) - (r1 . (r + (fm / 2))))) is V22() real ext-real set
x0 - (min (((r1 . (r - (fm / 2))) - (r1 . r)),((r1 . r) - (r1 . (r + (fm / 2)))))) is V22() real ext-real set
x0 + (min (((r1 . (r - (fm / 2))) - (r1 . r)),((r1 . r) - (r1 . (r + (fm / 2)))))) is V22() real ext-real set
].(x0 - (min (((r1 . (r - (fm / 2))) - (r1 . r)),((r1 . r) - (r1 . (r + (fm / 2))))))),(x0 + (min (((r1 . (r - (fm / 2))) - (r1 . r)),((r1 . r) - (r1 . (r + (fm / 2))))))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= x0 - (min (((r1 . (r - (fm / 2))) - (r1 . r)),((r1 . r) - (r1 . (r + (fm / 2)))))) & not x0 + (min (((r1 . (r - (fm / 2))) - (r1 . r)),((r1 . r) - (r1 . (r + (fm / 2)))))) <= b₁ ) } is set
x is open V84() V85() V86() Neighbourhood of x0
[.(r1 . (r - (fm / 2))),(r1 . (r + (fm / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( r1 . (r - (fm / 2)) <= b₁ & b₁ <= r1 . (r + (fm / 2)) ) } is set
[.(r1 . (r + (fm / 2))),(r1 . (r - (fm / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( r1 . (r + (fm / 2)) <= b₁ & b₁ <= r1 . (r - (fm / 2)) ) } is set
[.(r1 . (r - (fm / 2))),(r1 . (r + (fm / 2))).] \/ [.(r1 . (r + (fm / 2))),(r1 . (r - (fm / 2))).] is V84() V85() V86() Element of K19(REAL)
r2 is open V84() V85() V86() Neighbourhood of x0
s is set
].(r1 . (r + (fm / 2))),(r1 . (r - (fm / 2))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 . (r + (fm / 2)) & not r1 . (r - (fm / 2)) <= b₁ ) } is set
(r1 . r) - (min (((r1 . (r - (fm / 2))) - (r1 . r)),((r1 . r) - (r1 . (r + (fm / 2)))))) is V22() real ext-real Element of REAL
(r1 . r) + (min (((r1 . (r - (fm / 2))) - (r1 . r)),((r1 . r) - (r1 . (r + (fm / 2)))))) is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
(r1 . r) + ((r1 . (r - (fm / 2))) - (r1 . r)) is V22() real ext-real Element of REAL
(r1 . r) - ((r1 . r) - (r1 . (r + (fm / 2)))) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
r1 . s is V22() real ext-real Element of REAL
(r1 | ].f,L.[) . s is V22() real ext-real Element of REAL
N1 is open V84() V85() V86() Neighbourhood of x0
f is V22() real ext-real Element of REAL
halfline f is open V84() V85() V86() Element of K19(REAL)
K195(-infty,f) is V95() V96() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= -infty & not f <= b₁ ) } is set
L is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom L is V84() V85() V86() Element of K19(REAL)
L | (halfline f) is V1() V4( REAL ) V4( halfline f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
rng (L | (halfline f)) is V84() V85() V86() Element of K19(REAL)
x0 is V22() real ext-real set
dom (L | (halfline f)) is V84() V85() V86() Element of K19(REAL)
r is V22() real ext-real Element of REAL
(L | (halfline f)) . r is V22() real ext-real Element of REAL
L . r is V22() real ext-real Element of REAL
(dom L) /\ (halfline f) is V84() V85() V86() Element of K19(REAL)
r is open V84() V85() V86() Neighbourhood of r
fp is V22() real ext-real set
r - fp is V22() real ext-real Element of REAL
r + fp is V22() real ext-real Element of REAL
].(r - fp),(r + fp).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - fp & not r + fp <= b₁ ) } is set
fm is V22() real ext-real Element of REAL
fm / 2 is V22() real ext-real Element of REAL
r - 0 is V22() real ext-real Element of REAL
r - (fm / 2) is V22() real ext-real Element of REAL
r - fm is V22() real ext-real Element of REAL
r + (fm / 2) is V22() real ext-real Element of REAL
L . (r + (fm / 2)) is V22() real ext-real Element of REAL
L . (r - (fm / 2)) is V22() real ext-real Element of REAL
r + fm is V22() real ext-real Element of REAL
].(r - fm),(r + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - fm & not r + fm <= b₁ ) } is set
(halfline f) /\ (dom L) is V84() V85() V86() Element of K19(REAL)
[.(r - (fm / 2)),(r + (fm / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( r - (fm / 2) <= b₁ & b₁ <= r + (fm / 2) ) } is set
L | r is V1() V4( REAL ) V4(r) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L | [.(r - (fm / 2)),(r + (fm / 2)).] is V1() V4( REAL ) V4([.(r - (fm / 2)),(r + (fm / 2)).]) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(L . r) - (L . (r - (fm / 2))) is V22() real ext-real Element of REAL
(L . (r + (fm / 2))) - (L . r) is V22() real ext-real Element of REAL
min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r))) is V22() real ext-real set
x0 - (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r)))) is V22() real ext-real set
x0 + (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r)))) is V22() real ext-real set
].(x0 - (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r))))),(x0 + (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r))))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= x0 - (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r)))) & not x0 + (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r)))) <= b₁ ) } is set
x is open V84() V85() V86() Neighbourhood of x0
[.(L . (r + (fm / 2))),(L . (r - (fm / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( L . (r + (fm / 2)) <= b₁ & b₁ <= L . (r - (fm / 2)) ) } is set
[.(L . (r - (fm / 2))),(L . (r + (fm / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( L . (r - (fm / 2)) <= b₁ & b₁ <= L . (r + (fm / 2)) ) } is set
[.(L . (r - (fm / 2))),(L . (r + (fm / 2))).] \/ [.(L . (r + (fm / 2))),(L . (r - (fm / 2))).] is V84() V85() V86() Element of K19(REAL)
r2 is open V84() V85() V86() Neighbourhood of x0
s is set
].(L . (r - (fm / 2))),(L . (r + (fm / 2))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= L . (r - (fm / 2)) & not L . (r + (fm / 2)) <= b₁ ) } is set
(L . r) - (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r)))) is V22() real ext-real Element of REAL
(L . r) + (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r)))) is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
(L . r) + ((L . (r + (fm / 2))) - (L . r)) is V22() real ext-real Element of REAL
(L . r) - ((L . r) - (L . (r - (fm / 2)))) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
L . s is V22() real ext-real Element of REAL
(L | (halfline f)) . s is V22() real ext-real Element of REAL
(L . (r - (fm / 2))) - (L . r) is V22() real ext-real Element of REAL
(L . r) - (L . (r + (fm / 2))) is V22() real ext-real Element of REAL
min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2))))) is V22() real ext-real set
x0 - (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2)))))) is V22() real ext-real set
x0 + (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2)))))) is V22() real ext-real set
].(x0 - (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2))))))),(x0 + (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2))))))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= x0 - (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2)))))) & not x0 + (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2)))))) <= b₁ ) } is set
x is open V84() V85() V86() Neighbourhood of x0
[.(L . (r - (fm / 2))),(L . (r + (fm / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( L . (r - (fm / 2)) <= b₁ & b₁ <= L . (r + (fm / 2)) ) } is set
[.(L . (r + (fm / 2))),(L . (r - (fm / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( L . (r + (fm / 2)) <= b₁ & b₁ <= L . (r - (fm / 2)) ) } is set
[.(L . (r - (fm / 2))),(L . (r + (fm / 2))).] \/ [.(L . (r + (fm / 2))),(L . (r - (fm / 2))).] is V84() V85() V86() Element of K19(REAL)
r2 is open V84() V85() V86() Neighbourhood of x0
s is set
].(L . (r + (fm / 2))),(L . (r - (fm / 2))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= L . (r + (fm / 2)) & not L . (r - (fm / 2)) <= b₁ ) } is set
(L . r) - (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2)))))) is V22() real ext-real Element of REAL
(L . r) + (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2)))))) is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
(L . r) + ((L . (r - (fm / 2))) - (L . r)) is V22() real ext-real Element of REAL
(L . r) - ((L . r) - (L . (r + (fm / 2)))) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
L . s is V22() real ext-real Element of REAL
(L | (halfline f)) . s is V22() real ext-real Element of REAL
N1 is open V84() V85() V86() Neighbourhood of x0
f is V22() real ext-real Element of REAL
right_open_halfline f is open V84() V85() V86() Element of K19(REAL)
K195(f,+infty) is V95() V96() V100() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= f & not +infty <= b₁ ) } is set
L is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom L is V84() V85() V86() Element of K19(REAL)
L | (right_open_halfline f) is V1() V4( REAL ) V4( right_open_halfline f) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
rng (L | (right_open_halfline f)) is V84() V85() V86() Element of K19(REAL)
x0 is V22() real ext-real set
dom (L | (right_open_halfline f)) is V84() V85() V86() Element of K19(REAL)
r is V22() real ext-real Element of REAL
(L | (right_open_halfline f)) . r is V22() real ext-real Element of REAL
L . r is V22() real ext-real Element of REAL
(dom L) /\ (right_open_halfline f) is V84() V85() V86() Element of K19(REAL)
r is open V84() V85() V86() Neighbourhood of r
fp is V22() real ext-real set
r - fp is V22() real ext-real Element of REAL
r + fp is V22() real ext-real Element of REAL
].(r - fp),(r + fp).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - fp & not r + fp <= b₁ ) } is set
fm is V22() real ext-real Element of REAL
fm / 2 is V22() real ext-real Element of REAL
r - 0 is V22() real ext-real Element of REAL
r - (fm / 2) is V22() real ext-real Element of REAL
r - fm is V22() real ext-real Element of REAL
r + (fm / 2) is V22() real ext-real Element of REAL
L . (r + (fm / 2)) is V22() real ext-real Element of REAL
L . (r - (fm / 2)) is V22() real ext-real Element of REAL
r + fm is V22() real ext-real Element of REAL
].(r - fm),(r + fm).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r - fm & not r + fm <= b₁ ) } is set
(right_open_halfline f) /\ (dom L) is V84() V85() V86() Element of K19(REAL)
[.(r - (fm / 2)),(r + (fm / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( r - (fm / 2) <= b₁ & b₁ <= r + (fm / 2) ) } is set
L | r is V1() V4( REAL ) V4(r) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
L | [.(r - (fm / 2)),(r + (fm / 2)).] is V1() V4( REAL ) V4([.(r - (fm / 2)),(r + (fm / 2)).]) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
(L . r) - (L . (r - (fm / 2))) is V22() real ext-real Element of REAL
(L . (r + (fm / 2))) - (L . r) is V22() real ext-real Element of REAL
min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r))) is V22() real ext-real set
x0 - (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r)))) is V22() real ext-real set
x0 + (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r)))) is V22() real ext-real set
].(x0 - (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r))))),(x0 + (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r))))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= x0 - (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r)))) & not x0 + (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r)))) <= b₁ ) } is set
x is open V84() V85() V86() Neighbourhood of x0
[.(L . (r + (fm / 2))),(L . (r - (fm / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( L . (r + (fm / 2)) <= b₁ & b₁ <= L . (r - (fm / 2)) ) } is set
[.(L . (r - (fm / 2))),(L . (r + (fm / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( L . (r - (fm / 2)) <= b₁ & b₁ <= L . (r + (fm / 2)) ) } is set
[.(L . (r - (fm / 2))),(L . (r + (fm / 2))).] \/ [.(L . (r + (fm / 2))),(L . (r - (fm / 2))).] is V84() V85() V86() Element of K19(REAL)
r2 is open V84() V85() V86() Neighbourhood of x0
s is set
].(L . (r - (fm / 2))),(L . (r + (fm / 2))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= L . (r - (fm / 2)) & not L . (r + (fm / 2)) <= b₁ ) } is set
(L . r) - (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r)))) is V22() real ext-real Element of REAL
(L . r) + (min (((L . r) - (L . (r - (fm / 2)))),((L . (r + (fm / 2))) - (L . r)))) is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
(L . r) + ((L . (r + (fm / 2))) - (L . r)) is V22() real ext-real Element of REAL
(L . r) - ((L . r) - (L . (r - (fm / 2)))) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
L . s is V22() real ext-real Element of REAL
(L | (right_open_halfline f)) . s is V22() real ext-real Element of REAL
(L . (r - (fm / 2))) - (L . r) is V22() real ext-real Element of REAL
(L . r) - (L . (r + (fm / 2))) is V22() real ext-real Element of REAL
min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2))))) is V22() real ext-real set
x0 - (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2)))))) is V22() real ext-real set
x0 + (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2)))))) is V22() real ext-real set
].(x0 - (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2))))))),(x0 + (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2))))))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= x0 - (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2)))))) & not x0 + (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2)))))) <= b₁ ) } is set
x is open V84() V85() V86() Neighbourhood of x0
[.(L . (r - (fm / 2))),(L . (r + (fm / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( L . (r - (fm / 2)) <= b₁ & b₁ <= L . (r + (fm / 2)) ) } is set
[.(L . (r + (fm / 2))),(L . (r - (fm / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( L . (r + (fm / 2)) <= b₁ & b₁ <= L . (r - (fm / 2)) ) } is set
[.(L . (r - (fm / 2))),(L . (r + (fm / 2))).] \/ [.(L . (r + (fm / 2))),(L . (r - (fm / 2))).] is V84() V85() V86() Element of K19(REAL)
r2 is open V84() V85() V86() Neighbourhood of x0
s is set
].(L . (r + (fm / 2))),(L . (r - (fm / 2))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= L . (r + (fm / 2)) & not L . (r - (fm / 2)) <= b₁ ) } is set
(L . r) - (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2)))))) is V22() real ext-real Element of REAL
(L . r) + (min (((L . (r - (fm / 2))) - (L . r)),((L . r) - (L . (r + (fm / 2)))))) is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
(L . r) + ((L . (r - (fm / 2))) - (L . r)) is V22() real ext-real Element of REAL
(L . r) - ((L . r) - (L . (r + (fm / 2)))) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
L . s is V22() real ext-real Element of REAL
(L | (right_open_halfline f)) . s is V22() real ext-real Element of REAL
N1 is open V84() V85() V86() Neighbourhood of x0
f is V1() V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
dom f is V84() V85() V86() Element of K19(REAL)
f | ([#] REAL) is V1() V4( REAL ) V4( [#] REAL) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
rng f is V84() V85() V86() Element of K19(REAL)
r1 is V22() real ext-real set
x0 is V22() real ext-real Element of REAL
f . x0 is V22() real ext-real Element of REAL
([#] REAL) /\ (dom f) is V84() V85() V86() Element of K19(REAL)
the open V84() V85() V86() Neighbourhood of x0 is open V84() V85() V86() Neighbourhood of x0
r is V22() real ext-real set
x0 - r is V22() real ext-real Element of REAL
x0 + r is V22() real ext-real Element of REAL
].(x0 - r),(x0 + r).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
r is V22() real ext-real Element of REAL
r / 2 is V22() real ext-real Element of REAL
x0 - 0 is V22() real ext-real Element of REAL
x0 - (r / 2) is V22() real ext-real Element of REAL
x0 - r is V22() real ext-real Element of REAL
x0 + r is V22() real ext-real Element of REAL
x0 + (r / 2) is V22() real ext-real Element of REAL
f . (x0 + (r / 2)) is V22() real ext-real Element of REAL
f . (x0 - (r / 2)) is V22() real ext-real Element of REAL
[.(x0 - (r / 2)),(x0 + (r / 2)).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( x0 - (r / 2) <= b₁ & b₁ <= x0 + (r / 2) ) } is set
f | [.(x0 - (r / 2)),(x0 + (r / 2)).] is V1() V4( REAL ) V4([.(x0 - (r / 2)),(x0 + (r / 2)).]) V4( REAL ) V5( REAL ) Function-like V33() V34() V35() Element of K19(K20(REAL,REAL))
].(x0 - r),(x0 + r).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= x0 - r & not x0 + r <= b₁ ) } is set
(f . x0) - (f . (x0 - (r / 2))) is V22() real ext-real Element of REAL
(f . (x0 + (r / 2))) - (f . x0) is V22() real ext-real Element of REAL
min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) is V22() real ext-real set
r1 - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) is V22() real ext-real set
r1 + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) is V22() real ext-real set
].(r1 - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))),(r1 + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) & not r1 + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) <= b₁ ) } is set
N1 is open V84() V85() V86() Neighbourhood of r1
[.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f . (x0 + (r / 2)) <= b₁ & b₁ <= f . (x0 - (r / 2)) ) } is set
[.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f . (x0 - (r / 2)) <= b₁ & b₁ <= f . (x0 + (r / 2)) ) } is set
[.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] is V84() V85() V86() Element of K19(REAL)
N1 is open V84() V85() V86() Neighbourhood of r1
x is set
].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= f . (x0 - (r / 2)) & not f . (x0 + (r / 2)) <= b₁ ) } is set
(f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) is V22() real ext-real Element of REAL
(f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
(f . x0) + ((f . (x0 + (r / 2))) - (f . x0)) is V22() real ext-real Element of REAL
(f . x0) - ((f . x0) - (f . (x0 - (r / 2)))) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
f . s is V22() real ext-real Element of REAL
(f . (x0 - (r / 2))) - (f . x0) is V22() real ext-real Element of REAL
(f . x0) - (f . (x0 + (r / 2))) is V22() real ext-real Element of REAL
min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) is V22() real ext-real set
r1 - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) is V22() real ext-real set
r1 + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) is V22() real ext-real set
].(r1 - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))),(r1 + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= r1 - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) & not r1 + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) <= b₁ ) } is set
N1 is open V84() V85() V86() Neighbourhood of r1
[.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f . (x0 - (r / 2)) <= b₁ & b₁ <= f . (x0 + (r / 2)) ) } is set
[.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] is closed V84() V85() V86() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f . (x0 + (r / 2)) <= b₁ & b₁ <= f . (x0 - (r / 2)) ) } is set
[.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] is V84() V85() V86() Element of K19(REAL)
N1 is open V84() V85() V86() Neighbourhood of r1
x is set
].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ is open V84() V85() V86() V95() V96() V100() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( not b₁ <= f . (x0 + (r / 2)) & not f . (x0 - (r / 2)) <= b₁ ) } is set
(f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) is V22() real ext-real Element of REAL
(f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) is V22() real ext-real Element of REAL
r2 is V22() real ext-real Element of REAL
(f . x0) + ((f . (x0 - (r / 2))) - (f . x0)) is V22() real ext-real Element of REAL
(f . x0) - ((f . x0) - (f . (x0 + (r / 2)))) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
f . s is V22() real ext-real Element of REAL
R is open V84() V85() V86() Neighbourhood of r1