:: On Segre's Product of Partial Line Spaces
:: by Adam Naumowicz
::
:: Received May 29, 2000
:: Copyright (c) 2000-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FUNCT_1, CARD_3, RELAT_1, XBOOLE_0, TARSKI, CARD_1,
ZFMISC_1, SUBSET_1, PRE_TOPC, STRUCT_0, RELAT_2, FINSEQ_1, NAT_1,
XXREAL_0, ARYTM_3, FINSET_1, SETFAM_1, PRALG_1, PBOOLE, FUNCOP_1,
WAYBEL_3, FUNCT_4, RLVECT_2, INTEGRA1, ARYTM_1, ORDINAL4, PENCIL_1,
WAYBEL18;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, XCMPLX_0, SETFAM_1,
CARD_1, ORDINAL1, NUMBERS, NAT_1, FINSET_1, RELAT_1, DOMAIN_1, STRUCT_0,
FUNCT_1, PBOOLE, FUNCT_7, WAYBEL_3, FINSEQ_1, CARD_3, PRE_TOPC, PZFMISC1,
FUNCOP_1, PRALG_1, XXREAL_0, WAYBEL18;
constructors PZFMISC1, REALSET2, PRALG_1, WAYBEL_3, POLYNOM1, PBOOLE, FUNCT_7,
FUNCT_4, RELSET_1, SETFAM_1, WAYBEL18;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, XREAL_0, CARD_3,
PZFMISC1, STRUCT_0, YELLOW_6, ORDINAL1, CARD_1, ZFMISC_1, PRE_POLY,
FUNCOP_1, WAYBEL18;
requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
begin
theorem :: PENCIL_1:1
for f,g being Function st product f = product g holds f is
non-empty implies g is non-empty;
theorem :: PENCIL_1:2
for X being set holds 2 c= card X iff ex x,y being object st x in X
& y in X & x<>y;
theorem :: PENCIL_1:3
for X being set st 2 c= card X for x being object ex y being object st
y in X & x<>y;
theorem :: PENCIL_1:4
for X being set holds 2 c= card X iff X is non trivial;
theorem :: 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;
theorem :: PENCIL_1:6
for X being set st 3 c= card X for x,y being object ex z being object
st z in X & x<>z & y<>z;
begin
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
:: PENCIL_1:def 1
x=y or ex l being Block of S st {x,y} c= l;
end;
definition
let S be TopStruct;
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;
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;
end;
definition
let S be TopStruct;
attr S is void means
:: PENCIL_1:def 4
the topology of S is empty;
attr S is degenerated means
:: PENCIL_1:def 5
the carrier of S is Block of S;
attr S is with_non_trivial_blocks means
:: PENCIL_1:def 6
for k being Block of S holds 2 c= card k;
attr S is identifying_close_blocks means
:: 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
:: PENCIL_1:def 8
ex x,y being Point of S st not x,y are_collinear;
attr S is without_isolated_points means
:: 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
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 strong 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 strong) & for i being Nat st 1 <= i &
i < len f holds 2 c= card((f.i) /\ (f.(i+1)));
end;
theorem :: PENCIL_1:7
for X being non empty set st 3 c= card X
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 S is non empty non void non degenerated non truly-partial
with_non_trivial_blocks identifying_close_blocks without_isolated_points;
theorem :: PENCIL_1:8
for X being non empty set st 3 c= card X
for K being Subset of X st card K = 2
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 S is non empty non void
non degenerated truly-partial with_non_trivial_blocks identifying_close_blocks
without_isolated_points;
registration
cluster strict non empty non void non degenerated non truly-partial
with_non_trivial_blocks identifying_close_blocks without_isolated_points
for TopStruct;
cluster strict non empty non void non degenerated truly-partial
with_non_trivial_blocks identifying_close_blocks without_isolated_points
for TopStruct;
end;
registration
let S be non void TopStruct;
cluster the topology of S -> non empty;
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;
end;
definition
mode PLS is non empty non void non degenerated with_non_trivial_blocks
identifying_close_blocks TopStruct;
end;
definition
::$CD
let F be Relation;
attr F is non-void-yielding means
:: PENCIL_1:def 14
for S being TopStruct st S in rng F holds S is non void;
end;
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;
end;
definition
let F be Relation;
attr F is trivial-yielding means
:: PENCIL_1:def 16
for S being set st S in rng F holds S is trivial;
end;
definition
let F be Relation;
attr F is non-Trivial-yielding means
:: PENCIL_1:def 17
for S being 1-sorted st S in rng F holds S is non trivial;
end;
registration
cluster non-Trivial-yielding -> non-Empty for Relation;
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;
end;
definition
let I be non empty set;
let A be TopStruct-yielding ManySortedSet of I;
let j be Element of I;
redefine func A.j -> TopStruct;
end;
definition
let F be Relation;
attr F is PLS-yielding means
:: PENCIL_1:def 19
for x being set st x in rng F holds x is PLS;
end;
registration
cluster PLS-yielding -> non-Empty TopStruct-yielding for Function;
cluster PLS-yielding -> non-void-yielding for TopStruct-yielding Function;
cluster PLS-yielding -> non-Trivial-yielding for
TopStruct-yielding Function;
end;
registration
let I be set;
cluster PLS-yielding for ManySortedSet of I;
end;
definition
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
let j be Element of I;
redefine func A.j -> PLS;
end;
definition
let I be set;
let A be ManySortedSet of I;
attr A is Segre-like means
:: 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;
end;
registration
let I be set;
let A be ManySortedSet of I;
cluster {A} -> trivial-yielding;
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 A+*(i,S) is non trivial-yielding
;
registration
let I be non empty set;
let A be ManySortedSet of I;
cluster {A} -> Segre-like;
end;
theorem :: PENCIL_1:10
for I being non empty set for A being ManySortedSet of I for i,S be
set holds {A}+*(i,S) is Segre-like;
theorem :: 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;
registration
let I be non empty set;
let A be non-Empty 1-sorted-yielding ManySortedSet of I;
cluster Segre-like trivial-yielding non-empty for
ManySortedSubset of Carrier A;
end;
registration
let I be non empty set;
let A be non-Trivial-yielding 1-sorted-yielding ManySortedSet of I;
cluster Segre-like non trivial-yielding non-empty for ManySortedSubset of
Carrier A;
end;
registration
let I be non empty set;
cluster Segre-like non trivial-yielding for ManySortedSet of I;
end;
definition
let I be non empty set;
let B be Segre-like non trivial-yielding ManySortedSet of I;
func indx(B) -> Element of I means
:: PENCIL_1:def 21
B.it is non trivial;
end;
theorem :: PENCIL_1:12
for I being non empty set for A being Segre-like non
trivial-yielding ManySortedSet of I for i being Element of I st i <> indx(A)
holds A.i is 1-element;
registration
let I be non empty set;
cluster Segre-like non trivial-yielding -> non-empty for ManySortedSet of I;
end;
theorem :: 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 non trivial-yielding;
registration
let I be non empty set;
let B be Segre-like non trivial-yielding ManySortedSet of I;
cluster product B -> non trivial;
end;
begin
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
:: 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;
end;
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#);
end;
theorem :: PENCIL_1:14
for I being non empty set for A be non-Empty TopStruct-yielding
ManySortedSet of I for x being Point of Segre_Product A holds x is
ManySortedSet of I;
theorem :: PENCIL_1:15
for I being non empty set for A being non-Empty
TopStruct-yielding ManySortedSet of I st ex i being Element of I st A.i is non
void holds Segre_Product A is non void;
theorem :: 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 A.i is
non degenerated & ex i being Element of I st A.i is non void holds
Segre_Product A is non degenerated;
theorem :: 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 & ex i being Element of I st A.i is non void holds
Segre_Product A is with_non_trivial_blocks;
theorem :: 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 with_non_trivial_blocks & ex i being Element of I st A
.i is non void holds Segre_Product A is identifying_close_blocks;
registration
let I be non empty set;
let A be PLS-yielding ManySortedSet of I;
cluster Segre_Product A -> non void non degenerated
with_non_trivial_blocks identifying_close_blocks;
end;
theorem :: PENCIL_1:19
for T being TopStruct for S being Subset of T holds S is trivial
implies S is strong closed_under_lines;
theorem :: PENCIL_1:20
for S being identifying_close_blocks TopStruct, l being Block of
S for L being Subset of S st L=l holds L is closed_under_lines;
theorem :: PENCIL_1:21
for S being TopStruct, l being Block of S for L being Subset of
S st L=l holds L is strong;
theorem :: PENCIL_1:22
for S being non void TopStruct holds [#]S is closed_under_lines;
theorem :: PENCIL_1:23
for I being non empty set for A being Segre-like non
trivial-yielding ManySortedSet of I for x,y being ManySortedSet of I st x in
product A & y in product A
for i being object st i <> indx(A) holds x.i = y.i;
theorem :: 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
Segre-like non trivial-yielding ManySortedSubset of Carrier A st x = product L
& L.indx(L) is Block of A.indx(L);
theorem :: 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 for i
being Element of I for p being Point of A.i holds P+*(i,p) is Point of
Segre_Product A;
theorem :: PENCIL_1:26
for I being non empty set for A,B being Segre-like non
trivial-yielding 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;
theorem :: PENCIL_1:27
for I being non empty set for A being Segre-like non
trivial-yielding ManySortedSet of I for N being non trivial set holds A+*(indx(
A),N) is Segre-like non trivial-yielding;
theorem :: PENCIL_1:28
for S being non empty non void identifying_close_blocks
without_isolated_points TopStruct holds S is strongly_connected implies S is
connected;
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 S is non trivial strong
closed_under_lines iff ex B being Segre-like non trivial-yielding
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 closed_under_lines;