:: The Vector Space of Subsets of a Set Based on Symmetric Difference
:: by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, STRUCT_0, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, NAT_1,
ORDINAL4, VECTSP_1, INT_3, CARD_1, SUPINF_2, MESFUNC1, ARYTM_3, INT_1,
QC_LANG1, XBOOLE_0, TARSKI, BINOP_1, ZFMISC_1, RLVECT_1, ALGSTR_0,
GROUP_1, RLVECT_2, XXREAL_0, CARD_3, RLVECT_3, REALSET1, VALUED_1,
FINSEQ_2, PARTFUN1, FINSET_1, FUNCT_4, RLVECT_5, ORDINAL2, BSPACE;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, DOMAIN_1, RELSET_1,
FUNCT_1, ORDINAL1, NUMBERS, NAT_1, INT_1, PARTFUN1, FUNCT_2, BINOP_1,
FUNCT_7, XXREAL_0, CARD_1, FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQOP,
CARD_2, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, VECTSP_6,
VECTSP_7, MATRLIN, VECTSP_9, INT_3, RANKNULL;
constructors FINSEQOP, VECTSP_7, VECTSP_9, REALSET1, WELLORD2, NAT_D, FUNCT_7,
CARD_2, RANKNULL, INT_3, GR_CY_1, RELSET_1, BINOP_2, BINOP_1;
registrations STRUCT_0, CARD_1, FINSET_1, FINSEQ_1, SUBSET_1, XBOOLE_0,
VECTSP_1, ORDINAL1, XREAL_0, INT_1, VECTSP_7, RELSET_1;
requirements NUMERALS, BOOLE, ARITHM, SUBSET, REAL;
begin
definition
let S be 1-sorted;
func <*>S -> FinSequence of S equals
:: BSPACE:def 1
<*>([#]S);
end;
:: exactly as in FINSEQ_2
reserve S for 1-sorted,
i for Element of NAT,
p for FinSequence,
X for set;
:: copied from FINSEQ_2:13
theorem :: BSPACE:1
for p being FinSequence of S st i in dom p holds p.i in S;
:: copied from FINSEQ_2:14
theorem :: BSPACE:2
(for i being Nat st i in dom p holds p.i in S) implies p is FinSequence of S;
scheme :: BSPACE:sch 1
IndSeqS{S() -> 1-sorted, P[set]}: for p being FinSequence of S() holds P[p]
provided
P[<*> S()] and
for p being FinSequence of S() for x being Element of S() st P[p]
holds P[p^<*x*>];
begin :: The two-element field Z_2
definition
func Z_2 -> Field equals
:: BSPACE:def 2
INT.Ring(2);
end;
theorem :: BSPACE:3
[#]Z_2 = {0,1};
theorem :: BSPACE:4
for a being Element of Z_2 holds a = 0 or a = 1;
theorem :: BSPACE:5
0.Z_2 = 0;
theorem :: BSPACE:6
1.Z_2 = 1;
theorem :: BSPACE:7
1.Z_2 + 1.Z_2 = 0.Z_2;
theorem :: BSPACE:8
for x being Element of Z_2 holds x = 0.Z_2 iff x <> 1.Z_2;
begin :: Set-theoretical Preliminaries
definition
let X be set,x be object;
func X@x -> Element of Z_2 equals
:: BSPACE:def 3
1.Z_2 if x in X otherwise 0.Z_2;
end;
theorem :: BSPACE:9
for X,x being set holds X@x = 1.Z_2 iff x in X;
theorem :: BSPACE:10
for X,x being set holds X@x = 0.Z_2 iff not x in X;
theorem :: BSPACE:11
for X,x being set holds X@x <> 0.Z_2 iff X@x = 1.Z_2;
theorem :: BSPACE:12
for X,x,y being set holds X@x = X@y iff (x in X iff y in X);
theorem :: BSPACE:13
for X,Y,x being set holds X@x = Y@x iff (x in X iff x in Y);
theorem :: BSPACE:14
for x being set holds {}@x = 0.Z_2;
theorem :: BSPACE:15
for X being set, u,v being Subset of X, x being Element of X
holds (u \+\ v)@x = u@x + v@x;
theorem :: BSPACE:16
for X,Y being set holds X = Y iff for x being object holds X@x = Y@x;
begin :: The Boolean Bector Space of Subsets of a Set
definition
let X be set, a be Element of Z_2, c be Subset of X;
func a \*\ c -> Subset of X equals
:: BSPACE:def 4
c if a = 1.Z_2, {}X if a = 0.Z_2;
end;
definition
let X be set;
func bspace-sum(X) -> BinOp of bool X means
:: BSPACE:def 5
for c,d being Subset of X holds it.(c,d) = c \+\ d;
end;
theorem :: BSPACE:17
for a being Element of Z_2, c,d being Subset of X holds a \*\ (c
\+\ d) = (a \*\ c) \+\ (a \*\ d);
theorem :: BSPACE:18
for a,b being Element of Z_2, c being Subset of X holds (a+b)
\*\ c = (a \*\ c) \+\ (b \*\ c);
theorem :: BSPACE:19
for c being Subset of X holds (1.Z_2) \*\ c = c;
theorem :: BSPACE:20
for a,b being Element of Z_2, c being Subset of X holds a \*\ (b
\*\ c) = (a*b) \*\ c;
definition
let X be set;
func bspace-scalar-mult(X) -> Function of [:the carrier of Z_2,bool X:],bool
X means
:: BSPACE:def 6
for a being Element of Z_2, c being Subset of X holds it.(a,c) = a \*\ c;
end;
definition
let X be set;
func bspace(X) -> non empty ModuleStr over Z_2 equals
:: BSPACE:def 7
ModuleStr (# bool X,
bspace-sum(X), {}X, bspace-scalar-mult(X) #);
end;
theorem :: BSPACE:21
bspace(X) is Abelian;
theorem :: BSPACE:22
bspace(X) is add-associative;
theorem :: BSPACE:23
bspace(X) is right_zeroed;
theorem :: BSPACE:24
bspace(X) is right_complementable;
theorem :: BSPACE:25
for a being Element of Z_2, x,y being Element of bspace(X) holds
a*(x+y) = (a*x)+(a*y);
theorem :: BSPACE:26
for a,b being Element of Z_2, x being Element of bspace(X) holds
(a+b)*x = (a*x)+(b*x);
theorem :: BSPACE:27
for a,b being Element of Z_2, x being Element of bspace(X) holds
(a*b)*x = a*(b*x);
theorem :: BSPACE:28
for x being Element of bspace(X) holds (1_Z_2)*x = x;
theorem :: BSPACE:29
bspace(X) is vector-distributive scalar-distributive
scalar-associative scalar-unital;
registration
let X be set;
cluster bspace(X) -> vector-distributive scalar-distributive
scalar-associative scalar-unital
Abelian right_complementable
add-associative right_zeroed;
end;
begin :: The Linear Independence and Linear Span of 1-element Subsets
definition
let X be set;
func singletons(X) -> set equals
:: BSPACE:def 8
{ f where f is Subset of X : f is 1-element };
end;
definition
let X be set;
redefine func singletons(X) -> Subset of bspace(X);
end;
registration
let X be non empty set;
cluster singletons(X) -> non empty;
end;
theorem :: BSPACE:30
for X being non empty set, f being Subset of X st f is Element
of singletons(X) holds f is 1-element;
definition
let F be Field, V be VectSp of F, l be Linear_Combination of V, x be Element
of V;
redefine func l.x -> Element of F;
end;
definition
let X be non empty set, s be FinSequence of bspace(X), x be Element of X;
func s@x -> FinSequence of Z_2 means
:: BSPACE:def 9
len it = len s & for j being Nat st 1 <= j & j <= len s holds it.j = (s.j)@x;
end;
theorem :: BSPACE:31
for X being non empty set, x being Element of X holds (<*>(
bspace(X)))@x = <*>Z_2;
theorem :: BSPACE:32
for X being set, u,v being Element of bspace(X), x being Element
of X holds (u + v)@x = u@x + v@x;
theorem :: BSPACE:33
for X being non empty set, s being FinSequence of bspace(X), f
being Element of bspace(X), x being Element of X holds (s ^ <*f*>)@x = (s@x) ^
<*f@x*>;
theorem :: BSPACE:34
for X being non empty set, s being FinSequence of bspace(X), x
being Element of X holds (Sum s)@x = Sum (s@x);
theorem :: BSPACE:35
for X being non empty set, l being Linear_Combination of bspace(
X), x being Element of bspace(X) st x in Carrier l holds l.x = 1_Z_2;
registration let X be empty set;
cluster singletons X -> empty;
end;
theorem :: BSPACE:36
singletons(X) is linearly-independent;
theorem :: BSPACE:37
for f being Element of bspace(X) st (ex x being set st x in X & f = {x
}) holds f in singletons(X);
theorem :: BSPACE:38
for X being finite set, A being Subset of X ex l being
Linear_Combination of singletons(X) st Sum l = A;
theorem :: BSPACE:39
for X being finite set holds Lin(singletons(X)) = bspace(X);
theorem :: BSPACE:40
for X being finite set holds singletons(X) is Basis of bspace(X);
registration
let X be finite set;
cluster singletons(X) -> finite;
end;
registration
let X be finite set;
cluster bspace(X) -> finite-dimensional;
end;
theorem :: BSPACE:41
card (singletons X) = card X;
theorem :: BSPACE:42
card [#](bspace X) = exp(2,card(X));
theorem :: BSPACE:43
dim bspace {} = 0;