begin
:: 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);
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
begin
theorem Th7:
:: 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 b3 being Subset of (Segre_Product A) holds
( b3 is Segre-Coset of A iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( b3 = product L & L . (indx L) = [#] (A . (indx L)) ) );
theorem Th8:
:: 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))) ) ) );
theorem
theorem Th10:
theorem Th11:
begin
theorem
:: 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 ) );
theorem Th13:
theorem Th14:
theorem
theorem Th16:
theorem
theorem Th18:
theorem
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem