begin
theorem Th1:
theorem
theorem Th3:
theorem
theorem Th5:
begin
:: deftheorem defines = FILTER_2:def 1 :
for
D being non
empty set for
X1,
X2 being
Subset of holds
(
X1 = X2 iff for
x being
Element of
D holds
(
x in X1 iff
x in X2 ) );
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;
theorem
theorem
theorem
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
theorem Th14:
:: deftheorem FILTER_2:def 2 :
canceled;
:: deftheorem FILTER_2:def 3 :
canceled;
Def3:
for L being Lattice
for S being non empty Subset of holds
( S is Ideal of L iff for p, q being Element of holds
( ( p in S & q in S ) iff p "\/" q in S ) )
theorem
canceled;
theorem Th16:
theorem Th17:
:: deftheorem defines .: FILTER_2:def 4 :
:: deftheorem defines .: FILTER_2:def 5 :
theorem
theorem
theorem
:: deftheorem defines .: FILTER_2:def 6 :
:: deftheorem defines .: FILTER_2:def 7 :
theorem Th21:
theorem Th22:
theorem Th23:
theorem
theorem
theorem
theorem
begin
theorem Th28:
:: deftheorem defines (. FILTER_2:def 8 :
:: deftheorem defines (. FILTER_2:def 9 :
theorem Th29:
theorem Th30:
theorem
theorem
:: deftheorem defines is_max-ideal FILTER_2:def 10 :
theorem Th33:
theorem
theorem
theorem
:: deftheorem Def11 defines (. FILTER_2:def 11 :
Lm1:
for L1, L2 being Lattice
for D1 being non empty Subset of
for D2 being non empty Subset of 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.> )
theorem Th37:
theorem Th38:
theorem
theorem
theorem
theorem Th42:
theorem
:: deftheorem defines prime FILTER_2:def 12 :
theorem Th44:
:: deftheorem defines "\/" FILTER_2:def 13 :
Lm2:
for L1, L2 being Lattice
for D1, E1 being non empty Subset of
for D2, E2 being non empty Subset of 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
theorem Th45:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th53:
theorem Th54:
Lm3:
for B being B_Lattice
for a being Element of holds (a .: ) ` = a `
theorem Th55:
theorem
theorem
theorem
theorem
theorem
theorem Th61:
theorem Th62:
:: deftheorem Def14 defines [# FILTER_2:def 14 :
theorem Th63:
theorem
theorem
theorem
theorem
theorem
begin
definition
let L be
Lattice;
redefine mode SubLattice of
L means :
Def15:
ex
P being non
empty ClosedSubset of
L ex
o1,
o2 being
BinOp of
P st
(
o1 = the
L_join of
L || P &
o2 = the
L_meet of
L || P &
LattStr(# the
carrier of
it,the
L_join of
it,the
L_meet of
it #)
= LattStr(#
P,
o1,
o2 #) );
compatibility
for b1 being LattStr holds
( b1 is Sublattice of L iff ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of b1,the L_join of b1,the L_meet of b1 #) = LattStr(# P,o1,o2 #) ) )
end;
:: deftheorem Def15 defines Sublattice FILTER_2:def 15 :
theorem Th69:
definition
let L be
Lattice;
let P be non
empty ClosedSubset of
L;
func latt L,
P -> Sublattice of
L means :
Def16:
ex
o1,
o2 being
BinOp of
P st
(
o1 = the
L_join of
L || P &
o2 = the
L_meet of
L || P &
it = LattStr(#
P,
o1,
o2 #) );
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;
:: deftheorem Def16 defines latt FILTER_2:def 16 :
theorem Th70:
theorem Th71:
theorem
theorem Th73:
theorem Th74:
theorem Th75:
theorem
theorem
theorem Th78:
theorem
theorem Th80:
theorem Th81:
theorem Th82:
theorem Th83:
theorem Th84:
theorem
theorem Th86:
theorem
theorem