Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### The Jonsson Theorem

**by****Jaroslaw Gryko**- Received November 13, 1997
- MML identifier: LATTICE5

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, ORDINAL1, CLASSES1, ORDINAL2, MCART_1, PRALG_1, TARSKI, FUNCT_6, HAHNBAN, ZFMISC_1, ORDERS_1, LATTICE3, MSUALG_5, EQREL_1, LATTICES, BOOLE, WAYBEL_0, BHSP_3, SETFAM_1, CANTOR_1, RELAT_2, PRE_TOPC, GROUP_6, YELLOW_0, FILTER_2, CAT_1, FINSEQ_1, MATRIX_2, FINSEQ_2, ARYTM_1, SQUARE_1, REALSET1, SGRAPH1, CARD_1, PARTFUN1, LATTICE5; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1, FUNCT_2, FUNCT_6, NUMBERS, XCMPLX_0, XREAL_0, BINARITH, CANTOR_1, NAT_1, SETFAM_1, ORDINAL1, ORDINAL2, CARD_1, MCART_1, DOMAIN_1, PARTFUN1, PRALG_1, PRE_TOPC, STRUCT_0, ORDERS_1, EQREL_1, MSUALG_5, FINSEQ_1, FINSEQ_2, CLASSES1, CQC_SIM1, LATTICES, LATTICE3, BINOP_1, YELLOW_0, WAYBEL_0, YELLOW_2, ABIAN, FINSOP_1; constructors BINARITH, DOMAIN_1, RFUNCT_3, CANTOR_1, MSUALG_5, CQC_SIM1, BINOP_1, CLASSES1, WAYBEL_1, LATTICE3, ABIAN, FINSOP_1, MEMBERED; clusters SUBSET_1, RELSET_1, STRUCT_0, INT_1, YELLOW_0, YELLOW_1, CARD_1, ORDINAL1, PRALG_1, LATTICE3, ABIAN, GOBOARD4, ARYTM_3, LATTICES, MEMBERED, NUMBERS, ORDINAL2, PARTFUN1, EQREL_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Preliminaries scheme RecChoice{A() -> set,P[set,set,set]}: ex f being Function st dom f = NAT & f.0 = A() & for n being Element of NAT holds P[n,f.n,f.(n+1)] provided for n being Nat for x being set ex y being set st P[n,x,y]; 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; definition 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; definition let A be set; cluster EqRelLATT A -> complete; end; begin :: A type of a sublattice of equivalence lattice of a set definition let L1,L2 be LATTICE; cluster meet-preserving join-preserving map of L1,L2; end; definition let L1,L2 be LATTICE; mode Homomorphism of L1,L2 is meet-preserving join-preserving map of L1,L2; end; definition let L be LATTICE; cluster meet-inheriting join-inheriting strict SubRelStr of L; end; definition let L be non empty RelStr; mode Sublattice of L is meet-inheriting join-inheriting SubRelStr of L; end; definition let L1, L2 be LATTICE; let f be Homomorphism of L1,L2; redefine func Image f -> strict full Sublattice of L2; end; reserve e,e1,e2,e1',e2' for Equivalence_Relation of X, x,y,x',y' for set; definition let X; let f be non empty FinSequence of X; let x,y; 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 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; canceled; theorem :: LATTICE5:12 for x being set, o being 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; canceled; theorem :: LATTICE5:14 for x,y being set, R1,R2 being Relation, n,m being 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 Nat such that for e1,e2,x,y 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 -> Nat means :: LATTICE5:def 4 (for e1,e2,x,y 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,x,y 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:15 for Y being Sublattice of EqRelLATT X, n being Nat st (ex e st e in the carrier of Y & e <> id X) & (for e1,e2,x,y 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, L; mode BiFunction of A,L is Function of [:A,A:],the carrier of L; canceled; end; definition let A, L; 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, L; let f be BiFunction of A,L; attr f is symmetric means :: LATTICE5:def 6 for x,y being Element of A holds f.(x,y) = f.(y,x); attr f is zeroed means :: LATTICE5:def 7 for x being Element of A holds f.(x,x) = Bottom L; attr f is u.t.i. means :: LATTICE5:def 8 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 definition let A, L; cluster symmetric zeroed u.t.i. 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 -> map of L,EqRelLATT A means :: LATTICE5:def 9 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:16 for d being distance_function of A,L holds alpha d is meet-preserving; theorem :: LATTICE5:17 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 equals :: LATTICE5:def 10 A \/ {{A}, {{A}}, {{{A}}} }; end; definition 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 11 (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 & it.({{{A}}},{{A}}) = q`3 & it.({A},{{A}}) = q`4 & it.({{A}},{A}) = q`4 & it.({A},{{{A}}}) = q`3"\/"q`4 & it.({{{A}}},{A}) = 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`1)"\/"q`3"\/"q`4 & it.({{A}},u) = d.(u,q`1)"\/"q`3"\/" q`4 & it.(u,{{{A}}}) = d.(u,q`2)"\/"q`4 & it.({{{A}}},u) = d.(u,q`2)"\/"q`4); end; theorem :: LATTICE5:18 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:19 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:20 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_fun(d,q) is u.t.i.; theorem :: LATTICE5:21 for A be set holds A c= new_set A; theorem :: LATTICE5:22 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 12 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:23 for d be distance_function of A,L holds DistEsti(d) <> {}; reserve T,L1,LL for T-Sequence, O,O1,O2,O3,C for Ordinal; definition let A; let O; func ConsecutiveSet(A,O) means :: LATTICE5:def 13 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_set 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 :: LATTICE5:24 ConsecutiveSet(A,{}) = A; theorem :: LATTICE5:25 ConsecutiveSet(A,succ O) = new_set ConsecutiveSet(A,O); theorem :: LATTICE5:26 O <> {} & 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; definition let A; let O; cluster ConsecutiveSet(A,O) -> non empty; end; theorem :: LATTICE5:27 A c= ConsecutiveSet(A,O); definition let A,L; let d be BiFunction of A,L; mode QuadrSeq of d -> T-Sequence of [:A,A,the carrier of L,the carrier of L:] means :: LATTICE5:def 14 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 15 q.O; end; theorem :: LATTICE5:28 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 16 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) means :: LATTICE5:def 17 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_fun(BiFun(L0.C,ConsecutiveSet(A,C),L),Quadr(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 :: LATTICE5:29 for d being BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta(q,{}) = d; theorem :: LATTICE5:30 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:31 for d be BiFunction of A,L for q being QuadrSeq of d holds O <> {} & 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:32 O1 c= O2 implies ConsecutiveSet(A,O1) c= ConsecutiveSet(A,O2); theorem :: LATTICE5:33 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:34 for d be BiFunction of A,L for q being QuadrSeq of d holds d c= ConsecutiveDelta(q,O); theorem :: LATTICE5:35 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:36 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:37 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:38 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:39 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) equals :: LATTICE5:def 18 ConsecutiveSet(A,DistEsti(d)); end; definition 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) equals :: LATTICE5:def 19 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 20 ex q being QuadrSeq of d st Aq = NextSet(d) & dq = NextDelta(q); end; theorem :: LATTICE5:40 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 21 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_extension_of A',d' & it.n = [A',d'] & it.(n+1) = [Aq,dq]; end; theorem :: LATTICE5:41 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:42 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 22 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:43 BasicDF(L) is onto; theorem :: LATTICE5:44 for S being ExtensionSeq 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 :: LATTICE5:45 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 { (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,z3 being Element of FS st FD.(x,z1) = a & FD.(z2,z3) = a & FD.(z1,z2) = b & FD.(z3,y) = b; theorem :: LATTICE5:46 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 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 = 3+2 & x,y are_joint_by F,e1,e2; theorem :: LATTICE5:47 ex A being non empty set, f being Homomorphism of L,EqRelLATT A st f is one-to-one & type_of Image f <= 3;

Back to top