:: MSSUBFAM semantic presentation

definition

let c₁ be set ;
let c₂ be ManySortedFunction of c₁;
redefine func doms as doms c₂ -> ManySortedSet of a₁;
coherence

proof end;

redefine func rngs as rngs c₂ -> ManySortedSet of a₁;
coherence

proof end;

end;

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

ex b₁ being ManySortedFunction of F₂(),F₃() st
for b₂ being set st b₂ in F₁() holds
ex b₃ being Function of F₂() . b₂,F₃() . b₂ st
( b₃ = b₁ . b₂ & ( for b₄ being set st b₄ in F₂() . b₂ holds
P₁[b₃ . b₄,b₄,b₂] ) )

provided

E1: for b₁ being set st b₁ in F₁() holds
for b₂ being set st b₂ in F₂() . b₁ holds
ex b₃ being set st
( b₃ in F₃() . b₁ & P₁[b₃,b₂,b₁] )

proof end;

theorem Th1: :: MSSUBFAM:1

for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ <> {} holds
Intersect b₂ c= union b₂

proof end;

theorem Th2: :: MSSUBFAM:2

for b₁, b₂ being set
for b₃ being Subset-Family of b₁ st b₂ in b₃ holds
Intersect b₃ c= b₂

proof end;

theorem Th3: :: MSSUBFAM:3

for b₁ being set
for b₂ being Subset-Family of b₁ st {} in b₂ holds
Intersect b₂ = {}

proof end;

theorem Th4: :: MSSUBFAM:4

for b₁ being set
for b₂ being Subset-Family of b₁
for b₃ being Subset of b₁ st ( for b₄ being set st b₄ in b₂ holds
b₃ c= b₄ ) holds
b₃ c= Intersect b₂

proof end;

theorem Th5: :: MSSUBFAM:5

for b₁, b₂ being set
for b₃ being Subset-Family of b₁ st b₃ <> {} & ( for b₄ being set st b₄ in b₃ holds
b₂ c= b₄ ) holds
b₂ c= Intersect b₃

proof end;

theorem Th6: :: MSSUBFAM:6

for b₁, b₂, b₃ being set
for b₄ being Subset-Family of b₁ st b₂ in b₄ & b₂ c= b₃ holds
Intersect b₄ c= b₃

proof end;

theorem Th7: :: MSSUBFAM:7

for b₁, b₂, b₃ being set
for b₄ being Subset-Family of b₁ st b₂ in b₄ & b₂ misses b₃ holds
Intersect b₄ misses b₃

proof end;

theorem Th8: :: MSSUBFAM:8

for b₁ being set
for b₂, b₃, b₄ being Subset-Family of b₁ st b₂ = b₃ \/ b₄ holds
Intersect b₂ = (Intersect b₃) /\ (Intersect b₄)

proof end;

theorem Th9: :: MSSUBFAM:9

for b₁ being set
for b₂ being Subset-Family of b₁
for b₃ being Subset of b₁ st b₂ = {b₃} holds
Intersect b₂ = b₃

proof end;

theorem Th10: :: MSSUBFAM:10

for b₁ being set
for b₂ being Subset-Family of b₁
for b₃, b₄ being Subset of b₁ st b₂ = {b₃,b₄} holds
Intersect b₂ = b₃ /\ b₄

proof end;

theorem Th11: :: MSSUBFAM:11

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ in b₃ holds
b₂ is Element of b₃

proof end;

theorem Th12: :: MSSUBFAM:12

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being V3 ManySortedSet of b₁ st b₂ is Element of b₃ holds
b₂ in b₃

proof end;

theorem Th13: :: MSSUBFAM:13

for b₁, b₂ being set
for b₃ being ManySortedFunction of b₂
for b₄ being Function st b₁ in b₂ & b₄ = b₃ . b₁ holds
(rngs b₃) . b₁ = rng b₄

proof end;

theorem Th14: :: MSSUBFAM:14

for b₁, b₂ being set
for b₃ being ManySortedFunction of b₂
for b₄ being Function st b₁ in b₂ & b₄ = b₃ . b₁ holds
(doms b₃) . b₁ = dom b₄

proof end;

theorem Th15: :: MSSUBFAM:15

for b₁ being set
for b₂, b₃ being ManySortedFunction of b₁ holds b₃ ** b₂ is ManySortedFunction of b₁

proof end;

theorem Th16: :: MSSUBFAM:16

for b₁ being set
for b₂ being V3 ManySortedSet of b₁
for b₃ being ManySortedFunction of b₂, [0] b₁ holds b₃ = [0] b₁

proof end;

theorem Th17: :: MSSUBFAM:17

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being ManySortedFunction of b₁ st b₂ is_transformable_to b₃ & b₄ is ManySortedFunction of b₂,b₃ holds
( doms b₄ = b₂ & rngs b₄ c= b₃ )

proof end;

registration

let c₁ be set ;
cluster V4 -> locally-finite ManySortedSet of a₁;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster [0] a₁ -> V4 locally-finite ;
coherence ;

end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster V4 locally-finite ManySortedSubset of a₂;
existence

proof end;

end;

theorem Th18: :: MSSUBFAM:18

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ c= b₃ & b₃ is locally-finite holds
b₂ is locally-finite

proof end;

registration

let c₁ be set ;
let c₂ be locally-finite ManySortedSet of c₁;
cluster -> locally-finite ManySortedSubset of a₂;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂, c₃ be locally-finite ManySortedSet of c₁;
cluster a₂ \/ a₃ -> locally-finite ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be locally-finite ManySortedSet of c₁;
cluster a₂ /\ a₃ -> locally-finite ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be locally-finite ManySortedSet of c₁;
cluster a₃ /\ a₂ -> locally-finite ;
coherence ;

end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be locally-finite ManySortedSet of c₁;
cluster a₃ \ a₂ -> locally-finite ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be ManySortedFunction of c₁;
let c₃ be locally-finite ManySortedSet of c₁;
cluster a₂ .:.: a₃ -> locally-finite ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂, c₃ be locally-finite ManySortedSet of c₁;
cluster [|a₂,a₃|] -> locally-finite ;
coherence

proof end;

end;

theorem Th19: :: MSSUBFAM:19

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ is non-empty & [|b₃,b₂|] is locally-finite holds
b₃ is locally-finite

proof end;

theorem Th20: :: MSSUBFAM:20

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ is non-empty & [|b₂,b₃|] is locally-finite holds
b₃ is locally-finite

proof end;

theorem Th21: :: MSSUBFAM:21

for b₁ being set
for b₂ being ManySortedSet of b₁ holds
( b₂ is locally-finite iff bool b₂ is locally-finite )

proof end;

registration

let c₁ be set ;
let c₂ be locally-finite ManySortedSet of c₁;
cluster bool a₂ -> locally-finite ;
coherence by Th21;

end;

theorem Th22: :: MSSUBFAM:22

for b₁ being set
for b₂ being V3 ManySortedSet of b₁ st b₂ is locally-finite & ( for b₃ being ManySortedSet of b₁ st b₃ in b₂ holds
b₃ is locally-finite ) holds
union b₂ is locally-finite

proof end;

theorem Th23: :: MSSUBFAM:23

for b₁ being set
for b₂ being ManySortedSet of b₁ st union b₂ is locally-finite holds
( b₂ is locally-finite & ( for b₃ being ManySortedSet of b₁ st b₃ in b₂ holds
b₃ is locally-finite ) )

proof end;

theorem Th24: :: MSSUBFAM:24

for b₁ being set
for b₂ being ManySortedFunction of b₁ st doms b₂ is locally-finite holds
rngs b₂ is locally-finite

proof end;

theorem Th25: :: MSSUBFAM:25

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being ManySortedFunction of b₁ st b₂ c= rngs b₃ & ( for b₄ being set
for b₅ being Function st b₄ in b₁ & b₅ = b₃ . b₄ holds
b₅ " (b₂ . b₄) is finite ) holds
b₂ is locally-finite

proof end;

registration

let c₁ be set ;
let c₂, c₃ be locally-finite ManySortedSet of c₁;
cluster MSFuncs a₂,a₃ -> locally-finite ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂, c₃ be locally-finite ManySortedSet of c₁;
cluster a₂ \+\ a₃ -> locally-finite ;
coherence ;

end;

theorem Th26: :: MSSUBFAM:26

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ is locally-finite & b₂ c= [|b₃,b₄|] holds
ex b₅, b₆ being ManySortedSet of b₁ st
( b₅ is locally-finite & b₅ c= b₃ & b₆ is locally-finite & b₆ c= b₄ & b₂ c= [|b₅,b₆|] )

proof end;

theorem Th27: :: MSSUBFAM:27

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ is locally-finite & b₃ is locally-finite & b₂ c= [|b₄,b₃|] holds
ex b₅ being ManySortedSet of b₁ st
( b₅ is locally-finite & b₅ c= b₄ & b₂ c= [|b₅,b₃|] )

proof end;

theorem Th28: :: MSSUBFAM:28

for b₁ being set
for b₂ being V3 locally-finite ManySortedSet of b₁ st ( for b₃, b₄ being ManySortedSet of b₁ st b₃ in b₂ & b₄ in b₂ & not b₃ c= b₄ holds
b₄ c= b₃ ) holds
ex b₃ being ManySortedSet of b₁ st
( b₃ in b₂ & ( for b₄ being ManySortedSet of b₁ st b₄ in b₂ holds
b₃ c= b₄ ) )

proof end;

theorem Th29: :: MSSUBFAM:29

proof end;

theorem Th30: :: MSSUBFAM:30

for b₁ being set
for b₂ being ManySortedFunction of b₁
for b₃ being ManySortedSet of b₁ st b₃ is locally-finite & b₃ c= rngs b₂ holds
ex b₄ being ManySortedSet of b₁ st
( b₄ c= doms b₂ & b₄ is locally-finite & b₂ .:.: b₄ = b₃ )

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
mode MSSubsetFamily of a₂ is ManySortedSubset of bool a₂;

end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster V3 ManySortedSubset of bool a₂;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
redefine func bool as bool c₂ -> MSSubsetFamily of a₂;
coherence by PBOOLE:def 23;

end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster V4 locally-finite ManySortedSubset of bool a₂;
existence

proof end;

end;

theorem Th31: :: MSSUBFAM:31

for b₁ being set
for b₂ being ManySortedSet of b₁ holds [0] b₁ is V4 locally-finite MSSubsetFamily of b₂

proof end;

registration

let c₁ be set ;
let c₂ be locally-finite ManySortedSet of c₁;
cluster V3 locally-finite ManySortedSubset of bool a₂;
existence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be ManySortedSet of c₁;
let c₃ be MSSubsetFamily of c₂;
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> Subset-Family of (a₂ . a₄);
coherence

proof end;

end;

theorem Th32: :: MSSUBFAM:32

for b₁, b₂ being set
for b₃ being ManySortedSet of b₂
for b₄ being MSSubsetFamily of b₃ st b₁ in b₂ holds
b₄ . b₁ is Subset-Family of (b₃ . b₁)

proof end;

theorem Th33: :: MSSUBFAM:33

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being MSSubsetFamily of b₃ st b₂ in b₄ holds
b₂ is ManySortedSubset of b₃

proof end;

theorem Th34: :: MSSUBFAM:34

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being MSSubsetFamily of b₂ holds b₃ \/ b₄ is MSSubsetFamily of b₂

proof end;

theorem Th35: :: MSSUBFAM:35

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being MSSubsetFamily of b₂ holds b₃ /\ b₄ is MSSubsetFamily of b₂

proof end;

theorem Th36: :: MSSUBFAM:36

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being MSSubsetFamily of b₃ holds b₄ \ b₂ is MSSubsetFamily of b₃

proof end;

theorem Th37: :: MSSUBFAM:37

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being MSSubsetFamily of b₂ holds b₃ \+\ b₄ is MSSubsetFamily of b₂

proof end;

theorem Th38: :: MSSUBFAM:38

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ c= b₃ holds
{b₂} is MSSubsetFamily of b₃

proof end;

theorem Th39: :: MSSUBFAM:39

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁ st b₂ c= b₃ & b₄ c= b₃ holds
{b₂,b₄} is MSSubsetFamily of b₃

proof end;

theorem Th40: :: MSSUBFAM:40

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being MSSubsetFamily of b₂ holds union b₃ c= b₂

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be MSSubsetFamily of c₂;
canceled;
func meet c₃ -> ManySortedSet of a₁ means :Def2: :: MSSUBFAM:def 2
for b₁ being set st b₁ in a₁ holds
ex b₂ being Subset-Family of (a₂ . b₁) st
( b₂ = a₃ . b₁ & a₄ . b₁ = Intersect b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 MSSUBFAM:def 1 :

:: deftheorem Def2 defines meet MSSUBFAM:def 2 :

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be MSSubsetFamily of c₂;
redefine func meet as meet c₃ -> ManySortedSubset of a₂;
coherence

proof end;

end;

theorem Th41: :: MSSUBFAM:41

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being MSSubsetFamily of b₂ st b₃ = [0] b₁ holds
meet b₃ = b₂

proof end;

theorem Th42: :: MSSUBFAM:42

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being V3 MSSubsetFamily of b₂ holds meet b₃ c= union b₃

proof end;

theorem Th43: :: MSSUBFAM:43

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being MSSubsetFamily of b₂ st b₃ in b₄ holds
meet b₄ c= b₃

proof end;

theorem Th44: :: MSSUBFAM:44

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being MSSubsetFamily of b₂ st [0] b₁ in b₃ holds
meet b₃ = [0] b₁

proof end;

theorem Th45: :: MSSUBFAM:45

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being V3 MSSubsetFamily of b₃ st ( for b₅ being ManySortedSet of b₁ st b₅ in b₄ holds
b₂ c= b₅ ) holds
b₂ c= meet b₄

proof end;

theorem Th46: :: MSSUBFAM:46

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being MSSubsetFamily of b₂ st b₃ c= b₄ holds
meet b₄ c= meet b₃

proof end;

theorem Th47: :: MSSUBFAM:47

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁
for b₅ being MSSubsetFamily of b₂ st b₃ in b₅ & b₃ c= b₄ holds
meet b₅ c= b₄

proof end;

theorem Th48: :: MSSUBFAM:48

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁
for b₅ being MSSubsetFamily of b₂ st b₃ in b₅ & b₃ /\ b₄ = [0] b₁ holds
(meet b₅) /\ b₄ = [0] b₁

proof end;

theorem Th49: :: MSSUBFAM:49

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄, b₅ being MSSubsetFamily of b₂ st b₃ = b₄ \/ b₅ holds
meet b₃ = (meet b₄) /\ (meet b₅)

proof end;

theorem Th50: :: MSSUBFAM:50

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being MSSubsetFamily of b₂
for b₄ being ManySortedSubset of b₂ st b₃ = {b₄} holds
meet b₃ = b₄

proof end;

theorem Th51: :: MSSUBFAM:51

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being MSSubsetFamily of b₂
for b₄, b₅ being ManySortedSubset of b₂ st b₃ = {b₄,b₅} holds
meet b₃ = b₄ /\ b₅

proof end;

theorem Th52: :: MSSUBFAM:52

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being MSSubsetFamily of b₂ st b₃ in meet b₄ holds
for b₅ being ManySortedSet of b₁ st b₅ in b₄ holds
b₃ in b₅

proof end;

theorem Th53: :: MSSUBFAM:53

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being V3 MSSubsetFamily of b₃ st b₂ in b₃ & ( for b₅ being ManySortedSet of b₁ st b₅ in b₄ holds
b₂ in b₅ ) holds
b₂ in meet b₄

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be MSSubsetFamily of c₂;
attr a₃ is additive means :: MSSUBFAM:def 3
for b₁, b₂ being ManySortedSet of a₁ st b₁ in a₃ & b₂ in a₃ holds
b₁ \/ b₂ in a₃;
attr a₃ is absolutely-additive means :Def4: :: MSSUBFAM:def 4
for b₁ being MSSubsetFamily of a₂ st b₁ c= a₃ holds
union b₁ in a₃;
attr a₃ is multiplicative means :: MSSUBFAM:def 5
for b₁, b₂ being ManySortedSet of a₁ st b₁ in a₃ & b₂ in a₃ holds
b₁ /\ b₂ in a₃;
attr a₃ is absolutely-multiplicative means :Def6: :: MSSUBFAM:def 6
for b₁ being MSSubsetFamily of a₂ st b₁ c= a₃ holds
meet b₁ in a₃;
attr a₃ is properly-upper-bound means :Def7: :: MSSUBFAM:def 7
a₂ in a₃;
attr a₃ is properly-lower-bound means :Def8: :: MSSUBFAM:def 8
[0] a₁ in a₃;

end;

:: deftheorem Def3 defines additive MSSUBFAM:def 3 :

:: deftheorem Def4 defines absolutely-additive MSSUBFAM:def 4 :

:: deftheorem Def5 defines multiplicative MSSUBFAM:def 5 :

:: deftheorem Def6 defines absolutely-multiplicative MSSUBFAM:def 6 :

:: deftheorem Def7 defines properly-upper-bound MSSUBFAM:def 7 :

:: deftheorem Def8 defines properly-lower-bound MSSUBFAM:def 8 :

Lemma19: for b₁ being set
for b₂ being ManySortedSet of b₁ holds
( bool b₂ is additive & bool b₂ is absolutely-additive & bool b₂ is multiplicative & bool b₂ is absolutely-multiplicative & bool b₂ is properly-upper-bound & bool b₂ is properly-lower-bound )

proof end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster V3 additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSubset of bool a₂;
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
redefine func bool as bool c₂ -> additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound MSSubsetFamily of a₂;
coherence by Lemma19;

end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster absolutely-additive -> additive ManySortedSubset of bool a₂;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster absolutely-multiplicative -> multiplicative ManySortedSubset of bool a₂;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster absolutely-multiplicative -> properly-upper-bound ManySortedSubset of bool a₂;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster properly-upper-bound -> V3 ManySortedSubset of bool a₂;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster absolutely-additive -> properly-lower-bound ManySortedSubset of bool a₂;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
cluster properly-lower-bound -> V3 ManySortedSubset of bool a₂;
coherence

proof end;

end;