:: Dimension of Real Unitary Space
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 9, 2002
:: Copyright (c) 2002 Association of Mizar Users
theorem Th1: :: RUSUB_4:1
Lm1:
for X, x being set st x in X holds
(X \ {x}) \/ {x} = X
Lm2:
for X, x being set st not x in X holds
X \ {x} = X
theorem Th2: :: RUSUB_4:2
:: deftheorem Def1 defines finite-dimensional RUSUB_4:def 1 :
theorem Th3: :: RUSUB_4:3
theorem :: RUSUB_4:4
theorem Th5: :: RUSUB_4:5
theorem Th6: :: RUSUB_4:6
theorem Th7: :: RUSUB_4:7
:: deftheorem RUSUB_4:def 2 :
canceled;
:: deftheorem Def3 defines dim RUSUB_4:def 3 :
theorem Th8: :: RUSUB_4:8
theorem Th9: :: RUSUB_4:9
theorem Th10: :: RUSUB_4:10
theorem :: RUSUB_4:11
theorem Th12: :: RUSUB_4:12
theorem :: RUSUB_4:13
theorem :: RUSUB_4:14
theorem Th15: :: RUSUB_4:15
theorem :: RUSUB_4:16
theorem :: RUSUB_4:17
Lm3:
for V being finite-dimensional RealUnitarySpace
for n being Element of NAT st n <= dim V holds
ex W being strict Subspace of V st dim W = n
theorem :: RUSUB_4:18
:: deftheorem Def4 defines Subspaces_of RUSUB_4:def 4 :
theorem :: RUSUB_4:19
theorem :: RUSUB_4:20
theorem :: RUSUB_4:21
:: deftheorem Def5 defines Affine RUSUB_4:def 5 :
theorem Th22: :: RUSUB_4:22
theorem :: RUSUB_4:23
:: deftheorem defines Up RUSUB_4:def 6 :
:: deftheorem defines Up RUSUB_4:def 7 :
theorem :: RUSUB_4:24
theorem Th25: :: RUSUB_4:25
:: deftheorem Def8 defines Subspace-like RUSUB_4:def 8 :
theorem Th26: :: RUSUB_4:26
theorem :: RUSUB_4:27
theorem :: RUSUB_4:28
canceled;
theorem :: RUSUB_4:29
theorem :: RUSUB_4:30
:: deftheorem defines + RUSUB_4:def 9 :
theorem :: RUSUB_4:31
canceled;
theorem :: RUSUB_4:32
theorem Th33: :: RUSUB_4:33
theorem :: RUSUB_4:34
:: deftheorem defines + RUSUB_4:def 10 :
theorem Th35: :: RUSUB_4:35
theorem Th36: :: RUSUB_4:36
theorem :: RUSUB_4:37
theorem :: RUSUB_4:38
theorem :: RUSUB_4:39