Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### Lattice of Substitutions is a Heyting Algebra

**by****Adam Grabowski**- Received December 31, 1998
- MML identifier: HEYTING2

- [ Mizar article, MML identifier index ]

environ vocabulary SUBSTLAT, FUNCT_1, RELAT_1, PARTFUN1, FRAENKEL, BOOLE, FINSET_1, FINSUB_1, FINSEQ_1, NORMFORM, TARSKI, ARYTM_1, LATTICES, FUNCT_2, HEYTING1, BINOP_1, FDIFF_1, LATTICE2, SETWISEO, FUNCOP_1, FILTER_0, ZF_LANG, HEYTING2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, FUNCOP_1, BINOP_1, FINSET_1, FINSUB_1, FUNCT_2, FRAENKEL, PARTFUN1, LATTICES, STRUCT_0, SUBSTLAT, SETWISEO, HEYTING1, LATTICE2, FILTER_0; constructors SETWISEO, GRCAT_1, SUBSTLAT, LATTICE2, FILTER_0, HEYTING1, MEMBERED; clusters RELSET_1, FINSET_1, FINSUB_1, SETWISEO, SUBSTLAT, MONOID_1, STRUCT_0, RFINSEQ, SUBSET_1, RELAT_1, FUNCT_1, WELLFND1, FRAENKEL, FINSEQ_1; requirements SUBSET, BOOLE; begin :: Preliminaries reserve V, C, x, a, b for set; reserve A, B for Element of SubstitutionSet (V, C); definition let a, b be set; cluster {[a, b]} -> Function-like Relation-like; end; theorem :: HEYTING2:1 for V, C being non empty set ex f be Element of PFuncs (V, C) st f <> {}; theorem :: HEYTING2:2 for a, b being set st b in SubstitutionSet (V, C) & a in b holds a is finite Function; theorem :: HEYTING2:3 for f being Element of PFuncs (V, C), g being set st g c= f holds g in PFuncs (V, C); theorem :: HEYTING2:4 PFuncs(V,C) c= bool [:V,C:]; theorem :: HEYTING2:5 V is finite & C is finite implies PFuncs (V, C) is finite; definition cluster functional finite non empty set; end; begin :: Some properties of sets of substitutions theorem :: HEYTING2:6 for a being finite Element of PFuncs (V, C) holds {a} in SubstitutionSet (V, C); theorem :: HEYTING2:7 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:8 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:9 (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 means :: HEYTING2:def 1 x in it iff ex f being finite Function st f in A & x in dom f; end; reserve C for finite set; theorem :: HEYTING2:10 for V being set, C be finite set, A being Element of Fin PFuncs (V, C) holds Involved A c= V; theorem :: HEYTING2:11 for V being set, C being finite set, A being Element of Fin PFuncs (V, C) st A = {} holds Involved A = {}; theorem :: HEYTING2:12 for V being set, C being finite set, A being Element of Fin PFuncs (V, C) holds Involved A is finite; theorem :: HEYTING2:13 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:14 A ^ -A = {}; theorem :: HEYTING2:15 A = {} implies -A = { {} }; theorem :: HEYTING2:16 A = { {} } implies -A = {}; theorem :: HEYTING2:17 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:18 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:19 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:20 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:21 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:22 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 u' being Element of SubstitutionSet (V, C) st u' = u holds it.u = mi(-u'); func StrongImpl(V, C) -> BinOp of the carrier of SubstLatt (V, C) means :: HEYTING2:def 5 for u', v' being Element of SubstitutionSet (V, C) st u' = u & v' = v holds it.(u,v) = mi (u' =>> v'); 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:23 FinJoin (K, Atom(V, C)) = FinUnion(K, singleton PFuncs (V, C)); theorem :: HEYTING2:24 for u being Element of SubstitutionSet (V, C) holds u = FinJoin(u, Atom (V, C)); theorem :: HEYTING2:25 (diff u).v [= u; theorem :: HEYTING2:26 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:27 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:28 for a being finite Element of PFuncs (V,C) holds a in Atom(V, C).a; theorem :: HEYTING2:29 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:30 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:31 u "/\" pseudo_compl(V, C).u = Bottom SubstLatt (V, C); theorem :: HEYTING2:32 u "/\" StrongImpl(V, C).(u, v) [= v; definition let V, C; cluster SubstLatt (V, C) -> implicative; end; theorem :: HEYTING2:33 u => v = FinJoin(SUB u, (the L_meet of SubstLatt (V, C)).:(pseudo_compl(V, C), StrongImpl(V, C)[:](diff u, v)));

Back to top