let E be RealNormSpace; for F being RealBanachSpace
for E0 being non empty Subset of E
for F0 being non empty Subset of F
for Fai being PartFunc of [:E,F:],F st F0 is closed & [:E0,F0:] c= dom Fai & ( for x being Point of E
for y being Point of F st x in E0 & y in F0 holds
Fai . (x,y) in F0 ) & ( for y being Point of F st y in F0 holds
for x0 being Point of E st x0 in E0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in E0 & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) ) & ex k being Real st
( 0 < k & k < 1 & ( for x being Point of E st x in E0 holds
for y1, y2 being Point of F st y1 in F0 & y2 in F0 holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| ) ) holds
( ( for x being Point of E st x in E0 holds
( ex y being Point of F st
( y in F0 & Fai . (x,y) = y ) & ( for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds
y1 = y2 ) ) ) & ( for x0 being Point of E
for y0 being Point of F st x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) ) ) )
let F be RealBanachSpace; for E0 being non empty Subset of E
for F0 being non empty Subset of F
for Fai being PartFunc of [:E,F:],F st F0 is closed & [:E0,F0:] c= dom Fai & ( for x being Point of E
for y being Point of F st x in E0 & y in F0 holds
Fai . (x,y) in F0 ) & ( for y being Point of F st y in F0 holds
for x0 being Point of E st x0 in E0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in E0 & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) ) & ex k being Real st
( 0 < k & k < 1 & ( for x being Point of E st x in E0 holds
for y1, y2 being Point of F st y1 in F0 & y2 in F0 holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| ) ) holds
( ( for x being Point of E st x in E0 holds
( ex y being Point of F st
( y in F0 & Fai . (x,y) = y ) & ( for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds
y1 = y2 ) ) ) & ( for x0 being Point of E
for y0 being Point of F st x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) ) ) )
let E0 be non empty Subset of E; for F0 being non empty Subset of F
for Fai being PartFunc of [:E,F:],F st F0 is closed & [:E0,F0:] c= dom Fai & ( for x being Point of E
for y being Point of F st x in E0 & y in F0 holds
Fai . (x,y) in F0 ) & ( for y being Point of F st y in F0 holds
for x0 being Point of E st x0 in E0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in E0 & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) ) & ex k being Real st
( 0 < k & k < 1 & ( for x being Point of E st x in E0 holds
for y1, y2 being Point of F st y1 in F0 & y2 in F0 holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| ) ) holds
( ( for x being Point of E st x in E0 holds
( ex y being Point of F st
( y in F0 & Fai . (x,y) = y ) & ( for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds
y1 = y2 ) ) ) & ( for x0 being Point of E
for y0 being Point of F st x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) ) ) )
let F0 be non empty Subset of F; for Fai being PartFunc of [:E,F:],F st F0 is closed & [:E0,F0:] c= dom Fai & ( for x being Point of E
for y being Point of F st x in E0 & y in F0 holds
Fai . (x,y) in F0 ) & ( for y being Point of F st y in F0 holds
for x0 being Point of E st x0 in E0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in E0 & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) ) & ex k being Real st
( 0 < k & k < 1 & ( for x being Point of E st x in E0 holds
for y1, y2 being Point of F st y1 in F0 & y2 in F0 holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| ) ) holds
( ( for x being Point of E st x in E0 holds
( ex y being Point of F st
( y in F0 & Fai . (x,y) = y ) & ( for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds
y1 = y2 ) ) ) & ( for x0 being Point of E
for y0 being Point of F st x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) ) ) )
let Fai be PartFunc of [:E,F:],F; ( F0 is closed & [:E0,F0:] c= dom Fai & ( for x being Point of E
for y being Point of F st x in E0 & y in F0 holds
Fai . (x,y) in F0 ) & ( for y being Point of F st y in F0 holds
for x0 being Point of E st x0 in E0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in E0 & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) ) & ex k being Real st
( 0 < k & k < 1 & ( for x being Point of E st x in E0 holds
for y1, y2 being Point of F st y1 in F0 & y2 in F0 holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| ) ) implies ( ( for x being Point of E st x in E0 holds
( ex y being Point of F st
( y in F0 & Fai . (x,y) = y ) & ( for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds
y1 = y2 ) ) ) & ( for x0 being Point of E
for y0 being Point of F st x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) ) ) ) )
assume that
A1:
F0 is closed
and
A2:
[:E0,F0:] c= dom Fai
and
A3:
for x being Point of E
for y being Point of F st x in E0 & y in F0 holds
Fai . (x,y) in F0
and
A4:
for y being Point of F st y in F0 holds
for x0 being Point of E st x0 in E0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in E0 & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) )
and
A5:
ex k being Real st
( 0 < k & k < 1 & ( for x being Point of E st x in E0 holds
for y1, y2 being Point of F st y1 in F0 & y2 in F0 holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| ) )
; ( ( for x being Point of E st x in E0 holds
( ex y being Point of F st
( y in F0 & Fai . (x,y) = y ) & ( for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds
y1 = y2 ) ) ) & ( for x0 being Point of E
for y0 being Point of F st x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) ) ) )
consider k being Real such that
A6:
( 0 < k & k < 1 )
and
A7:
for x being Point of E st x in E0 holds
for y1, y2 being Point of F st y1 in F0 & y2 in F0 holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).||
by A5;
thus
for x being Point of E st x in E0 holds
( ex y being Point of F st
( y in F0 & Fai . (x,y) = y ) & ( for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds
y1 = y2 ) )
for x0 being Point of E
for y0 being Point of F st x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) )proof
let x be
Point of
E;
( x in E0 implies ( ex y being Point of F st
( y in F0 & Fai . (x,y) = y ) & ( for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds
y1 = y2 ) ) )
deffunc H1(
object )
-> set =
Fai . (
x,$1);
assume A8:
x in E0
;
( ex y being Point of F st
( y in F0 & Fai . (x,y) = y ) & ( for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds
y1 = y2 ) )
then A9:
for
y being
object st
y in F0 holds
H1(
y)
in F0
by A3;
consider Fai0 being
Function of
F0,
F0 such that A10:
for
y being
object st
y in F0 holds
Fai0 . y = H1(
y)
from FUNCT_2:sch 2(A9);
A11:
rng Fai0 c= F0
;
A12:
dom Fai0 = F0
by FUNCT_2:def 1;
rng Fai0 c= the
carrier of
F
by XBOOLE_1:1;
then reconsider Fai0 =
Fai0 as
PartFunc of
F,
F by A12, RELSET_1:4;
A13:
for
z,
y being
Point of
F st
z in F0 &
y in F0 holds
||.((Fai0 /. z) - (Fai0 /. y)).|| <= k * ||.(z - y).||
proof
let z,
y be
Point of
F;
( z in F0 & y in F0 implies ||.((Fai0 /. z) - (Fai0 /. y)).|| <= k * ||.(z - y).|| )
assume A14:
(
z in F0 &
y in F0 )
;
||.((Fai0 /. z) - (Fai0 /. y)).|| <= k * ||.(z - y).||
then A15:
[x,z] in [:E0,F0:]
by A8, ZFMISC_1:87;
A16:
[x,y] in [:E0,F0:]
by A8, A14, ZFMISC_1:87;
A18:
y in dom Fai0
by A14, FUNCT_2:def 1;
z in dom Fai0
by A14, FUNCT_2:def 1;
then A19:
Fai0 /. z =
Fai0 . z
by PARTFUN1:def 6
.=
H1(
z)
by A10, A14
.=
Fai /. [x,z]
by A2, A15, PARTFUN1:def 6
;
Fai0 /. y =
Fai0 . y
by A18, PARTFUN1:def 6
.=
H1(
y)
by A10, A14
.=
Fai /. [x,y]
by A2, A16, PARTFUN1:def 6
;
hence
||.((Fai0 /. z) - (Fai0 /. y)).|| <= k * ||.(z - y).||
by A7, A8, A14, A19;
verum
end;
thus
ex
y being
Point of
F st
(
y in F0 &
Fai . (
x,
y)
= y )
for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds
y1 = y2
thus
for
y1,
y2 being
Point of
F st
y1 in F0 &
y2 in F0 &
Fai . (
x,
y1)
= y1 &
Fai . (
x,
y2)
= y2 holds
y1 = y2
verumproof
let y1,
y2 be
Point of
F;
( y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 implies y1 = y2 )
assume A21:
(
y1 in F0 &
y2 in F0 &
Fai . (
x,
y1)
= y1 &
Fai . (
x,
y2)
= y2 )
;
y1 = y2
A22:
Fai0 . y1 = y1
by A10, A21;
Fai0 . y2 = y2
by A10, A21;
hence
y1 = y2
by A1, A6, A11, A12, A13, A21, A22, FIXPOINT;
verum
end;
end;
thus
for x0 being Point of E
for y0 being Point of F st x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) )
verumproof
let x0 be
Point of
E;
for y0 being Point of F st x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) )let y0 be
Point of
F;
( x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 implies for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) ) )
assume A24:
(
x0 in E0 &
y0 in F0 &
Fai . (
x0,
y0)
= y0 )
;
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) )
let e be
Real;
( 0 < e implies ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) ) )
assume A25:
0 < e
;
ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) )
reconsider e1 =
e * (1 - k) as
Real ;
A26:
0 < 1
- k
by A6, XREAL_1:50;
then consider d being
Real such that A27:
(
0 < d & ( for
x1 being
Point of
E st
x1 in E0 &
||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y0]) - (Fai /. [x0,y0])).|| < e1 ) )
by A4, A24, A25, XREAL_1:129;
take
d
;
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) )
thus
0 < d
by A27;
for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e
let x1 be
Point of
E;
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < elet y1 be
Point of
F;
( x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d implies ||.(y1 - y0).|| < e )
assume A28:
(
x1 in E0 &
y1 in F0 &
Fai . (
x1,
y1)
= y1 &
||.(x1 - x0).|| < d )
;
||.(y1 - y0).|| < e
[x0,y0] in [:E0,F0:]
by A24, ZFMISC_1:87;
then A29:
y0 = Fai /. [x0,y0]
by A2, A24, PARTFUN1:def 6;
[x1,y1] in [:E0,F0:]
by A28, ZFMISC_1:87;
then A30:
y1 = Fai /. [x1,y1]
by A2, A28, PARTFUN1:def 6;
((Fai /. [x1,y1]) - (Fai /. [x1,y0])) + ((Fai /. [x1,y0]) - (Fai /. [x0,y0])) =
(((Fai /. [x1,y1]) - (Fai /. [x1,y0])) + (Fai /. [x1,y0])) - (Fai /. [x0,y0])
by RLVECT_1:28
.=
(Fai /. [x1,y1]) - (Fai /. [x0,y0])
by RLVECT_4:1
;
then A31:
||.(y1 - y0).|| <= ||.((Fai /. [x1,y1]) - (Fai /. [x1,y0])).|| + ||.((Fai /. [x1,y0]) - (Fai /. [x0,y0])).||
by A29, A30, NORMSP_1:def 1;
||.((Fai /. [x1,y0]) - (Fai /. [x0,y0])).|| < e1
by A27, A28;
then
||.((Fai /. [x1,y1]) - (Fai /. [x1,y0])).|| + ||.((Fai /. [x1,y0]) - (Fai /. [x0,y0])).|| < e1 + (k * ||.(y1 - y0).||)
by A7, A24, A28, XREAL_1:8;
then
||.(y1 - y0).|| < e1 + (k * ||.(y1 - y0).||)
by A31, XXREAL_0:2;
then
||.(y1 - y0).|| - (k * ||.(y1 - y0).||) < (e1 + (k * ||.(y1 - y0).||)) - (k * ||.(y1 - y0).||)
by XREAL_1:14;
then
(1 - k) * ||.(y1 - y0).|| < e1
;
then
||.(y1 - y0).|| < e1 / (1 - k)
by A26, XREAL_1:81;
hence
||.(y1 - y0).|| < e
by A26, XCMPLX_1:89;
verum
end;