begin
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:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
begin
:: deftheorem Def1 defines is_FreeGen_set_of WAYBEL22:def 1 :
for S being non empty complete continuous Poset
for A being set holds
( A is_FreeGen_set_of S iff for T being non empty complete continuous Poset
for f being Function of A,the carrier of T ex h being CLHomomorphism of S,T st
( h | A = f & ( for h9 being CLHomomorphism of S,T st h9 | A = f holds
h9 = h ) ) );
theorem Th7:
theorem Th8:
begin
:: deftheorem defines FixedUltraFilters WAYBEL22:def 2 :
for X being set holds FixedUltraFilters X = { (uparrow x) where x is Element of (BoolePoset X) : ex z being Element of X st x = {z} } ;
theorem Th9:
theorem Th10:
theorem Th11:
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:
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 :
for X being set
for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X),the carrier of L
for b4 being Function of (InclPoset (Filt (BoolePoset X))),L holds
( b4 = f -extension_to_hom iff for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b4 . 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 );
theorem
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem