begin
:: deftheorem defines lattice VECTSP_8:def 1 :
for F being Field
for VS being strict VectSp of F holds lattice VS = LattStr(# (Subspaces VS),(SubJoin VS),(SubMeet VS) #);
:: deftheorem Def2 defines SubVS-Family VECTSP_8:def 2 :
for F being Field
for VS being strict VectSp of F
for b3 being set holds
( b3 is SubVS-Family of VS iff for x being set st x in b3 holds
x is Subspace of VS );
:: deftheorem Def3 defines carr VECTSP_8:def 3 :
for F being Field
for VS being strict VectSp of F
for x being Element of Subspaces VS
for b4 being Subset of VS holds
( b4 = carr x iff ex X being Subspace of VS st
( x = X & b4 = the carrier of X ) );
:: deftheorem Def4 defines carr VECTSP_8:def 4 :
for F being Field
for VS being strict VectSp of F
for b3 being Function of (Subspaces VS),(bool the carrier of VS) holds
( b3 = carr VS iff for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
b3 . h = the carrier of H );
theorem Th1:
theorem
:: deftheorem Def5 defines meet VECTSP_8:def 5 :
for F being Field
for VS being strict VectSp of F
for G being non empty Subset of (Subspaces VS)
for b4 being strict Subspace of VS holds
( b4 = meet G iff the carrier of b4 = meet ((carr VS) .: G) );
theorem
theorem
theorem
theorem Th6:
theorem Th7:
theorem Th8:
:: deftheorem defines complete VECTSP_8:def 6 :
for L being non empty LattStr holds
( L is complete iff 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 ) ) );
theorem
theorem Th10:
:: deftheorem Def7 defines FuncLatt VECTSP_8:def 7 :
for F being Field
for A, B being strict VectSp of F
for f being Function of the carrier of A, the carrier of B
for b5 being Function of the carrier of (lattice A), the carrier of (lattice B) holds
( b5 = FuncLatt f iff for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
b5 . S = Lin B0 );
:: deftheorem Def8 defines Semilattice-Homomorphism VECTSP_8:def 8 :
for L1, L2 being Lattice
for b3 being Function of the carrier of L1, the carrier of L2 holds
( b3 is Semilattice-Homomorphism of L1,L2 iff for a, b being Element of L1 holds b3 . (a "/\" b) = (b3 . a) "/\" (b3 . b) );
:: deftheorem Def9 defines sup-Semilattice-Homomorphism VECTSP_8:def 9 :
for L1, L2 being Lattice
for b3 being Function of the carrier of L1, the carrier of L2 holds
( b3 is sup-Semilattice-Homomorphism of L1,L2 iff for a, b being Element of L1 holds b3 . (a "\/" b) = (b3 . a) "\/" (b3 . b) );
theorem
theorem Th12:
theorem
theorem
theorem