:: WAYBEL27 semantic presentation

definition

let c₁ be Function;
attr a₁ is uncurrying means :Def1: :: WAYBEL27:def 1
( ( for b₁ being set st b₁ in dom a₁ holds
b₁ is Function-yielding Function ) & ( for b₁ being Function st b₁ in dom a₁ holds
a₁ . b₁ = uncurry b₁ ) );
attr a₁ is currying means :Def2: :: WAYBEL27:def 2
( ( for b₁ being set st b₁ in dom a₁ holds
( b₁ is Function & proj1 b₁ is Relation ) ) & ( for b₁ being Function st b₁ in dom a₁ holds
a₁ . b₁ = curry b₁ ) );
attr a₁ is commuting means :Def3: :: WAYBEL27:def 3
( ( for b₁ being set st b₁ in dom a₁ holds
b₁ is Function-yielding Function ) & ( for b₁ being Function st b₁ in dom a₁ holds
a₁ . b₁ = commute b₁ ) );

end;

:: deftheorem Def1 defines uncurrying WAYBEL27:def 1 :

:: deftheorem Def2 defines currying WAYBEL27:def 2 :

:: deftheorem Def3 defines commuting WAYBEL27:def 3 :

registration

cluster empty -> uncurrying currying commuting set ;
coherence

proof end;

end;

registration

cluster uncurrying currying commuting set ;
existence

proof end;

end;

registration

let c₁ be uncurrying Function;
let c₂ be set ;
cluster a₁ | a₂ -> uncurrying ;
coherence

proof end;

end;

registration

let c₁ be currying Function;
let c₂ be set ;
cluster a₁ | a₂ -> currying ;
coherence

proof end;

end;

theorem Th1: :: WAYBEL27:1

for b₁, b₂, b₃, b₄ being set st b₄ c= Funcs b₁,(Funcs b₂,b₃) holds
ex b₅ being ManySortedSet of b₄ st
( b₅ is uncurrying & rng b₅ c= Funcs [:b₁,b₂:],b₃ )

proof end;

theorem Th2: :: WAYBEL27:2

for b₁, b₂, b₃, b₄ being set st b₄ c= Funcs [:b₁,b₂:],b₃ holds
ex b₅ being ManySortedSet of b₄ st
( b₅ is currying & ( ( b₂ = {} implies b₁ = {} ) implies rng b₅ c= Funcs b₁,(Funcs b₂,b₃) ) )

proof end;

registration

let c₁, c₂, c₃ be set ;
cluster uncurrying ManySortedSet of Funcs a₁,(Funcs a₂,a₃);
existence

proof end;

cluster currying ManySortedSet of Funcs [:a₁,a₂:],a₃;
existence

proof end;

end;

theorem Th3: :: WAYBEL27:3

for b₁, b₂ being non empty set
for b₃ being set
for b₄, b₅ being commuting Function st dom b₄ c= Funcs b₁,(Funcs b₂,b₃) & rng b₄ c= dom b₅ holds
b₅ * b₄ = id (dom b₄)

proof end;

theorem Th4: :: WAYBEL27:4

for b₁ being non empty set
for b₂, b₃ being set
for b₄ being uncurrying Function
for b₅ being currying Function st dom b₄ c= Funcs b₂,(Funcs b₁,b₃) & rng b₄ c= dom b₅ holds
b₅ * b₄ = id (dom b₄)

proof end;

theorem Th5: :: WAYBEL27:5

for b₁, b₂, b₃ being set
for b₄ being currying Function
for b₅ being uncurrying Function st dom b₄ c= Funcs [:b₁,b₂:],b₃ & rng b₄ c= dom b₅ holds
b₅ * b₄ = id (dom b₄)

proof end;

theorem Th6: :: WAYBEL27:6

for b₁ being Function-yielding Function
for b₂, b₃ being set st b₂ in dom (commute b₁) holds
((commute b₁) . b₂) .: b₃ c= pi (b₁ .: b₃),b₂

proof end;

theorem Th7: :: WAYBEL27:7

for b₁ being Function-yielding Function
for b₂, b₃ being set st ( for b₄ being Function st b₄ in b₁ .: b₃ holds
b₂ in dom b₄ ) holds
pi (b₁ .: b₃),b₂ c= ((commute b₁) . b₂) .: b₃

proof end;

theorem Th8: :: WAYBEL27:8

for b₁, b₂ being set
for b₃ being Function st rng b₃ c= Funcs b₁,b₂ holds
for b₄, b₅ being set st b₄ in b₁ holds
((commute b₃) . b₄) .: b₅ = pi (b₃ .: b₅),b₄

proof end;

theorem Th9: :: WAYBEL27:9

for b₁ being Function
for b₂, b₃ being set st [:b₃,{b₂}:] c= dom b₁ holds
pi ((curry b₁) .: b₃),b₂ = b₁ .: [:b₃,{b₂}:]

proof end;

registration

let c₁ be set ;
let c₂ be non empty functional set ;
cluster -> Function-yielding M5(a₁,a₂);
coherence

proof end;

end;

registration

let c₁ be constituted-Functions 1-sorted ;
cluster the carrier of a₁ -> functional ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be non empty RelStr ;
cluster a₂ |^ a₁ -> constituted-Functions ;
coherence ;

end;

registration

cluster strict complete constituted-Functions RelStr ;
existence

proof end;

cluster non empty constituted-Functions 1-sorted ;
existence

proof end;

end;

registration

let c₁ be non empty constituted-Functions RelStr ;
cluster non empty -> non empty constituted-Functions SubRelStr of a₁;
coherence

proof end;

end;

theorem Th10: :: WAYBEL27:10

for b₁, b₂ being complete LATTICE
for b₃ being idempotent Function of b₂,b₂
for b₄ being Function of b₁,(Image b₃) holds b₃ * b₄ = b₄

proof end;

theorem Th11: :: WAYBEL27:11

for b₁, b₂, b₃ being non empty RelStr st b₂ is SubRelStr of b₃ holds
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ st b₄ is monotone & b₄ = b₅ holds
b₅ is monotone

proof end;

theorem Th12: :: WAYBEL27:12

for b₁, b₂, b₃ being non empty RelStr st b₂ is full SubRelStr of b₃ holds
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ st b₅ is monotone & b₄ = b₅ holds
b₄ is monotone

proof end;

theorem Th13: :: WAYBEL27:13

for b₁ being set
for b₂ being Subset of b₁ holds
( (chi b₂,b₁) " {1} = b₂ & (chi b₂,b₁) " {0} = b₁ \ b₂ )

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty RelStr ;
let c₃ be Element of (c₂ |^ c₁);
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> Element of a₂;
coherence

proof end;

end;

theorem Th14: :: WAYBEL27:14

for b₁ being non empty set
for b₂ being non empty RelStr
for b₃, b₄ being Element of (b₂ |^ b₁) holds
( b₃ <= b₄ iff for b₅ being Element of b₁ holds b₃ . b₅ <= b₄ . b₅ )

proof end;

theorem Th15: :: WAYBEL27:15

for b₁ being set
for b₂, b₃ being non empty RelStr st RelStr(# the carrier of b₂,the InternalRel of b₂ #) = RelStr(# the carrier of b₃,the InternalRel of b₃ #) holds
b₂ |^ b₁ = b₃ |^ b₁

proof end;

theorem Th16: :: WAYBEL27:16

for b₁, b₂, b₃, b₄ being non empty TopSpace st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & TopStruct(# the carrier of b₃,the topology of b₃ #) = TopStruct(# the carrier of b₄,the topology of b₄ #) holds
oContMaps b₁,b₃ = oContMaps b₂,b₄

proof end;

theorem Th17: :: WAYBEL27:17

for b₁ being set ex b₂ being Function of (BoolePoset b₁),((BoolePoset 1) |^ b₁) st
( b₂ is isomorphic & ( for b₃ being Subset of b₁ holds b₂ . b₃ = chi b₃,b₁ ) )

proof end;

theorem Th18: :: WAYBEL27:18

for b₁ being set holds BoolePoset b₁,(BoolePoset 1) |^ b₁ are_isomorphic

proof end;

theorem Th19: :: WAYBEL27:19

for b₁, b₂ being non empty set
for b₃ being non empty Poset
for b₄ being non empty full SubRelStr of (b₃ |^ b₁) |^ b₂
for b₅ being non empty full SubRelStr of (b₃ |^ b₂) |^ b₁
for b₆ being Function of b₄,b₅ st b₆ is commuting holds
b₆ is monotone

proof end;

theorem Th20: :: WAYBEL27:20

for b₁, b₂ being non empty set
for b₃ being non empty Poset
for b₄ being non empty full SubRelStr of (b₃ |^ b₂) |^ b₁
for b₅ being non empty full SubRelStr of b₃ |^ [:b₁,b₂:]
for b₆ being Function of b₄,b₅ st b₆ is uncurrying holds
b₆ is monotone

proof end;

theorem Th21: :: WAYBEL27:21

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be non empty reflexive antisymmetric RelStr ;
func UPS c₁,c₂ -> strict RelStr means :Def4: :: WAYBEL27:def 4
( a₃ is full SubRelStr of a₂ |^ the carrier of a₁ & ( for b₁ being set holds
( b₁ in the carrier of a₃ iff b₁ is directed-sups-preserving Function of a₁,a₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines UPS WAYBEL27:def 4 :

registration

let c₁ be non empty RelStr ;
let c₂ be non empty reflexive antisymmetric RelStr ;
cluster UPS a₁,a₂ -> non empty strict reflexive antisymmetric constituted-Functions ;
coherence

proof end;

end;

registration

let c₁ be non empty RelStr ;
let c₂ be non empty Poset;
cluster UPS a₁,a₂ -> non empty strict reflexive transitive antisymmetric constituted-Functions ;
coherence

proof end;

end;

theorem Th22: :: WAYBEL27:22

for b₁ being non empty RelStr
for b₂ being non empty reflexive antisymmetric RelStr holds the carrier of (UPS b₁,b₂) c= Funcs the carrier of b₁,the carrier of b₂

proof end;

definition

let c₁ be non empty RelStr ;
let c₂ be non empty reflexive antisymmetric RelStr ;
let c₃ be Element of (UPS c₁,c₂);
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> Element of a₂;
coherence

proof end;

end;

theorem Th23: :: WAYBEL27:23

for b₁ being non empty RelStr
for b₂ being non empty reflexive antisymmetric RelStr
for b₃, b₄ being Element of (UPS b₁,b₂) holds
( b₃ <= b₄ iff for b₅ being Element of b₁ holds b₃ . b₅ <= b₄ . b₅ )

proof end;

theorem Th24: :: WAYBEL27:24

for b₁, b₂ being Scott complete TopLattice holds UPS b₁,b₂ = SCMaps b₁,b₂

proof end;

theorem Th25: :: WAYBEL27:25

for b₁, b₂ being non empty RelStr
for b₃, b₄ being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & RelStr(# the carrier of b₃,the InternalRel of b₃ #) = RelStr(# the carrier of b₄,the InternalRel of b₄ #) holds
UPS b₁,b₃ = UPS b₂,b₄

proof end;

registration

let c₁, c₂ be complete LATTICE;
cluster UPS a₁,a₂ -> non empty strict reflexive transitive antisymmetric complete constituted-Functions ;
coherence

proof end;

end;

theorem Th26: :: WAYBEL27:26

for b₁, b₂ being complete LATTICE holds UPS b₁,b₂ is sups-inheriting SubRelStr of b₂ |^ the carrier of b₁

proof end;

theorem Th27: :: WAYBEL27:27

for b₁, b₂ being complete LATTICE
for b₃ being Subset of (UPS b₁,b₂) holds sup b₃ = "\/" b₃,(b₂ |^ the carrier of b₁)

proof end;

definition

let c₁, c₂, c₃, c₄ be non empty reflexive antisymmetric RelStr ;
let c₅ be Function of c₁,c₂;
assume E30: c₅ is directed-sups-preserving ;
let c₆ be Function of c₃,c₄;
assume E31: c₆ is directed-sups-preserving ;
func UPS c₅,c₆ -> Function of (UPS a₂,a₃),(UPS a₁,a₄) means :Def5: :: WAYBEL27:def 5
for b₁ being directed-sups-preserving Function of a₂,a₃ holds a₇ . b₁ = (a₆ * b₁) * a₅;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines UPS WAYBEL27:def 5 :

theorem Th28: :: WAYBEL27:28

for b₁, b₂, b₃, b₄, b₅, b₆ being non empty Poset
for b₇ being directed-sups-preserving Function of b₂,b₃
for b₈ being directed-sups-preserving Function of b₁,b₂
for b₉ being directed-sups-preserving Function of b₄,b₅
for b₁₀ being directed-sups-preserving Function of b₅,b₆ holds (UPS b₈,b₁₀) * (UPS b₇,b₉) = UPS (b₇ * b₈),(b₁₀ * b₉)

proof end;

theorem Th29: :: WAYBEL27:29

for b₁, b₂ being non empty reflexive antisymmetric RelStr holds UPS (id b₁),(id b₂) = id (UPS b₁,b₂)

proof end;

theorem Th30: :: WAYBEL27:30

for b₁, b₂, b₃, b₄ being complete LATTICE
for b₅ being directed-sups-preserving Function of b₁,b₂
for b₆ being directed-sups-preserving Function of b₃,b₄ holds UPS b₅,b₆ is directed-sups-preserving

proof end;

theorem Th31: :: WAYBEL27:31

Omega Sierpinski_Space is Scott

proof end;

theorem Th32: :: WAYBEL27:32

for b₁ being Scott complete TopLattice holds oContMaps b₁,Sierpinski_Space = UPS b₁,(BoolePoset 1)

proof end;

theorem Th33: :: WAYBEL27:33

for b₁ being complete LATTICE ex b₂ being Function of (UPS b₁,(BoolePoset 1)),(InclPoset (sigma b₁)) st
( b₂ is isomorphic & ( for b₃ being directed-sups-preserving Function of b₁,(BoolePoset 1) holds b₂ . b₃ = b₃ " {1} ) )

proof end;

theorem Th34: :: WAYBEL27:34

for b₁ being complete LATTICE holds UPS b₁,(BoolePoset 1), InclPoset (sigma b₁) are_isomorphic

proof end;

theorem Th35: :: WAYBEL27:35

for b₁, b₂, b₃, b₄ being complete LATTICE
for b₅ being Function of b₁,b₂
for b₆ being Function of b₃,b₄ st b₅ is isomorphic & b₆ is isomorphic holds
UPS b₅,b₆ is isomorphic

proof end;

theorem Th36: :: WAYBEL27:36

for b₁, b₂, b₃, b₄ being complete LATTICE st b₁,b₂ are_isomorphic & b₃,b₄ are_isomorphic holds
UPS b₂,b₃, UPS b₁,b₄ are_isomorphic

proof end;

theorem Th37: :: WAYBEL27:37

for b₁, b₂ being complete LATTICE
for b₃ being directed-sups-preserving projection Function of b₂,b₂ holds Image (UPS (id b₁),b₃) = UPS b₁,(Image b₃)

proof end;

E40: now

let c₁ be non empty set ;
let c₂, c₃ be non empty Poset;
let c₄ be directed-sups-preserving Function of c₂,(c₃ |^ c₁);
the carrier of (c₃ |^ c₁) = Funcs c₁,the carrier of c₃ by YELLOW_1:28;
then ( dom c₄ = the carrier of c₂ & rng c₄ c= Funcs c₁,the carrier of c₃ ) by FUNCT_2:def 1;
hence c₄ in Funcs the carrier of c₂,(Funcs c₁,the carrier of c₃) by FUNCT_2:def 2;
then commute c₄ in Funcs c₁,(Funcs the carrier of c₂,the carrier of c₃) by FUNCT_6:85;
then ex b₁ being Function st
( commute c₄ = b₁ & dom b₁ = c₁ & rng b₁ c= Funcs the carrier of c₂,the carrier of c₃ ) by FUNCT_2:def 2;
hence ( rng (commute c₄) c= Funcs the carrier of c₂,the carrier of c₃ & dom (commute c₄) = c₁ ) ;

end;

theorem Th38: :: WAYBEL27:38

for b₁ being non empty set
for b₂, b₃ being non empty Poset
for b₄ being directed-sups-preserving Function of b₂,(b₃ |^ b₁)
for b₅ being Element of b₁ holds (commute b₄) . b₅ is directed-sups-preserving Function of b₂,b₃

proof end;

theorem Th39: :: WAYBEL27:39

for b₁ being non empty set
for b₂, b₃ being non empty Poset
for b₄ being directed-sups-preserving Function of b₂,(b₃ |^ b₁) holds commute b₄ is Function of b₁,the carrier of (UPS b₂,b₃)

proof end;

theorem Th40: :: WAYBEL27:40

for b₁ being non empty set
for b₂, b₃ being non empty Poset
for b₄ being Function of b₁,the carrier of (UPS b₂,b₃) holds commute b₄ is directed-sups-preserving Function of b₂,(b₃ |^ b₁)

proof end;

theorem Th41: :: WAYBEL27:41

for b₁ being non empty set
for b₂, b₃ being non empty Poset ex b₄ being Function of (UPS b₂,(b₃ |^ b₁)),((UPS b₂,b₃) |^ b₁) st
( b₄ is commuting & b₄ is isomorphic )

proof end;

theorem Th42: :: WAYBEL27:42

for b₁ being non empty set
for b₂, b₃ being non empty Poset holds UPS b₂,(b₃ |^ b₁),(UPS b₂,b₃) |^ b₁ are_isomorphic

proof end;

theorem Th43: :: WAYBEL27:43

for b₁, b₂ being complete continuous LATTICE holds UPS b₁,b₂ is continuous

proof end;

theorem Th44: :: WAYBEL27:44

for b₁, b₂ being algebraic complete LATTICE holds UPS b₁,b₂ is algebraic

proof end;

theorem Th45: :: WAYBEL27:45

for b₁, b₂, b₃ being complete LATTICE
for b₄ being directed-sups-preserving Function of b₁,(UPS b₂,b₃) holds uncurry b₄ is directed-sups-preserving Function of [:b₁,b₂:],b₃

proof end;

theorem Th46: :: WAYBEL27:46

for b₁, b₂, b₃ being complete LATTICE
for b₄ being directed-sups-preserving Function of [:b₁,b₂:],b₃ holds curry b₄ is directed-sups-preserving Function of b₁,(UPS b₂,b₃)

proof end;

theorem Th47: :: WAYBEL27:47

for b₁, b₂, b₃ being complete LATTICE ex b₄ being Function of (UPS b₁,(UPS b₂,b₃)),(UPS [:b₁,b₂:],b₃) st
( b₄ is uncurrying & b₄ is isomorphic )

proof end;