lattad_1.miz
begin
theorem ::
LATTAD_1:1
Ble1: for L be non
empty
1-sorted, R be
total
Relation of the
carrier of L holds R is
reflexive iff for x be
Element of L holds
[x, x]
in R
proof
let L be non
empty
1-sorted, R be
total
Relation of the
carrier of L;
thus R is
reflexive implies for x be
Element of L holds
[x, x]
in R
proof
assume
A1: R is
reflexive;
let x be
Element of L;
A2: R
is_reflexive_in (
field R) by
A1,
RELAT_2:def 9;
(
dom R)
= the
carrier of L by
PARTFUN1:def 2;
then x
in ((
dom R)
\/ (
rng R)) by
XBOOLE_0:def 3;
hence thesis by
A2,
RELAT_2:def 1;
end;
assume
B1: for x be
Element of L holds
[x, x]
in R;
for x be
object st x
in (
field R) holds
[x, x]
in R
proof
let x be
object;
b2: (
field R)
c= (the
carrier of L
\/ the
carrier of L) by
RELSET_1: 8;
assume x
in (
field R);
hence thesis by
B1,
b2;
end;
hence thesis by
RELAT_2:def 9,
RELAT_2:def 1;
end;
registration
cluster
trivial ->
distributive for non
empty
LattStr;
coherence ;
end
begin
definition
let L be non
empty
LattStr;
::
LATTAD_1:def1
attr L is
Distributive means
:
DefD: for x,y,z be
Element of L holds ((x
"\/" y)
"/\" z)
= ((x
"/\" z)
"\/" (y
"/\" z));
::
LATTAD_1:def2
attr L is
Meet-absorbing means
:
DefA1: for x,y be
Element of L holds ((x
"\/" y)
"/\" y)
= y;
::
LATTAD_1:def3
attr L is
Meet-Absorbing means
:
DefA2: for x,y be
Element of L holds ((x
"\/" y)
"/\" x)
= x;
end
registration
cluster
trivial ->
Distributive
Meet-absorbing
Meet-Absorbing
meet-Absorbing for non
empty
LattStr;
coherence ;
cluster
trivial ->
Lattice-like for non
empty
LattStr;
coherence
proof
let L be non
empty
LattStr;
assume L is
trivial;
then
reconsider LL = L as
trivial non
empty
LattStr;
LL is
meet-absorbing
join-absorbing
meet-commutative
join-commutative
meet-associative
join-associative by
STRUCT_0:def 10;
hence thesis;
end;
end
registration
cluster
trivial for
Lattice;
existence
proof
take L = the
trivial non
empty
LattStr;
thus thesis;
end;
end
registration
cluster
Distributive
distributive
Meet-absorbing
Meet-Absorbing
meet-Absorbing for non
empty
LattStr;
existence
proof
take L = the
trivial
Lattice;
thus thesis;
end;
end
definition
mode
AD_Lattice is
Distributive
distributive
Meet-absorbing
Meet-Absorbing
meet-Absorbing non
empty
LattStr;
end
begin
reserve L for
AD_Lattice;
reserve x,y,z for
Element of L;
theorem ::
LATTAD_1:2
(x
"\/" y)
= x iff (x
"/\" y)
= y by
DefA1,
ROBBINS3:def 3;
theorem ::
LATTAD_1:3
ISum: (x
"\/" x)
= x
proof
A8: for x, y holds ((x
"\/" x)
"/\" y)
= (x
"/\" (y
"\/" y))
proof
let x, y;
set z = x;
((x
"/\" y)
"\/" (x
"/\" y))
= (x
"/\" (y
"\/" y)) by
LATTICES:def 11;
hence thesis by
DefD;
end;
A27: (x
"/\" (x
"\/" x))
= x
proof
((x
"\/" x)
"/\" x)
= (x
"/\" (x
"\/" x)) by
A8;
hence thesis by
DefA1;
end;
A43: for x, y holds ((x
"\/" y)
"/\" (y
"\/" y))
= (y
"\/" y)
proof
let x, y;
((x
"\/" y)
"/\" (y
"\/" y))
= (((x
"\/" y)
"/\" y)
"\/" ((x
"\/" y)
"/\" y)) by
LATTICES:def 11
.= (y
"\/" ((x
"\/" y)
"/\" y)) by
DefA1
.= (y
"\/" y) by
DefA1;
hence thesis;
end;
A49: ((x
"\/" x)
"\/" (x
"\/" x))
= (x
"\/" x)
proof
((x
"\/" x)
"/\" (x
"\/" x))
= (((x
"\/" x)
"/\" x)
"\/" ((x
"\/" x)
"/\" x)) by
LATTICES:def 11
.= (x
"\/" ((x
"\/" x)
"/\" x)) by
DefA1
.= (x
"\/" x) by
DefA1;
hence thesis by
ROBBINS3:def 3;
end;
set R = (x
"\/" x);
(x
"\/" x)
= ((x
"\/" x)
"/\" (x
"\/" x)) by
A43
.= x by
A27,
A49,
A8;
hence thesis;
end;
theorem ::
LATTAD_1:4
IMeet: (x
"/\" x)
= x
proof
thus (x
"/\" x)
= ((x
"\/" x)
"/\" x) by
ISum
.= x by
DefA2;
end;
theorem ::
LATTAD_1:5
LemXX: ((x
"/\" y)
"\/" y)
= y
proof
((x
"/\" y)
"\/" y)
= ((x
"/\" y)
"\/" (y
"/\" y)) by
IMeet
.= ((x
"\/" y)
"/\" y) by
DefD
.= y by
DefA1;
hence thesis;
end;
theorem ::
LATTAD_1:6
Lem232: (x
"\/" y)
= y iff (x
"/\" y)
= x
proof
hereby
assume (x
"\/" y)
= y;
then (x
"/\" y)
= ((x
"/\" x)
"\/" (x
"/\" y)) by
LATTICES:def 11
.= (x
"\/" (x
"/\" y)) by
IMeet
.= x by
ROBBINS3:def 3;
hence (x
"/\" y)
= x;
end;
assume (x
"/\" y)
= x;
hence thesis by
LemXX;
end;
theorem ::
LATTAD_1:7
Ze: (x
"/\" (x
"\/" y))
= x
proof
(x
"/\" (x
"\/" y))
= ((x
"/\" x)
"\/" (x
"/\" y)) by
LATTICES:def 11
.= (x
"\/" (x
"/\" y)) by
IMeet
.= x by
ROBBINS3:def 3;
hence thesis;
end;
theorem ::
LATTAD_1:8
(x
"\/" (y
"/\" x))
= x
proof
(x
"\/" (y
"/\" x))
= ((x
"/\" x)
"\/" (y
"/\" x)) by
IMeet
.= ((x
"\/" y)
"/\" x) by
DefD
.= x by
DefA2;
hence thesis;
end;
theorem ::
LATTAD_1:9
x
[= (x
"\/" y) & (x
"/\" y)
[= y
proof
(x
"/\" (x
"\/" y))
= x by
Ze;
hence thesis by
LemXX;
end;
theorem ::
LATTAD_1:10
x
[= y iff (x
"/\" y)
= x by
Lem232;
theorem ::
LATTAD_1:11
Lem36c: (x
"/\" (y
"/\" x))
= (y
"/\" x)
proof
for y,x be
Element of L holds (y
"/\" (x
"/\" y))
= (x
"/\" y)
proof
let y,x be
Element of L;
((x
"/\" y)
"\/" y)
= y by
LemXX;
hence thesis by
DefA2;
end;
hence thesis;
end;
theorem ::
LATTAD_1:12
Th1712: ((x
"/\" y)
"\/" x)
= x iff (x
"/\" (y
"\/" x))
= x
proof
hereby
assume
A1: ((x
"/\" y)
"\/" x)
= x;
(x
"/\" (y
"\/" x))
= ((x
"/\" y)
"\/" (x
"/\" x)) by
LATTICES:def 11
.= x by
A1,
IMeet;
hence (x
"/\" (y
"\/" x))
= x;
end;
assume
A1: (x
"/\" (y
"\/" x))
= x;
((x
"/\" y)
"\/" x)
= ((x
"/\" y)
"\/" (x
"/\" x)) by
IMeet
.= (x
"/\" (y
"\/" x)) by
LATTICES:def 11;
hence thesis by
A1;
end;
theorem ::
LATTAD_1:13
((y
"/\" x)
"\/" y)
= y iff (y
"/\" (x
"\/" y))
= y by
Th1712;
theorem ::
LATTAD_1:14
((x
"/\" y)
"\/" x)
= x implies (x
"/\" y)
= (y
"/\" x)
proof
assume ((x
"/\" y)
"\/" x)
= x;
then (y
"/\" x)
= ((y
"/\" (x
"/\" y))
"\/" (y
"/\" x)) by
LATTICES:def 11
.= ((x
"/\" y)
"\/" (y
"/\" x)) by
Lem36c
.= ((x
"/\" y)
"\/" (x
"/\" (y
"/\" x))) by
Lem36c
.= (x
"/\" (y
"\/" (y
"/\" x))) by
LATTICES:def 11
.= (x
"/\" y) by
ROBBINS3:def 3;
hence thesis;
end;
theorem ::
LATTAD_1:15
Th1726: (x
"/\" (y
"\/" x))
= x implies (x
"\/" y)
= (y
"\/" x)
proof
assume
A0: (x
"/\" (y
"\/" x))
= x;
(x
"\/" y)
= ((x
"/\" (y
"\/" x))
"\/" (y
"/\" (y
"\/" x))) by
Ze,
A0
.= ((x
"\/" y)
"/\" (y
"\/" x)) by
DefD
.= (((x
"\/" y)
"/\" y)
"\/" ((x
"\/" y)
"/\" x)) by
LATTICES:def 11
.= (y
"\/" ((x
"\/" y)
"/\" x)) by
DefA1
.= (y
"\/" x) by
DefA2;
hence thesis;
end;
theorem ::
LATTAD_1:16
Hehe1: (ex z be
Element of L st x
[= z & y
[= z) implies (x
"\/" y)
= (y
"\/" x)
proof
assume
A0: ex z be
Element of L st x
[= z & y
[= z;
(y
"/\" (x
"\/" y))
= y
proof
consider z be
Element of L such that
A1: x
[= z & y
[= z by
A0;
thus (y
"/\" (x
"\/" y))
= ((y
"/\" x)
"\/" (y
"/\" y)) by
LATTICES:def 11
.= ((y
"/\" x)
"\/" y) by
IMeet
.= ((y
"/\" x)
"\/" (y
"/\" z)) by
A1,
Lem232
.= (y
"/\" (x
"\/" z)) by
LATTICES:def 11
.= y by
A1,
Lem232;
end;
hence thesis by
Th1726;
end;
theorem ::
LATTAD_1:17
x
[= y implies (x
"\/" y)
= (y
"\/" x)
proof
assume
A1: x
[= y;
ex c be
Element of L st x
[= c & y
[= c
proof
take y;
thus thesis by
A1,
ISum;
end;
hence thesis by
Hehe1;
end;
begin
definition
let L be non
empty
LattStr;
::
LATTAD_1:def4
attr L is
left-Distributive means
:
DefLDS: for x,y,z be
Element of L holds (x
"\/" (y
"/\" z))
= ((x
"\/" y)
"/\" (x
"\/" z));
::
LATTAD_1:def5
attr L is
ADL-absorbing means for x,y be
Element of L holds (x
"/\" (y
"\/" x))
= x;
end
registration
cluster
trivial ->
meet-associative
distributive
left-Distributive
Meet-Absorbing for non
empty
LattStr;
coherence ;
end
registration
cluster
meet-associative
distributive
left-Distributive
join-absorbing
Meet-Absorbing
meet-absorbing for non
empty
LattStr;
existence
proof
take L = the
trivial
Lattice;
thus thesis;
end;
end
definition
mode
GAD_Lattice is
meet-associative
distributive
left-Distributive
join-absorbing
Meet-Absorbing
meet-absorbing non
empty
LattStr;
end
reserve L for
GAD_Lattice;
reserve x,y,z for
Element of L;
theorem ::
LATTAD_1:18
ISum: (x
"\/" x)
= x
proof
thus (x
"\/" x)
= (((x
"\/" x)
"/\" x)
"\/" x) by
DefA2
.= x by
LATTICES:def 8;
end;
theorem ::
LATTAD_1:19
IMeet: (x
"/\" x)
= x
proof
thus (x
"/\" x)
= (x
"/\" (x
"\/" x)) by
ISum
.= x by
LATTICES:def 9;
end;
theorem ::
LATTAD_1:20
ThA4: (x
"\/" (x
"/\" y))
= x
proof
thus (x
"\/" (x
"/\" y))
= ((x
"\/" x)
"/\" (x
"\/" y)) by
DefLDS
.= (x
"/\" (x
"\/" y)) by
ISum
.= x by
LATTICES:def 9;
end;
theorem ::
LATTAD_1:21
ThA5: (x
"\/" (y
"/\" x))
= x
proof
thus (x
"\/" (y
"/\" x))
= ((x
"\/" y)
"/\" (x
"\/" x)) by
DefLDS
.= ((x
"\/" y)
"/\" x) by
ISum
.= x by
DefA2;
end;
theorem ::
LATTAD_1:22
(x
"/\" y)
= y implies (x
"\/" y)
= x by
ThA4;
theorem ::
LATTAD_1:23
(x
"\/" y)
= y iff (x
"/\" y)
= x by
LATTICES:def 9,
LATTICES:def 8;
begin
theorem ::
LATTAD_1:24
Idem: x
[= x
proof
(x
"/\" x)
= x by
IMeet;
hence thesis by
LATTICES: 4;
end;
theorem ::
LATTAD_1:25
TransLat: x
[= y & y
[= z implies x
[= z
proof
assume
A0: x
[= y & y
[= z;
then (x
"/\" y)
= x & (y
"/\" z)
= y by
LATTICES: 4;
then
A1: (x
"/\" (y
"/\" z))
= (x
"/\" z) by
LATTICES:def 7;
(x
"/\" (y
"/\" z))
= (x
"/\" y) by
LATTICES:def 9,
A0
.= x by
A0,
LATTICES: 4;
hence x
[= z by
LATTICES: 4,
A1;
end;
definition
let L be non
empty
LattStr;
::
LATTAD_1:def6
func
LatOrder L ->
Relation equals {
[a, b] where a,b be
Element of L : a
[= b };
coherence
proof
now
let x be
object;
assume x
in {
[p, q] where p be
Element of L, q be
Element of L : p
[= q };
then ex p,q be
Element of L st x
=
[p, q] & p
[= q;
hence ex x1,x2 be
object st x
=
[x1, x2];
end;
hence thesis by
RELAT_1:def 1;
end;
end
theorem ::
LATTAD_1:26
Th32: (
dom (
LatOrder L))
= the
carrier of L & (
rng (
LatOrder L))
= the
carrier of L & (
field (
LatOrder L))
= the
carrier of L
proof
now
let x be
object;
thus x
in the
carrier of L implies ex y be
object st
[x, y]
in (
LatOrder L)
proof
assume x
in the
carrier of L;
then
reconsider p = x as
Element of L;
p
[= p by
Idem;
then
[p, p]
in (
LatOrder L);
hence thesis;
end;
given y be
object such that
A1:
[x, y]
in (
LatOrder L);
consider p,q be
Element of L such that
A2:
[x, y]
=
[p, q] and p
[= q by
A1;
x
= p by
A2,
XTUPLE_0: 1;
hence x
in the
carrier of L;
end;
hence
A3: (
dom (
LatOrder L))
= the
carrier of L by
XTUPLE_0:def 12;
T1:
now
let x be
object;
thus x
in the
carrier of L implies ex y be
object st
[y, x]
in (
LatOrder L)
proof
assume x
in the
carrier of L;
then
reconsider p = x as
Element of L;
p
[= p by
Idem;
then
[p, p]
in (
LatOrder L);
hence thesis;
end;
given y be
object such that
A4:
[y, x]
in (
LatOrder L);
consider p,q be
Element of L such that
A5:
[y, x]
=
[p, q] and p
[= q by
A4;
x
= q by
A5,
XTUPLE_0: 1;
hence x
in the
carrier of L;
end;
hence (
rng (
LatOrder L))
= the
carrier of L by
XTUPLE_0:def 13;
thus (
field (
LatOrder L))
= (the
carrier of L
\/ the
carrier of L) by
A3,
XTUPLE_0:def 13,
T1
.= the
carrier of L;
end;
definition
let L;
:: original:
LatOrder
redefine
func
LatOrder L ->
Relation of the
carrier of L ;
correctness
proof
(
dom (
LatOrder L))
= the
carrier of L & (
rng (
LatOrder L))
= the
carrier of L by
Th32;
hence thesis by
RELSET_1: 4;
end;
end
registration
let L;
cluster (
LatOrder L) ->
total;
correctness
proof
set R = (
LatOrder L);
(
dom R)
= the
carrier of L by
Th32;
hence thesis by
PARTFUN1:def 2;
end;
end
theorem ::
LATTAD_1:27
OrdLat:
[x, y]
in (
LatOrder L) iff x
[= y
proof
hereby
assume
[x, y]
in (
LatOrder L);
then
consider a1,b1 be
Element of L such that
A1:
[x, y]
=
[a1, b1] & a1
[= b1;
thus x
[= y by
A1,
XTUPLE_0: 1;
end;
assume x
[= y;
hence thesis;
end;
definition
let L be non
empty
LattStr;
::
LATTAD_1:def7
func
ThetaOrder L ->
Relation equals {
[a, b] where a,b be
Element of L : (a
"/\" b)
= b };
coherence
proof
now
let x be
object;
assume x
in {
[p, q] where p be
Element of L, q be
Element of L : (p
"/\" q)
= q };
then ex p,q be
Element of L st x
=
[p, q] & (p
"/\" q)
= q;
hence ex x1,x2 be
object st x
=
[x1, x2];
end;
hence thesis by
RELAT_1:def 1;
end;
end
theorem ::
LATTAD_1:28
Th32: (
dom (
ThetaOrder L))
= the
carrier of L & (
rng (
ThetaOrder L))
= the
carrier of L & (
field (
ThetaOrder L))
= the
carrier of L
proof
now
let x be
object;
thus x
in the
carrier of L implies ex y be
object st
[x, y]
in (
ThetaOrder L)
proof
assume x
in the
carrier of L;
then
reconsider p = x as
Element of L;
(p
"/\" p)
= p by
IMeet;
then
[p, p]
in (
ThetaOrder L);
hence thesis;
end;
given y be
object such that
A1:
[x, y]
in (
ThetaOrder L);
consider p,q be
Element of L such that
A2:
[x, y]
=
[p, q] and (p
"/\" q)
= q by
A1;
x
= p by
A2,
XTUPLE_0: 1;
hence x
in the
carrier of L;
end;
hence
A3: (
dom (
ThetaOrder L))
= the
carrier of L by
XTUPLE_0:def 12;
T1:
now
let x be
object;
thus x
in the
carrier of L implies ex y be
object st
[y, x]
in (
ThetaOrder L)
proof
assume x
in the
carrier of L;
then
reconsider p = x as
Element of L;
(p
"/\" p)
= p by
IMeet;
then
[p, p]
in (
ThetaOrder L);
hence thesis;
end;
given y be
object such that
A4:
[y, x]
in (
ThetaOrder L);
consider p,q be
Element of L such that
A5:
[y, x]
=
[p, q] and (p
"/\" q)
= q by
A4;
x
= q by
A5,
XTUPLE_0: 1;
hence x
in the
carrier of L;
end;
hence (
rng (
ThetaOrder L))
= the
carrier of L by
XTUPLE_0:def 13;
thus (
field (
ThetaOrder L))
= (the
carrier of L
\/ the
carrier of L) by
A3,
XTUPLE_0:def 13,
T1
.= the
carrier of L;
end;
definition
let L;
:: original:
ThetaOrder
redefine
func
ThetaOrder L ->
Relation of the
carrier of L ;
correctness
proof
(
dom (
ThetaOrder L))
= the
carrier of L & (
rng (
ThetaOrder L))
= the
carrier of L by
Th32;
hence thesis by
RELSET_1: 4;
end;
end
registration
let L;
cluster (
ThetaOrder L) ->
total;
correctness
proof
set R = (
ThetaOrder L);
(
dom R)
= the
carrier of L by
Th32;
hence thesis by
PARTFUN1:def 2;
end;
end
theorem ::
LATTAD_1:29
ThetaOrdLat:
[x, y]
in (
ThetaOrder L) iff (x
"/\" y)
= y
proof
hereby
assume
[x, y]
in (
ThetaOrder L);
then
consider a1,b1 be
Element of L such that
A1:
[x, y]
=
[a1, b1] & (a1
"/\" b1)
= b1;
thus (x
"/\" y)
= y by
A1,
XTUPLE_0: 1;
end;
assume (x
"/\" y)
= y;
hence thesis;
end;
registration
let L;
cluster (
LatOrder L) ->
reflexive;
coherence
proof
set R = (
LatOrder L);
for x be
Element of L holds
[x, x]
in R
proof
let x be
Element of L;
x
[= x by
Idem;
hence thesis;
end;
hence thesis by
Ble1;
end;
cluster (
LatOrder L) ->
transitive;
coherence
proof
set R = (
LatOrder L);
for x,y,z be
object st
[x, y]
in R &
[y, z]
in R holds
[x, z]
in R
proof
let x,y,z be
object;
assume
A1:
[x, y]
in R &
[y, z]
in R;
then
consider x1,y1 be
object such that
A2:
[x, y]
=
[x1, y1] & x1
in the
carrier of L & y1
in the
carrier of L by
RELSET_1: 2;
consider y2,z2 be
object such that
A3:
[y, z]
=
[y2, z2] & y2
in the
carrier of L & z2
in the
carrier of L by
A1,
RELSET_1: 2;
reconsider xx = x, yy = y, zz = z as
Element of L by
A2,
A3,
XTUPLE_0: 1;
xx
[= yy & yy
[= zz by
A1,
OrdLat;
then xx
[= zz by
TransLat;
hence
[x, z]
in R;
end;
hence thesis by
RELAT_2: 31;
end;
end
registration
let L;
cluster (
ThetaOrder L) ->
reflexive;
coherence
proof
set R = (
ThetaOrder L);
for x be
Element of L holds
[x, x]
in R
proof
let x be
Element of L;
(x
"/\" x)
= x by
IMeet;
hence thesis;
end;
hence thesis by
Ble1;
end;
cluster (
ThetaOrder L) ->
transitive;
coherence
proof
set R = (
ThetaOrder L);
for x,y,z be
object st
[x, y]
in R &
[y, z]
in R holds
[x, z]
in R
proof
let x,y,z be
object;
assume
A1:
[x, y]
in R &
[y, z]
in R;
then
consider x1,y1 be
object such that
A2:
[x, y]
=
[x1, y1] & x1
in the
carrier of L & y1
in the
carrier of L by
RELSET_1: 2;
consider y2,z2 be
object such that
A3:
[y, z]
=
[y2, z2] & y2
in the
carrier of L & z2
in the
carrier of L by
A1,
RELSET_1: 2;
reconsider xx = x, yy = y, zz = z as
Element of L by
A2,
A3,
XTUPLE_0: 1;
(xx
"/\" zz)
= (xx
"/\" (yy
"/\" zz)) by
A1,
ThetaOrdLat
.= ((xx
"/\" yy)
"/\" zz) by
LATTICES:def 7
.= (yy
"/\" zz) by
A1,
ThetaOrdLat
.= zz by
A1,
ThetaOrdLat;
hence
[x, z]
in R;
end;
hence thesis by
RELAT_2: 31;
end;
end
begin
theorem ::
LATTAD_1:30
Lem36X: (x
"\/" (x
"\/" y))
= (x
"\/" y)
proof
(x
"/\" (x
"\/" y))
= x by
LATTICES:def 9;
hence thesis by
LATTICES:def 8;
end;
theorem ::
LATTAD_1:31
Lem36c: (x
"/\" (y
"/\" x))
= (y
"/\" x)
proof
for v2,v0 be
Element of L holds (v2
"/\" (v0
"/\" v2))
= (v0
"/\" v2)
proof
let v2,v0 be
Element of L;
((v0
"/\" v2)
"\/" v2)
= v2 by
LATTICES:def 8;
hence thesis by
DefA2;
end;
hence thesis;
end;
theorem ::
LATTAD_1:32
(y
"/\" (x
"/\" y))
= (x
"/\" y) by
Lem36c;
Th3715: ((x
"/\" y)
"\/" x)
= x implies (x
"/\" y)
= (y
"/\" x)
proof
assume ((x
"/\" y)
"\/" x)
= x;
then (y
"/\" x)
= ((y
"/\" (x
"/\" y))
"\/" (y
"/\" x)) by
LATTICES:def 11
.= ((x
"/\" y)
"\/" (y
"/\" x)) by
Lem36c
.= ((x
"/\" y)
"\/" (x
"/\" (y
"/\" x))) by
Lem36c
.= (x
"/\" (y
"\/" (y
"/\" x))) by
LATTICES:def 11
.= (x
"/\" y) by
ThA4;
hence thesis;
end;
Th3713: ((x
"/\" y)
"\/" x)
= x implies ((y
"/\" x)
"\/" y)
= y
proof
assume ((x
"/\" y)
"\/" x)
= x;
then ((y
"/\" x)
"\/" y)
= ((x
"/\" y)
"\/" y) by
Th3715
.= y by
LATTICES:def 8;
hence thesis;
end;
Th3712: ((x
"/\" y)
"\/" x)
= x iff (x
"/\" (y
"\/" x))
= x
proof
thus ((x
"/\" y)
"\/" x)
= x implies (x
"/\" (y
"\/" x))
= x
proof
assume
A1: ((x
"/\" y)
"\/" x)
= x;
(x
"/\" (y
"\/" x))
= ((x
"/\" y)
"\/" (x
"/\" x)) by
LATTICES:def 11
.= ((x
"/\" y)
"\/" x) by
IMeet;
hence thesis by
A1;
end;
assume
A1: (x
"/\" (y
"\/" x))
= x;
((x
"/\" y)
"\/" x)
= ((x
"/\" y)
"\/" (x
"/\" x)) by
IMeet
.= (x
"/\" (y
"\/" x)) by
LATTICES:def 11;
hence thesis by
A1;
end;
Th3726: (x
"/\" (y
"\/" x))
= x implies (x
"\/" y)
= (y
"\/" x)
proof
assume
A0: (x
"/\" (y
"\/" x))
= x;
((x
"/\" y)
"\/" x)
= x by
Th3712,
A0;
then ((y
"/\" x)
"\/" y)
= y by
Th3713;
then
a3: (y
"/\" (x
"\/" y))
= y by
Th3712;
(y
"\/" x)
= (y
"\/" ((x
"\/" y)
"/\" x)) by
DefA2
.= ((y
"\/" (x
"\/" y))
"/\" (y
"\/" x)) by
DefLDS
.= ((x
"\/" y)
"/\" (y
"\/" x)) by
a3,
LATTICES:def 8
.= ((x
"\/" y)
"/\" (x
"\/" (y
"\/" x))) by
A0,
LATTICES:def 8
.= (x
"\/" (y
"/\" (y
"\/" x))) by
DefLDS
.= (x
"\/" y) by
LATTICES:def 9;
hence thesis;
end;
DefB2: for a,b be
Element of L st (ex c be
Element of L st a
[= c & b
[= c) holds (a
"\/" b)
= (b
"\/" a)
proof
let a,b be
Element of L;
assume
A0: ex c be
Element of L st a
[= c & b
[= c;
(b
"/\" (a
"\/" b))
= b
proof
consider c be
Element of L such that
A1: a
[= c & b
[= c by
A0;
thus (b
"/\" (a
"\/" b))
= ((b
"/\" a)
"\/" (b
"/\" b)) by
LATTICES:def 11
.= ((b
"/\" a)
"\/" b) by
IMeet
.= ((b
"/\" a)
"\/" (b
"/\" c)) by
A1,
LATTICES:def 9
.= (b
"/\" (a
"\/" c)) by
LATTICES:def 11
.= b by
A1,
LATTICES:def 9;
end;
hence thesis by
Th3726;
end;
definition
let L;
let a,b be
Element of L;
::
LATTAD_1:def8
pred
ex_lub_of a,b means ex c be
Element of L st a
[= c & b
[= c & for x be
Element of L st a
[= x & b
[= x holds c
[= x;
::
LATTAD_1:def9
pred
ex_glb_of a,b means ex c be
Element of L st c
[= a & c
[= b & for x be
Element of L st x
[= a & x
[= b holds x
[= c;
end
definition
let L;
let a,b be
Element of L;
assume
A1:
ex_lub_of (a,b);
::
LATTAD_1:def10
func
lub (a,b) ->
Element of L means
:
DefLUB: a
[= it & b
[= it & for x be
Element of L st a
[= x & b
[= x holds it
[= x;
existence by
A1;
correctness
proof
let A1,A2 be
Element of L such that
A1: a
[= A1 & b
[= A1 & for x be
Element of L st a
[= x & b
[= x holds A1
[= x and
A2: a
[= A2 & b
[= A2 & for x be
Element of L st a
[= x & b
[= x holds A2
[= x;
a3: A1
[= A2 by
A1,
A2;
B2: A2
[= A1 by
A1,
A2;
A1
[= A1 by
ISum;
hence thesis by
a3,
DefB2,
B2;
end;
end
definition
let L;
let a,b be
Element of L;
assume
A1:
ex_glb_of (a,b);
::
LATTAD_1:def11
func
glb (a,b) ->
Element of L means
:
DefGLB: it
[= a & it
[= b & for x be
Element of L st x
[= a & x
[= b holds x
[= it ;
existence by
A1;
correctness
proof
let A1,A2 be
Element of L such that
A1: A1
[= a & A1
[= b & for x be
Element of L st x
[= a & x
[= b holds x
[= A1 and
A2: A2
[= a & A2
[= b & for x be
Element of L st x
[= a & x
[= b holds x
[= A2;
a3: A1
[= A2 by
A1,
A2;
B2: A2
[= A1 by
A1,
A2;
A1
[= A1 by
ISum;
hence thesis by
a3,
DefB2,
B2;
end;
end
Th3751: (x
"/\" y)
= (y
"/\" x) implies ((x
"/\" y)
"\/" x)
= x by
LATTICES:def 8;
IffComm: (x
"\/" y)
= (y
"\/" x) implies (x
"/\" y)
= (y
"/\" x)
proof
assume (x
"\/" y)
= (y
"\/" x);
then (x
"/\" (y
"\/" x))
= x by
LATTICES:def 9;
then ((x
"/\" y)
"\/" x)
= x by
Th3712;
hence thesis by
Th3715;
end;
theorem ::
LATTAD_1:33
((x
"/\" y)
"\/" x)
= x iff (x
"/\" (y
"\/" x))
= x by
Th3712;
theorem ::
LATTAD_1:34
((x
"/\" y)
"\/" x)
= x iff ((y
"/\" x)
"\/" y)
= y by
Th3713;
theorem ::
LATTAD_1:35
((x
"/\" y)
"\/" x)
= x iff (y
"/\" (x
"\/" y))
= y
proof
thus ((x
"/\" y)
"\/" x)
= x implies (y
"/\" (x
"\/" y))
= y
proof
assume ((x
"/\" y)
"\/" x)
= x;
then ((y
"/\" x)
"\/" y)
= y by
Th3713;
hence thesis by
Th3712;
end;
assume (y
"/\" (x
"\/" y))
= y;
then ((y
"/\" x)
"\/" y)
= y by
Th3712;
hence thesis by
Th3713;
end;
theorem ::
LATTAD_1:36
((x
"/\" y)
"\/" x)
= x iff (x
"/\" y)
= (y
"/\" x) by
Th3715,
LATTICES:def 8;
theorem ::
LATTAD_1:37
Th3716: ((x
"/\" y)
"\/" x)
= x iff (x
"\/" y)
= (y
"\/" x)
proof
hereby
assume
A1: ((x
"/\" y)
"\/" x)
= x;
(x
"/\" (y
"\/" x))
= x by
A1,
Th3712;
hence (x
"\/" y)
= (y
"\/" x) by
Th3726;
end;
assume (x
"\/" y)
= (y
"\/" x);
then (x
"/\" (y
"\/" x))
= x by
LATTICES:def 9;
hence thesis by
Th3712;
end;
theorem ::
LATTAD_1:38
x
[= y iff (x
"/\" y)
= x by
LATTICES:def 9,
LATTICES:def 8;
LemX3: x
[= (x
"\/" y)
proof
(x
"/\" (x
"\/" y))
= x by
LATTICES:def 9;
hence thesis by
LATTICES:def 8;
end;
LemB1: (x
"/\" y)
[= y by
LATTICES:def 8;
Th3823: y
[= (x
"\/" y) implies ex z st x
[= z & y
[= z
proof
assume
A1: y
[= (x
"\/" y);
take z = (x
"\/" y);
thus thesis by
LemX3,
A1;
end;
Th3851: x
[= (y
"\/" x) implies (x
"\/" y)
= (y
"\/" x)
proof
assume
A1: x
[= (y
"\/" x);
(x
"/\" (y
"\/" x))
= x by
LATTICES: 4,
A1;
hence thesis by
Th3726;
end;
Th3856: x
[= (y
"\/" x) implies
ex_lub_of (x,y) & (y
"\/" x)
= (
lub (x,y))
proof
assume
A1: x
[= (y
"\/" x);
A2: y
[= (y
"\/" x) by
LemX3;
ex c be
Element of L st x
[= c & y
[= c & for d be
Element of L st x
[= d & y
[= d holds c
[= d
proof
take c = (y
"\/" x);
thus x
[= c & y
[= c by
A1,
LemX3;
let d be
Element of L;
assume
B1: x
[= d & y
[= d;
then ((y
"\/" x)
"/\" d)
= (y
"\/" (x
"/\" d)) by
DefLDS
.= (y
"\/" x) by
B1,
LATTICES:def 9;
hence thesis by
LATTICES:def 8;
end;
hence
A3:
ex_lub_of (x,y);
for c be
Element of L st x
[= c & y
[= c holds (y
"\/" x)
[= c
proof
let c be
Element of L;
assume
B1: x
[= c & y
[= c;
then ((y
"\/" x)
"/\" c)
= (y
"\/" (x
"/\" c)) by
DefLDS
.= (y
"\/" x) by
B1,
LATTICES:def 9;
hence thesis by
LATTICES:def 8;
end;
hence thesis by
DefLUB,
A1,
A2,
A3;
end;
Th3865:
ex_lub_of (x,y) & (y
"\/" x)
= (
lub (x,y)) implies x
[= (y
"\/" x) by
DefLUB;
Th3834: (ex c be
Element of L st x
[= c & y
[= c) implies
ex_lub_of (x,y) & (x
"\/" y)
= (
lub (x,y))
proof
given c be
Element of L such that
A0: x
[= c & y
[= c;
ex c be
Element of L st x
[= c & y
[= c & for d be
Element of L st x
[= d & y
[= d holds c
[= d
proof
take c = (x
"\/" y);
S1: (x
"\/" y)
= (y
"\/" x) by
A0,
DefB2;
hence x
[= c & y
[= c by
LemX3;
let d be
Element of L;
assume
B1: x
[= d & y
[= d;
then ((y
"\/" x)
"/\" d)
= (y
"\/" (x
"/\" d)) by
DefLDS
.= (y
"\/" x) by
B1,
LATTICES:def 9;
hence thesis by
S1,
LATTICES:def 8;
end;
hence
A3:
ex_lub_of (x,y);
(x
"\/" y)
= (y
"\/" x) by
A0,
DefB2;
then
B2: x
[= (x
"\/" y) & y
[= (x
"\/" y) by
LemX3;
for c be
Element of L st x
[= c & y
[= c holds (x
"\/" y)
[= c
proof
let c be
Element of L;
assume
B1: x
[= c & y
[= c;
then ((x
"\/" y)
"/\" c)
= (x
"\/" (y
"/\" c)) by
DefLDS
.= (x
"\/" y) by
B1,
LATTICES:def 9;
hence thesis by
LATTICES:def 8;
end;
hence thesis by
DefLUB,
A3,
B2;
end;
Th3841:
ex_lub_of (x,y) & (x
"\/" y)
= (
lub (x,y)) implies (x
"\/" y)
= (y
"\/" x)
proof
assume
ex_lub_of (x,y) & (x
"\/" y)
= (
lub (x,y));
then y
[= (x
"\/" y) by
DefLUB;
then (y
"/\" (x
"\/" y))
= y by
LATTICES:def 9;
hence thesis by
Th3726;
end;
theorem ::
LATTAD_1:39
(x
"\/" y)
= (y
"\/" x) iff y
[= (x
"\/" y)
proof
thus (x
"\/" y)
= (y
"\/" x) implies y
[= (x
"\/" y) by
LemX3;
assume y
[= (x
"\/" y);
then ex z st x
[= z & y
[= z by
Th3823;
hence thesis by
DefB2;
end;
theorem ::
LATTAD_1:40
(x
"\/" y)
= (y
"\/" x) iff ex z st x
[= z & y
[= z by
Th3823,
LemX3,
DefB2;
theorem ::
LATTAD_1:41
Th381i4: (x
"\/" y)
= (y
"\/" x) iff
ex_lub_of (x,y) & (x
"\/" y)
= (
lub (x,y))
proof
hereby
assume (x
"\/" y)
= (y
"\/" x);
then ex c be
Element of L st x
[= c & y
[= c by
Th3823,
LemX3;
hence
ex_lub_of (x,y) & (x
"\/" y)
= (
lub (x,y)) by
Th3834;
end;
assume
ex_lub_of (x,y) & (x
"\/" y)
= (
lub (x,y));
hence thesis by
Th3841;
end;
theorem ::
LATTAD_1:42
(x
"\/" y)
= (y
"\/" x) iff x
[= (y
"\/" x) by
LemX3,
Th3851;
theorem ::
LATTAD_1:43
(x
"\/" y)
= (y
"\/" x) iff
ex_lub_of (x,y) & (y
"\/" x)
= (
lub (x,y))
proof
hereby
assume (x
"\/" y)
= (y
"\/" x);
then x
[= (y
"\/" x) by
LemX3;
hence
ex_lub_of (x,y) & (y
"\/" x)
= (
lub (x,y)) by
Th3856;
end;
assume
ex_lub_of (x,y) & (y
"\/" x)
= (
lub (x,y));
hence thesis by
Th3851,
Th3865;
end;
Lm1:
now
let L;
let a,b be
Element of L;
assume
ZZ: L is
join-commutative;
Z1: for x,y be
Element of L holds
ex_lub_of (x,y) & (x
"\/" y)
= (
lub (x,y))
proof
let x,y be
Element of L;
(x
"\/" y)
= (y
"\/" x) by
ZZ;
hence thesis by
Th381i4;
end;
S1:
ex_lub_of (a,b) & (a
"\/" b)
= (
lub (a,b)) by
Z1;
let c be
Element of L;
thus c
= (a
"\/" b) iff a
[= c & b
[= c & for d be
Element of L st a
[= d & b
[= d holds c
[= d by
S1,
DefLUB;
end;
Th14: L is
join-commutative implies for u1,u2,u3 be
Element of L holds ((u1
"\/" u2)
"\/" u3)
= (u1
"\/" (u2
"\/" u3))
proof
assume
Z0: L is
join-commutative;
let u1,u2,u3 be
Element of L;
Z1: for x,y be
Element of L holds
ex_lub_of (x,y) & (x
"\/" y)
= (
lub (x,y))
proof
let x,y be
Element of L;
(x
"\/" y)
= (y
"\/" x) by
Z0;
hence thesis by
Th381i4;
end;
A2: u1
[= (u1
"\/" u2) by
Lm1,
Z0;
A3: u2
[= (u1
"\/" u2) by
Lm1,
Z0;
A4: u2
[= (u2
"\/" u3) by
Lm1,
Z0;
A5: u3
[= (u2
"\/" u3) by
Lm1,
Z0;
A6: (u1
"\/" u2)
[= ((u1
"\/" u2)
"\/" u3) by
Lm1,
Z0;
A7: u3
[= ((u1
"\/" u2)
"\/" u3) by
Lm1,
Z0;
A8: u1
[= ((u1
"\/" u2)
"\/" u3) by
A2,
A6,
TransLat;
u2
[= ((u1
"\/" u2)
"\/" u3) by
A3,
A6,
TransLat;
then
A9: (u2
"\/" u3)
[= ((u1
"\/" u2)
"\/" u3) by
A7,
Lm1,
Z0;
S1:
ex_lub_of (u1,(u2
"\/" u3)) & (u1
"\/" (u2
"\/" u3))
= (
lub (u1,(u2
"\/" u3))) by
Z1;
now
let u4 be
Element of L;
assume that
A10: u1
[= u4 and
A11: (u2
"\/" u3)
[= u4;
A12: u2
[= u4 by
A4,
A11,
TransLat;
A13: u3
[= u4 by
A5,
A11,
TransLat;
(u1
"\/" u2)
[= u4 by
A10,
A12,
Lm1,
Z0;
hence ((u1
"\/" u2)
"\/" u3)
[= u4 by
A13,
Lm1,
Z0;
end;
hence thesis by
A8,
A9,
S1,
DefLUB;
end;
theorem ::
LATTAD_1:44
(x
"/\" y)
[= x implies ex z st z
[= x & z
[= y by
LemB1;
theorem ::
LATTAD_1:45
Th391i4: (x
"/\" y)
= (y
"/\" x) iff (y
"/\" x)
[= y by
LATTICES:def 8,
Th3715;
Th3956: (y
"/\" x)
[= y implies
ex_glb_of (x,y) & (y
"/\" x)
= (
glb (x,y))
proof
assume
A1: (y
"/\" x)
[= y;
A2: (y
"/\" x)
[= x by
LATTICES:def 8;
ex c be
Element of L st c
[= x & c
[= y & for d be
Element of L st d
[= x & d
[= y holds d
[= c
proof
take c = (y
"/\" x);
thus c
[= x & c
[= y by
A1,
LATTICES:def 8;
let d be
Element of L;
assume d
[= x & d
[= y;
hence thesis by
DefLDS;
end;
hence
T1:
ex_glb_of (x,y);
for d be
Element of L st d
[= x & d
[= y holds d
[= (y
"/\" x) by
DefLDS;
hence thesis by
T1,
DefGLB,
A1,
A2;
end;
Th3965:
ex_glb_of (x,y) & (y
"/\" x)
= (
glb (x,y)) implies (y
"/\" x)
[= y by
DefGLB;
theorem ::
LATTAD_1:46
(x
"/\" y)
= (y
"/\" x) iff
ex_glb_of (x,y) & (y
"/\" x)
= (
glb (x,y))
proof
thus (x
"/\" y)
= (y
"/\" x) implies
ex_glb_of (x,y) & (y
"/\" x)
= (
glb (x,y))
proof
assume (x
"/\" y)
= (y
"/\" x);
then (y
"/\" x)
[= y by
LATTICES:def 8;
hence thesis by
Th3956;
end;
assume
ex_glb_of (x,y) & (y
"/\" x)
= (
glb (x,y));
hence thesis by
Th391i4,
Th3965;
end;
theorem ::
LATTAD_1:47
(x
"/\" y)
= (y
"/\" x) iff (x
"/\" y)
[= x by
LATTICES:def 8,
Th3715;
ThXXX: (x
"/\" y)
[= x implies
ex_glb_of (x,y) & (x
"/\" y)
= (
glb (x,y))
proof
assume
A1: (x
"/\" y)
[= x;
A2: (x
"/\" y)
[= y by
LATTICES:def 8;
ex c be
Element of L st c
[= x & c
[= y & for d be
Element of L st d
[= x & d
[= y holds d
[= c
proof
take c = (x
"/\" y);
thus c
[= x & c
[= y by
A1,
LATTICES:def 8;
let d be
Element of L;
assume d
[= x & d
[= y;
hence thesis by
DefLDS;
end;
hence
T1:
ex_glb_of (x,y);
for d be
Element of L st d
[= x & d
[= y holds d
[= (x
"/\" y) by
DefLDS;
hence thesis by
T1,
DefGLB,
A1,
A2;
end;
theorem ::
LATTAD_1:48
(x
"/\" y)
= (y
"/\" x) iff
ex_glb_of (x,y) & (x
"/\" y)
= (
glb (x,y))
proof
thus (x
"/\" y)
= (y
"/\" x) implies
ex_glb_of (x,y) & (x
"/\" y)
= (
glb (x,y))
proof
assume (x
"/\" y)
= (y
"/\" x);
then (x
"/\" y)
[= x by
LATTICES:def 8;
hence thesis by
ThXXX;
end;
assume
ex_glb_of (x,y) & (x
"/\" y)
= (
glb (x,y));
then (x
"/\" y)
[= x by
DefGLB;
hence thesis by
Th3715;
end;
theorem ::
LATTAD_1:49
Lem310: ((x
"/\" y)
"/\" z)
= ((y
"/\" x)
"/\" z)
proof
A1: (x
"/\" z)
[= z by
LATTICES:def 8;
(y
"/\" z)
[= z by
LATTICES:def 8;
then ((x
"/\" z)
"\/" (y
"/\" z))
= ((y
"/\" z)
"\/" (x
"/\" z)) by
DefB2,
A1;
then ((x
"/\" z)
"/\" (y
"/\" z))
= ((y
"/\" z)
"/\" (x
"/\" z)) by
IffComm;
then (((x
"/\" z)
"/\" y)
"/\" z)
= ((y
"/\" z)
"/\" (x
"/\" z)) by
LATTICES:def 7;
then (((x
"/\" z)
"/\" y)
"/\" z)
= (((y
"/\" z)
"/\" x)
"/\" z) by
LATTICES:def 7;
then ((x
"/\" z)
"/\" (y
"/\" z))
= (((y
"/\" z)
"/\" x)
"/\" z) by
LATTICES:def 7;
then (x
"/\" (z
"/\" (y
"/\" z)))
= (((y
"/\" z)
"/\" x)
"/\" z) by
LATTICES:def 7;
then (x
"/\" (y
"/\" z))
= (((y
"/\" z)
"/\" x)
"/\" z) by
Lem36c;
then ((x
"/\" y)
"/\" z)
= (((y
"/\" z)
"/\" x)
"/\" z) by
LATTICES:def 7;
then ((x
"/\" y)
"/\" z)
= ((y
"/\" z)
"/\" (x
"/\" z)) by
LATTICES:def 7;
then ((x
"/\" y)
"/\" z)
= (y
"/\" (z
"/\" (x
"/\" z))) by
LATTICES:def 7;
then ((x
"/\" y)
"/\" z)
= (y
"/\" (x
"/\" z)) by
Lem36c;
hence thesis by
LATTICES:def 7;
end;
definition
let L be
GAD_Lattice;
::
LATTAD_1:def12
func
LatRelStr L ->
strict
RelStr equals
RelStr (# the
carrier of L, (
LatOrder L) #);
coherence ;
end
registration
let L be
GAD_Lattice;
cluster (
LatRelStr L) ->
reflexive
transitive;
coherence ;
end
theorem ::
LATTAD_1:50
for a,b be
Element of L, x,y be
Element of (
LatRelStr L) st a
= x & b
= y holds x
<= y iff a
[= b by
OrdLat,
ORDERS_2:def 5;
Th31145: L is
join-commutative iff L is
meet-commutative
proof
hereby
assume
A1: L is
join-commutative;
thus L is
meet-commutative
proof
let a,b be
Element of L;
(a
"\/" b)
= (b
"\/" a) by
A1;
then ((a
"/\" b)
"\/" a)
= a by
Th3716;
hence thesis by
Th3715;
end;
end;
assume
B1: L is
meet-commutative;
let a,b be
Element of L;
(a
"/\" b)
= (b
"/\" a) by
B1;
then ((a
"/\" b)
"\/" a)
= a by
LATTICES:def 8;
hence thesis by
Th3716;
end;
theorem ::
LATTAD_1:51
Th31141: L is
join-commutative iff L is
Lattice-like
distributive
proof
thus L is
join-commutative implies L is
Lattice-like
distributive
proof
assume
T0: L is
join-commutative;
then L is
join-associative by
Th14;
hence thesis by
T0,
Th31145;
end;
thus thesis;
end;
theorem ::
LATTAD_1:52
L is
join-commutative iff (
LatRelStr L) is
directed
proof
thus L is
join-commutative implies (
LatRelStr L) is
directed
proof
assume
A1: L is
join-commutative;
set X = (
[#] (
LatRelStr L));
for x,y be
Element of (
LatRelStr L) st x
in X & y
in X holds ex z be
Element of (
LatRelStr L) st z
in X & x
<= z & y
<= z
proof
let x,y be
Element of (
LatRelStr L);
assume x
in X & y
in X;
reconsider xx = x, yy = y as
Element of L;
(xx
"\/" yy)
= (yy
"\/" xx) by
A1;
then
consider z be
Element of L such that
B1: xx
[= z & yy
[= z by
Th3823,
LemX3;
reconsider zz = z as
Element of (
LatRelStr L);
C1: x
<= zz by
OrdLat,
ORDERS_2:def 5,
B1;
y
<= zz by
OrdLat,
ORDERS_2:def 5,
B1;
hence thesis by
C1;
end;
hence thesis by
WAYBEL_0:def 6,
WAYBEL_0:def 1;
end;
assume
a1: (
LatRelStr L) is
directed;
for a,b be
Element of L holds (a
"\/" b)
= (b
"\/" a)
proof
let a,b be
Element of L;
reconsider aa = a, bb = b as
Element of (
LatRelStr L);
set X = (
[#] (
LatRelStr L));
consider z be
Element of (
LatRelStr L) such that
B2: z
in X & aa
<= z & bb
<= z by
WAYBEL_0:def 1,
a1,
WAYBEL_0:def 6;
reconsider zz = z as
Element of L;
B3: a
[= zz by
B2,
OrdLat,
ORDERS_2:def 5;
b
[= zz by
B2,
OrdLat,
ORDERS_2:def 5;
hence thesis by
DefB2,
B3;
end;
hence thesis;
end;
theorem ::
LATTAD_1:53
Th31143: L is
join-commutative iff L is
ADL-absorbing
proof
thus L is
join-commutative implies L is
ADL-absorbing
proof
assume
A1: L is
join-commutative;
let a,b be
Element of L;
(a
"\/" b)
= (b
"\/" a) by
A1;
hence thesis by
LATTICES:def 9;
end;
assume
B1: L is
ADL-absorbing;
let a,b be
Element of L;
(a
"/\" (b
"\/" a))
= a by
B1;
hence thesis by
Th3726;
end;
theorem ::
LATTAD_1:54
L is
join-commutative iff L is
meet-commutative by
Th31145;
theorem ::
LATTAD_1:55
Th31146: L is
join-commutative iff (
ThetaOrder L) is
antisymmetric
proof
set R = (
ThetaOrder L);
thus L is
join-commutative implies (
ThetaOrder L) is
antisymmetric
proof
assume L is
join-commutative;
then
A0: L is
meet-commutative by
Th31145;
for x,y be
object st
[x, y]
in R &
[y, x]
in R holds x
= y
proof
let x,y be
object;
assume
A1:
[x, y]
in R &
[y, x]
in R;
then
consider xx,yy be
Element of L such that
A3:
[x, y]
=
[xx, yy] & (xx
"/\" yy)
= yy;
A4: x
= xx & y
= yy by
A3,
XTUPLE_0: 1;
(xx
"/\" yy)
= yy & (yy
"/\" xx)
= xx by
ThetaOrdLat,
A1,
A4;
hence thesis by
A4,
A0;
end;
hence thesis by
PREFER_1: 31;
end;
assume
z1: (
ThetaOrder L) is
antisymmetric;
for x,y be
Element of L holds (x
"/\" y)
= (y
"/\" x)
proof
let x,y be
Element of L;
B1: ((x
"/\" y)
"/\" (y
"/\" x))
= ((y
"/\" x)
"/\" (y
"/\" x)) by
Lem310
.= (y
"/\" x) by
IMeet;
B2: ((y
"/\" x)
"/\" (x
"/\" y))
= ((x
"/\" y)
"/\" (x
"/\" y)) by
Lem310
.= (x
"/\" y) by
IMeet;
B3:
[(x
"/\" y), (y
"/\" x)]
in R by
B1;
[(y
"/\" x), (x
"/\" y)]
in R by
B2;
hence thesis by
z1,
B3,
PREFER_1: 31;
end;
then L is
meet-commutative;
hence thesis by
Th31145;
end;
theorem ::
LATTAD_1:56
L is
join-commutative iff (
ThetaOrder L) is
being_partial-order
proof
set R = (
ThetaOrder L);
thus L is
join-commutative implies (
ThetaOrder L) is
being_partial-order
proof
assume L is
join-commutative;
then R is
antisymmetric by
Th31146;
hence thesis by
ORDERS_1:def 5;
end;
assume (
ThetaOrder L) is
being_partial-order;
then R is
antisymmetric by
ORDERS_1:def 5;
hence thesis by
Th31146;
end;
registration
let L be
join-commutative
GAD_Lattice;
cluster (
ThetaOrder L) ->
antisymmetric;
coherence by
Th31146;
end
registration
cluster
join-commutative ->
ADL-absorbing for
GAD_Lattice;
coherence by
Th31143;
cluster
ADL-absorbing ->
join-commutative for
GAD_Lattice;
coherence by
Th31143;
end
registration
cluster
join-commutative ->
meet-commutative for
GAD_Lattice;
coherence by
Th31145;
cluster
meet-commutative ->
join-commutative for
GAD_Lattice;
coherence by
Th31145;
end
theorem ::
LATTAD_1:57
(for a,b,c be
Element of L holds ((a
"\/" b)
"/\" c)
= ((b
"\/" a)
"/\" c)) implies for a,b,c be
Element of L holds ((a
"\/" b)
"/\" c)
= ((a
"/\" c)
"\/" (b
"/\" c))
proof
assume
A1: for a,b,c be
Element of L holds ((a
"\/" b)
"/\" c)
= ((b
"\/" a)
"/\" c);
let a,b,c be
Element of L;
((a
"/\" c)
"\/" (b
"/\" c))
= (((a
"/\" c)
"\/" b)
"/\" ((a
"/\" c)
"\/" c)) by
DefLDS
.= (((a
"/\" c)
"\/" b)
"/\" c) by
LATTICES:def 8
.= ((b
"\/" (a
"/\" c))
"/\" c) by
A1
.= (((b
"\/" a)
"/\" (b
"\/" c))
"/\" c) by
DefLDS
.= ((((b
"\/" a)
"/\" b)
"\/" ((b
"\/" a)
"/\" c))
"/\" c) by
LATTICES:def 11
.= ((b
"\/" ((b
"\/" a)
"/\" c))
"/\" c) by
DefA2
.= (((b
"\/" (b
"\/" a))
"/\" (b
"\/" c))
"/\" c) by
DefLDS
.= ((b
"\/" (b
"\/" a))
"/\" ((b
"\/" c)
"/\" c)) by
LATTICES:def 7
.= ((b
"\/" (b
"\/" a))
"/\" ((c
"\/" b)
"/\" c)) by
A1
.= ((b
"\/" (b
"\/" a))
"/\" c) by
DefA2
.= ((b
"\/" a)
"/\" c) by
Lem36X
.= ((a
"\/" b)
"/\" c) by
A1;
hence thesis;
end;
theorem ::
LATTAD_1:58
(for a,b,c be
Element of L holds ((a
"\/" b)
"/\" c)
= ((a
"/\" c)
"\/" (b
"/\" c))) implies for a,b be
Element of L holds ((a
"\/" b)
"/\" b)
= b
proof
assume
A1: for a,b,c be
Element of L holds ((a
"\/" b)
"/\" c)
= ((a
"/\" c)
"\/" (b
"/\" c));
let a,b be
Element of L;
((a
"\/" b)
"/\" b)
= ((a
"/\" b)
"\/" (b
"/\" b)) by
A1
.= ((a
"/\" b)
"\/" b) by
IMeet
.= b by
LATTICES:def 8;
hence thesis;
end;
theorem ::
LATTAD_1:59
(for a,b be
Element of L holds ((a
"\/" b)
"/\" b)
= b) implies for a,b,c be
Element of L holds ((a
"\/" b)
"/\" c)
= ((b
"\/" a)
"/\" c)
proof
assume
AA: for a,b be
Element of L holds ((a
"\/" b)
"/\" b)
= b;
let a,b,c be
Element of L;
aa: ((b
"\/" a)
"/\" a)
= a by
AA;
S1: ex d be
Element of L st ((a
"\/" b)
"/\" c)
[= d & ((b
"\/" a)
"/\" c)
[= d
proof
take d = c;
thus thesis by
LATTICES:def 8;
end;
(((a
"\/" b)
"/\" c)
"\/" ((b
"\/" a)
"/\" c))
= (((b
"\/" a)
"/\" c)
"\/" ((a
"\/" b)
"/\" c)) by
S1,
DefB2;
then (((a
"\/" b)
"/\" c)
"/\" ((b
"\/" a)
"/\" c))
= (((b
"\/" a)
"/\" c)
"/\" ((a
"\/" b)
"/\" c)) by
IffComm;
then ((a
"\/" b)
"/\" (c
"/\" ((b
"\/" a)
"/\" c)))
= (((b
"\/" a)
"/\" c)
"/\" ((a
"\/" b)
"/\" c)) by
LATTICES:def 7;
then ((a
"\/" b)
"/\" (c
"/\" ((b
"\/" a)
"/\" c)))
= ((b
"\/" a)
"/\" (c
"/\" ((a
"\/" b)
"/\" c))) by
LATTICES:def 7;
then ((a
"\/" b)
"/\" ((b
"\/" a)
"/\" c))
= ((b
"\/" a)
"/\" (c
"/\" ((a
"\/" b)
"/\" c))) by
Lem36c;
then ((a
"\/" b)
"/\" ((b
"\/" a)
"/\" c))
= ((b
"\/" a)
"/\" ((a
"\/" b)
"/\" c)) by
Lem36c;
then ((a
"\/" b)
"/\" (((b
"\/" a)
"/\" c)
"/\" c))
= (((b
"\/" a)
"/\" ((a
"\/" b)
"/\" c))
"/\" c) by
LATTICES:def 7;
then ((a
"\/" b)
"/\" ((b
"\/" a)
"/\" (c
"/\" c)))
= (((b
"\/" a)
"/\" ((a
"\/" b)
"/\" c))
"/\" c) by
LATTICES:def 7;
then ((a
"\/" b)
"/\" ((b
"\/" a)
"/\" c))
= (((b
"\/" a)
"/\" ((a
"\/" b)
"/\" c))
"/\" c) by
IMeet;
then ((a
"\/" b)
"/\" ((b
"\/" a)
"/\" c))
= ((b
"\/" a)
"/\" (((a
"\/" b)
"/\" c)
"/\" c)) by
LATTICES:def 7;
then ((a
"\/" b)
"/\" ((b
"\/" a)
"/\" c))
= ((b
"\/" a)
"/\" ((a
"\/" b)
"/\" (c
"/\" c))) by
LATTICES:def 7;
then ((a
"\/" b)
"/\" ((b
"\/" a)
"/\" c))
= ((b
"\/" a)
"/\" ((a
"\/" b)
"/\" c)) by
IMeet;
then (((a
"\/" b)
"/\" (b
"\/" a))
"/\" c)
= ((b
"\/" a)
"/\" ((a
"\/" b)
"/\" c)) by
LATTICES:def 7;
then (((a
"\/" b)
"/\" (b
"\/" a))
"/\" c)
= (((b
"\/" a)
"/\" (a
"\/" b))
"/\" c) by
LATTICES:def 7;
then ((((a
"\/" b)
"/\" b)
"\/" ((a
"\/" b)
"/\" a))
"/\" c)
= (((b
"\/" a)
"/\" (a
"\/" b))
"/\" c) by
LATTICES:def 11;
then ((b
"\/" ((a
"\/" b)
"/\" a))
"/\" c)
= (((b
"\/" a)
"/\" (a
"\/" b))
"/\" c) by
AA;
then ((b
"\/" a)
"/\" c)
= (((b
"\/" a)
"/\" (a
"\/" b))
"/\" c) by
DefA2;
then ((b
"\/" a)
"/\" c)
= ((((b
"\/" a)
"/\" a)
"\/" ((b
"\/" a)
"/\" b))
"/\" c) by
LATTICES:def 11;
hence thesis by
DefA2,
aa;
end;
begin
definition
let L;
::
LATTAD_1:def13
attr L is
with_zero means ex x be
Element of L st for a be
Element of L holds (x
"/\" a)
= x;
end
registration
cluster
trivial ->
with_zero for non
empty
GAD_Lattice;
coherence
proof
let L be non
empty
GAD_Lattice;
assume L is
trivial;
then
reconsider LL = L as
trivial non
empty
GAD_Lattice;
set a = the
Element of LL;
for x be
Element of LL holds (a
"/\" x)
= a by
SUBSET_1:def 7;
hence thesis;
end;
end
registration
cluster
with_zero for non
empty
GAD_Lattice;
existence
proof
take L = the
trivial
GAD_Lattice;
thus thesis;
end;
end
definition
let L;
assume
A1: L is
with_zero;
::
LATTAD_1:def14
func
bottom L ->
Element of L means
:
GADL0: for a be
Element of L holds (it
"/\" a)
= it ;
existence by
A1;
uniqueness
proof
let b1,b2 be
Element of L such that
A2: for a be
Element of L holds (b1
"/\" a)
= b1 and
A3: for a be
Element of L holds (b2
"/\" a)
= b2;
A4: (b1
"/\" b2)
= b1 by
A2;
A5: (b2
"/\" b1)
= b2 by
A3;
((b1
"/\" b2)
"/\" b1)
= (b1
"/\" (b2
"/\" b1)) by
LATTICES:def 7
.= (b1
"/\" b2) by
A3;
then (b1
"/\" b2)
[= b1 by
LATTICES:def 8;
hence thesis by
A4,
A5,
Th3715;
end;
end
reserve L for
with_zero
GAD_Lattice,
x,y for
Element of L;
theorem ::
LATTAD_1:60
(x
"\/" (
bottom L))
= x
proof
((
bottom L)
"/\" x)
= (
bottom L) by
GADL0;
then
a1: (
bottom L)
[= x by
LATTICES:def 8;
set b1 = (
bottom L);
(x
"/\" b1)
= (x
"/\" (b1
"/\" x)) by
GADL0
.= ((x
"/\" b1)
"/\" x) by
LATTICES:def 7
.= ((b1
"/\" x)
"/\" x) by
Lem310
.= (b1
"/\" x) by
GADL0;
then ((b1
"/\" x)
"\/" b1)
= b1 by
LATTICES:def 8;
hence thesis by
a1,
Th3716;
end;
theorem ::
LATTAD_1:61
((
bottom L)
"\/" x)
= x
proof
((
bottom L)
"/\" x)
= (
bottom L) by
GADL0;
hence thesis by
LATTICES:def 8;
end;
theorem ::
LATTAD_1:62
(x
"/\" (
bottom L))
= (
bottom L)
proof
set b1 = (
bottom L);
A4: (b1
"/\" x)
= b1 by
GADL0;
(x
"/\" b1)
= ((x
"/\" b1)
"/\" x) by
LATTICES:def 7,
A4
.= ((b1
"/\" x)
"/\" x) by
Lem310
.= (b1
"/\" x) by
GADL0;
hence thesis by
GADL0;
end;
theorem ::
LATTAD_1:63
Lem316: (x
"/\" y)
= (
bottom L) iff (y
"/\" x)
= (
bottom L)
proof
set b1 = (
bottom L);
thus (x
"/\" y)
= (
bottom L) implies (y
"/\" x)
= (
bottom L)
proof
assume
Z1: (x
"/\" y)
= b1;
(y
"/\" x)
= (y
"/\" (x
"/\" x)) by
IMeet
.= ((y
"/\" x)
"/\" x) by
LATTICES:def 7
.= ((x
"/\" y)
"/\" x) by
Lem310
.= b1 by
GADL0,
Z1;
hence (y
"/\" x)
= (
bottom L);
end;
assume
Z1: (y
"/\" x)
= (
bottom L);
(x
"/\" y)
= (x
"/\" (y
"/\" y)) by
IMeet
.= ((x
"/\" y)
"/\" y) by
LATTICES:def 7
.= ((y
"/\" x)
"/\" y) by
Lem310
.= b1 by
GADL0,
Z1;
hence thesis;
end;
theorem ::
LATTAD_1:64
(x
"/\" y)
= (
bottom L) implies (x
"\/" y)
= (y
"\/" x)
proof
assume (x
"/\" y)
= (
bottom L);
then ((y
"/\" x)
"\/" y)
= y by
Th3751,
Lem316;
hence thesis by
Th3716;
end;
begin
Lmx2: ex x be
Element of
{1, 2, 3} st x
= 1
proof
reconsider x = 1 as
Element of
{1, 2, 3} by
ENUMSET1:def 1;
take x;
thus thesis;
end;
definition
let x,y be
Element of
{1, 2, 3};
::
LATTAD_1:def15
func x
example32"/\" y ->
Element of
{1, 2, 3} equals
:
Defx5: 1 if y
= 1 or (y
= 2 & (x
= 1 or x
= 3)),
2 if x
= 2 & y
= 2,
3 if y
= 3;
coherence by
Lmx2;
consistency ;
::
LATTAD_1:def16
func x
example32"\/" y ->
Element of
{1, 2, 3} equals
:
Defx6: 1 if x
= 1 & (y
= 1 or y
= 3),
2 if x
= 2 or (x
= 1 & y
= 2),
3 if x
= 3;
coherence ;
consistency ;
end
definition
::
LATTAD_1:def17
func
example32\/ ->
BinOp of
{1, 2, 3} means
:
Defx7: for x,y be
Element of
{1, 2, 3} holds (it
. (x,y))
= (x
example32"\/" y);
existence
proof
deffunc
O(
Element of
{1, 2, 3},
Element of
{1, 2, 3}) = ($1
example32"\/" $2);
ex o be
BinOp of
{1, 2, 3} st for a,b be
Element of
{1, 2, 3} holds (o
. (a,b))
=
O(a,b) from
BINOP_1:sch 4;
hence thesis;
end;
uniqueness
proof
let o1,o2 be
BinOp of
{1, 2, 3} such that
A1: for x,y be
Element of
{1, 2, 3} holds (o1
. (x,y))
= (x
example32"\/" y) and
A2: for x,y be
Element of
{1, 2, 3} holds (o2
. (x,y))
= (x
example32"\/" y);
now
let x,y be
Element of
{1, 2, 3};
thus (o1
. (x,y))
= (x
example32"\/" y) by
A1
.= (o2
. (x,y)) by
A2;
end;
hence thesis by
BINOP_1: 2;
end;
::
LATTAD_1:def18
func
example32/\ ->
BinOp of
{1, 2, 3} means
:
Defx8: for x,y be
Element of
{1, 2, 3} holds (it
. (x,y))
= (x
example32"/\" y);
existence
proof
deffunc
O(
Element of
{1, 2, 3},
Element of
{1, 2, 3}) = ($1
example32"/\" $2);
ex o be
BinOp of
{1, 2, 3} st for a,b be
Element of
{1, 2, 3} holds (o
. (a,b))
=
O(a,b) from
BINOP_1:sch 4;
hence thesis;
end;
uniqueness
proof
let o1,o2 be
BinOp of
{1, 2, 3} such that
A1: for x,y be
Element of
{1, 2, 3} holds (o1
. (x,y))
= (x
example32"/\" y) and
A2: for x,y be
Element of
{1, 2, 3} holds (o2
. (x,y))
= (x
example32"/\" y);
now
let x,y be
Element of
{1, 2, 3};
thus (o1
. (x,y))
= (x
example32"/\" y) by
A1
.= (o2
. (x,y)) by
A2;
end;
hence thesis by
BINOP_1: 2;
end;
end
theorem ::
LATTAD_1:65
ex L be non
empty
LattStr st (for x be
Element of L holds x
= 1 or x
= 2 or x
= 3) & (for x,y be
Element of L holds ((x
"/\" y)
= 1 iff y
= 1 or (y
= 2 & (x
= 1 or x
= 3))) & ((x
"/\" y)
= 2 iff x
= 2 & y
= 2) & ((x
"/\" y)
= 3 iff y
= 3)) & (for x,y be
Element of L holds ((x
"\/" y)
= 1 iff x
= 1 & (y
= 1 or y
= 3)) & ((x
"\/" y)
= 2 iff x
= 2 or (x
= 1 & y
= 2)) & ((x
"\/" y)
= 3 iff x
= 3)) & L is
GAD_Lattice & not L is
AD_Lattice
proof
set L =
LattStr (#
{1, 2, 3},
example32\/ ,
example32/\ #);
take L;
thus for x be
Element of L holds x
= 1 or x
= 2 or x
= 3 by
ENUMSET1:def 1;
thus
Z7: for x,y be
Element of L holds ((x
"/\" y)
= 1 iff y
= 1 or (y
= 2 & (x
= 1 or x
= 3))) & ((x
"/\" y)
= 2 iff x
= 2 & y
= 2) & ((x
"/\" y)
= 3 iff y
= 3)
proof
let x,y be
Element of L;
reconsider x1 = x, y1 = y as
Element of
{1, 2, 3};
B1: (x
"/\" y)
= (x1
example32"/\" y1) by
Defx8;
thus (x
"/\" y)
= 1 iff y
= 1 or (y
= 2 & (x
= 1 or x
= 3))
proof
hereby
assume
B3: (x
"/\" y)
= 1;
assume not (y
= 1 or (y
= 2 & (x
= 1 or x
= 3)));
then (x
= 2 & y
= 2) or y
= 3 by
ENUMSET1:def 1;
hence contradiction by
B3,
B1,
Defx5;
end;
assume y
= 1 or (y
= 2 & (x
= 1 or x
= 3));
hence (x
"/\" y)
= 1 by
B1,
Defx5;
end;
thus (x
"/\" y)
= 2 iff x
= 2 & y
= 2
proof
hereby
assume
B3: (x
"/\" y)
= 2;
assume not (x
= 2 & y
= 2);
then (y
= 1 or (y
= 2 & (x
= 1 or x
= 3))) or y
= 3 by
ENUMSET1:def 1;
hence contradiction by
B3,
B1,
Defx5;
end;
assume x
= 2 & y
= 2;
hence (x
"/\" y)
= 2 by
B1,
Defx5;
end;
thus (x
"/\" y)
= 3 iff y
= 3
proof
hereby
assume
B3: (x
"/\" y)
= 3;
assume not y
= 3;
then (y
= 1 or (y
= 2 & (x
= 1 or x
= 3))) or (x
= 2 & y
= 2) by
ENUMSET1:def 1;
hence contradiction by
B3,
B1,
Defx5;
end;
assume y
= 3;
hence (x
"/\" y)
= 3 by
B1,
Defx5;
end;
end;
thus
Z8: for x,y be
Element of L holds ((x
"\/" y)
= 1 iff x
= 1 & (y
= 1 or y
= 3)) & ((x
"\/" y)
= 2 iff x
= 2 or (x
= 1 & y
= 2)) & ((x
"\/" y)
= 3 iff x
= 3)
proof
let x,y be
Element of L;
reconsider x1 = x, y1 = y as
Element of
{1, 2, 3};
B1: (x
"\/" y)
= (x1
example32"\/" y1) by
Defx7;
thus (x
"\/" y)
= 1 iff x
= 1 & (y
= 1 or y
= 3)
proof
hereby
assume
B3: (x
"\/" y)
= 1;
assume not (x
= 1 & (y
= 1 or y
= 3));
then (x
= 2 or (x
= 1 & y
= 2)) or x
= 3 by
ENUMSET1:def 1;
hence contradiction by
B3,
B1,
Defx6;
end;
assume x
= 1 & (y
= 1 or y
= 3);
hence (x
"\/" y)
= 1 by
B1,
Defx6;
end;
thus (x
"\/" y)
= 2 iff x
= 2 or (x
= 1 & y
= 2)
proof
hereby
assume
B3: (x
"\/" y)
= 2;
assume not (x
= 2 or (x
= 1 & y
= 2));
then (x
= 1 & (y
= 1 or y
= 3)) or x
= 3 by
ENUMSET1:def 1;
hence contradiction by
B3,
B1,
Defx6;
end;
assume x
= 2 or (x
= 1 & y
= 2);
hence (x
"\/" y)
= 2 by
B1,
Defx6;
end;
thus (x
"\/" y)
= 3 iff x
= 3
proof
hereby
assume
B3: (x
"\/" y)
= 3;
assume not (x
= 3);
then (x
= 1 & (y
= 1 or y
= 3)) or (x
= 2 or (x
= 1 & y
= 2)) by
ENUMSET1:def 1;
hence contradiction by
B3,
B1,
Defx6;
end;
assume x
= 3;
hence (x
"\/" y)
= 3 by
B1,
Defx6;
end;
end;
for x,y,z be
Element of L holds (x
"/\" (y
"/\" z))
= ((x
"/\" y)
"/\" z)
proof
let x,y,z be
Element of L;
per cases by
ENUMSET1:def 1;
suppose
B1: (x
"/\" (y
"/\" z))
= 1;
then (y
"/\" z)
= 1 or ((y
"/\" z)
= 2 & (x
= 1 or x
= 3)) by
Z7;
then (z
= 1 or (z
= 2 & (y
= 1 or y
= 3))) or ((y
= 2 & z
= 2) & (x
= 1 or x
= 3)) by
Z7;
then z
= 1 or (z
= 2 & ((x
"/\" y)
= 1 or (x
"/\" y)
= 3)) by
Z7;
hence thesis by
B1,
Z7;
end;
suppose
B1: (x
"/\" (y
"/\" z))
= 2;
then x
= 2 & (y
"/\" z)
= 2 by
Z7;
then x
= 2 & y
= 2 & z
= 2 by
Z7;
then (x
"/\" y)
= 2 & z
= 2 by
Z7;
hence thesis by
B1,
Z7;
end;
suppose
B1: (x
"/\" (y
"/\" z))
= 3;
then (y
"/\" z)
= 3 by
Z7;
then z
= 3 by
Z7;
hence thesis by
B1,
Z7;
end;
end;
then
C1: L is
meet-associative;
for x,y,z be
Element of L holds (x
"/\" (y
"\/" z))
= ((x
"/\" y)
"\/" (x
"/\" z))
proof
let x,y,z be
Element of L;
per cases by
ENUMSET1:def 1;
suppose
B1: (x
"/\" (y
"\/" z))
= 1;
(y
"\/" z)
= 1 or ((y
"\/" z)
= 2 & (x
= 1 or x
= 3)) by
B1,
Z7;
then (y
= 1 or (y
= 2 & (x
= 1 or x
= 3))) & ((z
= 1 or (z
= 2 & (x
= 1 or x
= 3))) or z
= 3) by
Z8,
ENUMSET1:def 1;
then (x
"/\" y)
= 1 & ((x
"/\" z)
= 1 or z
= 3) by
Z7;
hence thesis by
B1,
Z7,
Z8;
end;
suppose
B1: (x
"/\" (y
"\/" z))
= 2;
then x
= 2 & (y
"\/" z)
= 2 by
Z7;
then x
= 2 & (y
= 2 or (y
= 1 & z
= 2)) by
Z8;
then (x
"/\" y)
= 2 or ((x
"/\" y)
= 1 & (x
"/\" z)
= 2) by
Z7;
hence thesis by
B1,
Z8;
end;
suppose
B1: (x
"/\" (y
"\/" z))
= 3;
then (y
"\/" z)
= 3 by
Z7;
then (x
"/\" y)
= 3 by
Z7,
Z8;
hence thesis by
B1,
Z8;
end;
end;
then
C2: L is
distributive;
for x,y,z be
Element of L holds (x
"\/" (y
"/\" z))
= ((x
"\/" y)
"/\" (x
"\/" z))
proof
let x,y,z be
Element of L;
per cases by
ENUMSET1:def 1;
suppose
B1: (x
"\/" (y
"/\" z))
= 1;
then x
= 1 & ((y
"/\" z)
= 1 or (y
"/\" z)
= 3) by
Z8;
then x
= 1 & ((z
= 1 or (z
= 2 & (y
= 1 or y
= 3))) or z
= 3) by
Z7;
then (x
"\/" z)
= 1 or ((x
"\/" z)
= 2 & ((x
"\/" y)
= 1 or (x
"\/" y)
= 3)) by
Z8;
hence thesis by
B1,
Z7;
end;
suppose
B1: (x
"\/" (y
"/\" z))
= 2;
then x
= 2 or (x
= 1 & (y
"/\" z)
= 2) by
Z8;
then x
= 2 or (x
= 1 & y
= 2 & z
= 2) by
Z7;
then (x
"\/" y)
= 2 & (x
"\/" z)
= 2 by
Z8;
hence thesis by
B1,
Z7;
end;
suppose
B1: (x
"\/" (y
"/\" z))
= 3;
then x
= 3 by
Z8;
then (x
"\/" z)
= 3 by
Z8;
hence thesis by
B1,
Z7;
end;
end;
then
C3: L is
left-Distributive;
for x,y be
Element of L holds (x
"/\" (x
"\/" y))
= x
proof
let x,y be
Element of L;
per cases by
ENUMSET1:def 1;
suppose
B1: (x
"/\" (x
"\/" y))
= 1;
then (x
"\/" y)
= 1 or ((x
"\/" y)
= 2 & (x
= 1 or x
= 3)) by
Z7;
hence thesis by
B1,
Z8;
end;
suppose (x
"/\" (x
"\/" y))
= 2;
hence thesis by
Z7;
end;
suppose
B1: (x
"/\" (x
"\/" y))
= 3;
then (x
"\/" y)
= 3 by
Z7;
hence thesis by
B1,
Z8;
end;
end;
then
C4: L is
join-absorbing;
for x,y be
Element of L holds ((x
"\/" y)
"/\" x)
= x
proof
let x,y be
Element of L;
per cases by
ENUMSET1:def 1;
suppose
B1: ((x
"\/" y)
"/\" x)
= 1;
then x
= 1 or (x
= 2 & ((x
"\/" y)
= 1 or (x
"\/" y)
= 3)) by
Z7;
hence thesis by
B1,
Z8;
end;
suppose ((x
"\/" y)
"/\" x)
= 2;
hence thesis by
Z7;
end;
suppose ((x
"\/" y)
"/\" x)
= 3;
hence thesis by
Z7;
end;
end;
then
C5: L is
Meet-Absorbing;
for x,y be
Element of L holds ((x
"/\" y)
"\/" y)
= y
proof
let x,y be
Element of L;
per cases by
ENUMSET1:def 1;
suppose
B1: ((x
"/\" y)
"\/" y)
= 1;
then (x
"/\" y)
= 1 & (y
= 1 or y
= 3) by
Z8;
hence thesis by
B1,
Z7;
end;
suppose
B1: ((x
"/\" y)
"\/" y)
= 2;
then (x
"/\" y)
= 2 or ((x
"/\" y)
= 1 & y
= 2) by
Z8;
hence thesis by
Z7,
B1;
end;
suppose
B1: ((x
"/\" y)
"\/" y)
= 3;
then (x
"/\" y)
= 3 by
Z8;
hence thesis by
B1,
Z7;
end;
end;
then
C6: L is
meet-absorbing;
not L is
Meet-absorbing
proof
assume
B1: L is
Meet-absorbing;
set x = 3, y = 2;
reconsider x = 3, y = 2 as
Element of L by
ENUMSET1:def 1;
((x
"\/" y)
"/\" y)
= 1 by
Z7,
Z8;
hence contradiction by
B1;
end;
hence thesis by
C1,
C2,
C3,
C4,
C5,
C6;
end;
Lmx3: ex x be
Element of
{1, 2, 3} st x
= 2
proof
reconsider x = 2 as
Element of
{1, 2, 3} by
ENUMSET1:def 1;
take x;
thus thesis;
end;
definition
let x,y be
Element of
{1, 2, 3};
::
LATTAD_1:def19
func x
example33"/\" y ->
Element of
{1, 2, 3} equals
:
Defx5: 1 if x
= 1 & y
= 1,
2 if y
= 2 or (y
= 1 & (x
= 2 or x
= 3)),
3 if y
= 3;
coherence by
Lmx3;
consistency ;
::
LATTAD_1:def20
func x
example33"\/" y ->
Element of
{1, 2, 3} equals
:
Defx6: 1 if x
= 1 or (x
= 2 & y
= 1),
2 if x
= 2 & (y
= 2 or y
= 3),
3 if x
= 3;
coherence ;
consistency ;
end
definition
::
LATTAD_1:def21
func
example33\/ ->
BinOp of
{1, 2, 3} means
:
Defx7: for x,y be
Element of
{1, 2, 3} holds (it
. (x,y))
= (x
example33"\/" y);
existence
proof
deffunc
O(
Element of
{1, 2, 3},
Element of
{1, 2, 3}) = ($1
example33"\/" $2);
ex o be
BinOp of
{1, 2, 3} st for a,b be
Element of
{1, 2, 3} holds (o
. (a,b))
=
O(a,b) from
BINOP_1:sch 4;
hence thesis;
end;
uniqueness
proof
let o1,o2 be
BinOp of
{1, 2, 3} such that
A1: for x,y be
Element of
{1, 2, 3} holds (o1
. (x,y))
= (x
example33"\/" y) and
A2: for x,y be
Element of
{1, 2, 3} holds (o2
. (x,y))
= (x
example33"\/" y);
now
let x,y be
Element of
{1, 2, 3};
thus (o1
. (x,y))
= (x
example33"\/" y) by
A1
.= (o2
. (x,y)) by
A2;
end;
hence thesis by
BINOP_1: 2;
end;
::
LATTAD_1:def22
func
example33/\ ->
BinOp of
{1, 2, 3} means
:
Defx8: for x,y be
Element of
{1, 2, 3} holds (it
. (x,y))
= (x
example33"/\" y);
existence
proof
deffunc
O(
Element of
{1, 2, 3},
Element of
{1, 2, 3}) = ($1
example33"/\" $2);
ex o be
BinOp of
{1, 2, 3} st for a,b be
Element of
{1, 2, 3} holds (o
. (a,b))
=
O(a,b) from
BINOP_1:sch 4;
hence thesis;
end;
uniqueness
proof
let o1,o2 be
BinOp of
{1, 2, 3} such that
A1: for x,y be
Element of
{1, 2, 3} holds (o1
. (x,y))
= (x
example33"/\" y) and
A2: for x,y be
Element of
{1, 2, 3} holds (o2
. (x,y))
= (x
example33"/\" y);
now
let x,y be
Element of
{1, 2, 3};
thus (o1
. (x,y))
= (x
example33"/\" y) by
A1
.= (o2
. (x,y)) by
A2;
end;
hence thesis by
BINOP_1: 2;
end;
end
theorem ::
LATTAD_1:66
ex L be non
empty
LattStr st (for x be
Element of L holds x
= 1 or x
= 2 or x
= 3) & (for x,y be
Element of L holds ((x
"/\" y)
= 1 iff x
= 1 & y
= 1) & ((x
"/\" y)
= 2 iff y
= 2 or (y
= 1 & (x
= 2 or x
= 3))) & ((x
"/\" y)
= 3 iff y
= 3)) & (for x,y be
Element of L holds ((x
"\/" y)
= 1 iff x
= 1 or (x
= 2 & y
= 1)) & ((x
"\/" y)
= 2 iff x
= 2 & (y
= 2 or y
= 3)) & ((x
"\/" y)
= 3 iff x
= 3)) & L is
GAD_Lattice
proof
set L =
LattStr (#
{1, 2, 3},
example33\/ ,
example33/\ #);
take L;
thus for x be
Element of L holds x
= 1 or x
= 2 or x
= 3 by
ENUMSET1:def 1;
thus
Z7: for x,y be
Element of L holds ((x
"/\" y)
= 1 iff x
= 1 & y
= 1) & ((x
"/\" y)
= 2 iff y
= 2 or (y
= 1 & (x
= 2 or x
= 3))) & ((x
"/\" y)
= 3 iff y
= 3)
proof
let x,y be
Element of L;
reconsider x1 = x, y1 = y as
Element of
{1, 2, 3};
B1: (x
"/\" y)
= (x1
example33"/\" y1) by
Defx8;
thus (x
"/\" y)
= 1 iff x
= 1 & y
= 1
proof
hereby
assume
B3: (x
"/\" y)
= 1;
assume not (x
= 1 & y
= 1);
then (y
= 2 or (y
= 1 & (x
= 2 or x
= 3))) or y
= 3 by
ENUMSET1:def 1;
hence contradiction by
B3,
B1,
Defx5;
end;
assume x
= 1 & y
= 1;
hence (x
"/\" y)
= 1 by
B1,
Defx5;
end;
thus (x
"/\" y)
= 2 iff y
= 2 or (y
= 1 & (x
= 2 or x
= 3))
proof
hereby
assume
B3: (x
"/\" y)
= 2;
assume not (y
= 2 or (y
= 1 & (x
= 2 or x
= 3)));
then (x
= 1 & y
= 1) or y
= 3 by
ENUMSET1:def 1;
hence contradiction by
B3,
B1,
Defx5;
end;
assume y
= 2 or (y
= 1 & (x
= 2 or x
= 3));
hence (x
"/\" y)
= 2 by
B1,
Defx5;
end;
thus (x
"/\" y)
= 3 iff y
= 3
proof
hereby
assume
B3: (x
"/\" y)
= 3;
assume not y
= 3;
then (y
= 2 or (y
= 1 & (x
= 2 or x
= 3))) or (x
= 1 & y
= 1) by
ENUMSET1:def 1;
hence contradiction by
B3,
B1,
Defx5;
end;
assume y
= 3;
hence (x
"/\" y)
= 3 by
B1,
Defx5;
end;
end;
thus
Z8: for x,y be
Element of L holds ((x
"\/" y)
= 1 iff x
= 1 or (x
= 2 & y
= 1)) & ((x
"\/" y)
= 2 iff x
= 2 & (y
= 2 or y
= 3)) & ((x
"\/" y)
= 3 iff x
= 3)
proof
let x,y be
Element of L;
reconsider x1 = x, y1 = y as
Element of
{1, 2, 3};
B1: (x
"\/" y)
= (x1
example33"\/" y1) by
Defx7;
thus (x
"\/" y)
= 1 iff x
= 1 or (x
= 2 & y
= 1)
proof
hereby
assume
B3: (x
"\/" y)
= 1;
assume not (x
= 1 or (x
= 2 & y
= 1));
then (x
= 2 & (y
= 2 or y
= 3)) or x
= 3 by
ENUMSET1:def 1;
hence contradiction by
B3,
B1,
Defx6;
end;
assume x
= 1 or (x
= 2 & y
= 1);
hence (x
"\/" y)
= 1 by
B1,
Defx6;
end;
thus (x
"\/" y)
= 2 iff x
= 2 & (y
= 2 or y
= 3)
proof
hereby
assume
B3: (x
"\/" y)
= 2;
assume not (x
= 2 & (y
= 2 or y
= 3));
then (x
= 1 or (x
= 2 & y
= 1)) or x
= 3 by
ENUMSET1:def 1;
hence contradiction by
B3,
B1,
Defx6;
end;
assume x
= 2 & (y
= 2 or y
= 3);
hence (x
"\/" y)
= 2 by
B1,
Defx6;
end;
thus (x
"\/" y)
= 3 iff x
= 3
proof
hereby
assume
B3: (x
"\/" y)
= 3;
assume not (x
= 3);
then (x
= 2 & (y
= 2 or y
= 3)) or (x
= 1 or (x
= 2 & y
= 1)) by
ENUMSET1:def 1;
hence contradiction by
B3,
B1,
Defx6;
end;
assume x
= 3;
hence (x
"\/" y)
= 3 by
B1,
Defx6;
end;
end;
for x,y,z be
Element of L holds (x
"/\" (y
"/\" z))
= ((x
"/\" y)
"/\" z)
proof
let x,y,z be
Element of L;
per cases by
ENUMSET1:def 1;
suppose
B1: (x
"/\" (y
"/\" z))
= 2;
then (y
"/\" z)
= 2 or ((y
"/\" z)
= 1 & (x
= 2 or x
= 3)) by
Z7;
then (z
= 2 or (z
= 1 & (y
= 2 or y
= 3))) or ((y
= 1 & z
= 1) & (x
= 2 or x
= 3)) by
Z7;
then z
= 2 or (z
= 1 & ((x
"/\" y)
= 2 or (x
"/\" y)
= 3)) by
Z7;
hence thesis by
B1,
Z7;
end;
suppose
B1: (x
"/\" (y
"/\" z))
= 1;
then x
= 1 & (y
"/\" z)
= 1 by
Z7;
then x
= 1 & y
= 1 & z
= 1 by
Z7;
then (x
"/\" y)
= 1 & z
= 1 by
Z7;
hence thesis by
B1,
Z7;
end;
suppose
B1: (x
"/\" (y
"/\" z))
= 3;
then (y
"/\" z)
= 3 by
Z7;
then z
= 3 by
Z7;
hence thesis by
B1,
Z7;
end;
end;
then
C1: L is
meet-associative;
for x,y,z be
Element of L holds (x
"/\" (y
"\/" z))
= ((x
"/\" y)
"\/" (x
"/\" z))
proof
let x,y,z be
Element of L;
per cases by
ENUMSET1:def 1;
suppose
B1: (x
"/\" (y
"\/" z))
= 2;
(y
"\/" z)
= 2 or ((y
"\/" z)
= 1 & (x
= 2 or x
= 3)) by
B1,
Z7;
then (y
= 2 or (y
= 1 & (x
= 2 or x
= 3))) & ((z
= 2 or (z
= 1 & (x
= 2 or x
= 3))) or z
= 3) by
Z8,
ENUMSET1:def 1;
then (x
"/\" y)
= 2 & ((x
"/\" z)
= 2 or z
= 3) by
Z7;
hence thesis by
B1,
Z7,
Z8;
end;
suppose
B1: (x
"/\" (y
"\/" z))
= 1;
then x
= 1 & (y
"\/" z)
= 1 by
Z7;
then x
= 1 & (y
= 1 or (y
= 2 & z
= 1)) by
Z8;
then (x
"/\" y)
= 1 or ((x
"/\" y)
= 2 & (x
"/\" z)
= 1) by
Z7;
hence thesis by
B1,
Z8;
end;
suppose
B1: (x
"/\" (y
"\/" z))
= 3;
then (y
"\/" z)
= 3 by
Z7;
then (x
"/\" y)
= 3 by
Z7,
Z8;
hence thesis by
B1,
Z8;
end;
end;
then
C2: L is
distributive;
for x,y,z be
Element of L holds (x
"\/" (y
"/\" z))
= ((x
"\/" y)
"/\" (x
"\/" z))
proof
let x,y,z be
Element of L;
per cases by
ENUMSET1:def 1;
suppose
B1: (x
"\/" (y
"/\" z))
= 2;
then x
= 2 & ((y
"/\" z)
= 2 or (y
"/\" z)
= 3) by
Z8;
then x
= 2 & ((z
= 2 or (z
= 1 & (y
= 2 or y
= 3))) or z
= 3) by
Z7;
then (x
"\/" z)
= 2 or ((x
"\/" z)
= 1 & ((x
"\/" y)
= 2 or (x
"\/" y)
= 3)) by
Z8;
hence thesis by
B1,
Z7;
end;
suppose
B1: (x
"\/" (y
"/\" z))
= 1;
then x
= 1 or (x
= 2 & (y
"/\" z)
= 1) by
Z8;
then x
= 1 or (x
= 2 & y
= 1 & z
= 1) by
Z7;
then (x
"\/" y)
= 1 & (x
"\/" z)
= 1 by
Z8;
hence thesis by
B1,
Z7;
end;
suppose
B1: (x
"\/" (y
"/\" z))
= 3;
then x
= 3 by
Z8;
then (x
"\/" z)
= 3 by
Z8;
hence thesis by
B1,
Z7;
end;
end;
then
C3: L is
left-Distributive;
for x,y be
Element of L holds (x
"/\" (x
"\/" y))
= x
proof
let x,y be
Element of L;
per cases by
ENUMSET1:def 1;
suppose
B1: (x
"/\" (x
"\/" y))
= 2;
then (x
"\/" y)
= 2 or ((x
"\/" y)
= 1 & (x
= 2 or x
= 3)) by
Z7;
hence thesis by
B1,
Z8;
end;
suppose (x
"/\" (x
"\/" y))
= 1;
hence thesis by
Z7;
end;
suppose
B1: (x
"/\" (x
"\/" y))
= 3;
then (x
"\/" y)
= 3 by
Z7;
hence thesis by
B1,
Z8;
end;
end;
then
C4: L is
join-absorbing;
for x,y be
Element of L holds ((x
"\/" y)
"/\" x)
= x
proof
let x,y be
Element of L;
per cases by
ENUMSET1:def 1;
suppose
B1: ((x
"\/" y)
"/\" x)
= 2;
then x
= 2 or (x
= 1 & ((x
"\/" y)
= 2 or (x
"\/" y)
= 3)) by
Z7;
hence thesis by
B1,
Z8;
end;
suppose ((x
"\/" y)
"/\" x)
= 1;
hence thesis by
Z7;
end;
suppose ((x
"\/" y)
"/\" x)
= 3;
hence thesis by
Z7;
end;
end;
then
C5: L is
Meet-Absorbing;
for x,y be
Element of L holds ((x
"/\" y)
"\/" y)
= y
proof
let x,y be
Element of L;
per cases by
ENUMSET1:def 1;
suppose
B1: ((x
"/\" y)
"\/" y)
= 2;
then (x
"/\" y)
= 2 & (y
= 2 or y
= 3) by
Z8;
hence thesis by
B1,
Z7;
end;
suppose
B1: ((x
"/\" y)
"\/" y)
= 1;
then (x
"/\" y)
= 1 or ((x
"/\" y)
= 2 & y
= 1) by
Z8;
hence thesis by
Z7,
B1;
end;
suppose
B1: ((x
"/\" y)
"\/" y)
= 3;
then (x
"/\" y)
= 3 by
Z8;
hence thesis by
B1,
Z7;
end;
end;
then L is
meet-absorbing;
hence thesis by
C1,
C2,
C3,
C4,
C5;
end;
definition
let L be non
empty
LattStr;
::
LATTAD_1:def23
mode
SubLattStr of L ->
LattStr means
:
Defx1: the
carrier of it
c= the
carrier of L & the
L_join of it
= (the
L_join of L
|| the
carrier of it ) & the
L_meet of it
= (the
L_meet of L
|| the
carrier of it );
existence
proof
take L;
thus thesis;
end;
end
registration
let L be non
empty
LattStr;
cluster
strict for
SubLattStr of L;
correctness
proof
set S =
LattStr (# the
carrier of L, the
L_join of L, the
L_meet of L #);
the
L_join of S
= (the
L_join of L
|| the
carrier of S) & the
L_meet of S
= (the
L_meet of L
|| the
carrier of S);
then S is
SubLattStr of L by
Defx1;
hence thesis;
end;
end
definition
::$Canceled
end
registration
let L be non
empty
LattStr;
cluster
meet-closed
join-closed non
empty for
Subset of L;
existence
proof
take (
[#] L);
thus thesis;
end;
end
definition
let L be non
empty
LattStr;
mode
ClosedSubset of L is
meet-closed
join-closed
Subset of L;
end
definition
let L be non
empty
LattStr;
let P be
ClosedSubset of L;
::
LATTAD_1:def26
func
latt (L,P) ->
strict
SubLattStr of L means
:
Defx4: the
carrier of it
= P;
existence
proof
for o be
set st o
in
[:P, P:] holds (the
L_join of L
. o)
in P
proof
let o be
set;
assume o
in
[:P, P:];
then
consider x,y be
object such that
B1: x
in P & y
in P & o
=
[x, y] by
ZFMISC_1:def 2;
reconsider x, y as
Element of L by
B1;
(the
L_join of L
. o)
= (x
"\/" y) by
B1;
hence (the
L_join of L
. o)
in P by
B1,
LATTICES:def 25;
end;
then P is
Preserv of the
L_join of L by
REALSET1:def 1;
then
reconsider lj = (the
L_join of L
|| P) as
BinOp of P by
REALSET1: 2;
for o be
set st o
in
[:P, P:] holds (the
L_meet of L
. o)
in P
proof
let o be
set;
assume o
in
[:P, P:];
then
consider x,y be
object such that
B1: x
in P & y
in P & o
=
[x, y] by
ZFMISC_1:def 2;
reconsider x, y as
Element of L by
B1;
(the
L_meet of L
. o)
= (x
"/\" y) by
B1;
hence (the
L_meet of L
. o)
in P by
B1,
LATTICES:def 24;
end;
then P is
Preserv of the
L_meet of L by
REALSET1:def 1;
then
reconsider lm = (the
L_meet of L
|| P) as
BinOp of P by
REALSET1: 2;
reconsider S =
LattStr (# P, lj, lm #) as
strict
SubLattStr of L by
Defx1;
take S;
thus thesis;
end;
uniqueness
proof
let S1,S2 be
strict
SubLattStr of L;
assume
A1: the
carrier of S1
= P & the
carrier of S2
= P;
A2: the
L_join of S1
= (the
L_join of L
|| the
carrier of S1) by
Defx1
.= the
L_join of S2 by
A1,
Defx1;
the
L_meet of S1
= (the
L_meet of L
|| the
carrier of S1) by
Defx1
.= the
L_meet of S2 by
A1,
Defx1;
hence thesis by
A1,
A2;
end;
end
registration
let L be non
empty
LattStr;
let S be non
empty
ClosedSubset of L;
cluster (
latt (L,S)) -> non
empty;
correctness by
Defx4;
end
registration
let L be non
empty
LattStr;
cluster non
empty for
SubLattStr of L;
correctness
proof
take (
latt (L, the non
empty
ClosedSubset of L));
thus thesis;
end;
end
theorem ::
LATTAD_1:67
Thx3: for L be non
empty
LattStr, S be non
empty
SubLattStr of L, x1,x2 be
Element of L, y1,y2 be
Element of S st x1
= y1 & x2
= y2 holds (x1
"\/" x2)
= (y1
"\/" y2)
proof
let L be non
empty
LattStr;
let S be non
empty
SubLattStr of L;
let x1,x2 be
Element of L;
let y1,y2 be
Element of S;
assume
Z4: x1
= y1 & x2
= y2;
Z5: the
L_join of S
= (the
L_join of L
|| the
carrier of S) by
Defx1
.= (the
L_join of L
|
[:the
carrier of S, the
carrier of S:]);
[y1, y2]
in
[:the
carrier of S, the
carrier of S:] by
ZFMISC_1:def 2;
hence (x1
"\/" x2)
= (y1
"\/" y2) by
Z4,
Z5,
FUNCT_1: 49;
end;
theorem ::
LATTAD_1:68
Thx4: for L be non
empty
LattStr, S be non
empty
SubLattStr of L, x1,x2 be
Element of L, y1,y2 be
Element of S st x1
= y1 & x2
= y2 holds (x1
"/\" x2)
= (y1
"/\" y2)
proof
let L be non
empty
LattStr;
let S be non
empty
SubLattStr of L;
let x1,x2 be
Element of L;
let y1,y2 be
Element of S;
assume
Z4: x1
= y1 & x2
= y2;
Z5: the
L_meet of S
= (the
L_meet of L
|| the
carrier of S) by
Defx1
.= (the
L_meet of L
|
[:the
carrier of S, the
carrier of S:]);
[y1, y2]
in
[:the
carrier of S, the
carrier of S:] by
ZFMISC_1:def 2;
hence (x1
"/\" x2)
= (y1
"/\" y2) by
Z4,
Z5,
FUNCT_1: 49;
end;
theorem ::
LATTAD_1:69
Thx1: for L be non
empty
LattStr, S be non
empty
ClosedSubset of L holds (L is
meet-associative implies (
latt (L,S)) is
meet-associative) & (L is
meet-absorbing implies (
latt (L,S)) is
meet-absorbing) & (L is
meet-commutative implies (
latt (L,S)) is
meet-commutative) & (L is
join-associative implies (
latt (L,S)) is
join-associative) & (L is
join-absorbing implies (
latt (L,S)) is
join-absorbing) & (L is
join-commutative implies (
latt (L,S)) is
join-commutative) & (L is
Meet-Absorbing implies (
latt (L,S)) is
Meet-Absorbing) & (L is
distributive implies (
latt (L,S)) is
distributive) & (L is
left-Distributive implies (
latt (L,S)) is
left-Distributive)
proof
let L be non
empty
LattStr;
let S be non
empty
ClosedSubset of L;
thus L is
meet-associative implies (
latt (L,S)) is
meet-associative
proof
assume
Z2: L is
meet-associative;
let a,b,c be
Element of (
latt (L,S));
reconsider x = a, y = b, z = c as
Element of L by
Defx1,
TARSKI:def 3;
(b
"/\" c)
= (y
"/\" z) & (a
"/\" b)
= (x
"/\" y) by
Thx4;
then (a
"/\" (b
"/\" c))
= (x
"/\" (y
"/\" z)) & ((a
"/\" b)
"/\" c)
= ((x
"/\" y)
"/\" z) by
Thx4;
hence (a
"/\" (b
"/\" c))
= ((a
"/\" b)
"/\" c) by
Z2;
end;
thus L is
meet-absorbing implies (
latt (L,S)) is
meet-absorbing
proof
assume
Z3: L is
meet-absorbing;
let a,b be
Element of (
latt (L,S));
reconsider x = a, y = b as
Element of L by
Defx1,
TARSKI:def 3;
(a
"/\" b)
= (x
"/\" y) by
Thx4;
then ((a
"/\" b)
"\/" b)
= ((x
"/\" y)
"\/" y) by
Thx3;
hence ((a
"/\" b)
"\/" b)
= b by
Z3;
end;
thus L is
meet-commutative implies (
latt (L,S)) is
meet-commutative
proof
assume
Z3: L is
meet-commutative;
let a,b be
Element of (
latt (L,S));
reconsider x = a, y = b as
Element of L by
Defx1,
TARSKI:def 3;
(a
"/\" b)
= (x
"/\" y) & (b
"/\" a)
= (y
"/\" x) by
Thx4;
hence (a
"/\" b)
= (b
"/\" a) by
Z3;
end;
thus L is
join-associative implies (
latt (L,S)) is
join-associative
proof
assume
Z3: L is
join-associative;
let a,b,c be
Element of (
latt (L,S));
reconsider x = a, y = b, z = c as
Element of L by
Defx1,
TARSKI:def 3;
(b
"\/" c)
= (y
"\/" z) & (a
"\/" b)
= (x
"\/" y) by
Thx3;
then (a
"\/" (b
"\/" c))
= (x
"\/" (y
"\/" z)) & ((a
"\/" b)
"\/" c)
= ((x
"\/" y)
"\/" z) by
Thx3;
hence (a
"\/" (b
"\/" c))
= ((a
"\/" b)
"\/" c) by
Z3;
end;
thus L is
join-absorbing implies (
latt (L,S)) is
join-absorbing
proof
assume
Z3: L is
join-absorbing;
let a,b be
Element of (
latt (L,S));
reconsider x = a, y = b as
Element of L by
Defx1,
TARSKI:def 3;
(a
"\/" b)
= (x
"\/" y) by
Thx3;
then (a
"/\" (a
"\/" b))
= (x
"/\" (x
"\/" y)) by
Thx4;
hence (a
"/\" (a
"\/" b))
= a by
Z3;
end;
thus L is
join-commutative implies (
latt (L,S)) is
join-commutative
proof
assume
Z3: L is
join-commutative;
let a,b be
Element of (
latt (L,S));
reconsider x = a, y = b as
Element of L by
Defx1,
TARSKI:def 3;
(a
"\/" b)
= (x
"\/" y) & (b
"\/" a)
= (y
"\/" x) by
Thx3;
hence (a
"\/" b)
= (b
"\/" a) by
Z3;
end;
thus L is
Meet-Absorbing implies (
latt (L,S)) is
Meet-Absorbing
proof
assume
Z3: L is
Meet-Absorbing;
let a,b be
Element of (
latt (L,S));
reconsider x = a, y = b as
Element of L by
Defx1,
TARSKI:def 3;
(a
"\/" b)
= (x
"\/" y) by
Thx3;
then ((a
"\/" b)
"/\" a)
= ((x
"\/" y)
"/\" x) by
Thx4;
hence ((a
"\/" b)
"/\" a)
= a by
Z3;
end;
thus L is
distributive implies (
latt (L,S)) is
distributive
proof
assume
Z3: L is
distributive;
let a,b,c be
Element of (
latt (L,S));
reconsider x = a, y = b, z = c as
Element of L by
Defx1,
TARSKI:def 3;
(b
"\/" c)
= (y
"\/" z) & (a
"/\" b)
= (x
"/\" y) & (a
"/\" c)
= (x
"/\" z) by
Thx3,
Thx4;
then (a
"/\" (b
"\/" c))
= (x
"/\" (y
"\/" z)) & ((a
"/\" b)
"\/" (a
"/\" c))
= ((x
"/\" y)
"\/" (x
"/\" z)) by
Thx3,
Thx4;
hence (a
"/\" (b
"\/" c))
= ((a
"/\" b)
"\/" (a
"/\" c)) by
Z3;
end;
thus L is
left-Distributive implies (
latt (L,S)) is
left-Distributive
proof
assume
Z3: L is
left-Distributive;
let a,b,c be
Element of (
latt (L,S));
reconsider x = a, y = b, z = c as
Element of L by
Defx1,
TARSKI:def 3;
(b
"/\" c)
= (y
"/\" z) & (a
"\/" b)
= (x
"\/" y) & (a
"\/" c)
= (x
"\/" z) by
Thx3,
Thx4;
then (a
"\/" (b
"/\" c))
= (x
"\/" (y
"/\" z)) & ((a
"\/" b)
"/\" (a
"\/" c))
= ((x
"\/" y)
"/\" (x
"\/" z)) by
Thx3,
Thx4;
hence (a
"\/" (b
"/\" c))
= ((a
"\/" b)
"/\" (a
"\/" c)) by
Z3;
end;
end;
theorem ::
LATTAD_1:70
for a be
Element of L, X be
set st X
= the set of all (x
"/\" a) where x be
Element of L holds X
= { x where x be
Element of L : x
[= a } & X is
ClosedSubset of L
proof
let a be
Element of L;
let X be
set;
assume
B1: X
= the set of all (x
"/\" a) where x be
Element of L;
B2: for o be
object holds o
in the set of all (x
"/\" a) where x be
Element of L iff o
in { x where x be
Element of L : x
[= a }
proof
let o be
object;
hereby
assume o
in the set of all (x
"/\" a) where x be
Element of L;
then
consider x be
Element of L such that
A1: o
= (x
"/\" a);
set y = (x
"/\" a);
L is
meet-absorbing;
then y
[= a;
hence o
in { y where y be
Element of L : y
[= a } by
A1;
end;
assume o
in { x where x be
Element of L : x
[= a };
then
consider x be
Element of L such that
A1: o
= x & x
[= a;
(x
"/\" a)
= x by
A1,
LATTICES:def 9;
hence o
in the set of all (x
"/\" a) where x be
Element of L by
A1;
end;
now
let o be
object;
assume o
in X;
then
consider x be
Element of L such that
B3: o
= (x
"/\" a) by
B1;
thus o
in the
carrier of L by
B3;
end;
then
reconsider S = X as
Subset of L by
TARSKI:def 3;
for p,q be
Element of L st p
in S & q
in S holds (p
"/\" q)
in S
proof
let p,q be
Element of L;
assume p
in S;
then
consider x be
Element of L such that
B5: p
= (x
"/\" a) by
B1;
assume q
in S;
then
consider y be
Element of L such that
B6: q
= (y
"/\" a) by
B1;
(p
"/\" q)
= (x
"/\" (a
"/\" (y
"/\" a))) by
B5,
B6,
LATTICES:def 7
.= (x
"/\" ((a
"/\" y)
"/\" a)) by
LATTICES:def 7
.= ((x
"/\" (a
"/\" y))
"/\" a) by
LATTICES:def 7;
hence (p
"/\" q)
in S by
B1;
end;
then
B4: S is
meet-closed;
for p,q be
Element of L st p
in S & q
in S holds (p
"\/" q)
in S
proof
let p,q be
Element of L;
assume p
in S;
then
consider x be
Element of L such that
B5: p
= (x
"/\" a) by
B1;
assume q
in S;
then
consider y be
Element of L such that
B6: q
= (y
"/\" a) by
B1;
(p
"\/" q)
= (((x
"/\" a)
"\/" y)
"/\" ((x
"/\" a)
"\/" a)) by
B5,
B6,
DefLDS
.= (((x
"/\" a)
"\/" y)
"/\" a) by
LATTICES:def 8;
hence (p
"\/" q)
in S by
B1;
end;
then S is
join-closed;
hence thesis by
B1,
B2,
B4,
TARSKI: 2;
end;
theorem ::
LATTAD_1:71
for a be
Element of L, S be non
empty
ClosedSubset of L, b be
Element of (
latt (L,S)) st b
= a & S
= the set of all (x
"/\" a) where x be
Element of L holds (
latt (L,S)) is
Lattice-like
distributive & (for c be
Element of (
latt (L,S)) holds (b
"\/" c)
= b & (c
"\/" b)
= b & c
[= b)
proof
let a be
Element of L;
let S be non
empty
ClosedSubset of L;
let b be
Element of (
latt (L,S));
assume
Z5: b
= a;
assume
Z2: S
= the set of all (x
"/\" a) where x be
Element of L;
for y1,y2 be
Element of (
latt (L,S)) holds (y1
"/\" y2)
= (y2
"/\" y1)
proof
let y1,y2 be
Element of (
latt (L,S));
y1
in the
carrier of (
latt (L,S));
then y1
in S by
Defx4;
then
consider x1 be
Element of L such that
B1: y1
= (x1
"/\" a) by
Z2;
y2
in the
carrier of (
latt (L,S));
then y2
in S by
Defx4;
then
consider x2 be
Element of L such that
B2: y2
= (x2
"/\" a) by
Z2;
thus (y1
"/\" y2)
= ((x1
"/\" a)
"/\" (x2
"/\" a)) by
B1,
B2,
Thx4
.= ((a
"/\" x1)
"/\" (x2
"/\" a)) by
Lem310
.= (a
"/\" (x1
"/\" (x2
"/\" a))) by
LATTICES:def 7
.= (a
"/\" ((x1
"/\" x2)
"/\" a)) by
LATTICES:def 7
.= (a
"/\" ((x2
"/\" x1)
"/\" a)) by
Lem310
.= (a
"/\" (x2
"/\" (x1
"/\" a))) by
LATTICES:def 7
.= ((a
"/\" x2)
"/\" (x1
"/\" a)) by
LATTICES:def 7
.= ((x2
"/\" a)
"/\" (x1
"/\" a)) by
Lem310
.= (y2
"/\" y1) by
B1,
B2,
Thx4;
end;
then
Z12: (
latt (L,S)) is
meet-commutative;
(
latt (L,S)) is
GAD_Lattice by
Thx1;
hence (
latt (L,S)) is
Lattice-like
distributive by
Z12,
Th31141;
let c be
Element of (
latt (L,S));
c
in the
carrier of (
latt (L,S));
then c
in S by
Defx4;
then
consider x be
Element of L such that
A1: c
= (x
"/\" a) by
Z2;
reconsider d = c as
Element of L by
A1;
thus (b
"\/" c)
= (a
"\/" (x
"/\" a)) by
A1,
Z5,
Thx3
.= b by
Z5,
ThA5;
thus
A2: (c
"\/" b)
= ((x
"/\" a)
"\/" a) by
A1,
Z5,
Thx3
.= b by
Z5,
LATTICES:def 8;
thus c
[= b by
A2;
end;