environ
vocabularies HIDDEN, NUMBERS, NAT_1, ARYTM_3, XXREAL_0, ARYTM_1, FINSET_1, CARD_1, SUBSET_1, TARSKI, XBOOLE_0, VECTSP_1, RLSUB_1, STRUCT_0, SUPINF_2, RLSUB_2, RLVECT_5, SETFAM_1, ZFMISC_1, RLVECT_3, RELAT_1, PRE_TOPC, PENCIL_1, PENCIL_4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, SETFAM_1, DOMAIN_1, STRUCT_0, FINSET_1, PRE_TOPC, PENCIL_1, RLVECT_1, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_7, MATRLIN, VECTSP_9;
definitions TARSKI, XBOOLE_0, PENCIL_1, VECTSP_4;
theorems XBOOLE_0, ZFMISC_1, NAT_1, TARSKI, PENCIL_1, CARD_1, XBOOLE_1, CARD_2, SUBSET_1, VECTSP_5, VECTSP_9, VECTSP_4, RLVECT_1, VECTSP_7, VECTSP10, VECTSP_1, EULER_1, XREAL_1, XXREAL_0, ORDINAL1, NAT_D, FINSEQ_4;
schemes XBOOLE_0, SUBSET_1;
registrations SUBSET_1, FINSET_1, XXREAL_0, XREAL_0, STRUCT_0, MATRLIN, VECTSP_9, PENCIL_1, ORDINAL1, CARD_1, NAT_1;
constructors HIDDEN, REALSET1, VECTSP_5, VECTSP_7, VECTSP_9, PENCIL_1, NAT_D;
requirements HIDDEN, REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
equalities XBOOLE_0, STRUCT_0, VECTSP_4, RLVECT_1, CARD_1, ORDINAL1;
expansions TARSKI, XBOOLE_0, STRUCT_0, PENCIL_1;
theorem Th1:
for
k,
n being
Nat st
k < n & 3
<= n & not
k + 1
< n holds
2
<= k
Lm1:
for X being finite set
for n being Nat st n <= card X holds
ex Y being Subset of X st card Y = n
by FINSEQ_4:72;
definition
let F be
Field;
let V be
finite-dimensional VectSp of
F;
let k be
Nat;
existence
ex b1 being Subset-Family of (k Subspaces_of V) st
for X being set holds
( X in b1 iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) )
uniqueness
for b1, b2 being Subset-Family of (k Subspaces_of V) st ( for X being set holds
( X in b1 iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) ) ) & ( for X being set holds
( X in b2 iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) ) ) holds
b1 = b2
end;
definition
let X be
set ;
existence
ex b1 being set st
for z being set holds
( z in b1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) )
uniqueness
for b1, b2 being set st ( for z being set holds
( z in b1 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ) & ( for z being set holds
( z in b2 iff ex x, y being set st
( x in X & y in X & z = {x,y} ) ) ) holds
b1 = b2
end;