:: On the Lattice of Subspaces of Vector Space
:: by Andrzej Iwaniuk
::
:: Received May 23, 1995
:: Copyright (c) 1995 Association of Mizar Users
:: deftheorem defines lattice VECTSP_8:def 1 :
:: deftheorem Def2 defines SubVS-Family VECTSP_8:def 2 :
:: deftheorem Def3 defines carr VECTSP_8:def 3 :
:: deftheorem Def4 defines carr VECTSP_8:def 4 :
theorem Th1: :: VECTSP_8:1
theorem :: VECTSP_8:2
:: deftheorem Def5 defines meet VECTSP_8:def 5 :
theorem :: VECTSP_8:3
theorem :: VECTSP_8:4
theorem :: VECTSP_8:5
theorem Th6: :: VECTSP_8:6
theorem Th7: :: VECTSP_8:7
theorem Th8: :: VECTSP_8:8
:: deftheorem defines complete VECTSP_8:def 6 :
theorem :: VECTSP_8:9
theorem Th10: :: VECTSP_8:10
:: deftheorem Def7 defines FuncLatt VECTSP_8:def 7 :
:: deftheorem Def8 defines Semilattice-Homomorphism VECTSP_8:def 8 :
:: deftheorem Def9 defines sup-Semilattice-Homomorphism VECTSP_8:def 9 :
theorem :: VECTSP_8:11
theorem Th12: :: VECTSP_8:12
theorem :: VECTSP_8:13
theorem :: VECTSP_8:14
theorem :: VECTSP_8:15