:: The Equational Characterization of Continuous Lattices
:: by Mariusz \.Zynel
::
:: Received October 25, 1996
:: Copyright (c) 1996-2011 Association of Mizar Users


begin

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 is upper_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 is upper_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
F . j is Function of (K . j),D
by Th6;
end;

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;
cluster proj2 (F . j) -> non empty ;
correctness
coherence
not rng (F . j) is empty
;
proof end;
end;

registration
let J be set ;
let D be non empty set ;
let K be V9() ManySortedSet of J;
cluster -> V9() ManySortedFunction of K,J --> D;
correctness
coherence
for b1 being DoubleIndexedSet of K,D holds b1 is non-empty
;
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
coherence
doms f is non-empty
;
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
Frege F is DoubleIndexedSet of (product (doms F)) --> J,D
proof end;
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
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
ex b1 being Function of (dom F), the carrier of L st
for x being set st x in dom F holds
b1 . x = \\/ ((F . x),L)
proof end;
uniqueness
for b1, b2 being Function of (dom F), the carrier of L st ( for x being set st x in dom F holds
b1 . x = \\/ ((F . x),L) ) & ( for x being set st x in dom F holds
b2 . x = \\/ ((F . x),L) ) holds
b1 = b2
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
ex b1 being Function of (dom F), the carrier of L st
for x being set st x in dom F holds
b1 . x = //\ ((F . x),L)
proof end;
uniqueness
for b1, b2 being Function of (dom F), the carrier of L st ( for x being set st x in dom F holds
b1 . x = //\ ((F . x),L) ) & ( for x being set st x in dom F holds
b2 . x = //\ ((F . x),L) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines \// WAYBEL_5:def 1 :
for L being non empty RelStr
for F being Function-yielding Function
for b3 being Function of (dom F), the carrier of L holds
( b3 = \// (F,L) iff for x being set st x in dom F holds
b3 . x = \\/ ((F . x),L) );

:: deftheorem Def2 defines /\\ WAYBEL_5:def 2 :
for L being non empty RelStr
for F being Function-yielding Function
for b3 being Function of (dom F), the carrier of L holds
( b3 = /\\ (F,L) iff for x being set st x in dom F holds
b3 . x = //\ ((F . x),L) );

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 proj2 (Sups ) -> non empty ;
correctness
coherence
not rng (Sups ) is empty
;
proof end;
cluster proj2 (Infs ) -> non empty ;
correctness
coherence
not rng (Infs ) is empty
;
proof end;
end;

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
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
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 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
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
for L being complete LATTICE holds
( L is continuous iff 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 ) 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
curry F is DoubleIndexedSet of J --> K,D
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 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 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 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 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 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 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 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 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 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 set st x in f . j holds
(G . j) . x = F . (j,x) ) & a = Inf ) )
}
holds
Inf = sup X ) by Lm13, Lm14;

begin

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 V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Inf = Sup ) );
end;

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

registration
cluster non empty trivial reflexive transitive antisymmetric -> non empty completely-distributive RelStr ;
coherence
for b1 being non empty Poset st b1 is trivial holds
b1 is completely-distributive
proof end;
end;

registration
cluster non empty total reflexive transitive antisymmetric with_suprema with_infima completely-distributive RelStr ;
existence
ex b1 being LATTICE st b1 is completely-distributive
proof end;
end;

theorem Th24: :: WAYBEL_5:24
for L being completely-distributive LATTICE holds L is continuous
proof end;

registration
cluster reflexive transitive antisymmetric with_suprema with_infima completely-distributive -> complete continuous RelStr ;
correctness
coherence
for b1 being LATTICE st b1 is completely-distributive holds
( b1 is complete & b1 is continuous )
;
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 reflexive transitive antisymmetric with_suprema with_infima completely-distributive -> Heyting RelStr ;
correctness
coherence
for b1 being LATTICE st b1 is completely-distributive holds
b1 is Heyting
;
proof end;
end;

begin

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

registration
let J, y be set ;
cluster J => y -> J -defined total J -defined Function;
coherence
for b1 being J -defined Function st b1 = J => y holds
b1 is total
;
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
J => f is ManySortedFunction of J --> A,J --> B
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;