environ
vocabularies HIDDEN, XBOOLE_0, TARSKI, ORDINAL1, SUBSET_1, LATTICES, CARD_FIL, FILTER_0, INT_2, PBOOLE, GROUP_6, FUNCT_1, STRUCT_0, EQREL_1, FUNCT_2, RELAT_1, WELLORD1, FILTER_1, XBOOLEAN, FINSUB_1, LATTICE2, SETWISEO, BINOP_1, FUNCOP_1, XXREAL_2, VECTSP_1, ZFMISC_1, SETFAM_1, LATTICE4;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, ORDINAL1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FINSUB_1, STRUCT_0, LATTICES, LATTICE2, FILTER_0, FUNCOP_1, SETWISEO, WELLORD1, FILTER_1;
definitions TARSKI, FILTER_0, LATTICES, XBOOLE_0;
theorems LATTICES, ZFMISC_1, FUNCT_2, FILTER_0, SETFAM_1, ORDERS_1, TARSKI, SETWISEO, LATTICE2, FUNCOP_1, FILTER_1, WELLORD1, RELAT_1, XBOOLE_1, FUNCT_1;
schemes FUNCT_2, SETWISEO, BINOP_2, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, LATTICES, LATTICE2;
constructors HIDDEN, WELLORD1, DOMAIN_1, SETWISEO, LATTICE2, FILTER_1, GRCAT_1, FUNCOP_1, RELSET_1, FILTER_0;
requirements HIDDEN, BOOLE, SUBSET;
equalities FILTER_0, LATTICES, STRUCT_0;
expansions TARSKI, FILTER_0, LATTICES;
theorem
for
X being
set st
X <> {} & ( for
Z being
set st
Z <> {} &
Z c= X &
Z is
c=-linear holds
ex
Y being
set st
(
Y in X & ( for
X1 being
set st
X1 in Z holds
X1 c= Y ) ) ) holds
ex
Y being
set st
(
Y in X & ( for
Z being
set st
Z in X &
Z <> Y holds
not
Y c= Z ) )
Lm1:
for 0L being lower-bounded Lattice
for f being Function of the carrier of 0L, the carrier of 0L holds FinJoin (({}. the carrier of 0L),f) = Bottom 0L
Lm2:
for 1L being upper-bounded Lattice
for f being Function of the carrier of 1L, the carrier of 1L holds FinMeet (({}. the carrier of 1L),f) = Top 1L
Lm3:
for DL being distributive upper-bounded Lattice
for B being Element of Fin the carrier of DL
for p being Element of DL
for f being UnOp of the carrier of DL holds the L_join of DL . (( the L_meet of DL $$ (B,f)),p) = the L_meet of DL $$ (B,( the L_join of DL [:] (f,p)))