environ
vocabularies HIDDEN, LATTICES, SUBSET_1, XBOOLE_0, PBOOLE, EQREL_1, CARD_FIL, STRUCT_0, TARSKI, ORDINAL1, ZFMISC_1, SETFAM_1, INT_2, XBOOLEAN, BINOP_1, REALSET1, FUNCT_1, RELAT_1, MCART_1, XXREAL_2, RELAT_2, FILTER_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, FUNCT_1, XTUPLE_0, MCART_1, ORDINAL1, RELAT_2, FUNCT_2, BINOP_1, REALSET1, STRUCT_0, LATTICES, DOMAIN_1, RELAT_1, RELSET_1, EQREL_1;
definitions TARSKI, XBOOLE_0, LATTICES, RELAT_1, RELAT_2;
theorems TARSKI, ZFMISC_1, SETFAM_1, FUNCT_1, MCART_1, FUNCT_2, LATTICES, RELAT_1, ORDERS_1, RLSUB_2, WELLSET1, RELSET_1, ORDINAL1, XBOOLE_0, XBOOLE_1, PARTFUN1, RELAT_2, SUBSET_1;
schemes RELAT_1, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICES;
constructors HIDDEN, SETFAM_1, RELAT_2, ORDINAL1, PARTFUN1, BINOP_1, REALSET1, LATTICES, RELSET_1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities LATTICES, BINOP_1, REALSET1, STRUCT_0;
expansions TARSKI, XBOOLE_0, LATTICES;
definition
let L be
Lattice;
let F be
Filter of
L;
uniqueness
for b1, b2 being Lattice st ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & b1 = LattStr(# F,o1,o2 #) ) & ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & b2 = LattStr(# F,o1,o2 #) ) holds
b1 = b2
;
existence
ex b1 being Lattice ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & b1 = LattStr(# F,o1,o2 #) )
end;
theorem
for
B being
B_Lattice for
FB being
Filter of
B for
I being
I_Lattice for
i,
j,
k being
Element of
I for
FI being
Filter of
I for
a,
b,
c being
Element of
B holds
( (
i,
j are_equivalence_wrt FI &
j,
k are_equivalence_wrt FI implies
i,
k are_equivalence_wrt FI ) & (
a,
b are_equivalence_wrt FB &
b,
c are_equivalence_wrt FB implies
a,
c are_equivalence_wrt FB ) )
by Th62;