:: Topological Properties of Real Normed Space
:: by Kazuhisa Nakasho , Yuichi Futa and Yasunari Shidama
::
:: Received September 15, 2014
:: Copyright (c) 2014-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RLSUB_1, UNIALG_1, DUALSP01, NORMSP_3, CFCONT_1, MOD_4, RLVECT_1,
ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, RSSPACE3, VECTSP_1, REAL_1, TARSKI,
MSSUBFAM, STRUCT_0, REALSET1, FUNCOP_1, FCONT_1, NORMSP_0, SEQ_2,
LOPBAN_1, ORDINAL2, ARYTM_3, ALGSTR_0, NORMSP_1, FUNCT_2, PRE_TOPC,
SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, SEQ_4, XBOOLE_0, CARD_1, SUPINF_2,
COMPLEX1, XXREAL_0, XXREAL_2, NAT_1, REWRITE1, METRIC_1, RELAT_2,
PARTFUN1, RCOMP_1, TOPS_1, SETFAM_1, TOPGEN_1, CARD_3, NORMSP_2,
RLVECT_3, VECTSP10, GROUP_6;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, CARD_1, ORDINAL1,
SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, FUNCOP_1, REALSET1,
NUMBERS, CARD_3, XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, COMPLEX1,
XXREAL_2, SEQ_4, STRUCT_0, ALGSTR_0, PRE_TOPC, TOPS_1, RLVECT_1,
RLVECT_3, RLSUB_1, VECTSP_1, VECTSP_4, NORMSP_0, NORMSP_1, NORMSP_2,
HAHNBAN, RSSPACE, RSSPACE3, LOPBAN_1, NFCONT_1, VECTSP10, DUALSP01,
TOPGEN_1;
constructors REALSET1, RSSPACE3, BINOP_2, LOPBAN_2, NFCONT_1, DUALSP01,
RELSET_1, SEQ_4, NORMSP_2, CARD_3, PCOMPS_1, RLVECT_3, SETFAM_1, TOPS_1,
VECTSP10, TOPGEN_1;
registrations STRUCT_0, XREAL_0, NUMBERS, ORDINAL1, MEMBERED, RELAT_1,
XXREAL_0, VECTSP_1, FUNCT_2, SEQ_4, RELSET_1, TOPS_1, XCMPLX_0, NORMSP_0,
NAT_1, NORMSP_1, XBOOLE_0, SUBSET_1, NORMSP_2, RLSUB_1, REALSET1,
LOPBAN_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions ALGSTR_0, VECTSP_1, TARSKI, LOPBAN_1;
equalities BINOP_1, RLVECT_1, STRUCT_0, REALSET1, ALGSTR_0, NORMSP_0,
VECTSP_1, VECTSP_4, RLSUB_1, VECTSP10, PCOMPS_1, DUALSP01, NORMSP_2;
expansions RLSUB_1, TARSKI, XBOOLE_0, FUNCT_2, NORMSP_0, NORMSP_1, VECTSP_1,
STRUCT_0, RLVECT_1, TOPS_1, NFCONT_1;
theorems SEQ_4, FUNCT_1, COMPLEX1, TARSKI, RSSPACE3, XREAL_0, XXREAL_0,
NORMSP_1, LOPBAN_1, FUNCT_2, XBOOLE_0, XREAL_1, RLVECT_1, FUNCOP_1,
VECTSP_1, RLSUB_1, RSSPACE, NORMSP_0, ORDINAL1, VECTSP_4, LOPBAN_7,
NDIFF_1, PRE_TOPC, TOPS_1, TOPGEN_1, SUBSET_1, NFCONT_1, XXREAL_2,
DUALSP01, RELAT_1, XCMPLX_1, NORMSP_2, LOPBAN_3, RLVECT_3, VECTSP10,
CARD_3;
schemes FUNCT_2;
begin :: Open and Closed Subsets
registration
let X be RealNormSpace;
cluster open closed for Subset of X;
correctness
proof
set F = the open closed Subset of LinearTopSpaceNorm X;
reconsider G = F as Subset of X by NORMSP_2:def 4;
take G;
thus thesis by NORMSP_2:32,33;
end;
end;
theorem
for X be RealNormSpace, R be Subset of X
holds R is closed iff R` is open;
registration
let X be RealNormSpace, R be closed Subset of X;
cluster R` -> open;
correctness;
end;
theorem Th0:
for X be RealNormSpace, R be Subset of X
holds R is open iff R` is closed;
registration
let X be RealNormSpace, R be open Subset of X;
cluster R` -> closed;
correctness by Th0;
end;
registration
let X be RealNormSpace;
cluster [#]X -> closed;
correctness;
cluster {} X -> closed;
correctness;
cluster [#]X -> open;
correctness
proof
[#]X = [#](LinearTopSpaceNorm X) by NORMSP_2:def 4;
hence thesis by NORMSP_2:33;
end;
cluster {} X -> open;
correctness
proof
[#]X = [#](LinearTopSpaceNorm X) by NORMSP_2:def 4;
hence thesis by NORMSP_2:33;
end;
end;
registration
let X be RealNormSpace;
let P,Q be closed Subset of X;
cluster P /\ Q -> closed for Subset of X;
correctness
proof
reconsider P1 = P, Q1 = Q as Subset of LinearTopSpaceNorm X
by NORMSP_2:def 4;
P1 is closed & Q1 is closed by NORMSP_2:32; then
P1 /\ Q1 is closed;
hence thesis by NORMSP_2:32;
end;
cluster P \/ Q -> closed for Subset of X;
correctness
proof
reconsider P1 = P, Q1 = Q as Subset of LinearTopSpaceNorm X
by NORMSP_2:def 4;
P1 is closed & Q1 is closed by NORMSP_2:32; then
P1 \/ Q1 is closed;
hence thesis by NORMSP_2:32;
end;
end;
registration
let X be RealNormSpace;
let P,Q be open Subset of X;
cluster P /\ Q -> open for Subset of X;
correctness
proof
reconsider P1 = P, Q1 = Q as Subset of LinearTopSpaceNorm X
by NORMSP_2:def 4;
P1 is open & Q1 is open by NORMSP_2:33; then
P1 /\ Q1 is open;
hence thesis by NORMSP_2:33;
end;
cluster P \/ Q -> open for Subset of X;
correctness
proof
reconsider P1 = P, Q1 = Q as Subset of LinearTopSpaceNorm X
by NORMSP_2:def 4;
P1 is open & Q1 is open by NORMSP_2:33; then
P1 \/ Q1 is open;
hence thesis by NORMSP_2:33;
end;
end;
definition
let X be RealNormSpace, Y be Subset of X;
func Cl Y -> Subset of X means
:defcl:
ex Z be Subset of LinearTopSpaceNorm X st Z = Y & it = Cl Z;
correctness
proof
reconsider Z = Y as Subset of LinearTopSpaceNorm X by NORMSP_2:def 4;
Cl Z is Subset of X by NORMSP_2:def 4;
hence thesis;
end;
end;
registration
let X be RealNormSpace, Y be Subset of X;
cluster Cl Y -> closed;
correctness
proof
ex Z be Subset of LinearTopSpaceNorm X st Z = Y & Cl Y = Cl Z by defcl;
hence thesis by NORMSP_2:32;
end;
end;
theorem EQCL1:
for X be RealNormSpace,
Y be Subset of X,
Z be Subset of LinearTopSpaceNorm X
st Y = Z
holds Cl Y = Cl Z
proof
let X be RealNormSpace,
Y be Subset of X,
Z be Subset of LinearTopSpaceNorm X;
assume
A1: Y = Z;
ex Z0 be Subset of LinearTopSpaceNorm X
st Z0 = Y & Cl Y = Cl Z0 by defcl;
hence Cl Y = Cl Z by A1;
end;
theorem PRETOPC18:
for X be RealNormSpace, Z be Subset of X holds Z c= Cl(Z)
proof
let X be RealNormSpace, Z be Subset of X;
reconsider W = Z as Subset of LinearTopSpaceNorm X by NORMSP_2:def 4;
Cl Z = Cl W by EQCL1;
hence Z c= Cl Z by PRE_TOPC:18;
end;
theorem
for X be RealNormSpace,
Y be Subset of X,
v be object
st v in the carrier of X
holds
v in Cl(Y)
iff
for G being Subset of X
st G is open & v in G
holds G meets Y
proof
let X be RealNormSpace,
Y be Subset of X,
v be object;
assume
A1: v in the carrier of X;
reconsider Z = Y as Subset of LinearTopSpaceNorm X by NORMSP_2:def 4;
hereby
assume v in Cl(Y); then
A2: v in Cl(Z) by EQCL1;
thus for G being Subset of X st G is open & v in G holds G meets Y
proof
let G be Subset of X;
assume
A3: G is open & v in G;
reconsider G0 = G as Subset of LinearTopSpaceNorm X
by NORMSP_2:def 4;
G0 is open by A3,NORMSP_2:33;
hence G meets Y by A2,A3,PRE_TOPC:def 7;
end;
end;
assume
A4: for G being Subset of X st G is open & v in G holds G meets Y;
A5: for G0 being Subset of LinearTopSpaceNorm X
st G0 is open & v in G0 holds G0 meets Z
proof
let G0 be Subset of LinearTopSpaceNorm X;
assume
A6: G0 is open & v in G0;
reconsider G = G0 as Subset of X by NORMSP_2:def 4;
G is open by A6,NORMSP_2:33;
hence G0 meets Z by A4,A6;
end;
v in the carrier of LinearTopSpaceNorm X by A1,NORMSP_2:def 4; then
v in Cl(Z) by A5,PRE_TOPC:def 7;
hence v in Cl(Y) by EQCL1;
end;
theorem EQCL3:
for X be RealNormSpace,
Y be Subset of X,
v be object
holds
v in Cl(Y)
iff
ex seq be sequence of X st rng seq c= Y & seq is convergent & lim seq = v
proof
let X be RealNormSpace,
Y be Subset of X,
v be object;
reconsider Z = Y as Subset of LinearTopSpaceNorm X by NORMSP_2:def 4;
A1: Cl Z = Cl Y by EQCL1;
hereby
assume
A2: v in Cl(Y); then
A3: for G being Subset of LinearTopSpaceNorm X st G is open & v in G
holds G meets Z by A1,PRE_TOPC:def 7;
reconsider v0 = v as Point of X by A2;
defpred P[Nat,Point of X] means ||.v0 -$2.|| < 1/($1 +1) & $2 in Y;
A4: for n be Element of NAT holds ex w be Element of X st P[n, w]
proof
let n be Element of NAT;
set e = 1/(n+1);
for x be object st x in {y where y is Point of X:||.v0-y.|| < e}
holds x in the carrier of LinearTopSpaceNorm X
proof
let x be object;
assume x in {y where y is Point of X:||.v0-y.|| < e}; then
ex y be Point of X st x = y & ||.v0 - y.|| < e; then
x in the carrier of X;
hence thesis by NORMSP_2:def 4;
end; then
reconsider G = {y where y is Point of X:||.v0-y.|| < e} as Subset of
LinearTopSpaceNorm X by TARSKI:def 3;
||.v0-v0.|| < e by NORMSP_1:6; then
v0 in G; then
G meets Z by A3,NORMSP_2:23; then
consider w be object such that
A5: w in G /\ Z by XBOOLE_0:def 1;
A6: w in G & w in Z by A5,XBOOLE_0:def 4; then
A7: ex y be Point of X st w=y & ||.v0-y.|| < e;
reconsider w as Point of X by A6;
take w;
thus thesis by A5,A7,XBOOLE_0:def 4;
end;
consider seq be Function of NAT, X such that
A8: for n be Element of NAT holds P[n, seq.n] from FUNCT_2:sch 3(A4);
take seq;
for y be object st y in rng seq holds y in Y
proof
let y be object;
assume y in rng seq; then
ex x being object st x in NAT & seq.x = y by FUNCT_2:11;
hence thesis by A8;
end;
hence rng seq c= Y;
A10: now
let s be Real;
consider n being Nat such that
A11: s" < n by SEQ_4:3;
assume
A12: 0 < s;
s" + 0 < n + 1 by A11,XREAL_1:8; then
1/(n+1) < 1/s" by A12,XREAL_1:76; then
A13: 1/(n+1) < s by XCMPLX_1:216;
take k = n;
let m be Nat;
A14: m in NAT by ORDINAL1:def 12;
assume k <= m; then
k+1 <= m+1 by XREAL_1:6; then
1/(m+1) <= 1/(k+1) by XREAL_1:118; then
1/(m+1) < s by A13,XXREAL_0:2; then
||.v0 -seq.m.|| < s by A8,A14,XXREAL_0:2;
hence ||.seq.m-v0.|| <s by NORMSP_1:7;
end;
hence seq is convergent;
hence lim seq = v by A10,NORMSP_1:def 7;
end;
given seq be sequence of X such that
A15: rng seq c= Y and
A16: seq is convergent and
A17: lim seq = v;
v in the carrier of X by A17; then
A18: v in the carrier of (LinearTopSpaceNorm X) by NORMSP_2:def 4;
reconsider v0 = v as Point of X by A17;
for G being Subset of LinearTopSpaceNorm X
st G is open & v in G holds G meets Z
proof
let G be Subset of LinearTopSpaceNorm X;
assume G is open & v in G; then
consider r be Real such that
A20: r > 0 & {y where y is Point of X:||.v0-y.|| < r} c= G
by NORMSP_2:22;
consider m be Nat such that
A21: for n be Nat st m <= n holds ||.(seq.n) - v0.|| < r
by A16,A17,A20,NORMSP_1:def 7;
||.(seq.m) - v0.|| < r by A21; then
||.v0 - (seq.m).|| < r by NORMSP_1:7; then
A22: seq.m in {y where y is Point of X:||.v0-y.|| < r};
seq.m in rng seq by FUNCT_2:4,ORDINAL1:def 12;
hence G meets Z by A15,A20,A22,XBOOLE_0:def 4;
end;
hence v in Cl(Y) by A1,A18,PRE_TOPC:def 7;
end;
theorem
for X be RealNormSpace, A being Subset of X
ex F being Subset-Family of X
st (for C being Subset of X holds C in F iff C is closed & A c= C)
& Cl A = meet F
proof
let X be RealNormSpace, A be Subset of X;
reconsider B = A as Subset of LinearTopSpaceNorm X by NORMSP_2:def 4;
consider G being Subset-Family of LinearTopSpaceNorm X such that
A1: (for C being Subset of LinearTopSpaceNorm X
holds C in G iff C is closed & B c= C)
& Cl B = meet G by PRE_TOPC:16;
reconsider F = G as Subset-Family of X by NORMSP_2:def 4;
for C being Subset of X holds C in F iff C is closed & A c= C
proof
let C be Subset of X;
reconsider D = C as Subset of LinearTopSpaceNorm X by NORMSP_2:def 4;
D in G iff D is closed & B c= D by A1;
hence thesis by NORMSP_2:32;
end;
hence thesis by A1,EQCL1;
end;
theorem
for X be RealNormSpace, A,B being Subset of X
st A c= B holds Cl A c= Cl B
proof
let X be RealNormSpace, A,B be Subset of X;
assume
A1: A c= B;
reconsider A1 = A, B1 = B as Subset of LinearTopSpaceNorm X
by NORMSP_2:def 4;
A2: Cl A1 = Cl A by EQCL1;
Cl B1 = Cl B by EQCL1;
hence thesis by A1,A2,PRE_TOPC:19;
end;
theorem
for X be RealNormSpace, A,B being Subset of X
holds Cl(A \/ B) = Cl A \/ Cl B
proof
let X be RealNormSpace, A,B be Subset of X;
reconsider A1 = A, B1 = B as Subset of LinearTopSpaceNorm X
by NORMSP_2:def 4;
A1: Cl A1 = Cl A by EQCL1;
A2: Cl B1 = Cl B by EQCL1;
Cl (A1 \/ B1) = Cl (A \/ B) by EQCL1;
hence thesis by A1,A2,PRE_TOPC:20;
end;
theorem
for X be RealNormSpace, A,B being Subset of X
holds Cl (A /\ B) c= (Cl A) /\ Cl B
proof
let X be RealNormSpace, A,B be Subset of X;
reconsider A1 = A, B1 = B as Subset of LinearTopSpaceNorm X
by NORMSP_2:def 4;
A1: Cl A1 = Cl A by EQCL1;
A2: Cl B1 = Cl B by EQCL1;
Cl (A1 /\ B1) = Cl (A /\ B) by EQCL1;
hence thesis by A1,A2,PRE_TOPC:21;
end;
theorem
for X be RealNormSpace, A being Subset of X
holds A is closed iff Cl A = A
proof
let X be RealNormSpace, A be Subset of X;
reconsider A1 = A as Subset of LinearTopSpaceNorm X by NORMSP_2:def 4;
A1: Cl A1 = Cl A by EQCL1;
A1 is closed iff A is closed by NORMSP_2:32;
hence thesis by A1,PRE_TOPC:22;
end;
theorem
for X be RealNormSpace, A being Subset of X
holds A is open iff Cl([#](X) \ A) = [#](X) \ A
proof
let X be RealNormSpace, A be Subset of X;
reconsider A1 = A as Subset of LinearTopSpaceNorm X by NORMSP_2:def 4;
A1: [#](X) = [#](LinearTopSpaceNorm X) by NORMSP_2:def 4;
A2: Cl([#](LinearTopSpaceNorm X) \ A1) = Cl([#]X \ A) by A1,EQCL1;
A1 is open iff A is open by NORMSP_2:33;
hence thesis by A1,A2,PRE_TOPC:23;
end;
theorem Cl01:
for X be RealNormSpace,
Y be Subspace of X,
CY be Subset of X
st CY = the carrier of Y
holds Cl(CY) is linearly-closed
proof
let X be RealNormSpace,
Y be Subspace of X,
CY be Subset of X;
assume
A1: CY = the carrier of Y;
A2: for v,u be Point of X st v in Cl(CY) & u in Cl(CY) holds v+u in Cl(CY)
proof
let v,u be Point of X;
assume
A3: v in Cl(CY) & u in Cl(CY);
thus v+u in Cl(CY)
proof
consider seqv be sequence of X such that
A4: rng seqv c= CY & seqv is convergent & lim seqv = v by A3,EQCL3;
consider sequ be sequence of X such that
A5: rng sequ c= CY & sequ is convergent & lim sequ = u by A3,EQCL3;
now
let y be object;
assume y in rng (seqv + sequ); then
consider x being object such that
A6: x in NAT & (seqv + sequ).x = y by FUNCT_2:11;
reconsider x as Element of NAT by A6;
seqv.x in rng seqv & sequ.x in rng sequ by FUNCT_2:4; then
seqv.x in Y & sequ.x in Y by A1,A4,A5; then
seqv.x + sequ.x in Y by RLSUB_1:20;
hence y in CY by A1,A6,NORMSP_1:def 2;
end; then
A7: rng(seqv + sequ) c= CY;
lim(seqv + sequ) = v+u by A4,A5,NORMSP_1:25;
hence v+u in Cl(CY) by A4,A5,A7,EQCL3,NORMSP_1:19;
end;
end;
for r be Real, v be Point of X st v in Cl(CY) holds r*v in Cl(CY)
proof
let r be Real, v be Point of X;
assume
A8: v in Cl(CY);
thus r*v in Cl(CY)
proof
consider seqv be sequence of X such that
A9: rng seqv c= CY & seqv is convergent & lim seqv = v by A8,EQCL3;
A10: r*seqv is convergent & lim(r*seqv) = r*lim(seqv)
by A9,NORMSP_1:22,NORMSP_1:28;
now
let y be object;
assume y in rng (r*seqv); then
consider x being object such that
A11: x in NAT & (r*seqv).x = y by FUNCT_2:11;
reconsider x as Element of NAT by A11;
seqv.x in rng seqv by FUNCT_2:4; then
seqv.x in Y by A1,A9; then
r*seqv.x in Y by RLSUB_1:21;
hence y in CY by A1,A11,NORMSP_1:def 5;
end; then
rng(r*seqv) c= CY;
hence r*v in Cl(CY) by A9,A10,EQCL3;
end;
end;
hence thesis by A2;
end;
begin :: Density
definition
let X be RealNormSpace, A be Subset of X;
attr A is dense means
Cl A = [#] X;
end;
registration
let X be RealNormSpace;
cluster [#]X -> dense;
correctness
proof
A1: Cl ([#](LinearTopSpaceNorm X)) = [#] (LinearTopSpaceNorm X)
by TOPS_1:def 3;
[#](LinearTopSpaceNorm X) = [#] X by NORMSP_2:def 4;
hence thesis by A1,EQCL1;
end;
end;
registration
let X be RealNormSpace;
cluster open closed dense for Subset of X;
correctness
proof
take [#]X;
thus thesis;
end;
end;
theorem
for X be RealNormSpace, A be Subset of X
holds
A is dense
iff
for x be Point of X ex seq be sequence of X
st rng seq c= A & seq is convergent & lim seq = x
proof
let X be RealNormSpace, A be Subset of X;
thus A is dense implies for x be Point of X ex seq be sequence of X
st rng seq c= A & seq is convergent & lim seq = x by EQCL3;
assume
A1: for x be Point of X ex seq be sequence of X
st rng seq c= A & seq is convergent & lim seq = x;
for z be object st z in [#] X holds z in Cl A
proof
let z be object;
assume z in [#] X; then
reconsider x = z as Point of X;
ex seq be sequence of X
st rng seq c= A & seq is convergent & lim seq = x by A1;
hence thesis by EQCL3;
end; then
[#] X c= Cl A; then
[#] X = Cl A;
hence thesis;
end;
theorem EQCL2:
for X be RealNormSpace,
Y be Subset of X,
Z be Subset of LinearTopSpaceNorm X
st Y = Z
holds Y is dense iff Z is dense
proof
let X be RealNormSpace,
Y be Subset of X,
Z be Subset of LinearTopSpaceNorm X;
assume
A1: Y = Z;
hereby
assume Y is dense; then
Cl Z = [#] X by A1,EQCL1
.= [#] LinearTopSpaceNorm X by NORMSP_2:def 4;
hence Z is dense;
end;
assume Z is dense; then
Cl Y = [#] (LinearTopSpaceNorm X) by A1,EQCL1
.= [#]X by NORMSP_2:def 4;
hence Y is dense;
end;
theorem
for X be RealNormSpace, R,S being Subset of X
st R is dense & R c= S
holds S is dense
proof
let X be RealNormSpace, R,S be Subset of X;
reconsider R1 = R, S1 = S as Subset of LinearTopSpaceNorm X
by NORMSP_2:def 4;
assume R is dense & R c= S; then
R1 is dense & R1 c= S1 by EQCL2; then
S1 is dense by TOPS_1:44;
hence S is dense by EQCL2;
end;
theorem TOPS145:
for X be RealNormSpace, R be Subset of X
holds
R is dense
iff
for S be Subset of X st S <> {} & S is open holds R meets S
proof
let X be RealNormSpace, R be Subset of X;
reconsider R1 = R as Subset of LinearTopSpaceNorm X by NORMSP_2:def 4;
hereby
assume R is dense; then
A1: R1 is dense by EQCL2;
thus for S be Subset of X st S <> {} & S is open holds R meets S
proof
let S be Subset of X;
assume
A2: S <> {} & S is open;
reconsider S1 = S as Subset of LinearTopSpaceNorm X by NORMSP_2:def 4;
S1 is open by A2,NORMSP_2:33;
hence R meets S by A1,A2,TOPS_1:45;
end;
end;
assume
A3: for S be Subset of X st S <> {} & S is open holds R meets S;
for S1 be Subset of LinearTopSpaceNorm X st S1 <> {} & S1 is open
holds R1 meets S1
proof
let S1 be Subset of LinearTopSpaceNorm X;
assume
A4: S1 <> {} & S1 is open;
reconsider S = S1 as Subset of X by NORMSP_2:def 4;
S is open by A4,NORMSP_2:33;
hence R1 meets S1 by A3,A4;
end; then
R1 is dense by TOPS_1:45;
hence R is dense by EQCL2;
end;
theorem
for X be RealNormSpace, R,S be Subset of X
st R is dense & S is open
holds Cl S = Cl(S /\ R)
proof
let X be RealNormSpace, R,S be Subset of X;
reconsider R1 = R, S1 = S as Subset of LinearTopSpaceNorm X
by NORMSP_2:def 4;
A1: Cl S = Cl S1 by EQCL1;
A2: Cl(S1 /\ R1) = Cl(S /\ R) by EQCL1;
assume R is dense & S is open; then
R1 is dense & S1 is open by EQCL2,NORMSP_2:33;
hence Cl S = Cl(S /\ R) by A1,A2,TOPS_1:46;
end;
theorem
for X be RealNormSpace, R,S be Subset of X
st R is dense & S is dense open
holds R /\ S is dense
proof
let X be RealNormSpace, R,S be Subset of X;
reconsider R1 = R, S1 = S as Subset of LinearTopSpaceNorm X
by NORMSP_2:def 4;
assume R is dense & S is dense open; then
R1 is dense & S1 is dense & S1 is open by EQCL2,NORMSP_2:33; then
R1 /\ S1 is dense by TOPS_1:47;
hence R /\ S is dense by EQCL2;
end;
theorem NONEMP:
for X be RealNormSpace, A be Subset of X
st A is dense holds A is non empty
proof
let X be RealNormSpace, A be Subset of X;
assume A is dense; then
A meets [#]X by TOPS145;
hence A is non empty;
end;
begin :: Separability
definition
let X be RealNormSpace;
attr X is separable means
LinearTopSpaceNorm X is separable;
end;
theorem
for X be RealNormSpace holds
X is separable iff ex seq be sequence of X st rng seq is dense
proof
let X be RealNormSpace;
set Y = LinearTopSpaceNorm X;
consider B being Subset of Y such that
A1: B is dense & density Y = card B by TOPGEN_1:def 12;
hereby
assume
A2: X is separable;
reconsider A = B as Subset of X by NORMSP_2:def 4;
A is dense by A1,EQCL2; then
A3: A is non empty by NONEMP;
A is countable by A1,A2,CARD_3:def 14,TOPGEN_1:def 13; then
consider f be Function of omega, A such that
A4: rng f = A by A3,CARD_3:96;
reconsider seq = f as Function of NAT, the carrier of X
by A3,A4,FUNCT_2:6;
reconsider seq as sequence of X;
rng seq is dense by A1,A4,EQCL2;
hence ex seq be sequence of X st rng seq is dense;
end;
given seq be sequence of X such that
A5: rng seq is dense;
reconsider D = rng seq as Subset of Y by NORMSP_2:def 4;
D is dense by A5,EQCL2; then
A6: density Y c= card D by TOPGEN_1:def 12;
dom seq = NAT by FUNCT_2:def 1; then
card D c= omega by CARD_3:93,def 14; then
density Y c= omega by A6;
hence thesis by TOPGEN_1:def 13;
end;
begin :: Sequence and Convergence
theorem LMINEQ:
for x,y,z be Real st 0 <= y
& for e be Real st 0 < e holds x <= z + y*e
holds x <= z
proof
let x,y,z be Real such that
A1: 0 <= y and
A2: for e be Real st 0 < e holds x <= z + y*e;
per cases;
suppose
A3: y = 0;
x <= z + y*1 by A2;
hence x <= z by A3;
end;
suppose
A4: y<>0;
thus x <= z
proof
assume not x <= z; then
A6: 0 < x-z by XREAL_1:50; then
x <= z + y*(((x-z)/2)/y) by A1,A2,A4; then
A7: x <= z + (y*((x-z)/2))/y by XCMPLX_1:74;
(x-z)/2 < x-z by A6,XREAL_1:216; then
z + (x-z)/2 < z + (x-z) by XREAL_1:8;
hence contradiction by A4,A7,XCMPLX_1:89;
end;
end;
end;
theorem CLOSE01:
for X be RealNormSpace,
x be Point of X,
seq be sequence of X
st for n be Nat holds seq.n = x
holds seq is convergent & lim seq = x
proof
let X be RealNormSpace,
x be Point of X,
seq be sequence of X;
assume
A1: for n be Nat holds seq.n = x;
now
let z,w be object;
assume z in dom seq & w in dom seq; then
reconsider n1 = z, n2 = w as Nat;
thus seq.z = seq.n1
.= x by A1
.= seq.n2 by A1
.= seq.w;
end; then
A2: seq is constant by FUNCT_1:def 10;
hence seq is convergent by NDIFF_1:18;
thus lim seq = seq.0 by A2,NDIFF_1:18
.= x by A1;
end;
theorem
for X be RealNormSpace, x be Point of X holds {x} is closed
proof
let X be RealNormSpace, x be Point of X;
for s1 be sequence of X st rng s1 c= {x} & s1 is convergent
holds lim s1 in {x}
proof
let s1 be sequence of X;
assume
A1: rng s1 c= {x} & s1 is convergent;
now
let n be Nat;
s1.n in rng s1 by FUNCT_2:4,ORDINAL1:def 12;
hence s1.n = x by A1,TARSKI:def 1;
end; then
lim s1 = x by CLOSE01;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
theorem CLOSE1:
for X be RealNormSpace,
Y be Subset of X,
v be VECTOR of X
st Y is closed
& for e be Real st 0 < e
holds ex w be VECTOR of X st w in Y & ||.v-w.|| <= e
holds v in Y
proof
let X be RealNormSpace,
Y be Subset of X,
v be VECTOR of X;
assume that
A1: Y is closed and
A2: for e be Real st 0 < e
holds ex w be VECTOR of X st w in Y & ||.v-w.|| <= e;
assume
A3: not v in Y;
reconsider Z = Y` as Subset of TopSpaceNorm X;
A4: Z is open by A1,NORMSP_2:16;
v in (the carrier of X) \ Y by A3,XBOOLE_0:def 5; then
v in Z by SUBSET_1:def 4; then
consider e be Real such that
A5: e > 0 & {y where y is Point of X: ||.v-y.|| < e} c= Z by A4,NORMSP_2:7;
consider w be VECTOR of X such that
A6: w in Y & ||.v-w.|| <= e/2 by A2,A5;
e/2 < e by A5,XREAL_1:216; then
||.v-w.|| < e by A6,XXREAL_0:2; then
w in {y where y is Point of X: ||.v-y.|| < e}; then
w in Y` by A5; then
w in (the carrier of X) \ Y by SUBSET_1:def 4;
hence contradiction by A6,XBOOLE_0:def 5;
end;
begin :: Subspace
theorem NSUBA:
for V be RealNormSpace,
W be SubRealNormSpace of V
st the carrier of W = the carrier of V
holds the NORMSTR of W = the NORMSTR of V
proof
let V be RealNormSpace,
W be SubRealNormSpace of V;
assume
A1: the carrier of W = the carrier of V;
A2: 0.W = 0.V by DUALSP01:def 16;
A3: the addF of W = (the addF of V) || the carrier of W by DUALSP01:def 16
.= the addF of V by A1;
A4: the Mult of W
= (the Mult of V) | [:REAL, the carrier of W:] by DUALSP01:def 16
.= the Mult of V by A1;
the normF of W
= (the normF of V) | (the carrier of W) by DUALSP01:def 16
.= the normF of V by A1;
hence thesis by A2,A3,A4;
end;
theorem
for V be RealNormSpace,
W be SubRealNormSpace of V
holds W is Subspace of V
proof
let V be RealNormSpace,
W be SubRealNormSpace of V;
the carrier of W c= the carrier of V
& 0.W = 0.V
& the addF of W = (the addF of V) || (the carrier of W)
& the Mult of W = (the Mult of V) | [:REAL, the carrier of W:]
& the normF of W = (the normF of V) | (the carrier of W)
by DUALSP01:def 16;
hence thesis by RLSUB_1:def 2;
end;
theorem SUBTH0:
for V be RealNormSpace,
V1 be SubRealNormSpace of V,
x,y being Point of V,
x1,y1 being Point of V1,
a be Real
st x = x1 & y = y1 holds
||.x.|| = ||.x1.||
& x+y = x1+y1
& a*x = a*x1
proof
let V be RealNormSpace,
V1 be SubRealNormSpace of V,
x,y be Point of V,
x1,y1 be Point of V1,
a be Real;
assume
A1: x = x1 & y = y1;
reconsider aa = a as Element of REAL by XREAL_0:def 1;
thus ||.x1.|| = ((the normF of V) | (the carrier of V1)).x1
by DUALSP01:def 16
.= ||.x.|| by A1,FUNCT_1:49;
thus x1+y1 = ((the addF of V) || (the carrier of V1)) . [x1,y1]
by DUALSP01:def 16
.= x+y by A1,FUNCT_1:49;
A2: [aa,x1] in [:REAL, the carrier of V1:];
aa*x1 = ((the Mult of V) | [:REAL, the carrier of V1:]).[a,x1]
by DUALSP01:def 16
.= aa*x by A1,A2,FUNCT_1:49;
hence a*x = a*x1;
end;
theorem RLSUB134:
for V be RealNormSpace,
V1 be SubRealNormSpace of V,
S be Subset of V
st S = the carrier of V1
holds S is linearly-closed
proof
let V be RealNormSpace,
V1 be SubRealNormSpace of V,
S be Subset of V;
assume
A1: S = the carrier of V1;
A2: for v,u be VECTOR of V st v in S & u in S holds v+u in S
proof
let v,u be VECTOR of V such that
A3: v in S and
A4: u in S;
reconsider v1 = v, u1 = u as Point of V1 by A1,A3,A4;
v+u = v1+u1 by SUBTH0;
hence thesis by A1;
end;
for r be Real for v be VECTOR of V st v in S holds r*v in S
proof
let r be Real;
let v be VECTOR of V such that
A5: v in S;
reconsider v1 = v as Point of V1 by A1,A5;
r*v = r*v1 by SUBTH0;
hence thesis by A1;
end;
hence thesis by A2;
end;
definition
let X be RealNormSpace;
let X1 be set;
assume
A1: X1 c= the carrier of X;
func Norm_(X1,X) -> Function of X1,REAL equals
:DefNorm:
(the normF of X) | X1;
correctness
proof
A2: dom the normF of X = the carrier of X by FUNCT_2:def 1;
A3: for z being object st z in X1 holds
((the normF of X) | X1) . z in REAL
proof
let z be object;
assume
A4: z in X1; then
reconsider y = z as VECTOR of X by A1;
z in dom ( (the normF of X) | X1 ) by A1,A2,A4,RELAT_1:62; then
((the normF of X) | X1) . z = ||.y.|| by FUNCT_1:47;
hence ((the normF of X) | X1) . z in REAL;
end;
dom ((the normF of X) | X1) = X1 by A1,A2,RELAT_1:62;
hence (the normF of X) | X1 is Function of X1,REAL by A3,FUNCT_2:3;
end;
end;
definition
let V be RealNormSpace, V1 be Subset of V;
func NLin(V1) -> non empty NORMSTR equals
NORMSTR(# the carrier of Lin(V1), 0.Lin(V1),
the addF of Lin(V1),
the Mult of Lin(V1),
Norm_(the carrier of Lin(V1),V) #);
correctness;
end;
SUBTH:
for V be RealNormSpace,
V1 be Subset of V,
x,y being Point of V,
x1,y1 being Point of NLin(V1),
a be Real st x = x1 & y = y1 holds
||.x.|| = ||.x1.||
& x+y = x1+y1
& a*x = a*x1
proof
let V be RealNormSpace,
V1 be Subset of V,
x,y be Point of V,
x1,y1 be Point of NLin(V1),
a be Real;
assume
A1: x = x1 & y = y1;
set l = NLin(V1);
A2: the carrier of l c= the carrier of V by RLSUB_1:def 2;
reconsider x2 = x1 as Point of Lin(V1);
reconsider y2 = y1 as Point of Lin(V1);
thus ||.x1.|| = ((the normF of V) | (the carrier of l)).x1 by A2,DefNorm
.= ||.x.|| by A1,FUNCT_1:49;
thus x1+y1 = x2+y2
.= x+y by A1,RLSUB_1:13;
thus a*x1 = a*x2
.= a*x by A1,RLSUB_1:14;
end;
XTh7:
for V be RealNormSpace,
V1 be Subset of V,
x,y be Point of NLin(V1),
a be Real holds
(||.x.|| = 0 iff x = 0.NLin(V1))
& 0 <= ||.x.||
& ||.x+y.|| <= ||.x.|| + ||.y.||
& ||.a*x.|| = |.a.| * ||.x.||
proof
let V be RealNormSpace, V1 be Subset of V;
let x,y be Point of NLin(V1), a be Real;
set l = NLin(V1);
the carrier of l c= the carrier of V by RLSUB_1:def 2; then
reconsider x0 = x, y0 = y as Point of V;
A1: ||.x.|| = ||.x0.|| by SUBTH;
A2: ||.y.|| = ||.y0.|| by SUBTH;
A3: 0.NLin(V1) = 0.V by RLSUB_1:11;
x+y = x0+y0 by SUBTH; then
A4: ||.x0+y0.|| = ||.x+y.|| by SUBTH;
a*x = a*x0 by SUBTH; then
A5: ||.a*x0.|| = ||.a*x.|| by SUBTH;
thus (||.x.|| = 0 iff x = 0.NLin(V1)) by A1,A3,NORMSP_0:def 5;
thus 0 <= ||.x.|| by A1;
thus ||.x+y.|| <= ||.x.|| + ||.y.|| by A1,A2,A4,NORMSP_1:def 1;
thus ||.a*x.|| = |.a.| * ||.x.|| by A1,A5,NORMSP_1:def 1;
end;
theorem ThSubSpace:
for V be RealNormSpace, V1 be Subset of V
holds NLin(V1) is SubRealNormSpace of V
proof
let V be RealNormSpace;
let V1 be Subset of V;
set l = NLin(V1);
A1: the carrier of l c= the carrier of V by RLSUB_1:def 2;
A2: l is reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable
by RSSPACE:15,XTh7;
A3: 0.l = 0.V by RLSUB_1:def 2;
A4: the addF of l
= (the addF of V) || (the carrier of l) by RLSUB_1:def 2;
A5: the Mult of l
= (the Mult of V) | [:REAL, the carrier of l:] by RLSUB_1:def 2;
the normF of l = (the normF of V) | (the carrier of l) by A1,DefNorm;
hence thesis by A1,A2,A3,A4,A5,DUALSP01:def 16;
end;
definition
let V be RealNormSpace, V1 be Subset of V;
redefine func NLin(V1) -> SubRealNormSpace of V; :: redefines NLin (NORMSP_3, definition)
coherence by ThSubSpace;
end;
theorem LCL1:
for V be RealLinearSpace, V1 be Subset of V
st V1 <> {} & V1 is linearly-closed
holds the carrier of Lin(V1) = V1
proof
let V be RealLinearSpace, V1 be Subset of V;
assume V1 <> {} & V1 is linearly-closed; then
ex W0 being strict Subspace of V st V1 = the carrier of W0 by RLSUB_1:35;
hence the carrier of Lin(V1) = V1 by RLVECT_3:18;
end;
theorem
for V be RealNormSpace,
W be SubRealNormSpace of V,
V1 be Subset of V
st the carrier of W = V1
holds NLin(V1) = the NORMSTR of W
proof
let V be RealNormSpace,
W be SubRealNormSpace of V,
V1 be Subset of V;
assume
A1: the carrier of W = V1;
set l = NLin(V1);
A2: the carrier of l c= the carrier of V by RLSUB_1:def 2;
A3: the carrier of l = the carrier of W by A1,LCL1,RLSUB134;
A4: 0.l = 0.V by RLSUB_1:def 2;
A5: the addF of l = (the addF of V)|| the carrier of l by RLSUB_1:def 2;
A6: the Mult of l = (the Mult of V) | [:REAL, the carrier of l:]
by RLSUB_1:def 2;
A7: 0.W = 0.l by A4,DUALSP01:def 16;
A8: the addF of W = the addF of l by A3,A5,DUALSP01:def 16;
the normF of W = (the normF of V) | (the carrier of W) by DUALSP01:def 16
.= the normF of l by A2,A3,DefNorm;
hence thesis by A6,A7,A8,DUALSP01:def 16;
end;
begin :: Linear Functions
theorem KERX1:
for X,Y be RealLinearSpace,
f be Function of X, Y
st f is homogeneous
holds f"{0.Y} is non empty
proof
let X,Y be RealLinearSpace,
f be Function of X, Y;
assume
A1: f is homogeneous;
f.(0.X) = f.(0 * 0.X) by RLVECT_1:10
.= 0 * f.(0.X) by A1,LOPBAN_1:def 5
.= 0.Y by RLVECT_1:10; then
f.(0.X) in {0.Y} by TARSKI:def 1;
hence thesis by FUNCT_2:38;
end;
registration
let X,Y be RealLinearSpace,
f be LinearOperator of X,Y;
cluster f"{0.Y} -> non empty;
correctness by KERX1;
end;
theorem KLXY1:
for X,Y be RealLinearSpace,
f be Function of X, Y
st f is additive homogeneous
holds f"{0.Y} is linearly-closed
proof
let X,Y be RealLinearSpace,
f be Function of X, Y;
assume
A1: f is additive homogeneous;
set X1 = f"{0.Y};
A2: for v,u be Point of X st v in X1 & u in X1 holds v+u in X1
proof
let v,u be Point of X;
assume AS1: v in X1 & u in X1; then
v in the carrier of X & f.v in {0.Y} by FUNCT_2:38; then
A3: f.v = 0.Y by TARSKI:def 1;
A4: u in the carrier of X & f.u in {0.Y} by AS1,FUNCT_2:38;
f.(v+u) = f.v + f.u by A1
.= 0.Y + 0.Y by A3,A4,TARSKI:def 1
.= 0.Y by RLVECT_1:4; then
f.(v+u) in {0.Y} by TARSKI:def 1;
hence thesis by FUNCT_2:38;
end;
for r be Real, v be Point of X st v in X1 holds r*v in X1
proof
let r be Real, v be Point of X;
assume v in X1; then
A5: v in the carrier of X & f.v in {0.Y} by FUNCT_2:38;
f.(r*v) = r * (f.v) by A1,LOPBAN_1:def 5
.= r * 0.Y by A5,TARSKI:def 1
.= 0.Y by RLVECT_1:10; then
f.(r*v) in {0.Y} by TARSKI:def 1;
hence thesis by FUNCT_2:38;
end;
hence thesis by A2;
end;
theorem IMX2:
for X,Y be RealLinearSpace,
f be Function of X, Y
st f is additive homogeneous
holds rng f is linearly-closed
proof
let X,Y be RealLinearSpace,
f be Function of X, Y;
assume
A1: f is additive homogeneous;
set Y1 = rng f;
A2: for v,u be Point of Y st v in Y1 & u in Y1 holds v+u in Y1
proof
let v,u be Point of Y;
assume
A3: v in Y1 & u in Y1; then
consider x1 be Element of the carrier of X such that
A4: v = f.x1 by FUNCT_2:113;
consider x2 be Element of the carrier of X such that
A5: u = f.x2 by A3,FUNCT_2:113;
v+u = f.(x1+x2) by A1,A4,A5;
hence thesis by FUNCT_2:4;
end;
for r be Real, v be Point of Y st v in Y1 holds r*v in Y1
proof
let r be Real, v be Point of Y;
assume v in Y1; then
consider x be Element of the carrier of X such that
A6: v = f.x by FUNCT_2:113;
r*v = f.(r*x) by A1,A6,LOPBAN_1:def 5;
hence thesis by FUNCT_2:4;
end;
hence thesis by A2;
end;
definition
let X,Y be RealLinearSpace,
f be LinearOperator of X,Y;
func Ker(f) -> Subspace of X equals
Lin(f"{0.Y});
coherence;
end;
definition
let X,Y be RealNormSpace,
f be LinearOperator of X,Y;
func NKer(f) -> SubRealNormSpace of X equals
NLin(f"{0.Y});
coherence;
end;
definition
let X,Y be RealLinearSpace,
f be LinearOperator of X,Y;
func Im(f) -> Subspace of Y equals
Lin(rng f);
coherence;
end;
definition
let X,Y be RealNormSpace,
f be LinearOperator of X,Y;
func Im(f) -> SubRealNormSpace of Y equals
NLin(rng f);
coherence;
end;
definition
let X,Y be RealLinearSpace,
L be LinearOperator of X,Y;
attr L is isomorphism means
L is one-to-one onto;
end;
registration
let X,Y be RealLinearSpace;
cluster isomorphism -> one-to-one onto for LinearOperator of X,Y;
coherence;
cluster one-to-one onto -> isomorphism for LinearOperator of X,Y;
coherence;
end;
theorem
for X,Y be RealLinearSpace,
L be LinearOperator of X,Y
st L is isomorphism holds
ex K be LinearOperator of Y,X st K = L" & K is isomorphism
proof
let X,Y be RealLinearSpace,
L be LinearOperator of X,Y;
assume
A1: L is isomorphism; then
A2: L is one-to-one & L is onto;
reconsider K = L" as Function of Y,X by A2,FUNCT_2:25;
A3: dom L = the carrier of X by FUNCT_2:def 1;
A4: K is additive
proof
let x,y be Point of Y;
consider a be Point of X such that
A5: x = L.a by A2,FUNCT_2:113;
consider b be Point of X such that
A6: y = L.b by A2,FUNCT_2:113;
A7: K.x = a by A1,A3,A5,FUNCT_1:34;
A8: K.y = b by A1,A3,A6,FUNCT_1:34;
x+y = L.(a+b) by A5,A6,VECTSP_1:def 20;
hence K.(x+y) = K.x + K.y by A1,A3,A7,A8,FUNCT_1:34;
end;
K is homogeneous
proof
let x be Point of Y, r be Real;
consider a be Point of X such that
A10: x = L.a by A2,FUNCT_2:113;
A11: K.x = a by A1,A3,A10,FUNCT_1:34;
A12: r*x = L.(r*a) by A10,LOPBAN_1:def 5;
thus K.(r*x) = r * K.x by A1,A3,A11,A12,FUNCT_1:34;
end; then
reconsider K as LinearOperator of Y, X by A4;
take K;
K is onto by A1,A3,FUNCT_1:33;
hence thesis by A1,FUNCT_1:40;
end;
definition
let X,Y be RealNormSpace,
L be LinearOperator of X,Y;
attr L is isomorphism means
L is one-to-one onto
& for x be Point of X holds ||.x.|| = ||.L.x.||;
end;
registration
let X,Y be RealNormSpace;
cluster isomorphism -> one-to-one onto for LinearOperator of X,Y;
coherence;
end;
theorem NISOM01:
for X,Y be RealNormSpace,
L be LinearOperator of X,Y
st L is isomorphism
holds
ex K be Lipschitzian LinearOperator of Y,X
st K = L" & K is isomorphism
proof
let X,Y be RealNormSpace,
L be LinearOperator of X,Y;
assume
A1: L is isomorphism; then
A2: L is one-to-one & L is onto
& for x be Point of X holds ||.x.|| = ||.L.x.||;
reconsider K = L" as Function of Y,X by A2,FUNCT_2:25;
A3: dom L = the carrier of X by FUNCT_2:def 1;
A4: K is additive
proof
let x,y be Point of Y;
consider a be Point of X such that
A5: x = L.a by A2,FUNCT_2:113;
consider b be Point of X such that
A6: y = L.b by A2,FUNCT_2:113;
A7: K.x = a by A1,A3,A5,FUNCT_1:34;
A8: K.y = b by A1,A3,A6,FUNCT_1:34;
x+y = L.(a+b) by A5,A6,VECTSP_1:def 20;
hence K.(x+y) = K.x + K.y by A1,A3,A7,A8,FUNCT_1:34;
end;
K is homogeneous
proof
let x be Point of Y, r be Real;
consider a be Point of X such that
A10: x = L.a by A2,FUNCT_2:113;
A11: K.x = a by A1,A3,A10,FUNCT_1:34;
A12: r*x = L.(r*a) by A10,LOPBAN_1:def 5;
thus K.(r*x) = r * K.x by A1,A3,A11,A12,FUNCT_1:34;
end; then
reconsider K as LinearOperator of Y, X by A4;
A13: K is onto by A1,A3,FUNCT_1:33;
A14: for y be Point of Y holds ||.y.|| = ||.K.y.||
proof
let y be Point of Y;
consider b be Point of X such that
A15: y = L.b by A2,FUNCT_2:113;
K.y = b by A1,A3,A15,FUNCT_1:34;
hence ||.y.|| = ||.K.y.|| by A1,A15;
end; then
for x being VECTOR of Y holds ||.K.x.|| <= 1 * ||.x.||; then
reconsider K as Lipschitzian LinearOperator of Y,X by LOPBAN_1:def 8;
take K;
thus thesis by A1,A13,A14,FUNCT_1:40;
end;
theorem NISOM02:
for X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
seq be sequence of X holds
seq is convergent implies L * seq is convergent & lim(L * seq) = L.(lim seq)
proof
let X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
seq be sequence of X;
assume
A1: seq is convergent;
A2: L is_continuous_on the carrier of X by LOPBAN_7:6;
A3: the carrier of X = dom L by FUNCT_2:def 1;
A4: rng seq c= the carrier of X;
lim seq in the carrier of X; then
A5: L /* seq is convergent & L /. (lim seq) = lim(L /* seq)
by A1,A2,A4,NFCONT_1:18;
rng seq c= dom L by A3;
hence thesis by A5,FUNCT_2:def 11;
end;
theorem KERCL01:
for X,Y be RealNormSpace,
L be Function of X,Y,
w be Point of Y
st L is_continuous_on the carrier of X
holds L"{w} is closed
proof
let X,Y be RealNormSpace,
L be Function of X,Y,
w be Point of Y;
assume
A1: L is_continuous_on the carrier of X;
for seq be sequence of X st rng seq c= L"{w} & seq is convergent
holds lim seq in L"{w}
proof
let seq be sequence of X;
assume
A2: rng seq c= L"{w} & seq is convergent;
lim seq in the carrier of X; then
A3: L /* seq is convergent & L /. (lim seq) = lim(L /* seq)
by A1,A2,NFCONT_1:18;
now
let n be Nat;
A4: n in NAT by ORDINAL1:def 12;
seq.n in rng seq by FUNCT_2:4,ORDINAL1:def 12; then
L.(seq.n) in {w} by A2,FUNCT_2:38; then
L.(seq.n) = w by TARSKI:def 1;
hence (L /* seq).n = w by A4,FUNCT_2:115;
end; then
lim(L /* seq) = w by CLOSE01; then
L /. (lim seq) in {w} by A3,TARSKI:def 1;
hence lim seq in L"{w} by FUNCT_2:38;
end;
hence thesis;
end;
theorem
for X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X,Y holds
the carrier of Ker L = L"{0.Y} & L"{0.Y} is closed
by LCL1,KLXY1,KERCL01,LOPBAN_7:6;
theorem NISOM03:
for X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
seq be sequence of X
st L is isomorphism
holds seq is convergent iff L * seq is convergent
proof
let X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
seq be sequence of X;
assume
A1: L is isomorphism;
A2: dom L = the carrier of X by FUNCT_2:def 1;
set Lseq = L * seq;
set Ls = L.(lim seq);
thus seq is convergent implies Lseq is convergent by NISOM02;
assume
A3: Lseq is convergent;
consider K be Lipschitzian LinearOperator of Y,X such that
A4: K = L" & K is isomorphism by A1,NISOM01;
for n be Element of NAT holds (K * Lseq).n = seq.n
proof
let n be Element of NAT;
A5: dom seq = NAT by FUNCT_2:def 1;
dom Lseq = NAT by FUNCT_2:def 1;
hence (K * Lseq).n = K.(Lseq.n) by FUNCT_1:13
.= L".(L.(seq.n)) by A4,A5,FUNCT_1:13
.= seq.n by A1,A2,FUNCT_1:34;
end; then
K * Lseq = seq;
hence seq is convergent by A3,NISOM02;
end;
theorem NISOM04:
for X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
seq be sequence of X
st L is isomorphism
holds
seq is Cauchy_sequence_by_Norm implies L * seq is Cauchy_sequence_by_Norm
proof
let X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
seq be sequence of X;
assume
A1: L is isomorphism;
set Lseq = L * seq;
assume
A2: seq is Cauchy_sequence_by_Norm;
for r be Real st r > 0 ex k be Nat
st for n, m be Nat st n >= k & m >= k
holds ||.(Lseq.n) - (Lseq.m).|| < r
proof
let r be Real;
assume 0 < r; then
consider k be Nat such that
A3: for n, m be Nat st n >= k & m >= k
holds ||.(seq.n) - (seq.m).|| < r by A2,RSSPACE3:8;
take k;
let n, m be Nat;
assume
A4: n >= k & m >= k;
A5: dom seq = NAT by FUNCT_2:def 1;
(Lseq.n) - (Lseq.m)
= L.(seq.n) - (L*seq).m by A5,FUNCT_1:13,ORDINAL1:def 12
.= L.(seq.n) + - L.(seq.m) by A5,FUNCT_1:13,ORDINAL1:def 12
.= L.(seq.n) + (-1) * L.(seq.m) by RLVECT_1:16
.= L.(seq.n) + L.((- 1)*(seq.m)) by LOPBAN_1:def 5
.= L.((seq.n) + (- 1)*(seq.m)) by VECTSP_1:def 20
.= L.((seq.n) - (seq.m)) by RLVECT_1:16; then
||.(Lseq.n) - (Lseq.m).|| = ||.(seq.n) - seq.m.|| by A1;
hence ||.(Lseq.n) - (Lseq.m).|| < r by A3,A4;
end;
hence thesis by RSSPACE3:8;
end;
theorem NISOM05:
for X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
seq be sequence of X
st L is isomorphism
holds
seq is Cauchy_sequence_by_Norm iff L * seq is Cauchy_sequence_by_Norm
proof
let X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
seq be sequence of X;
assume
A1: L is isomorphism;
A2: dom L = the carrier of X by FUNCT_2:def 1;
set Lseq = L * seq;
thus seq is Cauchy_sequence_by_Norm implies
Lseq is Cauchy_sequence_by_Norm by A1,NISOM04;
assume
A3: Lseq is Cauchy_sequence_by_Norm;
consider K be Lipschitzian LinearOperator of Y,X such that
A4: K = L" & K is isomorphism by A1,NISOM01;
for n be Element of NAT holds (K*Lseq).n = seq.n
proof
let n be Element of NAT;
A5: dom seq = NAT by FUNCT_2:def 1;
dom Lseq = NAT by FUNCT_2:def 1;
hence (K * Lseq).n = K.(Lseq.n) by FUNCT_1:13
.= L".(L.(seq.n)) by A4,A5,FUNCT_1:13
.= seq.n by A1,A2,FUNCT_1:34;
end; then
K * Lseq = seq;
hence seq is Cauchy_sequence_by_Norm by A3,A4,NISOM04;
end;
theorem
for X,Y be RealNormSpace
st ex L be Lipschitzian LinearOperator of X,Y st L is isomorphism
holds X is complete iff Y is complete
proof
let X,Y be RealNormSpace;
given L be Lipschitzian LinearOperator of X,Y such that
A1: L is isomorphism;
hereby
assume
A2: X is complete;
for seq be sequence of Y holds
seq is Cauchy_sequence_by_Norm implies seq is convergent
proof
let seq be sequence of Y;
assume
A3: seq is Cauchy_sequence_by_Norm;
consider K be Lipschitzian LinearOperator of Y,X such that
A4: K = L" & K is isomorphism by A1,NISOM01;
K * seq is Cauchy_sequence_by_Norm by A3,A4,NISOM05; then
K * seq is convergent by A2,LOPBAN_1:def 15;
hence seq is convergent by A4,NISOM03;
end;
hence Y is complete by LOPBAN_1:def 15;
end;
assume
A5: Y is complete;
for seq be sequence of X holds
seq is Cauchy_sequence_by_Norm implies seq is convergent
proof
let seq be sequence of X;
assume seq is Cauchy_sequence_by_Norm; then
L * seq is Cauchy_sequence_by_Norm by A1,NISOM05; then
L * seq is convergent by A5,LOPBAN_1:def 15;
hence seq is convergent by A1,NISOM03;
end;
hence X is complete by LOPBAN_1:def 15;
end;
NISOM06:
for X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
V be Subset of X,
W be Subset of Y
st L is isomorphism & W = L.:V
holds W is closed implies V is closed
proof
let X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
V be Subset of X,
W be Subset of Y;
assume
A1: L is isomorphism & W = L.:V; then
consider K be Lipschitzian LinearOperator of Y,X such that
A2: K = L" & K is isomorphism by NISOM01;
A3: dom L = the carrier of X by FUNCT_2:def 1;
assume
A4: W is closed;
for s1 be sequence of X st rng s1 c= V & s1 is convergent holds lim s1 in V
proof
let s1 be sequence of X;
assume
A5: rng s1 c= V & s1 is convergent;
set s2 = L * s1;
A6: s2 is convergent & lim(s2)= L.(lim s1) by A5,NISOM02;
L.: (rng s1) c= L.:V by A5,RELAT_1:123; then
rng s2 c= W by A1,RELAT_1:127; then
L.(lim s1) in L.:V by A1,A4,A6; then
(L").(L.(lim s1)) in K.:(L.:V) by A2,FUNCT_2:35; then
A8: lim s1 in K.:(L.:V) by A1,A3,FUNCT_1:34;
A9: K.:(L.:V) = L"(L.:V) by A1,A2,FUNCT_1:85;
L"(L.:V) c= V by A1,FUNCT_1:82;
hence lim s1 in V by A8,A9;
end;
hence V is closed;
end;
theorem
for X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
V be Subset of X,
W be Subset of Y
st L is isomorphism & W = L.:V
holds V is closed iff W is closed
proof
let X,Y be RealNormSpace,
L be Lipschitzian LinearOperator of X,Y,
V be Subset of X,
W be Subset of Y;
assume
A1: L is isomorphism & W = L.:V; then
consider K be Lipschitzian LinearOperator of Y,X such that
A2: K = L" & K is isomorphism by NISOM01;
A3: dom L = the carrier of X by FUNCT_2:def 1;
K.:(L.:V) = L"(L.:V) by A1,A2,FUNCT_1:85; then
V = K.:W by A1,A3,FUNCT_1:76,82;
hence V is closed implies W is closed by A2,NISOM06;
thus thesis by A1,NISOM06;
end;
theorem
for X,Y be RealNormSpace, L be LinearOperator of X,Y st L is onto
holds Im(L) = the NORMSTR of Y
proof
let X,Y be RealNormSpace, L be LinearOperator of X,Y;
assume L is onto; then
the carrier of Im(L) = the carrier of Y by LCL1,IMX2;
hence Im(L) = the NORMSTR of Y by NSUBA;
end;
begin :: Banach Space
theorem LM76A:
for V be RealBanachSpace, V1 be SubRealNormSpace of V
st ex CV1 be Subset of V st CV1 = the carrier of V1 & CV1 is closed
holds V1 is RealBanachSpace
proof
let V be RealBanachSpace, V1 be SubRealNormSpace of V;
given CV1 be Subset of V such that
A1: CV1 = the carrier of V1 & CV1 is closed;
for seq be sequence of V1 st seq is Cauchy_sequence_by_Norm
holds seq is convergent
proof
let seq be sequence of V1;
assume
A2: seq is Cauchy_sequence_by_Norm;
the carrier of V1 c= the carrier of V by DUALSP01:def 16; then
reconsider seq1 = seq as sequence of V by FUNCT_2:7;
for r be Real st r > 0 ex k be Nat st for n, m be Nat st n >= k & m >= k
holds ||.(seq1.n) - (seq1.m).|| < r
proof
let r be Real;
assume r > 0; then
consider k be Nat such that
A3: for n, m be Nat st n >= k & m >= k
holds ||.(seq.n) - (seq.m).|| < r by A2,RSSPACE3:8;
take k;
let n, m be Nat;
assume n >= k & m >= k; then
A4: ||.(seq.n) - (seq.m).|| < r by A3;
- (seq.m) = (-1) * seq.m by RLVECT_1:16
.= (-1) * seq1.m by SUBTH0
.= - (seq1.m) by RLVECT_1:16; then
(seq.n) - (seq.m) = (seq1.n) - (seq1.m) by SUBTH0;
hence ||.(seq1.n) - (seq1.m).|| < r by A4,SUBTH0;
end; then
A6: seq1 is convergent by LOPBAN_1:def 15,RSSPACE3:8;
rng seq c= CV1 by A1; then
reconsider s = lim seq1 as Point of V1 by A1,A6;
for r be Real st 0 < r ex m be Nat st for n be Nat st m <= n
holds ||.(seq.n) - s.|| < r
proof
let r be Real;
assume r > 0; then
consider m be Nat such that
A7: for n be Nat st m <= n holds ||.(seq1.n) - lim seq1.|| < r
by A6,NORMSP_1:def 7;
take m;
let n be Nat;
assume m <= n; then
A8: ||.(seq1.n) - lim seq1.|| < r by A7;
- (lim seq1) = (-1) * lim seq1 by RLVECT_1:16
.= (-1) * s by SUBTH0
.= - s by RLVECT_1:16; then
(seq1.n) - (lim seq1) = (seq.n) - s by SUBTH0;
hence ||.(seq.n) - s.|| < r by A8,SUBTH0;
end;
hence seq is convergent;
end;
hence thesis by LOPBAN_1:def 15;
end;
theorem
for V be RealNormSpace,
V1 be SubRealNormSpace of V,
CV1 be Subset of V
st V1 is complete & CV1 = the carrier of V1
holds CV1 is closed
proof
let V be RealNormSpace,
V1 be SubRealNormSpace of V,
CV1 be Subset of V;
assume
A1: V1 is complete & CV1 = the carrier of V1;
for s1 be sequence of V st rng s1 c= CV1 & s1 is convergent
holds lim s1 in CV1
proof
let s1 be sequence of V;
assume
A2: rng s1 c= CV1 & s1 is convergent; then
reconsider s2 = s1 as sequence of V1 by A1,FUNCT_2:6;
for s be Real st 0 < s ex n be Nat st
for m be Nat st n <= m holds ||.s2.m -s2.n.|| < s
proof
let s be Real;
assume 0 < s; then
consider n be Nat such that
A3: for m be Nat st n <= m holds ||.s1.m -s1.n.|| < s
by A2,LOPBAN_3:4;
take n;
let m be Nat;
assume n <= m; then
A4: ||.s1.m -s1.n.|| < s by A3;
- (s1.n) = (-1) * s1.n by RLVECT_1:16
.= (-1) * s2.n by SUBTH0
.= - (s2.n) by RLVECT_1:16; then
(s1.m) - (s1.n) = (s2.m) - (s2.n) by SUBTH0;
hence ||.(s2.m) - (s2.n).|| < s by A4,SUBTH0;
end; then
A6: s2 is convergent by A1,LOPBAN_1:def 15,LOPBAN_3:5;
the carrier of V1 c= the carrier of V by DUALSP01:def 16; then
reconsider s0 = lim s2 as Point of V;
for r be Real st 0 < r ex m be Nat
st for n be Nat st m <= n holds ||.(s1.n) - s0.|| < r
proof
let r be Real;
assume 0 < r; then
consider m be Nat such that
A7: for n be Nat st m <= n holds ||.(s2.n) - lim s2.|| < r
by A6,NORMSP_1:def 7;
take m;
let n be Nat;
assume m <= n; then
A8: ||.(s2.n) - lim s2.|| < r by A7;
- (lim s2) = (-1) * lim s2 by RLVECT_1:16
.= (-1) * s0 by SUBTH0
.= - s0 by RLVECT_1:16; then
(s2.n) - (lim s2) = (s1.n) - s0 by SUBTH0;
hence ||.(s1.n) - s0.|| < r by A8,SUBTH0;
end; then
lim s1 = s0 by A2,NORMSP_1:def 7;
hence lim s1 in CV1 by A1;
end;
hence thesis;
end;
theorem
for X be RealBanachSpace, M be non empty Subset of X
st M is linearly-closed & M is closed
holds NLin(M) is RealBanachSpace
proof
let X be RealBanachSpace, M be non empty Subset of X;
assume
A1: M is linearly-closed & M is closed; then
the carrier of NLin(M) = M by LCL1;
hence thesis by A1,LM76A;
end;
begin :: Quotient Vector Space
definition
let X be RealLinearSpace,
Y be Subspace of X;
redefine func RLSp2RVSp Y -> Subspace of RLSp2RVSp X; :: redefines RLSp2RVSp (DUALSP01, definition)
correctness
proof
set V = RLSp2RVSp X;
set W = RLSp2RVSp Y;
A1: the carrier of W c= the carrier of V by RLSUB_1:def 2;
A2: 0.W = 0.Y
.= 0.X by RLSUB_1:def 2
.= 0.V;
A3: the addF of W = (the addF of V) || the carrier of W by RLSUB_1:def 2;
the lmult of W = (the lmult of V) | [:REAL, the carrier of W:]
by RLSUB_1:def 2;
hence thesis by A1,A2,A3,VECTSP_4:def 2;
end;
end;
definition
let X be RealLinearSpace,
Y be Subspace of X;
func VectQuot(X,Y) -> RealLinearSpace equals
RVSp2RLSp VectQuot(RLSp2RVSp X, RLSp2RVSp Y);
correctness;
end;
theorem
for X be RealLinearSpace,
v be Element of X,
a be Real,
v1 be Element of RLSp2RVSp X,
a1 be Element of F_Real
st v = v1 & a = a1
holds a * v = a1 * v1;
theorem
for X be VectSp of F_Real,
v be Element of X,
a be Element of F_Real,
v1 be Element of RVSp2RLSp X,
a1 be Real
st v = v1 & a = a1
holds a * v = a1 * v1;
theorem LMQ03:
for X be RealLinearSpace,
Y be Subspace of X,
v be Element of X,
v1 be Element of RLSp2RVSp X
st v = v1
holds v + Y = v1 + RLSp2RVSp Y
proof
let X be RealLinearSpace,
Y be Subspace of X,
v be Element of X,
v1 be Element of RLSp2RVSp X;
set V = RLSp2RVSp X;
set W = RLSp2RVSp Y;
assume
A1: v = v1;
for x be object holds x in v+Y iff x in v1 + W
proof
let x be object;
hereby
assume x in v+Y; then
consider y be Point of X such that
A2: x = v + y & y in Y;
reconsider y1 = y as Point of V;
A3: y1 in W by A2;
v + y = v1 + y1 by A1;
hence x in v1 + W by A2,A3;
end;
assume x in v1 + W; then
consider y1 be Element of V such that
A4: x = v1 + y1 & y1 in W;
reconsider y = y1 as Point of X;
A5: y in Y by A4;
v + y = v1 + y1 by A1;
hence x in v + Y by A4,A5;
end;
hence thesis by TARSKI:2;
end;
theorem LMQ04:
for X be RealLinearSpace, Y be Subspace of X holds
for x be object holds x is Coset of Y iff x is Coset of RLSp2RVSp Y
proof
let X be RealLinearSpace, Y be Subspace of X;
let x be object;
hereby
assume x is Coset of Y; then
consider v be Element of X such that
A1: x = v + Y by RLSUB_1:def 6;
reconsider v1 = v as Element of RLSp2RVSp X;
x = v1 + RLSp2RVSp Y by A1,LMQ03;
hence x is Coset of RLSp2RVSp Y by VECTSP_4:def 6;
end;
assume x is Coset of RLSp2RVSp Y; then
consider v1 be Element of RLSp2RVSp X such that
A2: x = v1 + RLSp2RVSp Y by VECTSP_4:def 6;
reconsider v = v1 as Element of X;
x = v + Y by A2,LMQ03;
hence x is Coset of Y by RLSUB_1:def 6;
end;
definition
let X be RealLinearSpace, Y be Subspace of X;
func CosetSet(X,Y) -> non empty Subset-Family of X equals
the set of all A where A is Coset of Y;
correctness
proof
set C = the set of all A where A is Coset of Y;
A1: C c= bool the carrier of X
proof
let x be object;
assume x in C; then
ex A be Coset of Y st A = x;
hence thesis;
end;
the carrier of Y is Coset of Y by RLSUB_1:74; then
the carrier of Y in C;
hence thesis by A1;
end;
end;
definition
let V be RealLinearSpace, W be Subspace of V;
func zeroCoset(V,W) -> Element of CosetSet(V,W) equals
the carrier of W;
coherence
proof
the carrier of W = 0.V+W by RLSUB_1:44; then
the carrier of W is Coset of W by RLSUB_1:def 6; then
the carrier of W in CosetSet(V,W);
hence thesis;
end;
end;
theorem LMQ05:
for X be RealLinearSpace, Y be Subspace of X
holds CosetSet(X,Y) = CosetSet(RLSp2RVSp X,RLSp2RVSp Y)
proof
let X be RealLinearSpace, Y be Subspace of X;
for x be object holds
x in CosetSet(X,Y) iff x in CosetSet(RLSp2RVSp X,RLSp2RVSp Y)
proof
let x be object;
hereby
assume x in CosetSet(X,Y); then
consider A be Coset of Y such that
A1: x = A;
x is Coset of RLSp2RVSp Y by A1,LMQ04;
hence x in CosetSet(RLSp2RVSp X, RLSp2RVSp Y);
end;
assume x in CosetSet(RLSp2RVSp X, RLSp2RVSp Y); then
consider B be Coset of RLSp2RVSp Y such that
A2: x = B;
x is Coset of Y by A2,LMQ04;
hence x in CosetSet(X,Y);
end;
hence thesis by TARSKI:2;
end;
theorem LMQ06:
for V be RealLinearSpace, W be Subspace of V
holds the carrier of VectQuot(V,W) = CosetSet(V,W)
proof
let V be RealLinearSpace, W be Subspace of V;
set X = RLSp2RVSp V;
set Y = RLSp2RVSp W;
thus the carrier of VectQuot(V,W) = CosetSet(X,Y) by VECTSP10:def 6
.= CosetSet(V,W) by LMQ05;
end;
theorem LMQ07:
for V be RealLinearSpace, W be Subspace of V holds
for x be object holds x is Point of VectQuot(V,W)
iff ex v be Point of V st x = v + W
proof
let V be RealLinearSpace, W be Subspace of V;
let x be object;
A1: x in the carrier of VectQuot (V,W)
iff x in CosetSet(V,W) by LMQ06;
(ex A be Coset of W st x = A)
iff ex v be Point of V st x = v + W
proof
thus (ex A be Coset of W st x = A) implies
ex v be Point of V st x = v + W by RLSUB_1:def 6;
assume ex v be Point of V st x = v + W; then
x is Coset of W by RLSUB_1:def 6;
hence thesis;
end;
hence thesis by A1;
end;
theorem LMQ08:
for V be RealLinearSpace, W be Subspace of V
holds 0. VectQuot(V,W) = zeroCoset(V,W)
proof
let V be RealLinearSpace, W be Subspace of V;
set X = RLSp2RVSp V;
set Y = RLSp2RVSp W;
thus 0. VectQuot(V,W) = 0.VectQuot(X,Y)
.= zeroCoset(X,Y) by VECTSP10:def 6
.= zeroCoset(V,W);
end;
theorem LMQ09:
for V be RealLinearSpace, W be Subspace of V holds
for A be VECTOR of VectQuot(V,W), v be VECTOR of V, a be Real st A = v + W
holds a * A = a * v + W
proof
let V be RealLinearSpace, W be Subspace of V;
set X = RLSp2RVSp V;
set Y = RLSp2RVSp W;
let A be VECTOR of VectQuot(V,W), v be VECTOR of V, a be Real;
assume
A1: A = v + W;
reconsider v1 = v as Vector of X;
reconsider A1 = A as Vector of VectQuot (X,Y);
reconsider a1 = a as Element of F_Real by XREAL_0:def 1;
A2: A1 = v1 + Y by A1,LMQ03;
thus a * A = a1 * A1
.= (a1 * v1) + Y by A2,VECTSP10:25
.= (a * v) + W by LMQ03;
end;
theorem LMQ10:
for V be RealLinearSpace, W be Subspace of V holds
for A be VECTOR of VectQuot(V,W), v be VECTOR of V, a be Real st A = v + W
holds -A = -v + W
proof
let V be RealLinearSpace, W be Subspace of V;
let A be VECTOR of VectQuot(V,W), v be VECTOR of V, a be Real;
assume
A1: A = v + W;
thus -A = (-1) * A by RLVECT_1:16
.= (-1) * v + W by A1,LMQ09
.= -v + W by RLVECT_1:16;
end;
theorem LMQ11:
for V be RealLinearSpace, W be Subspace of V holds
for A1,A2 be VECTOR of VectQuot(V,W),
v1,v2 be VECTOR of V
st A1 = v1 + W & A2 = v2 + W
holds A1 + A2 = v1 + v2 + W
proof
let V be RealLinearSpace, W be Subspace of V;
set X = RLSp2RVSp V;
set Y = RLSp2RVSp W;
let A1,A2 be VECTOR of VectQuot(V,W),
v1,v2 be VECTOR of V;
assume
A1: A1 = v1 + W & A2 = v2 + W;
reconsider x1 = v1, x2 = v2 as Vector of X;
reconsider B1 = A1, B2 = A2 as Vector of VectQuot(X,Y);
A2: B1 = x1 + Y & B2 = x2 + Y by A1,LMQ03;
thus A1 + A2 = B1 + B2
.= (x1 + x2) + Y by A2,VECTSP10:26
.= (v1 + v2) + W by LMQ03;
end;
theorem
for V be RealLinearSpace, W be Subspace of V holds
for A1,A2 be VECTOR of VectQuot(V,W),
v1,v2 be VECTOR of V
st A1 = v1 + W & A2 = v2 + W
holds A1 - A2 = (v1 - v2) + W
proof
let V be RealLinearSpace, W be Subspace of V;
let A1,A2 be VECTOR of VectQuot(V,W),
v1,v2 be VECTOR of V;
assume
A1: A1 = v1 + W & A2 = v2 + W; then
-A2 = -v2 + W by LMQ10;
hence A1 - A2 = (v1 - v2) + W by A1,LMQ11;
end;
theorem LMQ13:
for V be RealLinearSpace, W be Subspace of V
holds 0.VectQuot(V,W) = the carrier of W & 0.VectQuot(V,W) = 0.V + W
proof
let V be RealLinearSpace, W be Subspace of V;
thus 0. VectQuot(V,W) = zeroCoset(V,W) by LMQ08
.= the carrier of W;
hence 0. VectQuot(V,W) = 0.V + W by RLSUB_1:44;
end;
theorem LMQ20:
for V be RealLinearSpace, W be Subspace of V holds
ex QL be LinearOperator of V, VectQuot(V,W)
st QL is onto & for v be VECTOR of V holds QL.v = v + W
proof
let V be RealLinearSpace, W be Subspace of V;
defpred P[VECTOR of V,object] means $2 = $1 + W;
A1: for x being Element of the carrier of V
ex y being Element of the carrier of VectQuot(V,W) st P[x,y]
proof
let x be Element of the carrier of V;
reconsider v = x + W as Point of VectQuot(V,W) by LMQ07;
take v;
thus thesis;
end;
consider QL being Function of the carrier of V, VectQuot(V,W) such that
A2: for x being Element of V holds P[x, QL.x] from FUNCT_2:sch 3(A1);
A3: for v,w be Element of V holds QL.(v+w) = QL.v + QL.w
proof
let v,w be Element of V;
A4: QL.v = v + W by A2;
A5: QL.w = w + W by A2;
thus QL.(v+w) = (v+w) + W by A2
.= QL.v + QL.w by A4,A5,LMQ11;
end;
for v being VECTOR of V, r being Real holds QL.(r*v) = r * QL.v
proof
let v be VECTOR of V, r be Real;
A6: QL.v = v + W by A2;
thus QL.(r*v) = (r*v) + W by A2
.= r * QL.v by A6,LMQ09;
end; then
QL is additive homogeneous by A3,LOPBAN_1:def 5; then
reconsider QL as LinearOperator of V, VectQuot(V,W);
take QL;
for v being object st v in the carrier of VectQuot(V,W)
ex s being object st s in the carrier of V & v = QL.s
proof
let v be object;
assume v in the carrier of VectQuot(V,W); then
reconsider v1 = v as Point of VectQuot(V,W);
consider s be VECTOR of V such that
A7: v1 = s + W by LMQ07;
take s;
thus s in the carrier of V;
thus v = QL.s by A2,A7;
end;
hence thesis by A2,FUNCT_2:10;
end;
definition
let V be RealLinearSpace, W be Subspace of V;
func InducedSur(V,W) -> LinearOperator of V, VectQuot(V,W) means
:defDQuot:
it is onto & for v being VECTOR of V holds it.v = v + W;
existence by LMQ20;
uniqueness
proof
let QL1,QL2 be LinearOperator of V, VectQuot(V,W);
assume
A1: QL1 is onto & for v be VECTOR of V holds QL1.v = v + W;
assume
A2: QL2 is onto & for v be VECTOR of V holds QL2.v = v + W;
now
let v be VECTOR of V;
thus QL1.v = v + W by A1
.= QL2.v by A2;
end;
hence QL1 = QL2;
end;
end;
theorem LMQ21:
for V,W be RealLinearSpace, L be LinearOperator of V,W holds
ex QL be LinearOperator of VectQuot(V,Ker L), Im L
st QL is isomorphism
& for z be Point of VectQuot(V,Ker L), v be VECTOR of V
st z = v + Ker L holds QL.z = L.v
proof
let V,W be RealLinearSpace, L be LinearOperator of V,W;
A1: the carrier of Im(L) = rng L by IMX2,LCL1;
A2: the carrier of Ker(L) = L"{0.W} by KLXY1,LCL1;
defpred P[object,object] means
ex v be VECTOR of V st $1 = v + Ker L & $2 = L.v;
A3: for x being Element of the carrier of VectQuot(V,Ker L)
ex y being Element of the carrier of (Im L) st P[x,y]
proof
let x be Element of the carrier of VectQuot(V,Ker L);
consider v be Point of V such that
A4: x = v + Ker L by LMQ07;
reconsider y = L.v as Element of the carrier of Im L by A1,FUNCT_2:4;
take y;
thus thesis by A4;
end;
consider QL being Function of the carrier of VectQuot(V,Ker L), the
carrier of Im L such that
A5: for x being Element of VectQuot(V,Ker L) holds P[x,QL.x]
from FUNCT_2:sch 3(A3);
A6: for z be Point of VectQuot(V,Ker L), v be VECTOR of V st z = v + Ker L
holds QL.z = L.v
proof
let z be Point of VectQuot(V,Ker L), v be VECTOR of V;
assume
A7: z = v + Ker L;
consider w be VECTOR of V such that
A8: z = w + Ker L & QL.z = L.w by A5;
consider v1 be Point of V such that
A9: v1 in Ker L & w = v + v1 by A7,A8,RLSUB_1:54,63;
w - v = v1 + (v -v) by A9,RLVECT_1:28
.= v1 + 0.V by RLVECT_1:15
.= v1 by RLVECT_1:4; then
A10: w - v in the carrier of V & L.(w-v) in {0.W} by A2,A9,FUNCT_2:38;
L.(w-v) = L.(w+(-1)*v) by RLVECT_1:16
.= L.w + L.((-1)*v) by VECTSP_1:def 20
.= L.w + (-1)* L.v by LOPBAN_1:def 5
.= L.w + - L.v by RLVECT_1:16; then
L.w - L.v = 0.W by A10,TARSKI:def 1; then
L.v = L.w - L.v + L.v by RLVECT_1:4
.= L.w - (L.v - L.v) by RLVECT_1:29
.= L.w - 0.W by RLVECT_1:15
.= L.w by RLVECT_1:13;
hence QL.z = L.v by A8;
end;
A11: for x1,x2 being object
st x1 in the carrier of VectQuot(V,Ker L)
& x2 in the carrier of VectQuot(V,Ker L)
& QL.x1 = QL.x2
holds x1 = x2
proof
let x1,x2 be object;
assume
A12: x1 in the carrier of VectQuot(V,Ker L)
& x2 in the carrier of VectQuot(V,Ker L)
& QL.x1 = QL.x2;
reconsider z1 = x1, z2 = x2 as Point of VectQuot(V,Ker L) by A12;
consider v1 be VECTOR of V such that
A13: z1 = v1 + Ker L & QL.x1 = L.v1 by A5;
consider v2 be VECTOR of V such that
A14: z2 = v2 + Ker L & QL.x2 = L.v2 by A5;
L.v1 - L.v2 = L.v1 + (-1) * L.v2 by RLVECT_1:16
.= L.v1 + L.((-1) * v2) by LOPBAN_1:def 5
.= L.(v1 + (-1) * v2) by VECTSP_1:def 20
.= L.(v1 - v2) by RLVECT_1:16; then
L.(v1-v2) = 0.W by A12,A13,A14,RLVECT_1:15; then
L.(v1-v2) in {0.W} by TARSKI:def 1; then
A15: v1-v2 in Ker(L) by A2,FUNCT_2:38;
(v1-v2) + v2 = v1 - (v2-v2) by RLVECT_1:29
.= v1 - 0.V by RLVECT_1:15
.= v1 by RLVECT_1:13; then
v1 in v2 + Ker(L) by A15;
hence thesis by A13,A14,RLSUB_1:54;
end;
for v being object st v in the carrier of Im(L)
ex s being object st s in the carrier of VectQuot(V,Ker L) & v = QL.s
proof
let v be object;
assume v in the carrier of Im(L); then
v in rng L by IMX2,LCL1; then
consider x be object such that
A16: x in the carrier of V & L.x = v by FUNCT_2:11;
reconsider x as Point of V by A16;
reconsider s = x + Ker L as Point of VectQuot(V,Ker L) by LMQ07;
take s;
thus s in the carrier of VectQuot(V,Ker L) & v = QL.s by A6,A16;
end; then
A17: QL is onto by FUNCT_2:10;
A18: for v,w be Element of VectQuot(V,Ker L) holds QL.(v+w) = QL.v + QL.w
proof
let v,w be Element of VectQuot(V,Ker L);
consider x be Point of V such that
A19: v = x + Ker L by LMQ07;
consider y be Point of V such that
A20: w = y + Ker L by LMQ07;
A21: v + w = (x + y) + Ker L by A19,A20,LMQ11;
A22: QL.v = L.x by A6,A19;
A23: QL.w = L.y by A6,A20;
thus QL.(v + w) = L.(x + y) by A6,A21
.= L.x + L.y by VECTSP_1:def 20
.= QL.v + QL.w by A22,A23,RLSUB_1:13;
end;
for v being VECTOR of VectQuot(V,Ker L), r being Real
holds QL.(r*v) = r * QL.v
proof
let v be VECTOR of VectQuot(V,Ker L), r being Real;
consider x be Point of V such that
A24: v = x + Ker L by LMQ07;
r*v = (r*x) + Ker L by A24,LMQ09;
hence QL.(r*v) = L.(r*x) by A6
.= r * L.x by LOPBAN_1:def 5
.= r * QL.v by A6,A24,RLSUB_1:14;
end; then
QL is additive homogeneous by A18,LOPBAN_1:def 5; then
reconsider QL as LinearOperator of VectQuot(V,Ker L), Im L;
take QL;
thus QL is isomorphism by A11,A17,FUNCT_2:19;
thus thesis by A6;
end;
definition
let V,W be RealLinearSpace, L be LinearOperator of V,W;
func InducedBi (V,W,L) -> LinearOperator of VectQuot(V,Ker L),Im L means
:defQuotR:
it is isomorphism
& for z be Point of VectQuot(V,Ker L), v be VECTOR of V
st z = v + Ker L holds it.z = L.v;
existence by LMQ21;
uniqueness
proof
let QL1,QL2 be LinearOperator of VectQuot(V,Ker L), Im L;
assume
A1: QL1 is isomorphism
& for z be Point of VectQuot(V,Ker L), v be VECTOR of V
st z = v + Ker L holds QL1.z = L.v;
assume
A2: QL2 is isomorphism
& for z be Point of VectQuot(V,Ker L), v be VECTOR of V
st z = v + Ker L holds QL2.z = L.v;
now
let z be VECTOR of VectQuot(V,Ker L);
consider v be Point of V such that
A3: z= v + Ker L by LMQ07;
thus QL1.z = L.v by A1,A3
.= QL2.z by A2,A3;
end;
hence QL1 = QL2;
end;
end;
theorem
for V,W be RealLinearSpace, L be LinearOperator of V,W
holds L = InducedBi(V,W,L) * InducedSur(V,Ker L)
proof
let V,W be RealLinearSpace, L be LinearOperator of V,W;
now
let v be VECTOR of V;
A1: dom InducedSur(V,Ker L) = the carrier of V by FUNCT_2:def 1;
reconsider z = v + Ker L as Point of VectQuot(V,Ker L) by LMQ07;
thus (InducedBi(V,W,L) * InducedSur(V,Ker L)).v
= (InducedBi(V,W,L)).((InducedSur(V,Ker L)).v) by A1,FUNCT_1:13
.= (InducedBi(V,W,L)).z by defDQuot
.= L.v by defQuotR;
end;
hence thesis;
end;
definition
let V be RealNormSpace, W be Subspace of V, v be VECTOR of V;
func NormVSets(V,W,v) -> non empty Subset of REAL equals
{||.x.|| where x is VECTOR of V : x in v + W};
correctness
proof
now let r be object;
assume r in {||.x.|| where x is VECTOR of V : x in v + W}; then
consider x be VECTOR of V such that
A1: r = ||.x.|| & x in v + W;
thus r in REAL by A1;
end; then
A2: {||.x.|| where x is VECTOR of V : x in v + W} c= REAL;
v in v + W by RLSUB_1:43; then
||.v.|| in {||.x.|| where x is VECTOR of V : x in v + W};
hence thesis by A2;
end;
end;
LMQ231:
for V be RealNormSpace, W be Subspace of V, v be VECTOR of V
holds NormVSets(V,W,v) is bounded_below
proof
let V be RealNormSpace, W be Subspace of V, v be VECTOR of V;
for r being ExtReal st r in NormVSets(V,W,v) holds 0 <= r
proof
let r be ExtReal;
assume r in NormVSets(V,W,v); then
consider x be VECTOR of V such that
A1: r = ||.x.|| & x in v + W;
thus thesis by A1;
end; then
0 is LowerBound of NormVSets(V,W,v) by XXREAL_2:def 2;
hence NormVSets(V,W,v) is bounded_below by XXREAL_2:def 9;
end;
registration
let V be RealNormSpace, W be Subspace of V, v be VECTOR of V;
cluster NormVSets(V,W,v) -> non empty bounded_below;
correctness by LMQ231;
end;
theorem LMQ23:
for V be RealNormSpace, W be Subspace of V, v be VECTOR of V holds
0 <= lower_bound NormVSets(V,W,v) & lower_bound NormVSets(V,W,v) <= ||.v.||
proof
let V be RealNormSpace, W be Subspace of V, v be VECTOR of V;
for r being ExtReal st r in NormVSets(V,W,v) holds 0 <= r
proof
let r be ExtReal;
assume r in NormVSets(V,W,v); then
consider x be VECTOR of V such that
A1: r = ||.x.|| & x in v + W;
thus thesis by A1;
end; then
0 is LowerBound of NormVSets(V,W,v) by XXREAL_2:def 2;
hence 0 <= lower_bound NormVSets(V,W,v) by XXREAL_2:def 4;
v in v + W by RLSUB_1:43; then
A2: ||.v.|| in NormVSets(V,W,v);
inf NormVSets(V,W,v) is LowerBound of NormVSets(V,W,v) by XXREAL_2:def 4;
hence thesis by A2,XXREAL_2:def 2;
end;
definition
let V be RealNormSpace, W be Subspace of V;
func NormCoset(V,W) -> Function of CosetSet(V,W), REAL means
:DeNorm:
for A be Element of CosetSet(V,W) for v be VECTOR of V st A = v + W holds
it.A = lower_bound NormVSets(V,W,v);
existence
proof
defpred P[set, set] means for v be VECTOR of V st $1 = v + W
holds $2 = lower_bound NormVSets(V,W,v);
set C = CosetSet(V,W);
A1: now
let A be Element of C;
A in C; then
consider A1 be Coset of W such that
A2: A1 = A;
consider v0 be VECTOR of V such that
A3: A1 = v0 + W by RLSUB_1:def 6;
reconsider r = lower_bound NormVSets(V,W,v0) as Element of REAL
by XREAL_0:def 1;
take r;
thus P[A, r] by A2,A3;
end;
consider f be Function of C,REAL such that
A4: for A be Element of C holds P[A, f.A] from FUNCT_2:sch 3(A1);
take f;
let A be Element of C, v be VECTOR of V;
assume A = v + W;
hence thesis by A4;
end;
uniqueness
proof
set C = CosetSet(V,W);
let f1,f2 be Function of C, REAL such that
A5: for A be Element of CosetSet(V,W) for a be VECTOR of V st A = a + W
holds f1.A = lower_bound NormVSets(V,W,a) and
A6: for A be Element of CosetSet(V,W) for a be VECTOR of V st A = a + W
holds f2.A = lower_bound NormVSets(V,W,a);
set C = CosetSet(V,W);
now
let A be Element of CosetSet(V,W);
A in C; then
consider A1 be Coset of W such that
A7: A1 = A;
consider a be VECTOR of V such that
A8: A1 = a + W by RLSUB_1:def 6;
thus f1.A = lower_bound NormVSets(V,W,a) by A5,A7,A8
.= f2.A by A6,A7,A8;
end;
hence thesis;
end;
end;
definition
let X be RealNormSpace, Y be Subspace of X;
assume
A1: ex CY be Subset of X st CY = the carrier of Y & CY is closed;
func NVectQuot (X,Y) -> strict RealNormSpace means
:defQuotN:
the RLSStruct of it = VectQuot (X,Y) & the normF of it = NormCoset(X,Y);
existence
proof
consider CY be Subset of X such that
A2: CY = the carrier of Y & CY is closed by A1;
set S = VectQuot(X,Y);
A3: the carrier of S = CosetSet(X,Y) by LMQ06; then
reconsider NF = NormCoset(X,Y) as Function of the carrier of S,REAL;
reconsider T = NORMSTR(# the carrier of S,
0.S,
the addF of S,
the Mult of S, NF #) as non empty NORMSTR;
now
let v,w be Element of T;
reconsider v1 = v, w1 = w as Element of S;
thus v + w = v1 + w1
.= w1 + v1
.= w + v;
end; then
A4: T is Abelian;
now
let u,v,w be Element of T;
reconsider u1 = u, v1 = v, w1 = w as Element of S;
thus (u + v) + w = (u1 + v1) + w1
.= u1 + (v1 + w1) by RLVECT_1:def 3
.= u + (v + w);
end; then
A5: T is add-associative;
now
let v be Element of T;
reconsider v1 = v as Element of S;
thus v + 0.T = v1 + 0.S
.= v by RLVECT_1:def 4;
end; then
A6: T is right_zeroed;
A7: T is right_complementable
proof
let v be Element of T;
reconsider v1 = v as Element of S;
reconsider w1 = -v1 as Element of S;
reconsider w = w1 as Element of T;
take w;
thus v + w = v1 + w1
.= 0.T by RLVECT_1:5;
end;
now
let a,b be Real, v be Element of T;
reconsider v1 = v as Element of S;
thus (a + b) * v = (a + b) * v1
.= a * v1 + b * v1 by RLVECT_1:def 6
.= a * v + b * v;
end; then
A8: T is scalar-distributive;
now
let a be Real, v,w be Element of T;
reconsider v1 = v, w1 = w as Element of S;
thus a * (v + w) = a * (v1 + w1)
.= a * v1 + a * w1 by RLVECT_1:def 5
.= a * v + a * w;
end; then
A9: T is vector-distributive;
now
let a,b be Real, v be Element of T;
reconsider v1 = v as Element of S;
thus (a * b) * v = (a * b) * v1
.= a * (b * v1) by RLVECT_1:def 7
.= a * (b * v);
end; then
A10: T is scalar-associative;
now
let v be Element of T;
reconsider v1 = v as Element of S;
thus 1 * v = 1 * v1
.= v by RLVECT_1:def 8;
end; then
A11: T is scalar-unital;
A13: ||.0.T.|| = lower_bound NormVSets(X,Y,0.X) by A3,DeNorm,LMQ13; then
A14: ||.0.T.|| <= ||.0.X.|| by LMQ23; then
A15: T is reflexive by A13,LMQ23;
now
let z be Element of T;
assume
A16: ||.z.|| = 0;
reconsider z1 = z as Element of S;
consider v be Point of X such that
A17: z1 = v + Y by LMQ07;
A18: 0 = lower_bound NormVSets(X,Y,v) by A3,A16,A17,DeNorm;
for e be Real st 0 < e holds
ex w be VECTOR of X st w in CY & ||.v-w.|| <= e
proof
let e be Real;
set g = lower_bound NormVSets(X,Y,v);
assume 0 < e; then
consider r be Real such that
A19: r in NormVSets(X,Y,v) & r < g + e by SEQ_4:def 2;
consider x be VECTOR of X such that
A20: r = ||.x.|| & x in v + Y by A19;
consider u be Point of X such that
A21: x = v + u & u in Y by A20;
set w = -u;
take w;
w in Y by A21,RLSUB_1:22;
hence w in CY by A2;
thus ||.v-w.|| <= e by A18,A19,A20,A21,RLVECT_1:17;
end; then
v in Y by A2,CLOSE1; then
v + Y = the carrier of Y by RLSUB_1:48;
hence z = 0.T by A17,LMQ13;
end; then
A22: T is discerning;
now
let a be Real, v,w be Element of T;
reconsider v1 = v, w1 = w as Element of S;
thus ||.a*v.|| = |.a.| * ||.v.||
proof
per cases;
suppose
A23: a = 0; then
0.T = a * v1 by RLVECT_1:10
.= a * v;
hence thesis by A13,A14,A23,COMPLEX1:44,LMQ23;
end;
suppose
A24: not a = 0; then
A25: 0 < |.a.| by COMPLEX1:47;
consider vv1 be Point of X such that
A26: v1 = vv1 + Y by LMQ07;
A27: ||.v.|| = lower_bound NormVSets(X,Y,vv1) by A3,A26,DeNorm;
a * v = a * v1
.= (a * vv1) + Y by A26,LMQ09; then
A29: ||.a*v.|| = lower_bound NormVSets(X,Y,a*vv1)
by A3,DeNorm;
for r being ExtReal st r in NormVSets(X,Y,a*vv1)
holds |.a.| * ||.v.|| <= r
proof
let r be ExtReal;
assume r in NormVSets(X,Y,a*vv1); then
consider x be VECTOR of X such that
A30: r = ||.x.|| & x in a*vv1 + Y;
consider y be VECTOR of X such that
A31: x= a*vv1 + y & y in Y by A30;
A32: a*vv1+y = a*vv1 + 1*y by RLVECT_1:def 8
.= a*vv1 + (a*(1/a))*y by A24,XCMPLX_1:106
.= a*vv1 + a*((1/a)*y) by RLVECT_1:def 7
.= a*(vv1 + (1/a)*y) by RLVECT_1:def 5;
A33: (1/a)*y in Y by A31,RLSUB_1:21;
A34: ||.a*vv1 + y.|| = |.a.| * ||.(vv1 + (1/a)*y).||
by A32,NORMSP_1:def 1;
vv1 + (1/a)*y in vv1+Y by A33; then
||.(vv1 + (1/a)*y).|| in NormVSets(X,Y,vv1); then
||.v.|| <= ||.(vv1 + (1/a)*y).|| by A27,SEQ_4:def 2;
hence thesis by A25,A30,A31,A34,XREAL_1:64;
end; then
|.a.| * ||.v.|| is LowerBound of NormVSets(X,Y,a*vv1)
by XXREAL_2:def 2; then
A36: |.a.| * ||.v.|| <= ||.a*v.|| by A29,XXREAL_2:def 4;
for r being ExtReal st r in NormVSets(X,Y,vv1)
holds (1/|.a.|) * ||.a*v.|| <= r
proof
let r be ExtReal;
assume r in NormVSets(X,Y,vv1); then
consider x be VECTOR of X such that
A37: r = ||.x.|| & x in vv1 + Y;
consider y be VECTOR of X such that
A38: x = vv1 + y & y in Y by A37;
A39: vv1 + y = 1*(vv1 + y) by RLVECT_1:def 8
.= ((1/a)*a)*(vv1 + y) by A24,XCMPLX_1:106
.= (1/a)*(a*(vv1 + y)) by RLVECT_1:def 7
.= (1/a)*(a*vv1 + a*y) by RLVECT_1:def 5;
A40: a*y in Y by A38,RLSUB_1:21;
A41: ||.vv1 + y.|| = |.1/a.| * ||.a*vv1 + a*y.||
by A39,NORMSP_1:def 1;
a*vv1 + a*y in a*vv1 + Y by A40; then
||.a*vv1 + a*y.|| in NormVSets(X,Y,a*vv1); then
A42: ||.a*v.|| <= ||.a*vv1 + a*y.|| by A29,SEQ_4:def 2;
0 <= |.1/a.| by COMPLEX1:46; then
|.1/a.| * ||.a*v.|| <= |.1/a.| * ||.a*vv1 + a*y.||
by A42,XREAL_1:64;
hence thesis by A37,A38,A41,COMPLEX1:80;
end; then
A43: (1/|.a.|) * ||.a*v.|| is LowerBound of NormVSets(X,Y,vv1)
by XXREAL_2:def 2;
0 <= |.a.| by COMPLEX1:46; then
|.a.| * ((1/|.a.|) * ||.a*v.||) <= |.a.| * ||.v.||
by A27,A43,XREAL_1:64,XXREAL_2:def 4; then
|.a.| * (1/|.a.|) * ||.a*v.|| <= |.a.| * ||.v.||; then
1 * ||.a*v.|| <= |.a.| * ||.v.|| by A25,XCMPLX_1:106;
hence ||.a*v.|| = |.a.| * ||.v.|| by A36,XXREAL_0:1;
end;
end;
thus ||.v+w.|| <= ||.v.|| + ||.w.||
proof
consider vv1 be Point of X such that
A44: v1 = vv1 + Y by LMQ07;
A45: ||.v.|| = lower_bound NormVSets(X,Y,vv1) by A3,A44,DeNorm;
consider ww1 be Point of X such that
A46: w1= ww1 + Y by LMQ07;
A47: ||.w.|| = lower_bound NormVSets(X,Y,ww1) by A3,A46,DeNorm;
v + w = v1 + w1
.= (vv1 + ww1) + Y by A44,A46,LMQ11; then
A49: ||.v+w.|| = lower_bound NormVSets(X,Y,vv1+ww1)
by A3,DeNorm;
A50: for y1,y2 be Point of X st y1 in Y & y2 in Y
holds ||.v+w.|| <= ||.vv1+y1.|| + ||.ww1+y2.||
proof
let y1,y2 be Point of X;
assume y1 in Y & y2 in Y; then
y1 + y2 in Y by RLSUB_1:20; then
(vv1+ww1) + (y1+y2) in (vv1+ww1) + Y; then
||.(vv1+ww1) + (y1+y2).|| in NormVSets(X,Y,vv1+ww1); then
A51: lower_bound NormVSets(X,Y,vv1+ww1) <= ||.(vv1+ww1) + (y1+y2).||
by SEQ_4:def 2;
||.(vv1+ww1) + (y1+y2).||
= ||.(vv1+ww1+y1) + y2.|| by RLVECT_1:def 3
.= ||.(vv1+y1+ww1) + y2.|| by RLVECT_1:def 3
.= ||.(vv1+y1) + (ww1+y2).|| by RLVECT_1:def 3; then
||.(vv1+ww1) + (y1+y2).|| <= ||.vv1+y1.|| + ||.ww1+y2.||
by NORMSP_1:def 1;
hence thesis by A49,A51,XXREAL_0:2;
end;
A52: for y1 be Point of X st y1 in Y
holds ||.v+w.|| - ||.w.|| <= ||.vv1+y1.||
proof
let y1 be Point of X;
assume
A53: y1 in Y;
A54: now
let y2 be Point of X;
assume y2 in Y; then
||.v+w.|| - ||.vv1+y1.||
<= ||.vv1+y1.|| + ||.ww1+y2.|| - ||.vv1+y1.||
by A50,A53,XREAL_1:9;
hence ||.v+w.|| - ||.vv1+y1.|| <= ||.ww1+y2.||;
end;
for r being ExtReal st r in NormVSets(X,Y,ww1)
holds ||.v+w.|| - ||.vv1+y1.|| <= r
proof
let r be ExtReal;
assume r in NormVSets(X,Y,ww1); then
consider x be VECTOR of X such that
A55: r = ||.x.|| & x in ww1 + Y;
consider y2 be VECTOR of X such that
A56: x = ww1 + y2 & y2 in Y by A55;
thus ||.v+w.|| - ||.vv1+y1.|| <= r by A54,A55,A56;
end; then
||.v+w.|| - ||.vv1+y1.|| is LowerBound of NormVSets(X,Y,ww1)
by XXREAL_2:def 2; then
||.v+w.|| - ||.vv1+y1.|| + ||.vv1+y1.|| <= ||.w.|| + ||.vv1+y1.||
by A47,XREAL_1:6,XXREAL_2:def 4; then
||.v+w.|| - ||.w.|| <= ||.w.|| + ||.vv1+y1.|| - ||.w.|| by XREAL_1:9;
hence ||.v+w.|| - ||.w.|| <= ||.vv1+y1.||;
end;
for r being ExtReal st r in NormVSets(X,Y,vv1)
holds ||.v+w.|| - ||.w.|| <= r
proof
let r be ExtReal;
assume r in NormVSets(X,Y,vv1); then
consider x be VECTOR of X such that
A58: r = ||.x.|| & x in vv1 + Y;
consider y1 be VECTOR of X such that
A59: x = vv1 + y1 & y1 in Y by A58;
thus thesis by A52,A58,A59;
end; then
||.v+w.|| - ||.w.|| is LowerBound of NormVSets(X,Y,vv1)
by XXREAL_2:def 2; then
||.v+w.|| - ||.w.|| + ||.w.|| <= ||.v.|| + ||.w.||
by A45,XREAL_1:6,XXREAL_2:def 4;
hence thesis;
end;
end; then
T is RealNormSpace-like; then
reconsider T as strict RealNormSpace by A4,A5,A6,A7,A8,A9,A10,A11,A15,A22;
take T;
thus thesis;
end;
uniqueness;
end;
theorem
for V,W be RealNormSpace,
L be Lipschitzian LinearOperator of V,W
holds
ex QL be Lipschitzian LinearOperator of NVectQuot(V,Ker L), Im L,
PQL be Point of R_NormSpace_of_BoundedLinearOperators(NVectQuot(V,Ker L),
Im L),
PL be Point of R_NormSpace_of_BoundedLinearOperators(V,W)
st QL is onto & QL is one-to-one
& L = PL & QL = PQL & ||.PL.|| = ||.PQL.||
& for z be Point of NVectQuot(V,Ker L), v be VECTOR of V
st z = v + Ker L holds QL.z = L.v
proof
let V,W be RealNormSpace,
L be Lipschitzian LinearOperator of V,W;
A1: the carrier of Ker L = L"{0.W} & L"{0.W} is closed
by KERCL01,KLXY1,LCL1,LOPBAN_7:6;
reconsider V1 = V as RealLinearSpace;
reconsider W1 = W as RealLinearSpace;
reconsider L1 = L as LinearOperator of V1,W1;
A2: the RLSStruct of NVectQuot(V,Ker L) = VectQuot (V,Ker L)
& the normF of NVectQuot(V,Ker L) = NormCoset(V,Ker L) by A1,defQuotN;
A3: the carrier of VectQuot(V,Ker L) = CosetSet(V,Ker L) by LMQ06;
consider QL1 be LinearOperator of VectQuot(V1,Ker L1), Im L1 such that
A4: QL1 is isomorphism
& for z be Point of VectQuot(V1,Ker L1), v be VECTOR of V1
st z = v + Ker L1 holds QL1.z = L1.v by LMQ21;
reconsider KL1 = Ker L1 as Subspace of V;
A5: the RLSStruct of NVectQuot(V,Ker L) = VectQuot (V,KL1) by A1,defQuotN;
reconsider QL = QL1 as Function of NVectQuot(V,Ker L),Im L by A5;
A6: for v,w be Element of NVectQuot(V,Ker L) holds QL.(v+w) = QL.v + QL.w
proof
let v,w be Element of NVectQuot(V,Ker L);
reconsider v1 = v, w1 = w as Element of VectQuot(V1,Ker L1) by A5;
thus QL.(v+w) = QL1.(v1+w1) by A5
.= QL1.v1 + QL1.w1 by VECTSP_1:def 20
.= QL.v + QL.w;
end;
for v being VECTOR of NVectQuot(V,Ker L), r being Real
holds QL.(r * v) = r * QL.v
proof
let v be VECTOR of NVectQuot(V,Ker L), r be Real;
reconsider v1 = v as Element of VectQuot(V1,Ker L1) by A5;
thus QL.(r*v) = QL1.(r*v1) by A5
.= r * QL1.v1 by LOPBAN_1:def 5
.= r * QL.v;
end; then
QL is additive homogeneous by A6,LOPBAN_1:def 5; then
reconsider QL as LinearOperator of NVectQuot(V,Ker L), Im L;
A7: R_NormSpace_of_BoundedLinearOperators(V,W)
= NORMSTR (# BoundedLinearOperators(V,W),
Zero_(BoundedLinearOperators(V,W),
R_VectorSpace_of_LinearOperators(V,W)),
Add_(BoundedLinearOperators(V,W),
R_VectorSpace_of_LinearOperators(V,W)),
Mult_(BoundedLinearOperators(V,W),
R_VectorSpace_of_LinearOperators(V,W)),
BoundedLinearOperatorsNorm(V,W) #) by LOPBAN_1:def 14;
reconsider PL = L as Point of R_NormSpace_of_BoundedLinearOperators(V,W)
by A7,LOPBAN_1:def 9;
A8: for v be Point of NVectQuot(V,Ker L)
holds ||.QL.v.|| <= ||.PL.|| * ||.v.||
proof
let v be Point of NVectQuot(V,Ker L);
reconsider v1 = v as Element of VectQuot(V,Ker L) by A5;
consider vv1 be Point of V such that
A9: v1 = vv1 + Ker L by LMQ07;
A10: ||.v.|| = (NormCoset(V,Ker L)).v1 by A1,defQuotN
.= lower_bound NormVSets(V,Ker L,vv1) by A3,A9,DeNorm;
per cases;
suppose
||.PL.|| = 0; then
PL = 0.R_NormSpace_of_BoundedLinearOperators(V,W) by NORMSP_0:def 5;
then
A11: (the carrier of V) --> 0.W = L by LOPBAN_1:31;
QL.v = L.vv1 by A4,A9
.= 0.W by A11,FUNCOP_1:7; then
||.QL.v.|| = ||.0.W.|| by SUBTH0;
hence ||.QL.v.|| <= ||.PL.|| * ||.v.||;
end;
suppose
A12: ||.PL.|| <> 0;
set a = ||.PL.||;
A13: for y be VECTOR of V st y in Ker L
holds (1/a) * ||.QL.v.|| <= ||.vv1+y.||
proof
let y be VECTOR of V;
assume y in Ker L; then
y in L"{0.W} by KLXY1,LCL1; then
A14: y in the carrier of V & L.y in {0.W} by FUNCT_2:38;
A15: QL.v = L.vv1 by A4,A9
.= L.vv1 + 0.W by RLVECT_1:4
.= L.vv1 + L.y by A14,TARSKI:def 1
.= L.(vv1+y) by VECTSP_1:def 20;
(1/a) * ||.L.(vv1+y).|| <= (1/a) * (||.PL.|| * ||.vv1+y.||)
by LOPBAN_1:32,XREAL_1:64; then
(1/a) * ||.L.(vv1+y).|| <= (1/a) * ||.PL.|| * ||.vv1+y.||; then
(1/a) * ||.L.(vv1+y).|| <= 1 * ||.vv1+y.|| by A12,XCMPLX_1:106;
hence thesis by A15,SUBTH0;
end;
for r being ExtReal st r in NormVSets(V,Ker L,vv1)
holds (1/a) * ||.QL.v.|| <= r
proof
let r be ExtReal;
assume r in NormVSets(V,Ker L,vv1); then
consider x be VECTOR of V such that
A16: r = ||.x.|| & x in vv1 + Ker L;
consider y be VECTOR of V such that
A17: x = vv1+y & y in Ker L by A16;
thus thesis by A13,A16,A17;
end; then
A18: (1/a) * ||.QL.v.|| is LowerBound of NormVSets(V,Ker L,vv1)
by XXREAL_2:def 2;
a * ((1/a) * ||.QL.v.||) <= a * ||.v.||
by A10,A18,XREAL_1:64,XXREAL_2:def 4; then
a * (1/a) * ||.QL.v.|| <= a * ||.v.||; then
1 * ||.QL.v.|| <= a * ||.v.|| by A12,XCMPLX_1:106;
hence ||.QL.v.|| <= ||.PL.|| * ||.v.||;
end;
end;
reconsider QL as Lipschitzian LinearOperator of NVectQuot(V,Ker L), Im L
by A8,LOPBAN_1:def 8;
take QL;
A19: R_NormSpace_of_BoundedLinearOperators(NVectQuot(V,Ker L), Im L)
= NORMSTR (# BoundedLinearOperators(NVectQuot(V,Ker L), Im L),
Zero_(BoundedLinearOperators(NVectQuot(V,Ker L), Im L),
R_VectorSpace_of_LinearOperators(NVectQuot(V,Ker L), Im L)),
Add_(BoundedLinearOperators(NVectQuot(V,Ker L), Im L),
R_VectorSpace_of_LinearOperators(NVectQuot(V,Ker L), Im L)),
Mult_(BoundedLinearOperators(NVectQuot(V,Ker L), Im L),
R_VectorSpace_of_LinearOperators(NVectQuot(V,Ker L), Im L)),
BoundedLinearOperatorsNorm(NVectQuot(V,Ker L), Im L) #)
by LOPBAN_1:def 14; then
reconsider PQL = QL as Point of
R_NormSpace_of_BoundedLinearOperators(NVectQuot(V,Ker L), Im L)
by LOPBAN_1:def 9;
A20: PreNorms(QL)
= {||.QL.t.|| where t is VECTOR of NVectQuot(V,Ker L) : ||.t.|| <= 1}
by LOPBAN_1:def 12;
now
let r be Real;
assume r in PreNorms QL; then
consider v be VECTOR of NVectQuot(V,Ker L) such that
A21: r = ||.QL.v.|| and
A22: ||.v.|| <= 1 by A20;
A23: ||.QL.v.|| <= ||.PL.|| * ||.v.|| by A8;
||.PL.|| * ||.v.|| <= ||.PL.|| * 1 by A22,XREAL_1:64;
hence r <= ||.PL.|| by A21,A23,XXREAL_0:2;
end; then
upper_bound PreNorms QL <= ||.PL.|| by SEQ_4:45; then
A24: ||.PQL.|| <= ||.PL.|| by A19,LOPBAN_1:30;
R_NormSpace_of_BoundedLinearOperators(V,W)
= NORMSTR(# BoundedLinearOperators(V,W),
Zero_(BoundedLinearOperators(V,W),
R_VectorSpace_of_LinearOperators(V,W)),
Add_(BoundedLinearOperators(V,W),
R_VectorSpace_of_LinearOperators(V,W)),
Mult_(BoundedLinearOperators(V,W),
R_VectorSpace_of_LinearOperators(V,W)),
BoundedLinearOperatorsNorm(V,W) #) by LOPBAN_1:def 14; then
A26: ||.PL.|| = upper_bound PreNorms(L) by LOPBAN_1:30;
A27: PreNorms L is non empty bounded_above by LOPBAN_1:27;
A28: PreNorms(L) = {||.L.t.|| where t is VECTOR of V : ||.t.|| <= 1}
by LOPBAN_1:def 12;
now
let s be Real;
assume 0 < s; then
consider p be Real such that
A29: p in PreNorms(L) & ||.PL.||- s < p by A26,A27,SEQ_4:def 1;
consider vv1 be VECTOR of V such that
A30: p = ||.L.vv1.|| and
A31: ||.vv1.|| <= 1 by A28,A29;
A32: lower_bound NormVSets(V,Ker L,vv1) <= ||.vv1.|| by LMQ23;
reconsider v = vv1 + (Ker L) as Point of NVectQuot(V,Ker L) by A2,LMQ07;
||.v.|| = lower_bound NormVSets(V,Ker L,vv1) by A2,DeNorm; then
A33: ||.v.|| <= 1 by A31,A32,XXREAL_0:2;
QL.v = L.vv1 by A4,A5; then
A34: ||.QL.v.|| = ||.L.vv1.|| by SUBTH0;
A35: ||.QL.v.|| <= ||.PQL.|| * ||.v.|| by LOPBAN_1:32;
||.PQL.|| * ||.v.|| <= ||.PQL.|| * 1 by A33,XREAL_1:64; then
||.QL.v.|| <= ||.PQL.|| by A35,XXREAL_0:2; then
||.PL.|| - s <= ||.PQL.|| by A29,A30,A34,XXREAL_0:2; then
||.PL.||- s + s <= ||.PQL.|| + s by XREAL_1:6;
hence ||.PL.|| <= ||.PQL.|| + 1 * s;
end; then
||.PL.|| <= ||.PQL.|| by LMINEQ;
hence thesis by A4,A5,A24,XXREAL_0:1;
end;
LMCL1:
for X be RealNormSpace, Y,Z be Subset of X st Z = the carrier of Lin(Y)
holds Cl(Z) is non empty
proof
let X be RealNormSpace, Y,Z be Subset of X;
assume
A1: Z = the carrier of Lin(Y);
Z c= Cl Z by PRETOPC18;
hence Cl Z is non empty by A1;
end;
begin :: Closure
definition
let X be RealNormSpace, Y be Subset of X;
func ClNLin(Y) -> non empty NORMSTR means
:defClN:
ex Z be Subset of X
st Z = the carrier of Lin(Y)
& it = NORMSTR(# Cl(Z),
Zero_(Cl(Z), X),
Add_(Cl(Z), X),
Mult_(Cl(Z), X),
Norm_(Cl(Z),X) #);
correctness
proof
reconsider Z = the carrier of Lin(Y) as Subset of X by RLSUB_1:def 2;
reconsider T = NORMSTR(# Cl(Z),
Zero_(Cl(Z), X),
Add_(Cl(Z), X),
Mult_(Cl(Z), X),
Norm_(Cl(Z),X) #) as non empty NORMSTR by LMCL1;
ex Z be Subset of X
st Z = the carrier of Lin(Y)
& T = NORMSTR(# Cl(Z),
Zero_(Cl(Z), X),
Add_(Cl(Z), X),
Mult_(Cl(Z), X),
Norm_(Cl(Z),X) #);
hence thesis;
end;
end;
theorem RSSPACE11:
for X be RealNormSpace, V1 be Subset of X, CL be Subset of X
st CL = the carrier of ClNLin(V1)
holds RLSStruct(# CL,Zero_(CL,X), Add_(CL,X),Mult_(CL,X) #) is Subspace of X
proof
let X be RealNormSpace, V1 be Subset of X, CL be Subset of X;
assume
A1: CL = the carrier of ClNLin(V1);
consider Z be Subset of X such that
A2: Z = the carrier of Lin(V1)
& ClNLin(V1) = NORMSTR(# Cl(Z),
Zero_(Cl(Z), X),
Add_(Cl(Z), X),
Mult_(Cl(Z), X),
Norm_(Cl(Z),X) #) by defClN;
thus thesis by A1,RSSPACE:11,A2,Cl01;
end;
SUBTHCL:
for V be RealNormSpace,
V1 be Subset of V,
x,y being Point of V,
x1,y1 being Point of ClNLin(V1),
a be Real st x = x1 & y = y1
holds ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1
proof
let V be RealNormSpace,
V1 be Subset of V,
x,y be Point of V,
x1,y1 be Point of ClNLin(V1),
a be Real;
assume
A1: x = x1 & y = y1;
set l = ClNLin(V1);
consider Z be Subset of V such that
A2: Z = the carrier of Lin(V1)
& l = NORMSTR(# Cl(Z),
Zero_(Cl(Z), V),
Add_(Cl(Z), V),
Mult_(Cl(Z), V),
Norm_(Cl(Z),V) #) by defClN;
reconsider W = the RLSStruct of l as Subspace of V by A2,RSSPACE11;
reconsider x2 = x1, y2 = y1 as Point of W;
thus ||.x1.|| = ((the normF of V) | Cl(Z)).x1 by A2,DefNorm
.= ||.x.|| by A1,A2,FUNCT_1:49;
thus x + y = x2 + y2 by A1,RLSUB_1:13
.= x1 + y1;
thus a * x = a * x2 by A1,RLSUB_1:14
.= a * x1;
end;
theorem CLTh37:
for X be RealNormSpace, Y be Subset of X,
f,g be Point of ClNLin(Y), a be Real holds
(||.f.|| = 0 iff f = 0.ClNLin(Y))
& ||.a*f.|| = |.a.| * ||.f.||
& ||.f+g.|| <= ||.f.|| + ||.g.||
proof
let X be RealNormSpace, Y be Subset of X;
let f,g be Point of ClNLin(Y);
let a be Real;
consider Z be Subset of X such that
A1: Z = the carrier of Lin(Y)
& ClNLin(Y) = NORMSTR(# Cl(Z),
Zero_(Cl(Z), X),
Add_(Cl(Z), X),
Mult_(Cl(Z), X),
Norm_(Cl(Z),X) #) by defClN;
reconsider CL = Cl(Z) as Subset of X;
reconsider f1 = f, g1 = g as Point of X by A1,TARSKI:def 3;
A3: f1+g1 = f+g by SUBTHCL;
A4: a*f1 = a*f by SUBTHCL;
A5: ||.f+g.|| = ||.f1+g1.|| by A3,SUBTHCL;
A6: ||.a*f.|| = ||.a*f1.|| by A4,SUBTHCL;
A7: ||.f.|| = ||.f1.|| by SUBTHCL;
A8: ||.g.|| = ||.g1.|| by SUBTHCL;
0.ClNLin(Y) = 0.X by A1,Cl01,RSSPACE:def 10;
hence thesis by A5,A6,A7,A8,NORMSP_0:def 5,NORMSP_1:def 1;
end;
registration
let X be RealNormSpace, Y be Subset of X;
cluster ClNLin(Y) -> reflexive discerning RealNormSpace-like;
correctness by CLTh37;
end;
theorem CLTh39:
for V be RealNormSpace, V1 be Subset of V
holds ClNLin(V1) is RealNormSpace
proof
let V be RealNormSpace, V1 be Subset of V;
set l = ClNLin(V1);
consider Z be Subset of V such that
A1: Z =the carrier of Lin(V1)
& l = NORMSTR(# Cl(Z),
Zero_(Cl(Z), V),
Add_(Cl(Z), V),
Mult_(Cl(Z), V),
Norm_(Cl(Z),V) #) by defClN;
reconsider W = the RLSStruct of l as Subspace of V by A1,RSSPACE11;
W is RealLinearSpace;
hence thesis by RSSPACE3:2;
end;
registration
let X be RealNormSpace, Y be Subset of X;
cluster ClNLin(Y) -> reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence by CLTh39;
end;
theorem CLTh40:
for V be RealNormSpace, V1 be Subset of V
holds ClNLin(V1) is SubRealNormSpace of V
proof
let V be RealNormSpace, V1 be Subset of V;
set l = ClNLin(V1);
consider Z be Subset of V such that
A1: Z = the carrier of Lin(V1)
& ClNLin(V1) = NORMSTR(# Cl(Z),
Zero_(Cl(Z), V),
Add_(Cl(Z), V),
Mult_(Cl(Z), V),
Norm_(Cl(Z),V) #) by defClN;
reconsider CL = Cl(Z) as Subset of V;
A3: 0.ClNLin(V1) = 0.V by A1,Cl01,RSSPACE:def 10;
A4: the addF of l = (the addF of V) || the carrier of l
by A1,Cl01,RSSPACE:def 8;
A5: the Mult of l = (the Mult of V)| [:REAL, the carrier of l:]
by A1,Cl01,RSSPACE:def 9;
the normF of l = (the normF of V) | (the carrier of l) by A1,DefNorm;
hence thesis by A1,A3,A4,A5,DUALSP01:def 16;
end;
definition
let V be RealNormSpace, V1 be Subset of V;
redefine func ClNLin(V1) -> SubRealNormSpace of V; :: redefines ClNLin (NORMSP_3, definition)
coherence by CLTh40;
end;