:: On the Many Sorted Closure Operator and the Many Sorted Closure
:: System
:: 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, 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;
definitions XBOOLE_0, FUNCT_1, MSSUBFAM, MSUALG_3, PBOOLE, FINSET_1, TARSKI;
equalities XBOOLE_0, FUNCOP_1;
expansions XBOOLE_0, FUNCT_1, MSUALG_1, PBOOLE, TARSKI;
theorems FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_4, MBOOLEAN, MSSUBFAM, MSUALG_3,
PBOOLE, PZFMISC1, TARSKI, ZFMISC_1, PRALG_1, XBOOLE_0, PARTFUN1, RELAT_1;
schemes MSSUBFAM, PBOOLE, XBOOLE_0;
begin :: Preliminaries
reserve i, x, I for set,
A, M for ManySortedSet of I,
f for Function,
F for ManySortedFunction of I;
scheme
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() proof
assume
A1: for X being ManySortedSet of I() holds X in A() iff X in B() & P[X];
consider K being ManySortedSet of I() such that
A2: K in A() by PBOOLE:134;
let i be object such that
A3: i in I();
let x be object such that
A4: x in A().i;
dom (K +* (i .--> x)) = I() by A3,PZFMISC1:1;
then reconsider X = K +* (i .--> x) as ManySortedSet of I() by PARTFUN1:def 2
,RELAT_1:def 18;
A5: dom (i .--> x) = {i};
i in {i} by TARSKI:def 1;
then
A6: X.i = (i .--> x).i by A5,FUNCT_4:13
.= x by FUNCOP_1:72;
X in A()
proof
let s be object such that
A7: s in I();
per cases;
suppose
s = i;
hence thesis by A4,A6;
end;
suppose
s <> i;
then not s in dom (i .--> x) by TARSKI:def 1;
then X.s = K.s by FUNCT_4:11;
hence thesis by A2,A7;
end;
end;
then X in B() by A1;
hence thesis by A3,A6;
end;
theorem Th1:
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 }
proof
let X be non empty set, x, y be set such that
A1: x c= y;
let a be object;
reconsider aa=a as set by TARSKI:1;
assume a in { t where t is Element of X : y c= t };
then
A2: ex b be Element of X st b = a & y c= b;
then x c= aa by A1;
hence thesis by A2;
end;
theorem
(ex A st A in M) implies M is non-empty;
registration
let I, F, A;
cluster F..A -> total for I-defined Function;
coherence;
end;
Lm1: now
let I;
let A, B be non-empty ManySortedSet of I;
let F be ManySortedFunction of A, B;
let X be Element of A;
thus F..X is Element of B
proof
let i be object such that
A1: i in I;
reconsider g = F.i as Function;
g is Function of A.i, B.i & X.i is Element of A.i
by A1,PBOOLE:def 14,def 15; then
dom F = I & g.(X.i) in B.i by A1,FUNCT_2:5,PARTFUN1:def 2;
hence thesis by A1,PRALG_1:def 20;
end;
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; :: redefines .. (PRALG_1, definition)
coherence by Lm1;
end;
theorem
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
proof
let A, X be ManySortedSet of I;
let B be non-empty ManySortedSet of I;
let F be ManySortedFunction of A, B such that
A1: X in A;
let i be object such that
A2: i in I;
reconsider g = F.i as Function;
A3: g is Function of A.i, B.i by A2,PBOOLE:def 15;
X.i in A.i by A1,A2;
then dom F = I & g.(X.i) in B.i by A2,A3,FUNCT_2:5,PARTFUN1:def 2;
hence thesis by A2,PRALG_1:def 20;
end;
theorem Th4:
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
proof
let F, G be ManySortedFunction of I;
reconsider FG = F ** G as ManySortedFunction of I by MSSUBFAM:15;
A3: dom FG = I by PARTFUN1:def 2;
let A be ManySortedSet of I such that
A4: A in doms G;
A5: now
let i be object;
reconsider f = F.i as Function;
reconsider g = G.i as Function;
reconsider fg = (F**G).i as Function;
assume
A6: i in I;
then dom g = (doms G).i by MSSUBFAM:14;
then
A7: A.i in dom g by A4,A6;
(G..A).i = g.(A.i) by A6,PRALG_1:def 20;
hence (F..(G..A)).i = f.(g.(A.i)) by A6,PRALG_1:def 20
.= (f*g).(A.i) by A7,FUNCT_1:13
.= fg.(A.i) by A3,A6,PBOOLE:def 19
.= ((F ** G)..A).i by A3,A6,PRALG_1:def 20;
end;
FG..A is ManySortedSet of I;
hence thesis by A5,PBOOLE:3;
end;
theorem
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
proof
assume
A1: F is "1-1";
let A, B be ManySortedSet of I such that
A2: A in doms F & B in doms F and
A3: F..A = F..B;
now
let i be object such that
A4: i in I;
reconsider f = F.i as Function;
A5: f is one-to-one by A1,A4,MSUALG_3:1;
dom f = (doms F).i by A4,MSSUBFAM:14;
then
A6: A.i in dom f & B.i in dom f by A2,A4;
f.(A.i) = (F..A).i by A4,PRALG_1:def 20
.= f.(B.i) by A3,A4,PRALG_1:def 20;
hence A.i = B.i by A5,A6;
end;
hence thesis;
end;
theorem
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"
proof
assume that
A1: doms F is non-empty and
A2: for A, B being ManySortedSet of I st A in doms F & B in doms F & F..
A = F..B holds A = B;
consider K being ManySortedSet of I such that
A3: K in doms F by A1,PBOOLE:134;
let i be set, f be Function such that
A4: i in dom F and
A5: F.i = f;
let x1, x2 be object such that
A6: x1 in dom f and
A7: x2 in dom f and
A8: f.x1 = f.x2;
A9: dom F = I by PARTFUN1:def 2;
then dom (K +* (i .--> x1)) = I by A4,PZFMISC1:1;
then reconsider X1 = K +* (i .--> x1) as ManySortedSet of I
by PARTFUN1:def 2,RELAT_1:def 18;
A10: dom (i .--> x1) = {i};
i in {i} by TARSKI:def 1; then
A11: X1.i = (i .--> x1).i by A10,FUNCT_4:13
.= x1 by FUNCOP_1:72;
A12: X1 in doms F
proof
let s be object such that
A13: s in I;
per cases;
suppose
s = i;
hence thesis by A5,A6,A11,A13,MSSUBFAM:14;
end;
suppose
s <> i;
then not s in dom (i .--> x1) by TARSKI:def 1;
then X1.s = K.s by FUNCT_4:11;
hence thesis by A3,A13;
end;
end;
dom (K +* (i .--> x2)) = I by A4,A9,PZFMISC1:1;
then reconsider X2 = K +* (i .--> x2) as ManySortedSet of I
by PARTFUN1:def 2,RELAT_1:def 18;
A14: dom (i .--> x2) = {i};
i in {i} by TARSKI:def 1; then
A15: X2.i = (i .--> x2).i by A14,FUNCT_4:13
.= x2 by FUNCOP_1:72;
A16: X2 in doms F
proof
let s be object such that
A17: s in I;
per cases;
suppose
s = i;
hence thesis by A5,A7,A15,A17,MSSUBFAM:14;
end;
suppose
s <> i;
then not s in dom (i .--> x2) by TARSKI:def 1;
then X2.s = K.s by FUNCT_4:11;
hence thesis by A3,A17;
end;
end;
now
let s be object such that
A18: s in I;
per cases;
suppose
A19: s = i;
B1: s in dom F by A18,PARTFUN1:def 2;
B2: s in dom X2 & s in dom X1 by A18,PARTFUN1:def 2; then
s in dom F /\ dom X2 by B1,XBOOLE_0:def 4; then
a20: s in dom (F..X2) by PRALG_1:def 19;
s in dom F /\ dom X1 by B1,B2,XBOOLE_0:def 4; then
s in dom (F..X1) by PRALG_1:def 19;
hence (F..X1).s = f.(X2.s) by A5,A8,A11,A15,A19,PRALG_1:def 19
.= (F..X2).s by A5,A19,PRALG_1:def 19,a20;
end;
suppose
A20: s <> i;
then not s in dom (i .--> x2) by TARSKI:def 1;
then
A21: X2.s = K.s by FUNCT_4:11;
reconsider f1 = F.s as Function;
A22: not s in dom (i .--> x1) by A20,TARSKI:def 1;
thus (F..X1).s = f1.(X1.s) by A18,PRALG_1:def 20
.= f1.(X2.s) by A22,A21,FUNCT_4:11
.= (F..X2).s by A18,PRALG_1:def 20;
end;
end;
hence thesis by A2,A11,A15,A12,A16,PBOOLE:3;
end;
theorem Th7: :: 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
proof
let A, B be non-empty ManySortedSet of I, F, G be ManySortedFunction of A, B
such that
A1: for M st M in A holds F..M = G..M;
now
let i be object;
assume
A2: i in I;
then reconsider f = F.i as Function of A.i, B.i by PBOOLE:def 15;
reconsider g = G.i as Function of A.i, B.i by A2,PBOOLE:def 15;
now
consider K being ManySortedSet of I such that
A4: K in A by PBOOLE:134;
let x be object such that
A5: x in A.i;
dom (K +* (i .--> x)) = I by A2,PZFMISC1:1;
then reconsider X = K +* (i .--> x) as ManySortedSet of I by
PARTFUN1:def 2,RELAT_1:def 18;
A6: dom (i .--> x) = {i};
i in {i} by TARSKI:def 1;
then
A7: X.i = (i .--> x).i by A6,FUNCT_4:13
.= x by FUNCOP_1:72;
X in A
proof
let s be object such that
A8: s in I;
per cases;
suppose
s = i;
hence thesis by A5,A7;
end;
suppose
s <> i;
then not s in dom (i .--> x) by TARSKI:def 1;
then X.s = K.s by FUNCT_4:11;
hence thesis by A4,A8;
end;
end;
then
A9: F..X = G..X by A1;
thus f.x = (F..X).i by A2,A7,PRALG_1:def 20
.= g.x by A2,A7,A9,PRALG_1:def 20;
end;
hence F.i = G.i by FUNCT_2:12;
end;
hence thesis;
end;
registration
let I, M;
cluster empty-yielding finite-yielding for Element of bool M;
existence
proof
EmptyMS I c= M by MBOOLEAN:5;
then EmptyMS I in bool M by MBOOLEAN:1;
then reconsider a = EmptyMS I as Element of bool M by MSSUBFAM:11;
take a;
thus thesis;
end;
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; :: redefines .. (PRALG_1, definition)
coherence by Lm1;
end;
definition
let I, M;
let IT be MSSetOp of M;
attr IT is reflexive means
:Def1:
for X being Element of bool M holds X c= IT..X;
attr IT is monotonic means
for X, Y being Element of bool M st X c= Y holds IT..X c= IT..Y;
attr IT is idempotent means
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;
theorem Th8:
for M being non-empty ManySortedSet of I for X being Element of M
holds X = (id M)..X
proof
let M be non-empty ManySortedSet of I;
let X be Element of M;
set F = id M;
now
let i be object;
reconsider g = F.i as Function;
assume
A2: i in I;
then X.i is Element of M.i & F.i = id (M.i)
by MSUALG_3:def 1,PBOOLE:def 14;
then g.(X.i) = X.i;
hence X.i = (F..X).i by A2,PRALG_1:def 20;
end;
hence thesis;
end;
theorem Th9:
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
proof
let M be non-empty ManySortedSet of I;
let X, Y be Element of M such that
A1: X c= Y;
(id M)..X = X by Th8;
hence thesis by A1,Th8;
end;
theorem Th10:
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)
proof
let M be non-empty ManySortedSet of I;
let X, Y be Element of M;
set F = id M;
assume X (\/) Y is Element of M;
hence F..(X (\/) Y) = X (\/) Y by Th8
.= (F..X) (\/) Y by Th8
.= (F..X) (\/) (F..Y) by Th8;
end;
theorem
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
proof
let X be Element of bool M, i, x be set such that
A1: i in I and
A2: x in ((id (bool M))..X).i;
A3: x in X.i by A2,Th8;
set Y = (I --> {}) +* (i.-->{x});
dom Y = I by A1,PZFMISC1:1;
then reconsider Y as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18;
A4: dom (i .--> {x}) = {i};
i in {i} by TARSKI:def 1;
then
A5: Y.i = (i .--> {x}).i by A4,FUNCT_4:13
.= {x} by FUNCOP_1:72;
X in bool M by MSSUBFAM:12;
then X c= M by MBOOLEAN:18;
then
A6: X.i c= M.i by A1;
Y is Element of bool M
proof
let j be object such that
A7: j in I;
now
per cases;
case
A8: j = i;
then {x} c= M.j by A3,A6,ZFMISC_1:31;
hence thesis by A5,A7,A8,MBOOLEAN:def 1;
end;
case
j <> i;
then not j in dom (i .--> {x}) by TARSKI:def 1;
then Y.j = (I --> {}).j by FUNCT_4:11;
then Y.j = {};
then Y.j c= M.j;
hence thesis by A7,MBOOLEAN:def 1;
end;
end;
hence thesis;
end;
then reconsider Y as Element of bool M;
Y is finite-yielding
proof
let j be object such that
j in I;
now
per cases;
case
j = i;
hence thesis by A5;
end;
case
j <> i;
then not j in dom (i .--> {x}) by TARSKI:def 1;
then Y.j = (I --> {}).j by FUNCT_4:11;
hence thesis;
end;
end;
hence thesis;
end;
then reconsider Y as finite-yielding Element of bool M;
take Y;
thus Y c= X
proof
let j be object such that
j in I;
now
per cases;
case
j = i;
hence thesis by A3,A5,ZFMISC_1:31;
end;
case
j <> i;
then not j in dom (i .--> {x}) by TARSKI:def 1;
then Y.j = (I --> {}).j by FUNCT_4:11;
then Y.j = {};
hence thesis;
end;
end;
hence thesis;
end;
x in Y.i by A5,TARSKI:def 1;
hence thesis by Th8;
end;
registration
let I, M;
cluster reflexive monotonic idempotent topological for MSSetOp of M;
existence
proof
reconsider F = id (bool M) as MSSetOp of M;
take F;
thus F is reflexive
by Th8;
thus F is monotonic
by Th9;
thus F is idempotent
by Th8;
thus F is topological
proof
let X, Y be Element of bool M;
Y in bool M by MSSUBFAM:12;
then
A1: Y c= M by MBOOLEAN:1;
X in bool M by MSSUBFAM:12;
then X c= M by MBOOLEAN:1;
then X (\/) Y c= M by A1,PBOOLE:16;
then X (\/) Y in bool M by MBOOLEAN:1;
then X (\/) Y is Element of bool M by MSSUBFAM:11;
hence thesis by Th10;
end;
end;
end;
theorem
id (bool A) is reflexive MSSetOp of A
proof
reconsider a = id (bool A) as MSSetOp of A;
a is reflexive
by Th8;
hence thesis;
end;
theorem
id (bool A) is monotonic MSSetOp of A
proof
reconsider a = id (bool A) as MSSetOp of A;
a is monotonic
by Th9;
hence thesis;
end;
theorem
id (bool A) is idempotent MSSetOp of A
proof
reconsider a = id (bool A) as MSSetOp of A;
a is idempotent
by Th8;
hence thesis;
end;
theorem
id (bool A) is topological MSSetOp of A
proof
reconsider a = id (bool A) as MSSetOp of A;
a is topological
proof
let X, Y be Element of bool A;
Y in bool A by MSSUBFAM:12;
then
A1: Y c= A by MBOOLEAN:1;
X in bool A by MSSUBFAM:12;
then X c= A by MBOOLEAN:1;
then X (\/) Y c= A by A1,PBOOLE:16;
then X (\/) Y in bool A by MBOOLEAN:1;
then X (\/) Y is Element of bool A by MSSUBFAM:11;
hence thesis by Th10;
end;
hence thesis;
end;
reserve P, R for MSSetOp of M,
E, T for Element of bool M;
theorem
E = M & P is reflexive implies E = P..E
proof
assume
A1: E = M;
assume P is reflexive;
then
A2: E c= P..E;
P..E in bool E by A1,MSSUBFAM:12;
then P..E c= E by MBOOLEAN:18;
hence thesis by A2,PBOOLE:146;
end;
theorem
(P is reflexive & for X being Element of bool M holds P..X c= X)
implies P is idempotent
proof
assume that
A1: P is reflexive and
A2: for X being Element of bool M holds P..X c= X;
let X be Element of bool M;
A3: P..X c= P..(P..X) by A1;
P..(P..X) c= P..X by A2;
hence thesis by A3,PBOOLE:146;
end;
theorem
P is monotonic implies P..(E (/\) T) c= P..E (/\) P..T
proof
assume
A1: P is monotonic;
E in bool M by MSSUBFAM:12;
then E c= M by MBOOLEAN:1;
then E (/\) T c= M by MBOOLEAN:14;
then E (/\) T in bool M by MBOOLEAN:1;
then
A2: E (/\) T is Element of bool M by MSSUBFAM:11;
E (/\) T c= T by PBOOLE:15;
then
A3: P..(E (/\) T) c= P..T by A1,A2;
E (/\) T c= E by PBOOLE:15;
then P..(E (/\) T) c= P..E by A1,A2;
hence thesis by A3,PBOOLE:17;
end;
registration
let I, M;
cluster topological -> monotonic for MSSetOp of M;
coherence
proof
let P be MSSetOp of M such that
A1: P is topological;
let X, Y be Element of bool M such that
A2: X c= Y;
P..X (\/) P..Y = P..(X (\/) Y) by A1
.= P..Y by A2,PBOOLE:22;
hence thesis by PBOOLE:26;
end;
end;
theorem
P is topological implies P..E (\) P..T c= P..(E (\) T)
proof
E in bool M by MSSUBFAM:12;
then E c= M by MBOOLEAN:1;
then E(\)T c= M by MBOOLEAN:15;
then E(\)T in bool M by MBOOLEAN:1;
then
A1: E(\)T is Element of bool M by MSSUBFAM:11;
assume
A2: P is topological;
then P..E (\/) P..T = P..(E (\/) T)
.= P..((E(\)T) (\/) T) by PBOOLE:67
.= (P..(E(\)T)) (\/) (P..T) by A1,A2;
then P..E c= P..(E(\)T) (\/) P..T by PBOOLE:14;
then P..E (\) P..T c= (P..(E(\)T) (\/) P..T) (\) P..T by PBOOLE:53;
then
A3: P..E (\) P..T c= P..(E(\)T) (\) P..T by PBOOLE:75;
P..(E(\)T) (\) P..T c= P..(E(\)T) by PBOOLE:56;
hence thesis by A3,PBOOLE:13;
end;
definition
let I, M, R, P;
redefine func P ** R -> MSSetOp of M; :: redefines ** (PBOOLE, definition)
coherence
proof
P ** R is ManySortedFunction of bool M, bool M;
hence thesis;
end;
end;
theorem
P is reflexive & R is reflexive implies P ** R is reflexive
proof
assume
A1: P is reflexive & R is reflexive;
let X be Element of bool M;
X c= R..X & R..X c= P..(R..X) by A1;
then doms R = bool M & X c= P..(R..X) by MSSUBFAM:17,PBOOLE:13;
hence thesis by Th4,MSSUBFAM:12;
end;
theorem
P is monotonic & R is monotonic implies P ** R is monotonic
proof
assume that
A1: P is monotonic and
A2: R is monotonic;
A3: doms R = bool M by MSSUBFAM:17;
let X, Y be Element of bool M;
assume X c= Y;
then R..X c= R..Y by A2;
then P..(R..X) c= P..(R..Y) by A1;
then P..(R..X) c= (P**R)..Y by A3,Th4,MSSUBFAM:12;
hence thesis by A3,Th4,MSSUBFAM:12;
end;
theorem
P is idempotent & R is idempotent & P**R = R**P implies P ** R is idempotent
proof
assume that
A1: P is idempotent and
A2: R is idempotent and
A3: P**R = R**P;
let X be Element of bool M;
A4: doms P = bool M by MSSUBFAM:17;
A5: doms R = bool M by MSSUBFAM:17;
hence (P**R)..X = P..(R..X) by Th4,MSSUBFAM:12
.= P..(R..(R..X)) by A2
.= P..(P..(R..(R..X))) by A1
.= P..((R**P)..(R..X)) by A3,A5,Th4,MSSUBFAM:12
.= P..(R..(P..(R..X))) by A4,Th4,MSSUBFAM:12
.= P..(R..((P**R)..X)) by A5,Th4,MSSUBFAM:12
.= (P**R)..((P**R)..X) by A5,Th4,MSSUBFAM:12;
end;
theorem
P is topological & R is topological implies P ** R is topological
proof
assume that
A1: P is topological and
A2: R is topological;
let X, Y be Element of bool M;
A3: doms R = bool M by MSSUBFAM:17;
Y in bool M by MSSUBFAM:12;
then
A4: Y c= M by MBOOLEAN:1;
X in bool M by MSSUBFAM:12;
then X c= M by MBOOLEAN:1;
then X (\/) Y c= M by A4,PBOOLE:16;
then X (\/) Y in doms R by A3,MBOOLEAN:1;
hence (P**R)..(X (\/) Y) = P..(R..(X (\/) Y)) by Th4
.= P..(R..X (\/) R..Y) by A2
.= P..(R..X) (\/) P..(R..Y) by A1
.= (P**R)..X (\/) P..(R..Y) by A3,Th4,MSSUBFAM:12
.= (P**R)..X (\/) (P**R)..Y by A3,Th4,MSSUBFAM:12;
end;
Lm2: now
let I, M, i;
let a be ManySortedSet of I, b be Element of bool (M.i) such that
A1: a = EmptyMS I +* (i .--> b);
A2: dom (i .--> b) = {i};
EmptyMS I c= M by MBOOLEAN:5;
then
A3: EmptyMS I in bool M by MBOOLEAN:1;
thus a in bool M
proof
let j be object such that
A4: j in I;
i in {i} by TARSKI:def 1;
then
A5: a.i = (i .--> b).i by A1,A2,FUNCT_4:13
.= b by FUNCOP_1:72;
now
per cases;
case
A6: j = i;
then b in bool (M.j);
hence thesis by A4,A5,A6,MBOOLEAN:def 1;
end;
case
j <> i;
then not j in dom (i .--> b) by TARSKI:def 1;
then a.j = EmptyMS I.j by A1,FUNCT_4:11;
hence thesis by A3,A4;
end;
end;
hence thesis;
end;
end;
theorem Th24:
P is reflexive & i in I & f = P.i implies
for x being Element of bool (M.i) holds x c= f.x
proof
assume that
A1: P is reflexive and
A2: i in I and
A3: f = P.i;
let x be Element of bool (M.i);
dom (EmptyMS I +* (i .--> x)) = I by A2,PZFMISC1:1;
then reconsider X = EmptyMS I +* (i .--> x) as ManySortedSet of I
by PARTFUN1:def 2,RELAT_1:def 18;
X is Element of bool M by Lm2,MSSUBFAM:11;
then X c= P..X by A1; then
A4: X.i c= (P..X).i by A2;
dom (i .--> x) = {i} & i in {i} by TARSKI:def 1; then
A5: X.i = (i .--> x).i by FUNCT_4:13
.= x by FUNCOP_1:72;
i in dom X & i in dom P by A2,PARTFUN1:def 2; then
i in dom P /\ dom X by XBOOLE_0:def 4; then
i in dom (P..X) by PRALG_1:def 19;
hence thesis by A3,A5,A4,PRALG_1:def 19;
end;
theorem Th25:
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
proof
assume that
A1: P is monotonic and
A2: i in I and
A3: f = P.i;
let x, y be Element of bool (M.i) such that
A4: x c= y;
dom (EmptyMS I +* (i .--> y)) = I by A2,PZFMISC1:1;
then reconsider Y = EmptyMS I +* (i .--> y) as ManySortedSet of I
by PARTFUN1:def 2,RELAT_1:def 18;
dom (EmptyMS I +* (i .--> x)) = I by A2,PZFMISC1:1;
then reconsider X = EmptyMS I +* (i .--> x) as ManySortedSet of I
by PARTFUN1:def 2,RELAT_1:def 18;
A5: i in {i} by TARSKI:def 1;
dom (i .--> y) = {i}; then
A6: Y.i = (i .--> y).i by A5,FUNCT_4:13
.= y by FUNCOP_1:72;
dom (i .--> x) = {i}; then
A8: X.i = (i .--> x).i by A5,FUNCT_4:13
.= x by FUNCOP_1:72;
A9: X c= Y
proof
let s be object such that
s in I;
per cases;
suppose
s = i;
hence thesis by A4,A8,A6;
end;
suppose s <> i;
then not s in dom (i .--> x) by TARSKI:def 1; then
A10: X.s = EmptyMS I.s by FUNCT_4:11;
thus thesis by A10;
end;
end;
A11: i in dom P by A2,PARTFUN1:def 2;
X is Element of bool M & Y is Element of bool M by Lm2,MSSUBFAM:11;
then P..X c= P..Y by A1,A9;
then A12: (P..X).i c= (P..Y).i by A2;
i in dom Y by A2,PARTFUN1:def 2; then
i in dom P /\ dom Y by A11,XBOOLE_0:def 4; then
i in dom (P..Y) by PRALG_1:def 19; then
W: (P..Y).i = f.(Y.i) by PRALG_1:def 19,A3;
dom X = I by PARTFUN1:def 2; then
i in dom X by A2; then
i in dom P /\ dom X by A11,XBOOLE_0:def 4; then
i in dom (P..X) by PRALG_1:def 19; then
f.(X.i) = (P..X).i by A3,PRALG_1:def 19;
then f.(X.i) c= (P..Y).i by A12;
hence thesis by A8,A6,W;
end;
theorem Th26:
P is idempotent & i in I & f = P.i implies
for x being Element of bool (M.i) holds f.x = f.(f.x)
proof
assume that
A1: P is idempotent and
A2: i in I and
A3: f = P.i;
A4: i in dom P by A2,PARTFUN1:def 2;
let x be Element of bool (M.i);
dom (EmptyMS I +* (i .--> x)) = I by A2,PZFMISC1:1;
then reconsider X = EmptyMS I +* (i .--> x) as ManySortedSet of I
by PARTFUN1:def 2,RELAT_1:def 18;
A5: X is Element of bool M by Lm2,MSSUBFAM:11;
dom (i .--> x) = {i} & i in {i} by TARSKI:def 1; then
A6: X.i = (i .--> x).i by FUNCT_4:13
.= x by FUNCOP_1:72;
i in dom X by A2,PARTFUN1:def 2; then
i in dom P /\ dom X by A4,XBOOLE_0:def 4; then
A7: i in dom (P..X) by PRALG_1:def 19;
i in dom P by A2,PARTFUN1:def 2; then
i in dom P /\ dom (P..X) by A7,XBOOLE_0:def 4; then
B1: i in dom (P..(P..X)) by PRALG_1:def 19;
thus f.x = (P..X).i by A6,A3,PRALG_1:def 19,A7
.= (P..(P..X)).i by A1,A5
.= f.((P..X).i) by B1,A3,PRALG_1:def 19
.= f.(f.x) by A3,A6,A7,PRALG_1:def 19;
end;
theorem
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)
proof
assume that
A1: P is topological and
A2: i in I and
A3: f = P.i;
A4: i in dom P by A2,PARTFUN1:def 2;
let x, y be Element of bool (M.i);
dom (EmptyMS I +* (i .--> y)) = I by A2,PZFMISC1:1;
then reconsider Y = EmptyMS I +* (i .--> y) as ManySortedSet of I
by PARTFUN1:def 2,RELAT_1:def 18;
dom (EmptyMS I +* (i .--> x)) = I by A2,PZFMISC1:1;
then reconsider X = EmptyMS I +* (i .--> x) as ManySortedSet of I
by PARTFUN1:def 2,RELAT_1:def 18;
A5: i in {i} by TARSKI:def 1;
dom (i .--> y) = {i}; then
A6: Y.i = (i .--> y).i by A5,FUNCT_4:13
.= y by FUNCOP_1:72;
A7: X is Element of bool M & Y is Element of bool M by Lm2,MSSUBFAM:11;
i in dom (X (\/) Y) by A2,PARTFUN1:def 2; then
i in (dom P) /\ dom (X (\/) Y) by A4,XBOOLE_0:def 4; then
B1: i in dom (P..(X (\/) Y)) by PRALG_1:def 19;
i in dom X by A2,PARTFUN1:def 2; then
i in dom P /\ dom X by XBOOLE_0:def 4,A4; then
B2: i in dom (P..X) by PRALG_1:def 19;
i in dom Y by A2,PARTFUN1:def 2; then
i in dom P /\ dom Y by XBOOLE_0:def 4,A4; then
B3: i in dom (P..Y) by PRALG_1:def 19;
dom (i .--> x) = {i};
then
A8: X.i = (i .--> x).i by A5,FUNCT_4:13
.= x by FUNCOP_1:72;
hence f.(x \/ y) = f.((X (\/) Y).i) by A2,A6,PBOOLE:def 4
.= (P..(X (\/) Y)).i by A3,PRALG_1:def 19,B1
.= ((P..X) (\/) (P..Y)).i by A1,A7
.= (P..X).i \/ (P..Y).i by A2,PBOOLE:def 4
.= f.(X.i) \/ (P..Y).i by A3,PRALG_1:def 19,B2
.= (f.x) \/ (f.y) by A3,A8,A6,PRALG_1:def 19,B3;
end;
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
:Def5:
the Family of IT is additive;
attr IT is absolutely-additive means
:Def6:
the Family of IT is absolutely-additive;
attr IT is multiplicative means
:Def7:
the Family of IT is multiplicative;
attr IT is absolutely-multiplicative means
:Def8:
the Family of IT is absolutely-multiplicative;
attr IT is properly-upper-bound means
:Def9:
the Family of IT is properly-upper-bound;
attr IT is properly-lower-bound means
:Def10:
the Family of IT is properly-lower-bound;
end;
definition
let S, MS;
func MSFull MS -> MSClosureStr over S equals
MSClosureStr (#the Sorts of MS,
bool the Sorts of MS#);
correctness;
end;
registration
let S, MS;
cluster MSFull 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 MSFull 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 MSClosureStr over S;
existence
proof
set a = the non-empty many-sorted over S;
take MSFull a;
thus thesis;
end;
end;
registration
let S;
let CS be additive MSClosureStr over S;
cluster the Family of CS -> additive;
coherence by Def5;
end;
registration
let S;
let CS be absolutely-additive MSClosureStr over S;
cluster the Family of CS -> absolutely-additive;
coherence by Def6;
end;
registration
let S;
let CS be multiplicative MSClosureStr over S;
cluster the Family of CS -> multiplicative;
coherence by Def7;
end;
registration
let S;
let CS be absolutely-multiplicative MSClosureStr over S;
cluster the Family of CS -> absolutely-multiplicative;
coherence by Def8;
end;
registration
let S;
let CS be properly-upper-bound MSClosureStr over S;
cluster the Family of CS -> properly-upper-bound;
coherence by Def9;
end;
registration
let S;
let CS be properly-lower-bound MSClosureStr over S;
cluster the Family of CS -> properly-lower-bound;
coherence by Def10;
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;
coherence;
end;
registration
let S, MS;
let F be additive MSSubsetFamily of the Sorts of MS;
cluster MSClosureStr (#the Sorts of MS, F#) -> additive;
coherence;
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;
coherence;
end;
registration
let S, MS;
let F be multiplicative MSSubsetFamily of the Sorts of MS;
cluster MSClosureStr (#the Sorts of MS, F#) -> multiplicative;
coherence;
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;
coherence;
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;
coherence;
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;
coherence;
end;
registration
let S;
cluster absolutely-additive -> additive for MSClosureStr over S;
coherence;
end;
registration
let S;
cluster absolutely-multiplicative -> multiplicative for MSClosureStr over S;
coherence;
end;
registration
let S;
cluster absolutely-multiplicative -> properly-upper-bound for
MSClosureStr over
S;
coherence;
end;
registration
let S;
cluster absolutely-additive -> properly-lower-bound for MSClosureStr over S;
coherence;
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
:Def12:
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;
existence
proof
defpred P[object,object] means
ex D2 being set st D2 = $2 &
for x being object holds x in D2 iff x in M.$1 & ex f being
Function st f = F.$1 & x in dom f & f.x = x;
A1: now
let i be object such that
i in I;
defpred R[object] means
ex f being Function st f = F.i & $1 in dom f & f.$1
= $1;
consider j being set such that
A2: for x being object holds x in j iff x in M.i & R[ x ]
from XBOOLE_0:sch 1;
reconsider j as object;
take j;
thus P[i,j] by A2;
end;
consider A being ManySortedSet of I such that
A3: for i being object st i in I holds P[i,A.i] from PBOOLE:sch 3(A1);
A is ManySortedSubset of M
proof
let i be object such that
A4: i in I;
let x be object;
assume
A5: x in A.i;
P[i,A.i] by A3,A4;
hence thesis by A5;
end;
then reconsider A as ManySortedSubset of M;
take A;
thus for i being object
st i in I holds x in A.i iff ex f being Function st f = F.i & x
in dom f & f.x = x
proof
let i be object;
assume
A6: i in I;
then P[i,A.i] by A3;
hence x in A.i implies ex f being Function st f = F.i & x in dom f & f.x
= x;
given f being Function such that
A7: f = F.i and
A8: x in dom f & f.x = x;
doms F = M by MSSUBFAM:17;
then
A9: dom f = M.i by A6,A7,MSSUBFAM:14;
P[i,A.i] by A3,A6;
hence thesis by A7,A8,A9;
end;
end;
uniqueness
proof
let A, B be ManySortedSubset of M such that
A10: for i being object
st i in I holds x in A.i iff ex f being Function st f = F.i
& x in dom f & f.x = x and
A11: for i being object
st i in I holds x in B.i iff ex f being Function st f = F.i
& x in dom f & f.x = x;
now
let i be object such that
A12: i in I;
thus A.i = B.i
proof
thus A.i c= B.i
proof
let x be object;
assume x in A.i;
then ex f being Function st f = F.i & x in dom f & f.x = x by A10,A12
;
hence thesis by A11,A12;
end;
let x be object;
assume x in B.i;
then ex f being Function st f = F.i & x in dom f & f.x = x by A11,A12;
hence thesis by A10,A12;
end;
end;
hence A = B;
end;
end;
registration
let I;
let M be empty-yielding ManySortedSet of I;
let F be ManySortedFunction of M, M;
cluster MSFixPoints F -> empty-yielding;
coherence
proof
let i be object such that
A1: i in I;
assume (MSFixPoints F).i is non empty;
then consider x being object such that
A2: x in (MSFixPoints F).i;
consider f being Function such that
A3: f = F.i and
A4: x in dom f and
f.x = x by A1,A2,Def12;
M.i = {};
then f is Function of {}, {} by A1,A3,PBOOLE:def 15;
hence contradiction by A4;
end;
end;
theorem Th28:
for F being ManySortedFunction of M, M holds A in M & F..A = A
iff A in MSFixPoints F
proof
let F be ManySortedFunction of M, M;
thus A in M & F..A = A implies A in MSFixPoints F
proof
assume that
A1: A in M and
A2: F..A = A;
let i be object;
assume
A3: i in I;
then reconsider f = F.i as Function of M.i, M.i by PBOOLE:def 15;
i in dom (F..A) by A3,PARTFUN1:def 2; then
A4: f.(A.i) = A.i by A2,PRALG_1:def 19;
M = doms F by MSSUBFAM:17;
then M.i = dom f by A3,MSSUBFAM:14;
then A.i in dom f by A1,A3;
hence thesis by A3,A4,Def12;
end;
assume
A5: A in MSFixPoints F;
thus A in M
proof
let i be object;
A6: M = doms F by MSSUBFAM:17;
assume
A7: i in I;
then A.i in (MSFixPoints F).i by A5;
then ex f being Function st f = F.i & A.i in dom f & f.(A.i) = A.i by A7
,Def12;
hence thesis by A7,A6,MSSUBFAM:14;
end;
now
let i be object;
assume
A8: i in I;
then A.i in (MSFixPoints F).i by A5; then
A9: ex f being Function st f = F.i & A.i in dom f & f.(A.i) = A.i by A8,Def12;
i in dom A & i in dom F by A8,PARTFUN1:def 2; then
i in dom F /\ dom A by XBOOLE_0:def 4; then
i in dom (F..A) by PRALG_1:def 19;
hence (F..A).i = A.i by A9,PRALG_1:def 19;
end;
hence thesis;
end;
theorem
MSFixPoints id A = A
proof
now
let i be object such that
A1: i in I;
thus (MSFixPoints id A).i = A.i
proof
thus (MSFixPoints id A).i c= A.i
proof
let x be object;
assume x in (MSFixPoints id A).i;
then consider f being Function such that
A2: f = (id A).i and
A3: x in dom f and
f.x = x by A1,Def12;
f is Function of A.i, A.i by A1,A2,PBOOLE:def 15;
hence thesis by A3,FUNCT_2:52;
end;
reconsider f = (id A).i as Function of A.i, A.i by A1,PBOOLE:def 15;
let x be object such that
A4: x in A.i;
A5: x in dom f by A4,FUNCT_2:52;
f = id (A.i) by A1,MSUALG_3:def 1;
then f.x = x by A4,FUNCT_1:18;
hence thesis by A1,A5,Def12;
end;
end;
hence thesis;
end;
theorem Th30:
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
proof
let A be ManySortedSet of the carrier of S, J be reflexive monotonic MSSetOp
of A, D be MSSubsetFamily of A such that
A1: D = MSFixPoints J;
D is absolutely-multiplicative
proof
let F be MSSubsetFamily of A such that
A2: F c= D;
A3: J..(meet F) c= meet F
proof
let i be object;
assume
A4: i in the carrier of S;
then reconsider j = J.i as Function of (bool A).i, (bool A).i
by PBOOLE:def 15;
A5: i in dom J by A4,PARTFUN1:def 2;
i in dom meet F by A4,PARTFUN1:def 2; then
i in dom J /\ dom meet F by A5,XBOOLE_0:def 4; then
a5: i in dom (J..meet F) by PRALG_1:def 19;
consider Q being Subset-Family of A.i such that
A6: Q = F.i and
A7: (meet F).i = Intersect Q by A4,MSSUBFAM:def 1;
A8: now
let x such that
A9: x in Q;
Q c= D.i by A2,A4,A6; then
ex jj being Function st jj = J.i & x in dom jj & jj.x = x
by A1,A4,A9,Def12;
hence j.(Intersect Q) c= x by A4,A9,Th25,MSSUBFAM:2;
end;
(bool A).i = bool (A.i) by A4,MBOOLEAN:def 1;
then j.(Intersect Q) in bool (A.i) by FUNCT_2:5;
then j.(Intersect Q) c= Intersect Q by A8,MSSUBFAM:4;
hence thesis by A7,PRALG_1:def 19,a5;
end;
meet F c= A by PBOOLE:def 18;
then
A10: meet F in bool A by MBOOLEAN:18;
then meet F is Element of bool A by MSSUBFAM:11;
then meet F c= J..(meet F) by Def1;
then J..(meet F) = meet F by A3,PBOOLE:146;
hence thesis by A1,A10,Th28;
end;
hence thesis;
end;
theorem Th31:
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
proof
let D be properly-upper-bound MSSubsetFamily of M, X be Element of bool M;
defpred P[object,object] means
ex D2 being set st D2 = $2 & X.$1 c= D2;
consider SF being ManySortedSet of I such that
A1: for i being object st i in I
for e being object holds e in SF.i iff e in D.i & P[i,e]
from PBOOLE:sch 2;
A2: D c= bool M by PBOOLE:def 18;
SF is ManySortedSubset of bool M
proof
let i be object;
assume
A3: i in I;
then D.i c= (bool M).i by A2; then
A4: D.i c= bool (M.i) by A3,MBOOLEAN:def 1;
SF.i c= bool (M.i)
proof
let x be object;
assume x in SF.i;
then x in D.i by A1,A3;
hence thesis by A4;
end;
hence SF.i c= (bool M).i by A3,MBOOLEAN:def 1;
end;
then reconsider SF as ManySortedSubset of bool M;
reconsider SF as MSSubsetFamily of M;
SF is non-empty
proof
let i be object such that
A5: i in I;
M in D by MSSUBFAM:def 6;
then
A6: M.i in D.i by A5;
X in bool M by MSSUBFAM:12;
then X c= M by MBOOLEAN:18;
then X.i c= M.i by A5;
hence thesis by A1,A5,A6;
end;
then reconsider SF as non-empty MSSubsetFamily of M;
take SF;
let Y be ManySortedSet of I;
thus Y in SF implies Y in D & X c= Y
proof
assume
A7: Y in SF;
thus Y in D
proof
let i be object;
assume
A8: i in I;
then Y.i in SF.i by A7;
hence thesis by A1,A8;
end;
thus X c= Y
proof
let i be object;
assume
A9: i in I;
then Y.i in SF.i by A7;
then Y.i in D.i & P[i,Y.i] by A1,A9;
hence thesis;
end;
end;
assume
A10: Y in D & X c= Y;
let i be object;
assume
A11: i in I;
then Y.i in D.i & X.i c= Y.i by A10;
hence thesis by A1,A11;
end;
theorem Th32:
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 }
proof
let D be properly-upper-bound MSSubsetFamily of M, X be Element of bool M,
SF be non-empty MSSubsetFamily of M such that
A1: for Y being ManySortedSet of I holds Y in SF iff Y in D & X c= Y;
let i be set, Di be non empty set such that
A2: i in I and
A3: Di = D.i;
thus SF.i c= { z where z is Element of Di : X.i c= z }
proof
consider K be ManySortedSet of I such that
A4: K in SF by PBOOLE:134;
let x be object such that
A5: x in SF.i;
dom (K +* (i .--> x)) = I by A2,PZFMISC1:1;
then reconsider L = K +* (i .--> x) as ManySortedSet of I by PARTFUN1:def 2
,RELAT_1:def 18;
A6: dom (i .--> x) = {i};
i in {i} by TARSKI:def 1;
then
A7: L.i = (i .--> x).i by A6,FUNCT_4:13
.= x by FUNCOP_1:72;
A8: L in SF
proof
let s be object such that
A9: s in I;
per cases;
suppose
s = i;
hence thesis by A5,A7;
end;
suppose
s <> i;
then not s in dom (i .--> x) by TARSKI:def 1;
then L.s = K.s by FUNCT_4:11;
hence thesis by A4,A9;
end;
end;
then X c= L by A1;
then
A10: X.i c= L.i by A2;
L in D by A1,A8;
then L.i in D.i by A2;
hence thesis by A3,A7,A10;
end;
let x be object;
assume x in { z where z is Element of Di : X.i c= z };
then consider g be Element of Di such that
A11: g = x and
A12: X.i c= g;
dom (M +* (i .--> g)) = I by A2,PZFMISC1:1;
then reconsider L1 = M +* (i .--> g) as ManySortedSet of I by PARTFUN1:def 2
,RELAT_1:def 18;
A13: dom (i .--> g) = {i};
i in {i} by TARSKI:def 1;
then
A14: L1.i = (i .--> g).i by A13,FUNCT_4:13
.= g by FUNCOP_1:72;
A15: X c= L1
proof
let s be object such that
A16: s in I;
per cases;
suppose
s = i;
hence thesis by A12,A14;
end;
suppose
A17: s <> i;
X in bool M by MSSUBFAM:12;
then
A18: X c= M by MBOOLEAN:18;
not s in dom (i .--> g) by A17,TARSKI:def 1;
then L1.s = M.s by FUNCT_4:11;
hence thesis by A16,A18;
end;
end;
A19: M in D by MSSUBFAM:def 6;
L1 in D
proof
let s be object such that
A20: s in I;
per cases;
suppose
s = i;
hence thesis by A3,A14;
end;
suppose
s <> i;
then not s in dom (i .--> g) by TARSKI:def 1;
then L1.s = M.s by FUNCT_4:11;
hence thesis by A19,A20;
end;
end;
then L1 in SF by A1,A15;
hence thesis by A2,A11,A14;
end;
theorem Th33:
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
proof
let D be properly-upper-bound MSSubsetFamily of M;
set G = bool M;
defpred P[object,object,object] means
ex D2 being set st D2 = $2 &
for sf being Subset-Family of M.$3 for Fi being
non empty set st Fi = D.$3 & sf = { z where z is Element of Fi : D2 c= z }
holds $1 = Intersect sf;
A1: now
consider K being ManySortedSet of I such that
A2: K in G by PBOOLE:134;
let i be object such that
A3: i in I;
reconsider b = (bool M).i as non empty set by A3;
let x be object such that
A4: x in G.i;
dom (K +* (i .--> x)) = I by A3,PZFMISC1:1;
then reconsider X = K +* (i .--> x) as ManySortedSet of I by PARTFUN1:def 2
,RELAT_1:def 18;
A5: dom (i .--> x) = {i};
i in {i} by TARSKI:def 1;
then
A6: X.i = (i .--> x).i by A5,FUNCT_4:13
.= x by FUNCOP_1:72;
A7: X is Element of bool M
proof
let s be object such that
A8: s in I;
per cases;
suppose
s = i;
hence thesis by A4,A6;
end;
suppose
s <> i;
then not s in dom (i .--> x) by TARSKI:def 1;
then X.s = K.s by FUNCT_4:11;
hence thesis by A2,A8;
end;
end;
then consider SF being non-empty MSSubsetFamily of M such that
A9: for Y being ManySortedSet of I holds Y in SF iff Y in D & X c= Y by Th31;
reconsider sf = SF.i as Subset-Family of M.i by A3,MSSUBFAM:32;
reconsider q = Intersect sf as Element of b by A3,MBOOLEAN:def 1;
reconsider s = b --> q as Function of b, b;
reconsider y = s.x as object;
take y;
Intersect sf in bool (M.i);
then Intersect sf in b by A3,MBOOLEAN:def 1;
hence y in G.i by A4,FUNCOP_1:7;
thus P[y,x,i]
proof
reconsider Di = D.i as non empty set by A3;
A10: SF.i = { z where z is Element of Di : X.i c= z } by A3,A7,A9,Th32;
reconsider xx=x as set by TARSKI:1;
take xx;
thus xx = x;
let sf1 be Subset-Family of M.i, Fi be non empty set;
assume Fi = D.i & sf1 = { z where z is Element of Fi : xx c= z };
hence thesis by A4,A6,A10,FUNCOP_1:7;
end;
end;
consider J being ManySortedFunction of G, G such that
A11: for i be object st i in I
ex f be Function of G.i, G.i st f = J.i &
for x be object st x in G.i holds P[f.x,x,i] from MSSUBFAM:sch 1(A1);
reconsider J as MSSetOp of M;
take J;
let X be Element of bool M, SF be non-empty MSSubsetFamily of M such that
A12: for Y being ManySortedSet of I holds Y in SF iff Y in D & X c= Y;
now
let i be object;
assume
A13: i in I;
then consider Q being Subset-Family of (M.i) such that
A14: Q = SF.i and
A15: (meet SF).i = Intersect Q by MSSUBFAM:def 1;
reconsider Fi = D.i as non empty set by A13;
A16: Q = { z where z is Element of Fi : X.i c= z } by A12,A13,A14,Th32;
X in G by MSSUBFAM:12;
then
A17: X.i in G.i by A13;
consider f being Function of G.i, G.i such that
A18: f = J.i and
A19: for x being object st x in G.i holds P[f.x,x,i] by A11,A13;
A20: P[f.(X.i),X.i,i] by A19,A17;
thus (J..X).i = f.(X.i) by A13,A18,PRALG_1:def 20
.= (meet SF).i by A15,A16,A20;
end;
hence thesis;
end;
theorem Th34:
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
proof
let D be properly-upper-bound MSSubsetFamily of M, A be Element of bool M, J
be MSSetOp of M such that
A1: A in D and
A2: 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;
consider SF being non-empty MSSubsetFamily of M such that
A3: for Y being ManySortedSet of I holds Y in SF iff Y in D & A c= Y by Th31;
A in SF by A1,A3;
then meet SF c= A by MSSUBFAM:43;
then
A4: J..A c= A by A2,A3;
A5: for Z1 being ManySortedSet of I st Z1 in SF holds A c= Z1 by A3;
J..A = meet SF by A2,A3;
then A c= J..A by A5,MSSUBFAM:45;
hence J..A = A by A4,PBOOLE:146;
end;
theorem
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
proof
let D be absolutely-multiplicative MSSubsetFamily of M, A be Element of bool
M, J be MSSetOp of M such that
A1: J..A = A and
A2: 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;
defpred P[ManySortedSet of I] means A c= $1;
consider SF being non-empty MSSubsetFamily of M such that
A3: for Y being ManySortedSet of I holds Y in SF iff Y in D & A c= Y by Th31;
A4: (for Y being ManySortedSet of I holds Y in SF iff Y in D & P[Y]) implies
SF c= D from MSSUBSET;
J..A = meet SF by A2,A3;
hence thesis by A1,A3,A4,MSSUBFAM:def 5;
end;
theorem Th36:
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
proof
let D be properly-upper-bound MSSubsetFamily of M, J be MSSetOp of M such
that
A1: 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;
thus J is reflexive
proof
let X be Element of bool M;
consider SF being non-empty MSSubsetFamily of M such that
A2: for Y being ManySortedSet of I holds Y in SF iff Y in D & X c= Y by Th31;
J..X = meet SF & for Z1 being ManySortedSet of I st Z1 in SF holds X
c= Z1 by A1,A2;
hence thesis by MSSUBFAM:45;
end;
thus J is monotonic
proof
let x, y be Element of bool M such that
A3: x c= y;
consider SFx being non-empty MSSubsetFamily of M such that
A4: for Y being ManySortedSet of I holds Y in SFx iff Y in D & x c= Y by Th31;
consider SFy being non-empty MSSubsetFamily of M such that
A5: for Y being ManySortedSet of I holds Y in SFy iff Y in D & y c= Y by Th31;
SFy c= SFx
proof
let i be object;
assume
A6: i in I;
then consider Fi be non empty set such that
A7: Fi = D.i;
A8: x.i c= y.i by A3,A6;
SFx.i = { t where t is Element of Fi : x.i c= t } & SFy.i = { z
where z is Element of Fi : y.i c= z } by A4,A5,A6,A7,Th32;
hence thesis by A8,Th1;
end;
then
A9: meet SFx c= meet SFy by MSSUBFAM:46;
J..x = meet SFx by A1,A4;
hence thesis by A1,A5,A9;
end;
end;
theorem Th37:
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
proof
let D be absolutely-multiplicative MSSubsetFamily of M, J be MSSetOp of M
such that
A1: 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;
let X be Element of bool M;
defpred P[ManySortedSet of I] means X c= $1;
consider SF being non-empty MSSubsetFamily of M such that
A2: for Y being ManySortedSet of I holds Y in SF iff Y in D & X c= Y by Th31;
(for Y being ManySortedSet of I holds Y in SF iff Y in D & P[Y]) implies
SF c= D from MSSUBSET;
then
A3: meet SF in D by A2,MSSUBFAM:def 5;
D c= bool M by PBOOLE:def 18;
then
A4: meet SF is Element of bool M by A3,MSSUBFAM:11,PBOOLE:9;
thus J..X = meet SF by A1,A2
.= J..(meet SF) by A1,A3,A4,Th34
.= J..(J..X) by A1,A2;
end;
theorem
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 by Th36,Th37;
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
:Def13:
ex D being
MSSubsetFamily of A st D = MSFixPoints C & it = MSClosureStr (#A, D#);
existence
proof
reconsider D = MSFixPoints C as MSSubsetFamily of A;
reconsider a = MSClosureStr (#A, D#) as MSClosureSystem of S by Th30;
take a;
thus thesis;
end;
uniqueness;
end;
registration
let S;
let A be ManySortedSet of the carrier of S;
let C be MSClosureOperator of A;
cluster ClOp->ClSys C -> strict;
coherence
proof
ex D being MSSubsetFamily of A st D = MSFixPoints C & ClOp->ClSys C =
MSClosureStr (#A, D#) by Def13;
hence thesis;
end;
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;
coherence
proof
ex D being MSSubsetFamily of A st D = MSFixPoints C & ClOp->ClSys C =
MSClosureStr (#A, D#) by Def13;
hence thesis;
end;
end;
definition
let S;
let D be MSClosureSystem of S;
func ClSys->ClOp D -> MSClosureOperator of the Sorts of D means
:Def14:
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;
existence
proof
consider J being MSSetOp of the Sorts of D such that
A1: 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 by
Th33;
reconsider J as MSClosureOperator of the Sorts of D by A1,Th36,Th37;
take J;
thus thesis by A1;
end;
uniqueness
proof
set M = the Sorts of D;
let Q1, Q2 be MSClosureOperator of the Sorts of D such that
A2: 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 Q1..X = meet SF
and
A3: 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 Q2..X = meet SF;
now
let x be ManySortedSet of the carrier of S;
assume x in bool M;
then
A4: x is Element of bool M by MSSUBFAM:11;
then consider
SF being non-empty MSSubsetFamily of the Sorts of D such that
A5: for Y being ManySortedSet of the carrier of S holds Y in SF iff
Y in the Family of D & x c= Y by Th31;
thus Q1..x = meet SF by A2,A4,A5
.= Q2..x by A3,A4,A5;
end;
hence Q1 = Q2 by Th7;
end;
end;
theorem
for A being ManySortedSet of the carrier of S for J being
MSClosureOperator of A holds ClSys->ClOp (ClOp->ClSys J) = J
proof
let A be ManySortedSet of the carrier of S, J be MSClosureOperator of A;
set I = the carrier of S, M = the Sorts of ClOp->ClSys J, j = ClSys->ClOp (
ClOp->ClSys J);
A1: ex D being MSSubsetFamily of A st D = MSFixPoints J & ClOp->ClSys J =
MSClosureStr (#A, D#) by Def13;
for X being ManySortedSet of I st X in bool A holds j..X = J..X
proof
let X be ManySortedSet of I;
assume X in bool A;
then
A2: X is Element of bool M by A1,MSSUBFAM:11;
then consider SF being non-empty MSSubsetFamily of M such that
A3: for Y being ManySortedSet of I holds Y in SF iff Y in MSFixPoints
J & X c= Y by A1,Th31;
now
let i be object such that
A5: i in I;
reconsider f = J.i as Function of (bool A).i, (bool A).i by A5,
PBOOLE:def 15;
(bool A).i = bool (A.i) by A5,MBOOLEAN:def 1;
then reconsider f as Function of bool (A.i), bool (A.i);
X.i is Element of (bool A).i by A1,A2,A5,PBOOLE:def 14;
then
A6: X.i is Element of bool (A.i) by A5,MBOOLEAN:def 1;
then
A7: X.i c= f.(X.i) by A5,Th24;
reconsider Di = (MSFixPoints J).i as non empty set by A1,A5;
consider Q being Subset-Family of (M.i) such that
A8: Q = SF.i and
A9: (meet SF).i = Intersect Q by A5,MSSUBFAM:def 1;
A10: SF.i = { z where z is Element of Di : X.i c= z } by A1,A2,A3,A5,Th32;
now
let x;
assume x in Q;
then consider x1 being Element of Di such that
A11: x1 = x & X.i c= x1 by A8,A10;
MSFixPoints J c= bool A by PBOOLE:def 18;
then Di c= (bool A).i by A5;
then Di c= bool (A.i) by A5,MBOOLEAN:def 1;
then
A12: x1 is Element of bool (A.i);
ex g being Function st g = J.i & x1 in dom g & g.x1 = x1 by A5,Def12;
hence f.(X.i) c= x by A5,A6,A11,A12,Th25;
end;
then
A13: f.(X.i) c= Intersect Q by A5,A8,MSSUBFAM:5;
A14: dom f = bool (A.i) & f.(X.i) in bool (A.i) by A6,FUNCT_2:5,def 1;
f.(f.(X.i)) = f.(X.i) by A5,A6,Th26;
then f.(X.i) is Element of Di by A5,A14,Def12;
then f.(X.i) in { z where z is Element of Di : X.i c= z } by A7;
then Intersect Q c= f.(X.i) by A8,A10,MSSUBFAM:2;
then Intersect Q = f.(X.i) by A13;
hence (j..X).i = f.(X.i) by A1,A2,A3,A9,Def14
.= (J..X).i by A5,PRALG_1:def 20;
end;
hence thesis;
end;
hence thesis by A1,Th7;
end;
theorem
for D being MSClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) =
the MSClosureStr of D
proof
let D be MSClosureSystem of S;
set M = the Sorts of D, F = the Family of D, I = the carrier of S;
consider X1 being ManySortedSet of I such that
A1: X1 in bool M by PBOOLE:134;
F = MSFixPoints (ClSys->ClOp D)
proof
let i be object such that
A3: i in I;
reconsider f = (ClSys->ClOp D).i as Function of (bool M).i, (bool M).i
by A3,PBOOLE:def 15;
reconsider Fi = F.i as non empty set by A3;
thus F.i c= (MSFixPoints (ClSys->ClOp D)).i
proof
let x be object such that
A4: x in F.i;
reconsider xx=x as set by TARSKI:1;
dom (X1 +* (i .--> x)) = I by A3,PZFMISC1:1;
then reconsider X = X1 +* (i .--> x) as ManySortedSet of I by
PARTFUN1:def 2,RELAT_1:def 18;
A5: dom (i .--> x) = {i};
F c= bool M by PBOOLE:def 18;
then
A6: F.i c= (bool M).i by A3;
then x in (bool M).i by A4;
then
A7: x in dom f by FUNCT_2:def 1;
i in {i} by TARSKI:def 1;
then
A8: X.i = (i .--> x).i by A5,FUNCT_4:13
.= x by FUNCOP_1:72;
X is Element of bool M
proof
let s be object such that
A9: s in I;
per cases;
suppose
s = i;
hence thesis by A4,A8,A6;
end;
suppose
s <> i;
then not s in dom (i .--> x) by TARSKI:def 1;
then X.s = X1.s by FUNCT_4:11;
hence thesis by A1,A9;
end;
end;
then reconsider X as Element of bool M;
consider SF being non-empty MSSubsetFamily of M such that
A10: for Y being ManySortedSet of I holds Y in SF iff Y in F & X c= Y by Th31;
consider Q being Subset-Family of (M.i) such that
A11: Q = SF.i and
A12: (meet SF).i = Intersect Q by A3,MSSUBFAM:def 1;
A13: SF.i = { z where z is Element of Fi : X.i c= z } by A3,A10,Th32;
now
let Z1 be set;
assume Z1 in Q;
then ex q being Element of Fi st q = Z1 & X.i c= q by A11,A13;
hence xx c= Z1 by A8;
end;
then
A14: xx c= Intersect Q by A3,A11,MSSUBFAM:5;
x in { B where B is Element of Fi : xx c= B } by A4;
then Intersect Q c= xx by A8,A11,A13,MSSUBFAM:2;
then
A15: Intersect Q = x by A14,XBOOLE_0:def 10;
(ClSys->ClOp D)..X = meet SF by A10,Def14;
then f.x = x by A3,A8,A12,A15,PRALG_1:def 20;
hence thesis by A3,A7,Def12;
end;
let x be object;
assume
A16: x in (MSFixPoints (ClSys->ClOp D)).i;
then
A17: ex f being Function st f = (ClSys->ClOp D).i & x in dom f & f.x = x
by A3,Def12;
dom (X1 +* (i .--> x)) = I by A3,PZFMISC1:1;
then reconsider X = X1 +* (i .--> x) as ManySortedSet of I by
PARTFUN1:def 2,RELAT_1:def 18;
A18: dom (i .--> x) = {i};
i in {i} by TARSKI:def 1;
then
A19: X.i = (i .--> x).i by A18,FUNCT_4:13
.= x by FUNCOP_1:72;
MSFixPoints (ClSys->ClOp D) c= bool M by PBOOLE:def 18;
then
A20: (MSFixPoints (ClSys->ClOp D)).i c= (bool M).i by A3;
X is Element of bool M
proof
let s be object such that
A21: s in I;
per cases;
suppose
s = i;
hence thesis by A16,A19,A20;
end;
suppose
s <> i;
then not s in dom (i .--> x) by TARSKI:def 1;
then X.s = X1.s by FUNCT_4:11;
hence thesis by A1,A21;
end;
end;
then reconsider X as Element of bool M;
defpred P[ManySortedSet of I] means X c= $1;
consider SF being non-empty MSSubsetFamily of M such that
A22: for Y being ManySortedSet of I holds Y in SF iff Y in F & X c= Y by Th31;
(for Y being ManySortedSet of I holds Y in SF iff Y in F & P[Y])
implies SF c= F from MSSUBSET;
then
A24: meet SF in F by A22,MSSUBFAM:def 5;
(meet SF).i = ((ClSys->ClOp D)..X).i by A22,Def14
.= x by A3,A17,A19,PRALG_1:def 20;
hence thesis by A3,A24;
end;
hence thesis by Def13;
end;