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