:: Lattice of Substitutions Is a Heyting Algebra :: by Adam Grabowski :: :: Received December 31, 1998 :: Copyright (c) 1998-2021 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 SUBSET_1, SUBSTLAT, FINSET_1, FUNCT_1, FINSUB_1, PARTFUN1, TARSKI, XBOOLE_0, SETWISEO, ORDINAL4, NORMFORM, RELAT_1, ARYTM_1, LATTICES, FUNCT_2, HEYTING1, BINOP_1, STRUCT_0, ZFMISC_1, FDIFF_1, EQREL_1, LATTICE2, PBOOLE, FUNCOP_1, FILTER_0, XBOOLEAN, HEYTING2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCOP_1, BINOP_1, FINSET_1, FINSUB_1, FUNCT_2, PARTFUN1, LATTICES, STRUCT_0, SUBSTLAT, SETWISEO, HEYTING1, LATTICE2, FILTER_0; constructors FUNCOP_1, SETWISEO, FILTER_0, LATTICE2, HEYTING1, SUBSTLAT, RELSET_1, BINOP_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1, FINSUB_1, SETWISEO, STRUCT_0, LATTICES, SUBSTLAT, FUNCT_2, RELSET_1, PRE_POLY, LATTICE2; requirements SUBSET, BOOLE; begin :: Preliminaries reserve V, C, x, a, b for set; reserve A, B for Element of SubstitutionSet (V, C); theorem :: HEYTING2:1 for a, b being set st b in SubstitutionSet (V, C) & a in b holds a is finite Function; begin :: Some properties of sets of substitutions theorem :: HEYTING2:2 for a being finite Element of PFuncs (V, C) holds {a} in SubstitutionSet (V, C); theorem :: HEYTING2:3 A ^ B = A implies for a be set st a in A ex b be set st b in B & b c= a; theorem :: HEYTING2:4 mi (A ^ B) = A implies for a be set st a in A ex b be set st b in B & b c= a; theorem :: HEYTING2:5 (for a be set st a in A ex b be set st b in B & b c= a) implies mi (A ^ B) = A; definition let V be set, C be finite set; let A be Element of Fin PFuncs (V, C); func Involved A -> set means :: HEYTING2:def 1 for x being object holds x in it iff ex f being finite Function st f in A & x in dom f; end; reserve C for finite set; reserve A, B for Element of SubstitutionSet (V, C); theorem :: HEYTING2:6 for V being set, C be finite set, A being Element of Fin PFuncs (V, C) holds Involved A c= V; theorem :: HEYTING2:7 for V being set, C being finite set, A being Element of Fin PFuncs (V, C) st A = {} holds Involved A = {}; registration let V be set, C being finite set, A being Element of Fin PFuncs (V, C); cluster Involved A -> finite; end; theorem :: HEYTING2:8 for C being finite set, A being Element of Fin PFuncs ({}, C) holds Involved A = {}; definition let V be set, C be finite set; let A be Element of Fin PFuncs (V, C); func -A -> Element of Fin PFuncs (V, C) equals :: HEYTING2:def 2 { f where f is Element of PFuncs (Involved A, C) : for g be Element of PFuncs (V, C) st g in A holds not f tolerates g }; end; theorem :: HEYTING2:9 A ^ -A = {}; theorem :: HEYTING2:10 A = {} implies -A = { {} }; theorem :: HEYTING2:11 A = { {} } implies -A = {}; theorem :: HEYTING2:12 for V being set, C being finite set for A being Element of SubstitutionSet (V, C) holds mi (A ^ -A) = Bottom SubstLatt (V,C); theorem :: HEYTING2:13 for V being non empty set, C being finite non empty set for A being Element of SubstitutionSet (V, C) st A = {} holds mi -A = Top SubstLatt (V,C) ; theorem :: HEYTING2:14 for V being set, C being finite set for A being Element of SubstitutionSet (V, C), a being Element of PFuncs (V, C), B being Element of SubstitutionSet (V, C) st B = { a } holds A ^ B = {} implies ex b being finite set st b in -A & b c= a; definition let V be set, C be finite set; let A, B be Element of Fin PFuncs (V, C); func A =>> B -> Element of Fin PFuncs (V, C) equals :: HEYTING2:def 3 PFuncs (V, C) /\ { union {f.i \ i where i is Element of PFuncs (V, C) : i in A} where f is Element of PFuncs (A, B) : dom f = A }; end; theorem :: HEYTING2:15 for A, B being Element of Fin PFuncs (V, C), s being set st s in A =>> B holds ex f being PartFunc of A, B st s = union {f.i \ i where i is Element of PFuncs (V, C) : i in A} & dom f = A; theorem :: HEYTING2:16 for V being set, C being finite set, A being Element of Fin PFuncs (V, C ) st A = {} holds A =>> A = {{}}; reserve u, v for Element of SubstLatt (V, C); reserve s, t, a, b for Element of PFuncs (V,C); reserve K, L for Element of SubstitutionSet (V, C); theorem :: HEYTING2:17 for X being set st X c= u holds X is Element of SubstLatt (V, C); begin :: Lattice of substitutions is implicative definition let V, C; func pseudo_compl (V, C) -> UnOp of the carrier of SubstLatt (V, C) means :: HEYTING2:def 4 for u9 being Element of SubstitutionSet (V, C) st u9 = u holds it.u = mi( -u9); func StrongImpl(V, C) -> BinOp of the carrier of SubstLatt (V, C) means :: HEYTING2:def 5 for u9, v9 being Element of SubstitutionSet (V, C) st u9 = u & v9 = v holds it.(u,v) = mi (u9 =>> v9); let u; func SUB u -> Element of Fin the carrier of SubstLatt (V, C) equals :: HEYTING2:def 6 bool u; func diff(u) -> UnOp of the carrier of SubstLatt (V, C) means :: HEYTING2:def 7 it.v = u \ v; end; definition let V, C; func Atom(V, C) -> Function of PFuncs (V, C), the carrier of SubstLatt (V, C ) means :: HEYTING2:def 8 for a being Element of PFuncs (V,C) holds it.a = mi {.a.}; end; theorem :: HEYTING2:18 FinJoin (K, Atom(V, C)) = FinUnion(K, singleton PFuncs (V, C)); theorem :: HEYTING2:19 for u being Element of SubstitutionSet (V, C) holds u = FinJoin( u, Atom (V, C)); theorem :: HEYTING2:20 (diff u).v [= u; theorem :: HEYTING2:21 for a being Element of PFuncs (V, C) st a is finite for c being set st c in Atom(V, C).a holds c = a; theorem :: HEYTING2:22 for a being Element of PFuncs (V, C) st K = {a} & L = u & L ^ K = {} holds Atom(V, C).a [= pseudo_compl(V, C).u; theorem :: HEYTING2:23 for a being finite Element of PFuncs (V,C) holds a in Atom(V, C) .a; theorem :: HEYTING2:24 for u, v being Element of SubstitutionSet (V, C) holds ((for c being set st c in u ex b being set st b in v & b c= c \/ a) implies ex b being set st b in u =>> v & b c= a ); theorem :: HEYTING2:25 for a being finite Element of PFuncs (V,C) st (for b being Element of PFuncs (V, C) st b in u holds b tolerates a ) & u "/\" Atom(V, C).a [= v holds Atom(V, C).a [= StrongImpl(V, C).(u, v); theorem :: HEYTING2:26 u "/\" pseudo_compl(V, C).u = Bottom SubstLatt (V, C); theorem :: HEYTING2:27 u "/\" StrongImpl(V, C).(u, v) [= v; registration let V, C; cluster SubstLatt (V, C) -> implicative; end; theorem :: HEYTING2:28 u => v = FinJoin(SUB u, (the L_meet of SubstLatt (V, C)).:( pseudo_compl(V, C), StrongImpl(V, C)[:](diff u, v)));