:: Certain Facts about Families of Subsets of Many Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Received October 27, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users

registration

let I be set ;
let F be ManySortedFunction of I;

cluster doms F -> I -defined ;

coherence
doms F is I -defined

proof end;

cluster rngs F -> I -defined ;

coherence
rngs F is I -defined

proof end;

end;

registration

let I be set ;
let F be ManySortedFunction of I;

cluster doms F -> I -defined total for I -defined Function;

coherence
for b₁ being I -defined Function st b₁ = doms F holds
b₁ is total

proof end;

cluster rngs F -> I -defined total for I -defined Function;

coherence
for b₁ being I -defined Function st b₁ = rngs F holds
b₁ is total

proof end;

end;

scheme :: MSSUBFAM:sch 1
MSFExFunc{ F₁() -> set , F₂() -> ManySortedSet of F₁(), F₃() -> ManySortedSet of F₁(), P₁[ object , object , object ] } :

ex F being ManySortedFunction of F₂(),F₃() st
for i being object st i in F₁() holds
ex f being Function of (F₂() . i),(F₃() . i) st
( f = F . i & ( for x being object st x in F₂() . i holds
P₁[f . x,x,i] ) )

provided

A1: for i being object st i in F₁() holds
for x being object st x in F₂() . i holds
ex y being object st
( y in F₃() . i & P₁[y,x,i] )

proof end;

theorem :: MSSUBFAM:1

for I being set
for sf being Subset-Family of I st sf <> {} holds
Intersect sf c= union sf

proof end;

theorem :: MSSUBFAM:2

for I, G being set
for sf being Subset-Family of I st G in sf holds
Intersect sf c= G

proof end;

theorem :: MSSUBFAM:3

for I being set
for sf being Subset-Family of I st {} in sf holds
Intersect sf = {}

proof end;

theorem :: MSSUBFAM:4

for I being set
for sf being Subset-Family of I
for Z being Subset of I st ( for Z1 being set st Z1 in sf holds
Z c= Z1 ) holds
Z c= Intersect sf

proof end;

theorem :: MSSUBFAM:5

for I, G being set
for sf being Subset-Family of I st sf <> {} & ( for Z1 being set st Z1 in sf holds
G c= Z1 ) holds
G c= Intersect sf

proof end;

theorem :: MSSUBFAM:6

for I, G, H being set
for sf being Subset-Family of I st G in sf & G c= H holds
Intersect sf c= H

proof end;

theorem :: MSSUBFAM:7

for I, G, H being set
for sf being Subset-Family of I st G in sf & G misses H holds
Intersect sf misses H

proof end;

theorem :: MSSUBFAM:8

for I being set
for sf, sg, sh being Subset-Family of I st sh = sf \/ sg holds
Intersect sh = (Intersect sf) /\ (Intersect sg)

proof end;

theorem :: MSSUBFAM:9

for I being set
for sf being Subset-Family of I
for v being Subset of I st sf = {v} holds
Intersect sf = v

proof end;

theorem :: MSSUBFAM:10

for I being set
for sf being Subset-Family of I
for v, w being Subset of I st sf = {v,w} holds
Intersect sf = v /\ w

proof end;

theorem :: MSSUBFAM:11

for I being set
for A, B being ManySortedSet of I st A in B holds
A is Element of B

proof end;

theorem :: MSSUBFAM:12

for I being set
for A being ManySortedSet of I
for B being V8() ManySortedSet of I st A is Element of B holds
A in B

proof end;

theorem Th13: :: MSSUBFAM:13

for I being set
for i being object
for F being ManySortedFunction of I
for f being Function st i in I & f = F . i holds
(rngs F) . i = rng f

proof end;

theorem Th14: :: MSSUBFAM:14

for I being set
for i being object
for F being ManySortedFunction of I
for f being Function st i in I & f = F . i holds
(doms F) . i = dom f

proof end;

theorem :: MSSUBFAM:15

for I being set
for F, G being ManySortedFunction of I holds G ** F is ManySortedFunction of I

proof end;

theorem :: MSSUBFAM:16

for I being set
for A being V8() ManySortedSet of I
for F being ManySortedFunction of A, EmptyMS I holds F = EmptyMS I

proof end;

theorem :: MSSUBFAM:17

for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of I st A is_transformable_to B & F is ManySortedFunction of A,B holds
( doms F = A & rngs F c= B )

proof end;

registration

let I be set ;

cluster Relation-like V9() I -defined Function-like total -> V39() for set ;

coherence
for b₁ being ManySortedSet of I st b₁ is V9() holds
b₁ is V39()

proof end;

end;

registration

let I be set ;

cluster EmptyMS I -> V9() V39() ;

coherence
( EmptyMS I is empty-yielding & EmptyMS I is finite-yielding ) ;

end;

registration

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

cluster Relation-like V9() I -defined Function-like total V39() for ManySortedSubset of A;

existence
ex b₁ being ManySortedSubset of A st
( b₁ is V9() & b₁ is V39() )

proof end;

end;

theorem Th18: :: MSSUBFAM:18

for I being set
for A, B being ManySortedSet of I st A c= B & B is V39() holds
A is V39()

proof end;

registration

let I be set ;
let A be V39() ManySortedSet of I;

cluster -> V39() for ManySortedSubset of A;

coherence
for b₁ being ManySortedSubset of A holds b₁ is V39() by PBOOLE:def 18, Th18;

end;

registration

let I be set ;
let A, B be V39() ManySortedSet of I;

cluster A (\/) B -> V39() ;

coherence
A (\/) B is finite-yielding

proof end;

end;

registration

let I be set ;
let A be ManySortedSet of I;
let B be V39() ManySortedSet of I;

cluster A (/\) B -> V39() ;

coherence
A (/\) B is finite-yielding

proof end;

end;

registration

let I be set ;
let B be ManySortedSet of I;
let A be V39() ManySortedSet of I;

cluster A (/\) B -> V39() ;

coherence
A (/\) B is finite-yielding ;

end;

registration

let I be set ;
let B be ManySortedSet of I;
let A be V39() ManySortedSet of I;

cluster A (\) B -> V39() ;

coherence
A (\) B is finite-yielding

proof end;

end;

registration

let I be set ;
let F be ManySortedFunction of I;
let A be V39() ManySortedSet of I;

cluster F .:.: A -> V39() ;

coherence
F .:.: A is finite-yielding

proof end;

end;

registration

let I be set ;
let A, B be V39() ManySortedSet of I;

cluster [|A,B|] -> V39() ;

coherence
[|A,B|] is finite-yielding

proof end;

end;

theorem :: MSSUBFAM:19

for I being set
for A, B being ManySortedSet of I st B is V8() & [|A,B|] is V39() holds
A is V39()

proof end;

theorem :: MSSUBFAM:20

for I being set
for A, B being ManySortedSet of I st A is V8() & [|A,B|] is V39() holds
B is V39()

proof end;

theorem Th21: :: MSSUBFAM:21

for I being set
for A being ManySortedSet of I holds
( A is V39() iff bool A is V39() )

proof end;

registration

let I be set ;
let M be V39() ManySortedSet of I;

cluster bool M -> V39() ;

coherence
bool M is finite-yielding by Th21;

end;

theorem :: MSSUBFAM:22

for I being set
for A being V8() ManySortedSet of I st A is V39() & ( for M being ManySortedSet of I st M in A holds
M is V39() ) holds
union A is V39()

proof end;

theorem :: MSSUBFAM:23

for I being set
for A being ManySortedSet of I st union A is V39() holds
( A is V39() & ( for M being ManySortedSet of I st M in A holds
M is V39() ) )

proof end;

theorem :: MSSUBFAM:24

for I being set
for F being ManySortedFunction of I st doms F is V39() holds
rngs F is V39()

proof end;

theorem :: MSSUBFAM:25

for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I st A c= rngs F & ( for i being set
for f being Function st i in I & f = F . i holds
f " (A . i) is finite ) holds
A is V39()

proof end;

registration

let I be set ;
let A, B be V39() ManySortedSet of I;

cluster (Funcs) (A,B) -> V39() ;

coherence
(Funcs) (A,B) is finite-yielding

proof end;

end;

registration

let I be set ;
let A, B be V39() ManySortedSet of I;

cluster A (\+\) B -> V39() ;

coherence
A (\+\) B is finite-yielding ;

end;

theorem :: MSSUBFAM:26

for I being set
for X, Y, Z being ManySortedSet of I st X is V39() & X c= [|Y,Z|] holds
ex A, B being ManySortedSet of I st
( A is V39() & A c= Y & B is V39() & B c= Z & X c= [|A,B|] )

proof end;

theorem :: MSSUBFAM:27

for I being set
for X, Y, Z being ManySortedSet of I st X is V39() & X c= [|Y,Z|] holds
ex A being ManySortedSet of I st
( A is V39() & A c= Y & X c= [|A,Z|] )

proof end;

theorem :: MSSUBFAM:28

for I being set
for M being V8() V39() ManySortedSet of I st ( for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds
B c= A ) holds
ex m being ManySortedSet of I st
( m in M & ( for K being ManySortedSet of I st K in M holds
m c= K ) )

proof end;

theorem :: MSSUBFAM:29

for I being set
for M being V8() V39() ManySortedSet of I st ( for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds
B c= A ) holds
ex m being ManySortedSet of I st
( m in M & ( for K being ManySortedSet of I st K in M holds
K c= m ) )

proof end;

theorem :: MSSUBFAM:30

for I being set
for F being ManySortedFunction of I
for Z being ManySortedSet of I st Z is V39() & Z c= rngs F holds
ex Y being ManySortedSet of I st
( Y c= doms F & Y is V39() & F .:.: Y = Z )

proof end;

definition

let I be set ;
let M be ManySortedSet of I;
mode MSSubsetFamily of M is ManySortedSubset of bool M;

end;

registration

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

cluster Relation-like V8() I -defined Function-like total for ManySortedSubset of bool M;

existence
not for b₁ being MSSubsetFamily of M holds b₁ is V8()

proof end;

end;

definition

let I be set ;
let M be ManySortedSet of I;
:: original: bool
redefine func bool M -> MSSubsetFamily of M;
coherence
bool M is MSSubsetFamily of M by PBOOLE:def 18;

end;

registration

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

cluster Relation-like V9() I -defined Function-like total V39() for ManySortedSubset of bool M;

existence
ex b₁ being MSSubsetFamily of M st
( b₁ is V9() & b₁ is V39() )

proof end;

end;

theorem :: MSSUBFAM:31

for I being set
for M being ManySortedSet of I holds EmptyMS I is V9() V39() MSSubsetFamily of M by PBOOLE:43, PBOOLE:def 18;

registration

let I be set ;
let M be V39() ManySortedSet of I;

cluster Relation-like V8() I -defined Function-like total V39() for ManySortedSubset of bool M;

existence
ex b₁ being MSSubsetFamily of M st
( b₁ is V8() & b₁ is V39() )

proof end;

end;

definition

let I be non empty set ;
let M be ManySortedSet of I;
let SF be MSSubsetFamily of M;
let i be Element of I;
:: original: .
redefine func SF . i -> Subset-Family of (M . i);
coherence
SF . i is Subset-Family of (M . i)

proof end;

end;

theorem Th32: :: MSSUBFAM:32

for I being set
for i being object
for M being ManySortedSet of I
for SF being MSSubsetFamily of M st i in I holds
SF . i is Subset-Family of (M . i)

proof end;

theorem Th33: :: MSSUBFAM:33

for I being set
for A, M being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF holds
A is ManySortedSubset of M

proof end;

theorem Th34: :: MSSUBFAM:34

for I being set
for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M holds SF (\/) SG is MSSubsetFamily of M

proof end;

theorem :: MSSUBFAM:35

for I being set
for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M holds SF (/\) SG is MSSubsetFamily of M

proof end;

theorem Th36: :: MSSUBFAM:36

for I being set
for A, M being ManySortedSet of I
for SF being MSSubsetFamily of M holds SF (\) A is MSSubsetFamily of M

proof end;

theorem :: MSSUBFAM:37

for I being set
for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M holds SF (\+\) SG is MSSubsetFamily of M

proof end;

theorem Th38: :: MSSUBFAM:38

for I being set
for A, M being ManySortedSet of I st A c= M holds
{A} is MSSubsetFamily of M

proof end;

theorem Th39: :: MSSUBFAM:39

for I being set
for A, B, M being ManySortedSet of I st A c= M & B c= M holds
{A,B} is MSSubsetFamily of M

proof end;

theorem Th40: :: MSSUBFAM:40

for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M holds union SF c= M

proof end;

definition

let I be set ;
let M be ManySortedSet of I;
let SF be MSSubsetFamily of M;

func meet SF -> ManySortedSet of I means :Def1: :: MSSUBFAM:def 1
for i being object st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & it . i = Intersect Q );

existence
ex b₁ being ManySortedSet of I st
for i being object st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & b₁ . i = Intersect Q )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of I st ( for i being object st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & b₁ . i = Intersect Q ) ) & ( for i being object st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & b₂ . i = Intersect Q ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines meet MSSUBFAM:def 1 :
for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M
for b₄ being ManySortedSet of I holds
( b₄ = meet SF iff for i being object st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & b₄ . i = Intersect Q ) );

definition

let I be set ;
let M be ManySortedSet of I;
let SF be MSSubsetFamily of M;
:: original: meet
redefine func meet SF -> ManySortedSubset of M;
coherence
meet SF is ManySortedSubset of M

proof end;

end;

theorem Th41: :: MSSUBFAM:41

for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M st SF = EmptyMS I holds
meet SF = M

proof end;

theorem :: MSSUBFAM:42

for I being set
for M being ManySortedSet of I
for SFe being V8() MSSubsetFamily of M holds meet SFe c= union SFe

proof end;

theorem :: MSSUBFAM:43

for I being set
for A, M being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF holds
meet SF c= A

proof end;

theorem :: MSSUBFAM:44

for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M st EmptyMS I in SF holds
meet SF = EmptyMS I

proof end;

theorem :: MSSUBFAM:45

for I being set
for Z, M being ManySortedSet of I
for SF being V8() MSSubsetFamily of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c= Z1 ) holds
Z c= meet SF

proof end;

theorem :: MSSUBFAM:46

for I being set
for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M st SF c= SG holds
meet SG c= meet SF

proof end;

theorem :: MSSUBFAM:47

for I being set
for A, B, M being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF & A c= B holds
meet SF c= B

proof end;

theorem :: MSSUBFAM:48

for I being set
for A, B, M being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF & A (/\) B = EmptyMS I holds
(meet SF) (/\) B = EmptyMS I

proof end;

theorem :: MSSUBFAM:49

for I being set
for M being ManySortedSet of I
for SF, SG, SH being MSSubsetFamily of M st SH = SF (\/) SG holds
meet SH = (meet SF) (/\) (meet SG)

proof end;

theorem :: MSSUBFAM:50

for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M
for V being ManySortedSubset of M st SF = {V} holds
meet SF = V

proof end;

theorem Th51: :: MSSUBFAM:51

for I being set
for M being ManySortedSet of I
for SF being MSSubsetFamily of M
for V, W being ManySortedSubset of M st SF = {V,W} holds
meet SF = V (/\) W

proof end;

theorem :: MSSUBFAM:52

for I being set
for A, M being ManySortedSet of I
for SF being MSSubsetFamily of M st A in meet SF holds
for B being ManySortedSet of I st B in SF holds
A in B

proof end;

theorem :: MSSUBFAM:53

for I being set
for A, M being ManySortedSet of I
for SF being V8() MSSubsetFamily of M st A in M & ( for B being ManySortedSet of I st B in SF holds
A in B ) holds
A in meet SF

proof end;

definition

let I be set ;
let M be ManySortedSet of I;
let IT be MSSubsetFamily of M;

attr IT is additive means :: MSSUBFAM:def 2
for A, B being ManySortedSet of I st A in IT & B in IT holds
A (\/) B in IT;

attr IT is absolutely-additive means :: MSSUBFAM:def 3
for F being MSSubsetFamily of M st F c= IT holds
union F in IT;

attr IT is multiplicative means :: MSSUBFAM:def 4
for A, B being ManySortedSet of I st A in IT & B in IT holds
A (/\) B in IT;

attr IT is absolutely-multiplicative means :: MSSUBFAM:def 5
for F being MSSubsetFamily of M st F c= IT holds
meet F in IT;

attr IT is properly-upper-bound means :: MSSUBFAM:def 6
M in IT;

attr IT is properly-lower-bound means :: MSSUBFAM:def 7
EmptyMS I in IT;

end;

:: deftheorem defines additive MSSUBFAM:def 2 :
for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is additive iff for A, B being ManySortedSet of I st A in IT & B in IT holds
A (\/) B in IT );

:: deftheorem defines absolutely-additive MSSUBFAM:def 3 :
for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is absolutely-additive iff for F being MSSubsetFamily of M st F c= IT holds
union F in IT );

:: deftheorem defines multiplicative MSSUBFAM:def 4 :
for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is multiplicative iff for A, B being ManySortedSet of I st A in IT & B in IT holds
A (/\) B in IT );

:: deftheorem defines absolutely-multiplicative MSSUBFAM:def 5 :
for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is absolutely-multiplicative iff for F being MSSubsetFamily of M st F c= IT holds
meet F in IT );

:: deftheorem defines properly-upper-bound MSSUBFAM:def 6 :
for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is properly-upper-bound iff M in IT );

:: deftheorem defines properly-lower-bound MSSUBFAM:def 7 :
for I being set
for M being ManySortedSet of I
for IT being MSSubsetFamily of M holds
( IT is properly-lower-bound iff EmptyMS I in IT );

Lm1: for I being set
for M being ManySortedSet of I holds
( bool M is additive & bool M is absolutely-additive & bool M is multiplicative & bool M is absolutely-multiplicative & bool M is properly-upper-bound & bool M is properly-lower-bound )

proof end;

registration

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

cluster Relation-like V8() I -defined Function-like total additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for ManySortedSubset of bool M;

existence
ex b₁ being MSSubsetFamily of M st
( b₁ is V8() & b₁ is additive & b₁ is absolutely-additive & b₁ is multiplicative & b₁ is absolutely-multiplicative & b₁ is properly-upper-bound & b₁ is properly-lower-bound )

proof end;

end;

definition

let I be set ;
let M be ManySortedSet of I;
:: original: bool
redefine func bool M -> additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound MSSubsetFamily of M;
coherence
bool M is additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound MSSubsetFamily of M by Lm1;

end;

registration

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

cluster absolutely-additive -> additive for ManySortedSubset of bool M;

coherence
for b₁ being MSSubsetFamily of M st b₁ is absolutely-additive holds
b₁ is additive

proof end;

end;

registration

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

cluster absolutely-multiplicative -> multiplicative for ManySortedSubset of bool M;

coherence
for b₁ being MSSubsetFamily of M st b₁ is absolutely-multiplicative holds
b₁ is multiplicative

proof end;

end;

registration

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

cluster absolutely-multiplicative -> properly-upper-bound for ManySortedSubset of bool M;

coherence
for b₁ being MSSubsetFamily of M st b₁ is absolutely-multiplicative holds
b₁ is properly-upper-bound

proof end;

end;

registration

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

cluster properly-upper-bound -> V8() for ManySortedSubset of bool M;

coherence
for b₁ being MSSubsetFamily of M st b₁ is properly-upper-bound holds
b₁ is V8()

proof end;

end;

registration

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

cluster absolutely-additive -> properly-lower-bound for ManySortedSubset of bool M;

coherence
for b₁ being MSSubsetFamily of M st b₁ is absolutely-additive holds
b₁ is properly-lower-bound

proof end;

end;

registration

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

cluster properly-lower-bound -> V8() for ManySortedSubset of bool M;

coherence
for b₁ being MSSubsetFamily of M st b₁ is properly-lower-bound holds
b₁ is V8()

proof end;

end;