environ
vocabularies HIDDEN, REWRITE1, WAYBEL_0, TARSKI, ZFMISC_1, STRUCT_0, LATTICES, ORDINAL2, SUBSET_1, EQREL_1, XBOOLE_0, YELLOW_1, ARYTM_0, ORDERS_2, WAYBEL16, RELAT_1, YELLOW_0, LATTICE3, WAYBEL_5, WELLORD2, CARD_FIL, WELLORD1, CAT_1, SETFAM_1, XXREAL_0, FUNCT_1, CARD_1, SEQM_3, PBOOLE, FUNCOP_1, YELLOW_2, CARD_3, FUNCT_6, WAYBEL22, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_6, ORDERS_1, STRUCT_0, WELLORD1, CARD_1, CARD_3, ORDERS_2, LATTICE3, FUNCOP_1, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL16;
definitions TARSKI, FUNCT_1, ORDERS_3, LATTICE3, WELLORD2, YELLOW_0, WAYBEL_0;
theorems TARSKI, CARD_1, ZFMISC_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_4, FUNCT_6, FUNCOP_1, WELLORD1, WELLORD2, CARD_3, LATTICE3, PBOOLE, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1, WAYBEL_5, WAYBEL11, WAYBEL13, WAYBEL14, WAYBEL15, WAYBEL16, WAYBEL17, RELSET_1, WAYBEL_4, WAYBEL20, XBOOLE_0, XBOOLE_1, PARTFUN1;
schemes CLASSES1, FUNCT_2, MSSUBFAM, YELLOW_3;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FUNCOP_1, CARD_3, PBOOLE, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_5, YELLOW_7, WAYBEL_8, WAYBEL16, FUNCT_1, RELAT_1;
constructors HIDDEN, DOMAIN_1, TOLER_1, ORDERS_3, PRALG_3, WAYBEL_5, WAYBEL_8, WAYBEL16, RELSET_1, WAYBEL20;
requirements HIDDEN, SUBSET, BOOLE;
equalities LATTICE3, YELLOW_0, WAYBEL_0, STRUCT_0;
expansions FUNCT_1, LATTICE3, WELLORD2, WAYBEL_0;
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)
definition
let X be
set ;
let L be non
empty complete continuous Poset;
let f be
Function of
(FixedUltraFilters X), the
carrier of
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;