environ
vocabularies HIDDEN, XBOOLE_0, SUBSET_1, BINOP_1, REALSET1, RELAT_1, ZFMISC_1, FUNCT_1, LATTICE2, LATTICES, STRUCT_0, EQREL_1, PBOOLE, LATTICE4, FILTER_0, CARD_FIL, CAT_1, TARSKI, INT_2, YELLOW11, LATTICE5, NAT_LAT, XBOOLEAN, XXREAL_2, FILTER_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1, DOMAIN_1, BINOP_1, REALSET1, LATTICES, NAT_LAT, FILTER_0, LATTICE2, MCART_1, LATTICE4;
definitions BINOP_1, LATTICES, LATTICE2, FILTER_0, TARSKI, XBOOLE_0;
theorems TARSKI, ZFMISC_1, DOMAIN_1, FUNCT_1, FUNCT_2, BINOP_1, SUBSET_1, NAT_LAT, LATTICES, FILTER_0, LATTICE2, RELSET_1, RELAT_1;
schemes ;
registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, STRUCT_0, LATTICES, FILTER_0, LATTICE2, NAT_LAT;
constructors HIDDEN, BINOP_1, REALSET1, FILTER_0, LATTICE2, NAT_LAT, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities BINOP_1, LATTICES, LATTICE2, FILTER_0, REALSET1;
expansions LATTICES, TARSKI, XBOOLE_0;
deffunc H1( LattStr ) -> set = the carrier of $1;
deffunc H2( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_join of $1;
deffunc H3( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_meet of $1;
Lm1:
for L being Lattice
for S being non empty Subset of L holds
( S is Ideal of L iff for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) )
Lm2:
for L1, L2 being Lattice
for D1 being non empty Subset of L1
for D2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 holds
( <.D1.) = <.D2.) & (.D1.> = (.D2.> )
Lm3:
for L1, L2 being Lattice
for D1, E1 being non empty Subset of L1
for D2, E2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 & E1 = E2 holds
D1 "/\" E1 = D2 "/\" E2
Lm4:
for B being B_Lattice
for a being Element of B holds (a .:) ` = a `
definition
let L be
Lattice;
let P be non
empty ClosedSubset of
L;
existence
ex b1 being Sublattice of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & b1 = LattStr(# P,o1,o2 #) )
uniqueness
for b1, b2 being Sublattice of L st ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & b1 = LattStr(# P,o1,o2 #) ) & ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & b2 = LattStr(# P,o1,o2 #) ) holds
b1 = b2
;
end;