Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Finite Join and Finite Meet, and Dual Lattices

by
Andrzej Trybulec

Received August 10, 1990

MML identifier: LATTICE2
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, RELAT_1, BOOLE, FUNCT_4, FINSUB_1, BINOP_1, LATTICES,
SETWISEO, FUNCOP_1, FILTER_0, FINSET_1, LATTICE2;
notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4,
PARTFUN1, FUNCOP_1, BINOP_1, STRUCT_0, LATTICES, FINSET_1, FINSUB_1,
GROUP_1, SETWISEO, FILTER_0;
constructors FUNCT_4, FUNCOP_1, BINOP_1, GROUP_1, SETWISEO, FILTER_0,
PARTFUN1, MEMBERED, XBOOLE_0;
clusters LATTICES, STRUCT_0, RELSET_1, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1,
XBOOLE_0;
requirements SUBSET, BOOLE;

begin :: Auxiliary theorems

reserve A for set, C for non empty set,
B for Subset of A,
x for Element of A,
f,g for Function of A,C;

canceled;

theorem :: LATTICE2:2
dom (g|B) = B;

canceled 2;

theorem :: LATTICE2:5
f|B = g|B iff for x st x in B holds g.x = f.x;

theorem :: LATTICE2:6
for B being set holds f +* g|B is Function of A,C;

theorem :: LATTICE2:7
g|B +* f = f;

theorem :: LATTICE2:8
for f,g being Function holds g <= f implies f +* g = f;

theorem :: LATTICE2:9
f +* f|B = f;

theorem :: LATTICE2:10
(for x st x in B holds g.x = f.x) implies f +* g|B = f;

reserve B for Finite_Subset of A;

canceled;

theorem :: LATTICE2:12
g|B +* f = f;

theorem :: LATTICE2:13
dom (g|B) = B;

theorem :: LATTICE2:14
(for x st x in B holds g.x = f.x) implies f +* g|B = f;

canceled;

theorem :: LATTICE2:16
f|B = g|B implies f.:B = g.:B;

definition let D be non empty set;
let o,o' be BinOp of D;
pred o absorbs o' means
:: LATTICE2:def 1
for x,y being Element of D holds o.(x,o'.(x,y)) = x;
antonym o doesn't_absorb o';
end;

:: Dual Lattice structures

reserve L for non empty LattStr,
a,b,c for Element of L;

theorem :: LATTICE2:17
the L_join of L is commutative associative &
the L_meet of L is commutative associative &
the L_join of L absorbs the L_meet of L &
the L_meet of L absorbs the L_join of L
implies L is Lattice-like;

definition let L be LattStr;
func L.: -> strict LattStr equals
:: LATTICE2:def 2
LattStr(#the carrier of L, the L_meet of L, the L_join of L#);
end;

definition let L be non empty LattStr;
cluster L.: -> non empty;
end;

theorem :: LATTICE2:18
the carrier of L = the carrier of L.: &
the L_join of L = the L_meet of L.: &
the L_meet of L = the L_join of L.:;

theorem :: LATTICE2:19
for L being strict non empty LattStr holds L.:.: = L;

:: General Lattices

reserve L for Lattice;
reserve a,b,c,u,v for Element of L;

canceled;

theorem :: LATTICE2:21
(for v holds u "\/" v = v) implies u = Bottom L;

theorem :: LATTICE2:22
(for v holds (the L_join of L).(u,v) = v) implies u = Bottom L;

canceled;

theorem :: LATTICE2:24
(for v holds u "/\" v = v) implies u = Top L;

theorem :: LATTICE2:25
(for v holds (the L_meet of L).(u,v) = v) implies u = Top L;

theorem :: LATTICE2:26
the L_join of L is idempotent;

theorem :: LATTICE2:27
for L being join-commutative (non empty \/-SemiLattStr) holds
the L_join of L is commutative;

theorem :: LATTICE2:28
the L_join of L has_a_unity implies Bottom L = the_unity_wrt the L_join of L;

theorem :: LATTICE2:29
for L being join-associative (non empty \/-SemiLattStr) holds
the L_join of L is associative;

theorem :: LATTICE2:30
the L_meet of L is idempotent;

theorem :: LATTICE2:31
for L being meet-commutative (non empty /\-SemiLattStr) holds
the L_meet of L is commutative;

theorem :: LATTICE2:32
for L being meet-associative (non empty /\-SemiLattStr) holds
the L_meet of L is associative;

definition let L be join-commutative (non empty \/-SemiLattStr);
cluster the L_join of L -> commutative;
end;

definition let L be join-associative (non empty \/-SemiLattStr);
cluster the L_join of L -> associative;
end;

definition let L be meet-commutative (non empty /\-SemiLattStr);
cluster the L_meet of L -> commutative;
end;

definition let L be meet-associative (non empty /\-SemiLattStr);
cluster the L_meet of L -> associative;
end;

theorem :: LATTICE2:33
the L_meet of L has_a_unity implies Top L = the_unity_wrt the L_meet of L;

theorem :: LATTICE2:34
the L_join of L is_distributive_wrt the L_join of L;

theorem :: LATTICE2:35
L is D_Lattice implies
the L_join of L is_distributive_wrt the L_meet of L;

theorem :: LATTICE2:36
the L_join of L is_distributive_wrt the L_meet of L
implies L is distributive;

theorem :: LATTICE2:37
L is D_Lattice implies
the L_meet of L is_distributive_wrt the L_join of L;

theorem :: LATTICE2:38
the L_meet of L is_distributive_wrt the L_join of L
implies L is distributive;

theorem :: LATTICE2:39
the L_meet of L is_distributive_wrt the L_meet of L;

theorem :: LATTICE2:40
the L_join of L absorbs the L_meet of L;

theorem :: LATTICE2:41
the L_meet of L absorbs the L_join of L;

definition let A be non empty set, L be Lattice;
let B be Finite_Subset of A; let f be Function of A, the carrier of L;
func FinJoin(B, f) -> Element of L equals
:: LATTICE2:def 3
(the L_join of L)\$\$(B,f);
func FinMeet(B, f) -> Element of L equals
:: LATTICE2:def 4
(the L_meet of L)\$\$(B,f);
end;

reserve A for non empty set,
x for Element of A,
B for Finite_Subset of A,
f,g for Function of A, the carrier of L;

canceled;

theorem :: LATTICE2:43
x in B implies f.x [= FinJoin(B,f);

theorem :: LATTICE2:44
(ex x st x in B & u [= f.x) implies u [= FinJoin(B,f);

theorem :: LATTICE2:45
(for x st x in B holds f.x = u) & B <> {} implies FinJoin(B,f) = u;

theorem :: LATTICE2:46
FinJoin(B,f) [= u implies for x st x in B holds f.x [= u;

theorem :: LATTICE2:47
B <> {} & (for x st x in B holds f.x [= u) implies FinJoin(B,f) [= u;

theorem :: LATTICE2:48
B <> {} & (for x st x in B holds f.x [= g.x)
implies FinJoin(B,f) [= FinJoin(B,g);

theorem :: LATTICE2:49
B <> {} & f|B = g|B implies FinJoin(B,f) = FinJoin(B,g);

theorem :: LATTICE2:50
B <> {} implies v "\/" FinJoin(B,f) = FinJoin(B, (the L_join of L)[;](v,f)
);

definition let L be Lattice;
cluster L.: -> Lattice-like;
end;

theorem :: LATTICE2:51
for L being Lattice,
B being Finite_Subset of A
for f being Function of A, the carrier of L,
f' being Function of A, the carrier of L.: st f = f'
holds FinJoin(B,f) = FinMeet(B,f') &
FinMeet(B,f) = FinJoin(B,f');

theorem :: LATTICE2:52
for a',b' being Element of L.: st a = a' & b = b' holds
a "/\" b = a'"\/" b' & a "\/" b = a'"/\" b';

theorem :: LATTICE2:53
a [= b implies
for a',b' being Element of L.: st a = a' & b = b'
holds b' [= a';

theorem :: LATTICE2:54
for a',b' being Element of L.:
st a' [= b' & a = a' & b = b'
holds b [= a;

:: Dualizations

theorem :: LATTICE2:55
x in B implies FinMeet(B,f) [= f.x;

theorem :: LATTICE2:56
(ex x st x in B & f.x [= u) implies FinMeet(B,f)[= u;

theorem :: LATTICE2:57
(for x st x in B holds f.x = u) & B <> {} implies FinMeet(B,f) = u;

theorem :: LATTICE2:58
B <> {} implies v "/\" FinMeet(B,f) = FinMeet(B, (the L_meet of L)[;](v,f))
;

theorem :: LATTICE2:59
u [= FinMeet(B,f) implies for x st x in B holds u [= f.x;

theorem :: LATTICE2:60
B <> {} & f|B = g|B implies FinMeet(B,f) = FinMeet(B,g);

theorem :: LATTICE2:61
B <> {} & (for x st x in B holds u [= f.x) implies u [= FinMeet(B,f);

theorem :: LATTICE2:62
B <> {} & (for x st x in B holds f.x [= g.x)
implies FinMeet(B,f) [= FinMeet(B,g);

theorem :: LATTICE2:63
for L being Lattice holds L is lower-bounded iff L.: is upper-bounded;

theorem :: LATTICE2:64
for L being Lattice holds L is upper-bounded iff L.: is lower-bounded;

theorem :: LATTICE2:65
L is D_Lattice iff L.: is D_Lattice;

:::::::::::::::::::::::::::
::
:: Lower bounded lattices
::
:::::::::::::::::::::::::::

reserve L for 0_Lattice,
f,g for Function of A, the carrier of L,
u for Element of L;

theorem :: LATTICE2:66
Bottom L is_a_unity_wrt the L_join of L;

theorem :: LATTICE2:67
the L_join of L has_a_unity;

theorem :: LATTICE2:68
Bottom L = the_unity_wrt the L_join of L;

theorem :: LATTICE2:69
f|B = g|B implies FinJoin(B,f) = FinJoin(B,g);

theorem :: LATTICE2:70
(for x st x in B holds f.x [= u) implies FinJoin(B,f) [= u;

theorem :: LATTICE2:71
(for x st x in B holds f.x [= g.x)
implies FinJoin(B,f) [= FinJoin(B,g);

:::::::::::::::::::::::::::
::
:: Upper bounded lattices
::
:::::::::::::::::::::::::::

reserve L for 1_Lattice,
f,g for Function of A, the carrier of L,
u for Element of L;

theorem :: LATTICE2:72
Top L is_a_unity_wrt the L_meet of L;

theorem :: LATTICE2:73
the L_meet of L has_a_unity;

theorem :: LATTICE2:74
Top L = the_unity_wrt the L_meet of L;

theorem :: LATTICE2:75
f|B = g|B implies FinMeet(B,f) = FinMeet(B,g);

theorem :: LATTICE2:76
(for x st x in B holds u [= f.x) implies u [= FinMeet(B,f);

theorem :: LATTICE2:77
(for x st x in B holds f.x [= g.x)
implies FinMeet(B,f) [= FinMeet(B,g);

theorem :: LATTICE2:78
for L being 0_Lattice holds Bottom L = Top (L.:);

theorem :: LATTICE2:79
for L being 1_Lattice holds Top L = Bottom (L.:);

:::::::::::::::::::::::::::
::
:: Distributive lattices with the minimal element
::
:::::::::::::::::::::::::::

definition
mode D0_Lattice is distributive lower-bounded Lattice;
end;

reserve L for D0_Lattice,
f,g for (Function of A, the carrier of L),
u for Element of L;

theorem :: LATTICE2:80
the L_meet of L is_distributive_wrt the L_join of L;

theorem :: LATTICE2:81
(the L_meet of L).(u, FinJoin(B, f))
= FinJoin(B, (the L_meet of L)[;](u,f));

theorem :: LATTICE2:82
(for x st x in B holds g.x = u "/\" f.x)
implies u "/\" FinJoin(B,f) = FinJoin(B,g);

theorem :: LATTICE2:83
u "/\" FinJoin(B,f) = FinJoin(B, (the L_meet of L)[;](u, f));

:: Heyting Lattices

definition
let IT be Lattice;
canceled;

attr IT is Heyting means
:: LATTICE2:def 6
IT is implicative lower-bounded;
end;

definition
cluster Heyting Lattice;
end;

definition
cluster Heyting -> implicative lower-bounded Lattice;
cluster implicative lower-bounded -> Heyting Lattice;
end;

definition
mode H_Lattice is Heyting Lattice;
end;

definition
cluster Heyting strict Lattice;
end;

theorem :: LATTICE2:84
for L being 0_Lattice holds
L is H_Lattice iff
for x,z being Element of L
ex y being Element of L st x "/\" y [= z
& for v being Element of L st x "/\" v [= z holds v [= y;

theorem :: LATTICE2:85
for L being Lattice holds L is finite iff L.: is finite;

definition
cluster finite -> lower-bounded Lattice;
cluster finite -> upper-bounded Lattice;
end;

definition
cluster finite -> bounded Lattice;
end;

definition
cluster distributive finite -> Heyting Lattice;
end;
```