:: Finite Join and Finite Meet, and Dual Lattices :: by Andrzej Trybulec :: :: Received August 10, 1990 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, SUBSET_1, FUNCT_1, RELAT_1, FUNCT_4, TARSKI, FINSUB_1, BINOP_1, LATTICES, EQREL_1, STRUCT_0, PBOOLE, SETWISEO, FUNCOP_1, FILTER_0, FINSET_1, XXREAL_2, LATTICE2; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, PARTFUN1, FUNCOP_1, BINOP_1, FINSET_1, STRUCT_0, LATTICES, FINSUB_1, SETWISEO, FILTER_0; constructors BINOP_1, FUNCOP_1, FUNCT_4, SETWISEO, GROUP_1, FILTER_0, RELSET_1; registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES, RELSET_1, FILTER_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; theorem :: LATTICE2:1 dom (g|B) = B; theorem :: LATTICE2:2 f|B = g|B iff for x st x in B holds g.x = f.x; theorem :: LATTICE2:3 for B being set holds f +* g|B is Function of A,C; theorem :: LATTICE2:4 g|B +* f = f; theorem :: LATTICE2:5 for f,g being Function holds g c= f implies f +* g = f; theorem :: LATTICE2:6 f +* f|B = f; theorem :: LATTICE2:7 (for x st x in B holds g.x = f.x) implies f +* g|B = f; reserve B for Element of Fin A; theorem :: LATTICE2:8 g|B +* f = f; theorem :: LATTICE2:9 dom (g|B) = B; theorem :: LATTICE2:10 (for x st x in B holds g.x = f.x) implies f +* g|B = f; definition let D be non empty set; let o,o9 be BinOp of D; pred o absorbs o9 means :: LATTICE2:def 1 for x,y being Element of D holds o.(x,o9.(x,y )) = x; end; notation let D be non empty set; let o,o9 be BinOp of D; antonym o doesn't_absorb o9 for o absorbs o9; end; :: Dual Lattice structures reserve L for non empty LattStr, a,b,c for Element of L; theorem :: LATTICE2:11 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; registration let L be non empty LattStr; cluster L.: -> non empty; end; theorem :: LATTICE2:12 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:13 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; theorem :: LATTICE2:14 (for v holds u "\/" v = v) implies u = Bottom L; theorem :: LATTICE2:15 (for v holds (the L_join of L).(u,v) = v) implies u = Bottom L; theorem :: LATTICE2:16 (for v holds u "/\" v = v) implies u = Top L; theorem :: LATTICE2:17 (for v holds (the L_meet of L).(u,v) = v) implies u = Top L; registration let L; cluster the L_join of L -> idempotent; end; registration let L be join-commutative non empty \/-SemiLattStr; cluster the L_join of L -> commutative; end; theorem :: LATTICE2:18 the L_join of L is having_a_unity implies Bottom L = the_unity_wrt the L_join of L; registration let L be join-associative non empty \/-SemiLattStr; cluster the L_join of L -> associative; end; registration let L; cluster the L_meet of L -> idempotent; end; registration let L be meet-commutative non empty /\-SemiLattStr; cluster the L_meet of L -> commutative; end; registration let L be meet-associative non empty /\-SemiLattStr; cluster the L_meet of L -> associative; end; theorem :: LATTICE2:19 the L_meet of L is having_a_unity implies Top L = the_unity_wrt the L_meet of L; theorem :: LATTICE2:20 the L_join of L is_distributive_wrt the L_join of L; theorem :: LATTICE2:21 L is D_Lattice implies the L_join of L is_distributive_wrt the L_meet of L; theorem :: LATTICE2:22 the L_join of L is_distributive_wrt the L_meet of L implies L is distributive ; theorem :: LATTICE2:23 L is D_Lattice implies the L_meet of L is_distributive_wrt the L_join of L; theorem :: LATTICE2:24 the L_meet of L is_distributive_wrt the L_join of L implies L is distributive ; theorem :: LATTICE2:25 the L_meet of L is_distributive_wrt the L_meet of L; theorem :: LATTICE2:26 the L_join of L absorbs the L_meet of L; theorem :: LATTICE2:27 the L_meet of L absorbs the L_join of L; definition let A be non empty set, L be Lattice; let B be Element of Fin 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 Element of Fin A, f,g for Function of A, the carrier of L; theorem :: LATTICE2:28 x in B implies f.x [= FinJoin(B,f); theorem :: LATTICE2:29 (ex x st x in B & u [= f.x) implies u [= FinJoin(B,f); theorem :: LATTICE2:30 (for x st x in B holds f.x = u) & B <> {} implies FinJoin(B,f) = u; theorem :: LATTICE2:31 FinJoin(B,f) [= u implies for x st x in B holds f.x [= u; theorem :: LATTICE2:32 B <> {} & (for x st x in B holds f.x [= u) implies FinJoin(B,f) [= u; theorem :: LATTICE2:33 B <> {} & (for x st x in B holds f.x [= g.x) implies FinJoin(B,f) [= FinJoin(B,g); theorem :: LATTICE2:34 B <> {} & f|B = g|B implies FinJoin(B,f) = FinJoin(B,g); theorem :: LATTICE2:35 B <> {} implies v "\/" FinJoin(B,f) = FinJoin(B, (the L_join of L)[;]( v, f ) ); registration let L be Lattice; cluster L.: -> Lattice-like; end; theorem :: LATTICE2:36 for L being Lattice, B being Element of Fin A for f being Function of A, the carrier of L, f9 being Function of A, the carrier of L.: st f = f9 holds FinJoin(B,f) = FinMeet(B,f9) & FinMeet(B,f) = FinJoin(B,f9); theorem :: LATTICE2:37 for a9,b9 being Element of L.: st a = a9 & b = b9 holds a "/\" b = a9"\/" b9 & a "\/" b = a9"/\" b9; theorem :: LATTICE2:38 a [= b implies for a9,b9 being Element of L.: st a = a9 & b = b9 holds b9 [= a9; theorem :: LATTICE2:39 for a9,b9 being Element of L.: st a9 [= b9 & a = a9 & b = b9 holds b [= a; :: Dualizations theorem :: LATTICE2:40 x in B implies FinMeet(B,f) [= f.x; theorem :: LATTICE2:41 (ex x st x in B & f.x [= u) implies FinMeet(B,f)[= u; theorem :: LATTICE2:42 (for x st x in B holds f.x = u) & B <> {} implies FinMeet(B,f) = u; theorem :: LATTICE2:43 B <> {} implies v "/\" FinMeet(B,f) = FinMeet(B, (the L_meet of L)[;]( v, f ) ); theorem :: LATTICE2:44 u [= FinMeet(B,f) implies for x st x in B holds u [= f.x; theorem :: LATTICE2:45 B <> {} & f|B = g|B implies FinMeet(B,f) = FinMeet(B,g); theorem :: LATTICE2:46 B <> {} & (for x st x in B holds u [= f.x) implies u [= FinMeet( B,f); theorem :: LATTICE2:47 B <> {} & (for x st x in B holds f.x [= g.x) implies FinMeet(B,f) [= FinMeet(B,g); theorem :: LATTICE2:48 for L being Lattice holds L is lower-bounded iff L.: is upper-bounded; theorem :: LATTICE2:49 for L being Lattice holds L is upper-bounded iff L.: is lower-bounded; theorem :: LATTICE2:50 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:51 Bottom L is_a_unity_wrt the L_join of L; registration let L; cluster the L_join of L -> having_a_unity; end; theorem :: LATTICE2:52 Bottom L = the_unity_wrt the L_join of L; theorem :: LATTICE2:53 f|B = g|B implies FinJoin(B,f) = FinJoin(B,g); theorem :: LATTICE2:54 (for x st x in B holds f.x [= u) implies FinJoin(B,f) [= u; theorem :: LATTICE2:55 (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:56 Top L is_a_unity_wrt the L_meet of L; registration let L; cluster the L_meet of L -> having_a_unity; end; theorem :: LATTICE2:57 Top L = the_unity_wrt the L_meet of L; theorem :: LATTICE2:58 f|B = g|B implies FinMeet(B,f) = FinMeet(B,g); theorem :: LATTICE2:59 (for x st x in B holds u [= f.x) implies u [= FinMeet(B,f); theorem :: LATTICE2:60 (for x st x in B holds f.x [= g.x) implies FinMeet(B,f) [= FinMeet(B,g ); theorem :: LATTICE2:61 for L being 0_Lattice holds Bottom L = Top (L.:); theorem :: LATTICE2:62 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:63 the L_meet of L is_distributive_wrt the L_join of L; theorem :: LATTICE2:64 (the L_meet of L).(u, FinJoin(B, f)) = FinJoin(B, (the L_meet of L)[;](u,f)); theorem :: LATTICE2:65 (for x st x in B holds g.x = u "/\" f.x) implies u "/\" FinJoin(B,f) = FinJoin(B,g); theorem :: LATTICE2:66 u "/\" FinJoin(B,f) = FinJoin(B, (the L_meet of L)[;](u, f)); :: Heyting Lattices definition let IT be Lattice; attr IT is Heyting means :: LATTICE2:def 5 IT is implicative lower-bounded; end; registration cluster Heyting for Lattice; end; registration cluster Heyting -> implicative lower-bounded for Lattice; cluster implicative lower-bounded -> Heyting for Lattice; end; definition mode H_Lattice is Heyting Lattice; end; registration cluster Heyting strict for Lattice; end; theorem :: LATTICE2:67 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:68 for L being Lattice holds L is finite iff L.: is finite; registration cluster finite -> lower-bounded for Lattice; cluster finite -> upper-bounded for Lattice; end; registration cluster finite -> bounded for Lattice; end; registration cluster distributive finite -> Heyting for Lattice; end;