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 : 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 : 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 :
theorem Th7:
theorem Th8:
begin
:: deftheorem defines FixedUltraFilters WAYBEL22:def 2 :
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 holds
it . Fi = "\/" { ("/\" { (f . (uparrow x)) where x is Element of : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of : Y in Fi } ,
L;
existence
ex b1 being Function of (InclPoset (Filt (BoolePoset X))),L st
for Fi being Element of holds b1 . Fi = "\/" { ("/\" { (f . (uparrow x)) where x is Element of : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of : Y in Fi } ,L
uniqueness
for b1, b2 being Function of (InclPoset (Filt (BoolePoset X))),L st ( for Fi being Element of holds b1 . Fi = "\/" { ("/\" { (f . (uparrow x)) where x is Element of : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of : Y in Fi } ,L ) & ( for Fi being Element of holds b2 . Fi = "\/" { ("/\" { (f . (uparrow x)) where x is Element of : ex z being Element of X st
( x = {z} & z in Y ) } ,L) where Y is Subset of : Y in Fi } ,L ) holds
b1 = b2
end;
:: deftheorem Def3 defines -extension_to_hom WAYBEL22:def 3 :
theorem
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem