:: On Segre's Product of Partial Line Spaces :: by Adam Naumowicz :: :: Received May 29, 2000 :: Copyright (c) 2000-2021 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;