environ
vocabularies HIDDEN, ORDERS_2, CAT_1, YELLOW_0, STRUCT_0, TARSKI, WELLORD1, XBOOLE_0, FUNCT_1, FUNCT_2, RELAT_1, SUBSET_1, YELLOW_1, WAYBEL_0, XXREAL_0, LATTICES, RELAT_2, WAYBEL_1, GROUP_6, SEQM_3, WAYBEL_8, RCOMP_1, FINSET_1, LATTICE3, WAYBEL_3, ORDINAL2, YELLOW_2, CARD_FIL, BINOP_1, EQREL_1, REWRITE1, WAYBEL_6, ARYTM_0, INT_2, ARYTM_3, XBOOLEAN, WAYBEL_5, WAYBEL15;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, WELLORD1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, DOMAIN_1, STRUCT_0, ORDERS_2, QUANTAL1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_8;
definitions TARSKI;
theorems TARSKI, RELAT_1, WELLORD1, FUNCT_1, FUNCT_2, ORDERS_2, QUANTAL1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_5, YELLOW_6, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_8, WAYBEL13, XBOOLE_0, XBOOLE_1, WAYBEL14;
schemes FUNCT_2, SUBSET_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL10, SUBSET_1;
constructors HIDDEN, DOMAIN_1, TOLER_1, QUANTAL1, ORDERS_3, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_8, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities YELLOW_2, WAYBEL_1, STRUCT_0;
expansions WAYBEL_1;
Lm1:
for X being set
for Y, Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z st f is onto & g is onto holds
g * f is onto
by FUNCT_2:27;
Lm2:
for L being lower-bounded LATTICE st L is continuous holds
ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving )
Lm3:
for L being lower-bounded LATTICE st ex A being lower-bounded algebraic LATTICE ex g being Function of A,L st
( g is onto & g is infs-preserving & g is directed-sups-preserving ) holds
ex X being non empty set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic )
Lm4:
for L being LATTICE st ex X being set ex p being projection Function of (BoolePoset X),(BoolePoset X) st
( p is directed-sups-preserving & L, Image p are_isomorphic ) holds
L is continuous
Lm5:
for L being Boolean LATTICE st L is completely-distributive holds
( L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) )
Lm6:
for L being Boolean LATTICE st L is complete & ( for x being Element of L ex X being Subset of L st
( X c= ATOM L & x = sup X ) ) holds
ex Y being set st L, BoolePoset Y are_isomorphic