Volume 7, 1995

University of Bialystok

Copyright (c) 1995 Association of Mizar Users

### The abstract of the Mizar article:

### On the Lattice of Subspaces of a Vector Space

**by****Andrzej Iwaniuk**- Received May 23, 1995
- MML identifier: VECTSP_8

- [ Mizar article, MML identifier index ]

environ vocabulary VECTSP_1, GROUP_4, LATTICES, RLSUB_2, RLSUB_1, BOOLE, GROUP_2, FUNCT_1, RELAT_1, RLVECT_1, SETFAM_1, BHSP_3, LATTICE3, RLVECT_3, GROUP_6, PRE_TOPC, INCSP_1, VECTSP_8; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, LATTICE4, SETFAM_1, RLVECT_1, STRUCT_0, VECTSP_1, PRE_TOPC, LATTICES, VECTSP_5, LATTICE3, VECTSP_4, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, VECTSP_7, MOD_2; constructors LATTICE4, VECTSP_5, LATTICE3, BINOP_1, VECTSP_7, MOD_2, VECTSP_2; clusters LATTICES, VECTSP_4, VECTSP_2, STRUCT_0, VECTSP_5, RELSET_1, SUBSET_1, FUNCT_2, PARTFUN1, XBOOLE_0; requirements BOOLE, SUBSET; begin reserve F for Field; reserve VS for strict VectSp of F; definition let F, VS; func lattice VS -> strict bounded Lattice equals :: VECTSP_8:def 1 LattStr (# Subspaces(VS), SubJoin(VS), SubMeet(VS) #); end; definition let F,VS; mode SubVS-Family of VS means :: VECTSP_8:def 2 for x be set st x in it holds x is Subspace of VS; end; definition let F,VS; cluster non empty SubVS-Family of VS; end; definition let F,VS; redefine func Subspaces(VS) -> non empty SubVS-Family of VS; let X be non empty SubVS-Family of VS; mode Element of X -> Subspace of VS; end; definition let F,VS; let x be Element of Subspaces VS; func carr(x) -> Subset of VS means :: VECTSP_8:def 3 ex X being Subspace of VS st x=X & it = the carrier of X; end; reserve u,e for set; definition let F,VS; func carr VS -> Function of Subspaces(VS),bool the carrier of VS means :: VECTSP_8:def 4 for h being Element of Subspaces(VS), H being Subspace of VS st h = H holds it.h = the carrier of H; end; theorem :: VECTSP_8:1 for VS being strict VectSp of F for H being non empty Subset of Subspaces VS holds (carr VS).:H is non empty; theorem :: VECTSP_8:2 for VS being strict VectSp of F for H being strict Subspace of VS holds 0.VS in (carr VS).H; reserve x for set; definition let F,VS; let G be non empty Subset of Subspaces(VS); func meet G -> strict Subspace of VS means :: VECTSP_8:def 5 the carrier of it = meet ((carr VS).:G); end; theorem :: VECTSP_8:3 Subspaces(VS) = the carrier of lattice VS; theorem :: VECTSP_8:4 the L_meet of lattice VS = SubMeet(VS); theorem :: VECTSP_8:5 the L_join of lattice VS = SubJoin(VS); theorem :: VECTSP_8:6 for VS being strict VectSp of F, p,q being Element of lattice VS, H1,H2 being strict Subspace of VS st p=H1 & q=H2 holds p [= q iff the carrier of H1 c= the carrier of H2; theorem :: VECTSP_8:7 for VS being strict VectSp of F, p,q being Element of lattice VS, H1,H2 being Subspace of VS st p=H1 & q=H2 holds p"\/"q = H1+H2; theorem :: VECTSP_8:8 for VS being strict VectSp of F, p,q being Element of lattice VS, H1,H2 being Subspace of VS st p=H1 & q=H2 holds p"/\"q = H1 /\ H2; definition let L be non empty LattStr; redefine attr L is complete means :: VECTSP_8:def 6 for X being Subset of L ex a being Element of L st a is_less_than X & for b being Element of L st b is_less_than X holds b [= a; end; reserve Z1 for set; theorem :: VECTSP_8:9 for VS holds lattice VS is complete; theorem :: VECTSP_8:10 for x being set for VS being strict VectSp of F for S being Subset of VS st S is non empty & S is lineary-closed holds x in Lin S implies x in S; definition let F be Field; let A,B be strict VectSp of F; let f be Function of the carrier of A,the carrier of B; func FuncLatt f -> Function of the carrier of lattice A, the carrier of lattice B means :: VECTSP_8:def 7 for S being strict Subspace of A, B0 being Subset of B st B0 = f.:the carrier of S holds it.S = Lin B0; end; definition let L1, L2 be Lattice; mode Semilattice-Homomorphism of L1,L2 -> Function of the carrier of L1, the carrier of L2 means :: VECTSP_8:def 8 for a, b being Element of L1 holds it.(a "/\" b) = it.a "/\" it.b; end; definition let L1, L2 be Lattice; mode sup-Semilattice-Homomorphism of L1, L2 -> Function of the carrier of L1, the carrier of L2 means :: VECTSP_8:def 9 for a, b being Element of L1 holds it.(a "\/" b) = it.a "\/" it.b; end; theorem :: VECTSP_8:11 for L1,L2 being Lattice for f being Function of the carrier of L1, the carrier of L2 holds f is Homomorphism of L1, L2 iff f is sup-Semilattice-Homomorphism of L1, L2 & f is Semilattice-Homomorphism of L1, L2; theorem :: VECTSP_8:12 for F being Field for A,B being strict VectSp of F for f be map of A, B st f is linear holds FuncLatt f is sup-Semilattice-Homomorphism of lattice A, lattice B; theorem :: VECTSP_8:13 for F being Field for A,B being strict VectSp of F for f be map of A,B st f is one-to-one linear holds FuncLatt f is Homomorphism of lattice A, lattice B; theorem :: VECTSP_8:14 for A,B being strict VectSp of F for f being map of A, B st f is linear & f is one-to-one holds FuncLatt f is one-to-one; theorem :: VECTSP_8:15 for A being strict VectSp of F holds FuncLatt id the carrier of A = id the carrier of lattice A;

Back to top