Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### On Segre's Product of Partial Line Spaces

**by****Adam Naumowicz**- Received May 29, 2000
- MML identifier: PENCIL_1

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, CARD_3, ZF_REFLE, RELAT_1, BOOLE, CARD_1, REALSET1, PRE_TOPC, AMI_1, VECTSP_1, RELAT_2, FINSEQ_1, FINSET_1, SETFAM_1, PRALG_1, PBOOLE, FUNCOP_1, WAYBEL_3, FUNCT_4, RLVECT_2, MSUALG_2, INTEGRA1, SUBSET_1, ARYTM_1, PENCIL_1; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, SETFAM_1, NAT_1, FINSET_1, RELAT_1, STRUCT_0, FUNCT_1, REALSET1, WAYBEL_3, CARD_1, FINSEQ_1, CARD_3, PRE_TOPC, PBOOLE, MSUALG_1, MSUALG_2, PZFMISC1, PRE_CIRC, PRALG_1, POLYNOM1; constructors PRE_CIRC, WAYBEL_3, ENUMSET1, MSUALG_2, POLYNOM1, PZFMISC1, CQC_LANG; clusters STRUCT_0, RELSET_1, SUBSET_1, FINSET_1, YELLOW_6, PRALG_1, TEX_1, TEX_2, YELLOW13, REALSET1, PZFMISC1, XREAL_0, ARYTM_3, XBOOLE_0; 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 set 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 set ex y being set 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 set 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 set ex z being set 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; definition cluster strict non empty non void non degenerated non truly-partial with_non_trivial_blocks identifying_close_blocks without_isolated_points TopStruct; cluster strict non empty non void non degenerated truly-partial with_non_trivial_blocks identifying_close_blocks without_isolated_points TopStruct; end; definition 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 let F be Relation; attr F is TopStruct-yielding means :: PENCIL_1:def 13 for x being set st x in rng F holds x is TopStruct; end; definition cluster TopStruct-yielding -> 1-sorted-yielding Function; end; definition let I be set; cluster TopStruct-yielding ManySortedSet of I; end; definition cluster TopStruct-yielding Function; end; definition 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; definition cluster non-Trivial-yielding -> non-Empty 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; definition cluster PLS-yielding -> non-Empty TopStruct-yielding Function; cluster PLS-yielding -> non-void-yielding (TopStruct-yielding Function); cluster PLS-yielding -> non-Trivial-yielding (TopStruct-yielding Function); end; definition let I be set; cluster PLS-yielding 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 non empty trivial; end; definition 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; definition 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; definition let I be non empty set; let A be non-Empty (1-sorted-yielding ManySortedSet of I); cluster Segre-like trivial-yielding non-empty ManySortedSubset of Carrier A; end; definition 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 ManySortedSubset of Carrier A; end; definition let I be non empty set; cluster Segre-like non trivial-yielding 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 non empty trivial; definition let I be non empty set; cluster Segre-like non trivial-yielding -> non-empty 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; definition 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; definition let I be non empty set; let A be PLS-yielding ManySortedSet of I; redefine func Segre_Product A -> PLS; 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 set 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 set 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;

Back to top