:: Dimension of Real Unitary Space
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 9, 2002
:: Copyright (c) 2002-2017 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 NUMBERS, BHSP_1, FINSET_1, SUBSET_1, RLVECT_1, RLVECT_3,
XBOOLE_0, RLVECT_2, CARD_3, TARSKI, FUNCT_1, CARD_1, FINSEQ_1, STRUCT_0,
RELAT_1, VALUED_1, FINSEQ_4, ORDINAL4, ARYTM_1, ARYTM_3, XXREAL_0,
RLSUB_1, RLVECT_5, NAT_1, SUPINF_2, FUNCT_2, RLSUB_2, REAL_1, ALGSTR_0,
RUSUB_4;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, REAL_1, NAT_1, FINSEQ_1, FUNCT_1, FUNCT_2, DOMAIN_1,
STRUCT_0, ALGSTR_0, RLVECT_1, FINSEQ_3, FINSEQ_4, FINSET_1, RLSUB_1,
RLVECT_2, BHSP_1, RLVECT_3, RUSUB_1, RUSUB_2, RUSUB_3, XXREAL_0;
constructors XXREAL_0, REAL_1, NAT_1, PARTFUN1, FINSEQ_3, FINSEQ_4, REALSET1,
RLVECT_2, RLVECT_3, RUSUB_2, RUSUB_3, RELSET_1;
registrations SUBSET_1, RELSET_1, FINSET_1, XREAL_0, NAT_1, FINSEQ_1,
STRUCT_0, RLVECT_1, RLSUB_1, RLVECT_3, ORDINAL1, CARD_1, RLVECT_2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Finite-dimensional real unitary space
theorem :: RUSUB_4:1
for V being RealUnitarySpace, A,B being finite Subset of V, v
being VECTOR of V st v in Lin(A \/ B) & not v in Lin(B) holds ex w being VECTOR
of V st w in A & w in Lin(A \/ B \ {w} \/ {v});
theorem :: RUSUB_4:2
for V being RealUnitarySpace, A,B being finite Subset of V st the
UNITSTR of V = Lin(A) & B is linearly-independent holds card B <= card A & ex C
being finite Subset of V st C c= A & card C = card A - card B & the UNITSTR of
V = Lin(B \/ C);
definition
let V be RealUnitarySpace;
attr V is finite-dimensional means
:: RUSUB_4:def 1
ex A being finite Subset of V st A is Basis of V;
end;
registration
cluster strict finite-dimensional for RealUnitarySpace;
end;
theorem :: RUSUB_4:3
for V being RealUnitarySpace st V is finite-dimensional holds for
I being Basis of V holds I is finite;
theorem :: RUSUB_4:4
for V being RealUnitarySpace, A being Subset of V st V is
finite-dimensional & A is linearly-independent holds A is finite;
theorem :: RUSUB_4:5
for V being RealUnitarySpace, A,B being Basis of V st V is
finite-dimensional holds card A = card B;
theorem :: RUSUB_4:6
for V being RealUnitarySpace holds (0).V is finite-dimensional;
theorem :: RUSUB_4:7
for V being RealUnitarySpace, W being Subspace of V st V is
finite-dimensional holds W is finite-dimensional;
registration
let V be RealUnitarySpace;
cluster finite-dimensional strict for Subspace of V;
end;
registration
let V be finite-dimensional RealUnitarySpace;
cluster -> finite-dimensional for Subspace of V;
end;
registration
let V be finite-dimensional RealUnitarySpace;
cluster strict for Subspace of V;
end;
begin :: Dimension of real unitary space
definition
let V be RealUnitarySpace;
assume
V is finite-dimensional;
func dim V -> Element of NAT means
:: RUSUB_4:def 2
for I being Basis of V holds it = card I;
end;
theorem :: RUSUB_4:8
for V being finite-dimensional RealUnitarySpace, W being Subspace
of V holds dim W <= dim V;
theorem :: RUSUB_4:9
for V being finite-dimensional RealUnitarySpace, A being Subset
of V st A is linearly-independent holds card A = dim Lin(A);
theorem :: RUSUB_4:10
for V being finite-dimensional RealUnitarySpace holds dim V = dim (Omega).V;
theorem :: RUSUB_4:11
for V being finite-dimensional RealUnitarySpace, W being Subspace of V
holds dim V = dim W iff (Omega).V = (Omega).W;
theorem :: RUSUB_4:12
for V being finite-dimensional RealUnitarySpace holds dim V = 0
iff (Omega).V = (0).V;
theorem :: RUSUB_4:13
for V being finite-dimensional RealUnitarySpace holds dim V = 1 iff ex
v being VECTOR of V st v <> 0.V & (Omega).V = Lin{v};
theorem :: RUSUB_4:14
for V being finite-dimensional RealUnitarySpace holds dim V = 2 iff ex
u,v being VECTOR of V st u <> v & {u, v} is linearly-independent & (Omega).V =
Lin{u, v};
theorem :: RUSUB_4:15
for V being finite-dimensional RealUnitarySpace, W1,W2 being
Subspace of V holds dim(W1 + W2) + dim(W1 /\ W2) = dim W1 + dim W2;
theorem :: RUSUB_4:16
for V being finite-dimensional RealUnitarySpace, W1,W2 being Subspace
of V holds dim(W1 /\ W2) >= dim W1 + dim W2 - dim V;
theorem :: RUSUB_4:17
for V being finite-dimensional RealUnitarySpace, W1,W2 being Subspace
of V st V is_the_direct_sum_of W1, W2 holds dim V = dim W1 + dim W2;
begin
theorem :: RUSUB_4:18
for V being finite-dimensional RealUnitarySpace, W being Subspace of V
, n being Element of NAT holds n <= dim V iff ex W being strict Subspace of V
st dim W = n;
definition
let V be finite-dimensional RealUnitarySpace, n be Element of NAT;
func n Subspaces_of V -> set means
:: RUSUB_4:def 3
for x being object holds x in it iff
ex W being strict Subspace of V st W = x & dim W = n;
end;
theorem :: RUSUB_4:19
for V being finite-dimensional RealUnitarySpace, n being Element of
NAT st n <= dim V holds n Subspaces_of V is non empty;
theorem :: RUSUB_4:20
for V being finite-dimensional RealUnitarySpace, n being Element of
NAT st dim V < n holds n Subspaces_of V = {};
theorem :: RUSUB_4:21
for V being finite-dimensional RealUnitarySpace, W being Subspace of V
, n being Element of NAT holds n Subspaces_of W c= n Subspaces_of V;
begin :: Affine set
definition
let V be non empty RLSStruct, S be Subset of V;
attr S is Affine means
:: RUSUB_4:def 4
for x,y being VECTOR of V, a being Real st x
in S & y in S holds (1 - a) * x + a * y in S;
end;
theorem :: RUSUB_4:22
for V being non empty RLSStruct holds [#]V is Affine & {}V is Affine;
theorem :: RUSUB_4:23
for V being vector-distributive scalar-distributive scalar-associative
scalar-unital non empty RLSStruct, v being VECTOR
of V holds {v} is Affine;
registration
let V be non empty RLSStruct;
cluster non empty Affine for Subset of V;
cluster empty Affine for Subset of V;
end;
definition
let V be RealLinearSpace, W be Subspace of V;
func Up(W) -> non empty Subset of V equals
:: RUSUB_4:def 5
the carrier of W;
end;
definition
let V be RealUnitarySpace, W be Subspace of V;
func Up(W) -> non empty Subset of V equals
:: RUSUB_4:def 6
the carrier of W;
end;
theorem :: RUSUB_4:24
for V being RealLinearSpace, W being Subspace of V holds Up(W) is
Affine & 0.V in the carrier of W;
theorem :: RUSUB_4:25
for V being RealLinearSpace, A being Affine Subset of V st 0.V in A
for x being VECTOR of V, a being Real st x in A holds a * x in A;
definition
let V be non empty RLSStruct, S be non empty Subset of V;
attr S is Subspace-like means
:: RUSUB_4:def 7
0.V in S & for x,y being Element of V,
a being Real st x in S & y in S holds x + y in S & a * x in S;
end;
theorem :: RUSUB_4:26
for V being RealLinearSpace, A being non empty Affine Subset of
V st 0.V in A holds A is Subspace-like & A = the carrier of Lin(A);
theorem :: RUSUB_4:27
for V being RealLinearSpace, W being Subspace of V holds Up(W) is
Subspace-like;
theorem :: RUSUB_4:28
for V being RealUnitarySpace, A being non empty Affine Subset of V st
0.V in A holds A = the carrier of Lin(A);
theorem :: RUSUB_4:29
for V being RealUnitarySpace, W being Subspace of V holds Up(W) is
Subspace-like;
definition
let V be non empty addLoopStr, M be Subset of V, v be Element of V;
func v + M -> Subset of V equals
:: RUSUB_4:def 8
{v + u where u is Element of V: u in M};
end;
theorem :: RUSUB_4:30
for V being RealLinearSpace, W being strict Subspace of V, M being
Subset of V, v being VECTOR of V st Up(W) = M holds v + W = v + M;
theorem :: RUSUB_4:31
for V being Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non
empty RLSStruct, M being Affine Subset of V, v being VECTOR of V holds v + M
is Affine;
theorem :: RUSUB_4:32
for V being RealUnitarySpace, W being strict Subspace of V, M being
Subset of V, v being VECTOR of V st Up(W) = M holds v + W = v + M;
definition
let V be non empty addLoopStr, M,N be Subset of V;
func M + N -> Subset of V equals
:: RUSUB_4:def 9
{u + v where u,v is Element of V: u in M &
v in N};
end;
definition
let V be Abelian non empty addLoopStr, M,N be Subset of V;
redefine func M + N;
commutativity;
end;
theorem :: RUSUB_4:33
for V being non empty addLoopStr, M being Subset of V, v being
Element of V holds {v} + M = v + M;
theorem :: RUSUB_4:34
for V being Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty
RLSStruct, M being Affine Subset of V, v being VECTOR of V holds {v} + M is
Affine;
theorem :: RUSUB_4:35
for V being non empty RLSStruct, M,N being Affine Subset of V holds M
/\ N is Affine;
theorem :: RUSUB_4:36
for V being Abelian add-associative vector-distributive scalar-distributive
scalar-associative scalar-unital non empty
RLSStruct, M,N being Affine Subset of V holds M + N is Affine;