:: Subspaces and Cosets of Subspace of Real Unitary Space
:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama
::
:: Received October 9, 2002
:: Copyright (c) 2002 Association of Mizar Users
:: deftheorem Def1 defines Subspace RUSUB_1:def 1 :
theorem :: RUSUB_1:1
theorem Th2: :: RUSUB_1:2
theorem Th3: :: RUSUB_1:3
theorem :: RUSUB_1:4
theorem :: RUSUB_1:5
theorem Th6: :: RUSUB_1:6
theorem Th7: :: RUSUB_1:7
theorem :: RUSUB_1:8
theorem Th9: :: RUSUB_1:9
theorem Th10: :: RUSUB_1:10
theorem Th11: :: RUSUB_1:11
theorem :: RUSUB_1:12
theorem :: RUSUB_1:13
Lm1:
for V being RealUnitarySpace
for W being Subspace of V
for V1, V2 being Subset of V st the carrier of W = V1 holds
V1 is linearly-closed
theorem Th14: :: RUSUB_1:14
theorem Th15: :: RUSUB_1:15
theorem Th16: :: RUSUB_1:16
theorem Th17: :: RUSUB_1:17
theorem Th18: :: RUSUB_1:18
theorem Th19: :: RUSUB_1:19
theorem Th20: :: RUSUB_1:20
theorem Th21: :: RUSUB_1:21
theorem Th22: :: RUSUB_1:22
theorem :: RUSUB_1:23
theorem Th24: :: RUSUB_1:24
theorem Th25: :: RUSUB_1:25
theorem :: RUSUB_1:26
theorem :: RUSUB_1:27
theorem :: RUSUB_1:28
theorem Th29: :: RUSUB_1:29
:: deftheorem Def2 defines (0). RUSUB_1:def 2 :
:: deftheorem defines (Omega). RUSUB_1:def 3 :
theorem Th30: :: RUSUB_1:30
theorem Th31: :: RUSUB_1:31
theorem :: RUSUB_1:32
theorem :: RUSUB_1:33
theorem :: RUSUB_1:34
theorem :: RUSUB_1:35
:: deftheorem defines + RUSUB_1:def 4 :
Lm2:
for V being RealUnitarySpace
for W being Subspace of V holds (0. V) + W = the carrier of W
:: deftheorem Def5 defines Coset RUSUB_1:def 5 :
theorem Th36: :: RUSUB_1:36
theorem Th37: :: RUSUB_1:37
theorem :: RUSUB_1:38
theorem Th39: :: RUSUB_1:39
Lm3:
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V holds
( v in W iff v + W = the carrier of W )
theorem Th40: :: RUSUB_1:40
theorem Th41: :: RUSUB_1:41
theorem :: RUSUB_1:42
theorem Th43: :: RUSUB_1:43
theorem Th44: :: RUSUB_1:44
theorem Th45: :: RUSUB_1:45
theorem Th46: :: RUSUB_1:46
theorem :: RUSUB_1:47
theorem Th48: :: RUSUB_1:48
theorem Th49: :: RUSUB_1:49
theorem Th50: :: RUSUB_1:50
theorem :: RUSUB_1:51
theorem Th52: :: RUSUB_1:52
theorem Th53: :: RUSUB_1:53
theorem :: RUSUB_1:54
theorem Th55: :: RUSUB_1:55
theorem :: RUSUB_1:56
theorem Th57: :: RUSUB_1:57
theorem :: RUSUB_1:58
theorem Th59: :: RUSUB_1:59
theorem Th60: :: RUSUB_1:60
theorem Th61: :: RUSUB_1:61
theorem Th62: :: RUSUB_1:62
theorem Th63: :: RUSUB_1:63
theorem :: RUSUB_1:64
theorem :: RUSUB_1:65
theorem :: RUSUB_1:66
theorem :: RUSUB_1:67
theorem :: RUSUB_1:68
theorem :: RUSUB_1:69
theorem :: RUSUB_1:70
theorem :: RUSUB_1:71
theorem Th72: :: RUSUB_1:72
theorem :: RUSUB_1:73
theorem :: RUSUB_1:74
theorem :: RUSUB_1:75
theorem :: RUSUB_1:76