let X, Y be RealBanachSpace; :: thesis: 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; :: thesis: 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); :: thesis: ( T1 = T & T1 is onto implies T1 is open )
assume AS0:
( T1 = T & T1 is onto )
; :: thesis: T1 is open
thus
for G being Subset of (LinearTopSpaceNorm X) st G is open holds
T1 .: G is open
:: according to T_0TOPSP:def 2 :: thesis: verumproof
let G be
Subset of
(LinearTopSpaceNorm X);
:: thesis: ( G is open implies T1 .: G is open )
assume AA1:
G is
open
;
:: thesis: T1 .: G is open
defpred S1[
Element of
NAT ,
set ]
means ex
TBn being
Subset of
(TopSpaceNorm Y) st
(
TBn = T .: (Ball (0. X),$1) & $2
= Cl TBn );
P1:
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 P2:
for
x being
Element of
NAT holds
S1[
x,
f . x]
from FUNCT_2:sch 3(P1);
reconsider f =
f as
SetSequence of
Y ;
AD1:
union (rng f) is
Subset of
Y
by PROB_1:23;
the
carrier of
Y c= union (rng f)
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in the carrier of Y or z in union (rng f) )
assume
z in the
carrier of
Y
;
:: thesis: z in union (rng f)
then reconsider z1 =
z as
Point of
Y ;
AQ1:
rng T = the
carrier of
(LinearTopSpaceNorm Y)
by AS0, FUNCT_2:def 3;
rng T = the
carrier of
Y
by AQ1, NORMSP_2:def 4;
then consider x1 being
set such that AZ3:
(
x1 in the
carrier of
X &
z1 = T . x1 )
by FUNCT_2:17;
reconsider x1 =
x1 as
Point of
X by AZ3;
consider m being
Element of
NAT such that AZ9:
||.x1.|| <= m
by MESFUNC1:11;
set n =
m + 1;
||.x1.|| + 0 < m + 1
by AZ9, XREAL_1:10;
then
||.(- x1).|| < m + 1
by NORMSP_1:6;
then
||.((0. X) - x1).|| < m + 1
by RLVECT_1:27;
then AZ4:
x1 in Ball (0. X),
(m + 1)
;
AZ7:
T . x1 in T .: (Ball (0. X),(m + 1))
by AZ4, FUNCT_2:43;
consider TBn being
Subset of
(TopSpaceNorm Y) such that AZ5:
(
TBn = T .: (Ball (0. X),(m + 1)) &
f . (m + 1) = Cl TBn )
by P2;
AZ6:
TBn c= f . (m + 1)
by AZ5, PRE_TOPC:48;
NAT = dom f
by FUNCT_2:def 1;
then
f . (m + 1) in rng f
by FUNCT_1:12;
hence
z in union (rng f)
by AZ3, AZ5, AZ6, AZ7, TARSKI:def 4;
:: thesis: verum
end;
then P3:
union (rng f) = the
carrier of
Y
by AD1, XBOOLE_0:def 10;
for
n being
Element of
NAT holds
f . n is
closed
then consider n0 being
Element of
NAT ,
r being
Real,
y0 being
Point of
Y such that P4:
(
0 < r &
Ball y0,
r c= f . n0 )
by P3, LOPBAN_5:3;
consider TBn0 being
Subset of
(TopSpaceNorm Y) such that YP0:
(
TBn0 = T .: (Ball (0. X),n0) &
f . n0 = Cl TBn0 )
by P2;
consider TBn01 being
Subset of
(TopSpaceNorm Y) such that YP1:
(
TBn01 = T .: (Ball (0. X),(n0 + 1)) &
f . (n0 + 1) = Cl TBn01 )
by P2;
Ball (0. X),
n0 c= Ball (0. X),
(n0 + 1)
by Lm13, NAT_1:11;
then
TBn0 c= TBn01
by YP0, YP1, RELAT_1:156;
then
f . n0 c= f . (n0 + 1)
by YP0, YP1, PRE_TOPC:49;
then YP3:
Ball y0,
r c= Cl TBn01
by YP1, P4, XBOOLE_1:1;
||.(y0 - y0).|| < r
by P4, NORMSP_1:10;
then
y0 in Ball y0,
r
;
then ZP4:
y0 in Cl TBn01
by YP3;
reconsider LTBn01 =
TBn01 as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
- 1 is non
zero Real
;
then ZP5:
Cl ((- 1) * LTBn01) = (- 1) * (Cl LTBn01)
by RLTOPSP1:53;
reconsider XB01 =
Ball (0. X),
(n0 + 1) as
Subset of
X ;
reconsider XTB01 =
T .: (Ball (0. X),(n0 + 1)) as
Subset of
Y ;
ZP6:
(- 1) * LTBn01 =
(- 1) * XTB01
by Lm06, YP1
.=
T .: ((- 1) * (Ball (0. X),(n0 + 1)))
by Lm032
.=
LTBn01
by YP1, Lm10
;
reconsider yy0 =
y0 as
Point of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
YY1:
- yy0 =
(- 1) * yy0
by RLVECT_1:29
.=
(- 1) * y0
by NORMSP_2:def 4
.=
- y0
by RLVECT_1:29
;
reconsider BYr =
Ball (0. Y),
r 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;
yy0 in Cl LTBn01
by Lm08, ZP4;
then
(- 1) * yy0 in (- 1) * (Cl LTBn01)
;
then
- yy0 in Cl LTBn01
by ZP5, ZP6, RLVECT_1:29;
then YP4:
- yy0 in Cl TBn01
by Lm08;
Ball y0,
r = y0 + (Ball (0. Y),r)
by Lm01;
then
BYyr = yy0 + BYr
by Lm05;
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 YP5:
Ball (0. Y),
r = (- y0) + (Ball y0,r)
by Lm05, YY1;
reconsider TBnx01 =
T .: (Ball (0. X),(n0 + 1)) as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
reconsider my0 =
{(- yy0)} as
Subset of
(LinearTopSpaceNorm Y) ;
YP11:
BYyr c= Cl TBnx01
by Lm08, YP3, YP1;
{(- yy0)} c= Cl TBn01
by YP4, ZFMISC_1:37;
then
my0 c= Cl TBnx01
by Lm08, YP1;
then
my0 + BYyr c= (Cl TBnx01) + (Cl TBnx01)
by YP11, RLTOPSP1:11;
then
(- yy0) + BYyr c= (Cl TBnx01) + (Cl TBnx01)
by RUSUB_4:36;
then YP6:
(- y0) + (Ball y0,r) c= (Cl TBnx01) + (Cl TBnx01)
by YY1, Lm05;
(Cl TBnx01) + (Cl TBnx01) c= Cl (TBnx01 + TBnx01)
by RLTOPSP1:63;
then YP7:
Ball (0. Y),
r c= Cl (TBnx01 + TBnx01)
by YP5, YP6, XBOOLE_1:1;
YP71:
TBnx01 = 1
* TBnx01
by CONVEX1:32;
reconsider TB1 =
T .: (Ball (0. X),1) as
Subset of
(LinearTopSpaceNorm Y) by NORMSP_2:def 4;
YP8:
TBnx01 + TBnx01 =
(1 + 1) * TBnx01
by YP71, Lm12, CONVEX1:13
.=
2
* TBnx01
;
reconsider TBX1 =
T .: (Ball (0. X),1) as
Subset of
Y ;
Ball (0. X),
((n0 + 1) * 1) = (n0 + 1) * (Ball (0. X),1)
by Lm02;
then
(n0 + 1) * TBX1 = T .: (Ball (0. X),(n0 + 1))
by Lm032;
then TBnx01 + TBnx01 =
2
* ((n0 + 1) * TB1)
by YP8, Lm06
.=
(2 * (n0 + 1)) * TB1
by CONVEX1:37
.=
((2 * n0) + 2) * TB1
;
then YP10:
Cl (TBnx01 + TBnx01) = ((2 * n0) + 2) * (Cl TB1)
by RLTOPSP1:53;
YP13:
(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
;
reconsider nb1 = 1
/ ((2 * n0) + 2) as non
zero Real by 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 Lm02
.=
nb1 * BYr
by Lm06
;
then Q4:
Ball (0. Y),
(r / ((2 * n0) + 2)) c= (1 / ((2 * n0) + 2)) * (((2 * n0) + 2) * (Cl TB1))
by YP10, YP7, CONVEX1:39;
Q5:
0 < r / ((2 * n0) + 2)
by P4, XREAL_1:141;
(
Ball (0. X),1 is
Subset of
(LinearTopSpaceNorm X) &
Ball (0. Y),
(r / ((2 * n0) + 2)) is
Subset of
(LinearTopSpaceNorm Y) )
by NORMSP_2:def 4;
then P5:
Ball (0. Y),
(r / ((2 * n0) + 2)) c= T .: (Ball (0. X),1)
by LM040, Q4, P4, YP13, XREAL_1:141;
P6:
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
let p be
Real;
:: thesis: ( p > 0 implies ex q being Real st
( 0 < q & Ball (0. Y),q c= T .: (Ball (0. X),p) ) )
assume P61:
p > 0
;
:: thesis: ex q being Real st
( 0 < q & Ball (0. Y),q c= T .: (Ball (0. X),p) )
reconsider TB1 =
T .: (Ball (0. X),1) as
Subset of
Y ;
P610:
p * (Ball (0. X),1) = Ball (0. X),
(p * 1)
by P61, Lm02;
p * (Ball (0. Y),(r / ((2 * n0) + 2))) c= p * TB1
by P5, CONVEX1:39;
then P612:
Ball (0. Y),
((r / ((2 * n0) + 2)) * p) c= p * TB1
by P61, Lm02;
take q =
(r / ((2 * n0) + 2)) * p;
:: thesis: ( 0 < q & Ball (0. Y),q c= T .: (Ball (0. X),p) )
thus
(
0 < q &
Ball (0. Y),
q c= T .: (Ball (0. X),p) )
by P61, P610, P612, Lm032, Q5, XREAL_1:131;
:: thesis: verum
end;
now let y be
Point of
Y;
:: thesis: ( 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 P7:
y in T1 .: G
;
:: thesis: ex q being Real st
( 0 < q & { w where w is Point of Y : ||.(y - w).|| < q } c= T1 .: G )consider x being
Point of
X such that P8:
(
x in G &
y = T . x )
by P7, AS0, FUNCT_2:116;
consider p being
Real such that P9:
(
p > 0 &
{ z where z is Point of X : ||.(x - z).|| < p } c= G )
by P8, AA1, NORMSP_2:22;
Ball x,
p c= G
by P9;
then P11:
x + (Ball (0. X),p) c= G
by Lm01;
reconsider TBp =
T .: (Ball (0. X),p) as
Subset of
Y ;
then Q11:
y + TBp c= T .: G
by AS0, TARSKI:def 3;
consider q being
Real such that P12:
(
0 < q &
Ball (0. Y),
q c= TBp )
by P6, P9;
take q =
q;
:: thesis: ( 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 Lm01;
hence
(
0 < q &
{ w where w is Point of Y : ||.(y - w).|| < q } c= T1 .: G )
by AS0, Q11, P12, XBOOLE_1:1;
:: thesis: verum end;
hence
T1 .: G is
open
by NORMSP_2:22;
:: thesis: verum
end;