:: The Equational Characterization of Continuous Lattices
:: by Mariusz \.Zynel
::
:: Received October 25, 1996
:: Copyright (c) 1996 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 ) )
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
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 ) )
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
theorem :: WAYBEL_5:2
theorem :: WAYBEL_5:3
theorem :: WAYBEL_5:4
theorem :: WAYBEL_5:5
theorem Th6: :: WAYBEL_5:6
theorem Th7: :: WAYBEL_5:7
theorem Th8: :: WAYBEL_5:8
theorem Th9: :: WAYBEL_5:9
theorem Th10: :: WAYBEL_5:10
Lm5:
for J, D being set
for K being ManySortedSet of
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) )
Lm6:
for J being set
for K being ManySortedSet of
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
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
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
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
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
end;
:: deftheorem Def1 defines \// WAYBEL_5:def 1 :
:: deftheorem Def2 defines /\\ WAYBEL_5:def 2 :
theorem Th11: :: WAYBEL_5:11
theorem Th12: :: WAYBEL_5:12
theorem Th13: :: WAYBEL_5:13
theorem Th14: :: WAYBEL_5:14
Lm7:
for L being complete LATTICE
for J being non empty set
for K being V9() ManySortedSet of
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) )
theorem Th15: :: WAYBEL_5:15
theorem Th16: :: WAYBEL_5:16
theorem Th17: :: WAYBEL_5:17
Lm8:
for L being complete LATTICE st L is continuous holds
for J being non empty set
for K being V9() ManySortedSet of
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
Inf = Sup
theorem Th18: :: WAYBEL_5:18
Lm9:
for L being complete LATTICE st ( for J being non empty set
for K being V9() ManySortedSet of
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
theorem :: WAYBEL_5:19
theorem Th20: :: WAYBEL_5:20
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
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
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 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))
theorem Th22: :: WAYBEL_5:22
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 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
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 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
theorem :: WAYBEL_5:23
:: deftheorem Def3 defines completely-distributive WAYBEL_5:def 3 :
theorem Th24: :: WAYBEL_5:24
theorem Th25: :: WAYBEL_5:25
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
theorem Th26: :: WAYBEL_5:26
theorem Th27: :: WAYBEL_5:27
theorem :: WAYBEL_5:28
theorem Th29: :: WAYBEL_5:29
theorem Th30: :: WAYBEL_5:30
theorem Th31: :: WAYBEL_5:31
theorem Th32: :: WAYBEL_5:32
theorem :: WAYBEL_5:33