:: Steinitz Theorem and Dimension of a Vector Space
:: by Mariusz \.Zynel
::
:: Received October 6, 1995
:: Copyright (c) 1995 Association of Mizar Users
theorem :: VECTSP_9:1
canceled;
theorem :: VECTSP_9:2
canceled;
theorem :: VECTSP_9:3
canceled;
theorem :: VECTSP_9:4
canceled;
Lm1:
for X, x being set st x in X holds
(X \ {x}) \/ {x} = X
theorem Th5: :: VECTSP_9:5
theorem Th6: :: VECTSP_9:6
theorem Th7: :: VECTSP_9:7
theorem Th8: :: VECTSP_9:8
theorem Th9: :: VECTSP_9:9
theorem Th10: :: VECTSP_9:10
theorem Th11: :: VECTSP_9:11
theorem Th12: :: VECTSP_9:12
theorem Th13: :: VECTSP_9:13
theorem Th14: :: VECTSP_9:14
theorem Th15: :: VECTSP_9:15
theorem Th16: :: VECTSP_9:16
theorem Th17: :: VECTSP_9:17
theorem Th18: :: VECTSP_9:18
theorem Th19: :: VECTSP_9:19
theorem Th20: :: VECTSP_9:20
theorem Th21: :: VECTSP_9:21
theorem Th22: :: VECTSP_9:22
theorem Th23: :: VECTSP_9:23
theorem Th24: :: VECTSP_9:24
theorem :: VECTSP_9:25
theorem Th26: :: VECTSP_9:26
theorem Th27: :: VECTSP_9:27
theorem Th28: :: VECTSP_9:28
:: deftheorem VECTSP_9:def 1 :
canceled;
:: deftheorem Def2 defines dim VECTSP_9:def 2 :
theorem Th29: :: VECTSP_9:29
theorem Th30: :: VECTSP_9:30
theorem Th31: :: VECTSP_9:31
theorem :: VECTSP_9:32
theorem Th33: :: VECTSP_9:33
theorem :: VECTSP_9:34
theorem :: VECTSP_9:35
theorem Th36: :: VECTSP_9:36
theorem :: VECTSP_9:37
theorem :: VECTSP_9:38
Lm2:
for GF being Field
for n being Nat
for V being finite-dimensional VectSp of GF st n <= dim V holds
ex W being strict Subspace of V st dim W = n
theorem :: VECTSP_9:39
:: deftheorem Def3 defines Subspaces_of VECTSP_9:def 3 :
theorem :: VECTSP_9:40
theorem :: VECTSP_9:41
theorem :: VECTSP_9:42