Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### 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;

Back to top