Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### The Jonsson Theorem about the Representation of Modular Lattices

**by****Mariusz \Lapinski**- Received June 29, 2000
- MML identifier: LATTICE8

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_1, ORDERS_1, EQREL_1, LATTICES, FINSEQ_1, LATTICE5, WAYBEL_0, REALSET1, GROUP_6, FUNCT_1, FINSET_1, MATRIX_2, CAT_1, FILTER_2, BOOLE, YELLOW_0, ORDINAL2, ORDINAL1, PRE_TOPC, WELLORD1, SEQM_3, LATTICE3, WAYBEL_1, MCART_1, RELAT_2, TARSKI, ZFMISC_1, HAHNBAN, PARTFUN1, PRALG_1, FUNCT_6, SGRAPH1, LATTICE8; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, FUNCT_6, NUMBERS, XREAL_0, NAT_1, ORDINAL1, ORDINAL2, MCART_1, DOMAIN_1, PARTFUN1, PRALG_1, PRE_TOPC, STRUCT_0, GROUP_1, REALSET1, ORDERS_1, EQREL_1, FINSEQ_1, LATTICE3, BINOP_1, YELLOW_0, YELLOW_2, LATTICE5, YELLOW11, WAYBEL_1, WAYBEL_0, ABIAN; constructors NAT_1, DOMAIN_1, RFUNCT_3, LATTICE5, YELLOW11, ORDERS_3, YELLOW10, ABIAN, SCMPDS_1, MEMBERED, PRE_TOPC; clusters SUBSET_1, RELSET_1, STRUCT_0, INT_1, YELLOW_0, YELLOW_2, YELLOW11, CARD_1, ORDINAL1, PRALG_1, LATTICE3, LATTICE5, WAYBEL10, WAYBEL21, REALSET1, EQREL_1, LATTICE7, FINSEQ_6, ABIAN, ARYTM_3, MEMBERED, PARTFUN1, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: Preliminaries definition let A be non empty set; let P,R be Relation of A; redefine pred P c= R means :: LATTICE8:def 1 for a,b being Element of A st [a,b] in P holds [a,b] in R; end; definition let L be RelStr; attr L is finitely_typed means :: LATTICE8:def 2 ex A being non empty set st (for e being set st e in the carrier of L holds e is Equivalence_Relation of A) & ex o being Nat st for e1,e2 being Equivalence_Relation of A, x,y being set st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of A st len F = o & x,y are_joint_by F,e1,e2; end; definition let L be lower-bounded LATTICE; let n be Nat; pred L has_a_representation_of_type<= n means :: LATTICE8:def 3 ex A being non trivial set, f be Homomorphism of L,EqRelLATT A st f is one-to-one & Image f is finitely_typed & (ex e being Equivalence_Relation of A st e in the carrier of Image f & e <> id A) & type_of Image f <= n; end; definition cluster lower-bounded distributive finite LATTICE; end; definition let A be non trivial set; cluster non trivial finitely_typed full (non empty Sublattice of EqRelLATT A); end; theorem :: LATTICE8:1 for A be non empty set for L be lower-bounded LATTICE for d be distance_function of A,L holds succ {} c= DistEsti(d); theorem :: LATTICE8:2 for L being trivial Semilattice holds L is modular; theorem :: LATTICE8:3 for A being non empty set for L being non empty Sublattice of EqRelLATT A holds L is trivial or ex e being Equivalence_Relation of A st e in the carrier of L & e <> id A; theorem :: LATTICE8:4 for L1,L2 be lower-bounded LATTICE for f being map of L1,L2 st f is infs-preserving sups-preserving holds f is meet-preserving join-preserving; theorem :: LATTICE8:5 for L1,L2 be lower-bounded LATTICE st L1,L2 are_isomorphic & L1 is modular holds L2 is modular; theorem :: LATTICE8:6 for S being lower-bounded non empty Poset for T being non empty Poset for f being monotone map of S,T holds Image f is lower-bounded; theorem :: LATTICE8:7 for L being lower-bounded LATTICE for x,y being Element of L for A being non empty set for f be Homomorphism of L,EqRelLATT A st f is one-to-one holds (corestr f).x <= (corestr f).y implies x <= y; begin :: J\'onsson theorem ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: => :: L has_a_representation_of_type<= 2 implies L is modular :: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: theorem :: LATTICE8:8 for A being non trivial set for L being finitely_typed full (non empty Sublattice of EqRelLATT A) for e being Equivalence_Relation of A st e in the carrier of L & e <> id A holds type_of L <= 2 implies L is modular; theorem :: LATTICE8:9 for L be lower-bounded LATTICE holds L has_a_representation_of_type<= 2 implies L is modular; ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: <= :: L is modular implies L has_a_representation_of_type<= 2 :: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: definition let A be set; func new_set2 A equals :: LATTICE8:def 4 A \/ {{A}, {{A}}}; end; definition let A be set; cluster new_set2 A -> non empty; end; definition let A be non empty set; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be Element of [:A,A,the carrier of L,the carrier of L:]; func new_bi_fun2(d,q) -> BiFunction of new_set2 A,L means :: LATTICE8:def 5 (for u,v being Element of A holds it.(u,v) = d.(u,v)) & it.({A},{A}) = Bottom L & it.({{A}},{{A}}) = Bottom L & it.({A},{{A}}) = (d.(q`1,q`2)"\/"q`3)"/\"q`4 & it.({{A}},{A}) = (d.(q`1,q`2)"\/"q`3)"/\"q`4 & for u being Element of A holds (it.(u,{A}) = d.(u,q`1)"\/"q`3 & it.({A},u) = d.(u,q`1)"\/"q`3 & it.(u,{{A}}) = d.(u,q`2)"\/"q`3 & it.({{A}},u) = d.(u,q`2)"\/"q`3); end; theorem :: LATTICE8:10 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L st d is zeroed for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun2(d,q) is zeroed; theorem :: LATTICE8:11 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L st d is symmetric for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun2(d,q) is symmetric; theorem :: LATTICE8:12 for A being non empty set for L being lower-bounded LATTICE st L is modular for d being BiFunction of A,L st d is symmetric & d is u.t.i. for q being Element of [:A,A,the carrier of L,the carrier of L:] st d.(q`1,q`2) <= q`3"\/"q`4 holds new_bi_fun2(d,q) is u.t.i.; theorem :: LATTICE8:13 for A be set holds A c= new_set2 A; theorem :: LATTICE8:14 for A being non empty set for L being lower-bounded LATTICE for d be BiFunction of A,L for q be Element of [:A,A,the carrier of L,the carrier of L:] holds d c= new_bi_fun2(d,q); reserve x,y for set, C for Ordinal, L0,L1 for T-Sequence; definition let A be non empty set; let O be Ordinal; func ConsecutiveSet2(A,O) means :: LATTICE8:def 6 ex L0 being T-Sequence st it = last L0 & dom L0 = succ O & L0.{} = A & (for C being Ordinal st succ C in succ O holds L0.succ C = new_set2(L0.C)) & for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds L0.C = union rng (L0|C); end; theorem :: LATTICE8:15 for A being non empty set holds ConsecutiveSet2(A,{}) = A; theorem :: LATTICE8:16 for A being non empty set for O being Ordinal holds ConsecutiveSet2(A,succ O) = new_set2 ConsecutiveSet2(A,O); theorem :: LATTICE8:17 for A being non empty set for O being Ordinal for T being T-Sequence holds O <> {} & O is_limit_ordinal & dom T = O & (for O1 being Ordinal st O1 in O holds T.O1 = ConsecutiveSet2(A,O1)) implies ConsecutiveSet2(A,O) = union rng T; reserve O1,O2 for Ordinal; definition let A be non empty set; let O be Ordinal; cluster ConsecutiveSet2(A,O) -> non empty; end; theorem :: LATTICE8:18 for A being non empty set for O being Ordinal holds A c= ConsecutiveSet2(A,O); definition let A be non empty set; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be QuadrSeq of d; let O be Ordinal; assume O in dom q; func Quadr2(q,O) -> Element of [:ConsecutiveSet2(A,O),ConsecutiveSet2(A,O), the carrier of L,the carrier of L:] equals :: LATTICE8:def 7 q.O; end; definition let A be non empty set; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be QuadrSeq of d; let O be Ordinal; func ConsecutiveDelta2(q,O) means :: LATTICE8:def 8 ex L0 being T-Sequence st it = last L0 & dom L0 = succ O & L0.{} = d & (for C being Ordinal st succ C in succ O holds L0.succ C = new_bi_fun2(BiFun(L0.C,ConsecutiveSet2(A,C),L),Quadr2(q,C))) & for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds L0.C = union rng(L0|C); end; theorem :: LATTICE8:19 for A being non empty set for L be lower-bounded LATTICE for d being BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta2(q,{}) = d; theorem :: LATTICE8:20 for A being non empty set for L be lower-bounded LATTICE for d be BiFunction of A,L for q being QuadrSeq of d for O being Ordinal holds ConsecutiveDelta2(q,succ O) = new_bi_fun2(BiFun(ConsecutiveDelta2(q,O), ConsecutiveSet2(A,O),L),Quadr2(q,O)); theorem :: LATTICE8:21 for A being non empty set for L be lower-bounded LATTICE for d be BiFunction of A,L for q being QuadrSeq of d for T being T-Sequence for O being Ordinal holds O <> {} & O is_limit_ordinal & dom T = O & (for O1 being Ordinal st O1 in O holds T.O1 = ConsecutiveDelta2(q,O1)) implies ConsecutiveDelta2(q,O) = union rng T; theorem :: LATTICE8:22 for A being non empty set for O,O1,O2 being Ordinal holds O1 c= O2 implies ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,O2); theorem :: LATTICE8:23 for A being non empty set for L be lower-bounded LATTICE for d be BiFunction of A,L for q being QuadrSeq of d for O being Ordinal holds ConsecutiveDelta2(q,O) is BiFunction of ConsecutiveSet2(A,O),L; definition let A be non empty set; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be QuadrSeq of d; let O be Ordinal; redefine func ConsecutiveDelta2(q,O) -> BiFunction of ConsecutiveSet2(A,O),L; end; theorem :: LATTICE8:24 for A being non empty set for L be lower-bounded LATTICE for d be BiFunction of A,L for q being QuadrSeq of d for O being Ordinal holds d c= ConsecutiveDelta2(q,O); theorem :: LATTICE8:25 for A being non empty set for L be lower-bounded LATTICE for d being BiFunction of A,L for O1,O2 being Ordinal for q being QuadrSeq of d st O1 c= O2 holds ConsecutiveDelta2(q,O1) c= ConsecutiveDelta2(q,O2); theorem :: LATTICE8:26 for A being non empty set for L be lower-bounded LATTICE for d be BiFunction of A,L st d is zeroed for q being QuadrSeq of d for O being Ordinal holds ConsecutiveDelta2(q,O) is zeroed; theorem :: LATTICE8:27 for A being non empty set for L be lower-bounded LATTICE for d be BiFunction of A,L st d is symmetric for q being QuadrSeq of d for O being Ordinal holds ConsecutiveDelta2(q,O) is symmetric; theorem :: LATTICE8:28 for A being non empty set for L being lower-bounded LATTICE st L is modular for d be BiFunction of A,L st d is symmetric u.t.i. for O being Ordinal for q being QuadrSeq of d st O c= DistEsti(d) holds ConsecutiveDelta2(q,O) is u.t.i.; theorem :: LATTICE8:29 for A being non empty set for L being lower-bounded modular LATTICE for d being distance_function of A,L for O being Ordinal for q being QuadrSeq of d st O c= DistEsti(d) holds ConsecutiveDelta2(q,O) is distance_function of ConsecutiveSet2(A,O),L; definition let A be non empty set; let L be lower-bounded LATTICE; let d be BiFunction of A,L; func NextSet2(d) equals :: LATTICE8:def 9 ConsecutiveSet2(A,DistEsti(d)); end; definition let A be non empty set; let L be lower-bounded LATTICE; let d be BiFunction of A,L; cluster NextSet2(d) -> non empty; end; definition let A be non empty set; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be QuadrSeq of d; func NextDelta2(q) equals :: LATTICE8:def 10 ConsecutiveDelta2(q,DistEsti(d)); end; definition let A be non empty set; let L be lower-bounded modular LATTICE; let d be distance_function of A,L; let q be QuadrSeq of d; redefine func NextDelta2(q) -> distance_function of NextSet2(d),L; end; definition let A be non empty set; let L be lower-bounded LATTICE; let d be distance_function of A,L; let Aq be non empty set; let dq be distance_function of Aq,L; pred Aq, dq is_extension2_of A,d means :: LATTICE8:def 11 ex q being QuadrSeq of d st Aq = NextSet2(d) & dq = NextDelta2(q); end; theorem :: LATTICE8:30 for A being non empty set for L be lower-bounded LATTICE for d be distance_function of A,L for Aq be non empty set for dq be distance_function of Aq,L st Aq, dq is_extension2_of A,d for x,y being Element of A, a,b being Element of L st d.(x,y) <= a "\/" b ex z1,z2 being Element of Aq st dq.(x,z1) = a & dq.(z1,z2) = (d.(x,y) "\/" a) "/\" b & dq.(z2,y) = a; definition let A be non empty set; let L be lower-bounded modular LATTICE; let d be distance_function of A,L; mode ExtensionSeq2 of A,d -> Function means :: LATTICE8:def 12 dom it = NAT & it.0 = [A,d] & for n being Nat holds ex A' being non empty set, d' being distance_function of A',L, Aq being non empty set, dq being distance_function of Aq,L st Aq, dq is_extension2_of A',d' & it.n = [A',d'] & it.(n+1) = [Aq,dq]; end; theorem :: LATTICE8:31 for A being non empty set for L be lower-bounded modular LATTICE for d be distance_function of A,L for S being ExtensionSeq2 of A,d for k,l being Nat st k <= l holds (S.k)`1 c= (S.l)`1; theorem :: LATTICE8:32 for A being non empty set for L be lower-bounded modular LATTICE for d be distance_function of A,L for S being ExtensionSeq2 of A,d for k,l being Nat st k <= l holds (S.k)`2 c= (S.l)`2; theorem :: LATTICE8:33 for L be lower-bounded modular LATTICE for S being ExtensionSeq2 of the carrier of L, BasicDF(L) for FS being non empty set st FS = union { (S.i)`1 where i is Nat: not contradiction} holds union { (S.i)`2 where i is Nat: not contradiction} is distance_function of FS,L; theorem :: LATTICE8:34 for L be lower-bounded modular LATTICE for S being ExtensionSeq2 of the carrier of L, BasicDF(L) for FS being non empty set for FD being distance_function of FS,L for x,y being Element of FS for a,b being Element of L st FS = union { (S.i)`1 where i is Nat: not contradiction} & FD = union { (S.i)`2 where i is Nat: not contradiction} & FD.(x,y) <= a"\/"b ex z1,z2 being Element of FS st FD.(x,z1) = a & FD.(z1,z2) = (FD.(x,y)"\/"a)"/\"b & FD.(z2,y) = a; theorem :: LATTICE8:35 for L be lower-bounded modular LATTICE for S being ExtensionSeq2 of the carrier of L, BasicDF(L) for FS being non empty set for FD being distance_function of FS,L for f being Homomorphism of L,EqRelLATT FS for e1,e2 being Equivalence_Relation of FS for x,y being set st f = alpha FD & FS = union { (S.i)`1 where i is Nat: not contradiction} & FD = union { (S.i)`2 where i is Nat: not contradiction} & e1 in the carrier of Image f & e2 in the carrier of Image f & [x,y] in e1 "\/" e2 ex F being non empty FinSequence of FS st len F = 2+2 & x,y are_joint_by F,e1,e2; theorem :: LATTICE8:36 for L be lower-bounded modular LATTICE holds L has_a_representation_of_type<= 2; ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: <=> :: L has_a_representation_of_type<= 2 iff L is modular :: ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: theorem :: LATTICE8:37 for L be lower-bounded LATTICE holds L has_a_representation_of_type<= 2 iff L is modular;

Back to top