:: PENCIL_4 semantic presentation

theorem Th1: :: PENCIL_4:1

for k, n being Nat st 1 <= k & k < n & 3 <= n & not k + 1 < n holds
2 <= k

proof end;

theorem Th2: :: PENCIL_4:2

for X being finite set
for n being Nat st n <= card X holds
ex Y being Subset of X st card Y = n

proof end;

theorem Th3: :: PENCIL_4:3

for F being Field
for V being VectSp of F
for W being Subspace of V holds W is Subspace of (Omega). V

proof end;

theorem Th4: :: PENCIL_4:4

for F being Field
for V being VectSp of F
for W being Subspace of (Omega). V holds W is Subspace of V

proof end;

theorem Th5: :: PENCIL_4:5

for F being Field
for V being VectSp of F
for W being Subspace of V holds (Omega). W is Subspace of V

proof end;

theorem Th6: :: PENCIL_4:6

for F being Field
for V, W being VectSp of F st (Omega). W is Subspace of V holds
W is Subspace of V

proof end;

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 & W is Subspace of W2 ) ) if W1 is Subspace of W2
otherwise it = {} ;
consistency ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines segment PENCIL_4:def 1 :

theorem Th7: :: 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 & W3 is Subspace of W4 & (Omega). W1 = (Omega). W3 & (Omega). W2 = (Omega). W4 holds
segment W1,W2 = segment W3,W4

proof end;

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

proof end;

end;

:: deftheorem defines pencil PENCIL_4:def 2 :

theorem Th8: :: PENCIL_4:8

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 & W3 is Subspace of W4 & (Omega). W1 = (Omega). W3 & (Omega). W2 = (Omega). W4 holds
pencil W1,W2 = pencil W3,W4 by Th7;

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 by XBOOLE_1:17;

end;

:: deftheorem defines pencil PENCIL_4:def 3 :

theorem Th9: :: PENCIL_4:9

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 & W is Subspace of W2 )

proof end;

theorem Th10: :: PENCIL_4:10

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 & W3 is Subspace of W4 & (Omega). W1 = (Omega). W3 & (Omega). W2 = (Omega). W4 holds
pencil W1,W2,k = pencil W3,W4,k by Th8;

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: :: 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 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil W1,W2,k ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Pencils_of PENCIL_4:def 4 :

theorem Th11: :: PENCIL_4:11

for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
not k Pencils_of V is empty

proof end;

theorem Th12: :: PENCIL_4:12

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 1 <= k & k < dim V & (dim W1) + 1 = k & dim W2 = k + 1 & P in pencil W1,W2,k & Q in pencil W1,W2,k & P <> Q holds
( P /\ Q = (Omega). W1 & P + Q = (Omega). W2 )

proof end;

theorem Th13: :: PENCIL_4:13

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

proof end;

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 being Vector of V st not v in W holds
dim (W + (Lin {v})) = (dim W) + 1

proof end;

theorem Th15: :: PENCIL_4:15

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 not v in W & not u in W & v <> u & {v,u} is linearly-independent & W /\ (Lin {v,u}) = (0). V holds
dim (W + (Lin {v,u})) = (dim W) + 2

proof end;

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 1 <= k & k < dim V & (dim W1) + 1 = k & dim W2 = k + 1 holds
for v being Vector of V st v in W2 & not v in W1 holds
W1 + (Lin {v}) in pencil W1,W2,k

proof end;

theorem Th17: :: PENCIL_4:17

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 1 <= k & k < dim V & (dim W1) + 1 = k & dim W2 = k + 1 holds
not pencil W1,W2,k is trivial

proof end;

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 ;

end;

:: deftheorem defines PencilSpace PENCIL_4:def 5 :

theorem Th18: :: PENCIL_4:18

for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st k <= dim V holds
not PencilSpace V,k is empty

proof end;

theorem Th19: :: PENCIL_4:19

for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
not PencilSpace V,k is void

proof end;

theorem Th20: :: PENCIL_4:20

for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V & 3 <= dim V holds
not PencilSpace V,k is degenerated

proof end;

theorem Th21: :: PENCIL_4:21

for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
PencilSpace V,k is with_non_trivial_blocks

proof end;

theorem Th22: :: PENCIL_4:22

for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V holds
PencilSpace V,k is identifying_close_blocks

proof end;

theorem :: PENCIL_4:23

for F being Field
for V being finite-dimensional VectSp of F
for k being Nat st 1 <= k & k < dim V & 3 <= dim V holds
PencilSpace V,k is PLS by Th18, Th19, Th20, Th21, Th22;

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 & X = m Subspaces_of W ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines SubspaceSet PENCIL_4:def 6 :

theorem Th24: :: PENCIL_4:24

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

proof end;

theorem Th25: :: PENCIL_4:25

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

proof end;

theorem Th26: :: PENCIL_4:26

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 & m <= dim V & m Subspaces_of V c= m Subspaces_of W holds
(Omega). V = (Omega). W

proof end;

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 ;

end;

:: deftheorem defines GrassmannSpace PENCIL_4:def 7 :

theorem Th27: :: PENCIL_4:27

for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat st m <= dim V holds
not GrassmannSpace V,m,n is empty

proof end;

theorem Th28: :: PENCIL_4:28

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

proof end;

theorem Th29: :: PENCIL_4:29

for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat st 1 <= m & m < n & n < dim V holds
not GrassmannSpace V,m,n is degenerated

proof end;

theorem Th30: :: PENCIL_4:30

for F being Field
for V being finite-dimensional VectSp of F
for m, n being Nat st 1 <= m & m < n & n <= dim V holds
GrassmannSpace V,m,n is with_non_trivial_blocks

proof end;

theorem Th31: :: PENCIL_4:31

for F being Field
for V being finite-dimensional VectSp of F
for m being Nat st 1 <= m & m + 1 <= dim V holds
GrassmannSpace V,m,(m + 1) is identifying_close_blocks

proof end;

theorem :: PENCIL_4:32

for F being Field
for V being finite-dimensional VectSp of F
for m being Nat st 1 <= m & m + 1 < dim V holds
GrassmannSpace V,m,(m + 1) is PLS

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines PairSet PENCIL_4:def 8 :

registration

let X be non empty set ;
cluster PairSet X -> non empty ;
coherence

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines PairSet PENCIL_4:def 9 :

registration

let t be set ;
let X be non empty set ;
cluster PairSet t,X -> non empty ;
coherence

proof end;

end;

registration

let t be set ;
let X be non trivial set ;
cluster PairSet t,X -> non empty non trivial ;
coherence

proof end;

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 & l in L & S = PairSet t,l ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines PairSetFamily PENCIL_4:def 10 :

registration

let X be non empty set ;
let L be non empty Subset-Family of X;
cluster PairSetFamily L -> non empty ;
coherence

proof end;

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 ;

end;

:: deftheorem defines VeroneseSpace PENCIL_4:def 11 :

registration

let S be non empty TopStruct ;
cluster VeroneseSpace S -> non empty strict ;
coherence

proof end;

end;

registration

let S be non empty non void TopStruct ;
cluster VeroneseSpace S -> non empty strict non void ;
coherence

proof end;

end;

registration

let S be non empty non void non degenerated TopStruct ;
cluster VeroneseSpace S -> non empty strict non void non degenerated ;
coherence

proof end;

end;

registration

let S be non empty non void with_non_trivial_blocks TopStruct ;
cluster VeroneseSpace S -> non empty strict non void with_non_trivial_blocks ;
coherence

proof end;

end;

registration

let S be identifying_close_blocks TopStruct ;
cluster VeroneseSpace S -> strict identifying_close_blocks ;
coherence

proof end;

end;

definition

let S be PLS;
:: original: VeroneseSpace
redefine func VeroneseSpace S -> strict PLS;
coherence ;

end;