:: Spaces of Pencils, {G}rassmann Spaces, and Generalized {V}eronese Spaces
:: by Adam Naumowicz
::
:: Received November 8, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem Th1: :: PENCIL_4:1
for k, n being Nat st k < n &amp; 3 <= n &amp; not k + 1 < n holds
2 <= k
proofend;

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;

theorem Th2: :: PENCIL_4:2
for F being Field
for V being VectSp of F
for W being Subspace of V holds W is Subspace of (Omega). V
proofend;

theorem Th3: :: PENCIL_4:3
for F being Field
for V being VectSp of F
for W being Subspace of (Omega). V holds W is Subspace of V
proofend;

theorem Th4: :: PENCIL_4:4
for F being Field
for V being VectSp of F
for W being Subspace of V holds (Omega). W is Subspace of V
proofend;

theorem Th5: :: PENCIL_4:5
for F being Field
for V, W being VectSp of F st (Omega). W is Subspace of V holds
W is Subspace of V
proofend;

definition
let F be Field;
let V be VectSp of F;
let W1, W2 be Subspace of V;
func segment (W1,W2) ->  Subset of (Subspaces V) means :Def1: :: PENCIL_4:def 1
 for W being strict Subspace of V holds
( W in it iff ( W1 is Subspace of W &amp; W is Subspace of W2 ) ) if W1 is Subspace of W2
otherwise it = {} ;
consistency
 for b1 being Subset of (Subspaces V) holds verum ;
existence
 ( ( W1 is Subspace of W2 implies ex b1 being Subset of (Subspaces V) st
for W being strict Subspace of V holds
( W in b1 iff ( W1 is Subspace of W &amp; W is Subspace of W2 ) ) ) &amp; ( W1 is not Subspace of W2 implies ex b1 being Subset of (Subspaces V) st b1 = {} ) )
proofend;
uniqueness
 for b1, b2 being Subset of (Subspaces V) holds
( ( W1 is Subspace of W2 &amp; ( for W being strict Subspace of V holds
( W in b1 iff ( W1 is Subspace of W &amp; W is Subspace of W2 ) ) ) &amp; ( for W being strict Subspace of V holds
( W in b2 iff ( W1 is Subspace of W &amp; W is Subspace of W2 ) ) ) implies b1 = b2 ) &amp; ( W1 is not Subspace of W2 &amp; b1 = {} &amp; b2 = {} implies b1 = b2 ) )
proofend;
end;

:: deftheorem Def1 defines segment PENCIL_4:def_1_:_
 for F being Field
for V being VectSp of F
for W1, W2 being Subspace of V
for b5 being Subset of (Subspaces V) holds
( ( W1 is Subspace of W2 implies ( b5 = segment (W1,W2) iff for W being strict Subspace of V holds
( W in b5 iff ( W1 is Subspace of W &amp; W is Subspace of W2 ) ) ) ) &amp; ( W1 is not Subspace of W2 implies ( b5 = segment (W1,W2) iff b5 = {} ) ) );

theorem Th6: :: PENCIL_4:6
for F being Field
for V being VectSp of F
for W1, W2, W3, W4 being Subspace of V st W1 is Subspace of W2 &amp; W3 is Subspace of W4 &amp; (Omega). W1 = (Omega). W3 &amp; (Omega). W2 = (Omega). W4 holds
segment (W1,W2) = segment (W3,W4)
proofend;

definition
let F be Field;
let V be VectSp of F;
let W1, W2 be Subspace of V;
func pencil (W1,W2) ->  Subset of (Subspaces V) equals :: PENCIL_4:def 2
(segment (W1,W2)) \ {((Omega). W1),((Omega). W2)};
coherence
 (segment (W1,W2)) \ {((Omega). W1),((Omega). W2)} is Subset of (Subspaces V) ;
end;

:: deftheorem  defines pencil PENCIL_4:def_2_:_
 for F being Field
for V being VectSp of F
for W1, W2 being Subspace of V holds pencil (W1,W2) = (segment (W1,W2)) \ {((Omega). W1),((Omega). W2)};

theorem :: PENCIL_4:7
for F being Field
for V being VectSp of F
for W1, W2, W3, W4 being Subspace of V st W1 is Subspace of W2 &amp; W3 is Subspace of W4 &amp; (Omega). W1 = (Omega). W3 &amp; (Omega). W2 = (Omega). W4 holds
pencil (W1,W2) = pencil (W3,W4) by Th6;

definition
let F be Field;
let V be finite-dimensional VectSp of F;
let W1, W2 be Subspace of V;
let k be Nat;
func pencil (W1,W2,k) ->  Subset of (k Subspaces_of V) equals :: PENCIL_4:def 3
(pencil (W1,W2)) /\ (k Subspaces_of V);
coherence
 (pencil (W1,W2)) /\ (k Subspaces_of V) is Subset of (k Subspaces_of V) by XBOOLE_1:17;
end;

:: deftheorem  defines pencil PENCIL_4:def_3_:_
 for F being Field
for V being finite-dimensional VectSp of F
for W1, W2 being Subspace of V
for k being Nat holds pencil (W1,W2,k) = (pencil (W1,W2)) /\ (k Subspaces_of V);

theorem Th8: :: PENCIL_4:8
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat
for W1, W2, W being Subspace of V st W in pencil (W1,W2,k) holds
( W1 is Subspace of W &amp; W is Subspace of W2 )
proofend;

theorem :: PENCIL_4:9
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat
for W1, W2, W3, W4 being Subspace of V st W1 is Subspace of W2 &amp; W3 is Subspace of W4 &amp; (Omega). W1 = (Omega). W3 &amp; (Omega). W2 = (Omega). W4 holds
pencil (W1,W2,k) = pencil (W3,W4,k) by Th6;

definition
let F be Field;
let V be finite-dimensional VectSp of F;
let k be Nat;
funck Pencils_of V ->  Subset-Family of (k Subspaces_of V) means :Def4: :: PENCIL_4:def 4
 for X being set holds
( X in it iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 &amp; (dim W1) + 1 = k &amp; dim W2 = k + 1 &amp; 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 &amp; (dim W1) + 1 = k &amp; dim W2 = k + 1 &amp; X = pencil (W1,W2,k) ) )
proofend;
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 &amp; (dim W1) + 1 = k &amp; dim W2 = k + 1 &amp; X = pencil (W1,W2,k) ) ) ) &amp; ( for X being set holds
( X in b2 iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 &amp; (dim W1) + 1 = k &amp; dim W2 = k + 1 &amp; X = pencil (W1,W2,k) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines Pencils_of PENCIL_4:def_4_:_
 for F being Field
for V being finite-dimensional VectSp of F
for k being Nat
for b4 being Subset-Family of (k Subspaces_of V) holds
( b4 = k Pencils_of V iff for X being set holds
( X in b4 iff ex W1, W2 being Subspace of V st
( W1 is Subspace of W2 &amp; (dim W1) + 1 = k &amp; dim W2 = k + 1 &amp; X = pencil (W1,W2,k) ) ) );

theorem Th10: :: PENCIL_4:10
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k &amp; k < dim V holds
not k Pencils_of V is empty
proofend;

theorem Th11: :: PENCIL_4:11
for F being Field
for V being finite-dimensional VectSp of F
for W1, W2, P, Q being Subspace of V
for k being Nat st (dim W1) + 1 = k &amp; dim W2 = k + 1 &amp; P in pencil (W1,W2,k) &amp; Q in pencil (W1,W2,k) &amp; P <> Q holds
( P /\ Q = (Omega). W1 &amp; P + Q = (Omega). W2 )
proofend;

theorem Th12: :: PENCIL_4:12
for F being Field
for V being finite-dimensional VectSp of F
for v being Vector of V st v <> 0. V holds
dim (Lin {v}) = 1
proofend;

theorem Th13: :: PENCIL_4:13
for F being Field
for V being finite-dimensional VectSp of F
for W being Subspace of V
for v being Vector of V st not v in W holds
dim (W + (Lin {v})) = (dim W) + 1
proofend;

theorem Th14: :: PENCIL_4:14
for F being Field
for V being finite-dimensional VectSp of F
for W being Subspace of V
for v, u being Vector of V st v <> u &amp; {v,u} is linearly-independent &amp; W /\ (Lin {v,u}) = (0). V holds
dim (W + (Lin {v,u})) = (dim W) + 2
proofend;

theorem Th15: :: PENCIL_4:15
for F being Field
for V being finite-dimensional VectSp of F
for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k &amp; dim W2 = k + 1 holds
for v being Vector of V st v in W2 &amp; not v in W1 holds
W1 + (Lin {v}) in pencil (W1,W2,k)
proofend;

theorem Th16: :: PENCIL_4:16
for F being Field
for V being finite-dimensional VectSp of F
for W1, W2 being Subspace of V st W1 is Subspace of W2 holds
for k being Nat st (dim W1) + 1 = k &amp; dim W2 = k + 1 holds
not pencil (W1,W2,k) is trivial
proofend;

definition
let F be Field;
let V be finite-dimensional VectSp of F;
let k be Nat;
func PencilSpace (V,k) ->  strict TopStruct  equals :: PENCIL_4:def 5
 TopStruct(# (k Subspaces_of V),(k Pencils_of V) #);
coherence
 TopStruct(# (k Subspaces_of V),(k Pencils_of V) #) is strict TopStruct ;
end;

:: deftheorem  defines PencilSpace PENCIL_4:def_5_:_
 for F being Field
for V being finite-dimensional VectSp of F
for k being Nat holds PencilSpace (V,k) = TopStruct(# (k Subspaces_of V),(k Pencils_of V) #);

theorem Th17: :: PENCIL_4:17
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k &amp; k < dim V holds
not PencilSpace (V,k) is void
proofend;

theorem Th18: :: PENCIL_4:18
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k &amp; k < dim V &amp; 3 <= dim V holds
not PencilSpace (V,k) is degenerated
proofend;

theorem Th19: :: PENCIL_4:19
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k &amp; k < dim V holds
PencilSpace (V,k) is with_non_trivial_blocks
proofend;

theorem Th20: :: PENCIL_4:20
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k &amp; k < dim V holds
PencilSpace (V,k) is identifying_close_blocks
proofend;

theorem :: PENCIL_4:21
for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k &amp; k < dim V &amp; 3 <= dim V holds
PencilSpace (V,k) is PLS by Th17, Th18, Th19, Th20, VECTSP_9:36;

begin

definition
let F be Field;
let V be finite-dimensional VectSp of F;
let m, n be Nat;
func SubspaceSet (V,m,n) ->  Subset-Family of (m Subspaces_of V) means :Def6: :: PENCIL_4:def 6
 for X being set holds
( X in it iff ex W being Subspace of V st
( dim W = n &amp; X = m Subspaces_of W ) );
existence
 ex b1 being Subset-Family of (m Subspaces_of V) st
for X being set holds
( X in b1 iff ex W being Subspace of V st
( dim W = n &amp; X = m Subspaces_of W ) )
proofend;
uniqueness
 for b1, b2 being Subset-Family of (m Subspaces_of V) st ( for X being set holds
( X in b1 iff ex W being Subspace of V st
( dim W = n &amp; X = m Subspaces_of W ) ) ) &amp; ( for X being set holds
( X in b2 iff ex W being Subspace of V st
( dim W = n &amp; X = m Subspaces_of W ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines SubspaceSet PENCIL_4:def_6_:_
 for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat
for b5 being Subset-Family of (m Subspaces_of V) holds
( b5 = SubspaceSet (V,m,n) iff for X being set holds
( X in b5 iff ex W being Subspace of V st
( dim W = n &amp; X = m Subspaces_of W ) ) );

theorem Th22: :: PENCIL_4:22
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat st n <= dim V holds
not SubspaceSet (V,m,n) is empty
proofend;

theorem Th23: :: PENCIL_4:23
for F being Field
for W1, W2 being finite-dimensional VectSp of F st (Omega). W1 = (Omega). W2 holds
for m being Nat holds m Subspaces_of W1 = m Subspaces_of W2
proofend;

theorem Th24: :: PENCIL_4:24
for F being Field
for V being finite-dimensional VectSp of F
for W being Subspace of V
for m being Nat st 1 <= m &amp; m <= dim V &amp; m Subspaces_of V c= m Subspaces_of W holds
(Omega). V = (Omega). W
proofend;

definition
let F be Field;
let V be finite-dimensional VectSp of F;
let m, n be Nat;
func GrassmannSpace (V,m,n) ->  strict TopStruct  equals :: PENCIL_4:def 7
 TopStruct(# (m Subspaces_of V),(SubspaceSet (V,m,n)) #);
coherence
 TopStruct(# (m Subspaces_of V),(SubspaceSet (V,m,n)) #) is strict TopStruct ;
end;

:: deftheorem  defines GrassmannSpace PENCIL_4:def_7_:_
 for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat holds GrassmannSpace (V,m,n) = TopStruct(# (m Subspaces_of V),(SubspaceSet (V,m,n)) #);

theorem Th25: :: PENCIL_4:25
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat st n <= dim V holds
not GrassmannSpace (V,m,n) is void
proofend;

theorem Th26: :: PENCIL_4:26
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat st 1 <= m &amp; m < n &amp; n < dim V holds
not GrassmannSpace (V,m,n) is degenerated
proofend;

theorem Th27: :: PENCIL_4:27
for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat st 1 <= m &amp; m < n &amp; n <= dim V holds
GrassmannSpace (V,m,n) is with_non_trivial_blocks
proofend;

theorem Th28: :: PENCIL_4:28
for F being Field
for V being finite-dimensional VectSp of F
for m being Nat st m + 1 <= dim V holds
GrassmannSpace (V,m,(m + 1)) is identifying_close_blocks
proofend;

theorem :: PENCIL_4:29
for F being Field
for V being finite-dimensional VectSp of F
for m being Nat st 1 <= m &amp; m + 1 < dim V holds
GrassmannSpace (V,m,(m + 1)) is PLS
proofend;

begin

definition
let X be set ;
func PairSet X ->  set  means :Def8: :: PENCIL_4:def 8
 for z being set holds
( z in it iff ex x, y being set st
( x in X &amp; y in X &amp; z = {x,y} ) );
existence
 ex b1 being set st
for z being set holds
( z in b1 iff ex x, y being set st
( x in X &amp; y in X &amp; z = {x,y} ) )
proofend;
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 &amp; y in X &amp; z = {x,y} ) ) ) &amp; ( for z being set holds
( z in b2 iff ex x, y being set st
( x in X &amp; y in X &amp; z = {x,y} ) ) ) holds
b1 = b2
proofend;
end;

:: 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 &amp; y in X &amp; z = {x,y} ) ) );

registration
let X be non empty set ;
cluster PairSet X ->  non empty ;
coherence
 not PairSet X is empty
proofend;
end;

definition
let t, X be set ;
func PairSet (t,X) ->  set  means :Def9: :: PENCIL_4:def 9
 for z being set holds
( z in it iff ex y being set st
( y in X &amp; z = {t,y} ) );
existence
 ex b1 being set st
for z being set holds
( z in b1 iff ex y being set st
( y in X &amp; z = {t,y} ) )
proofend;
uniqueness
 for b1, b2 being set st ( for z being set holds
( z in b1 iff ex y being set st
( y in X &amp; z = {t,y} ) ) ) &amp; ( for z being set holds
( z in b2 iff ex y being set st
( y in X &amp; z = {t,y} ) ) ) holds
b1 = b2
proofend;
end;

:: 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 &amp; z = {t,y} ) ) );

registration
let t be set ;
let X be non empty set ;
cluster PairSet (t,X) ->  non empty ;
coherence
 not PairSet (t,X) is empty
proofend;
end;

registration
let t be set ;
let X be non trivial set ;
cluster PairSet (t,X) ->  non trivial ;
coherence
 not PairSet (t,X) is trivial
proofend;
end;

definition
let X be set ;
let L be Subset-Family of X;
func PairSetFamily L ->  Subset-Family of (PairSet X) means :Def10: :: PENCIL_4:def 10
 for S being set holds
( S in it iff ex t being set ex l being Subset of X st
( t in X &amp; l in L &amp; S = PairSet (t,l) ) );
existence
 ex b1 being Subset-Family of (PairSet X) st
for S being set holds
( S in b1 iff ex t being set ex l being Subset of X st
( t in X &amp; l in L &amp; S = PairSet (t,l) ) )
proofend;
uniqueness
 for b1, b2 being Subset-Family of (PairSet X) st ( for S being set holds
( S in b1 iff ex t being set ex l being Subset of X st
( t in X &amp; l in L &amp; S = PairSet (t,l) ) ) ) &amp; ( for S being set holds
( S in b2 iff ex t being set ex l being Subset of X st
( t in X &amp; l in L &amp; S = PairSet (t,l) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines PairSetFamily PENCIL_4:def_10_:_
 for X being set
for L being Subset-Family of X
for b3 being Subset-Family of (PairSet X) holds
( b3 = PairSetFamily L iff for S being set holds
( S in b3 iff ex t being set ex l being Subset of X st
( t in X &amp; l in L &amp; S = PairSet (t,l) ) ) );

registration
let X be non empty set ;
let L be non empty Subset-Family of X;
cluster PairSetFamily L ->  non empty ;
coherence
 not PairSetFamily L is empty
proofend;
end;

definition
let S be TopStruct ;
func VeroneseSpace S ->  strict TopStruct  equals :: PENCIL_4:def 11
 TopStruct(# (PairSet the carrier of S),(PairSetFamily the topology of S) #);
coherence
 TopStruct(# (PairSet the carrier of S),(PairSetFamily the topology of S) #) is strict TopStruct ;
end;

:: deftheorem  defines VeroneseSpace PENCIL_4:def_11_:_
 for S being TopStruct holds VeroneseSpace S = TopStruct(# (PairSet the carrier of S),(PairSetFamily the topology of S) #);

registration
let S be non empty TopStruct ;
cluster VeroneseSpace S ->  non empty strict ;
coherence
 not VeroneseSpace S is empty ;
end;

registration
let S be non empty non void TopStruct ;
cluster VeroneseSpace S ->  strict non void ;
coherence
 not VeroneseSpace S is void
proofend;
end;

registration
let S be non empty non void non degenerated TopStruct ;
cluster VeroneseSpace S ->  strict non degenerated ;
coherence
 not VeroneseSpace S is degenerated
proofend;
end;

registration
let S be non empty non void with_non_trivial_blocks TopStruct ;
cluster VeroneseSpace S ->  strict with_non_trivial_blocks ;
coherence
 VeroneseSpace S is with_non_trivial_blocks
proofend;
end;

registration
let S be identifying_close_blocks TopStruct ;
cluster VeroneseSpace S ->  strict identifying_close_blocks ;
coherence
 VeroneseSpace S is identifying_close_blocks
proofend;
end;