begin
:: deftheorem defines <*> BSPACE:def 1 :
theorem
theorem
begin
:: deftheorem defines Z_2 BSPACE:def 2 :
theorem
theorem
theorem Th5:
theorem Th6:
theorem Th7:
theorem
begin
:: deftheorem Def3 defines @ BSPACE:def 3 :
theorem
theorem
theorem
theorem
for
X,
x,
y being
set holds
(
X @ x = X @ y iff (
x in X iff
y in X ) )
theorem
for
X,
Y,
x being
set holds
(
X @ x = Y @ x iff (
x in X iff
x in Y ) )
theorem
theorem Th15:
theorem
for
X,
Y being
set holds
(
X = Y iff for
x being
set holds
X @ x = Y @ x )
begin
:: deftheorem Def4 defines \*\ BSPACE:def 4 :
:: deftheorem Def5 defines bspace-sum BSPACE:def 5 :
theorem Th17:
theorem Th18:
theorem
theorem Th20:
definition
let X be
set ;
func bspace-scalar-mult X -> Function of
[:the carrier of Z_2 ,(bool X):],
bool X means :
Def6:
for
a being
Element of
for
c being
Subset of holds
it . a,
c = a \*\ c;
existence
ex b1 being Function of [:the carrier of Z_2 ,(bool X):], bool X st
for a being Element of
for c being Subset of holds b1 . a,c = a \*\ c
uniqueness
for b1, b2 being Function of [:the carrier of Z_2 ,(bool X):], bool X st ( for a being Element of
for c being Subset of holds b1 . a,c = a \*\ c ) & ( for a being Element of
for c being Subset of holds b2 . a,c = a \*\ c ) holds
b1 = b2
end;
:: deftheorem Def6 defines bspace-scalar-mult BSPACE:def 6 :
:: deftheorem defines bspace BSPACE:def 7 :
Lm1:
for X being set
for a, b, c being Element of
for A, B, C being Subset of st a = A & b = B & c = C holds
( a + (b + c) = A \+\ (B \+\ C) & (a + b) + c = (A \+\ B) \+\ C )
Lm2:
for X being set
for a, b being Element of
for x, y being Element of
for c, d being Subset of st x = c & y = d holds
( (a * x) + (b * y) = (a \*\ c) \+\ (b \*\ d) & a * (x + y) = a \*\ (c \+\ d) & (a + b) * x = (a + b) \*\ c & (a * b) * x = (a * b) \*\ c & a * (b * x) = a \*\ (b \*\ c) )
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
begin
:: deftheorem Def8 defines Singleton BSPACE:def 8 :
:: deftheorem Def9 defines Singleton BSPACE:def 9 :
:: deftheorem defines singletons BSPACE:def 10 :
theorem Th30:
:: deftheorem Def11 defines @ BSPACE:def 11 :
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem Th39:
theorem Th40:
theorem Th41:
theorem
theorem
theorem