:: Representation theorem for free continuous lattices
:: by Piotr Rudnicki
::
:: Received July 21, 1998
:: Copyright (c) 1998 Association of Mizar Users
Lm1:
for L being complete LATTICE
for X being set st X c= bool the carrier of L holds
"/\" (union X),L = "/\" { (inf Y) where Y is Subset of L : Y in X } ,L
Lm2:
for L being complete LATTICE
for X being set st X c= bool the carrier of L holds
"\/" (union X),L = "\/" { (sup Y) where Y is Subset of L : Y in X } ,L
theorem Th1: :: WAYBEL22:1
theorem Th2: :: WAYBEL22:2
theorem Th3: :: WAYBEL22:3
theorem Th4: :: WAYBEL22:4
theorem Th5: :: WAYBEL22:5
theorem Th6: :: WAYBEL22:6
:: deftheorem Def1 defines is_FreeGen_set_of WAYBEL22:def 1 :
theorem Th7: :: WAYBEL22:7
theorem Th8: :: WAYBEL22:8
:: deftheorem defines FixedUltraFilters WAYBEL22:def 2 :
theorem Th9: :: WAYBEL22:9
theorem Th10: :: WAYBEL22:10
theorem Th11: :: WAYBEL22:11
definition
let X be
set ;
let L be non
empty complete continuous Poset;
let f be
Function of
FixedUltraFilters X,the
carrier of
L;
func f -extension_to_hom -> Function of
(InclPoset (Filt (BoolePoset X))),
L means :
Def3:
:: WAYBEL22:def 3
for
Fi being
Element of
(InclPoset (Filt (BoolePoset X))) holds
it . Fi = "\/" { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in Fi } ,
L;
existence
ex b1 being Function of (InclPoset (Filt (BoolePoset X))),L st
for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b1 . Fi = "\/" { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in Fi } ,L
uniqueness
for b1, b2 being Function of (InclPoset (Filt (BoolePoset X))),L st ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b1 . Fi = "\/" { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in Fi } ,L ) & ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b2 . Fi = "\/" { ("/\" { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of X : Y in Fi } ,L ) holds
b1 = b2
end;
:: deftheorem Def3 defines -extension_to_hom WAYBEL22:def 3 :
theorem :: WAYBEL22:12
theorem Th13: :: WAYBEL22:13
theorem Th14: :: WAYBEL22:14
theorem Th15: :: WAYBEL22:15
theorem Th16: :: WAYBEL22:16
theorem Th17: :: WAYBEL22:17
theorem :: WAYBEL22:18