let X, Y be RealBanachSpace; for T being bounded LinearOperator of X,Y
for T1 being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) st T1 = T & T1 is onto holds
T1 is open
let T be bounded LinearOperator of X,Y; for T1 being Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y) st T1 = T & T1 is onto holds
T1 is open
let T1 be Function of (LinearTopSpaceNorm X),(LinearTopSpaceNorm Y); ( T1 = T & T1 is onto implies T1 is open )
assume that
A1:
T1 = T
and
A2:
T1 is onto
; T1 is open
thus
for G being Subset of (LinearTopSpaceNorm X) st G is open holds
T1 .: G is open
T_0TOPSP:def 2 verumproof
reconsider TB1 =
T .: (Ball (0. X),1) as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
defpred S1[
Element of
NAT ,
set ]
means ex
TBn being
Subset of
(TopSpaceNorm Y) st
(
TBn = T .: (Ball (0. X),$1) & $2
= Cl TBn );
let G be
Subset of
(LinearTopSpaceNorm X);
( G is open implies T1 .: G is open )
A3:
for
n being
Element of
NAT ex
y being
Element of
bool the
carrier of
Y st
S1[
n,
y]
consider f being
Function of
NAT ,
(bool the carrier of Y) such that A4:
for
x being
Element of
NAT holds
S1[
x,
f . x]
from FUNCT_2:sch 3(A3);
reconsider f =
f as
SetSequence of
Y ;
A5:
for
n being
Element of
NAT holds
f . n is
closed
A6:
the
carrier of
Y c= union (rng f)
proof
let z be
set ;
TARSKI:def 3 ( not z in the carrier of Y or z in union (rng f) )
assume
z in the
carrier of
Y
;
z in union (rng f)
then reconsider z1 =
z as
Point of
Y ;
rng T = the
carrier of
(LinearTopSpaceNorm Y)
by A1, A2, FUNCT_2:def 3;
then
rng T = the
carrier of
Y
by NORMSP_2:def 4;
then consider x1 being
set such that A7:
x1 in the
carrier of
X
and A8:
z1 = T . x1
by FUNCT_2:17;
reconsider x1 =
x1 as
Point of
X by A7;
consider m being
Element of
NAT such that A9:
||.x1.|| <= m
by MESFUNC1:11;
set n =
m + 1;
||.x1.|| + 0 < m + 1
by A9, XREAL_1:10;
then
||.(- x1).|| < m + 1
by NORMSP_1:6;
then
||.((0. X) - x1).|| < m + 1
by RLVECT_1:27;
then
x1 in Ball (0. X),
(m + 1)
;
then A10:
T . x1 in T .: (Ball (0. X),(m + 1))
by FUNCT_2:43;
NAT = dom f
by FUNCT_2:def 1;
then A11:
f . (m + 1) in rng f
by FUNCT_1:12;
consider TBn being
Subset of
(TopSpaceNorm Y) such that A12:
TBn = T .: (Ball (0. X),(m + 1))
and A13:
f . (m + 1) = Cl TBn
by A4;
TBn c= f . (m + 1)
by A13, PRE_TOPC:48;
hence
z in union (rng f)
by A8, A10, A12, A11, TARSKI:def 4;
verum
end;
union (rng f) is
Subset of
Y
by PROB_1:23;
then
union (rng f) = the
carrier of
Y
by A6, XBOOLE_0:def 10;
then consider n0 being
Element of
NAT ,
r being
Real,
y0 being
Point of
Y such that A14:
0 < r
and A15:
Ball y0,
r c= f . n0
by A5, LOPBAN_5:3;
consider TBn0 being
Subset of
(TopSpaceNorm Y) such that A16:
TBn0 = T .: (Ball (0. X),n0)
and A17:
f . n0 = Cl TBn0
by A4;
consider TBn01 being
Subset of
(TopSpaceNorm Y) such that A18:
TBn01 = T .: (Ball (0. X),(n0 + 1))
and A19:
f . (n0 + 1) = Cl TBn01
by A4;
Ball (0. X),
n0 c= Ball (0. X),
(n0 + 1)
by Th14, NAT_1:11;
then
TBn0 c= TBn01
by A16, A18, RELAT_1:156;
then
f . n0 c= f . (n0 + 1)
by A17, A19, PRE_TOPC:49;
then A20:
Ball y0,
r c= Cl TBn01
by A15, A19, XBOOLE_1:1;
reconsider LTBn01 =
TBn01 as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
- 1 is non
zero Real
;
then A21:
Cl ((- 1) * LTBn01) = (- 1) * (Cl LTBn01)
by RLTOPSP1:53;
reconsider yy0 =
y0 as
Point of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
A22:
Ball (0. Y),
(r / ((2 * n0) + 2)) is
Subset of
(LinearTopSpaceNorm Y)
by NORMSP_2:def 4;
||.(y0 - y0).|| < r
by A14, NORMSP_1:10;
then
y0 in Ball y0,
r
;
then
y0 in Cl TBn01
by A20;
then
yy0 in Cl LTBn01
by Th10;
then A23:
(- 1) * yy0 in (- 1) * (Cl LTBn01)
;
reconsider nb1 = 1
/ ((2 * n0) + 2) as non
zero Real by XREAL_1:141;
reconsider TBX1 =
T .: (Ball (0. X),1) as
Subset of
Y ;
reconsider XB01 =
Ball (0. X),
(n0 + 1) as
Subset of
X ;
reconsider my0 =
{(- yy0)} as
Subset of
(LinearTopSpaceNorm Y) ;
reconsider TBnx01 =
T .: (Ball (0. X),(n0 + 1)) as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
reconsider BYyr =
Ball y0,
r as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
reconsider BYr =
Ball (0. Y),
r as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
reconsider XTB01 =
T .: (Ball (0. X),(n0 + 1)) as
Subset of
Y ;
A24:
- yy0 =
(- 1) * yy0
by RLVECT_1:29
.=
(- 1) * y0
by NORMSP_2:def 4
.=
- y0
by RLVECT_1:29
;
(- 1) * LTBn01 =
(- 1) * XTB01
by A18, Th9
.=
T .: ((- 1) * (Ball (0. X),(n0 + 1)))
by Th5
.=
LTBn01
by A18, Th11
;
then
- yy0 in Cl LTBn01
by A21, A23, RLVECT_1:29;
then
- yy0 in Cl TBn01
by Th10;
then
{(- yy0)} c= Cl TBn01
by ZFMISC_1:37;
then A25:
my0 c= Cl TBnx01
by A18, Th10;
BYyr c= Cl TBnx01
by A18, A20, Th10;
then
my0 + BYyr c= (Cl TBnx01) + (Cl TBnx01)
by A25, RLTOPSP1:11;
then
(- yy0) + BYyr c= (Cl TBnx01) + (Cl TBnx01)
by RUSUB_4:36;
then A26:
(- y0) + (Ball y0,r) c= (Cl TBnx01) + (Cl TBnx01)
by A24, Th8;
A27:
(Cl TBnx01) + (Cl TBnx01) c= Cl (TBnx01 + TBnx01)
by RLTOPSP1:63;
Ball y0,
r = y0 + (Ball (0. Y),r)
by Th2;
then
BYyr = yy0 + BYr
by Th8;
then
(- yy0) + BYyr = ((- yy0) + yy0) + BYr
by RLTOPSP1:6;
then
(- yy0) + BYyr = (0. (LinearTopSpaceNorm Y)) + BYr
by RLVECT_1:16;
then
(- yy0) + BYyr = {(0. (LinearTopSpaceNorm Y))} + BYr
by RUSUB_4:36;
then
(- yy0) + BYyr = BYr
by CONVEX1:35;
then
Ball (0. Y),
r = (- y0) + (Ball y0,r)
by A24, Th8;
then A28:
Ball (0. Y),
r c= Cl (TBnx01 + TBnx01)
by A26, A27, XBOOLE_1:1;
TBnx01 = 1
* TBnx01
by CONVEX1:32;
then A29:
TBnx01 + TBnx01 =
(1 + 1) * TBnx01
by Th13, CONVEX1:13
.=
2
* TBnx01
;
Ball (0. X),
((n0 + 1) * 1) = (n0 + 1) * (Ball (0. X),1)
by Th3;
then
(n0 + 1) * TBX1 = T .: (Ball (0. X),(n0 + 1))
by Th5;
then TBnx01 + TBnx01 =
2
* ((n0 + 1) * TB1)
by A29, Th9
.=
(2 * (n0 + 1)) * TB1
by CONVEX1:37
.=
((2 * n0) + 2) * TB1
;
then A30:
Cl (TBnx01 + TBnx01) = ((2 * n0) + 2) * (Cl TB1)
by RLTOPSP1:53;
A31:
0 < r / ((2 * n0) + 2)
by A14, XREAL_1:141;
Ball (0. Y),
(r / ((2 * n0) + 2)) =
Ball (0. Y),
((r * 1) / ((2 * n0) + 2))
.=
Ball (0. Y),
(r * (1 / ((2 * n0) + 2)))
by XCMPLX_1:75
.=
nb1 * (Ball (0. Y),r)
by Th3
.=
nb1 * BYr
by Th9
;
then A32:
Ball (0. Y),
(r / ((2 * n0) + 2)) c= (1 / ((2 * n0) + 2)) * (((2 * n0) + 2) * (Cl TB1))
by A28, A30, CONVEX1:39;
(1 / ((2 * n0) + 2)) * (((2 * n0) + 2) * (Cl TB1)) =
((1 / ((2 * n0) + 2)) * ((2 * n0) + 2)) * (Cl TB1)
by CONVEX1:37
.=
1
* (Cl TB1)
by XCMPLX_1:107
.=
Cl TB1
by CONVEX1:32
;
then A33:
Ball (0. Y),
(r / ((2 * n0) + 2)) c= T .: (Ball (0. X),1)
by A14, A32, A22, Th15, XREAL_1:141;
A34:
for
p being
Real st
p > 0 holds
ex
q being
Real st
(
0 < q &
Ball (0. Y),
q c= T .: (Ball (0. X),p) )
proof
reconsider TB1 =
T .: (Ball (0. X),1) as
Subset of
Y ;
let p be
Real;
( p > 0 implies ex q being Real st
( 0 < q & Ball (0. Y),q c= T .: (Ball (0. X),p) ) )
assume A35:
p > 0
;
ex q being Real st
( 0 < q & Ball (0. Y),q c= T .: (Ball (0. X),p) )
then A36:
p * (Ball (0. X),1) = Ball (0. X),
(p * 1)
by Th3;
take q =
(r / ((2 * n0) + 2)) * p;
( 0 < q & Ball (0. Y),q c= T .: (Ball (0. X),p) )
p * (Ball (0. Y),(r / ((2 * n0) + 2))) c= p * TB1
by A33, CONVEX1:39;
then
Ball (0. Y),
((r / ((2 * n0) + 2)) * p) c= p * TB1
by A35, Th3;
hence
(
0 < q &
Ball (0. Y),
q c= T .: (Ball (0. X),p) )
by A31, A35, A36, Th5, XREAL_1:131;
verum
end;
assume A37:
G is
open
;
T1 .: G is open
now let y be
Point of
Y;
( y in T1 .: G implies ex q being Real st
( 0 < q & { w where w is Point of Y : ||.(y - w).|| < q } c= T1 .: G ) )assume
y in T1 .: G
;
ex q being Real st
( 0 < q & { w where w is Point of Y : ||.(y - w).|| < q } c= T1 .: G )then consider x being
Point of
X such that A38:
x in G
and A39:
y = T . x
by A1, FUNCT_2:116;
consider p being
Real such that A40:
p > 0
and A41:
{ z where z is Point of X : ||.(x - z).|| < p } c= G
by A37, A38, NORMSP_2:22;
reconsider TBp =
T .: (Ball (0. X),p) as
Subset of
Y ;
consider q being
Real such that A42:
0 < q
and A43:
Ball (0. Y),
q c= TBp
by A34, A40;
Ball x,
p c= G
by A41;
then A44:
x + (Ball (0. X),p) c= G
by Th2;
then A50:
y + TBp c= T .: G
by A1, TARSKI:def 3;
take q =
q;
( 0 < q & { w where w is Point of Y : ||.(y - w).|| < q } c= T1 .: G )then
y + (Ball (0. Y),q) c= y + TBp
by TARSKI:def 3;
then
Ball y,
q c= y + TBp
by Th2;
hence
(
0 < q &
{ w where w is Point of Y : ||.(y - w).|| < q } c= T1 .: G )
by A1, A50, A42, XBOOLE_1:1;
verum end;
hence
T1 .: G is
open
by NORMSP_2:22;
verum
end;