:: J\'onsson Theorem
:: by Jaros{\l}aw Gryko
::
:: Received November 13, 1997
:: Copyright (c) 1997-2016 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;