:: 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 b₁ being DoubleIndexedSet of K,D holds b₁ 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 b₁ being Function of (dom F), the carrier of L st
for x being set st x in dom F holds
b₁ . x = \\/ ((F . x),L)

proof end;

uniqueness
for b₁, b₂ being Function of (dom F), the carrier of L st ( for x being set st x in dom F holds
b₁ . x = \\/ ((F . x),L) ) & ( for x being set st x in dom F holds
b₂ . x = \\/ ((F . x),L) ) holds
b₁ = b₂

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 b₁ being Function of (dom F), the carrier of L st
for x being set st x in dom F holds
b₁ . x = //\ ((F . x),L)

proof end;

uniqueness
for b₁, b₂ being Function of (dom F), the carrier of L st ( for x being set st x in dom F holds
b₁ . x = //\ ((F . x),L) ) & ( for x being set st x in dom F holds
b₂ . x = //\ ((F . x),L) ) holds
b₁ = b₂

proof end;

end;

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

:: deftheorem Def2 defines /\\ WAYBEL_5:def 2 :
for L being non empty RelStr
for F being Function-yielding Function
for b₃ being Function of (dom F), the carrier of L holds
( b₃ = /\\ (F,L) iff for x being set st x in dom F holds
b₃ . 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 b₁ being non empty Poset st b₁ is trivial holds
b₁ is completely-distributive

proof end;

end;

registration

cluster non empty total reflexive transitive antisymmetric with_suprema with_infima completely-distributive RelStr ;
existence
ex b₁ being LATTICE st b₁ 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 b₁ being LATTICE st b₁ is completely-distributive holds
( b₁ is complete & b₁ 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 b₁ being LATTICE st b₁ is completely-distributive holds
b₁ 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 b₁ being J -defined Function st b₁ = J => y holds
b₁ 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;