:: On the Closure Operator and the Closure System of Many Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Received February 7, 1996
:: Copyright (c) 1996-2026 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;
definitions XBOOLE_0, PBOOLE, CARD_3, TARSKI;
equalities FUNCOP_1;
expansions XBOOLE_0, FUNCT_1, MSUALG_1, PBOOLE, TARSKI;
theorems FUNCOP_1, ENUMSET1, FUNCT_1, FUNCT_2, FUNCT_4, MBOOLEAN, PBOOLE,
PZFMISC1, SETFAM_1, TARSKI, MSSUBFAM, ZFMISC_1, XBOOLE_0, XBOOLE_1,
PARTFUN1, RELAT_1;
schemes FRAENKEL, FUNCT_1, FUNCT_2, DOMAIN_1, XBOOLE_0;
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
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 Th2:
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
proof
let I be non empty set, A be ManySortedSet of I, B be ManySortedSubset of A;
let a be object;
assume a in rng B;
then consider i being object such that
A1: i in I and
A2: a = B.i by PBOOLE:138;
i in dom bool A & bool (A.i) = (bool A).i by A1,MBOOLEAN:def 1,PARTFUN1:def 2
;
then
A3: bool (A.i) in rng bool A by FUNCT_1:def 3;
B c= A by PBOOLE:def 18;
then B in bool A by MBOOLEAN:18;
then B.i in (bool A).i by A1;
then a in bool (A.i) by A1,A2,MBOOLEAN:def 1;
hence thesis by A3,TARSKI:def 4;
end;
begin :: Set of Many Sorted Subsets of a Many Sorted Set
definition
let I, M;
defpred f[object] means $1 is ManySortedSubset of M;
func Bool M -> set means
:Def1:
for x being object holds x in it iff x is ManySortedSubset of M;
existence
proof
per cases;
suppose
A1: I is non empty;
consider X being set such that
A2: for e being object holds e in X iff e in Funcs(I, union rng bool M)
& f[e] from XBOOLE_0:sch 1;
take X;
let x be object;
thus x in X implies x is ManySortedSubset of M by A2;
assume
A3: x is ManySortedSubset of M;
now
reconsider xx = x as ManySortedSubset of M by A3;
dom xx = I & rng xx c= union rng bool M by A1,Th2,PARTFUN1:def 2;
hence x in Funcs(I, union rng bool M) by FUNCT_2:def 2;
thus f[ x ] by A3;
end;
hence thesis by A2;
end;
suppose
A4: I is empty;
take {EmptyMS {}};
let x be object;
thus x in {EmptyMS {}} implies x is ManySortedSubset of M
proof
reconsider M9 = M as ManySortedSet of {} by A4;
assume
A5: x in {EmptyMS {}};
reconsider y = EmptyMS {} as ManySortedSubset of M9 by PBOOLE:def 18;
y is ManySortedSubset of M by A4;
hence thesis by A5,TARSKI:def 1;
end;
assume x is ManySortedSubset of M;
then consider y being ManySortedSubset of M such that
A6: y = x;
y = EmptyMS {} by A4;
hence thesis by A6,TARSKI:def 1;
end;
end;
uniqueness
proof
thus for X1,X2 being set st
(for x being object holds x in X1 iff f[ x ]) & (
for x being object holds x in X2 iff f[ x ])
holds X1 = X2 from XBOOLE_0:sch 3;
end;
end;
registration
let I, M;
cluster Bool M -> non empty functional with_common_domain;
coherence
proof
M is ManySortedSubset of M by PBOOLE:def 18;
hence Bool M is non empty by Def1;
thus Bool M is functional
by Def1;
let f, g be Function;
assume that
A1: f in Bool M and
A2: g in Bool M;
A3: g is ManySortedSubset of M by A2,Def1;
f is ManySortedSubset of M by A1,Def1;
hence dom f = I by PARTFUN1:def 2
.= dom g by A3,PARTFUN1:def 2;
end;
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; :: redefines Bool (CLOSURE2, definition)
coherence
proof
Bool M c= Bool M;
hence thesis;
end;
end;
registration
let I, M;
cluster non empty functional with_common_domain for SubsetFamily of M;
existence
proof
take Bool M;
thus thesis;
end;
end;
registration
let I, M;
cluster empty finite for SubsetFamily of M;
existence
proof
reconsider x = {} as SubsetFamily of M by XBOOLE_1:2;
take x;
thus thesis;
end;
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; :: redefines Element (SUBSET_1, definition)
coherence
proof
let e be Element of S;
thus thesis by Def1;
end;
end;
theorem Th3: :: MSSUBFAM:34
SF \/ SG is SubsetFamily of M;
theorem :: MSSUBFAM:35
SF /\ SG is SubsetFamily of M;
theorem :: MSSUBFAM:36
SF \ x is SubsetFamily of M;
theorem :: MSSUBFAM:37
SF \+\ SG is SubsetFamily of M;
theorem Th7: :: MSSUBFAM:38
A c= M implies {A} is SubsetFamily of M
proof
assume A c= M;
then A is ManySortedSubset of M by PBOOLE:def 18;
then A in Bool M by Def1;
hence thesis by ZFMISC_1:31;
end;
theorem Th8: :: MSSUBFAM:39
A c= M & B c= M implies {A,B} is SubsetFamily of M
proof
assume A c= M & B c= M;
then {A} is SubsetFamily of M & {B} is SubsetFamily of M by Th7;
then {A} \/ {B} is SubsetFamily of M by Th3;
hence thesis by ENUMSET1:1;
end;
reserve E, T for Element of Bool M;
theorem Th9:
E (/\) T in Bool M
proof
E c= M & T c= M by PBOOLE:def 18;
then E (/\) T c= M (/\) M by PBOOLE:21;
then E (/\) T is ManySortedSubset of M by PBOOLE:def 18;
hence thesis by Def1;
end;
theorem Th10:
E (\/) T in Bool M
proof
E c= M & T c= M by PBOOLE:def 18;
then E (\/) T c= M (\/) M by PBOOLE:20;
then E (\/) T is ManySortedSubset of M by PBOOLE:def 18;
hence thesis by Def1;
end;
theorem
E (\) A in Bool M
proof
E c= M by PBOOLE:def 18;
then E (\) A c= M by MBOOLEAN:15;
then E (\) A is ManySortedSubset of M by PBOOLE:def 18;
hence thesis by Def1;
end;
theorem
E (\+\) T in Bool M
proof
T c= M by PBOOLE:def 18;
then
A1: T (\) E c= M by MBOOLEAN:15;
E c= M by PBOOLE:def 18;
then E (\) T c= M by MBOOLEAN:15;
then E (\+\) T c= M by A1,PBOOLE:91;
then E (\+\) T is ManySortedSubset of M by PBOOLE:def 18;
hence thesis by Def1;
end;
begin :: Many Sorted Operator corresponding
:: to the Operator on Many Sorted Subsets
definition
let S be functional set;
func |. S .| -> Function means
:Def2:
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 = {};
existence
proof
thus S <> {} implies ex f being Function st ex A being non empty
functional set st A = S & dom f = meet the set of all
dom x where x is Element of A & for i st i in dom f holds f.i = the set of
all x.i where x is Element of A
proof
assume S <> {};
then consider A being non empty functional set such that
A1: A = S;
deffunc F(object)
= the set of all x.$1 where x is Element of A ;
consider f being Function such that
A2: dom f = meet the set of all dom x where x is Element of A
& for i being object st
i in meet the set of all dom x where x is Element of A
holds f.i = F (i) from FUNCT_1:sch 3;
take f, A;
thus thesis by A1,A2;
end;
thus thesis;
end;
uniqueness
proof
let f, g be Function;
defpred P[Function] means ex A being non empty functional set st A = S &
dom $1 = meet the set of all dom x where x is Element of A & for i st
i in dom $1 holds $1.i = the set of all x.i where x is Element of A ;
thus S <> {} & P[f] & P[g] implies f = g
proof
assume that
S <> {} and
A3: P[f] and
A4: P[g];
consider A being non empty functional set such that
A5: A = S and
A6: dom f = meet the set of all dom x where x is Element of A and
A7: for i st i in dom f holds f.i = the set of all
x.i where x is Element of A by A3;
now
let a be object;
assume
A8: a in meet the set of all dom x where x is Element of A ;
hence f.a = the set of all x.a where x is Element of A by A6
,A7
.= g.a by A4,A5,A8;
end;
hence thesis by A4,A5,A6;
end;
thus thesis;
end;
consistency;
end;
theorem Th13:
for SF being non empty SubsetFamily of M holds dom |.SF.| = I
proof
let SF be non empty SubsetFamily of M;
consider A being non empty functional set such that
A1: A = SF and
A2: dom |.SF.| = meet the set of all dom x where x is Element of A and
for i st i in dom |.SF.| holds |.SF.|.i = the set of all
x.i where x is Element of A
by Def2;
the set of all dom x where x is Element of A = {I}
proof
thus the set of all dom x where x is Element of A c= {I}
proof
let a be object;
assume a in the set of all dom x where x is Element of A ;
then consider x being Element of A such that
A3: a = dom x;
x is Element of SF by A1;
then a = I by A3,PARTFUN1:def 2;
hence thesis by TARSKI:def 1;
end;
set x = the Element of A;
let a be object;
assume a in {I};
then
A4: a = I by TARSKI:def 1;
x is Element of SF by A1;
then dom x = I by PARTFUN1:def 2;
hence thesis by A4;
end;
hence thesis by A2,SETFAM_1:10;
end;
registration
let S be empty functional set;
cluster |. S .| -> empty;
coherence by Def2;
end;
definition
let I, M;
let S be SubsetFamily of M;
func |: S :| -> ManySortedSet of I equals
:Def3:
|. S .| if S <> {}
otherwise EmptyMS I;
coherence
proof
thus S <> {} implies |.S.| is ManySortedSet of I
proof
assume S <> {};
then dom |.S.| = I by Th13;
hence thesis by PARTFUN1:def 2,RELAT_1:def 18;
end;
thus thesis;
end;
consistency;
end;
registration
let I, M;
let S be empty SubsetFamily of M;
cluster |: S :| -> empty-yielding;
coherence
proof
|:S:| = EmptyMS I by Def3;
hence thesis;
end;
end;
theorem Th14:
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 }
proof
A1: dom |:SF:| = I by PARTFUN1:def 2;
assume
A2: SF is non empty;
then consider A being non empty functional set such that
A3: A = SF and
dom |.SF.| = meet the set of all dom x where x is Element of A and
A4: for i st i in dom |.SF.| holds |.SF.|.i = the set of all
x.i where x is Element
of A by Def2;
let i such that
A5: i in I;
set K = { x.i where x is Element of Bool M : x in SF }, N = the set of all
x.i where x is
Element of A ;
A6: K = N
proof
thus K c= N
proof
let q be object;
assume q in K;
then ex x being Element of Bool M st q = x.i & x in SF;
hence thesis by A3;
end;
let q be object;
assume q in N;
then consider x being Element of A such that
A7: q = x.i;
x in SF by A3;
hence thesis by A7;
end;
|:SF:| = |.SF.| by A2,Def3;
hence thesis by A4,A5,A1,A6;
end;
registration
let I, M;
let SF be non empty SubsetFamily of M;
cluster |: SF :| -> non-empty;
coherence
proof
let i be object;
assume i in I;
then
A1: |:SF:|.i = { x.i where x is Element of Bool M : x in SF} by Th14;
consider x being object such that
A2: x in SF by XBOOLE_0:def 1;
reconsider x as Element of Bool M by A2;
x.i in |:SF:|.i by A1,A2;
hence thesis;
end;
end;
theorem Th15:
dom |.{f}.| = dom f
proof
consider A being non empty functional set such that
A1: A = {f} and
A2: dom |.{f}.| = meet the set of all dom x where x is Element of A and
for i st i in dom |.{f}.| holds |.{f}.|.i = the set of all
x.i where x is Element of
A by Def2;
set m = the set of all dom x where x is Element of A ;
m = {dom f}
proof
thus m c= {dom f}
proof
let q be object;
assume q in m;
then consider x being Element of A such that
A3: q = dom x;
x = f by A1,TARSKI:def 1;
hence thesis by A3,TARSKI:def 1;
end;
let q be object;
assume q in {dom f};
then
A4: q = dom f by TARSKI:def 1;
f is Element of A by A1,TARSKI:def 1;
hence thesis by A4;
end;
hence thesis by A2,SETFAM_1:10;
end;
theorem
dom |.{f,f1}.| = dom f /\ dom f1
proof
consider A being non empty functional set such that
A1: A = {f,f1} and
A2: dom |.{f,f1}.| = meet the set of all dom x where x is Element of A and
for i st i in dom |.{f,f1}.| holds |.{f,f1}.|.i = the set of all
x.i where x is
Element of A by Def2;
set m = the set of all dom x where x is Element of A ;
m = {dom f, dom f1}
proof
thus m c= {dom f, dom f1}
proof
let q be object;
assume q in m;
then consider x being Element of A such that
A3: q = dom x;
x = f or x = f1 by A1,TARSKI:def 2;
hence thesis by A3,TARSKI:def 2;
end;
let q be object;
assume q in {dom f, dom f1};
then
A4: q = dom f or q = dom f1 by TARSKI:def 2;
f is Element of A & f1 is Element of A by A1,TARSKI:def 2;
hence thesis by A4;
end;
hence thesis by A2,SETFAM_1:11;
end;
theorem Th17:
i in dom f implies |.{f}.|.i = {f.i}
proof
A1: f in {f} by TARSKI:def 1;
consider A being non empty functional set such that
A2: A = {f} and
dom |.{f}.| = meet the set of all dom x where x is Element of A and
A3: for i st i in dom |.{f}.| holds |.{f}.|.i = the set of all
x.i where x is Element
of A by Def2;
assume i in dom f;
then i in dom |.{f}.| by Th15;
then
A4: |.{f}.|.i = the set of all x.i where x is Element of A by A3;
thus |.{f}.|.i c= { f.i }
proof
let q be object;
assume q in |.{f}.|.i;
then consider x being Element of A such that
A5: q = x.i by A4;
x = f by A2,TARSKI:def 1;
hence thesis by A5,TARSKI:def 1;
end;
let q be object;
assume q in { f.i };
then q = f.i by TARSKI:def 1;
hence thesis by A2,A4,A1;
end;
theorem
i in I & SF = {f} implies |:SF:|.i = {f.i}
proof
assume that
A1: i in I and
A2: SF = {f};
A3: |:SF:| = |.SF.| by A2,Def3;
dom |:SF:| = I by PARTFUN1:def 2;
then i in dom f by A1,A2,A3,Th15;
hence thesis by A2,A3,Th17;
end;
theorem Th19:
i in dom |.{f,f1}.| implies |.{f,f1}.|.i = { f.i, f1.i }
proof
A1: f in {f,f1} & f1 in {f,f1} by TARSKI:def 2;
consider A being non empty functional set such that
A2: A = {f,f1} and
dom |.{f,f1}.| = meet the set of all dom x where x is Element of A and
A3: for i st i in dom |.{f,f1}.| holds |.{f,f1}.|.i = the set of all
x.i where x is
Element of A by Def2;
assume i in dom |.{f,f1}.|;
then
A4: |.{f,f1}.|.i = the set of all x.i where x is Element of A by A3;
thus |.{f,f1}.|.i c= { f.i, f1.i }
proof
let q be object;
assume q in |.{f,f1}.|.i;
then consider x being Element of A such that
A5: q = x.i by A4;
per cases by A2,TARSKI:def 2;
suppose
x = f;
hence thesis by A5,TARSKI:def 2;
end;
suppose
x = f1;
hence thesis by A5,TARSKI:def 2;
end;
end;
let q be object;
assume q in { f.i, f1.i };
then q = f.i or q = f1.i by TARSKI:def 2;
hence thesis by A2,A4,A1;
end;
theorem Th20:
i in I & SF = {f,f1} implies |:SF:|.i = { f.i, f1.i }
proof
assume that
A1: i in I and
A2: SF = {f,f1};
dom |:SF:| = I & |:SF:| = |.SF.| by A2,Def3,PARTFUN1:def 2;
hence thesis by A1,A2,Th19;
end;
definition
let I, M, SF;
redefine func |:SF:| -> MSSubsetFamily of M; :: redefines |: (CLOSURE2, definition)
coherence
proof
per cases;
suppose
A1: SF is non empty;
|:SF:| is ManySortedSubset of bool M
proof
let i be object;
assume
A2: i in I;
then
A3: |:SF:|.i = { x.i where x is Element of Bool M : x in SF } by A1,Th14;
thus |:SF:|.i c= (bool M).i
proof
let x be object;
assume x in |:SF:|.i;
then consider a being Element of Bool M such that
A4: x = a.i and
a in SF by A3;
a c= M by PBOOLE:def 18;
then a.i c= M.i by A2;
then x in bool (M.i) by A4;
hence thesis by A2,MBOOLEAN:def 1;
end;
end;
hence thesis;
end;
suppose
SF is empty;
then |:SF:| = EmptyMS I;
hence thesis by MSSUBFAM:31;
end;
end;
end;
theorem Th21:
A in SF implies A in' |:SF:|
proof
assume
A1: A in SF;
let i be object;
assume i in I;
then |:SF:|.i = { x.i where x is Element of Bool M : x in SF } by A1,Th14;
hence thesis by A1;
end;
theorem Th22:
SF = {A,B} implies union |:SF:| = A (\/) B
proof
assume
A1: SF = {A,B};
now
let i be object;
assume
A2: i in I;
hence (union |:SF:|).i = union (|:SF:|.i) by MBOOLEAN:def 2
.= union { A.i, B.i } by A1,A2,Th20
.= A.i \/ B.i by ZFMISC_1:75
.= (A (\/) B).i by A2,PBOOLE:def 4;
end;
hence thesis;
end;
theorem Th23: :: SETFAM_1:12
SF = {E,T} implies meet |:SF:| = E (/\) T
proof
assume
A1: SF = { E,T };
now
reconsider sf1 = SF as non empty SubsetFamily of M by A1;
let i be object such that
A2: i in I;
ex Q be Subset-Family of (M.i) st Q = |:sf1:|.i & (meet |:sf1:|).i =
Intersect Q by A2,MSSUBFAM:def 1;
hence (meet |:SF:|).i = meet (|:sf1:|.i) by A2,SETFAM_1:def 9
.= meet {E.i,T.i} by A1,A2,Th20
.= E.i /\ T.i by SETFAM_1:11
.= (E (/\) T).i by A2,PBOOLE:def 5;
end;
hence thesis;
end;
theorem Th24: :: 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:|
proof
let Z be ManySortedSubset of M such that
A1: for Z1 be ManySortedSet of I st Z1 in SF holds Z c=' Z1;
let i be object such that
A2: i in I;
consider Q being Subset-Family of M.i such that
A3: Q = |:SF:|.i and
A4: (meet |:SF:|).i = Intersect Q by A2,MSSUBFAM:def 1;
A5: now
let q be set such that
A6: q in Q;
per cases;
suppose
SF is non empty;
then |:SF:|.i = { x.i where x is Element of Bool M : x in SF } by A2,Th14
;
then consider a being Element of Bool M such that
A7: q = a.i and
A8: a in SF by A3,A6;
Z c=' a by A1,A8;
hence Z.i c= q by A2,A7;
end;
suppose
SF is empty;
then |:SF:| = EmptyMS I;
hence Z.i c= q by A3,A6;
end;
end;
Z c= M by PBOOLE:def 18;
then Z.i is Subset of M.i by A2;
hence thesis by A4,A5,MSSUBFAM:4;
end;
theorem
|: Bool M :| = bool M
proof
now
let i be object;
assume
A1: i in I;
then
A2: |:Bool M:|.i = { x.i where x is Element of Bool M : x in Bool M} by Th14;
thus |: Bool M :|.i = (bool M).i
proof
thus |: Bool M :|.i c= (bool M).i
by A1,PBOOLE:def 2,def 18;
let a be object such that
A3: a in (bool M).i;
dom (EmptyMS I +* (i .--> a)) = I by A1,PZFMISC1:1;
then reconsider X = EmptyMS I +* (i .--> a) as ManySortedSet of I by
PARTFUN1:def 2,RELAT_1:def 18;
A4: dom (i .--> a) = {i};
i in {i} by TARSKI:def 1;
then
A5: X.i = (i .--> a).i by A4,FUNCT_4:13
.= a by FUNCOP_1:72;
X is ManySortedSubset of M
proof
let s be object such that
A6: s in I;
per cases;
suppose
A7: s = i;
then a in bool (M.s) by A3,A6,MBOOLEAN:def 1;
hence thesis by A5,A7;
end;
suppose
s <> i;
then not s in dom (i .--> a) by TARSKI:def 1;
then X.s = EmptyMS I.s by FUNCT_4:11
.= {};
hence thesis;
end;
end;
then X is Element of Bool M by Def1;
hence thesis by A2,A5;
end;
end;
hence thesis;
end;
definition
let I, M;
let IT be SubsetFamily of M;
attr IT is additive means
for A, B st A in IT & B in IT holds A (\/) B in IT;
attr IT is absolutely-additive means
for F be SubsetFamily of M st F c= IT holds union |:F:| in IT;
attr IT is multiplicative means
for A, B st A in IT & B in IT holds A (/\) B in IT;
attr IT is absolutely-multiplicative means
:Def7:
for F be SubsetFamily of M st F c= IT holds meet |:F:| in IT;
attr IT is properly-upper-bound means
:Def8:
M in IT;
attr IT is properly-lower-bound means
EmptyMS I in IT;
end;
Lm1: Bool M is additive absolutely-additive multiplicative
absolutely-multiplicative properly-upper-bound properly-lower-bound
proof
thus Bool M is additive
by Th10;
thus Bool M is absolutely-additive
proof
let F be SubsetFamily of M such that
F c= Bool M;
union |:F:| c= M by MSSUBFAM:40;
then union |:F:| is ManySortedSubset of M by PBOOLE:def 18;
hence thesis by Def1;
end;
thus Bool M is multiplicative
by Th9;
thus Bool M is absolutely-multiplicative
by Def1;
M is ManySortedSubset of M by PBOOLE:def 18;
then M in Bool M by Def1;
hence Bool M is properly-upper-bound;
EmptyMS I c= M by PBOOLE:43;
then EmptyMS I is ManySortedSubset of M by PBOOLE:def 18;
hence EmptyMS I in Bool M by Def1;
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;
existence
proof
take Bool M;
thus thesis by Lm1;
end;
end;
definition
let I, M;
redefine func Bool M -> additive absolutely-additive multiplicative :: redefines Bool (CLOSURE2, definition)
absolutely-multiplicative properly-upper-bound properly-lower-bound
SubsetFamily of M;
coherence by Lm1;
end;
registration
let I, M;
cluster absolutely-additive -> additive for SubsetFamily of M;
coherence
proof
let SF be SubsetFamily of M such that
A1: SF is absolutely-additive;
let A, B;
assume that
A2: A in SF and
A3: B in SF;
B is ManySortedSubset of M by A3,Def1;
then
A4: B c= M by PBOOLE:def 18;
A is ManySortedSubset of M by A2,Def1;
then A c= M by PBOOLE:def 18;
then reconsider ab = {A,B} as SubsetFamily of M by A4,Th8;
{A} c= SF & {B} c= SF by A2,A3,ZFMISC_1:31;
then {A} \/ {B} c= SF by XBOOLE_1:8;
then {A,B} c= SF by ENUMSET1:1;
then union |:ab:| in SF by A1;
hence thesis by Th22;
end;
end;
registration
let I, M;
cluster absolutely-multiplicative -> multiplicative for SubsetFamily of M;
coherence
proof
let SF be SubsetFamily of M such that
A1: SF is absolutely-multiplicative;
let A, B;
assume that
A2: A in SF and
A3: B in SF;
B is ManySortedSubset of M by A3,Def1;
then
A4: B c= M by PBOOLE:def 18;
A is ManySortedSubset of M by A2,Def1;
then A c= M by PBOOLE:def 18;
then reconsider ab = {A,B} as SubsetFamily of M by A4,Th8;
{A} c= SF & {B} c= SF by A2,A3,ZFMISC_1:31;
then {A} \/ {B} c= SF by XBOOLE_1:8;
then {A,B} c= SF by ENUMSET1:1;
then meet |:ab:| in SF by A1;
hence thesis by A2,A3,Th23;
end;
end;
registration
let I, M;
cluster absolutely-multiplicative -> properly-upper-bound for
SubsetFamily of M;
coherence
proof
reconsider a = {} as SubsetFamily of M by XBOOLE_1:2;
let SF be SubsetFamily of M such that
A1: SF is absolutely-multiplicative;
|:a:| = EmptyMS I;
then
A2: meet |:a:| = M by MSSUBFAM:41;
a c= SF;
hence M in SF by A1,A2;
end;
end;
registration
let I, M;
cluster properly-upper-bound -> non empty for SubsetFamily of M;
coherence;
end;
registration
let I, M;
cluster absolutely-additive -> properly-lower-bound for SubsetFamily of M;
coherence
proof
reconsider a = {} as SubsetFamily of M by XBOOLE_1:2;
let SF be SubsetFamily of M such that
A1: SF is absolutely-additive;
|:a:| = EmptyMS I;
then
A2: union |:a:| = EmptyMS I by MBOOLEAN:21;
a c= SF;
hence EmptyMS I in SF by A1,A2;
end;
end;
registration
let I, M;
cluster properly-lower-bound -> non empty for SubsetFamily of M;
coherence;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
f.x in Bool M;
hence thesis;
end;
end;
definition
let I, M;
let IT be SetOp of M;
attr IT is reflexive means
:Def10:
for x being Element of Bool M holds x c=' IT.x;
attr IT is monotonic means
:Def11:
for x, y being Element of Bool M st x c=' y holds IT.x c=' IT.y;
attr IT is idempotent means
:Def12:
for x being Element of Bool M holds IT.x = IT.(IT.x);
attr IT is topological means
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;
existence
proof
reconsider f = id (Bool M) as SetOp of M;
take f;
thus f is reflexive;
thus f is monotonic;
thus f is idempotent;
thus f is topological
proof
let X, Y be Element of Bool M;
X c= M & Y c= M by PBOOLE:def 18;
then X (\/) Y c= M by PBOOLE:16;
then X (\/) Y is ManySortedSubset of M by PBOOLE:def 18;
then X (\/) Y in Bool M by Def1;
hence f.(X (\/) Y) = X (\/) Y by FUNCT_1:18
.= f.X (\/) Y
.= f.X (\/) f.Y;
end;
end;
end;
theorem :: CLOSURE:11
id (Bool A) is reflexive SetOp of A
proof
reconsider f = id (Bool A) as SetOp of A;
f is reflexive;
hence thesis;
end;
theorem :: CLOSURE:12
id (Bool A) is monotonic SetOp of A
proof
reconsider f = id (Bool A) as SetOp of A;
f is monotonic;
hence thesis;
end;
theorem :: CLOSURE:13
id (Bool A) is idempotent SetOp of A
proof
reconsider f = id (Bool A) as SetOp of A;
f is idempotent;
hence thesis;
end;
theorem :: CLOSURE:15
id (Bool A) is topological SetOp of A
proof
reconsider f = id (Bool A) as SetOp of A;
f is topological
proof
let X, Y be Element of Bool A;
X c= A & Y c= A by PBOOLE:def 18;
then X (\/) Y c= A by PBOOLE:16;
then X (\/) Y is ManySortedSubset of A by PBOOLE:def 18;
then X (\/) Y in Bool A by Def1;
hence f.(X (\/) Y) = X (\/) Y by FUNCT_1:18
.= f.X (\/) Y
.= f.X (\/) f.Y;
end;
hence thesis;
end;
reserve g, h for SetOp of M;
theorem :: CLOSURE:16
E = M & g is reflexive implies E = g.E
proof
assume
A1: E = M;
assume g is reflexive;
then
A2: E c= g.E;
g.E c= E by A1,PBOOLE:def 18;
hence thesis by A2,PBOOLE:146;
end;
theorem :: CLOSURE:17
(g is reflexive & for X being Element of Bool M holds g.X c= X)
implies g is idempotent
proof
assume that
A1: g is reflexive and
A2: for X being Element of Bool M holds g.X c= X;
let X be Element of Bool M;
A3: g.X c= g.(g.X) by A1;
g.(g.X) c= g.X by A2;
hence thesis by A3,PBOOLE:146;
end;
theorem :: 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
proof
let A be Element of Bool M such that
A1: A = E (/\) T;
assume
A2: g is monotonic;
E (/\) T c= T by PBOOLE:15;
then
A3: g.A c= g.T by A1,A2;
E (/\) T c= E by PBOOLE:15;
then g.A c= g.E by A1,A2;
hence thesis by A3,PBOOLE:17;
end;
registration
let I, M;
cluster topological -> monotonic for SetOp of M;
coherence
proof
let g be SetOp of M such that
A1: g is topological;
let X, Y be Element of Bool M such that
A2: X c= Y;
g.X (\/) g.Y = g.(X (\/) Y) by A1
.= g.Y by A2,PBOOLE:22;
hence thesis by PBOOLE:26;
end;
end;
theorem :: 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
proof
let A be Element of Bool M such that
A1: A = E (\) T;
assume
A2: g is topological;
then g.E (\/) g.T = g.(E (\/) T)
.= g.((E(\)T) (\/) T) by PBOOLE:67
.= (g.A) (\/) (g.T) by A1,A2;
then g.E c= g.A (\/) g.T by PBOOLE:14;
then g.E (\) g.T c= (g.A (\/) g.T) (\) g.T by PBOOLE:53;
then
A3: g.E (\) g.T c= g.A (\) g.T by PBOOLE:75;
g.A (\) g.T c= g.A by PBOOLE:56;
hence thesis by A3,PBOOLE:13;
end;
definition
let I, M, h, g;
redefine func g * h -> SetOp of M; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence
proof
g * h is Function of Bool M, Bool M;
hence thesis;
end;
end;
theorem :: CLOSURE:21
g is reflexive & h is reflexive implies g * h is reflexive
proof
assume
A1: g is reflexive & h is reflexive;
let X be Element of Bool M;
X c= h.X & h.X c= g.(h.X) by A1;
then dom h = Bool M & X c= g.(h.X) by FUNCT_2:def 1,PBOOLE:13;
hence thesis by FUNCT_1:13;
end;
theorem :: CLOSURE:22
g is monotonic & h is monotonic implies g * h is monotonic
proof
assume that
A1: g is monotonic and
A2: h is monotonic;
A3: dom h = Bool M by FUNCT_2:def 1;
let X, Y be Element of Bool M;
assume X c= Y;
then h.X c= h.Y by A2;
then g.(h.X) c= g.(h.Y) by A1;
then g.(h.X) c= (g*h).Y by A3,FUNCT_1:13;
hence thesis by A3,FUNCT_1:13;
end;
theorem :: CLOSURE:23
g is idempotent & h is idempotent & g*h = h*g implies g * h is idempotent
proof
assume that
A1: g is idempotent and
A2: h is idempotent and
A3: g*h = h*g;
let X be Element of Bool M;
A4: dom g = Bool M by FUNCT_2:def 1;
A5: dom h = Bool M by FUNCT_2:def 1;
hence (g*h).X = g.(h.X) by FUNCT_1:13
.= g.(h.(h.X)) by A2
.= g.(g.(h.(h.X))) by A1
.= g.((h*g).(h.X)) by A3,A5,FUNCT_1:13
.= g.(h.(g.(h.X))) by A4,FUNCT_1:13
.= g.(h.((g*h).X)) by A5,FUNCT_1:13
.= (g*h).((g*h).X) by A5,FUNCT_1:13;
end;
theorem :: CLOSURE:25
g is topological & h is topological implies g * h is topological
proof
assume that
A1: g is topological and
A2: h is topological;
let X, Y be Element of Bool M;
A3: dom h = Bool M by FUNCT_2:def 1;
hence (g*h).(X (\/) Y) = g.(h.(X (\/) Y)) by Th10,FUNCT_1:13
.= g.(h.X (\/) h.Y) by A2
.= g.(h.X) (\/) g.(h.Y) by A1
.= (g*h).X (\/) g.(h.Y) by A3,FUNCT_1:13
.= (g*h).X (\/) (g*h).Y by A3,FUNCT_1:13;
end;
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
:Def14:
the Family of IT is additive;
attr IT is absolutely-additive means
:Def15:
the Family of IT is absolutely-additive;
attr IT is multiplicative means
:Def16:
the Family of IT is multiplicative;
attr IT is absolutely-multiplicative means
:Def17:
the Family of IT is absolutely-multiplicative;
attr IT is properly-upper-bound means
:Def18:
the Family of IT is properly-upper-bound;
attr IT is properly-lower-bound means
:Def19:
the Family of IT is properly-lower-bound;
end;
definition
let S, MS;
func Full MS -> ClosureStr over S equals
ClosureStr (#the Sorts of MS, Bool the Sorts of MS#);
correctness;
end;
registration
let S, MS;
cluster Full MS -> strict additive absolutely-additive multiplicative
absolutely-multiplicative properly-upper-bound properly-lower-bound;
coherence;
end;
registration
let S;
let MS be non-empty many-sorted over S;
cluster Full MS -> non-empty;
coherence;
end;
registration
let S;
cluster strict non-empty additive absolutely-additive multiplicative
absolutely-multiplicative properly-upper-bound properly-lower-bound for
ClosureStr
over S;
existence
proof
set a = the non-empty many-sorted over S;
take Full a;
thus thesis;
end;
end;
registration
let S;
let CS be additive ClosureStr over S;
cluster the Family of CS -> additive;
coherence by Def14;
end;
registration
let S;
let CS be absolutely-additive ClosureStr over S;
cluster the Family of CS -> absolutely-additive;
coherence by Def15;
end;
registration
let S;
let CS be multiplicative ClosureStr over S;
cluster the Family of CS -> multiplicative;
coherence by Def16;
end;
registration
let S;
let CS be absolutely-multiplicative ClosureStr over S;
cluster the Family of CS -> absolutely-multiplicative;
coherence by Def17;
end;
registration
let S;
let CS be properly-upper-bound ClosureStr over S;
cluster the Family of CS -> properly-upper-bound;
coherence by Def18;
end;
registration
let S;
let CS be properly-lower-bound ClosureStr over S;
cluster the Family of CS -> properly-lower-bound;
coherence by Def19;
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;
coherence;
end;
registration
let S, MS;
let F be additive SubsetFamily of the Sorts of MS;
cluster ClosureStr (#the Sorts of MS, F#) -> additive;
coherence;
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;
coherence;
end;
registration
let S, MS;
let F be multiplicative SubsetFamily of the Sorts of MS;
cluster ClosureStr (#the Sorts of MS, F#) -> multiplicative;
coherence;
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;
coherence;
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;
coherence;
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;
coherence;
end;
registration
let S;
cluster absolutely-additive -> additive for ClosureStr over S;
coherence;
end;
registration
let S;
cluster absolutely-multiplicative -> multiplicative for ClosureStr over S;
coherence;
end;
registration
let S;
cluster absolutely-multiplicative -> properly-upper-bound for
ClosureStr over S;
coherence;
end;
registration
let S;
cluster absolutely-additive -> properly-lower-bound for ClosureStr over S;
coherence;
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
:Def21:
the Sorts of it = A &
the Family of it = { x where x is Element of Bool A : g.x = x };
existence
proof
defpred P[set] means g.$1 = $1;
set SF = { x where x is Element of Bool A : P[ x ] };
SF is Subset of Bool A from DOMAIN_1:sch 7;
then reconsider D = SF as SubsetFamily of A;
take ClosureStr (#A, D#);
thus thesis;
end;
uniqueness;
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;
coherence
proof
A1: the Sorts of ClOp->ClSys g = A by Def21;
defpred P[set] means g.$1 = $1;
set SF = { x where x is Element of Bool A : P[ x ] };
A2: SF = the Family of ClOp->ClSys g by Def21;
SF is Subset of Bool A from DOMAIN_1:sch 7;
then reconsider D = SF as SubsetFamily of A;
A3: ClOp->ClSys g = ClosureStr (#A, D#) by A1,A2;
D is absolutely-multiplicative
proof
let F be SubsetFamily of A such that
A4: F c= D;
reconsider mf = meet |:F:| as Element of Bool A by Def1;
now
let Z1 be ManySortedSet of the carrier of S;
assume
A5: Z1 in F;
then reconsider y1 = Z1 as Element of Bool A;
Z1 in D by A4,A5;
then
A6: ex a being Element of Bool A st Z1 = a & g.a = a;
mf c=' y1 by A5,Th21,MSSUBFAM:43;
hence g.mf c=' Z1 by A6,Def11;
end;
then
A7: g.mf c=' mf by Th24;
mf c=' g.mf by Def10;
then g.mf = mf by A7,PBOOLE:146;
hence thesis;
end;
hence ClOp->ClSys g is absolutely-multiplicative by A3;
end;
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
:Def22:
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 };
existence
proof
defpred P[Element of Bool the Sorts of A] means C c= $1 & $1 in the Family
of A;
{ X where X is Element of Bool the Sorts of A : P[X] } is Subset of
Bool the Sorts of A from DOMAIN_1:sch 7;
then reconsider
F = { X where X is Element of Bool the Sorts of A : C c= X & X
in the Family of A } as SubsetFamily of the Sorts of A;
reconsider IT = meet |:F:| as Element of Bool the Sorts of A by Def1;
take IT,F;
thus thesis;
end;
uniqueness;
end;
theorem Th38:
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
proof
let D be ClosureSystem of S, a be Element of Bool the Sorts of D, f be SetOp
of the Sorts of D such that
A1: a in the Family of D and
A2: for x being Element of Bool the Sorts of D holds f.x = Cl x;
consider F being SubsetFamily of the Sorts of D such that
A3: Cl a = meet |:F:| and
A4: F = { X where X is Element of Bool the Sorts of D : a c=' X & X in
the Family of D } by Def22;
A5: f.a = meet |:F:| by A2,A3;
a in F by A1,A4;
then
A6: f.a c= a by A5,Th21,MSSUBFAM:43;
for Z1 being ManySortedSet of the carrier of S st Z1 in F holds a c=' Z1
proof
let Z1 be ManySortedSet of the carrier of S;
assume Z1 in F;
then ex b being Element of Bool the Sorts of D st Z1 = b & a c=' b & b in
the Family of D by A4;
hence thesis;
end;
then a c= f.a by A5,Th24;
hence thesis by A6,PBOOLE:146;
end;
theorem
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
proof
deffunc F(set) = $1;
let D be ClosureSystem of S, a be Element of Bool the Sorts of D, f be SetOp
of the Sorts of D such that
A1: f.a = a & for x being Element of Bool the Sorts of D holds f.x = Cl x;
set F = the Family of D, M = the Sorts of D;
defpred P[Element of Bool M] means a c=' $1;
defpred R[Element of Bool M] means a c=' $1 & $1 in F;
defpred S[Element of Bool M] means $1 in F & a c=' $1;
A2: { F(w) where w is Element of Bool M : F(w) in F & P[w] } c= F from
FRAENKEL:sch 17;
A3: for q being Element of Bool M holds R[q] iff S[q];
A4: { F(s) where s is Element of Bool M : R[s] } = { F(b) where b is Element
of Bool M : S[b] } from FRAENKEL:sch 3(A3);
consider SF being SubsetFamily of M such that
A5: Cl a = meet |:SF:| and
A6: SF = { X where X is Element of Bool M : a c= X & X in F } by Def22;
a = meet |:SF:| by A1,A5;
hence thesis by A6,A2,A4,Def7;
end;
theorem Th40:
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
proof
let D be ClosureSystem of S, f be SetOp of the Sorts of D such that
A1: for x being Element of Bool the Sorts of D holds f.x = Cl x;
set M = the Sorts of D;
A2: f is reflexive
proof
let x be Element of Bool M;
consider F being SubsetFamily of M such that
A3: Cl x = meet |:F:| and
A4: F = { X where X is Element of Bool the Sorts of D : x c=' X & X in
the Family of D } by Def22;
A5: for Z1 being ManySortedSet of the carrier of S st Z1 in F holds x c=' Z1
proof
let Z1 be ManySortedSet of the carrier of S;
assume Z1 in F;
then
ex a being Element of Bool M st Z1 = a & x c=' a & a in the Family of
D by A4;
hence thesis;
end;
f.x = meet |:F:| by A1,A3;
hence thesis by A5,Th24;
end;
A6: f is monotonic
proof
let x, y be Element of Bool M such that
A7: x c=' y;
consider Fy being SubsetFamily of M such that
A8: Cl y = meet |:Fy:| and
A9: Fy = { X where X is Element of Bool the Sorts of D : y c=' X & X
in the Family of D } by Def22;
consider Fx being SubsetFamily of M such that
A10: Cl x = meet |:Fx:| and
A11: Fx = { X where X is Element of Bool the Sorts of D : x c=' X & X
in the Family of D } by Def22;
|:Fy:| c=' |:Fx:|
proof
let i be object such that
A12: i in the carrier of S;
thus |:Fy:|.i c= |:Fx:|.i
proof
let q be object such that
A13: q in |:Fy:|.i;
per cases;
suppose
Fy is empty;
then reconsider Fy9 = Fy as empty SubsetFamily of M;
|:Fy9:|.i is empty;
hence thesis by A13;
end;
suppose
Fy is non empty;
then |:Fy:|.i = { e.i where e is Element of Bool M : e in Fy } by A12
,Th14;
then consider w being Element of Bool M such that
A14: q = w.i and
A15: w in Fy by A13;
A16: ex r being Element of Bool M st r = w & y c=' r & r in the
Family of D by A9,A15;
then x c=' w by A7,PBOOLE:13;
then
A17: w in Fx by A11,A16;
then |:Fx:|.i = { e.i where e is Element of Bool M : e in Fx } by A12
,Th14;
hence thesis by A14,A17;
end;
end;
end;
then meet |:Fx:| c=' meet |:Fy:| by MSSUBFAM:46;
then meet |:Fx:| c=' f.y by A1,A8;
hence thesis by A1,A10;
end;
f is idempotent
proof
let x be Element of Bool M;
consider F being SubsetFamily of M such that
A18: Cl x = meet |:F:| and
A19: F = { X where X is Element of Bool the Sorts of D : x c=' X & X
in the Family of D } by Def22;
F c= the Family of D
proof
let k be object;
assume k in F;
then
ex q being Element of Bool M st k = q & x c=' q & q in the Family of
D by A19;
hence thesis;
end;
then
A20: meet |:F:| in the Family of D by Def7;
thus f.x = meet |:F:| by A1,A18
.= f.(meet |:F:|) by A1,A20,Th38
.= f.(f.x) by A1,A18;
end;
hence thesis by A2,A6;
end;
definition
let S;
let D be ClosureSystem of S;
func ClSys->ClOp D -> ClosureOperator of the Sorts of D means
:Def23:
for x being Element of Bool the Sorts of D holds it.x = Cl x;
existence
proof
set M = the Sorts of D;
deffunc F(Element of Bool M) = Cl $1;
consider f being Function of Bool M, Bool M such that
A1: for x being Element of Bool M holds f.x = F(x) from FUNCT_2:sch 4;
reconsider f as SetOp of M;
reconsider f as ClosureOperator of M by A1,Th40;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f, g be ClosureOperator of the Sorts of D such that
A2: for x being Element of Bool the Sorts of D holds f.x = Cl x and
A3: for x being Element of Bool the Sorts of D holds g.x = Cl x;
now
set X = Bool the Sorts of D;
thus X = dom f by FUNCT_2:def 1;
thus X = dom g by FUNCT_2:def 1;
let x be object;
assume x in X;
then reconsider x1 = x as Element of Bool the Sorts of D;
thus f.x = Cl x1 by A2
.= g.x by A3;
end;
hence f = g;
end;
end;
theorem
for A being ManySortedSet of the carrier of S for f being
ClosureOperator of A holds ClSys->ClOp (ClOp->ClSys f) = f
proof
let A be ManySortedSet of the carrier of S, f be ClosureOperator of A;
set D = ClOp->ClSys f, M = the Sorts of D, f1 = ClSys->ClOp D;
A1: A = M by Def21;
then reconsider ff = f as reflexive idempotent monotonic SetOp of M;
for x being object st x in Bool A holds f1.x = ff.x
proof
let x be object;
assume x in Bool A;
then reconsider x1 = x as Element of Bool M by Def21;
consider F being SubsetFamily of M such that
A2: Cl x1 = meet |:F:| and
A3: F = { X where X is Element of Bool M : x1 c=' X & X in the Family
of D } by Def22;
A4: now
A5: x1 c=' ff.x1 by Def10;
x1 c=' M & M in the Family of D by Def8,PBOOLE:def 18;
then M in F by A3;
then reconsider F9 = F as non empty SubsetFamily of M;
let i be object;
assume
A6: i in the carrier of S;
then consider Q be Subset-Family of (M.i) such that
A7: Q = |:F:|.i and
A8: (meet |:F:|).i = Intersect Q by MSSUBFAM:def 1;
A9: Q = { q.i where q is Element of Bool M : q in F9 } by A6,A7,Th14;
A10: the Family of D = { q where q is Element of Bool M : ff.q = q } by A1
,Def21;
A11: now
let z be set;
assume z in Q;
then consider q being Element of Bool M such that
A12: z = q.i and
A13: q in F9 by A9;
consider X being Element of Bool M such that
A14: q = X and
A15: x1 c=' X & X in the Family of D by A3,A13;
(ex t being Element of Bool M st X = t & ff.t = t )& ff.x1 c=' ff
.X by A10,A15,Def11;
hence ff.x1.i c= z by A6,A12,A14;
end;
ff.(ff.x1) = ff.x1 by Def12;
then ff.x1 in the Family of D by A10;
then ff.x1 in F9 by A3,A5;
then ff.x1.i in Q by A9;
then
A16: (meet |:F:|).i c= ff.x1.i by A8,MSSUBFAM:2;
Q = |:F9:|.i by A7;
then ff.x1.i c= (meet |:F:|).i by A6,A8,A11,MSSUBFAM:5;
hence (meet |:F:|).i = ff.x1.i by A16;
end;
thus f1.x = Cl x1 by Def23
.= ff.x by A2,A4,PBOOLE:3;
end;
hence thesis by A1,FUNCT_2:12;
end;
deffunc F(set) = $1;
theorem
for D being ClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = the
ClosureStr of D
proof
let D be ClosureSystem of S;
set M = the Sorts of D, F = the Family of D, d = the Family of ClOp->ClSys (
ClSys->ClOp D), f = ClSys->ClOp D;
A1: d = { x where x is Element of Bool M : f.x = x } by Def21;
F = d
proof
thus F c= d
proof
let q be object;
assume
A2: q in F;
then reconsider q1 = q as Element of Bool M;
consider SF being SubsetFamily of M such that
A3: Cl q1 = meet |:SF:| and
A4: SF = { X where X is Element of Bool M : q1 c= X & X in F } by Def22;
q1 c=' M & M in F by Def8,PBOOLE:def 18;
then M in SF by A4;
then reconsider SF9 = SF as non empty SubsetFamily of M;
now
let i be object;
assume
A5: i in the carrier of S;
then consider Q be Subset-Family of (M.i) such that
A6: Q = |:SF9:|.i and
A7: (meet |:SF9:|).i = Intersect Q by MSSUBFAM:def 1;
A8: Q = { x.i where x is Element of Bool M : x in SF9 } by A5,A6,Th14;
q1 in SF9 by A2,A4;
then
A9: q1.i in Q by A8;
then
A10: Intersect Q c= q1.i by MSSUBFAM:2;
now
let z be set;
assume z in Q;
then consider x being Element of Bool M such that
A11: z = x.i and
A12: x in SF9 by A8;
ex xx being Element of Bool M st xx = x & q1 c=' xx & xx in F by A4
,A12;
hence q1.i c= z by A5,A11;
end;
then q1.i c= Intersect Q by A9,MSSUBFAM:5;
then Intersect Q = q1.i by A10;
hence f.q1.i = q1.i by A3,A7,Def23;
end;
then f.q1 = q1;
hence thesis by A1;
end;
let q be object;
assume q in d;
then consider x being Element of Bool M such that
A13: q = x & f.x = x by A1;
defpred S[Element of Bool M] means $1 in F & x c=' $1;
defpred R[Element of Bool M] means x c=' $1 & $1 in F;
defpred P[Element of Bool M] means x c=' $1;
A14: { F(w) where w is Element of Bool M : F(w) in F & P[w] } c= F from
FRAENKEL:sch 17;
A15: for a being Element of Bool M holds R[a] iff S[a];
A16: { F(a) where a is Element of Bool M : R[a] } = { F(b) where b is
Element of Bool M : S[b] } from FRAENKEL:sch 3(A15);
consider SF being SubsetFamily of M such that
A17: Cl x = meet |:SF:| and
A18: SF = { X where X is Element of Bool M : x c=' X & X in F } by Def22;
meet |:SF:| = q by A13,A17,Def23;
hence thesis by A18,A14,A16,Def7;
end;
hence thesis by Def21;
end;