:: by Mariusz \.Zynel

::

:: Received October 25, 1996

:: Copyright (c) 1996-2018 Association of Mizar Users

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

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;

( 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:5

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

SupMap L is upper_adjoint

SupMap L is upper_adjoint

proof end;

:: Corollary 2.2 can be found in WAYBEL_4.

definition

let J, D be set ;

let K be ManySortedSet of J;

mode DoubleIndexedSet of K,D is ManySortedFunction of K,J --> D;

end;
let K be ManySortedSet of J;

mode DoubleIndexedSet of K,D is ManySortedFunction of K,J --> D;

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;
let K be ManySortedSet of J;

let S be 1-sorted ;

mode DoubleIndexedSet of K,S is DoubleIndexedSet of K, the carrier of S;

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

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

F . j is Function of (K . j),D by Th6;

end;
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

F . j is Function of (K . j),D by Th6;

registration

let J, D be non empty set ;

let K be V9() ManySortedSet of J;

let F be DoubleIndexedSet of K,D;

let j be Element of J;

correctness

coherence

not rng (F . j) is empty ;

;

end;
let K be V9() ManySortedSet of J;

let F be DoubleIndexedSet of K,D;

let j be Element of J;

correctness

coherence

not rng (F . j) is empty ;

;

registration

let J be set ;

let D be non empty set ;

let K be V9() ManySortedSet of J;

correctness

coherence

for b_{1} being DoubleIndexedSet of K,D holds b_{1} is V9();

end;
let D be non empty set ;

let K be V9() ManySortedSet of J;

correctness

coherence

for b

proof end;

theorem :: WAYBEL_5:7

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) )

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) )

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

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-yielding Function;

correctness

coherence

doms f is non-empty ;

end;
correctness

coherence

doms f is non-empty ;

proof 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

Frege F is DoubleIndexedSet of (product (doms F)) --> J,D

end;
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

Frege F is DoubleIndexedSet of (product (doms F)) --> J,D

proof end;

definition

let J, D be non empty set ;

let K be V9() 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

G . f is Function of J,D

end;
let K be V9() 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

G . f is Function of J,D

proof end;

definition

let L be non empty RelStr ;

let F be Function-yielding Function;

ex b_{1} being Function of (dom F), the carrier of L st

for x being object st x in dom F holds

b_{1} . x = \\/ ((F . x),L)

for b_{1}, b_{2} being Function of (dom F), the carrier of L st ( for x being object st x in dom F holds

b_{1} . x = \\/ ((F . x),L) ) & ( for x being object st x in dom F holds

b_{2} . x = \\/ ((F . x),L) ) holds

b_{1} = b_{2}

ex b_{1} being Function of (dom F), the carrier of L st

for x being object st x in dom F holds

b_{1} . x = //\ ((F . x),L)

for b_{1}, b_{2} being Function of (dom F), the carrier of L st ( for x being object st x in dom F holds

b_{1} . x = //\ ((F . x),L) ) & ( for x being object st x in dom F holds

b_{2} . x = //\ ((F . x),L) ) holds

b_{1} = b_{2}

end;
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 object st x in dom F holds

it . x = \\/ ((F . x),L);

existence for x being object st x in dom F holds

it . x = \\/ ((F . x),L);

ex b

for x being object st x in dom F holds

b

proof end;

uniqueness for b

b

b

b

proof end;

func /\\ (F,L) -> Function of (dom F), the carrier of L means :Def2: :: WAYBEL_5:def 2

for x being object st x in dom F holds

it . x = //\ ((F . x),L);

existence for x being object st x in dom F holds

it . x = //\ ((F . x),L);

ex b

for x being object st x in dom F holds

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for L being non empty RelStr

for F being Function-yielding Function

for b_{3} being Function of (dom F), the carrier of L holds

( b_{3} = \// (F,L) iff for x being object st x in dom F holds

b_{3} . x = \\/ ((F . x),L) );

for L being non empty RelStr

for F being Function-yielding Function

for b

( b

b

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

for L being non empty RelStr

for F being Function-yielding Function

for b_{3} being Function of (dom F), the carrier of L holds

( b_{3} = /\\ (F,L) iff for x being object st x in dom F holds

b_{3} . x = //\ ((F . x),L) );

for L being non empty RelStr

for F being Function-yielding Function

for b

( b

b

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;
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);

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;
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);

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 object st x in dom F holds

\\/ ((F . x),L) = \\/ ((G . x),L) ) holds

\// (F,L) = \// (G,L)

for F, G being Function-yielding Function st dom F = dom G & ( for x being object 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 object st x in dom F holds

//\ ((F . x),L) = //\ ((G . x),L) ) holds

/\\ (F,L) = /\\ (G,L)

for F, G being Function-yielding Function st dom F = dom G & ( for x being object 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 object

for L being non empty RelStr

for F being Function-yielding Function holds

( ( y in rng (\// (F,L)) implies ex x being object st

( x in dom F & y = \\/ ((F . x),L) ) ) & ( ex x being object st

( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) ) & ( y in rng (/\\ (F,L)) implies ex x being object st

( x in dom F & y = //\ ((F . x),L) ) ) & ( ex x being object st

( x in dom F & y = //\ ((F . x),L) ) implies y in rng (/\\ (F,L)) ) )

for L being non empty RelStr

for F being Function-yielding Function holds

( ( y in rng (\// (F,L)) implies ex x being object st

( x in dom F & y = \\/ ((F . x),L) ) ) & ( ex x being object st

( x in dom F & y = \\/ ((F . x),L) ) implies y in rng (\// (F,L)) ) & ( y in rng (/\\ (F,L)) implies ex x being object st

( x in dom F & y = //\ ((F . x),L) ) ) & ( ex x being object 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 object

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 ) ) )

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;

correctness

coherence

not rng (Sups ) is empty ;

;

correctness

coherence

not rng (Infs ) is empty ;

;

end;
let K be ManySortedSet of J;

let L be non empty RelStr ;

let F be DoubleIndexedSet of K,L;

correctness

coherence

not rng (Sups ) is empty ;

;

correctness

coherence

not rng (Infs ) is empty ;

;

Lm7: for L being complete LATTICE

for J being non empty set

for K being V9() 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

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 V9() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Inf >= Sup

for J being non empty set

for K being V9() 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

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 V9() 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 V9() 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

for K being V9() 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 V9() 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

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

curry F is DoubleIndexedSet of J --> K,D

end;
let F be Function of [:J,K:],D;

:: original: curry

redefine func curry F -> DoubleIndexedSet of J --> K,D;

coherence

curry F is DoubleIndexedSet of J --> K,D

proof 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 )

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

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 V9() 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 object 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 V9() 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 object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds

Inf >= sup X

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 V9() 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 object 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 V9() 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 object 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 V9() 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 object 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 V9() 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 object st x in f . j holds

(G . j) . x = F . (j,x) ) & a = Inf ) ) } holds

Inf = sup X ) by Lm13, Lm14;

( 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 V9() 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 object 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 ;

end;
attr L is completely-distributive means :Def3: :: WAYBEL_5:def 3

( L is complete & ( for J being non empty set

for K being V9() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Inf = Sup ) );

( L is complete & ( for J being non empty set

for K being V9() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Inf = Sup ) );

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

for L being non empty RelStr holds

( L is completely-distributive iff ( L is complete & ( for J being non empty set

for K being V9() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Inf = Sup ) ) );

for L being non empty RelStr holds

( L is completely-distributive iff ( L is complete & ( for J being non empty set

for K being V9() ManySortedSet of J

for F being DoubleIndexedSet of K,L holds Inf = Sup ) ) );

registration

for b_{1} being 1 -element Poset holds b_{1} is completely-distributive
end;

cluster 1 -element reflexive transitive antisymmetric -> 1 -element completely-distributive for Poset;

coherence for b

proof end;

registration

ex b_{1} being LATTICE st b_{1} is completely-distributive
end;

cluster non empty total reflexive transitive antisymmetric with_suprema with_infima completely-distributive for LATTICE;

existence ex b

proof end;

registration

coherence

for b_{1} being LATTICE st b_{1} is completely-distributive holds

( b_{1} is complete & b_{1} is continuous );

by Th24;

end;

cluster reflexive transitive antisymmetric with_suprema with_infima completely-distributive -> complete continuous for LATTICE;

correctness coherence

for b

( b

by Th24;

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

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)

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

coherence

for b_{1} being LATTICE st b_{1} is completely-distributive holds

b_{1} is Heyting ;

end;

cluster reflexive transitive antisymmetric with_suprema with_infima completely-distributive -> Heyting for LATTICE;

correctness coherence

for b

b

proof 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;
mode CLSubFrame of L is non empty full infs-inheriting directed-sups-inheriting SubRelStr of L;

theorem Th27: :: WAYBEL_5:27

for L being complete LATTICE

for J being non empty set

for K being V9() 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

for J being non empty set

for K being V9() 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

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

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;

registration

let J, y be set ;

coherence

for b_{1} being J -defined Function st b_{1} = J => y holds

b_{1} is total
;

end;
coherence

for b

b

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

J => f is ManySortedFunction of J --> A,J --> B

end;
let f be Function of A,B;

:: original: =>

redefine func J => f -> ManySortedFunction of J --> A,J --> B;

coherence

J => f is ManySortedFunction of J --> A,J --> B

proof 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)

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

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

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

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;