:: by Adam Naumowicz

::

:: Received November 8, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

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

for V being VectSp of F

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

proof end;

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

for V being VectSp of F

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

proof end;

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

for V being VectSp of F

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

proof end;

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

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;

for b_{1} being Subset of (Subspaces V) holds verum
;

existence

( ( W1 is Subspace of W2 implies ex b_{1} being Subset of (Subspaces V) st

for W being strict Subspace of V holds

( W in b_{1} iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( W1 is not Subspace of W2 implies ex b_{1} being Subset of (Subspaces V) st b_{1} = {} ) )

for b_{1}, b_{2} being Subset of (Subspaces V) holds

( ( W1 is Subspace of W2 & ( for W being strict Subspace of V holds

( W in b_{1} iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) & ( for W being strict Subspace of V holds

( W in b_{2} iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) implies b_{1} = b_{2} ) & ( W1 is not Subspace of W2 & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )

end;
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 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 = {} ;

for b

existence

( ( W1 is Subspace of W2 implies ex b

for W being strict Subspace of V holds

( W in b

proof end;

uniqueness for b

( ( W1 is Subspace of W2 & ( for W being strict Subspace of V holds

( W in b

( W in b

proof 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 b_{5} being Subset of (Subspaces V) holds

( ( W1 is Subspace of W2 implies ( b_{5} = segment (W1,W2) iff for W being strict Subspace of V holds

( W in b_{5} iff ( W1 is Subspace of W & W is Subspace of W2 ) ) ) ) & ( W1 is not Subspace of W2 implies ( b_{5} = segment (W1,W2) iff b_{5} = {} ) ) );

for F being Field

for V being VectSp of F

for W1, W2 being Subspace of V

for b

( ( W1 is Subspace of W2 implies ( b

( W in b

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

segment (W1,W2) = segment (W3,W4)

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;

(segment (W1,W2)) \ {((Omega). W1),((Omega). W2)} is Subset of (Subspaces V) ;

end;
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)};

(segment (W1,W2)) \ {((Omega). W1),((Omega). W2)} is Subset of (Subspaces V) ;

:: 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)};

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

definition

let F be Field;

let V be finite-dimensional VectSp of F;

let W1, W2 be Subspace of V;

let k be Nat;

(pencil (W1,W2)) /\ (k Subspaces_of V) is Subset of (k Subspaces_of V) by XBOOLE_1:17;

end;
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);

(pencil (W1,W2)) /\ (k Subspaces_of V) is Subset of (k Subspaces_of V) by XBOOLE_1:17;

:: 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);

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

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 :: PENCIL_4:9

definition

let F be Field;

let V be finite-dimensional VectSp of F;

let k be Nat;

ex b_{1} being Subset-Family of (k Subspaces_of V) st

for X being set holds

( X in b_{1} 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 b_{1}, b_{2} being Subset-Family of (k Subspaces_of V) st ( for X being set holds

( X in b_{1} 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 b_{2} 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

b_{1} = b_{2}

end;
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 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) ) );

ex b

for X being set holds

( X in b

( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) )

proof end;

uniqueness for b

( X in b

( 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 b

( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & X = pencil (W1,W2,k) ) ) ) holds

b

proof 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 b_{4} being Subset-Family of (k Subspaces_of V) holds

( b_{4} = k Pencils_of V iff for X being set holds

( X in b_{4} 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 F being Field

for V being finite-dimensional VectSp of F

for k being Nat

for b

( b

( X in b

( W1 is Subspace of W2 & (dim W1) + 1 = k & dim W2 = k + 1 & 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 & k < dim V holds

not k Pencils_of V is empty

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 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 & 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 )

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 & 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 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

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 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

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

dim (W + (Lin {v,u})) = (dim W) + 2

for V being finite-dimensional VectSp of F

for W being Subspace of V

for v, u being Vector of V st 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 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 & 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)

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 & 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 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 & dim W2 = k + 1 holds

not pencil (W1,W2,k) is trivial

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 & 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;

TopStruct(# (k Subspaces_of V),(k Pencils_of V) #) is strict TopStruct ;

end;
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) #);

TopStruct(# (k Subspaces_of V),(k Pencils_of V) #) is strict TopStruct ;

:: 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) #);

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 & k < dim V holds

not PencilSpace (V,k) is void by Th10;

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 by Th10;

theorem Th18: :: PENCIL_4:18

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

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 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

PencilSpace (V,k) is with_non_trivial_blocks

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 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 holds

PencilSpace (V,k) is identifying_close_blocks

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:21

definition

let F be Field;

let V be finite-dimensional VectSp of F;

let m, n be Nat;

ex b_{1} being Subset-Family of (m Subspaces_of V) st

for X being set holds

( X in b_{1} iff ex W being Subspace of V st

( dim W = n & X = m Subspaces_of W ) )

for b_{1}, b_{2} being Subset-Family of (m Subspaces_of V) st ( for X being set holds

( X in b_{1} iff ex W being Subspace of V st

( dim W = n & X = m Subspaces_of W ) ) ) & ( for X being set holds

( X in b_{2} iff ex W being Subspace of V st

( dim W = n & X = m Subspaces_of W ) ) ) holds

b_{1} = b_{2}

end;
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 for X being set holds

( X in it iff ex W being Subspace of V st

( dim W = n & X = m Subspaces_of W ) );

ex b

for X being set holds

( X in b

( dim W = n & X = m Subspaces_of W ) )

proof end;

uniqueness for b

( X in b

( dim W = n & X = m Subspaces_of W ) ) ) & ( for X being set holds

( X in b

( dim W = n & X = m Subspaces_of W ) ) ) holds

b

proof 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 b_{5} being Subset-Family of (m Subspaces_of V) holds

( b_{5} = SubspaceSet (V,m,n) iff for X being set holds

( X in b_{5} iff ex W being Subspace of V st

( dim W = n & X = m Subspaces_of W ) ) );

for F being Field

for V being finite-dimensional VectSp of F

for m, n being Nat

for b

( b

( X in b

( dim W = n & 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

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 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

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

(Omega). V = (Omega). W

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;

TopStruct(# (m Subspaces_of V),(SubspaceSet (V,m,n)) #) is strict TopStruct ;

end;
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)) #);

TopStruct(# (m Subspaces_of V),(SubspaceSet (V,m,n)) #) is strict TopStruct ;

:: 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)) #);

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 by Th22;

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 by Th22;

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 & m < n & n < dim V holds

not GrassmannSpace (V,m,n) is degenerated

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 Th27: :: PENCIL_4:27

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

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 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

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

proof end;

theorem :: PENCIL_4:29

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

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 ;

ex b_{1} being set st

for z being set holds

( z in b_{1} iff ex x, y being set st

( x in X & y in X & z = {x,y} ) )

for b_{1}, b_{2} being set st ( for z being set holds

( z in b_{1} iff ex x, y being set st

( x in X & y in X & z = {x,y} ) ) ) & ( for z being set holds

( z in b_{2} iff ex x, y being set st

( x in X & y in X & z = {x,y} ) ) ) holds

b_{1} = b_{2}

end;
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 for z being set holds

( z in it iff ex x, y being set st

( x in X & y in X & z = {x,y} ) );

ex b

for z being set holds

( z in b

( x in X & y in X & z = {x,y} ) )

proof end;

uniqueness for b

( z in b

( x in X & y in X & z = {x,y} ) ) ) & ( for z being set holds

( z in b

( x in X & y in X & z = {x,y} ) ) ) holds

b

proof end;

:: deftheorem Def8 defines PairSet PENCIL_4:def 8 :

for X, b_{2} being set holds

( b_{2} = PairSet X iff for z being set holds

( z in b_{2} iff ex x, y being set st

( x in X & y in X & z = {x,y} ) ) );

for X, b

( b

( z in b

( x in X & y in X & z = {x,y} ) ) );

definition

let t be object ;

let X be set ;

ex b_{1} being set st

for z being set holds

( z in b_{1} iff ex y being set st

( y in X & z = {t,y} ) )

for b_{1}, b_{2} being set st ( for z being set holds

( z in b_{1} iff ex y being set st

( y in X & z = {t,y} ) ) ) & ( for z being set holds

( z in b_{2} iff ex y being set st

( y in X & z = {t,y} ) ) ) holds

b_{1} = b_{2}

end;
let 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 for z being set holds

( z in it iff ex y being set st

( y in X & z = {t,y} ) );

ex b

for z being set holds

( z in b

( y in X & z = {t,y} ) )

proof end;

uniqueness for b

( z in b

( y in X & z = {t,y} ) ) ) & ( for z being set holds

( z in b

( y in X & z = {t,y} ) ) ) holds

b

proof end;

:: deftheorem Def9 defines PairSet PENCIL_4:def 9 :

for t being object

for X, b_{3} being set holds

( b_{3} = PairSet (t,X) iff for z being set holds

( z in b_{3} iff ex y being set st

( y in X & z = {t,y} ) ) );

for t being object

for X, b

( b

( z in b

( y in X & z = {t,y} ) ) );

registration
end;

registration
end;

definition

let X be set ;

let L be Subset-Family of X;

ex b_{1} being Subset-Family of (PairSet X) st

for S being set holds

( S in b_{1} iff ex t being set ex l being Subset of X st

( t in X & l in L & S = PairSet (t,l) ) )

for b_{1}, b_{2} being Subset-Family of (PairSet X) st ( for S being set holds

( S in b_{1} iff ex t being set ex l being Subset of X st

( t in X & l in L & S = PairSet (t,l) ) ) ) & ( for S being set holds

( S in b_{2} iff ex t being set ex l being Subset of X st

( t in X & l in L & S = PairSet (t,l) ) ) ) holds

b_{1} = b_{2}

end;
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 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) ) );

ex b

for S being set holds

( S in b

( t in X & l in L & S = PairSet (t,l) ) )

proof end;

uniqueness for b

( S in b

( t in X & l in L & S = PairSet (t,l) ) ) ) & ( for S being set holds

( S in b

( t in X & l in L & S = PairSet (t,l) ) ) ) holds

b

proof end;

:: deftheorem Def10 defines PairSetFamily PENCIL_4:def 10 :

for X being set

for L being Subset-Family of X

for b_{3} being Subset-Family of (PairSet X) holds

( b_{3} = PairSetFamily L iff for S being set holds

( S in b_{3} iff ex t being set ex l being Subset of X st

( t in X & l in L & S = PairSet (t,l) ) ) );

for X being set

for L being Subset-Family of X

for b

( b

( S in b

( t in X & l in L & S = PairSet (t,l) ) ) );

registration

let X be non empty set ;

let L be non empty Subset-Family of X;

coherence

not PairSetFamily L is empty

end;
let L be non empty Subset-Family of X;

coherence

not PairSetFamily L is empty

proof end;

definition

let S be TopStruct ;

TopStruct(# (PairSet the carrier of S),(PairSetFamily the topology of S) #) is strict TopStruct ;

end;
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) #);

TopStruct(# (PairSet the carrier of S),(PairSetFamily the topology of S) #) is strict TopStruct ;

:: 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) #);

for S being TopStruct holds VeroneseSpace S = TopStruct(# (PairSet the carrier of S),(PairSetFamily the topology of S) #);

registration

let S be non empty non void non degenerated TopStruct ;

coherence

not VeroneseSpace S is degenerated

end;
coherence

not VeroneseSpace S is degenerated

proof end;

registration

let S be non empty non void with_non_trivial_blocks TopStruct ;

coherence

VeroneseSpace S is with_non_trivial_blocks

end;
coherence

VeroneseSpace S is with_non_trivial_blocks

proof end;

registration

let S be identifying_close_blocks TopStruct ;

coherence

VeroneseSpace S is identifying_close_blocks

end;
coherence

VeroneseSpace S is identifying_close_blocks

proof end;