:: by Adam Naumowicz

::

:: Received August 14, 2001

:: Copyright (c) 2001-2012 Association of Mizar Users

begin

definition

let D be set ;

let p be FinSequence of D;

let i, j be Nat;

coherence

(p | (i -' 1)) ^ (p /^ j) is FinSequence of D ;

end;
let p be FinSequence of D;

let i, j be Nat;

coherence

(p | (i -' 1)) ^ (p /^ j) is FinSequence of D ;

:: deftheorem defines Del PENCIL_2:def 1 :

for D being set

for p being FinSequence of D

for i, j being Nat holds Del (p,i,j) = (p | (i -' 1)) ^ (p /^ j);

for D being set

for p being FinSequence of D

for i, j being Nat holds Del (p,i,j) = (p | (i -' 1)) ^ (p /^ j);

theorem Th1: :: PENCIL_2:1

for D being set

for p being FinSequence of D

for i, j being Element of NAT holds rng (Del (p,i,j)) c= rng p

for p being FinSequence of D

for i, j being Element of 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 Element of NAT st i in dom p & j in dom p holds

len (Del (p,i,j)) = (((len p) - j) + i) - 1

for p being FinSequence of D

for i, j being Element of 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 Element of NAT st i in dom p & j in dom p & len (Del (p,i,j)) = 0 holds

( i = 1 & j = len p )

for p being FinSequence of D

for i, j being Element of 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 Element of NAT st i in dom p & 1 <= k & k <= i - 1 holds

(Del (p,i,j)) . k = p . k

for p being FinSequence of D

for i, j, k being Element of 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 Element of NAT st (len p) + 1 <= k holds

(p ^ q) . k = q . (k - (len p))

for k being Element of 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 Element of 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)

for p being FinSequence of D

for i, j, k being Element of 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_{1}() -> set , F_{2}() -> set , F_{3}() -> set , F_{4}() -> FinSequence of F_{3}(), P_{1}[ set , set ] } :

FinSeqOneToOne{ F

ex g being one-to-one FinSequence of F_{3}() st

( F_{1}() = g . 1 & F_{2}() = g . (len g) & rng g c= rng F_{4}() & ( for j being Element of NAT st 1 <= j & j < len g holds

P_{1}[g . j,g . (j + 1)] ) )

provided( F

P

A1:
( F_{1}() = F_{4}() . 1 & F_{2}() = F_{4}() . (len F_{4}()) )
and

A2: for i being Element of NAT

for d1, d2 being set st 1 <= i & i < len F_{4}() & d1 = F_{4}() . i & d2 = F_{4}() . (i + 1) holds

P_{1}[d1,d2]

A2: for i being Element of NAT

for d1, d2 being set st 1 <= i & i < len F

P

proof end;

begin

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

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;

ex b_{1} being Subset of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st

( b_{1} = product L & L . (indx L) = [#] (A . (indx L)) )

end;
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 ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st

( it = product L & L . (indx L) = [#] (A . (indx L)) );

ex b

( b

proof end;

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

for I being non empty set

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

for b_{3} being Subset of (Segre_Product A) holds

( b_{3} is Segre-Coset of A iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st

( b_{3} = product L & L . (indx L) = [#] (A . (indx L)) ) );

for I being non empty set

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

for b

( b

( b

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

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;

end;
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 Element of NAT st 1 <= i & i < len f holds

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

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 Element of NAT st 1 <= i & i < len f holds

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

:: deftheorem Def3 defines are_joinable PENCIL_2:def 3 :

for S being TopStruct

for X, Y being Subset of S holds

( X,Y are_joinable iff 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 Element of NAT st 1 <= i & i < len f holds

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

for S being TopStruct

for X, Y being Subset of S holds

( X,Y are_joinable iff 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 Element of NAT st 1 <= i & i < len f holds

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

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 Element of NAT st 1 <= i & i < len f holds

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

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

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

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;

begin

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

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;

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

( f is bijective & f is open & f " is bijective & f " is open );

:: deftheorem Def4 defines isomorphic PENCIL_2:def 4 :

for S, T being TopStruct

for f being Function of S,T holds

( f is isomorphic iff ( f is bijective & f is open & f " is bijective & f " is open ) );

for S, T being TopStruct

for f being Function of S,T holds

( f is isomorphic iff ( f is bijective & f is open & f " is bijective & f " is open ) );

registration

let S be non empty TopStruct ;

ex b_{1} being Function of S,S st b_{1} is isomorphic

end;
cluster Relation-like the carrier of S -defined the carrier of S -valued Function-like non empty total quasi_total isomorphic for Element of bool [: the carrier of S, the carrier of S:];

existence ex b

proof 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

f .: l is Block of S

end;
let f be Collineation of S;

let l be Block of S;

:: original: .:

redefine func f .: l -> Block of S;

coherence

f .: l is Block of S

proof 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

f " l is Block of S

end;
let f be Collineation of S;

let l be Block of S;

:: original: "

redefine func f " l -> Block of S;

coherence

f " l is Block 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

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

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

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

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

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

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

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

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

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

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

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

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

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;