:: WAYBEL_5 semantic presentation

Lm1: for L being continuous Semilattice
for x being Element of L holds
( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds
waybelow x c= I ) )

proof end;

Lm2: for L being up-complete Semilattice st ( for x being Element of L holds
( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds
waybelow x c= I ) ) ) holds
L is continuous

proof end;

theorem :: WAYBEL_5:1

for L being up-complete Semilattice holds
( L is continuous iff for x being Element of L holds
( waybelow x is Ideal of L & x <= sup (waybelow x) & ( for I being Ideal of L st x <= sup I holds
waybelow x c= I ) ) ) by Lm1, Lm2;

Lm3: for L being up-complete Semilattice st L is continuous holds
for x being Element of L ex I being Ideal of L st
( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) )

proof end;

Lm4: for L being up-complete Semilattice st ( for x being Element of L ex I being Ideal of L st
( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) ) ) holds
L is continuous

proof end;

theorem :: WAYBEL_5:2

for L being up-complete Semilattice holds
( L is continuous iff for x being Element of L ex I being Ideal of L st
( x <= sup I & ( for J being Ideal of L st x <= sup J holds
I c= J ) ) ) by Lm3, Lm4;

theorem :: WAYBEL_5:3

for L being lower-bounded continuous sup-Semilattice holds SupMap L has_a_lower_adjoint

proof end;

theorem :: WAYBEL_5:4

for L being lower-bounded up-complete LATTICE st SupMap L is upper_adjoint holds
L is continuous

proof end;

theorem :: WAYBEL_5:5

for L being complete Semilattice st SupMap L is infs-preserving & SupMap L is sups-preserving holds
SupMap L has_a_lower_adjoint

proof end;

definition

let J, D be set ;
let K be ManySortedSet of J;
mode DoubleIndexedSet of K,D is ManySortedFunction of K,J --> D;

end;

definition

let J be set ;
let K be ManySortedSet of J;
let S be 1-sorted ;
mode DoubleIndexedSet of K,S is DoubleIndexedSet of K,the carrier of S;

end;

theorem Th6: :: WAYBEL_5:6

for J, D being set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,D
for j being set st j in J holds
F . j is Function of K . j,D

proof end;

definition

let J, D be non empty set ;
let K be ManySortedSet of J;
let F be DoubleIndexedSet of K,D;
let j be Element of J;
:: original: .
redefine func F . j -> Function of K . j,D;
coherence by Th6;

end;

registration

let J, D be non empty set ;
let K be V7 ManySortedSet of J;
let F be DoubleIndexedSet of K,D;
let j be Element of J;
cluster rng (F . j) -> non empty ;
correctness

proof end;

end;

registration

let J be set ;
let D be non empty set ;
let K be V7 ManySortedSet of J;
cluster -> V7 ManySortedFunction of K,J --> D;
correctness

proof end;

end;

theorem Th7: :: WAYBEL_5:7

for F being Function-yielding Function
for f being set st f in dom (Frege F) holds
f is Function

proof end;

theorem Th8: :: WAYBEL_5:8

for F being Function-yielding Function
for f being Function st f in dom (Frege F) holds
( dom f = dom F & dom F = dom ((Frege F) . f) )

proof end;

theorem Th9: :: WAYBEL_5:9

for F being Function-yielding Function
for f being Function st f in dom (Frege F) holds
for i being set st i in dom F holds
( f . i in dom (F . i) & ((Frege F) . f) . i = (F . i) . (f . i) & (F . i) . (f . i) in rng ((Frege F) . f) )

proof end;

theorem Th10: :: WAYBEL_5:10

for J, D being set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,D
for f being Function st f in dom (Frege F) holds
(Frege F) . f is Function of J,D

proof end;

Lm5: for J, D being set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,D
for f being Function st f in dom (Frege F) holds
for j being set st j in J holds
( ((Frege F) . f) . j = (F . j) . (f . j) & (F . j) . (f . j) in rng ((Frege F) . f) )

proof end;

Lm6: for J being set
for K being ManySortedSet of J
for D being non empty set
for F being DoubleIndexedSet of K,D
for f being Function st f in dom (Frege F) holds
for j being set st j in J holds
f . j in K . j

proof end;

registration

let f be non-empty Function;
cluster doms f -> non-empty ;
correctness

proof end;

end;

definition

let J, D be set ;
let K be ManySortedSet of J;
let F be DoubleIndexedSet of K,D;
:: original: Frege
redefine func Frege F -> DoubleIndexedSet of (product (doms F)) --> J,D;
coherence

proof end;

end;

definition

let J, D be non empty set ;
let K be V7 ManySortedSet of J;
let F be DoubleIndexedSet of K,D;
let G be DoubleIndexedSet of (product (doms F)) --> J,D;
let f be Element of product (doms F);
:: original: .
redefine func G . f -> Function of J,D;
coherence

proof end;

end;

definition

let L be non empty RelStr ;
let F be Function-yielding Function;
func \// F,L -> Function of dom F,the carrier of L means :Def1: :: WAYBEL_5:def 1
for x being set st x in dom F holds
it . x = \\/ (F . x),L;
existence

proof end;

uniqueness

proof end;

func /\\ F,L -> Function of dom F,the carrier of L means :Def2: :: WAYBEL_5:def 2
for x being set st x in dom F holds
it . x = //\ (F . x),L;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines \// WAYBEL_5:def 1 :

:: deftheorem Def2 defines /\\ WAYBEL_5:def 2 :

notation

let J be set ;
let K be ManySortedSet of J;
let L be non empty RelStr ;
let F be DoubleIndexedSet of K,L;
synonym Sups F for \// K,J;
synonym Infs F for /\\ K,J;

end;

notation

let I, J be set ;
let L be non empty RelStr ;
let F be DoubleIndexedSet of I --> J,L;
synonym Sups F for \// J,I;
synonym Infs F for /\\ J,I;

end;

theorem Th11: :: WAYBEL_5:11

for L being non empty RelStr
for F, G being Function-yielding Function st dom F = dom G & ( for x being set st x in dom F holds
\\/ (F . x),L = \\/ (G . x),L ) holds
\// F,L = \// G,L

proof end;

theorem Th12: :: WAYBEL_5:12

for L being non empty RelStr
for F, G being Function-yielding Function st dom F = dom G & ( for x being set st x in dom F holds
//\ (F . x),L = //\ (G . x),L ) holds
/\\ F,L = /\\ G,L

proof end;

theorem Th13: :: WAYBEL_5:13

for y being set
for L being non empty RelStr
for F being Function-yielding Function holds
( ( y in rng (\// F,L) implies ex x being set st
( x in dom F & y = \\/ (F . x),L ) ) & ( ex x being set st
( x in dom F & y = \\/ (F . x),L ) implies y in rng (\// F,L) ) & ( y in rng (/\\ F,L) implies ex x being set st
( x in dom F & y = //\ (F . x),L ) ) & ( ex x being set st
( x in dom F & y = //\ (F . x),L ) implies y in rng (/\\ F,L) ) )

proof end;

theorem Th14: :: WAYBEL_5:14

for x being set
for L being non empty RelStr
for J being non empty set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,L holds
( ( x in rng (Sups ) implies ex j being Element of J st x = Sup ) & ( ex j being Element of J st x = Sup implies x in rng (Sups ) ) & ( x in rng (Infs ) implies ex j being Element of J st x = Inf ) & ( ex j being Element of J st x = Inf implies x in rng (Infs ) ) )

proof end;

registration

let J be non empty set ;
let K be ManySortedSet of J;
let L be non empty RelStr ;
let F be DoubleIndexedSet of K,L;
cluster rng (Sups ) -> non empty ;
correctness

proof end;

cluster rng (Infs ) -> non empty ;
correctness

proof end;

end;

Lm7: for L being complete LATTICE
for J being non empty set
for K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L
for f being set holds
( f is Element of product (doms F) iff f in dom (Frege F) )

proof end;

theorem Th15: :: WAYBEL_5:15

for L being complete LATTICE
for a being Element of L
for F being Function-yielding Function st ( for f being Function st f in dom (Frege F) holds
//\ ((Frege F) . f),L <= a ) holds
Sup <= a

proof end;

theorem Th16: :: WAYBEL_5:16

for L being complete LATTICE
for J being non empty set
for K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf >= Sup

proof end;

theorem Th17: :: WAYBEL_5:17

for L being complete LATTICE
for a, b being Element of L st L is continuous & ( for c being Element of L st c << a holds
c <= b ) holds
a <= b

proof end;

Lm8: for L being complete LATTICE st L is continuous holds
for J being non empty set
for K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup

proof end;

theorem Th18: :: WAYBEL_5:18

for L being complete LATTICE st ( for J being non empty set st J in the_universe_of the carrier of L holds
for K being V7 ManySortedSet of J st ( for j being Element of J holds K . j in the_universe_of the carrier of L ) holds
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup ) holds
L is continuous

proof end;

Lm9: for L being complete LATTICE st ( for J being non empty set
for K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup ) holds
L is continuous

proof end;

theorem :: WAYBEL_5:19

for L being complete LATTICE holds
( L is continuous iff for J being non empty set
for K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup ) by Lm8, Lm9;

definition

let J, K, D be non empty set ;
let F be Function of [:J,K:],D;
:: original: curry
redefine func curry F -> DoubleIndexedSet of J --> K,D;
coherence

proof end;

end;

theorem Th20: :: WAYBEL_5:20

for J, K, D being non empty set
for j being Element of J
for k being Element of K
for F being Function of [:J,K:],D holds
( dom (curry F) = J & dom ((curry F) . j) = K & F . [j,k] = ((curry F) . j) . k )

proof end;

Lm10: for L being complete LATTICE st ( for J, K being non empty set
for F being Function of [:J,K:],the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds
Inf = Sup ) holds
L is continuous

proof end;

theorem :: WAYBEL_5:21

for L being complete LATTICE holds
( L is continuous iff for J, K being non empty set
for F being Function of [:J,K:],the carrier of L st ( for j being Element of J holds rng ((curry F) . j) is directed ) holds
Inf = Sup ) by Lm8, Lm10;

Lm11: for J, K being non empty set
for f being Function st f in Funcs J,(Fin K) holds
for j being Element of J holds f . j is finite Subset of K

proof end;

Lm12: for L being complete LATTICE
for J, K, D being non empty set
for j being Element of J
for F being Function of [:J,K:],D
for f being V7 ManySortedSet of J st f in Funcs J,(Fin K) holds
for G being DoubleIndexedSet of f,L st ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . [j,x] ) holds
rng (G . j) is finite Subset of (rng ((curry F) . j))

proof end;

theorem Th22: :: WAYBEL_5:22

for L being complete LATTICE
for J, K being non empty set
for F being Function of [:J,K:],the carrier of L
for X being Subset of L st X = { a where a is Element of L : ex f being V7 ManySortedSet of J st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . [j,x] ) & a = Inf ) ) } holds
Inf >= sup X

proof end;

Lm13: for L being complete LATTICE st L is continuous holds
for J, K being non empty set
for F being Function of [:J,K:],the carrier of L
for X being Subset of L st X = { a where a is Element of L : ex f being V7 ManySortedSet of J st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . [j,x] ) & a = Inf ) ) } holds
Inf = sup X

proof end;

Lm14: for L being complete LATTICE st ( for J, K being non empty set
for F being Function of [:J,K:],the carrier of L
for X being Subset of L st X = { a where a is Element of L : ex f being V7 ManySortedSet of J st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . [j,x] ) & a = Inf ) ) } holds
Inf = sup X ) holds
L is continuous

proof end;

theorem :: WAYBEL_5:23

for L being complete LATTICE holds
( L is continuous iff for J, K being non empty set
for F being Function of [:J,K:],the carrier of L
for X being Subset of L st X = { a where a is Element of L : ex f being V7 ManySortedSet of J st
( f in Funcs J,(Fin K) & ex G being DoubleIndexedSet of f,L st
( ( for j being Element of J
for x being set st x in f . j holds
(G . j) . x = F . [j,x] ) & a = Inf ) ) } holds
Inf = sup X ) by Lm13, Lm14;

definition

let L be non empty RelStr ;
attr L is completely-distributive means :Def3: :: WAYBEL_5:def 3
( L is complete & ( for J being non empty set
for K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf = Sup ) );

end;

:: deftheorem Def3 defines completely-distributive WAYBEL_5:def 3 :

registration

cluster non empty trivial -> non empty completely-distributive RelStr ;
coherence

proof end;

end;

registration

cluster completely-distributive RelStr ;
existence

proof end;

end;

theorem Th24: :: WAYBEL_5:24

for L being completely-distributive LATTICE holds L is continuous

proof end;

registration

cluster completely-distributive -> complete continuous RelStr ;
correctness by Def3, Th24;

end;

theorem Th25: :: WAYBEL_5:25

for L being non empty transitive antisymmetric with_infima RelStr
for x being Element of L
for X, Y being Subset of L st ex_sup_of X,L & ex_sup_of Y,L & Y = { (x "/\" y) where y is Element of L : y in X } holds
x "/\" (sup X) >= sup Y

proof end;

Lm15: for L being completely-distributive LATTICE
for X being non empty Subset of L
for x being Element of L holds x "/\" (sup X) = "\/" { (x "/\" y) where y is Element of L : y in X } ,L

proof end;

theorem Th26: :: WAYBEL_5:26

for L being completely-distributive LATTICE
for X being Subset of L
for x being Element of L holds x "/\" (sup X) = "\/" { (x "/\" y) where y is Element of L : y in X } ,L

proof end;

registration

cluster completely-distributive -> Heyting RelStr ;
correctness

proof end;

end;

definition

let L be non empty RelStr ;
mode CLSubFrame of L is non empty full infs-inheriting directed-sups-inheriting SubRelStr of L;

end;

theorem Th27: :: WAYBEL_5:27

for L being complete LATTICE
for J being non empty set
for K being V7 ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
rng (Infs ) is directed

proof end;

theorem :: WAYBEL_5:28

for L being complete LATTICE st L is continuous holds
for S being CLSubFrame of L holds S is continuous LATTICE

proof end;

theorem Th29: :: WAYBEL_5:29

for L being complete LATTICE
for S being non empty Poset st ex g being Function of L,S st
( g is infs-preserving & g is onto ) holds
S is complete LATTICE

proof end;

notation

let J, y be set ;
synonym J => y for J --> y;

end;

notation

let J, y be set ;
synonym J => y for J --> y;

end;

definition

let J, y be set ;
:: original: =>
redefine func J => y -> ManySortedSet of J;
coherence

proof end;

end;

definition

let A, B, J be set ;
let f be Function of A,B;
:: original: =>
redefine func J => f -> ManySortedFunction of J --> A,J --> B;
coherence

proof end;

end;

theorem Th30: :: WAYBEL_5:30

for J being non empty set
for A, B being set
for f being Function of A,B
for g being Function of B,A st g * f = id A holds
(J => g) ** (J => f) = id (J --> A)

proof end;

theorem Th31: :: WAYBEL_5:31

for J, A being non empty set
for B being set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,A
for f being Function of A,B holds (J => f) ** F is DoubleIndexedSet of K,B

proof end;

theorem Th32: :: WAYBEL_5:32

for J, A, B being non empty set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,A
for f being Function of A,B holds doms ((J => f) ** F) = doms F

proof end;

theorem :: WAYBEL_5:33

for L being complete LATTICE st L is continuous holds
for S being non empty Poset st ex g being Function of L,S st
( g is infs-preserving & g is directed-sups-preserving & g is onto ) holds
S is continuous LATTICE

proof end;