CLOSURE3: Algebraic Operation on Subsets of Many Sorted Sets

:: Algebraic Operation on Subsets of Many Sorted Sets
:: by Agnieszka Julia Marasik
::
:: Received June 23, 1997
:: Copyright (c) 1997-2021 Association of Mizar Users

registration

let S be non empty 1-sorted ;

cluster 1-sorted(# the carrier of S #) -> non empty ;

end;

theorem Th1: :: CLOSURE3:1

for I being non empty set
for M, N being ManySortedSet of I holds M +* N = N

proof end;

theorem :: CLOSURE3:2

for I being set
for M, N being ManySortedSet of I
for F being SubsetFamily of M st N in F holds
meet |:F:| c=' N by CLOSURE2:21, MSSUBFAM:43;

theorem Th3: :: CLOSURE3:3

for S being non empty non void ManySortedSign
for MA being strict non-empty MSAlgebra over S
for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds
for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed

proof end;

theorem :: CLOSURE3:4

for A, B, C being set st A is_coarser_than B & B is_coarser_than C holds
A is_coarser_than C

proof end;

Lm1: now :: thesis:

let I be non empty set ; :: thesis:
let M be ManySortedSet of I; :: thesis:
set F = { x where x is Element of I : M . x <> {} } ;
thus support M = { x where x is Element of I : M . x <> {} } :: thesis:

thus support M c= { x where x is Element of I : M . x <> {} } :: according to XBOOLE_0:def 10 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
A1: dom M = I by PARTFUN1:def 2;
A2: support M c= dom M by PRE_POLY:37;
assume A3: x in support M ; :: thesis:
then M . x <> {} by PRE_POLY:def 7;
hence x in { x where x is Element of I : M . x <> {} } by A1, A2, A3; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { x where x is Element of I : M . x <> {} } ; :: thesis:
then ex i being Element of I st
( x = i & M . i <> {} ) ;
hence x in support M by PRE_POLY:def 7; :: thesis:

end;

end;

definition

let I be non empty set ;
let M be ManySortedSet of I;

:: original: support
redefine func support M -> set equals :: CLOSURE3:def 1
{ x where x is Element of I : M . x <> {} } ;

compatibility by Lm1;

end;

:: deftheorem defines support CLOSURE3:def 1 :

theorem :: CLOSURE3:5

for I being non empty set
for M being V8() ManySortedSet of I holds M = (EmptyMS I) +* (M | (support M))

proof end;

theorem :: CLOSURE3:6

for I being non empty set
for M1, M2 being V8() ManySortedSet of I st M1 | (support M1) = M2 | (support M2) holds
M1 = M2

proof end;

theorem :: CLOSURE3:7

canceled;

::$CT

theorem Th7: :: CLOSURE3:8

for I being non empty set
for M being ManySortedSet of I
for x being Element of Bool M
for i being Element of I
for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is V45() & support a is finite & a c= x )

proof end;

definition

let I be set ;
let M be ManySortedSet of I;
let A be SubsetFamily of M;

func MSUnion A -> ManySortedSubset of M means :Def2: :: CLOSURE3:def 2
for i being set st i in I holds
it . i = union { (f . i) where f is Element of Bool M : f in A } ;

proof end;

proof end;

end;

:: deftheorem Def2 defines MSUnion CLOSURE3:def 2 :

registration

let I be set ;
let M be ManySortedSet of I;
let A be empty SubsetFamily of M;

cluster MSUnion A -> V9() ;

proof end;

end;

theorem :: CLOSURE3:9

for I being set
for M being ManySortedSet of I
for A being SubsetFamily of M holds MSUnion A = union |:A:|

proof end;

definition

let I be set ;
let M be ManySortedSet of I;
let A, B be SubsetFamily of M;
:: original: \/
redefine func A \/ B -> SubsetFamily of M;
correctness by CLOSURE2:3;

end;

theorem :: CLOSURE3:10

for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) (\/) (MSUnion B)

proof end;

theorem :: CLOSURE3:11

for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M st A c= B holds
MSUnion A c= MSUnion B

proof end;

definition

let I be set ;
let M be ManySortedSet of I;
let A, B be SubsetFamily of M;
:: original: /\
redefine func A /\ B -> SubsetFamily of M;
correctness by CLOSURE2:4;

end;

theorem :: CLOSURE3:12

for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) (/\) (MSUnion B)

proof end;

theorem :: CLOSURE3:13

for I being set
for M being ManySortedSet of I
for AA being set st ( for x being set st x in AA holds
x is SubsetFamily of M ) holds
for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds
MSUnion B = MSUnion A

proof end;

definition

let I be non empty set ;
let M be ManySortedSet of I;
let S be SetOp of M;

attr S is algebraic means :: CLOSURE3:def 3
for x being Element of Bool M st x = S . x holds
ex A being SubsetFamily of M st
( A = { (S . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } & x = MSUnion A );

end;

:: deftheorem defines algebraic CLOSURE3:def 3 :

registration

let I be non empty set ;
let M be ManySortedSet of I;

cluster non empty Relation-like Bool M -defined Bool M -valued Function-like V17( Bool M) quasi_total reflexive monotonic idempotent algebraic for Element of bool [:(Bool M),(Bool M):];

proof end;

end;

definition

let S be non empty 1-sorted ;
let IT be ClosureSystem of S;

attr IT is algebraic means :: CLOSURE3:def 4
ClSys->ClOp IT is algebraic ;

end;

:: deftheorem defines algebraic CLOSURE3:def 4 :

definition

let S be non empty non void ManySortedSign ;
let MA be non-empty MSAlgebra over S;

func SubAlgCl MA -> strict ClosureStr over 1-sorted(# the carrier of S #) means :Def5: :: CLOSURE3:def 5
( the Sorts of it = the Sorts of MA & the Family of it = SubSort MA );

proof end;

end;

:: deftheorem Def5 defines SubAlgCl CLOSURE3:def 5 :

theorem Th13: :: CLOSURE3:14

for S being non empty non void ManySortedSign
for MA being strict non-empty MSAlgebra over S holds SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA

proof end;

registration

let S be non empty non void ManySortedSign ;
let MA be strict non-empty MSAlgebra over S;

cluster SubAlgCl MA -> strict absolutely-multiplicative ;

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let MA be strict non-empty MSAlgebra over S;

cluster SubAlgCl MA -> strict algebraic ;

proof end;

end;