:: PENCIL_1 semantic presentation

theorem Th1: :: PENCIL_1:1

for f, g being Function st product f = product g & f is non-empty holds
g is non-empty

proof end;

theorem Th2: :: PENCIL_1:2

for X being set holds
( 2 c= Card X iff ex x, y being set st
( x in X & y in X & x <> y ) )

proof end;

theorem Th3: :: PENCIL_1:3

for X being set st 2 c= Card X holds
for x being set ex y being set st
( y in X & x <> y )

proof end;

theorem Th4: :: PENCIL_1:4

for X being set holds
( 2 c= Card X iff not X is trivial )

proof end;

theorem Th5: :: PENCIL_1:5

for X being set holds
( 3 c= Card X iff ex x, y, z being set 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 set ex z being set st
( z in X & x <> z & y <> z )

proof end;

definition

let S be TopStruct ;
mode Block of S is Element of the topology of S;

end;

definition

let S be TopStruct ;
let x, y be Point of S;
pred x,y are_collinear means :Def1: :: PENCIL_1:def 1
( x = y or ex l being Block of S st {x,y} c= l );

end;

:: deftheorem Def1 defines are_collinear PENCIL_1:def 1 :

definition

let S be TopStruct ;
let T be Subset of S;
attr T is closed_under_lines means :Def2: :: PENCIL_1:def 2
for l being Block of S st 2 c= Card (l /\ T) holds
l c= T;
attr T is strong means :Def3: :: PENCIL_1:def 3
for x, y being Point of S st x in T & y in T holds
x,y are_collinear ;

end;

:: deftheorem Def2 defines closed_under_lines PENCIL_1:def 2 :

:: deftheorem Def3 defines strong PENCIL_1:def 3 :

definition

let S be TopStruct ;
attr S is void means :Def4: :: PENCIL_1:def 4
the topology of S is empty;
attr S is degenerated means :Def5: :: PENCIL_1:def 5
the carrier of S is Block of S;
attr S is with_non_trivial_blocks means :Def6: :: PENCIL_1:def 6
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;
attr S is truly-partial means :Def8: :: PENCIL_1:def 8
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;
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 ) );
attr S is strongly_connected means :Def11: :: 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))) ) );

end;

:: deftheorem Def4 defines void PENCIL_1:def 4 :

:: deftheorem Def5 defines degenerated PENCIL_1:def 5 :

:: deftheorem Def6 defines with_non_trivial_blocks PENCIL_1:def 6 :

:: deftheorem Def7 defines identifying_close_blocks PENCIL_1:def 7 :

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

:: deftheorem Def9 defines without_isolated_points PENCIL_1:def 9 :

:: deftheorem defines connected PENCIL_1:def 10 :

:: deftheorem Def11 defines strongly_connected PENCIL_1:def 11 :

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 )

proof end;

Lm1: ex S being TopStruct st
( S is strict & 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 )

proof end;

Lm2: ex S being TopStruct st
( S is strict & 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

cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks non truly-partial without_isolated_points TopStruct ;
existence by Lm1;
cluster non empty strict non void non degenerated with_non_trivial_blocks identifying_close_blocks truly-partial without_isolated_points TopStruct ;
existence by Lm2;

end;

registration

let S be non void TopStruct ;
cluster the topology of S -> non empty ;
coherence by Def4;

end;

definition

let S be without_isolated_points TopStruct ;
let x, y be Point of S;
redefine pred x,y are_collinear means :: PENCIL_1:def 12
ex l being Block of S st {x,y} c= l;
compatibility

proof end;

end;

:: deftheorem defines are_collinear PENCIL_1:def 12 :

definition

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

end;

definition

let F be Relation;
attr F is TopStruct-yielding means :Def13: :: PENCIL_1:def 13
for x being set st x in rng F holds
x is TopStruct ;

end;

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

registration

cluster TopStruct-yielding -> 1-sorted-yielding set ;
coherence

proof end;

end;

registration

let I be set ;
cluster 1-sorted-yielding TopStruct-yielding ManySortedSet of I;
existence

proof end;

end;

registration

cluster 1-sorted-yielding TopStruct-yielding set ;
existence

proof end;

end;

definition

let F be Relation;
attr F is non-void-yielding means :Def14: :: PENCIL_1:def 14
for S being TopStruct st S in rng F holds
not S is void;

end;

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

definition

let F be TopStruct-yielding Function;
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

proof end;

end;

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

definition

let F be Relation;
attr F is trivial-yielding means :Def16: :: PENCIL_1:def 16
for S being set st S in rng F holds
S is trivial;

end;

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

definition

let F be Relation;
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;

end;

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

registration

cluster non-Trivial-yielding -> non-Empty set ;
coherence

proof end;

end;

definition

let F be 1-sorted-yielding Function;
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

proof end;

end;

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

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

proof end;

end;

definition

let F be Relation;
attr F is PLS-yielding means :Def19: :: PENCIL_1:def 19
for x being set st x in rng F holds
x is PLS;

end;

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

registration

cluster PLS-yielding -> non-Empty 1-sorted-yielding TopStruct-yielding set ;
coherence

proof end;

cluster TopStruct-yielding PLS-yielding -> 1-sorted-yielding TopStruct-yielding non-void-yielding set ;
coherence

proof end;

cluster TopStruct-yielding PLS-yielding -> non-Empty 1-sorted-yielding TopStruct-yielding non-Trivial-yielding set ;
coherence

proof end;

end;

registration

let I be set ;
cluster non-Empty 1-sorted-yielding TopStruct-yielding non-void-yielding non-Trivial-yielding PLS-yielding ManySortedSet of I;
existence

proof end;

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

proof end;

end;

definition

let I be set ;
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
( not A . j is empty & A . j is trivial );

end;

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

registration

let I be set ;
let A be ManySortedSet of I;
cluster {A} -> trivial-yielding ;
coherence

proof end;

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

proof end;

registration

let I be non empty set ;
let A be ManySortedSet of I;
cluster {A} -> trivial-yielding Segre-like ;
coherence

proof end;

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

proof end;

theorem Th11: :: PENCIL_1:11

for I being non empty set
for A being non-Empty 1-sorted-yielding 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 non-Empty 1-sorted-yielding ManySortedSet of I;
cluster V2 trivial-yielding Segre-like ManySortedSubset of Carrier A;
existence

proof end;

end;

registration

let I be non empty set ;
let A be 1-sorted-yielding non-Trivial-yielding ManySortedSet of I;
cluster V2 non trivial-yielding Segre-like ManySortedSubset of Carrier A;
existence

proof end;

end;

registration

let I be non empty set ;
cluster non trivial-yielding Segre-like ManySortedSet of I;
existence

proof end;

end;

definition

let I be non empty set ;
let B be non trivial-yielding Segre-like ManySortedSet of I;
func indx B -> Element of I means :Def21: :: PENCIL_1:def 21
not B . it is trivial;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def21 defines indx PENCIL_1:def 21 :

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
( not A . i is empty & A . i is trivial )

proof end;

registration

let I be non empty set ;
cluster non trivial-yielding Segre-like -> V2 ManySortedSet of I;
coherence

proof end;

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 non-empty & 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;
cluster product B -> non trivial ;
coherence

proof end;

end;

definition

let I be non empty set ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines Segre_Blocks PENCIL_1:def 22 :

definition

let I be non empty set ;
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 by STRUCT_0:def 1;

end;

:: deftheorem defines Segre_Product PENCIL_1:def 23 :

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

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

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

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

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

proof end;

definition

let I be non empty set ;
let A be PLS-yielding ManySortedSet of I;
:: original: Segre_Product
redefine func Segre_Product A -> PLS;
coherence

proof end;

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 )

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

proof end;

theorem Th21: :: PENCIL_1:21

for S being TopStruct
for l being Block of S
for L being Subset of S st L = l holds
L is strong

proof end;

theorem :: PENCIL_1:22

for S being non void TopStruct holds [#] S is closed_under_lines

proof end;

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

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)

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

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

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

proof end;