:: by Adam Naumowicz

::

:: Received May 29, 2000

:: Copyright (c) 2000-2016 Association of Mizar Users

theorem Th5: :: PENCIL_1:5

for X being set holds

( 3 c= card X iff ex x, y, z being object st

( x in X & y in X & z in X & x <> y & x <> z & y <> z ) )

( 3 c= card X iff ex x, y, z being object st

( x in X & y in X & z in X & x <> y & x <> z & y <> z ) )

proof end;

theorem Th6: :: PENCIL_1:6

for X being set st 3 c= card X holds

for x, y being object ex z being object st

( z in X & x <> z & y <> z )

for x, y being object ex z being object st

( z in X & x <> z & y <> z )

proof end;

:: deftheorem defines are_collinear PENCIL_1:def 1 :

for S being TopStruct

for x, y being Point of S holds

( x,y are_collinear iff ( x = y or ex l being Block of S st {x,y} c= l ) );

for S being TopStruct

for x, y being Point of S holds

( x,y are_collinear iff ( x = y or ex l being Block of S st {x,y} c= l ) );

definition

let S be TopStruct ;

let T be Subset of S;

end;
let T be Subset of S;

attr T is closed_under_lines means :: PENCIL_1:def 2

for l being Block of S st 2 c= card (l /\ T) holds

l c= T;

for l being Block of S st 2 c= card (l /\ T) holds

l c= T;

attr T is strong means :: PENCIL_1:def 3

for x, y being Point of S st x in T & y in T holds

x,y are_collinear ;

for x, y being Point of S st x in T & y in T holds

x,y are_collinear ;

:: deftheorem defines closed_under_lines PENCIL_1:def 2 :

for S being TopStruct

for T being Subset of S holds

( T is closed_under_lines iff for l being Block of S st 2 c= card (l /\ T) holds

l c= T );

for S being TopStruct

for T being Subset of S holds

( T is closed_under_lines iff for l being Block of S st 2 c= card (l /\ T) holds

l c= T );

:: deftheorem defines strong PENCIL_1:def 3 :

for S being TopStruct

for T being Subset of S holds

( T is strong iff for x, y being Point of S st x in T & y in T holds

x,y are_collinear );

for S being TopStruct

for T being Subset of S holds

( T is strong iff for x, y being Point of S st x in T & y in T holds

x,y are_collinear );

definition

let S be TopStruct ;

end;
attr S is with_non_trivial_blocks means :Def6: :: PENCIL_1:def 6

for k being Block of S holds 2 c= card k;

for k being Block of S holds 2 c= card k;

attr S is identifying_close_blocks means :Def7: :: PENCIL_1:def 7

for k, l being Block of S st 2 c= card (k /\ l) holds

k = l;

for k, l being Block of S st 2 c= card (k /\ l) holds

k = l;

attr S is truly-partial means :: PENCIL_1:def 8

not for x, y being Point of S holds x,y are_collinear ;

not for x, y being Point of S holds x,y are_collinear ;

attr S is without_isolated_points means :Def9: :: PENCIL_1:def 9

for x being Point of S ex l being Block of S st x in l;

for x being Point of S ex l being Block of S st x in l;

attr S is connected means :: PENCIL_1:def 10

for x, y being Point of S ex f being FinSequence of the carrier of S st

( x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds

for a, b being Point of S st a = f . i & b = f . (i + 1) holds

a,b are_collinear ) );

for x, y being Point of S ex f being FinSequence of the carrier of S st

( x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds

for a, b being Point of S st a = f . i & b = f . (i + 1) holds

a,b are_collinear ) );

attr S is strongly_connected means :: PENCIL_1:def 11

for x being Point of S

for X being Subset of S st X is closed_under_lines & X is strong holds

ex f being FinSequence of bool the carrier of S st

( X = f . 1 & x in f . (len f) & ( for W being Subset of S st W in rng f holds

( W is closed_under_lines & W is strong ) ) & ( for i being Nat st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) ) );

for x being Point of S

for X being Subset of S st X is closed_under_lines & X is strong holds

ex f being FinSequence of bool the carrier of S st

( X = f . 1 & x in f . (len f) & ( for W being Subset of S st W in rng f holds

( W is closed_under_lines & W is strong ) ) & ( for i being Nat st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) ) );

:: deftheorem Def4 defines void PENCIL_1:def 4 :

for S being TopStruct holds

( S is void iff the topology of S is empty );

for S being TopStruct holds

( S is void iff the topology of S is empty );

:: deftheorem defines degenerated PENCIL_1:def 5 :

for S being TopStruct holds

( S is degenerated iff the carrier of S is Block of S );

for S being TopStruct holds

( S is degenerated iff the carrier of S is Block of S );

:: deftheorem Def6 defines with_non_trivial_blocks PENCIL_1:def 6 :

for S being TopStruct holds

( S is with_non_trivial_blocks iff for k being Block of S holds 2 c= card k );

for S being TopStruct holds

( S is with_non_trivial_blocks iff for k being Block of S holds 2 c= card k );

:: deftheorem Def7 defines identifying_close_blocks PENCIL_1:def 7 :

for S being TopStruct holds

( S is identifying_close_blocks iff for k, l being Block of S st 2 c= card (k /\ l) holds

k = l );

for S being TopStruct holds

( S is identifying_close_blocks iff for k, l being Block of S st 2 c= card (k /\ l) holds

k = l );

:: deftheorem defines truly-partial PENCIL_1:def 8 :

for S being TopStruct holds

( S is truly-partial iff not for x, y being Point of S holds x,y are_collinear );

for S being TopStruct holds

( S is truly-partial iff not for x, y being Point of S holds x,y are_collinear );

:: deftheorem Def9 defines without_isolated_points PENCIL_1:def 9 :

for S being TopStruct holds

( S is without_isolated_points iff for x being Point of S ex l being Block of S st x in l );

for S being TopStruct holds

( S is without_isolated_points iff for x being Point of S ex l being Block of S st x in l );

:: deftheorem defines connected PENCIL_1:def 10 :

for S being TopStruct holds

( S is connected iff for x, y being Point of S ex f being FinSequence of the carrier of S st

( x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds

for a, b being Point of S st a = f . i & b = f . (i + 1) holds

a,b are_collinear ) ) );

for S being TopStruct holds

( S is connected iff for x, y being Point of S ex f being FinSequence of the carrier of S st

( x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds

for a, b being Point of S st a = f . i & b = f . (i + 1) holds

a,b are_collinear ) ) );

:: deftheorem defines strongly_connected PENCIL_1:def 11 :

for S being TopStruct holds

( S is strongly_connected iff for x being Point of S

for X being Subset of S st X is closed_under_lines & X is strong holds

ex f being FinSequence of bool the carrier of S st

( X = f . 1 & x in f . (len f) & ( for W being Subset of S st W in rng f holds

( W is closed_under_lines & W is strong ) ) & ( for i being Nat st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) ) ) );

for S being TopStruct holds

( S is strongly_connected iff for x being Point of S

for X being Subset of S st X is closed_under_lines & X is strong holds

ex f being FinSequence of bool the carrier of S st

( X = f . 1 & x in f . (len f) & ( for W being Subset of S st W in rng f holds

( W is closed_under_lines & W is strong ) ) & ( for i being Nat st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) ) ) );

theorem Th7: :: PENCIL_1:7

for X being non empty set st 3 c= card X holds

for S being TopStruct st the carrier of S = X & the topology of S = { L where L is Subset of X : 2 = card L } holds

( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )

for S being TopStruct st the carrier of S = X & the topology of S = { L where L is Subset of X : 2 = card L } holds

( not S is empty & not S is void & not S is degenerated & not S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )

proof end;

theorem Th8: :: PENCIL_1:8

for X being non empty set st 3 c= card X holds

for K being Subset of X st card K = 2 holds

for S being TopStruct st the carrier of S = X & the topology of S = { L where L is Subset of X : 2 = card L } \ {K} holds

( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )

for K being Subset of X st card K = 2 holds

for S being TopStruct st the carrier of S = X & the topology of S = { L where L is Subset of X : 2 = card L } \ {K} holds

( not S is empty & not S is void & not S is degenerated & S is truly-partial & S is with_non_trivial_blocks & S is identifying_close_blocks & S is without_isolated_points )

proof end;

registration

ex b_{1} being TopStruct st

( b_{1} is strict & not b_{1} is empty & not b_{1} is void & not b_{1} is degenerated & not b_{1} is truly-partial & b_{1} is with_non_trivial_blocks & b_{1} is identifying_close_blocks & b_{1} is without_isolated_points )

ex b_{1} being TopStruct st

( b_{1} is strict & not b_{1} is empty & not b_{1} is void & not b_{1} is degenerated & b_{1} is truly-partial & b_{1} is with_non_trivial_blocks & b_{1} is identifying_close_blocks & b_{1} is without_isolated_points )
end;

cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks non truly-partial without_isolated_points for TopStruct ;

existence ex b

( b

proof end;

cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks truly-partial without_isolated_points for TopStruct ;

existence ex b

( b

proof end;

definition

let S be without_isolated_points TopStruct ;

let x, y be Point of S;

compatibility

( x,y are_collinear iff ex l being Block of S st {x,y} c= l )

end;
let x, y be Point of S;

compatibility

( x,y are_collinear iff ex l being Block of S st {x,y} c= l )

proof end;

:: deftheorem defines are_collinear PENCIL_1:def 12 :

for S being without_isolated_points TopStruct

for x, y being Point of S holds

( x,y are_collinear iff ex l being Block of S st {x,y} c= l );

for S being without_isolated_points TopStruct

for x, y being Point of S holds

( x,y are_collinear iff ex l being Block of S st {x,y} c= l );

definition

mode PLS is non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks TopStruct ;

end;
definition

let F be Relation;

end;
attr F is TopStruct-yielding means :Def13: :: PENCIL_1:def 13

for x being set st x in rng F holds

x is TopStruct ;

for x being set st x in rng F holds

x is TopStruct ;

:: deftheorem Def13 defines TopStruct-yielding PENCIL_1:def 13 :

for F being Relation holds

( F is TopStruct-yielding iff for x being set st x in rng F holds

x is TopStruct );

for F being Relation holds

( F is TopStruct-yielding iff for x being set st x in rng F holds

x is TopStruct );

registration

coherence

for b_{1} being Function st b_{1} is TopStruct-yielding holds

b_{1} is 1-sorted-yielding

end;
for b

b

proof end;

registration

let I be set ;

existence

ex b_{1} being ManySortedSet of I st b_{1} is TopStruct-yielding

end;
existence

ex b

proof end;

definition

let F be Relation;

end;
attr F is non-void-yielding means :: PENCIL_1:def 14

for S being TopStruct st S in rng F holds

not S is void ;

for S being TopStruct st S in rng F holds

not S is void ;

:: deftheorem defines non-void-yielding PENCIL_1:def 14 :

for F being Relation holds

( F is non-void-yielding iff for S being TopStruct st S in rng F holds

not S is void );

for F being Relation holds

( F is non-void-yielding iff for S being TopStruct st S in rng F holds

not S is void );

definition

let F be TopStruct-yielding Function;

( F is non-void-yielding iff for i being set st i in rng F holds

i is non void TopStruct ) by Def13;

end;
redefine attr F is non-void-yielding means :: PENCIL_1:def 15

for i being set st i in rng F holds

i is non void TopStruct ;

compatibility for i being set st i in rng F holds

i is non void TopStruct ;

( F is non-void-yielding iff for i being set st i in rng F holds

i is non void TopStruct ) by Def13;

:: deftheorem defines non-void-yielding PENCIL_1:def 15 :

for F being TopStruct-yielding Function holds

( F is non-void-yielding iff for i being set st i in rng F holds

i is non void TopStruct );

for F being TopStruct-yielding Function holds

( F is non-void-yielding iff for i being set st i in rng F holds

i is non void TopStruct );

definition

let F be Relation;

end;
attr F is trivial-yielding means :Def16: :: PENCIL_1:def 16

for S being set st S in rng F holds

S is trivial ;

for S being set st S in rng F holds

S is trivial ;

:: deftheorem Def16 defines trivial-yielding PENCIL_1:def 16 :

for F being Relation holds

( F is trivial-yielding iff for S being set st S in rng F holds

S is trivial );

for F being Relation holds

( F is trivial-yielding iff for S being set st S in rng F holds

S is trivial );

definition

let F be Relation;

end;
attr F is non-Trivial-yielding means :Def17: :: PENCIL_1:def 17

for S being 1-sorted st S in rng F holds

not S is trivial ;

for S being 1-sorted st S in rng F holds

not S is trivial ;

:: deftheorem Def17 defines non-Trivial-yielding PENCIL_1:def 17 :

for F being Relation holds

( F is non-Trivial-yielding iff for S being 1-sorted st S in rng F holds

not S is trivial );

for F being Relation holds

( F is non-Trivial-yielding iff for S being 1-sorted st S in rng F holds

not S is trivial );

registration
end;

definition

let F be 1-sorted-yielding Function;

( F is non-Trivial-yielding iff for i being set st i in rng F holds

i is non trivial 1-sorted )

end;
redefine attr F is non-Trivial-yielding means :: PENCIL_1:def 18

for i being set st i in rng F holds

i is non trivial 1-sorted ;

compatibility for i being set st i in rng F holds

i is non trivial 1-sorted ;

( F is non-Trivial-yielding iff for i being set st i in rng F holds

i is non trivial 1-sorted )

proof end;

:: deftheorem defines non-Trivial-yielding PENCIL_1:def 18 :

for F being 1-sorted-yielding Function holds

( F is non-Trivial-yielding iff for i being set st i in rng F holds

i is non trivial 1-sorted );

for F being 1-sorted-yielding Function holds

( F is non-Trivial-yielding iff for i being set st i in rng F holds

i is non trivial 1-sorted );

definition

let I be non empty set ;

let A be TopStruct-yielding ManySortedSet of I;

let j be Element of I;

:: original: .

redefine func A . j -> TopStruct ;

coherence

A . j is TopStruct

end;
let A be TopStruct-yielding ManySortedSet of I;

let j be Element of I;

:: original: .

redefine func A . j -> TopStruct ;

coherence

A . j is TopStruct

proof end;

definition

let F be Relation;

end;
attr F is PLS-yielding means :Def19: :: PENCIL_1:def 19

for x being set st x in rng F holds

x is PLS;

for x being set st x in rng F holds

x is PLS;

:: deftheorem Def19 defines PLS-yielding PENCIL_1:def 19 :

for F being Relation holds

( F is PLS-yielding iff for x being set st x in rng F holds

x is PLS );

for F being Relation holds

( F is PLS-yielding iff for x being set st x in rng F holds

x is PLS );

registration

coherence

for b_{1} being Function st b_{1} is PLS-yielding holds

( b_{1} is non-Empty & b_{1} is TopStruct-yielding )
;

for b_{1} being TopStruct-yielding Function st b_{1} is PLS-yielding holds

b_{1} is non-void-yielding
;

for b_{1} being TopStruct-yielding Function st b_{1} is PLS-yielding holds

b_{1} is non-Trivial-yielding

end;
for b

( b

cluster Relation-like Function-like TopStruct-yielding PLS-yielding -> TopStruct-yielding non-void-yielding for set ;

coherence for b

b

cluster Relation-like Function-like TopStruct-yielding PLS-yielding -> TopStruct-yielding non-Trivial-yielding for set ;

coherence for b

b

proof end;

registration
end;

definition

let I be non empty set ;

let A be PLS-yielding ManySortedSet of I;

let j be Element of I;

:: original: .

redefine func A . j -> PLS;

coherence

A . j is PLS

end;
let A be PLS-yielding ManySortedSet of I;

let j be Element of I;

:: original: .

redefine func A . j -> PLS;

coherence

A . j is PLS

proof end;

definition

let I be set ;

let A be ManySortedSet of I;

end;
let A be ManySortedSet of I;

attr A is Segre-like means :Def20: :: PENCIL_1:def 20

ex i being Element of I st

for j being Element of I st i <> j holds

A . j is 1 -element ;

ex i being Element of I st

for j being Element of I st i <> j holds

A . j is 1 -element ;

:: deftheorem Def20 defines Segre-like PENCIL_1:def 20 :

for I being set

for A being ManySortedSet of I holds

( A is Segre-like iff ex i being Element of I st

for j being Element of I st i <> j holds

A . j is 1 -element );

for I being set

for A being ManySortedSet of I holds

( A is Segre-like iff ex i being Element of I st

for j being Element of I st i <> j holds

A . j is 1 -element );

registration
end;

theorem :: PENCIL_1:9

for I being non empty set

for A being ManySortedSet of I

for i being Element of I

for S being non trivial set holds not A +* (i,S) is trivial-yielding

for A being ManySortedSet of I

for i being Element of I

for S being non trivial set holds not A +* (i,S) is trivial-yielding

proof end;

registration
end;

theorem :: PENCIL_1:10

for I being non empty set

for A being ManySortedSet of I

for i, S being set holds {A} +* (i,S) is Segre-like

for A being ManySortedSet of I

for i, S being set holds {A} +* (i,S) is Segre-like

proof end;

theorem Th11: :: PENCIL_1:11

for I being non empty set

for A being 1-sorted-yielding non-Empty ManySortedSet of I

for B being Element of Carrier A holds {B} is ManySortedSubset of Carrier A

for A being 1-sorted-yielding non-Empty ManySortedSet of I

for B being Element of Carrier A holds {B} is ManySortedSubset of Carrier A

proof end;

registration

let I be non empty set ;

let A be 1-sorted-yielding non-Empty ManySortedSet of I;

ex b_{1} being ManySortedSubset of Carrier A st

( b_{1} is Segre-like & b_{1} is trivial-yielding & b_{1} is V2() )

end;
let A be 1-sorted-yielding non-Empty ManySortedSet of I;

cluster Relation-like V2() I -defined Function-like V14(I) trivial-yielding Segre-like for ManySortedSubset of Carrier A;

existence ex b

( b

proof end;

registration

let I be non empty set ;

let A be 1-sorted-yielding non-Trivial-yielding ManySortedSet of I;

ex b_{1} being ManySortedSubset of Carrier A st

( b_{1} is Segre-like & not b_{1} is trivial-yielding & b_{1} is V2() )

end;
let A be 1-sorted-yielding non-Trivial-yielding ManySortedSet of I;

cluster Relation-like V2() I -defined Function-like V14(I) non trivial-yielding Segre-like for ManySortedSubset of Carrier A;

existence ex b

( b

proof end;

registration

let I be non empty set ;

existence

ex b_{1} being ManySortedSet of I st

( b_{1} is Segre-like & not b_{1} is trivial-yielding )

end;
existence

ex b

( b

proof end;

definition

let I be non empty set ;

let B be non trivial-yielding Segre-like ManySortedSet of I;

existence

not for b_{1} being Element of I holds B . b_{1} is trivial

for b_{1}, b_{2} being Element of I st not B . b_{1} is trivial & not B . b_{2} is trivial holds

b_{1} = b_{2}

end;
let B be non trivial-yielding Segre-like ManySortedSet of I;

existence

not for b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def21 defines indx PENCIL_1:def 21 :

for I being non empty set

for B being non trivial-yielding Segre-like ManySortedSet of I

for b_{3} being Element of I holds

( b_{3} = indx B iff not B . b_{3} is trivial );

for I being non empty set

for B being non trivial-yielding Segre-like ManySortedSet of I

for b

( b

theorem Th12: :: PENCIL_1:12

for I being non empty set

for A being non trivial-yielding Segre-like ManySortedSet of I

for i being Element of I st i <> indx A holds

A . i is 1 -element

for A being non trivial-yielding Segre-like ManySortedSet of I

for i being Element of I st i <> indx A holds

A . i is 1 -element

proof end;

registration

let I be non empty set ;

for b_{1} being ManySortedSet of I st b_{1} is Segre-like & not b_{1} is trivial-yielding holds

b_{1} is V2()

end;
cluster Relation-like I -defined Function-like V14(I) non trivial-yielding Segre-like -> V2() for set ;

coherence for b

b

proof end;

theorem Th13: :: PENCIL_1:13

for I being non empty set

for A being ManySortedSet of I holds

( 2 c= card (product A) iff ( A is V2() & not A is trivial-yielding ) )

for A being ManySortedSet of I holds

( 2 c= card (product A) iff ( A is V2() & not A is trivial-yielding ) )

proof end;

registration

let I be non empty set ;

let B be non trivial-yielding Segre-like ManySortedSet of I;

coherence

not product B is trivial

end;
let B be non trivial-yielding Segre-like ManySortedSet of I;

coherence

not product B is trivial

proof end;

definition

let I be non empty set ;

let A be non-Empty TopStruct-yielding ManySortedSet of I;

ex b_{1} being Subset-Family of (product (Carrier A)) st

for x being set holds

( x in b_{1} iff ex B being Segre-like ManySortedSubset of Carrier A st

( x = product B & ex i being Element of I st B . i is Block of (A . i) ) )

for b_{1}, b_{2} being Subset-Family of (product (Carrier A)) st ( for x being set holds

( x in b_{1} iff ex B being Segre-like ManySortedSubset of Carrier A st

( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) ) & ( for x being set holds

( x in b_{2} iff ex B being Segre-like ManySortedSubset of Carrier A st

( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) ) holds

b_{1} = b_{2}

end;
let A be non-Empty TopStruct-yielding ManySortedSet of I;

func Segre_Blocks A -> Subset-Family of (product (Carrier A)) means :Def22: :: PENCIL_1:def 22

for x being set holds

( x in it iff ex B being Segre-like ManySortedSubset of Carrier A st

( x = product B & ex i being Element of I st B . i is Block of (A . i) ) );

existence for x being set holds

( x in it iff ex B being Segre-like ManySortedSubset of Carrier A st

( x = product B & ex i being Element of I st B . i is Block of (A . i) ) );

ex b

for x being set holds

( x in b

( x = product B & ex i being Element of I st B . i is Block of (A . i) ) )

proof end;

uniqueness for b

( x in b

( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) ) & ( for x being set holds

( x in b

( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) ) holds

b

proof end;

:: deftheorem Def22 defines Segre_Blocks PENCIL_1:def 22 :

for I being non empty set

for A being non-Empty TopStruct-yielding ManySortedSet of I

for b_{3} being Subset-Family of (product (Carrier A)) holds

( b_{3} = Segre_Blocks A iff for x being set holds

( x in b_{3} iff ex B being Segre-like ManySortedSubset of Carrier A st

( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) );

for I being non empty set

for A being non-Empty TopStruct-yielding ManySortedSet of I

for b

( b

( x in b

( x = product B & ex i being Element of I st B . i is Block of (A . i) ) ) );

definition

let I be non empty set ;

let A be non-Empty TopStruct-yielding ManySortedSet of I;

coherence

TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) is non empty TopStruct ;

;

end;
let A be non-Empty TopStruct-yielding ManySortedSet of I;

func Segre_Product A -> non empty TopStruct equals :: PENCIL_1:def 23

TopStruct(# (product (Carrier A)),(Segre_Blocks A) #);

correctness TopStruct(# (product (Carrier A)),(Segre_Blocks A) #);

coherence

TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) is non empty TopStruct ;

;

:: deftheorem defines Segre_Product PENCIL_1:def 23 :

for I being non empty set

for A being non-Empty TopStruct-yielding ManySortedSet of I holds Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #);

for I being non empty set

for A being non-Empty TopStruct-yielding ManySortedSet of I holds Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #);

theorem Th14: :: PENCIL_1:14

for I being non empty set

for A being non-Empty TopStruct-yielding ManySortedSet of I

for x being Point of (Segre_Product A) holds x is ManySortedSet of I

for A being non-Empty TopStruct-yielding ManySortedSet of I

for x being Point of (Segre_Product A) holds x is ManySortedSet of I

proof end;

theorem Th15: :: PENCIL_1:15

for I being non empty set

for A being non-Empty TopStruct-yielding ManySortedSet of I st not for i being Element of I holds A . i is void holds

not Segre_Product A is void

for A being non-Empty TopStruct-yielding ManySortedSet of I st not for i being Element of I holds A . i is void holds

not Segre_Product A is void

proof end;

theorem Th16: :: PENCIL_1:16

for I being non empty set

for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds

( not A . i is degenerated & not for i being Element of I holds A . i is void ) ) holds

not Segre_Product A is degenerated

for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds

( not A . i is degenerated & not for i being Element of I holds A . i is void ) ) holds

not Segre_Product A is degenerated

proof end;

theorem Th17: :: PENCIL_1:17

for I being non empty set

for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds

( A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds

Segre_Product A is with_non_trivial_blocks

for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds

( A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds

Segre_Product A is with_non_trivial_blocks

proof end;

theorem Th18: :: PENCIL_1:18

for I being non empty set

for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds

( A . i is identifying_close_blocks & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds

Segre_Product A is identifying_close_blocks

for A being non-Empty TopStruct-yielding ManySortedSet of I st ( for i being Element of I holds

( A . i is identifying_close_blocks & A . i is with_non_trivial_blocks & not for i being Element of I holds A . i is void ) ) holds

Segre_Product A is identifying_close_blocks

proof end;

registration

let I be non empty set ;

let A be PLS-yielding ManySortedSet of I;

( not Segre_Product A is void & not Segre_Product A is degenerated & Segre_Product A is with_non_trivial_blocks & Segre_Product A is identifying_close_blocks )

end;
let A be PLS-yielding ManySortedSet of I;

cluster Segre_Product A -> non empty non void non degenerated with_non_trivial_blocks identifying_close_blocks ;

coherence ( not Segre_Product A is void & not Segre_Product A is degenerated & Segre_Product A is with_non_trivial_blocks & Segre_Product A is identifying_close_blocks )

proof end;

theorem :: PENCIL_1:19

for T being TopStruct

for S being Subset of T st S is trivial holds

( S is strong & S is closed_under_lines )

for S being Subset of T st S is trivial holds

( S is strong & S is closed_under_lines )

proof end;

theorem Th20: :: PENCIL_1:20

for S being identifying_close_blocks TopStruct

for l being Block of S

for L being Subset of S st L = l holds

L is closed_under_lines by Def7;

for l being Block of S

for L being Subset of S st L = l holds

L is closed_under_lines by Def7;

theorem Th23: :: PENCIL_1:23

for I being non empty set

for A being non trivial-yielding Segre-like ManySortedSet of I

for x, y being ManySortedSet of I st x in product A & y in product A holds

for i being object st i <> indx A holds

x . i = y . i

for A being non trivial-yielding Segre-like ManySortedSet of I

for x, y being ManySortedSet of I st x in product A & y in product A holds

for i being object st i <> indx A holds

x . i = y . i

proof end;

theorem Th24: :: PENCIL_1:24

for I being non empty set

for A being PLS-yielding ManySortedSet of I

for x being set holds

( x is Block of (Segre_Product A) iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st

( x = product L & L . (indx L) is Block of (A . (indx L)) ) )

for A being PLS-yielding ManySortedSet of I

for x being set holds

( x is Block of (Segre_Product A) iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st

( x = product L & L . (indx L) is Block of (A . (indx L)) ) )

proof end;

theorem Th25: :: PENCIL_1:25

for I being non empty set

for A being PLS-yielding ManySortedSet of I

for P being ManySortedSet of I st P is Point of (Segre_Product A) holds

for i being Element of I

for p being Point of (A . i) holds P +* (i,p) is Point of (Segre_Product A)

for A being PLS-yielding ManySortedSet of I

for P being ManySortedSet of I st P is Point of (Segre_Product A) holds

for i being Element of I

for p being Point of (A . i) holds P +* (i,p) is Point of (Segre_Product A)

proof end;

theorem Th26: :: PENCIL_1:26

for I being non empty set

for A, B being non trivial-yielding Segre-like ManySortedSet of I st 2 c= card ((product A) /\ (product B)) holds

( indx A = indx B & ( for i being object st i <> indx A holds

A . i = B . i ) )

for A, B being non trivial-yielding Segre-like ManySortedSet of I st 2 c= card ((product A) /\ (product B)) holds

( indx A = indx B & ( for i being object st i <> indx A holds

A . i = B . i ) )

proof end;

theorem Th27: :: PENCIL_1:27

for I being non empty set

for A being non trivial-yielding Segre-like ManySortedSet of I

for N being non trivial set holds

( A +* ((indx A),N) is Segre-like & not A +* ((indx A),N) is trivial-yielding )

for A being non trivial-yielding Segre-like ManySortedSet of I

for N being non trivial set holds

( A +* ((indx A),N) is Segre-like & not A +* ((indx A),N) is trivial-yielding )

proof end;

theorem :: PENCIL_1:28

for S being non empty non void identifying_close_blocks without_isolated_points TopStruct st S is strongly_connected holds

S is connected

S is connected

proof end;

theorem :: PENCIL_1:29

for I being non empty set

for A being PLS-yielding ManySortedSet of I

for S being Subset of (Segre_Product A) holds

( ( not S is trivial & S is strong & S is closed_under_lines ) iff ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st

( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds

( C is strong & C is closed_under_lines ) ) ) )

for A being PLS-yielding ManySortedSet of I

for S being Subset of (Segre_Product A) holds

( ( not S is trivial & S is strong & S is closed_under_lines ) iff ex B being non trivial-yielding Segre-like ManySortedSubset of Carrier A st

( S = product B & ( for C being Subset of (A . (indx B)) st C = B . (indx B) holds

( C is strong & C is closed_under_lines ) ) ) )

proof end;