:: 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)));