:: 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 b₄ being Function of (InclPoset (Filt (BoolePoset X))),L holds
( b₄ = f -extension_to_hom iff for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds b₄ . 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) );