:: J\'onsson Theorem :: by Jaros{\l}aw Gryko :: :: Received November 13, 1997 :: Copyright (c) 1997-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, FUNCOP_1, TARSKI, RELAT_1, FUNCT_6, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDERS_2, LATTICE3, MSUALG_5, STRUCT_0, EQREL_1, PBOOLE, LATTICES, XXREAL_0, REWRITE1, SETFAM_1, RELAT_2, WAYBEL_0, GROUP_6, YELLOW_0, ORDINAL2, FINSEQ_1, ARYTM_3, ABIAN, FINSEQ_2, ARYTM_1, CARD_1, ORDINAL4, NAT_1, VALUED_0, FUNCT_2, MCART_1, PARTFUN1, LATTICE5, RECDEF_2; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, FUNCT_2, FUNCT_6, CARD_1, XCMPLX_0, ORDINAL1, NUMBERS, NAT_1, NAT_D, SETFAM_1, ORDINAL2, MCART_1, DOMAIN_1, PARTFUN1, FUNCOP_1, STRUCT_0, ORDERS_2, EQREL_1, MSUALG_5, FINSEQ_1, FINSEQ_2, SEQ_4, LATTICES, LATTICE3, BINOP_1, YELLOW_0, WAYBEL_0, YELLOW_2, ABIAN, XXREAL_0; constructors SETFAM_1, BINOP_1, DOMAIN_1, ORDINAL2, NAT_1, CLASSES1, SEQ_4, FINSOP_1, FUNCT_6, RFUNCT_3, BINARITH, ABIAN, LATTICE3, MSUALG_5, YELLOW_2, NAT_D, RELSET_1, XTUPLE_0, NUMBERS, XFAMILY; registrations XBOOLE_0, SUBSET_1, ORDINAL1, PARTFUN1, FUNCOP_1, XREAL_0, CARD_1, MEMBERED, FINSEQ_1, ABIAN, STRUCT_0, LATTICES, LATTICE3, YELLOW_0, YELLOW_1, RELAT_1, XXREAL_2, RELSET_1, FINSEQ_2, FUNCT_1, XTUPLE_0; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries theorem :: LATTICE5:1 for f being Function, F being Function-yielding Function st f = union rng F holds dom f = union rng doms F; theorem :: LATTICE5:2 for A,B being non empty set holds [:union A, union B:] = union { [:a,b:] where a is Element of A, b is Element of B : a in A & b in B }; theorem :: LATTICE5:3 for A being non empty set st A is c=-linear holds [:union A, union A:] = union { [:a,a:] where a is Element of A : a in A }; begin :: An equivalence lattice of a set reserve X for non empty set; definition let A be set; func EqRelLATT A -> Poset equals :: LATTICE5:def 1 LattPOSet EqRelLatt A; end; registration let A be set; cluster EqRelLATT A -> with_infima with_suprema; end; theorem :: LATTICE5:4 for A, x being set holds x in the carrier of EqRelLATT A iff x is Equivalence_Relation of A; theorem :: LATTICE5:5 for A being set, x,y being Element of EqRelLatt A holds x [= y iff x c= y; theorem :: LATTICE5:6 for A being set, a,b being Element of EqRelLATT A holds a <= b iff a c= b; theorem :: LATTICE5:7 for L being Lattice, a,b being Element of LattPOSet L holds a "/\" b = %a "/\" %b; theorem :: LATTICE5:8 for A being set, a,b being Element of EqRelLATT A holds a "/\" b = a /\ b; theorem :: LATTICE5:9 for L being Lattice, a,b being Element of LattPOSet L holds a "\/" b = %a "\/" %b; theorem :: LATTICE5:10 for A being set, a,b being Element of EqRelLATT A for E1,E2 being Equivalence_Relation of A st a = E1 & b = E2 holds a "\/" b = E1 "\/" E2; definition let L be non empty RelStr; redefine attr L is complete means :: LATTICE5:def 2 for X being Subset of L ex a being Element of L st a is_<=_than X & for b being Element of L st b is_<=_than X holds b <= a; end; registration let A be set; cluster EqRelLATT A -> complete; end; begin :: A type of a sublattice of equivalence lattice of a set registration let L1,L2 be LATTICE; cluster meet-preserving join-preserving for Function of L1,L2; end; definition let L1,L2 be LATTICE; mode Homomorphism of L1,L2 is meet-preserving join-preserving Function of L1,L2; end; registration let L be LATTICE; cluster meet-inheriting join-inheriting strict for SubRelStr of L; end; definition let L be non empty RelStr; mode Sublattice of L is meet-inheriting join-inheriting SubRelStr of L; end; registration let L1, L2 be LATTICE; let f be Homomorphism of L1,L2; cluster Image f -> meet-inheriting join-inheriting; end; reserve e,e1,e2,e19,e29 for Equivalence_Relation of X, x,y,x9,y9 for set; definition let X; let f be non empty FinSequence of X; let x,y be object; let R1, R2 be Relation; pred x,y are_joint_by f,R1,R2 means :: LATTICE5:def 3 f.1 = x & f.(len f) = y & for i being Element of NAT st 1 <= i & i < len f holds (i is odd implies [f.i,f.(i+1) ] in R1) & (i is even implies [f.i,f.(i+1)] in R2); end; theorem :: LATTICE5:11 for x being set, o being Element of NAT, R1,R2 being Relation, f being non empty FinSequence of X st R1 is_reflexive_in X & R2 is_reflexive_in X & f = o |-> x holds x,x are_joint_by f,R1,R2; theorem :: LATTICE5:12 for x,y being object, R1,R2 being Relation, n,m being Element of NAT st (n <= m & R1 is_reflexive_in X & R2 is_reflexive_in X & ex f being non empty FinSequence of X st len f = n & x,y are_joint_by f,R1,R2) ex h being non empty FinSequence of X st len h = m & x,y are_joint_by h,R1,R2; definition let X; let Y be Sublattice of EqRelLATT X; given e such that e in the carrier of Y and e <> id X; given o being Element of NAT such that for e1,e2 for x,y being object st e1 in the carrier of Y & e2 in the carrier of Y & [ x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st len F = o & x ,y are_joint_by F,e1,e2; func type_of Y -> Element of NAT means :: LATTICE5:def 4 (for e1,e2 for x,y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds (ex F being non empty FinSequence of X st len F = it+2 & x,y are_joint_by F,e1,e2)) & ex e1,e2 st ex x,y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & not (ex F being non empty FinSequence of X st len F = it+1 & x,y are_joint_by F,e1,e2); end; theorem :: LATTICE5:13 for Y being Sublattice of EqRelLATT X, n being Element of NAT st (ex e st e in the carrier of Y & e <> id X) & (for e1,e2 for x,y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds (ex F being non empty FinSequence of X st len F = n+2 & x,y are_joint_by F,e1,e2)) holds type_of Y <= n; begin :: A meet-representation of a lattice reserve A for non empty set, L for lower-bounded LATTICE; definition let A be set, L be 1-sorted; mode BiFunction of A,L is Function of [:A,A:],the carrier of L; end; definition let A be non empty set, L be 1-sorted; let f be BiFunction of A,L; let x,y be Element of A; redefine func f.(x,y) -> Element of L; end; definition let A; let L be 1-sorted; let f be BiFunction of A,L; attr f is symmetric means :: LATTICE5:def 5 for x,y being Element of A holds f.(x,y) = f.(y,x); end; definition let A,L; let f be BiFunction of A,L; attr f is zeroed means :: LATTICE5:def 6 for x being Element of A holds f.(x,x) = Bottom L; attr f is u.t.i. means :: LATTICE5:def 7 for x,y,z being Element of A holds f.(x,y) "\/" f.(y,z) >= f.(x,z); end; :: f is u.t.i. means that f satisfies the triangle inequality registration let A, L; cluster symmetric zeroed u.t.i. for BiFunction of A,L; end; definition let A, L; mode distance_function of A,L is symmetric zeroed u.t.i. BiFunction of A,L; end; definition let A, L; let d be distance_function of A,L; func alpha d -> Function of L,EqRelLATT A means :: LATTICE5:def 8 for e being Element of L ex E being Equivalence_Relation of A st E = it.e & for x,y be Element of A holds [x,y] in E iff d.(x,y) <= e; end; theorem :: LATTICE5:14 for d being distance_function of A,L holds alpha d is meet-preserving; theorem :: LATTICE5:15 for d being distance_function of A,L st d is onto holds alpha d is one-to-one ; begin :: J\'onsson theorem definition let A be set; func new_set A -> set equals :: LATTICE5:def 9 A \/ {{A}, {{A}}, {{{A}}} }; end; registration let A be set; cluster new_set A -> non empty; end; definition let A,L; 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_fun(d,q) -> BiFunction of new_set A,L means :: LATTICE5:def 10 (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}}}) = Bottom L & it.({{A}},{{{A}}}) = q`3_4 & it.({{{A}}},{{A}}) = q`3_4 & it.({A},{{A}}) = q`4_4 & it.({{A}},{A}) = q`4_4 & it.({A},{{{A}}}) = (q`3_4)"\/"(q`4_4) & it.({{{A}}},{A}) = (q`3_4)"\/"(q`4_4) & for u being Element of A holds it.(u,{A}) = d.(u,q`1_4)"\/"(q`3_4) & it.({A},u) = d.(u,q`1_4)"\/"(q`3_4) & it.(u,{{A}}) = d.(u,q`1_4)"\/"(q`3_4)"\/"(q`4_4) & it.({{A}},u) = d.(u,q`1_4)"\/"(q`3_4) "\/" (q`4_4) & it.(u,{{{A}}}) = d.(u,q`2_4)"\/"(q`4_4) & it.({{{A}}},u) = d.(u,q`2_4)"\/"(q`4_4); end; theorem :: LATTICE5:16 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_fun(d,q) is zeroed; theorem :: LATTICE5:17 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_fun(d,q) is symmetric; theorem :: LATTICE5:18 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_4,q`2_4) <= (q`3_4)"\/"(q`4_4) holds new_bi_fun(d,q) is u.t.i.; theorem :: LATTICE5:19 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_fun(d,q); definition let A,L; let d be BiFunction of A,L; func DistEsti(d) -> Cardinal means :: LATTICE5:def 11 it,{ [x,y,a,b] where x is Element of A, y is Element of A, a is Element of L, b is Element of L: d.(x,y) <= a"\/" b} are_equipotent; end; theorem :: LATTICE5:20 for d be distance_function of A,L holds DistEsti(d) <> {}; reserve T,L1 for Sequence, O,O1,O2,O3,C for Ordinal; definition let A; let O; func ConsecutiveSet(A,O) -> set means :: LATTICE5:def 12 ex L0 being Sequence st it = last L0 & dom L0 = succ O & L0.0 = A & (for C being Ordinal st succ C in succ O holds L0.succ C = new_set L0.C) & for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds L0.C = union rng (L0|C); end; theorem :: LATTICE5:21 ConsecutiveSet(A,0) = A; theorem :: LATTICE5:22 ConsecutiveSet(A,succ O) = new_set ConsecutiveSet(A,O); theorem :: LATTICE5:23 O <> 0 & O is limit_ordinal & dom T = O & (for O1 being Ordinal st O1 in O holds T.O1 = ConsecutiveSet(A,O1)) implies ConsecutiveSet(A,O) = union rng T; registration let A; let O; cluster ConsecutiveSet(A,O) -> non empty; end; theorem :: LATTICE5:24 A c= ConsecutiveSet(A,O); definition let A,L; let d be BiFunction of A,L; mode QuadrSeq of d -> Sequence of [:A,A,the carrier of L,the carrier of L :] means :: LATTICE5:def 13 dom it is Cardinal & it is one-to-one & rng it ={[x,y,a,b] where x is Element of A, y is Element of A, a is Element of L, b is Element of L: d.(x,y) <= a"\/"b}; end; definition let A,L; let d be BiFunction of A,L; let q be QuadrSeq of d; let O; assume O in dom q; func Quadr(q,O) -> Element of [:ConsecutiveSet(A,O),ConsecutiveSet(A,O), the carrier of L,the carrier of L:] equals :: LATTICE5:def 14 q.O; end; theorem :: LATTICE5:25 for d being BiFunction of A,L, q being QuadrSeq of d holds O in DistEsti(d) iff O in dom q; definition let A,L; let z be set; assume z is BiFunction of A,L; func BiFun(z,A,L) -> BiFunction of A,L equals :: LATTICE5:def 15 z; end; definition let A,L; let d be BiFunction of A,L; let q be QuadrSeq of d; let O; func ConsecutiveDelta(q,O) -> set means :: LATTICE5:def 16 ex L0 being Sequence st it = last L0 & dom L0 = succ O & L0.0 = d & (for C being Ordinal st succ C in succ O holds L0.succ C = new_bi_fun(BiFun(L0.C,ConsecutiveSet(A,C),L),Quadr(q,C))) & for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds L0.C = union rng(L0|C); end; theorem :: LATTICE5:26 for d being BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta(q,0) = d; theorem :: LATTICE5:27 for d be BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta(q,succ O) = new_bi_fun(BiFun(ConsecutiveDelta(q,O), ConsecutiveSet(A,O),L),Quadr(q,O)); theorem :: LATTICE5:28 for d be BiFunction of A,L for q being QuadrSeq of d holds O <> 0 & O is limit_ordinal & dom T = O & (for O1 being Ordinal st O1 in O holds T. O1 = ConsecutiveDelta(q,O1)) implies ConsecutiveDelta(q,O) = union rng T; theorem :: LATTICE5:29 O1 c= O2 implies ConsecutiveSet(A,O1) c= ConsecutiveSet(A,O2); theorem :: LATTICE5:30 for d be BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta(q,O) is BiFunction of ConsecutiveSet(A,O),L; definition let A,L; let d be BiFunction of A,L; let q be QuadrSeq of d; let O; redefine func ConsecutiveDelta(q,O) -> BiFunction of ConsecutiveSet(A,O),L; end; theorem :: LATTICE5:31 for d be BiFunction of A,L for q being QuadrSeq of d holds d c= ConsecutiveDelta(q,O); theorem :: LATTICE5:32 for d being BiFunction of A,L for q being QuadrSeq of d st O1 c= O2 holds ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,O2); theorem :: LATTICE5:33 for d be BiFunction of A,L st d is zeroed for q being QuadrSeq of d holds ConsecutiveDelta(q,O) is zeroed; theorem :: LATTICE5:34 for d be BiFunction of A,L st d is symmetric for q being QuadrSeq of d holds ConsecutiveDelta(q,O) is symmetric; theorem :: LATTICE5:35 for d be BiFunction of A,L st d is symmetric u.t.i. for q being QuadrSeq of d st O c= DistEsti(d) holds ConsecutiveDelta(q,O) is u.t.i.; theorem :: LATTICE5:36 for d being distance_function of A,L for q being QuadrSeq of d st O c= DistEsti(d) holds ConsecutiveDelta(q,O) is distance_function of ConsecutiveSet( A,O),L; definition let A,L; let d be BiFunction of A,L; func NextSet(d) -> set equals :: LATTICE5:def 17 ConsecutiveSet(A,DistEsti(d)); end; registration let A,L; let d be BiFunction of A,L; cluster NextSet(d) -> non empty; end; definition let A,L; let d be BiFunction of A,L; let q be QuadrSeq of d; func NextDelta(q) -> set equals :: LATTICE5:def 18 ConsecutiveDelta(q,DistEsti(d)); end; definition let A,L; let d be distance_function of A,L; let q be QuadrSeq of d; redefine func NextDelta(q) -> distance_function of NextSet(d),L; end; definition let A,L; let d be distance_function of A,L; let Aq be non empty set, dq be distance_function of Aq,L; pred Aq, dq is_extension_of A,d means :: LATTICE5:def 19 ex q being QuadrSeq of d st Aq = NextSet(d) & dq = NextDelta(q); end; theorem :: LATTICE5:37 for d be distance_function of A,L for Aq be non empty set, dq be distance_function of Aq,L st Aq, dq is_extension_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,z3 being Element of Aq st dq.(x,z1) = a & dq.(z2,z3) = a & dq.(z1,z2) = b & dq.(z3,y) = b; definition let A,L; let d be distance_function of A,L; mode ExtensionSeq of A,d -> Function means :: LATTICE5:def 20 dom it = NAT & it.0 = [A, d] & for n being Nat holds ex A9 being non empty set, d9 being distance_function of A9,L, Aq being non empty set, dq being distance_function of Aq,L st Aq, dq is_extension_of A9,d9 & it.n = [A9,d9] & it.(n+1) = [Aq,dq]; end; theorem :: LATTICE5:38 for d be distance_function of A,L for S being ExtensionSeq of A, d for k,l being Nat st k <= l holds (S.k)`1 c= (S.l)`1; theorem :: LATTICE5:39 for d be distance_function of A,L for S being ExtensionSeq of A, d for k,l being Nat st k <= l holds (S.k)`2 c= (S.l)`2; definition let L; func BasicDF(L) -> distance_function of the carrier of L,L means :: LATTICE5:def 21 for x,y being Element of L holds (x <> y implies it.(x,y) = x"\/"y) & (x = y implies it.(x,y) = Bottom L); end; theorem :: LATTICE5:40 BasicDF(L) is onto; theorem :: LATTICE5:41 for S being ExtensionSeq of the carrier of L, BasicDF(L) for FS being non empty set st FS = union the set of all (S.i)`1 where i is Element of NAT holds union the set of all (S.i)`2 where i is Element of NAT is distance_function of FS,L; theorem :: LATTICE5:42 for S being ExtensionSeq of the carrier of L, BasicDF(L) for FS being non empty set, FD being distance_function of FS,L for x,y being Element of FS for a,b being Element of L st FS = union the set of all (S.i)`1 where i is Element of NAT & FD = union the set of all (S.i)`2 where i is Element of NAT & FD.(x,y) <= a"\/"b ex z1,z2,z3 being Element of FS st FD.(x,z1 ) = a & FD.(z2,z3) = a & FD.(z1,z2) = b & FD.(z3,y) = b; theorem :: LATTICE5:43 for S being ExtensionSeq 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 x, y being Element of FS for e1,e2 being Equivalence_Relation of FS,x,y being object st f = alpha FD & FS = union the set of all (S.i)`1 where i is Element of NAT & FD = union the set of all (S.i)`2 where i is Element of NAT & 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 = 3+2 & x,y are_joint_by F,e1,e2; ::$N Jonsson Theorem for lattices theorem :: LATTICE5:44 ex A being non empty set, f being Homomorphism of L,EqRelLATT A st f is one-to-one & type_of Image f <= 3;