:: Real Vector Space and Related Notions
:: by Kazuhisa Nakasho , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received June 30, 2021
:: Copyright (c) 2021 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 ALGSTR_0, ARYTM_1, ARYTM_3, CARD_1, CARD_3, CLASSES1, EUCLID,
FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FUNCT_1, FUNCT_2, MATRIX_1,
MATRIX13, MATRLIN, MATRLIN2, MESFUNC1, NAT_1, NUMBERS, PARTFUN1,
PRE_TOPC, PRVECT_1, RANKNULL, RELAT_1, RLAFFIN1, RLSUB_1, RLVECT_1,
RLVECT_2, RLVECT_3, RLVECT_5, SEMI_AF1, STRUCT_0, SUBSET_1, SUPINF_2,
TARSKI, VALUED_0, VALUED_1, VECTSP_1, XBOOLE_0, XXREAL_0, REAL_NS1,
FUNCSDOM, FUNCOP_1, ZFMISC_1, REAL_1, NORMSP_2, PCOMPS_1, METRIC_1,
RUSUB_4, MATRIX_6, SETFAM_1, BINOP_2, MSSUBFAM, UNIALG_1, COMPLEX1,
NORMSP_1, REALSET1, MATRIXR1, MATRIXR2, LOPBAN_1, DUALSP01;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, REALSET1, FINSET_1, CARD_1,
ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, VALUED_0, BINOP_2,
FINSEQ_1, FINSEQ_2, FINSEQOP, RVSUM_1, MATRIX_0, STRUCT_0, ALGSTR_0,
PRE_TOPC, RLVECT_1, RLSUB_1, VECTSP_1, FUNCSDOM, RLVECT_2, METRIC_1,
RLVECT_3, VECTSP_4, NORMSP_0, NORMSP_1, VECTSP_6, VECTSP_7, MATRIX_1,
FVSUM_1, MATRLIN, PCOMPS_1, RLVECT_5, RUSUB_4, EUCLID, LOPBAN_1,
VECTSP_9, RANKNULL, PRVECT_1, MATRIXR1, RLAFFIN1, MATRIX_6, MATRIXR2,
MATRIX13, MATRLIN2, REAL_NS1, NORMSP_2, MATRTOP1, DUALSP01;
constructors FVSUM_1, MATRIX_6, MATRIX13, MATRLIN2, MATRTOP1, MONOID_0,
RANKNULL, REALSET1, RELSET_1, RLAFFIN1, RLVECT_3, RUSUB_5, VECTSP10,
PCOMPS_1, BINOP_2, REAL_NS1, RLVECT_5, REAL_1, VECTSP_9, NORMSP_2,
MATRIXR2, LOPBAN_1, DUALSP01, FINSOP_1;
registrations CARD_1, EUCLID, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_1, FUNCT_2,
MATRIX13, MATRLIN, MEMBERED, MONOID_0, NAT_1, NUMBERS, PRVECT_1, RELAT_1,
RELSET_1, RLAFFIN1, RLVECT_3, RVSUM_1, STRUCT_0, VALUED_0, VECTSP_1,
XREAL_0, ORDINAL1, REAL_NS1, RLVECT_5, RUSUB_4, XBOOLE_0, RLAFFIN3;
requirements NUMERALS, BOOLE, SUBSET;
begin :: Common properties between norm and topology
:: in finite dimensional linear spaces
reserve X for set,
n,m,k for Nat,
K for Field,
f for n-element real-valued FinSequence,
M for Matrix of n,m,F_Real;
theorem :: REAL_NS2:1
the RLSStruct of TOP-REAL n = the RLSStruct of REAL-NS n;
theorem :: REAL_NS2:2
Euclid n = MetricSpaceNorm REAL-NS n;
theorem :: REAL_NS2:3
the TopStruct of TOP-REAL n = TopSpaceNorm REAL-NS n;
theorem :: REAL_NS2:4
the carrier of TOP-REAL n = the carrier of REAL-NS n;
theorem :: REAL_NS2:5
the carrier of (n -VectSp_over F_Real) = the carrier of REAL-NS n;
theorem :: REAL_NS2:6
0.(TOP-REAL n) = 0.(REAL-NS n);
theorem :: REAL_NS2:7
for p,q be Element of TOP-REAL n,
f,g be Element of REAL-NS n
st p=f & q=g
holds p+q = f+g;
theorem :: REAL_NS2:8
for r be Real,
q be Element of TOP-REAL n,
g be Element of REAL-NS n
st q = g
holds r*q = r*g;
theorem :: REAL_NS2:9
for q be Element of TOP-REAL n,
g be Element of REAL-NS n
st q = g
holds -q = -g;
theorem :: REAL_NS2:10
for p,q be Element of TOP-REAL n,
f,g be Element of REAL-NS n
st p = f & q = g
holds p-q = f-g;
theorem :: REAL_NS2:11
for X be set
for n be Nat
holds
X is Linear_Combination of REAL-NS n
iff
X is Linear_Combination of TOP-REAL n;
theorem :: REAL_NS2:12
for X be set
for n be Nat holds
X is Linear_Combination of REAL-NS n
iff
X is Linear_Combination of n-VectSp_over F_Real;
theorem :: REAL_NS2:13
for Lv be Linear_Combination of TOP-REAL n,
Lr be Linear_Combination of REAL-NS n
st Lr = Lv
holds Carrier Lr = Carrier Lv;
theorem :: REAL_NS2:14
for Lv be Linear_Combination of n-VectSp_over F_Real,
Lr be Linear_Combination of REAL-NS n
st Lr = Lv
holds Carrier Lr = Carrier Lv;
theorem :: REAL_NS2:15
for F be set
holds
F is Subset of TOP-REAL n
iff
F is Subset of REAL-NS n;
theorem :: REAL_NS2:16
for F be set
holds
F is Subset of REAL-NS n
iff
F is Subset of n-VectSp_over F_Real;
theorem :: REAL_NS2:17
for F be set
holds
F is FinSequence of TOP-REAL n
iff
F is FinSequence of REAL-NS n;
theorem :: REAL_NS2:18
for F be set
holds
F is Function of TOP-REAL n, REAL
iff
F is Function of REAL-NS n, REAL;
theorem :: REAL_NS2:19
for Fr be FinSequence of TOP-REAL n,
fr be Function of TOP-REAL n,REAL,
Fv be FinSequence of REAL-NS n,
fv be Function of REAL-NS n,REAL
st fr = fv & Fr = Fv
holds fr(#)Fr = fv(#)Fv;
theorem :: REAL_NS2:20
for F be FinSequence of REAL-NS n,
fr be Function of REAL-NS n,REAL,
Fv be FinSequence of n-VectSp_over F_Real,
fv be Function of n-VectSp_over F_Real,F_Real
st fr = fv & F = Fv
holds fr(#)F = fv(#)Fv;
theorem :: REAL_NS2:21
for Ft be FinSequence of TOP-REAL n,
Fr be FinSequence of REAL-NS n
st Ft = Fr
holds Sum Ft = Sum Fr;
theorem :: REAL_NS2:22
for F be FinSequence of REAL-NS n,
Fv be FinSequence of n-VectSp_over F_Real
st Fv = F
holds Sum F = Sum Fv;
theorem :: REAL_NS2:23
for Lr be Linear_Combination of REAL-NS n,
Lt be Linear_Combination of TOP-REAL n st Lr = Lt
holds Sum Lr = Sum Lt;
theorem :: REAL_NS2:24
for Lv be Linear_Combination of n-VectSp_over F_Real,
Lr be Linear_Combination of REAL-NS n st Lr = Lv
holds Sum Lr = Sum Lv;
theorem :: REAL_NS2:25
for Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n
st Ar = At
holds
for X be object holds
X is Linear_Combination of Ar
iff
X is Linear_Combination of At;
theorem :: REAL_NS2:26
for Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n st Ar = At
holds [#]Lin Ar = [#]Lin At;
theorem :: REAL_NS2:27
for Af be Subset of n-VectSp_over F_Real,
Ar be Subset of REAL-NS n st Af = Ar
holds [#]Lin Ar = [#]Lin Af;
theorem :: REAL_NS2:28
for Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n
st Ar = At
holds
Ar is linearly-independent
iff
At is linearly-independent;
theorem :: REAL_NS2:29
for Af be Subset of n-VectSp_over F_Real,
Ar be Subset of REAL-NS n
st Af = Ar
holds
Af is linearly-independent
iff
Ar is linearly-independent;
theorem :: REAL_NS2:30
for X be object holds
X is Subspace of REAL-NS n
iff
X is Subspace of TOP-REAL n;
theorem :: REAL_NS2:31
for X be set,
U be Subspace of REAL-NS n,
W be Subspace of n -VectSp_over F_Real
st [#] U = [#] W
holds
X is Linear_Combination of U
iff
X is Linear_Combination of W;
theorem :: REAL_NS2:32
for F be one-to-one FinSequence of REAL-NS n
st rng F is linearly-independent
holds
ex M be Matrix of n,F_Real
st M is invertible & M | len F = F;
theorem :: REAL_NS2:33
for M be Matrix of n,F_Real
for N be Matrix of n,REAL
st N = MXF2MXR M
holds
M is invertible iff N is invertible;
theorem :: REAL_NS2:34
for M be Matrix of n,REAL
holds
M is invertible iff MXR2MXF M is invertible;
theorem :: REAL_NS2:35
for F be one-to-one FinSequence of REAL-NS n
st rng F is linearly-independent
holds
ex M be Matrix of n,REAL
st M is invertible & M | len F = F;
theorem :: REAL_NS2:36
for F be one-to-one FinSequence of REAL-NS n
st rng F is linearly-independent
holds
for B be OrdBasis of n -VectSp_over F_Real
st B = MX2FinS(1. (F_Real,n))
holds
for M be Matrix of n,F_Real
st M is invertible & M | len F = F
holds
(Mx2Tran M) .: ([#] (Lin (rng (B | len F))))
= [#] (Lin rng F);
theorem :: REAL_NS2:37
for A,B be linearly-independent Subset of REAL-NS n
st card A = card B
holds
ex M be Matrix of n,F_Real
st M is invertible
& (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B);
theorem :: REAL_NS2:38
for n, m be Nat
for M be Matrix of n,m,F_Real
for A be linearly-independent Subset of REAL-NS n
st the_rank_of M = n
holds
(Mx2Tran M) .: A is linearly-independent;
theorem :: REAL_NS2:39
for p be Element of TOP-REAL n,
f be Element of REAL-NS n,
H be Subset of TOP-REAL n,
I be Subset of REAL-NS n
st p = f & H = I
holds p + H = f + I;
theorem :: REAL_NS2:40
for Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n
st Ar = At
holds
Ar is Affine
iff
At is Affine;
theorem :: REAL_NS2:41
for X be set
holds
X is affinely-independent Subset of REAL-NS n
iff
X is affinely-independent Subset of TOP-REAL n;
theorem :: REAL_NS2:42
for n, m be Nat
for M be Matrix of n,m,F_Real
for A be affinely-independent Subset of REAL-NS n
st the_rank_of M = n
holds
(Mx2Tran M) .: A is affinely-independent;
theorem :: REAL_NS2:43
for Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n
st Ar = At
holds
Affin Ar = Affin At;
theorem :: REAL_NS2:44
for L be Linear_Combination of REAL-NS n,
S be Linear_Combination of TOP-REAL n
st L = S
holds
sum L = sum S;
theorem :: REAL_NS2:45
for Ar be Subset of REAL-NS n,
At be Subset of TOP-REAL n,
v be Element of REAL-NS n,
w be Element of TOP-REAL n
st Ar = At & v = w & v in Affin Ar & Ar is affinely-independent
holds
v |-- Ar = w |-- At;
theorem :: REAL_NS2:46
for n, m be Nat
for M be Matrix of n,m,F_Real
for A be affinely-independent Subset of REAL-NS n
st the_rank_of M = n
holds
for v be Element of REAL-NS n
st v in Affin A
holds
(Mx2Tran M).v in Affin((Mx2Tran M) .: A)
& (for f be n -element real-valued FinSequence
holds (v |-- A).f = (((Mx2Tran M).v)
|-- ((Mx2Tran M) .: A)) . ((Mx2Tran M).f));
theorem :: REAL_NS2:47
for n, m be Nat
for M be Matrix of n,m,F_Real
for A be linearly-independent Subset of REAL-NS m
st the_rank_of M = n
holds
(Mx2Tran M) " A is linearly-independent;
theorem :: REAL_NS2:48
for n, m be Nat
for M be Matrix of n,m,F_Real
for A be affinely-independent Subset of REAL-NS m
st the_rank_of M = n
holds
(Mx2Tran M) " A is affinely-independent;
theorem :: REAL_NS2:49
for V be RealLinearSpace,
W be strict Subspace of V
holds
W is strict Subspace of (Omega). V;
theorem :: REAL_NS2:50
for X be set holds
X is Basis of n -VectSp_over F_Real
iff
X is Basis of TOP-REAL n;
theorem :: REAL_NS2:51
for n be non empty Nat holds
RealFuncAdd Seg n = product(the addF of F_Real,n);
theorem :: REAL_NS2:52
for n be non empty Nat holds
RealFuncExtMult(Seg n) = n -Mult_over F_Real;
theorem :: REAL_NS2:53 ::: see also RLAFFIN3:4, not really used here
TOP-REAL n is finite-dimensional
&
dim TOP-REAL n = n;
theorem :: REAL_NS2:54
for n be non empty Nat holds
the carrier of (TOP-REAL n) = the carrier of (n -VectSp_over F_Real)
& 0. (TOP-REAL n) = 0. (n -VectSp_over F_Real)
& the addF of (TOP-REAL n) = the addF of (n -VectSp_over F_Real)
& the Mult of (TOP-REAL n) = the lmult of (n -VectSp_over F_Real);
theorem :: REAL_NS2:55
for n be non empty Nat,
xv, yv be Element of n -VectSp_over F_Real,
xt, yt be Element of TOP-REAL n
st xv = xt & yv = yt
holds xv + yv = xt + yt;
theorem :: REAL_NS2:56
for n be non empty Nat,
af be Element of F_Real,
at be Real,
xv be Element of n -VectSp_over F_Real,
xt be Element of TOP-REAL n
st af = at & xv = xt
holds af * xv = at * xt;
theorem :: REAL_NS2:57
for n be non empty Nat,
xv be Element of n -VectSp_over F_Real,
xt be Element of TOP-REAL n
st xv = xt
holds -xv = -xt;
theorem :: REAL_NS2:58
for n be non empty Nat,
xv, yv be Element of n -VectSp_over F_Real,
xt, yt be Element of TOP-REAL n
st xv = xt & yv = yt
holds xv - yv = xt - yt;
theorem :: REAL_NS2:59
for n be non empty Nat
for At be Subset of TOP-REAL n,
Ar be Subset of n -VectSp_over F_Real
st At = Ar
holds
the carrier of Lin At = the carrier of (Lin Ar)
& 0.(Lin At) = 0.(Lin Ar)
& the addF of Lin At = the addF of (Lin Ar)
& the Mult of Lin At = the lmult of (Lin Ar);
theorem :: REAL_NS2:60
for At be Subset of TOP-REAL n,
Ar be Subset of REAL-NS n
st At = Ar
holds Lin At = Lin Ar;
theorem :: REAL_NS2:61
for X be set holds
X is Basis of TOP-REAL n
iff
X is Basis of REAL-NS n;
theorem :: REAL_NS2:62
REAL-NS n is finite-dimensional
&
dim (REAL-NS n) = n;
begin :: Finite dimensional vector spaces over real field
registration
cluster finite-dimensional for RealNormSpace;
end;
theorem :: REAL_NS2:63
for K be Field,
V be finite-dimensional VectSp of K,
b be OrdBasis of V
holds
ex T be linear-transformation of V, (dim V) -VectSp_over K
st T is bijective
&
for x be Element of V holds T.x = x |-- b;
theorem :: REAL_NS2:64
for K be Field,
V be finite-dimensional VectSp of K
ex T be linear-transformation of V, (dim V) -VectSp_over K
st T is bijective;
theorem :: REAL_NS2:65
for K be Field,
V,W be finite-dimensional VectSp of K
holds
dim V = dim W
iff
ex T be linear-transformation of V, W st T is bijective;
theorem :: REAL_NS2:66
for X be RealLinearSpace
holds
the carrier of X = the carrier of (RLSp2RVSp X)
& the ZeroF of X = the ZeroF of (RLSp2RVSp X)
& the addF of X = the addF of (RLSp2RVSp X)
& the Mult of X = the lmult of (RLSp2RVSp X);
theorem :: REAL_NS2:67
for X be strict RealLinearSpace
holds RVSp2RLSp RLSp2RVSp X = X;
theorem :: REAL_NS2:68
for X be strict VectSp of F_Real
holds RLSp2RVSp RVSp2RLSp X = X;
theorem :: REAL_NS2:69
for V be RealLinearSpace,
F be set
holds
F is Subset of V
iff
F is Subset of RLSp2RVSp(V);
theorem :: REAL_NS2:70
for V be RealLinearSpace,
F be set
holds
F is FinSequence of V
iff
F is FinSequence of RLSp2RVSp(V);
theorem :: REAL_NS2:71
for V be RealLinearSpace,
F be set
holds
F is Function of V,REAL
iff
F is Function of RLSp2RVSp(V),REAL;
theorem :: REAL_NS2:72
for T be RealLinearSpace,
X be set
holds
X is Linear_Combination of RLSp2RVSp(T)
iff
X is Linear_Combination of T;
theorem :: REAL_NS2:73
for T be RealLinearSpace,
Lv be Linear_Combination of RLSp2RVSp(T),
Lr be Linear_Combination of T
st Lr = Lv
holds Carrier Lr = Carrier Lv;
theorem :: REAL_NS2:74
for V be RealLinearSpace,
Fr be FinSequence of V,
fr be Function of V,REAL,
Fv be FinSequence of RLSp2RVSp(V),
fv be Function of RLSp2RVSp(V),F_Real
st fr = fv & Fr = Fv
holds fr(#)Fr = fv(#)Fv;
theorem :: REAL_NS2:75
for T be RealLinearSpace,
Ft be FinSequence of T,
Fr be FinSequence of RLSp2RVSp(T)
st Ft = Fr
holds Sum Ft = Sum Fr;
theorem :: REAL_NS2:76
for T be RealLinearSpace,
Lv be Linear_Combination of RLSp2RVSp(T),
Lr be Linear_Combination of T
st Lr = Lv
holds Sum Lr = Sum Lv;
theorem :: REAL_NS2:77
for T be RealLinearSpace,
Af be Subset of RLSp2RVSp(T),
Ar be Subset of T
st Af = Ar
holds [#] (Lin Ar) = [#] (Lin Af);
theorem :: REAL_NS2:78
for T be RealLinearSpace,
Af be Subset of RLSp2RVSp(T),
Ar be Subset of T
st Af = Ar
holds
Af is linearly-independent
iff
Ar is linearly-independent;
theorem :: REAL_NS2:79
for T be RealLinearSpace
for X be set
for U be Subspace of RLSp2RVSp(T)
for W be Subspace of T
st [#] U = [#] W
holds
X is Linear_Combination of U
iff
X is Linear_Combination of W;
theorem :: REAL_NS2:80
for W be RealLinearSpace,
X be set
holds
X is Basis of RLSp2RVSp(W)
iff
X is Basis of W;
theorem :: REAL_NS2:81
for W be RealLinearSpace
st W is finite-dimensional
holds
RLSp2RVSp(W) is finite-dimensional
&
dim RLSp2RVSp(W) = dim W;
theorem :: REAL_NS2:82
for W be RealLinearSpace holds
W is finite-dimensional
iff
RLSp2RVSp(W) is finite-dimensional;
theorem :: REAL_NS2:83
for n be non empty Nat
holds
RLSp2RVSp(RealVectSpace(Seg n)) = n -VectSp_over F_Real;
theorem :: REAL_NS2:84
for V,W be RealLinearSpace,
X be set
holds
X is LinearOperator of V,W
iff
X is linear-transformation of RLSp2RVSp(V),RLSp2RVSp(W);
theorem :: REAL_NS2:85
for X, Y be RealLinearSpace,
L be LinearOperator of X,Y
st L is bijective
holds
ex K be LinearOperator of Y,X
st K = L" & K is one-to-one onto;
theorem :: REAL_NS2:86
for X,Y,Z be RealLinearSpace,
L be LinearOperator of X,Y,
K be LinearOperator of Y,Z
holds K*L is LinearOperator of X,Z;
theorem :: REAL_NS2:87
for V,W be RealLinearSpace,
A be Subset of V,
T be LinearOperator of V,W
st T is bijective
holds
A is Basis of V
iff
T.:A is Basis of W;
theorem :: REAL_NS2:88
for V be finite-dimensional RealLinearSpace,
W be RealLinearSpace
st (ex T be LinearOperator of V,W
st T is bijective)
holds
W is finite-dimensional
&
dim W = dim V;
theorem :: REAL_NS2:89
for V be finite-dimensional RealLinearSpace
st dim V <> 0
ex T be LinearOperator of V, RealVectSpace(Seg(dim V))
st T is bijective;
theorem :: REAL_NS2:90
for V,W be finite-dimensional RealLinearSpace
st dim V <> 0
holds
dim V = dim W
iff
ex T be LinearOperator of V, W st T is bijective;