:: by Artur Korni{\l}owicz

::

:: Received February 7, 1996

:: Copyright (c) 1996-2018 Association of Mizar Users

scheme :: CLOSURE1:sch 1

MSSUBSET{ F_{1}() -> set , F_{2}() -> V8() ManySortedSet of F_{1}(), F_{3}() -> ManySortedSet of F_{1}(), P_{1}[ set ] } :

MSSUBSET{ F

( ( for X being ManySortedSet of F_{1}() holds

( X in F_{2}() iff ( X in F_{3}() & P_{1}[X] ) ) ) implies F_{2}() c= F_{3}() )

( X in F

proof end;

theorem Th1: :: CLOSURE1:1

for X being non empty set

for x, y being set st x c= y holds

{ t where t is Element of X : y c= t } c= { z where z is Element of X : x c= z }

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 end;

theorem :: CLOSURE1:2

for I being set

for M being ManySortedSet of I st ex A being ManySortedSet of I st A in M holds

M is V8() ;

for M being ManySortedSet of I st ex A being ManySortedSet of I st A in M holds

M is V8() ;

registration

let I be set ;

let F be ManySortedFunction of I;

let A be ManySortedSet of I;

coherence

for b_{1} being I -defined Function st b_{1} = F .. A holds

b_{1} is total
;

end;
let F be ManySortedFunction of I;

let A be ManySortedSet of I;

coherence

for b

b

Lm1: now :: thesis: for I being set

for A, B being V8() ManySortedSet of I

for F being ManySortedFunction of A,B

for X being Element of A holds F .. X is Element of B

for A, B being V8() ManySortedSet of I

for F being ManySortedFunction of A,B

for X being Element of A holds F .. X is Element of B

let I be set ; :: thesis: for A, B being V8() ManySortedSet of I

for F being ManySortedFunction of A,B

for X being Element of A holds F .. X is Element of B

let A, B be V8() ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B

for X being Element of A holds F .. X is Element of B

let F be ManySortedFunction of A,B; :: thesis: for X being Element of A holds F .. X is Element of B

let X be Element of A; :: thesis: F .. X is Element of B

thus F .. X is Element of B :: thesis: verum

end;
for F being ManySortedFunction of A,B

for X being Element of A holds F .. X is Element of B

let A, B be V8() ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B

for X being Element of A holds F .. X is Element of B

let F be ManySortedFunction of A,B; :: thesis: for X being Element of A holds F .. X is Element of B

let X be Element of A; :: thesis: F .. X is Element of B

thus F .. X is Element of B :: thesis: verum

proof

let i be object ; :: according to PBOOLE:def 14 :: thesis: ( not i in I or (F .. X) . i is Element of B . i )

assume A1: i in I ; :: thesis: (F .. X) . i is Element of B . 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, PBOOLE:def 15;

then ( dom F = I & g . (X . i) in B . i ) by A1, FUNCT_2:5, PARTFUN1:def 2;

hence (F .. X) . i is Element of B . i by A1, PRALG_1:def 17; :: thesis: verum

end;
assume A1: i in I ; :: thesis: (F .. X) . i is Element of B . 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, PBOOLE:def 15;

then ( dom F = I & g . (X . i) in B . i ) by A1, FUNCT_2:5, PARTFUN1:def 2;

hence (F .. X) . i is Element of B . i by A1, PRALG_1:def 17; :: thesis: verum

definition

let I be set ;

let A, B be V8() ManySortedSet of I;

let F be ManySortedFunction of A,B;

let X be Element of A;

:: original: ..

redefine func F .. X -> Element of B;

coherence

F .. X is Element of B by Lm1;

end;
let A, B be V8() ManySortedSet of I;

let F be ManySortedFunction of A,B;

let X be Element of A;

:: original: ..

redefine func F .. X -> Element of B;

coherence

F .. X is Element of B by Lm1;

theorem :: CLOSURE1:3

for I being set

for A, X being ManySortedSet of I

for B being V8() ManySortedSet of I

for F being ManySortedFunction of A,B st X in A holds

F .. X in B

for A, X being ManySortedSet of I

for B being V8() ManySortedSet of I

for F being ManySortedFunction of A,B st X in A holds

F .. X in B

proof end;

theorem Th4: :: CLOSURE1:4

for I being set

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

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 end;

theorem :: CLOSURE1:5

for I being set

for F being ManySortedFunction of I st F is "1-1" holds

for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds

A = B

for F being ManySortedFunction of I st F is "1-1" holds

for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds

A = B

proof end;

theorem :: CLOSURE1:6

for I being set

for F being ManySortedFunction of I st doms F is V8() & ( for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds

A = B ) holds

F is "1-1"

for F being ManySortedFunction of I st doms F is V8() & ( for A, B being ManySortedSet of I st A in doms F & B in doms F & F .. A = F .. B holds

A = B ) holds

F is "1-1"

proof end;

theorem Th7: :: CLOSURE1:7

for I being set

for A, B being V8() ManySortedSet of I

for F, G being ManySortedFunction of A,B st ( for M being ManySortedSet of I st M in A holds

F .. M = G .. M ) holds

F = G

for A, B being V8() ManySortedSet of I

for F, G being ManySortedFunction of A,B st ( for M being ManySortedSet of I st M in A holds

F .. M = G .. M ) holds

F = G

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

existence

ex b_{1} being Element of bool M st

( b_{1} is V9() & b_{1} is V45() )

end;
let M be ManySortedSet of I;

existence

ex b

( b

proof end;

definition

let I be set ;

let M be ManySortedSet of I;

mode MSSetOp of M is ManySortedFunction of bool M, bool M;

end;
let M be ManySortedSet of I;

mode MSSetOp of M is ManySortedFunction of bool M, bool M;

definition

let I be set ;

let M be ManySortedSet of I;

let O be MSSetOp of M;

let X be Element of bool M;

:: original: ..

redefine func O .. X -> Element of bool M;

coherence

O .. X is Element of bool M by Lm1;

end;
let M be ManySortedSet of I;

let O be MSSetOp of M;

let X be Element of bool M;

:: original: ..

redefine func O .. X -> Element of bool M;

coherence

O .. X is Element of bool M by Lm1;

definition

let I be set ;

let M be ManySortedSet of I;

let IT be MSSetOp of M;

end;
let M be ManySortedSet of I;

let IT be MSSetOp of M;

attr IT is reflexive means :Def1: :: CLOSURE1:def 1

for X being Element of bool M holds X c= IT .. X;

for X being Element of bool M holds X c= IT .. X;

attr IT is monotonic means :: CLOSURE1:def 2

for X, Y being Element of bool M st X c= Y holds

IT .. X c= IT .. Y;

for X, Y being Element of bool M st X c= Y holds

IT .. X c= IT .. Y;

attr IT is idempotent means :: CLOSURE1:def 3

for X being Element of bool M holds IT .. X = IT .. (IT .. X);

for X being Element of bool M holds IT .. X = IT .. (IT .. X);

:: deftheorem Def1 defines reflexive CLOSURE1:def 1 :

for I being set

for M being ManySortedSet of I

for IT being MSSetOp of M holds

( IT is reflexive iff for X being Element of bool M holds X c= IT .. X );

for I being set

for M being ManySortedSet of I

for IT being MSSetOp of M holds

( IT is reflexive iff for X being Element of bool M holds X c= IT .. X );

:: deftheorem defines monotonic CLOSURE1:def 2 :

for I being set

for M being ManySortedSet of I

for IT being MSSetOp of M holds

( IT is monotonic iff for X, Y being Element of bool M st X c= Y holds

IT .. X c= IT .. Y );

for I being set

for M being ManySortedSet of I

for IT being MSSetOp of M holds

( IT is monotonic iff for X, Y being Element of bool M st X c= Y holds

IT .. X c= IT .. Y );

:: deftheorem defines idempotent CLOSURE1:def 3 :

for I being set

for M being ManySortedSet of I

for IT being MSSetOp of M holds

( IT is idempotent iff for X being Element of bool M holds IT .. X = IT .. (IT .. X) );

for I being set

for M being ManySortedSet of I

for IT being MSSetOp of M holds

( IT is idempotent iff for X being Element of bool M holds IT .. X = IT .. (IT .. X) );

:: deftheorem defines topological CLOSURE1:def 4 :

for I being set

for M being ManySortedSet of I

for IT being MSSetOp of M holds

( IT is topological iff for X, Y being Element of bool M holds IT .. (X (\/) Y) = (IT .. X) (\/) (IT .. Y) );

for I being set

for M being ManySortedSet of I

for IT being MSSetOp of M holds

( IT is topological iff for X, Y being Element of bool M holds IT .. (X (\/) Y) = (IT .. X) (\/) (IT .. Y) );

theorem Th9: :: CLOSURE1:9

for I being set

for M being V8() ManySortedSet of I

for X, Y being Element of M st X c= Y holds

(id M) .. X c= (id M) .. Y

for M being V8() ManySortedSet of I

for X, Y being Element of M st X c= Y holds

(id M) .. X c= (id M) .. Y

proof end;

theorem Th10: :: CLOSURE1:10

for I being set

for M being V8() 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)

for M being V8() 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 end;

theorem :: CLOSURE1:11

for I being set

for M being ManySortedSet of I

for X being Element of bool M

for i, x being set st i in I & x in ((id (bool M)) .. X) . i holds

ex Y being V45() Element of bool M st

( Y c= X & x in ((id (bool M)) .. Y) . i )

for M being ManySortedSet of I

for X being Element of bool M

for i, x being set st i in I & x in ((id (bool M)) .. X) . i holds

ex Y being V45() Element of bool M st

( Y c= X & x in ((id (bool M)) .. Y) . i )

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

ex b_{1} being MSSetOp of M st

( b_{1} is reflexive & b_{1} is monotonic & b_{1} is idempotent & b_{1} is topological )

end;
let M be ManySortedSet of I;

cluster Relation-like I -defined Function-like total Function-yielding V25() reflexive monotonic idempotent topological for MSSetOp of M;

existence ex b

( b

proof end;

theorem :: CLOSURE1:16

for I being set

for M being ManySortedSet of I

for P being MSSetOp of M

for E being Element of bool M st E = M & P is reflexive holds

E = P .. E

for M being ManySortedSet of I

for P being MSSetOp of M

for E being Element of bool M st E = M & P is reflexive holds

E = P .. E

proof end;

theorem :: CLOSURE1:17

for I being set

for M being ManySortedSet of I

for P being MSSetOp of M st P is reflexive & ( for X being Element of bool M holds P .. X c= X ) holds

P is idempotent

for M being ManySortedSet of I

for P being MSSetOp of M st P is reflexive & ( for X being Element of bool M holds P .. X c= X ) holds

P is idempotent

proof end;

theorem :: CLOSURE1:18

for I being set

for M being ManySortedSet of I

for P being MSSetOp of M

for E, T being Element of bool M st P is monotonic holds

P .. (E (/\) T) c= (P .. E) (/\) (P .. T)

for M being ManySortedSet of I

for P being MSSetOp of M

for E, T being Element of bool M st P is monotonic holds

P .. (E (/\) T) c= (P .. E) (/\) (P .. T)

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

coherence

for b_{1} being MSSetOp of M st b_{1} is topological holds

b_{1} is monotonic

end;
let M be ManySortedSet of I;

coherence

for b

b

proof end;

theorem :: CLOSURE1:19

for I being set

for M being ManySortedSet of I

for P being MSSetOp of M

for E, T being Element of bool M st P is topological holds

(P .. E) (\) (P .. T) c= P .. (E (\) T)

for M being ManySortedSet of I

for P being MSSetOp of M

for E, T being Element of bool M st P is topological holds

(P .. E) (\) (P .. T) c= P .. (E (\) T)

proof end;

definition

let I be set ;

let M be ManySortedSet of I;

let R, P be MSSetOp of M;

:: original: **

redefine func P ** R -> MSSetOp of M;

coherence

P ** R is MSSetOp of M

end;
let M be ManySortedSet of I;

let R, P be MSSetOp of M;

:: original: **

redefine func P ** R -> MSSetOp of M;

coherence

P ** R is MSSetOp of M

proof end;

theorem :: CLOSURE1:20

for I being set

for M being ManySortedSet of I

for P, R being MSSetOp of M st P is reflexive & R is reflexive holds

P ** R is reflexive

for M being ManySortedSet of I

for P, R being MSSetOp of M st P is reflexive & R is reflexive holds

P ** R is reflexive

proof end;

theorem :: CLOSURE1:21

for I being set

for M being ManySortedSet of I

for P, R being MSSetOp of M st P is monotonic & R is monotonic holds

P ** R is monotonic

for M being ManySortedSet of I

for P, R being MSSetOp of M st P is monotonic & R is monotonic holds

P ** R is monotonic

proof end;

theorem :: CLOSURE1:22

for I being set

for M being ManySortedSet of I

for P, R being MSSetOp of M st P is idempotent & R is idempotent & P ** R = R ** P holds

P ** R is idempotent

for M being ManySortedSet of I

for P, R being MSSetOp of M st P is idempotent & R is idempotent & P ** R = R ** P holds

P ** R is idempotent

proof end;

theorem :: CLOSURE1:23

for I being set

for M being ManySortedSet of I

for P, R being MSSetOp of M st P is topological & R is topological holds

P ** R is topological

for M being ManySortedSet of I

for P, R being MSSetOp of M st P is topological & R is topological holds

P ** R is topological

proof end;

Lm2: now :: thesis: for I being set

for M being ManySortedSet of I

for i being set

for a being ManySortedSet of I

for b being Element of bool (M . i) st a = (EmptyMS I) +* (i .--> b) holds

a in bool M

for M being ManySortedSet of I

for i being set

for a being ManySortedSet of I

for b being Element of bool (M . i) st a = (EmptyMS I) +* (i .--> b) holds

a in bool M

let I be set ; :: thesis: for M being ManySortedSet of I

for i being set

for a being ManySortedSet of I

for b being Element of bool (M . i) st a = (EmptyMS I) +* (i .--> b) holds

a in bool M

let M be ManySortedSet of I; :: thesis: for i being set

for a being ManySortedSet of I

for b being Element of bool (M . i) st a = (EmptyMS I) +* (i .--> b) holds

a in bool M

let i be set ; :: thesis: for a being ManySortedSet of I

for b being Element of bool (M . i) st a = (EmptyMS I) +* (i .--> b) holds

a in bool M

let a be ManySortedSet of I; :: thesis: for b being Element of bool (M . i) st a = (EmptyMS I) +* (i .--> b) holds

a in bool M

let b be Element of bool (M . i); :: thesis: ( a = (EmptyMS I) +* (i .--> b) implies a in bool M )

assume A1: a = (EmptyMS I) +* (i .--> b) ; :: thesis: a in bool M

A2: dom (i .--> b) = {i} by FUNCOP_1:13;

EmptyMS I c= M by MBOOLEAN:5;

then A3: EmptyMS I in bool M by MBOOLEAN:1;

thus a in bool M :: thesis: verum

end;
for i being set

for a being ManySortedSet of I

for b being Element of bool (M . i) st a = (EmptyMS I) +* (i .--> b) holds

a in bool M

let M be ManySortedSet of I; :: thesis: for i being set

for a being ManySortedSet of I

for b being Element of bool (M . i) st a = (EmptyMS I) +* (i .--> b) holds

a in bool M

let i be set ; :: thesis: for a being ManySortedSet of I

for b being Element of bool (M . i) st a = (EmptyMS I) +* (i .--> b) holds

a in bool M

let a be ManySortedSet of I; :: thesis: for b being Element of bool (M . i) st a = (EmptyMS I) +* (i .--> b) holds

a in bool M

let b be Element of bool (M . i); :: thesis: ( a = (EmptyMS I) +* (i .--> b) implies a in bool M )

assume A1: a = (EmptyMS I) +* (i .--> b) ; :: thesis: a in bool M

A2: dom (i .--> b) = {i} by FUNCOP_1:13;

EmptyMS I c= M by MBOOLEAN:5;

then A3: EmptyMS I in bool M by MBOOLEAN:1;

thus a in bool M :: thesis: verum

proof

let j be object ; :: according to PBOOLE:def 1 :: thesis: ( not j in I or a . j in (bool M) . j )

assume A4: j in I ; :: thesis: a . j in (bool M) . j

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 ;

end;
assume A4: j in I ; :: thesis: a . j in (bool M) . j

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 :: thesis: ( ( j = i & a . j in (bool M) . j ) or ( j <> i & a . j in (bool M) . j ) )
end;

hence
a . j in (bool M) . j
; :: thesis: verum
theorem Th24: :: CLOSURE1:24

for i, I being set

for M being ManySortedSet of I

for f being Function

for P being MSSetOp of M st P is reflexive & i in I & f = P . i holds

for x being Element of bool (M . i) holds x c= f . x

for M being ManySortedSet of I

for f being Function

for P being MSSetOp of M st P is reflexive & i in I & f = P . i holds

for x being Element of bool (M . i) holds x c= f . x

proof end;

theorem Th25: :: CLOSURE1:25

for i, I being set

for M being ManySortedSet of I

for f being Function

for P being MSSetOp of M st P is monotonic & i in I & f = P . i holds

for x, y being Element of bool (M . i) st x c= y holds

f . x c= f . y

for M being ManySortedSet of I

for f being Function

for P being MSSetOp of M st P is monotonic & i in I & f = P . i holds

for x, y being Element of bool (M . i) st x c= y holds

f . x c= f . y

proof end;

theorem Th26: :: CLOSURE1:26

for i, I being set

for M being ManySortedSet of I

for f being Function

for P being MSSetOp of M st P is idempotent & i in I & f = P . i holds

for x being Element of bool (M . i) holds f . x = f . (f . x)

for M being ManySortedSet of I

for f being Function

for P being MSSetOp of M st P is idempotent & i in I & f = P . i holds

for x being Element of bool (M . i) holds f . x = f . (f . x)

proof end;

theorem :: CLOSURE1:27

for i, I being set

for M being ManySortedSet of I

for f being Function

for P being MSSetOp of M st P is topological & i in I & f = P . i holds

for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y)

for M being ManySortedSet of I

for f being Function

for P being MSSetOp of M st P is topological & i in I & f = P . i holds

for x, y being Element of bool (M . i) holds f . (x \/ y) = (f . x) \/ (f . y)

proof end;

definition

let S be 1-sorted ;

attr c_{2} is strict ;

struct MSClosureStr over S -> many-sorted over S;

aggr MSClosureStr(# Sorts, Family #) -> MSClosureStr over S;

sel Family c_{2} -> MSSubsetFamily of the Sorts of c_{2};

end;
attr c

struct MSClosureStr over S -> many-sorted over S;

aggr MSClosureStr(# Sorts, Family #) -> MSClosureStr over S;

sel Family c

definition

let S be 1-sorted ;

let IT be MSClosureStr over S;

end;
let IT be MSClosureStr over S;

attr IT is absolutely-additive means :Def6: :: CLOSURE1:def 6

the Family of IT is absolutely-additive ;

the Family of IT is absolutely-additive ;

attr IT is absolutely-multiplicative means :Def8: :: CLOSURE1:def 8

the Family of IT is absolutely-multiplicative ;

the Family of IT is absolutely-multiplicative ;

attr IT is properly-upper-bound means :Def9: :: CLOSURE1:def 9

the Family of IT is properly-upper-bound ;

the Family of IT is properly-upper-bound ;

attr IT is properly-lower-bound means :Def10: :: CLOSURE1:def 10

the Family of IT is properly-lower-bound ;

the Family of IT is properly-lower-bound ;

:: deftheorem Def5 defines additive CLOSURE1:def 5 :

for S being 1-sorted

for IT being MSClosureStr over S holds

( IT is additive iff the Family of IT is additive );

for S being 1-sorted

for IT being MSClosureStr over S holds

( IT is additive iff the Family of IT is additive );

:: deftheorem Def6 defines absolutely-additive CLOSURE1:def 6 :

for S being 1-sorted

for IT being MSClosureStr over S holds

( IT is absolutely-additive iff the Family of IT is absolutely-additive );

for S being 1-sorted

for IT being MSClosureStr over S holds

( IT is absolutely-additive iff the Family of IT is absolutely-additive );

:: deftheorem Def7 defines multiplicative CLOSURE1:def 7 :

for S being 1-sorted

for IT being MSClosureStr over S holds

( IT is multiplicative iff the Family of IT is multiplicative );

for S being 1-sorted

for IT being MSClosureStr over S holds

( IT is multiplicative iff the Family of IT is multiplicative );

:: deftheorem Def8 defines absolutely-multiplicative CLOSURE1:def 8 :

for S being 1-sorted

for IT being MSClosureStr over S holds

( IT is absolutely-multiplicative iff the Family of IT is absolutely-multiplicative );

for S being 1-sorted

for IT being MSClosureStr over S holds

( IT is absolutely-multiplicative iff the Family of IT is absolutely-multiplicative );

:: deftheorem Def9 defines properly-upper-bound CLOSURE1:def 9 :

for S being 1-sorted

for IT being MSClosureStr over S holds

( IT is properly-upper-bound iff the Family of IT is properly-upper-bound );

for S being 1-sorted

for IT being MSClosureStr over S holds

( IT is properly-upper-bound iff the Family of IT is properly-upper-bound );

:: deftheorem Def10 defines properly-lower-bound CLOSURE1:def 10 :

for S being 1-sorted

for IT being MSClosureStr over S holds

( IT is properly-lower-bound iff the Family of IT is properly-lower-bound );

for S being 1-sorted

for IT being MSClosureStr over S holds

( IT is properly-lower-bound iff the Family of IT is properly-lower-bound );

definition

let S be 1-sorted ;

let MS be many-sorted over S;

coherence

MSClosureStr(# the Sorts of MS,(bool the Sorts of MS) #) is MSClosureStr over S;

;

end;
let MS be many-sorted over S;

func MSFull MS -> MSClosureStr over S equals :: CLOSURE1:def 11

MSClosureStr(# the Sorts of MS,(bool the Sorts of MS) #);

correctness MSClosureStr(# the Sorts of MS,(bool the Sorts of MS) #);

coherence

MSClosureStr(# the Sorts of MS,(bool the Sorts of MS) #) is MSClosureStr over S;

;

:: deftheorem defines MSFull CLOSURE1:def 11 :

for S being 1-sorted

for MS being many-sorted over S holds MSFull MS = MSClosureStr(# the Sorts of MS,(bool the Sorts of MS) #);

for S being 1-sorted

for MS being many-sorted over S holds MSFull MS = MSClosureStr(# the Sorts of MS,(bool the Sorts of MS) #);

registration

let S be 1-sorted ;

let MS be many-sorted over S;

( MSFull MS is strict & MSFull MS is additive & MSFull MS is absolutely-additive & MSFull MS is multiplicative & MSFull MS is absolutely-multiplicative & MSFull MS is properly-upper-bound & MSFull MS is properly-lower-bound ) ;

end;
let MS be many-sorted over S;

cluster MSFull MS -> strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ;

coherence ( MSFull MS is strict & MSFull MS is additive & MSFull MS is absolutely-additive & MSFull MS is multiplicative & MSFull MS is absolutely-multiplicative & MSFull MS is properly-upper-bound & MSFull MS is properly-lower-bound ) ;

registration
end;

registration

let S be 1-sorted ;

ex b_{1} being MSClosureStr over S st

( b_{1} is strict & b_{1} is non-empty & b_{1} is additive & b_{1} is absolutely-additive & b_{1} is multiplicative & b_{1} is absolutely-multiplicative & b_{1} is properly-upper-bound & b_{1} is properly-lower-bound )

end;
cluster non-empty strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for MSClosureStr over S;

existence ex b

( b

proof end;

registration

let S be 1-sorted ;

let CS be additive MSClosureStr over S;

coherence

the Family of CS is additive by Def5;

end;
let CS be additive MSClosureStr over S;

coherence

the Family of CS is additive by Def5;

registration

let S be 1-sorted ;

let CS be absolutely-additive MSClosureStr over S;

coherence

the Family of CS is absolutely-additive by Def6;

end;
let CS be absolutely-additive MSClosureStr over S;

coherence

the Family of CS is absolutely-additive by Def6;

registration

let S be 1-sorted ;

let CS be multiplicative MSClosureStr over S;

coherence

the Family of CS is multiplicative by Def7;

end;
let CS be multiplicative MSClosureStr over S;

coherence

the Family of CS is multiplicative by Def7;

registration

let S be 1-sorted ;

let CS be absolutely-multiplicative MSClosureStr over S;

coherence

the Family of CS is absolutely-multiplicative by Def8;

end;
let CS be absolutely-multiplicative MSClosureStr over S;

coherence

the Family of CS is absolutely-multiplicative by Def8;

registration

let S be 1-sorted ;

let CS be properly-upper-bound MSClosureStr over S;

coherence

the Family of CS is properly-upper-bound by Def9;

end;
let CS be properly-upper-bound MSClosureStr over S;

coherence

the Family of CS is properly-upper-bound by Def9;

registration

let S be 1-sorted ;

let CS be properly-lower-bound MSClosureStr over S;

coherence

the Family of CS is properly-lower-bound by Def10;

end;
let CS be properly-lower-bound MSClosureStr over S;

coherence

the Family of CS is properly-lower-bound by Def10;

registration

let S be 1-sorted ;

let M be V8() ManySortedSet of the carrier of S;

let F be MSSubsetFamily of M;

coherence

MSClosureStr(# M,F #) is non-empty ;

end;
let M be V8() ManySortedSet of the carrier of S;

let F be MSSubsetFamily of M;

coherence

MSClosureStr(# M,F #) is non-empty ;

registration

let S be 1-sorted ;

let MS be many-sorted over S;

let F be additive MSSubsetFamily of the Sorts of MS;

coherence

MSClosureStr(# the Sorts of MS,F #) is additive ;

end;
let MS be many-sorted over S;

let F be additive MSSubsetFamily of the Sorts of MS;

coherence

MSClosureStr(# the Sorts of MS,F #) is additive ;

registration

let S be 1-sorted ;

let MS be many-sorted over S;

let F be absolutely-additive MSSubsetFamily of the Sorts of MS;

coherence

MSClosureStr(# the Sorts of MS,F #) is absolutely-additive ;

end;
let MS be many-sorted over S;

let F be absolutely-additive MSSubsetFamily of the Sorts of MS;

coherence

MSClosureStr(# the Sorts of MS,F #) is absolutely-additive ;

registration

let S be 1-sorted ;

let MS be many-sorted over S;

let F be multiplicative MSSubsetFamily of the Sorts of MS;

coherence

MSClosureStr(# the Sorts of MS,F #) is multiplicative ;

end;
let MS be many-sorted over S;

let F be multiplicative MSSubsetFamily of the Sorts of MS;

coherence

MSClosureStr(# the Sorts of MS,F #) is multiplicative ;

registration

let S be 1-sorted ;

let MS be many-sorted over S;

let F be absolutely-multiplicative MSSubsetFamily of the Sorts of MS;

coherence

MSClosureStr(# the Sorts of MS,F #) is absolutely-multiplicative ;

end;
let MS be many-sorted over S;

let F be absolutely-multiplicative MSSubsetFamily of the Sorts of MS;

coherence

MSClosureStr(# the Sorts of MS,F #) is absolutely-multiplicative ;

registration

let S be 1-sorted ;

let MS be many-sorted over S;

let F be properly-upper-bound MSSubsetFamily of the Sorts of MS;

coherence

MSClosureStr(# the Sorts of MS,F #) is properly-upper-bound ;

end;
let MS be many-sorted over S;

let F be properly-upper-bound MSSubsetFamily of the Sorts of MS;

coherence

MSClosureStr(# the Sorts of MS,F #) is properly-upper-bound ;

registration

let S be 1-sorted ;

let MS be many-sorted over S;

let F be properly-lower-bound MSSubsetFamily of the Sorts of MS;

coherence

MSClosureStr(# the Sorts of MS,F #) is properly-lower-bound ;

end;
let MS be many-sorted over S;

let F be properly-lower-bound MSSubsetFamily of the Sorts of MS;

coherence

MSClosureStr(# the Sorts of MS,F #) is properly-lower-bound ;

registration

let S be 1-sorted ;

coherence

for b_{1} being MSClosureStr over S st b_{1} is absolutely-additive holds

b_{1} is additive
;

end;
coherence

for b

b

registration

let S be 1-sorted ;

coherence

for b_{1} being MSClosureStr over S st b_{1} is absolutely-multiplicative holds

b_{1} is multiplicative
;

end;
coherence

for b

b

registration

let S be 1-sorted ;

coherence

for b_{1} being MSClosureStr over S st b_{1} is absolutely-multiplicative holds

b_{1} is properly-upper-bound
;

end;
coherence

for b

b

registration

let S be 1-sorted ;

coherence

for b_{1} being MSClosureStr over S st b_{1} is absolutely-additive holds

b_{1} is properly-lower-bound
;

end;
coherence

for b

b

definition
end;

definition

let I be set ;

let M be ManySortedSet of I;

mode MSClosureOperator of M is reflexive monotonic idempotent MSSetOp of M;

end;
let M be ManySortedSet of I;

mode MSClosureOperator of M is reflexive monotonic idempotent MSSetOp of M;

definition

let I be set ;

let M be ManySortedSet of I;

let F be ManySortedFunction of M,M;

ex b_{1} being ManySortedSubset of M st

for x being set

for i being object st i in I holds

( x in b_{1} . i iff ex f being Function st

( f = F . i & x in dom f & f . x = x ) )

for b_{1}, b_{2} being ManySortedSubset of M st ( for x being set

for i being object st i in I holds

( x in b_{1} . i iff ex f being Function st

( f = F . i & x in dom f & f . x = x ) ) ) & ( for x being set

for i being object st i in I holds

( x in b_{2} . i iff ex f being Function st

( f = F . i & x in dom f & f . x = x ) ) ) holds

b_{1} = b_{2}

end;
let M be ManySortedSet of I;

let F be ManySortedFunction of M,M;

func MSFixPoints F -> ManySortedSubset of M means :Def12: :: CLOSURE1:def 12

for x being set

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 for x being set

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

ex b

for x being set

for i being object st i in I holds

( x in b

( f = F . i & x in dom f & f . x = x ) )

proof end;

uniqueness for b

for i being object st i in I holds

( x in b

( f = F . i & x in dom f & f . x = x ) ) ) & ( for x being set

for i being object st i in I holds

( x in b

( f = F . i & x in dom f & f . x = x ) ) ) holds

b

proof end;

:: deftheorem Def12 defines MSFixPoints CLOSURE1:def 12 :

for I being set

for M being ManySortedSet of I

for F being ManySortedFunction of M,M

for b_{4} being ManySortedSubset of M holds

( b_{4} = MSFixPoints F iff for x being set

for i being object st i in I holds

( x in b_{4} . i iff ex f being Function st

( f = F . i & x in dom f & f . x = x ) ) );

for I being set

for M being ManySortedSet of I

for F being ManySortedFunction of M,M

for b

( b

for i being object st i in I holds

( x in b

( f = F . i & x in dom f & f . x = x ) ) );

registration

let I be set ;

let M be V9() ManySortedSet of I;

let F be ManySortedFunction of M,M;

coherence

MSFixPoints F is empty-yielding

end;
let M be V9() ManySortedSet of I;

let F be ManySortedFunction of M,M;

coherence

MSFixPoints F is empty-yielding

proof end;

theorem Th28: :: CLOSURE1:28

for I being set

for A, M being ManySortedSet of I

for F being ManySortedFunction of M,M holds

( ( A in M & F .. A = A ) iff A in MSFixPoints F )

for A, M being ManySortedSet of I

for F being ManySortedFunction of M,M holds

( ( A in M & F .. A = A ) iff A in MSFixPoints F )

proof end;

theorem Th30: :: CLOSURE1:30

for S being 1-sorted

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

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 end;

theorem Th31: :: CLOSURE1:31

for I being set

for M being ManySortedSet of I

for D being properly-upper-bound MSSubsetFamily of M

for X being Element of bool M ex SF being V8() MSSubsetFamily of M st

for Y being ManySortedSet of I holds

( Y in SF iff ( Y in D & X c= Y ) )

for M being ManySortedSet of I

for D being properly-upper-bound MSSubsetFamily of M

for X being Element of bool M ex SF being V8() MSSubsetFamily of M st

for Y being ManySortedSet of I holds

( Y in SF iff ( Y in D & X c= Y ) )

proof end;

theorem Th32: :: CLOSURE1:32

for I being set

for M being ManySortedSet of I

for D being properly-upper-bound MSSubsetFamily of M

for X being Element of bool M

for SF being V8() 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

for 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 }

for M being ManySortedSet of I

for D being properly-upper-bound MSSubsetFamily of M

for X being Element of bool M

for SF being V8() 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

for 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 end;

theorem Th33: :: CLOSURE1:33

for I being set

for M being ManySortedSet of I

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 V8() 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

for M being ManySortedSet of I

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 V8() 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 end;

theorem Th34: :: CLOSURE1:34

for I being set

for M being ManySortedSet of I

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 V8() 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

for M being ManySortedSet of I

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 V8() 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 end;

theorem :: CLOSURE1:35

for I being set

for M being ManySortedSet of I

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 V8() 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

for M being ManySortedSet of I

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 V8() 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 end;

theorem Th36: :: CLOSURE1:36

for I being set

for M being ManySortedSet of I

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 V8() 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 & J is monotonic )

for M being ManySortedSet of I

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 V8() 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 & J is monotonic )

proof end;

theorem Th37: :: CLOSURE1:37

for I being set

for M being ManySortedSet of I

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 V8() 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

for M being ManySortedSet of I

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 V8() 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 end;

theorem :: CLOSURE1:38

for S being 1-sorted

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 V8() 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;

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 V8() 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 be 1-sorted ;

let A be ManySortedSet of the carrier of S;

let C be MSClosureOperator of A;

ex b_{1} being MSClosureSystem of S ex D being MSSubsetFamily of A st

( D = MSFixPoints C & b_{1} = MSClosureStr(# A,D #) )

for b_{1}, b_{2} being MSClosureSystem of S st ex D being MSSubsetFamily of A st

( D = MSFixPoints C & b_{1} = MSClosureStr(# A,D #) ) & ex D being MSSubsetFamily of A st

( D = MSFixPoints C & b_{2} = MSClosureStr(# A,D #) ) holds

b_{1} = b_{2}
;

end;
let A be ManySortedSet of the carrier of S;

let C be MSClosureOperator of A;

func ClOp->ClSys C -> MSClosureSystem of S means :Def13: :: CLOSURE1:def 13

ex D being MSSubsetFamily of A st

( D = MSFixPoints C & it = MSClosureStr(# A,D #) );

existence ex D being MSSubsetFamily of A st

( D = MSFixPoints C & it = MSClosureStr(# A,D #) );

ex b

( D = MSFixPoints C & b

proof end;

uniqueness for b

( D = MSFixPoints C & b

( D = MSFixPoints C & b

b

:: deftheorem Def13 defines ClOp->ClSys CLOSURE1:def 13 :

for S being 1-sorted

for A being ManySortedSet of the carrier of S

for C being MSClosureOperator of A

for b_{4} being MSClosureSystem of S holds

( b_{4} = ClOp->ClSys C iff ex D being MSSubsetFamily of A st

( D = MSFixPoints C & b_{4} = MSClosureStr(# A,D #) ) );

for S being 1-sorted

for A being ManySortedSet of the carrier of S

for C being MSClosureOperator of A

for b

( b

( D = MSFixPoints C & b

registration

let S be 1-sorted ;

let A be ManySortedSet of the carrier of S;

let C be MSClosureOperator of A;

coherence

ClOp->ClSys C is strict

end;
let A be ManySortedSet of the carrier of S;

let C be MSClosureOperator of A;

coherence

ClOp->ClSys C is strict

proof end;

registration

let S be 1-sorted ;

let A be V8() ManySortedSet of the carrier of S;

let C be MSClosureOperator of A;

coherence

ClOp->ClSys C is non-empty

end;
let A be V8() ManySortedSet of the carrier of S;

let C be MSClosureOperator of A;

coherence

ClOp->ClSys C is non-empty

proof end;

definition

let S be 1-sorted ;

let D be MSClosureSystem of S;

ex b_{1} being MSClosureOperator of the Sorts of D st

for X being Element of bool the Sorts of D

for SF being V8() 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

b_{1} .. X = meet SF

for b_{1}, b_{2} being MSClosureOperator of the Sorts of D st ( for X being Element of bool the Sorts of D

for SF being V8() 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

b_{1} .. X = meet SF ) & ( for X being Element of bool the Sorts of D

for SF being V8() 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

b_{2} .. X = meet SF ) holds

b_{1} = b_{2}

end;
let D be MSClosureSystem of S;

func ClSys->ClOp D -> MSClosureOperator of the Sorts of D means :Def14: :: CLOSURE1:def 14

for X being Element of bool the Sorts of D

for SF being V8() 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 for X being Element of bool the Sorts of D

for SF being V8() 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;

ex b

for X being Element of bool the Sorts of D

for SF being V8() 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

b

proof end;

uniqueness for b

for SF being V8() 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

b

for SF being V8() 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

b

b

proof end;

:: deftheorem Def14 defines ClSys->ClOp CLOSURE1:def 14 :

for S being 1-sorted

for D being MSClosureSystem of S

for b_{3} being MSClosureOperator of the Sorts of D holds

( b_{3} = ClSys->ClOp D iff for X being Element of bool the Sorts of D

for SF being V8() 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

b_{3} .. X = meet SF );

for S being 1-sorted

for D being MSClosureSystem of S

for b

( b

for SF being V8() 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

b

theorem :: CLOSURE1:39

for S being 1-sorted

for A being ManySortedSet of the carrier of S

for J being MSClosureOperator of A holds ClSys->ClOp (ClOp->ClSys J) = J

for A being ManySortedSet of the carrier of S

for J being MSClosureOperator of A holds ClSys->ClOp (ClOp->ClSys J) = J

proof end;

theorem :: CLOSURE1:40

for S being 1-sorted

for D being MSClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D, the Family of D #)

for D being MSClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = MSClosureStr(# the Sorts of D, the Family of D #)

proof end;