:: Subspaces and Cosets of Subspaces in Real Linear Space
:: by Wojciech A. Trybulec
::
:: Received July 24, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines linearly-closed RLSUB_1:def 1 :
theorem :: RLSUB_1:1
canceled;
theorem :: RLSUB_1:2
canceled;
theorem :: RLSUB_1:3
canceled;
theorem Th4: :: RLSUB_1:4
theorem Th5: :: RLSUB_1:5
theorem :: RLSUB_1:6
theorem Th7: :: RLSUB_1:7
theorem :: RLSUB_1:8
theorem :: RLSUB_1:9
theorem :: RLSUB_1:10
:: deftheorem Def2 defines Subspace RLSUB_1:def 2 :
theorem :: RLSUB_1:11
canceled;
theorem :: RLSUB_1:12
canceled;
theorem :: RLSUB_1:13
canceled;
theorem :: RLSUB_1:14
canceled;
theorem :: RLSUB_1:15
canceled;
theorem :: RLSUB_1:16
theorem Th17: :: RLSUB_1:17
theorem Th18: :: RLSUB_1:18
theorem :: RLSUB_1:19
theorem :: RLSUB_1:20
theorem Th21: :: RLSUB_1:21
theorem Th22: :: RLSUB_1:22
theorem Th23: :: RLSUB_1:23
theorem Th24: :: RLSUB_1:24
Lm1:
for V being RealLinearSpace
for V1 being Subset of V
for W being Subspace of V st the carrier of W = V1 holds
V1 is linearly-closed
theorem Th25: :: RLSUB_1:25
theorem :: RLSUB_1:26
theorem :: RLSUB_1:27
theorem Th28: :: RLSUB_1:28
theorem Th29: :: RLSUB_1:29
theorem Th30: :: RLSUB_1:30
theorem Th31: :: RLSUB_1:31
theorem Th32: :: RLSUB_1:32
theorem Th33: :: RLSUB_1:33
theorem Th34: :: RLSUB_1:34
theorem Th35: :: RLSUB_1:35
theorem Th36: :: RLSUB_1:36
theorem :: RLSUB_1:37
theorem Th38: :: RLSUB_1:38
theorem Th39: :: RLSUB_1:39
theorem :: RLSUB_1:40
theorem :: RLSUB_1:41
theorem :: RLSUB_1:42
theorem Th43: :: RLSUB_1:43
:: deftheorem Def3 defines (0). RLSUB_1:def 3 :
:: deftheorem defines (Omega). RLSUB_1:def 4 :
theorem :: RLSUB_1:44
canceled;
theorem :: RLSUB_1:45
canceled;
theorem :: RLSUB_1:46
canceled;
theorem :: RLSUB_1:47
canceled;
theorem Th48: :: RLSUB_1:48
theorem Th49: :: RLSUB_1:49
theorem :: RLSUB_1:50
theorem :: RLSUB_1:51
theorem :: RLSUB_1:52
theorem :: RLSUB_1:53
canceled;
theorem :: RLSUB_1:54
:: deftheorem defines + RLSUB_1:def 5 :
Lm2:
for V being RealLinearSpace
for W being Subspace of V holds (0. V) + W = the carrier of W
:: deftheorem Def6 defines Coset RLSUB_1:def 6 :
theorem :: RLSUB_1:55
canceled;
theorem :: RLSUB_1:56
canceled;
theorem :: RLSUB_1:57
canceled;
theorem Th58: :: RLSUB_1:58
theorem Th59: :: RLSUB_1:59
theorem :: RLSUB_1:60
theorem Th61: :: RLSUB_1:61
Lm3:
for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( v in W iff v + W = the carrier of W )
theorem Th62: :: RLSUB_1:62
theorem Th63: :: RLSUB_1:63
theorem :: RLSUB_1:64
theorem Th65: :: RLSUB_1:65
theorem Th66: :: RLSUB_1:66
theorem Th67: :: RLSUB_1:67
theorem Th68: :: RLSUB_1:68
theorem :: RLSUB_1:69
theorem Th70: :: RLSUB_1:70
theorem Th71: :: RLSUB_1:71
theorem Th72: :: RLSUB_1:72
theorem :: RLSUB_1:73
theorem Th74: :: RLSUB_1:74
theorem Th75: :: RLSUB_1:75
theorem :: RLSUB_1:76
theorem Th77: :: RLSUB_1:77
theorem :: RLSUB_1:78
theorem Th79: :: RLSUB_1:79
theorem :: RLSUB_1:80
theorem Th81: :: RLSUB_1:81
theorem Th82: :: RLSUB_1:82
theorem Th83: :: RLSUB_1:83
theorem Th84: :: RLSUB_1:84
theorem Th85: :: RLSUB_1:85
theorem :: RLSUB_1:86
theorem :: RLSUB_1:87
theorem :: RLSUB_1:88
theorem :: RLSUB_1:89
theorem :: RLSUB_1:90
theorem :: RLSUB_1:91
theorem :: RLSUB_1:92
theorem :: RLSUB_1:93
theorem Th94: :: RLSUB_1:94
theorem :: RLSUB_1:95
theorem :: RLSUB_1:96
theorem :: RLSUB_1:97
theorem :: RLSUB_1:98