begin
theorem Th1:
for
k,
n being
Nat st
k < n & 3
<= n & not
k + 1
< n holds
2
<= k
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
:: deftheorem Def1 defines segment PENCIL_4:def 1 :
theorem Th7:
:: deftheorem defines pencil PENCIL_4:def 2 :
theorem
:: deftheorem defines pencil PENCIL_4:def 3 :
theorem Th9:
theorem
definition
let F be
Field;
let V be
finite-dimensional VectSp of
F;
let k be
Nat;
func k Pencils_of V -> Subset-Family of
(k Subspaces_of V) means :
Def4:
for
X being
set holds
(
X in it 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 ) );
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;
:: deftheorem Def4 defines Pencils_of PENCIL_4:def 4 :
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
:: deftheorem defines PencilSpace PENCIL_4:def 5 :
theorem
canceled;
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
begin
:: deftheorem Def6 defines SubspaceSet PENCIL_4:def 6 :
theorem Th24:
theorem Th25:
theorem Th26:
:: deftheorem defines GrassmannSpace PENCIL_4:def 7 :
theorem
canceled;
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem
begin
:: deftheorem Def8 defines PairSet PENCIL_4:def 8 :
for
X being
set for
b2 being
set holds
(
b2 = PairSet X iff for
z being
set holds
(
z in b2 iff ex
x,
y being
set st
(
x in X &
y in X &
z = {x,y} ) ) );
:: deftheorem Def9 defines PairSet PENCIL_4:def 9 :
for
t,
X being
set for
b3 being
set holds
(
b3 = PairSet t,
X iff for
z being
set holds
(
z in b3 iff ex
y being
set st
(
y in X &
z = {t,y} ) ) );
:: deftheorem Def10 defines PairSetFamily PENCIL_4:def 10 :
:: deftheorem defines VeroneseSpace PENCIL_4:def 11 :