:: On the Closure Operator and the Closure System of Many Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Received February 7, 1996
:: Copyright (c) 1996-2016 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 PBOOLE, FUNCT_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ZFMISC_1,
FUNCT_2, CARD_3, FINSET_1, COMPLEX1, SETFAM_1, FUNCT_4, MSSUBFAM,
FUNCOP_1, RELAT_2, MSAFREE2, BINOP_1, YELLOW_6, STRUCT_0, MSUALG_1,
PRE_TOPC, CLOSURE2, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, SETFAM_1, RELAT_1,
FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, FUNCT_4, PBOOLE, CARD_3,
MSUALG_1, MBOOLEAN, MSSUBFAM;
constructors SETFAM_1, FUNCT_4, MSSUBFAM, MSUALG_1, CARD_3, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1,
FINSET_1, PBOOLE, MSUALG_1;
requirements SUBSET, BOOLE;
begin :: Preliminaries
reserve i, x, I for set,
A, B, M for ManySortedSet of I,
f, f1 for Function;
notation
let I, A, B;
synonym A in' B for A in B;
end;
notation
let I, A, B;
synonym A c=' B for A c= B;
end;
theorem :: CLOSURE2:1
for M being non empty set for X, Y being Element of M st X c= Y holds
(id M).X c= (id M).Y;
theorem :: CLOSURE2:2
for I being non empty set for A being ManySortedSet of I for B
being ManySortedSubset of A holds rng B c= union rng bool A;
begin :: Set of Many Sorted Subsets of a Many Sorted Set
definition
let I, M;
func Bool M -> set means
:: CLOSURE2:def 1
for x being object holds x in it iff x is ManySortedSubset of M;
end;
registration
let I, M;
cluster Bool M -> non empty functional with_common_domain;
end;
definition
let I, M;
mode SubsetFamily of M is Subset of Bool M;
end;
definition
let I, M;
redefine func Bool M -> SubsetFamily of M;
end;
registration
let I, M;
cluster non empty functional with_common_domain for SubsetFamily of M;
end;
registration
let I, M;
cluster empty finite for SubsetFamily of M;
end;
reserve SF, SG for SubsetFamily of M;
definition
let I, M;
let S be non empty SubsetFamily of M;
redefine mode Element of S -> ManySortedSubset of M;
end;
theorem :: CLOSURE2:3 :: MSSUBFAM:34
SF \/ SG is SubsetFamily of M;
theorem :: CLOSURE2:4 :: MSSUBFAM:35
SF /\ SG is SubsetFamily of M;
theorem :: CLOSURE2:5 :: MSSUBFAM:36
SF \ x is SubsetFamily of M;
theorem :: CLOSURE2:6 :: MSSUBFAM:37
SF \+\ SG is SubsetFamily of M;
theorem :: CLOSURE2:7 :: MSSUBFAM:38
A c= M implies {A} is SubsetFamily of M;
theorem :: CLOSURE2:8 :: MSSUBFAM:39
A c= M & B c= M implies {A,B} is SubsetFamily of M;
reserve E, T for Element of Bool M;
theorem :: CLOSURE2:9
E (/\) T in Bool M;
theorem :: CLOSURE2:10
E (\/) T in Bool M;
theorem :: CLOSURE2:11
E (\) A in Bool M;
theorem :: CLOSURE2:12
E (\+\) T in Bool M;
begin :: Many Sorted Operator corresponding
:: to the Operator on Many Sorted Subsets
definition
let S be functional set;
func |. S .| -> Function means
:: CLOSURE2:def 2
ex A being non empty functional set st
A = S & dom it = meet the set of all dom x where x is Element of A &
for i st i in dom it holds it.i = the set of all
x.i where x is Element of A if S <> {} otherwise it = {};
end;
theorem :: CLOSURE2:13
for SF being non empty SubsetFamily of M holds dom |.SF.| = I;
registration
let S be empty functional set;
cluster |. S .| -> empty;
end;
definition
let I, M;
let S be SubsetFamily of M;
func |: S :| -> ManySortedSet of I equals
:: CLOSURE2:def 3
|. S .| if S <> {}
otherwise EmptyMS I;
end;
registration
let I, M;
let S be empty SubsetFamily of M;
cluster |: S :| -> empty-yielding;
end;
theorem :: CLOSURE2:14
SF is non empty implies for i st i in I holds |:SF:|.i = { x.i
where x is Element of Bool M : x in SF };
registration
let I, M;
let SF be non empty SubsetFamily of M;
cluster |: SF :| -> non-empty;
end;
theorem :: CLOSURE2:15
dom |.{f}.| = dom f;
theorem :: CLOSURE2:16
dom |.{f,f1}.| = dom f /\ dom f1;
theorem :: CLOSURE2:17
i in dom f implies |.{f}.|.i = {f.i};
theorem :: CLOSURE2:18
i in I & SF = {f} implies |:SF:|.i = {f.i};
theorem :: CLOSURE2:19
i in dom |.{f,f1}.| implies |.{f,f1}.|.i = { f.i, f1.i };
theorem :: CLOSURE2:20
i in I & SF = {f,f1} implies |:SF:|.i = { f.i, f1.i };
definition
let I, M, SF;
redefine func |:SF:| -> MSSubsetFamily of M;
end;
theorem :: CLOSURE2:21
A in SF implies A in' |:SF:|;
theorem :: CLOSURE2:22
SF = {A,B} implies union |:SF:| = A (\/) B;
theorem :: CLOSURE2:23 :: SETFAM_1:12
SF = {E,T} implies meet |:SF:| = E (/\) T;
theorem :: CLOSURE2:24 :: MSSUBFAM:4
for Z being ManySortedSubset of M st for Z1 being ManySortedSet
of I st Z1 in SF holds Z c=' Z1 holds Z c=' meet |:SF:|;
theorem :: CLOSURE2:25
|: Bool M :| = bool M;
definition
let I, M;
let IT be SubsetFamily of M;
attr IT is additive means
:: CLOSURE2:def 4
for A, B st A in IT & B in IT holds A (\/) B in IT;
attr IT is absolutely-additive means
:: CLOSURE2:def 5
for F be SubsetFamily of M st F c= IT holds union |:F:| in IT;
attr IT is multiplicative means
:: CLOSURE2:def 6
for A, B st A in IT & B in IT holds A (/\) B in IT;
attr IT is absolutely-multiplicative means
:: CLOSURE2:def 7
for F be SubsetFamily of M st F c= IT holds meet |:F:| in IT;
attr IT is properly-upper-bound means
:: CLOSURE2:def 8
M in IT;
attr IT is properly-lower-bound means
:: CLOSURE2:def 9
EmptyMS I in IT;
end;
registration
let I, M;
cluster non empty functional with_common_domain additive absolutely-additive
multiplicative absolutely-multiplicative properly-upper-bound
properly-lower-bound for SubsetFamily of M;
end;
definition
let I, M;
redefine func Bool M -> additive absolutely-additive multiplicative
absolutely-multiplicative properly-upper-bound properly-lower-bound
SubsetFamily of M;
end;
registration
let I, M;
cluster absolutely-additive -> additive for SubsetFamily of M;
end;
registration
let I, M;
cluster absolutely-multiplicative -> multiplicative for SubsetFamily of M;
end;
registration
let I, M;
cluster absolutely-multiplicative -> properly-upper-bound for
SubsetFamily of M;
end;
registration
let I, M;
cluster properly-upper-bound -> non empty for SubsetFamily of M;
end;
registration
let I, M;
cluster absolutely-additive -> properly-lower-bound for SubsetFamily of M;
end;
registration
let I, M;
cluster properly-lower-bound -> non empty for SubsetFamily of M;
end;
begin :: Properties of Closure Operators
definition
let I, M;
mode SetOp of M is Function of Bool M, Bool M;
end;
definition
let I, M;
let f be SetOp of M;
let x be Element of Bool M;
redefine func f.x -> Element of Bool M;
end;
definition
let I, M;
let IT be SetOp of M;
attr IT is reflexive means
:: CLOSURE2:def 10
for x being Element of Bool M holds x c=' IT.x;
attr IT is monotonic means
:: CLOSURE2:def 11
for x, y being Element of Bool M st x c=' y holds IT.x c=' IT.y;
attr IT is idempotent means
:: CLOSURE2:def 12
for x being Element of Bool M holds IT.x = IT.(IT.x);
attr IT is topological means
:: CLOSURE2:def 13
for x, y being Element of Bool M holds IT.(x (\/) y) = (IT.x) (\/) (IT.y);
end;
registration
let I, M;
cluster reflexive monotonic idempotent topological for SetOp of M;
end;
theorem :: CLOSURE2:26 :: CLOSURE:11
id (Bool A) is reflexive SetOp of A;
theorem :: CLOSURE2:27 :: CLOSURE:12
id (Bool A) is monotonic SetOp of A;
theorem :: CLOSURE2:28 :: CLOSURE:13
id (Bool A) is idempotent SetOp of A;
theorem :: CLOSURE2:29 :: CLOSURE:15
id (Bool A) is topological SetOp of A;
reserve g, h for SetOp of M;
theorem :: CLOSURE2:30 :: CLOSURE:16
E = M & g is reflexive implies E = g.E;
theorem :: CLOSURE2:31 :: CLOSURE:17
(g is reflexive & for X being Element of Bool M holds g.X c= X)
implies g is idempotent;
theorem :: CLOSURE2:32 :: CLOSURE:18
for A being Element of Bool M st A = E (/\) T holds g is monotonic
implies g.A c= g.E (/\) g.T;
registration
let I, M;
cluster topological -> monotonic for SetOp of M;
end;
theorem :: CLOSURE2:33 :: CLOSURE:19
for A being Element of Bool M st A = E (\) T holds g is topological
implies g.E (\) g.T c= g.A;
definition
let I, M, h, g;
redefine func g * h -> SetOp of M;
end;
theorem :: CLOSURE2:34 :: CLOSURE:21
g is reflexive & h is reflexive implies g * h is reflexive;
theorem :: CLOSURE2:35 :: CLOSURE:22
g is monotonic & h is monotonic implies g * h is monotonic;
theorem :: CLOSURE2:36 :: CLOSURE:23
g is idempotent & h is idempotent & g*h = h*g implies g * h is idempotent;
theorem :: CLOSURE2:37 :: CLOSURE:25
g is topological & h is topological implies g * h is topological;
begin :: On the Closure Operator and the Closure System
reserve S for 1-sorted;
definition
let S;
struct(many-sorted over S) ClosureStr over S (# Sorts -> ManySortedSet of
the carrier of S, Family -> SubsetFamily of the Sorts #);
end;
reserve MS for many-sorted over S;
definition
let S;
let IT be ClosureStr over S;
attr IT is additive means
:: CLOSURE2:def 14
the Family of IT is additive;
attr IT is absolutely-additive means
:: CLOSURE2:def 15
the Family of IT is absolutely-additive;
attr IT is multiplicative means
:: CLOSURE2:def 16
the Family of IT is multiplicative;
attr IT is absolutely-multiplicative means
:: CLOSURE2:def 17
the Family of IT is absolutely-multiplicative;
attr IT is properly-upper-bound means
:: CLOSURE2:def 18
the Family of IT is properly-upper-bound;
attr IT is properly-lower-bound means
:: CLOSURE2:def 19
the Family of IT is properly-lower-bound;
end;
definition
let S, MS;
func Full MS -> ClosureStr over S equals
:: CLOSURE2:def 20
ClosureStr (#the Sorts of MS, Bool the Sorts of MS#);
end;
registration
let S, MS;
cluster Full MS -> strict additive absolutely-additive multiplicative
absolutely-multiplicative properly-upper-bound properly-lower-bound;
end;
registration
let S;
let MS be non-empty many-sorted over S;
cluster Full MS -> non-empty;
end;
registration
let S;
cluster strict non-empty additive absolutely-additive multiplicative
absolutely-multiplicative properly-upper-bound properly-lower-bound for
ClosureStr
over S;
end;
registration
let S;
let CS be additive ClosureStr over S;
cluster the Family of CS -> additive;
end;
registration
let S;
let CS be absolutely-additive ClosureStr over S;
cluster the Family of CS -> absolutely-additive;
end;
registration
let S;
let CS be multiplicative ClosureStr over S;
cluster the Family of CS -> multiplicative;
end;
registration
let S;
let CS be absolutely-multiplicative ClosureStr over S;
cluster the Family of CS -> absolutely-multiplicative;
end;
registration
let S;
let CS be properly-upper-bound ClosureStr over S;
cluster the Family of CS -> properly-upper-bound;
end;
registration
let S;
let CS be properly-lower-bound ClosureStr over S;
cluster the Family of CS -> properly-lower-bound;
end;
registration
let S;
let M be non-empty ManySortedSet of the carrier of S;
let F be SubsetFamily of M;
cluster ClosureStr (#M, F#) -> non-empty;
end;
registration
let S, MS;
let F be additive SubsetFamily of the Sorts of MS;
cluster ClosureStr (#the Sorts of MS, F#) -> additive;
end;
registration
let S, MS;
let F be absolutely-additive SubsetFamily of the Sorts of MS;
cluster ClosureStr (#the Sorts of MS, F#) -> absolutely-additive;
end;
registration
let S, MS;
let F be multiplicative SubsetFamily of the Sorts of MS;
cluster ClosureStr (#the Sorts of MS, F#) -> multiplicative;
end;
registration
let S, MS;
let F be absolutely-multiplicative SubsetFamily of the Sorts of MS;
cluster ClosureStr (#the Sorts of MS, F#) -> absolutely-multiplicative;
end;
registration
let S, MS;
let F be properly-upper-bound SubsetFamily of the Sorts of MS;
cluster ClosureStr (#the Sorts of MS, F#) -> properly-upper-bound;
end;
registration
let S, MS;
let F be properly-lower-bound SubsetFamily of the Sorts of MS;
cluster ClosureStr (#the Sorts of MS, F#) -> properly-lower-bound;
end;
registration
let S;
cluster absolutely-additive -> additive for ClosureStr over S;
end;
registration
let S;
cluster absolutely-multiplicative -> multiplicative for ClosureStr over S;
end;
registration
let S;
cluster absolutely-multiplicative -> properly-upper-bound for
ClosureStr over S;
end;
registration
let S;
cluster absolutely-additive -> properly-lower-bound for ClosureStr over S;
end;
definition
let S;
mode ClosureSystem of S is absolutely-multiplicative ClosureStr over S;
end;
definition
let I, M;
mode ClosureOperator of M is reflexive monotonic idempotent SetOp of M;
end;
definition
let S;
let A be ManySortedSet of the carrier of S;
let g be ClosureOperator of A;
func ClOp->ClSys g -> strict ClosureStr over S means
:: CLOSURE2:def 21
the Sorts of it = A &
the Family of it = { x where x is Element of Bool A : g.x = x };
end;
registration
let S;
let A be ManySortedSet of the carrier of S;
let g be ClosureOperator of A;
cluster ClOp->ClSys g -> absolutely-multiplicative;
end;
definition
let S;
let A be ClosureSystem of S;
let C be ManySortedSubset of the Sorts of A;
func Cl C -> Element of Bool the Sorts of A means
:: CLOSURE2:def 22
ex F being
SubsetFamily of the Sorts of A st it = meet |:F:| & F = { X where X is Element
of Bool the Sorts of A : C c=' X & X in the Family of A };
end;
theorem :: CLOSURE2:38
for D being ClosureSystem of S for a being Element of Bool the
Sorts of D for f being SetOp of the Sorts of D st a in the Family of D & for x
being Element of Bool the Sorts of D holds f.x = Cl x holds f.a = a;
theorem :: CLOSURE2:39
for D being ClosureSystem of S for a being Element of Bool the Sorts
of D for f being SetOp of the Sorts of D st f.a = a & for x being Element of
Bool the Sorts of D holds f.x = Cl x holds a in the Family of D;
theorem :: CLOSURE2:40
for D being ClosureSystem of S for f being SetOp of the Sorts of
D st for x being Element of Bool the Sorts of D holds f.x = Cl x holds f is
reflexive monotonic idempotent;
definition
let S;
let D be ClosureSystem of S;
func ClSys->ClOp D -> ClosureOperator of the Sorts of D means
:: CLOSURE2:def 23
for x being Element of Bool the Sorts of D holds it.x = Cl x;
end;
theorem :: CLOSURE2:41
for A being ManySortedSet of the carrier of S for f being
ClosureOperator of A holds ClSys->ClOp (ClOp->ClSys f) = f;
theorem :: CLOSURE2:42
for D being ClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = the
ClosureStr of D;