Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000
Association of Mizar Users
The abstract of the Mizar article:
-
- 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