:: PENCIL_2 semantic presentation

definition

let D be set ;
let p be FinSequence of D;
let i, j be Nat;
func Del p,i,j -> FinSequence of D equals :: PENCIL_2:def 1
(p | (i -' 1)) ^ (p /^ j);
coherence ;

end;

:: deftheorem defines Del PENCIL_2:def 1 :

theorem Th1: :: PENCIL_2:1

for D being set
for p being FinSequence of D
for i, j being Nat holds rng (Del p,i,j) c= rng p

proof end;

theorem Th2: :: PENCIL_2:2

for D being set
for p being FinSequence of D
for i, j being Nat st i in dom p & j in dom p holds
len (Del p,i,j) = (((len p) - j) + i) - 1

proof end;

theorem Th3: :: PENCIL_2:3

for D being set
for p being FinSequence of D
for i, j being Nat st i in dom p & j in dom p & len (Del p,i,j) = 0 holds
( i = 1 & j = len p )

proof end;

theorem Th4: :: PENCIL_2:4

for D being set
for p being FinSequence of D
for i, j, k being Nat st i in dom p & 1 <= k & k <= i - 1 holds
(Del p,i,j) . k = p . k

proof end;

theorem Th5: :: PENCIL_2:5

for p, q being FinSequence
for k being Nat st (len p) + 1 <= k holds
(p ^ q) . k = q . (k - (len p))

proof end;

theorem Th6: :: PENCIL_2:6

for D being set
for p being FinSequence of D
for i, j, k being Nat st i in dom p & j in dom p & i <= j & i <= k & k <= (((len p) - j) + i) - 1 holds
(Del p,i,j) . k = p . (((j -' i) + k) + 1)

proof end;

scheme :: PENCIL_2:sch 1
FinSeqOneToOne{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> FinSequence of F₃(), P₁[ set , set ] } :

ex g being one-to-one FinSequence of F₃() st
( F₁() = g . 1 & F₂() = g . (len g) & rng g c= rng F₄() & ( for j being Nat st 1 <= j & j < len g holds
P₁[g . j,g . (j + 1)] ) )

provided

A1: ( F₁() = F₄() . 1 & F₂() = F₄() . (len F₄()) ) and
A2: for i being Nat
for d1, d2 being set st 1 <= i & i < len F₄() & d1 = F₄() . i & d2 = F₄() . (i + 1) holds
P₁[d1,d2]

proof end;

theorem Th7: :: PENCIL_2:7

for I being non empty set
for A being 1-sorted-yielding ManySortedSet of I
for L being ManySortedSubset of Carrier A
for i being Element of I
for S being Subset of (A . i) holds L +* i,S is ManySortedSubset of Carrier A

proof end;

definition

let I be non empty set ;
let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of I;
mode Segre-Coset of A -> Subset of (Segre_Product A) means :Def2: :: PENCIL_2:def 2
ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( it = product L & L . (indx L) = [#] (A . (indx L)) );
existence

proof end;

end;

:: deftheorem Def2 defines Segre-Coset PENCIL_2:def 2 :

theorem Th8: :: PENCIL_2:8

for I being non empty set
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for B1, B2 being Segre-Coset of A st 2 c= Card (B1 /\ B2) holds
B1 = B2

proof end;

definition

let S be TopStruct ;
let X, Y be Subset of S;
pred X,Y are_joinable means :Def3: :: PENCIL_2:def 3
ex f being FinSequence of bool the carrier of S st
( X = f . 1 & Y = 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 Def3 defines are_joinable PENCIL_2:def 3 :

theorem :: PENCIL_2:9

for S being TopStruct
for X, Y being Subset of S st X,Y are_joinable holds
ex f being one-to-one FinSequence of bool the carrier of S st
( X = f . 1 & Y = 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))) ) )

proof end;

theorem Th10: :: PENCIL_2:10

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

proof end;

theorem Th11: :: PENCIL_2:11

for I being non empty set
for A being PLS-yielding ManySortedSet of I
for X, Y being Subset of (Segre_Product A) st not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable holds
for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds
( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds
X1 . i = Y1 . i ) )

proof end;

theorem :: PENCIL_2:12

for S being 1-sorted
for T being non empty 1-sorted
for f being Function of S,T st f is bijective holds
f " is bijective

proof end;

definition

let S, T be TopStruct ;
let f be Function of S,T;
attr f is isomorphic means :Def4: :: PENCIL_2:def 4
( f is bijective & f is open & f " is bijective & f " is open );

end;

:: deftheorem Def4 defines isomorphic PENCIL_2:def 4 :

registration

let S be non empty TopStruct ;
cluster isomorphic M5(the carrier of S,the carrier of S);
existence

proof end;

end;

definition

let S be non empty TopStruct ;
mode Collineation of S is isomorphic Function of S,S;

end;

definition

let S be non empty non void TopStruct ;
let f be Collineation of S;
let l be Block of S;
:: original: .:
redefine func f .: l -> Block of S;
coherence

proof end;

end;

definition

let S be non empty non void TopStruct ;
let f be Collineation of S;
let l be Block of S;
:: original: "
redefine func f " l -> Block of S;
coherence

proof end;

end;

theorem Th13: :: PENCIL_2:13

for S being non empty TopStruct
for f being Collineation of S holds f " is Collineation of S

proof end;

theorem Th14: :: PENCIL_2:14

for S being non empty TopStruct
for f being Collineation of S
for X being Subset of S st not X is trivial holds
not f .: X is trivial

proof end;

theorem :: PENCIL_2:15

for S being non empty TopStruct
for f being Collineation of S
for X being Subset of S st not X is trivial holds
not f " X is trivial

proof end;

theorem Th16: :: PENCIL_2:16

for S being non empty non void TopStruct
for f being Collineation of S
for X being Subset of S st X is strong holds
f .: X is strong

proof end;

theorem :: PENCIL_2:17

for S being non empty non void TopStruct
for f being Collineation of S
for X being Subset of S st X is strong holds
f " X is strong

proof end;

theorem Th18: :: PENCIL_2:18

for S being non empty non void TopStruct
for f being Collineation of S
for X being Subset of S st X is closed_under_lines holds
f .: X is closed_under_lines

proof end;

theorem :: PENCIL_2:19

for S being non empty non void TopStruct
for f being Collineation of S
for X being Subset of S st X is closed_under_lines holds
f " X is closed_under_lines

proof end;

theorem Th20: :: PENCIL_2:20

for S being non empty non void TopStruct
for f being Collineation of S
for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds
f .: X,f .: Y are_joinable

proof end;

theorem :: PENCIL_2:21

for S being non empty non void TopStruct
for f being Collineation of S
for X, Y being Subset of S st not X is trivial & not Y is trivial & X,Y are_joinable holds
f " X,f " Y are_joinable

proof end;

theorem Th22: :: PENCIL_2:22

for I being non empty set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for W being Subset of (Segre_Product A) st not W is trivial & W is strong & W is closed_under_lines holds
union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } is Segre-Coset of A

proof end;

theorem Th23: :: PENCIL_2:23

for I being non empty set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for B being set holds
( B is Segre-Coset of A iff ex W being Subset of (Segre_Product A) st
( not W is trivial & W is strong & W is closed_under_lines & B = union { Y where Y is Subset of (Segre_Product A) : ( not Y is trivial & Y is strong & Y is closed_under_lines & W,Y are_joinable ) } ) )

proof end;

theorem Th24: :: PENCIL_2:24

for I being non empty set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for B being Segre-Coset of A
for f being Collineation of (Segre_Product A) holds f .: B is Segre-Coset of A

proof end;

theorem :: PENCIL_2:25

proof end;