:: On the Many Sorted Closure Operator and the Many Sorted Closure
:: System
:: 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, RELAT_1, TARSKI, FUNCT_4, FUNCOP_1, XBOOLE_0,
SUBSET_1, FINSEQ_4, PARTFUN1, FUNCT_6, MEMBER_1, MSUALG_3, FINSET_1,
ZFMISC_1, RELAT_2, MSAFREE2, BINOP_1, YELLOW_6, STRUCT_0, MSUALG_1,
CLOSURE2, MSSUBFAM, SETFAM_1, CLOSURE1, SETLIM_2;
notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, SETFAM_1, RELAT_1, FUNCT_1,
FINSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, PBOOLE, FUNCT_6,
MSUALG_1, MSUALG_3, PRALG_1, MSSUBFAM;
constructors SETFAM_1, PZFMISC1, MSSUBFAM, PRALG_1, MSUALG_3, RELSET_1,
FUNCT_4, FUNCT_6;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCOP_1, FINSET_1, PBOOLE,
MSSUBFAM, MSUALG_1, RELAT_1, PRALG_1;
requirements SUBSET, BOOLE;
begin :: Preliminaries
reserve i, x, I for set,
A, M for ManySortedSet of I,
f for Function,
F for ManySortedFunction of I;
scheme :: CLOSURE1:sch 1
MSSUBSET { I() -> set, A() -> non-empty ManySortedSet of I(), B() ->
ManySortedSet of I(), P[set] } : (for X being ManySortedSet of I() holds X in A
() iff X in B() & P[X]) implies A() c= B();
theorem :: CLOSURE1:1
for X being non empty set for x, y being set st x c= y holds { t
where t is Element of X : y c= t } c= { z where z is Element of X : x c= z };
theorem :: CLOSURE1:2
(ex A st A in M) implies M is non-empty;
registration
let I, F, A;
cluster F..A -> total for I-defined Function;
end;
definition
let I;
let A, B be non-empty ManySortedSet of I;
let F be ManySortedFunction of A, B;
let X be Element of A;
redefine func F..X -> Element of B;
end;
theorem :: CLOSURE1:3
for A, X being ManySortedSet of I for B being non-empty ManySortedSet
of I for F being ManySortedFunction of A, B st X in A holds F..X in B;
theorem :: CLOSURE1:4
for F, G being ManySortedFunction of I for A being ManySortedSet
of I st A in doms G holds F..(G..A) = (F ** G)..A;
theorem :: CLOSURE1:5
F is "1-1" implies for A, B being ManySortedSet of I st A in doms F &
B in doms F & F..A = F..B holds A = B;
theorem :: CLOSURE1:6
doms F is non-empty & (for A, B being ManySortedSet of I st A in doms
F & B in doms F & F..A = F..B holds A = B) implies F is "1-1";
theorem :: CLOSURE1:7 :: FUNCT_2:18
for A, B being non-empty ManySortedSet of I for F, G being
ManySortedFunction of A, B st for M st M in A holds F..M = G..M holds F = G;
registration
let I, M;
cluster empty-yielding finite-yielding for Element of bool M;
end;
begin :: Properties of Many Sorted Closure Operators
definition
let I, M;
mode MSSetOp of M is ManySortedFunction of bool M, bool M;
end;
definition
let I, M;
let O be MSSetOp of M;
let X be Element of bool M;
redefine func O..X -> Element of bool M;
end;
definition
let I, M;
let IT be MSSetOp of M;
attr IT is reflexive means
:: CLOSURE1:def 1
for X being Element of bool M holds X c= IT..X;
attr IT is monotonic means
:: CLOSURE1:def 2
for X, Y being Element of bool M st X c= Y holds IT..X c= IT..Y;
attr IT is idempotent means
:: CLOSURE1:def 3
for X being Element of bool M holds IT..X = IT..(IT..X);
attr IT is topological means
:: CLOSURE1:def 4
for X, Y being Element of bool M holds IT..(X (\/) Y) = (IT..X) (\/) (IT..Y);
end;
theorem :: CLOSURE1:8
for M being non-empty ManySortedSet of I for X being Element of M
holds X = (id M)..X;
theorem :: CLOSURE1:9
for M being non-empty ManySortedSet of I for X, Y being Element
of M st X c= Y holds (id M)..X c= (id M)..Y;
theorem :: CLOSURE1:10
for M being non-empty ManySortedSet of I for X, Y being Element
of M st X (\/) Y is Element of M
holds (id M)..(X (\/) Y) = ((id M)..X) (\/) ((id M) ..Y);
theorem :: CLOSURE1:11
for X being Element of bool M for i, x being set st i in I & x in ((id
(bool M))..X).i ex Y being finite-yielding Element of bool M st Y c= X & x in (
(id (bool M))..Y).i;
registration
let I, M;
cluster reflexive monotonic idempotent topological for MSSetOp of M;
end;
theorem :: CLOSURE1:12
id (bool A) is reflexive MSSetOp of A;
theorem :: CLOSURE1:13
id (bool A) is monotonic MSSetOp of A;
theorem :: CLOSURE1:14
id (bool A) is idempotent MSSetOp of A;
theorem :: CLOSURE1:15
id (bool A) is topological MSSetOp of A;
reserve P, R for MSSetOp of M,
E, T for Element of bool M;
theorem :: CLOSURE1:16
E = M & P is reflexive implies E = P..E;
theorem :: CLOSURE1:17
(P is reflexive & for X being Element of bool M holds P..X c= X)
implies P is idempotent;
theorem :: CLOSURE1:18
P is monotonic implies P..(E (/\) T) c= P..E (/\) P..T;
registration
let I, M;
cluster topological -> monotonic for MSSetOp of M;
end;
theorem :: CLOSURE1:19
P is topological implies P..E (\) P..T c= P..(E (\) T);
definition
let I, M, R, P;
redefine func P ** R -> MSSetOp of M;
end;
theorem :: CLOSURE1:20
P is reflexive & R is reflexive implies P ** R is reflexive;
theorem :: CLOSURE1:21
P is monotonic & R is monotonic implies P ** R is monotonic;
theorem :: CLOSURE1:22
P is idempotent & R is idempotent & P**R = R**P implies P ** R is idempotent;
theorem :: CLOSURE1:23
P is topological & R is topological implies P ** R is topological;
theorem :: CLOSURE1:24
P is reflexive & i in I & f = P.i implies for x being Element of
bool (M.i) holds x c= f.x;
theorem :: CLOSURE1:25
P is monotonic & i in I & f = P.i implies for x, y being Element
of bool (M.i) st x c= y holds f.x c= f.y;
theorem :: CLOSURE1:26
P is idempotent & i in I & f = P.i implies for x being Element
of bool (M.i) holds f.x = f.(f.x);
theorem :: CLOSURE1:27
P is topological & i in I & f = P.i implies for x, y being Element of
bool (M.i) holds f.(x \/ y) = (f.x) \/ (f.y);
begin :: On the Many Sorted Closure Operator
:: and the Many Sorted Closure System
reserve S for 1-sorted;
definition
let S;
struct(many-sorted over S) MSClosureStr over S (# Sorts -> ManySortedSet of
the carrier of S, Family -> MSSubsetFamily of the Sorts #);
end;
reserve MS for many-sorted over S;
definition
let S;
let IT be MSClosureStr over S;
attr IT is additive means
:: CLOSURE1:def 5
the Family of IT is additive;
attr IT is absolutely-additive means
:: CLOSURE1:def 6
the Family of IT is absolutely-additive;
attr IT is multiplicative means
:: CLOSURE1:def 7
the Family of IT is multiplicative;
attr IT is absolutely-multiplicative means
:: CLOSURE1:def 8
the Family of IT is absolutely-multiplicative;
attr IT is properly-upper-bound means
:: CLOSURE1:def 9
the Family of IT is properly-upper-bound;
attr IT is properly-lower-bound means
:: CLOSURE1:def 10
the Family of IT is properly-lower-bound;
end;
definition
let S, MS;
func MSFull MS -> MSClosureStr over S equals
:: CLOSURE1:def 11
MSClosureStr (#the Sorts of MS,
bool the Sorts of MS#);
end;
registration
let S, MS;
cluster MSFull 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 MSFull MS -> non-empty;
end;
registration
let S;
cluster strict non-empty additive absolutely-additive multiplicative
absolutely-multiplicative properly-upper-bound properly-lower-bound
for MSClosureStr over S;
end;
registration
let S;
let CS be additive MSClosureStr over S;
cluster the Family of CS -> additive;
end;
registration
let S;
let CS be absolutely-additive MSClosureStr over S;
cluster the Family of CS -> absolutely-additive;
end;
registration
let S;
let CS be multiplicative MSClosureStr over S;
cluster the Family of CS -> multiplicative;
end;
registration
let S;
let CS be absolutely-multiplicative MSClosureStr over S;
cluster the Family of CS -> absolutely-multiplicative;
end;
registration
let S;
let CS be properly-upper-bound MSClosureStr over S;
cluster the Family of CS -> properly-upper-bound;
end;
registration
let S;
let CS be properly-lower-bound MSClosureStr 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 MSSubsetFamily of M;
cluster MSClosureStr (#M, F#) -> non-empty;
end;
registration
let S, MS;
let F be additive MSSubsetFamily of the Sorts of MS;
cluster MSClosureStr (#the Sorts of MS, F#) -> additive;
end;
registration
let S, MS;
let F be absolutely-additive MSSubsetFamily of the Sorts of MS;
cluster MSClosureStr (#the Sorts of MS, F#) -> absolutely-additive;
end;
registration
let S, MS;
let F be multiplicative MSSubsetFamily of the Sorts of MS;
cluster MSClosureStr (#the Sorts of MS, F#) -> multiplicative;
end;
registration
let S, MS;
let F be absolutely-multiplicative MSSubsetFamily of the Sorts of MS;
cluster MSClosureStr (#the Sorts of MS, F#) -> absolutely-multiplicative;
end;
registration
let S, MS;
let F be properly-upper-bound MSSubsetFamily of the Sorts of MS;
cluster MSClosureStr (#the Sorts of MS, F#) -> properly-upper-bound;
end;
registration
let S, MS;
let F be properly-lower-bound MSSubsetFamily of the Sorts of MS;
cluster MSClosureStr (#the Sorts of MS, F#) -> properly-lower-bound;
end;
registration
let S;
cluster absolutely-additive -> additive for MSClosureStr over S;
end;
registration
let S;
cluster absolutely-multiplicative -> multiplicative for MSClosureStr over S;
end;
registration
let S;
cluster absolutely-multiplicative -> properly-upper-bound for
MSClosureStr over
S;
end;
registration
let S;
cluster absolutely-additive -> properly-lower-bound for MSClosureStr over S;
end;
definition
let S;
mode MSClosureSystem of S is absolutely-multiplicative MSClosureStr over S;
end;
definition
let I, M;
mode MSClosureOperator of M is reflexive monotonic idempotent MSSetOp of M;
end;
definition
let I, M;
let F be ManySortedFunction of M, M;
func MSFixPoints F -> ManySortedSubset of M means
:: CLOSURE1:def 12
for i being object st i in I
holds x in it.i iff ex f being Function st f = F.i & x in dom f & f.x = x;
end;
registration
let I;
let M be empty-yielding ManySortedSet of I;
let F be ManySortedFunction of M, M;
cluster MSFixPoints F -> empty-yielding;
end;
theorem :: CLOSURE1:28
for F being ManySortedFunction of M, M holds A in M & F..A = A
iff A in MSFixPoints F;
theorem :: CLOSURE1:29
MSFixPoints id A = A;
theorem :: CLOSURE1:30
for A being ManySortedSet of the carrier of S for J being
reflexive monotonic MSSetOp of A for D being MSSubsetFamily of A st D =
MSFixPoints J holds MSClosureStr (#A, D#) is MSClosureSystem of S;
theorem :: CLOSURE1:31
for D being properly-upper-bound MSSubsetFamily of M for X being
Element of bool M ex SF being non-empty MSSubsetFamily of M st for Y being
ManySortedSet of I holds Y in SF iff Y in D & X c= Y;
theorem :: CLOSURE1:32
for D being properly-upper-bound MSSubsetFamily of M for X being
Element of bool M for SF being non-empty MSSubsetFamily of M st (for Y being
ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds for i being set, Di
being non empty set st i in I & Di = D.i holds SF.i = { z where z is Element of
Di: X.i c= z };
theorem :: CLOSURE1:33
for D being properly-upper-bound MSSubsetFamily of M ex J being
MSSetOp of M st for X being Element of bool M for SF being non-empty
MSSubsetFamily of M st (for Y being ManySortedSet of I holds Y in SF iff Y in D
& X c= Y) holds J..X = meet SF;
theorem :: CLOSURE1:34
for D being properly-upper-bound MSSubsetFamily of M for A being
Element of bool M for J being MSSetOp of M st A in D & for X being Element of
bool M for SF being non-empty MSSubsetFamily of M st (for Y being ManySortedSet
of I holds Y in SF iff Y in D & X c= Y) holds J..X = meet SF holds J..A = A;
theorem :: CLOSURE1:35
for D being absolutely-multiplicative MSSubsetFamily of M for A being
Element of bool M for J being MSSetOp of M st J..A = A & for X being Element of
bool M for SF being non-empty MSSubsetFamily of M st (for Y being ManySortedSet
of I holds Y in SF iff Y in D & X c= Y) holds J..X = meet SF holds A in D;
theorem :: CLOSURE1:36
for D being properly-upper-bound MSSubsetFamily of M for J being
MSSetOp of M st for X being Element of bool M for SF being non-empty
MSSubsetFamily of M st (for Y being ManySortedSet of I holds Y in SF iff Y in D
& X c= Y) holds J..X = meet SF holds J is reflexive monotonic;
theorem :: CLOSURE1:37
for D being absolutely-multiplicative MSSubsetFamily of M for J
being MSSetOp of M st for X being Element of bool M for SF being non-empty
MSSubsetFamily of M st (for Y being ManySortedSet of I holds Y in SF iff Y in D
& X c= Y) holds J..X = meet SF holds J is idempotent;
theorem :: CLOSURE1:38
for D being MSClosureSystem of S for J being MSSetOp of the Sorts of D
st for X being Element of bool the Sorts of D for SF being non-empty
MSSubsetFamily of the Sorts of D st (for Y being ManySortedSet of the carrier
of S holds Y in SF iff Y in the Family of D & X c= Y) holds J..X = meet SF
holds J is MSClosureOperator of the Sorts of D;
definition
let S;
let A be ManySortedSet of the carrier of S;
let C be MSClosureOperator of A;
func ClOp->ClSys C -> MSClosureSystem of S means
:: CLOSURE1:def 13
ex D being
MSSubsetFamily of A st D = MSFixPoints C & it = MSClosureStr (#A, D#);
end;
registration
let S;
let A be ManySortedSet of the carrier of S;
let C be MSClosureOperator of A;
cluster ClOp->ClSys C -> strict;
end;
registration
let S;
let A be non-empty ManySortedSet of the carrier of S;
let C be MSClosureOperator of A;
cluster ClOp->ClSys C -> non-empty;
end;
definition
let S;
let D be MSClosureSystem of S;
func ClSys->ClOp D -> MSClosureOperator of the Sorts of D means
:: CLOSURE1:def 14
for
X being Element of bool the Sorts of D for SF being non-empty MSSubsetFamily of
the Sorts of D st (for Y being ManySortedSet of the carrier of S holds Y in SF
iff Y in the Family of D & X c= Y) holds it..X = meet SF;
end;
theorem :: CLOSURE1:39
for A being ManySortedSet of the carrier of S for J being
MSClosureOperator of A holds ClSys->ClOp (ClOp->ClSys J) = J;
theorem :: CLOSURE1:40
for D being MSClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) =
the MSClosureStr of D;