:: Ideals
:: by Grzegorz Bancerek
::
:: Received October 24, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

theorem Th1: :: FILTER_2:1
for D being non empty set
for S being non empty Subset of D
for f being BinOp of D
for g being BinOp of S st g = f || S holds
( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) )
proofend;

theorem :: FILTER_2:2
for D being non empty set
for S being non empty Subset of D
for f being BinOp of D
for g being BinOp of S
for d being Element of D
for d9 being Element of S st g = f || S & d9 = d holds
( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
proofend;

theorem Th3: :: FILTER_2:3
for D being non empty set
for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S holds
( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) )
proofend;

theorem :: FILTER_2:4
for D being non empty set
for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 holds
g1 is_distributive_wrt g2
proofend;

theorem Th5: :: FILTER_2:5
for D being non empty set
for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 holds
g1 absorbs g2
proofend;

begin

definition
let D be non empty set ;
let X1, X2 be Subset of D;
:: original:=
redefine predX1 = X2 means :: FILTER_2:def 1
 for x being Element of D holds
( x in X1 iff x in X2 );
compatibility
 ( X1 = X2 iff for x being Element of D holds
( x in X1 iff x in X2 ) ) by SUBSET_1:3;
end;

:: deftheorem  defines = FILTER_2:def_1_:_
 for D being non empty set
for X1, X2 being Subset of D 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 :: FILTER_2:6
for L1, L2 being LattStr 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 #) holds
L1 .: = L2 .: ;

theorem :: FILTER_2:7
for L being Lattice holds (L .:) .: = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) ;

theorem :: FILTER_2:8
for L1, L2 being non empty LattStr 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 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
proofend;

theorem Th9: :: FILTER_2:9
for L1, L2 being 0_Lattice 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 #) holds
Bottom L1 = Bottom L2
proofend;

theorem Th10: :: FILTER_2:10
for L1, L2 being 1_Lattice 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 #) holds
Top L1 = Top L2
proofend;

theorem Th11: :: FILTER_2:11
for L1, L2 being C_Lattice 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 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds
a2 is_a_complement_of b2
proofend;

theorem :: FILTER_2:12
for L1, L2 being B_Lattice 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 #) holds
for a being Element of L1
for b being Element of L2 st a = b holds
a ` = b `
proofend;

theorem :: FILTER_2:13
for L being Lattice
for X being Subset of L st ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "/\" q in X ) ) holds
X is ClosedSubset of L
proofend;

theorem :: FILTER_2:14
for L being Lattice
for X being Subset of L st ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "\/" q in X ) ) holds
X is ClosedSubset of L
proofend;

definition
let L be Lattice;
mode Ideal of L is non empty initial join-closed Subset of L;
end;

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 ) )
proofend;

theorem Th15: :: FILTER_2:15
for L1, L2 being Lattice 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 #) holds
for x being set st x is Filter of L1 holds
x is Filter of L2
proofend;

theorem Th16: :: FILTER_2:16
for L1, L2 being Lattice 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 #) holds
for x being set st x is Ideal of L1 holds
x is Ideal of L2
proofend;

definition
let L be Lattice;
let p be Element of L;
funcp .:  ->  Element of (L .:) equals :: FILTER_2:def 2
p;
coherence
 p is Element of (L .:) ;
end;

:: deftheorem  defines .: FILTER_2:def_2_:_
 for L being Lattice
for p being Element of L holds p .: = p;

definition
let L be Lattice;
let p be Element of (L .:);
func .: p ->  Element of L equals :: FILTER_2:def 3
p;
coherence
 p is Element of L ;
end;

:: deftheorem  defines .: FILTER_2:def_3_:_
 for L being Lattice
for p being Element of (L .:) holds .: p = p;

theorem :: FILTER_2:17
for L being Lattice
for p being Element of L
for p9 being Element of (L .:) holds
( .: (p .:) = p & (.: p9) .: = p9 ) ;

theorem :: FILTER_2:18
for L being Lattice
for p, q being Element of L
for p9, q9 being Element of (L .:) holds
( p "/\" q = (p .:) "\/" (q .:) & p "\/" q = (p .:) "/\" (q .:) & p9 "/\" q9 = (.: p9) "\/" (.: q9) & p9 "\/" q9 = (.: p9) "/\" (.: q9) ) ;

theorem :: FILTER_2:19
for L being Lattice
for p, q being Element of L
for p9, q9 being Element of (L .:) holds
( ( p [= q implies q .: [= p .: ) & ( q .: [= p .: implies p [= q ) & ( p9 [= q9 implies .: q9 [= .: p9 ) & ( .: q9 [= .: p9 implies p9 [= q9 ) ) by LATTICE2:38, LATTICE2:39;

definition
let L be Lattice;
let X be Subset of L;
funcX .:  ->  Subset of (L .:) equals :: FILTER_2:def 4
X;
coherence
 X is Subset of (L .:) ;
end;

:: deftheorem  defines .: FILTER_2:def_4_:_
 for L being Lattice
for X being Subset of L holds X .: = X;

definition
let L be Lattice;
let X be Subset of (L .:);
func .: X ->  Subset of L equals :: FILTER_2:def 5
X;
coherence
 X is Subset of L ;
end;

:: deftheorem  defines .: FILTER_2:def_5_:_
 for L being Lattice
for X being Subset of (L .:) holds .: X = X;

registration
let L be Lattice;
let D be non empty Subset of L;
clusterD .:  ->  non empty ;
coherence
 not D .: is empty ;
end;

registration
let L be Lattice;
let D be non empty Subset of (L .:);
cluster .: D ->  non empty ;
coherence
 not .: D is empty ;
end;

registration
let L be Lattice;
let S be meet-closed Subset of L;
clusterS .:  ->  join-closed for Subset of (L .:);
coherence
 for b1 being Subset of (L .:) st b1 = S .: holds
b1 is join-closed
proofend;
end;

registration
let L be Lattice;
let S be join-closed Subset of L;
clusterS .:  ->  meet-closed for Subset of (L .:);
coherence
 for b1 being Subset of (L .:) st b1 = S .: holds
b1 is meet-closed
proofend;
end;

registration
let L be Lattice;
let S be meet-closed Subset of (L .:);
cluster .: S ->  join-closed for Subset of L;
coherence
 for b1 being Subset of L st b1 = .: S holds
b1 is join-closed
proofend;
end;

registration
let L be Lattice;
let S be join-closed Subset of (L .:);
cluster .: S ->  meet-closed for Subset of L;
coherence
 for b1 being Subset of L st b1 = .: S holds
b1 is meet-closed
proofend;
end;

registration
let L be Lattice;
let F be final Subset of L;
clusterF .:  ->  initial for Subset of (L .:);
coherence
 for b1 being Subset of (L .:) st b1 = F .: holds
b1 is initial
proofend;
end;

registration
let L be Lattice;
let F be initial Subset of L;
clusterF .:  ->  final for Subset of (L .:);
coherence
 for b1 being Subset of (L .:) st b1 = F .: holds
b1 is final
proofend;
end;

registration
let L be Lattice;
let F be final Subset of (L .:);
cluster .: F ->  initial for Subset of L;
coherence
 for b1 being Subset of L st b1 = .: F holds
b1 is initial
proofend;
end;

registration
let L be Lattice;
let F be initial Subset of (L .:);
clusterF .:  ->  final for Subset of L;
coherence
 for b1 being Subset of L st b1 = F .: holds
b1 is final
proofend;
end;

theorem Th20: :: FILTER_2:20
for L being Lattice
for x being set holds
( x is Ideal of L iff x is Filter of (L .:) )
proofend;

theorem Th21: :: FILTER_2:21
for L being Lattice
for D being non empty Subset of L holds
( D is Ideal of L iff ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) ) )
proofend;

theorem Th22: :: FILTER_2:22
for L being Lattice
for p, q being Element of L
for I being Ideal of L st p in I holds
( p "/\" q in I & q "/\" p in I )
proofend;

theorem :: FILTER_2:23
for L being Lattice
for I being Ideal of L ex p being Element of L st p in I
proofend;

theorem :: FILTER_2:24
for L being Lattice
for I being Ideal of L st L is lower-bounded holds
Bottom L in I
proofend;

theorem :: FILTER_2:25
for L being Lattice st L is lower-bounded holds
{(Bottom L)} is Ideal of L
proofend;

theorem :: FILTER_2:26
for L being Lattice
for p being Element of L st {p} is Ideal of L holds
L is lower-bounded
proofend;

begin

theorem Th27: :: FILTER_2:27
for L being Lattice holds the carrier of L is Ideal of L
proofend;

definition
let L be Lattice;
func(.L.> ->  Ideal of L equals :: FILTER_2:def 6
 the carrier of L;
coherence
 the carrier of L is Ideal of L by Th27;
end;

:: deftheorem  defines (. FILTER_2:def_6_:_
 for L being Lattice holds (.L.> = the carrier of L;

definition
let L be Lattice;
let p be Element of L;
func(.p.> ->  Ideal of L equals :: FILTER_2:def 7
 {  q where q is Element of L : q [= p  }  ;
coherence
  {  q where q is Element of L : q [= p  }  is Ideal of L
proofend;
end;

:: deftheorem  defines (. FILTER_2:def_7_:_
 for L being Lattice
for p being Element of L holds (.p.> =  {  q where q is Element of L : q [= p  }  ;

theorem Th28: :: FILTER_2:28
for L being Lattice
for q, p being Element of L holds
( q in (.p.> iff q [= p )
proofend;

theorem Th29: :: FILTER_2:29
for L being Lattice
for p being Element of L holds
( (.p.> = <.(p .:).) &amp; (.(p .:).> = <.p.) )
proofend;

theorem :: FILTER_2:30
for L being Lattice
for p, q being Element of L holds
( p in (.p.> &amp; p "/\" q in (.p.> &amp; q "/\" p in (.p.> )
proofend;

theorem :: FILTER_2:31
for L being Lattice st L is upper-bounded holds
(.L.> = (.(Top L).>
proofend;

definition
let L be Lattice;
let I be Ideal of L;
predI is_max-ideal  means :: FILTER_2:def 8
( I <> the carrier of L &amp; ( for J being Ideal of L st I c= J &amp; J <> the carrier of L holds
I = J ) );
end;

:: deftheorem  defines is_max-ideal FILTER_2:def_8_:_
 for L being Lattice
for I being Ideal of L holds
( I is_max-ideal iff ( I <> the carrier of L &amp; ( for J being Ideal of L st I c= J &amp; J <> the carrier of L holds
I = J ) ) );

theorem Th32: :: FILTER_2:32
for L being Lattice
for I being Ideal of L holds
( I is_max-ideal iff I .: is being_ultrafilter )
proofend;

theorem :: FILTER_2:33
for L being Lattice st L is upper-bounded holds
for I being Ideal of L st I <> the carrier of L holds
ex J being Ideal of L st
( I c= J &amp; J is_max-ideal )
proofend;

theorem :: FILTER_2:34
for L being Lattice
for p being Element of L st ex r being Element of L st p "\/" r <> p holds
(.p.> <> the carrier of L
proofend;

theorem :: FILTER_2:35
for L being Lattice
for p being Element of L st L is upper-bounded &amp; p <> Top L holds
ex I being Ideal of L st
( p in I &amp; I is_max-ideal )
proofend;

definition
let L be Lattice;
let D be non empty Subset of L;
func(.D.> ->  Ideal of L means :Def9: :: FILTER_2:def 9
( D c= it &amp; ( for I being Ideal of L st D c= I holds
it c= I ) );
existence
 ex b1 being Ideal of L st
( D c= b1 &amp; ( for I being Ideal of L st D c= I holds
b1 c= I ) )
proofend;
uniqueness
 for b1, b2 being Ideal of L st D c= b1 &amp; ( for I being Ideal of L st D c= I holds
b1 c= I ) &amp; D c= b2 &amp; ( for I being Ideal of L st D c= I holds
b2 c= I ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines (. FILTER_2:def_9_:_
 for L being Lattice
for D being non empty Subset of L
for b3 being Ideal of L holds
( b3 = (.D.> iff ( D c= b3 &amp; ( for I being Ideal of L st D c= I holds
b3 c= I ) ) );

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 #) &amp; D1 = D2 holds
( <.D1.) = <.D2.) &amp; (.D1.> = (.D2.> )
proofend;

theorem Th36: :: FILTER_2:36
for L being Lattice
for D being non empty Subset of L
for D9 being non empty Subset of (L .:) holds
( <.(D .:).) = (.D.> &amp; <.D.) = (.(D .:).> &amp; <.(.: D9).) = (.D9.> &amp; <.D9.) = (.(.: D9).> )
proofend;

theorem Th37: :: FILTER_2:37
for L being Lattice
for I being Ideal of L holds (.I.> = I
proofend;

theorem :: FILTER_2:38
for L being Lattice
for D, D1, D2 being non empty Subset of L holds
( ( D1 c= D2 implies (.D1.> c= (.D2.> ) &amp; (.(.D.>.> c= (.D.> )
proofend;

theorem :: FILTER_2:39
for L being Lattice
for p being Element of L
for D being non empty Subset of L st p in D holds
(.p.> c= (.D.>
proofend;

theorem :: FILTER_2:40
for L being Lattice
for p being Element of L
for D being non empty Subset of L st D = {p} holds
(.D.> = (.p.>
proofend;

theorem Th41: :: FILTER_2:41
for L being Lattice
for D being non empty Subset of L st L is upper-bounded &amp; Top L in D holds
( (.D.> = (.L.> &amp; (.D.> = the carrier of L )
proofend;

theorem :: FILTER_2:42
for L being Lattice
for I being Ideal of L st L is upper-bounded &amp; Top L in I holds
( I = (.L.> &amp; I = the carrier of L )
proofend;

definition
let L be Lattice;
let I be Ideal of L;
attrI is prime  means :: FILTER_2:def 10
 for p, q being Element of L holds
( p "/\" q in I iff ( p in I or q in I ) );
end;

:: deftheorem  defines prime FILTER_2:def_10_:_
 for L being Lattice
for I being Ideal of L holds
( I is prime iff for p, q being Element of L holds
( p "/\" q in I iff ( p in I or q in I ) ) );

theorem Th43: :: FILTER_2:43
for L being Lattice
for I being Ideal of L holds
( I is prime iff I .: is prime )
proofend;

definition
let L be Lattice;
let D1, D2 be non empty Subset of L;
funcD1 "\/" D2 ->  Subset of L equals :: FILTER_2:def 11
 {  (p "\/" q) where p, q is Element of L : ( p in D1 &amp; q in D2 )  }  ;
coherence
  {  (p "\/" q) where p, q is Element of L : ( p in D1 &amp; q in D2 )  }  is Subset of L
proofend;
end;

:: deftheorem  defines "\/" FILTER_2:def_11_:_
 for L being Lattice
for D1, D2 being non empty Subset of L holds D1 "\/" D2 =  {  (p "\/" q) where p, q is Element of L : ( p in D1 &amp; q in D2 )  }  ;

registration
let L be Lattice;
let D1, D2 be non empty Subset of L;
clusterD1 "\/" D2 ->  non empty ;
coherence
 not D1 "\/" D2 is empty
proofend;
end;

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 #) &amp; D1 = D2 &amp; E1 = E2 holds
D1 "/\" E1 = D2 "/\" E2
proofend;

theorem Th44: :: FILTER_2:44
for L being Lattice
for D1, D2 being non empty Subset of L
for D19, D29 being non empty Subset of (L .:) holds
( D1 "\/" D2 = (D1 .:) "/\" (D2 .:) &amp; (D1 .:) "\/" (D2 .:) = D1 "/\" D2 &amp; D19 "\/" D29 = (.: D19) "/\" (.: D29) &amp; (.: D19) "\/" (.: D29) = D19 "/\" D29 )
proofend;

theorem :: FILTER_2:45
for L being Lattice
for p, q being Element of L
for D1, D2 being non empty Subset of L st p in D1 &amp; q in D2 holds
( p "\/" q in D1 "\/" D2 &amp; q "\/" p in D1 "\/" D2 ) ;

theorem :: FILTER_2:46
for L being Lattice
for x being set
for D1, D2 being non empty Subset of L st x in D1 "\/" D2 holds
ex p, q being Element of L st
( x = p "\/" q &amp; p in D1 &amp; q in D2 ) ;

theorem :: FILTER_2:47
for L being Lattice
for D1, D2 being non empty Subset of L holds D1 "\/" D2 = D2 "\/" D1
proofend;

registration
let L be D_Lattice;
let I1, I2 be Ideal of L;
clusterI1 "\/" I2 ->  initial join-closed ;
coherence
 ( I1 "\/" I2 is initial &amp; I1 "\/" I2 is join-closed )
proofend;
end;

theorem :: FILTER_2:48
for L being Lattice
for D1, D2 being non empty Subset of L holds
( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> &amp; (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> )
proofend;

theorem :: FILTER_2:49
for L being Lattice
for I, J being Ideal of L holds (.(I \/ J).> =  {  r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q &amp; p in I &amp; q in J )  }
proofend;

theorem :: FILTER_2:50
for L being Lattice
for I, J being Ideal of L holds
( I c= I "\/" J &amp; J c= I "\/" J )
proofend;

theorem :: FILTER_2:51
for L being Lattice
for I, J being Ideal of L holds (.(I \/ J).> = (.(I "\/" J).>
proofend;

theorem Th52: :: FILTER_2:52
for L being Lattice holds
( L is C_Lattice iff L .: is C_Lattice )
proofend;

theorem Th53: :: FILTER_2:53
for L being Lattice holds
( L is B_Lattice iff L .: is B_Lattice )
proofend;

registration
let B be B_Lattice;
clusterB .:  ->  Lattice-like Boolean ;
coherence
 ( B .: is Boolean &amp; B .: is Lattice-like ) by Th53;
end;

Lm4:  for B being B_Lattice
for a being Element of B holds (a .:) ` = a `
proofend;

theorem Th54: :: FILTER_2:54
for B being B_Lattice
for a being Element of B
for a9 being Element of (B .:) holds
( (a .:) ` = a ` &amp; (.: a9) ` = a9 ` )
proofend;

theorem :: FILTER_2:55
for B being B_Lattice
for IB, JB being Ideal of B holds (.(IB \/ JB).> = IB "\/" JB
proofend;

theorem :: FILTER_2:56
for B being B_Lattice
for IB being Ideal of B holds
( IB is_max-ideal iff ( IB <> the carrier of B &amp; ( for a being Element of B holds
( a in IB or a ` in IB ) ) ) )
proofend;

theorem :: FILTER_2:57
for B being B_Lattice
for IB being Ideal of B holds
( ( IB <> (.B.> &amp; IB is prime ) iff IB is_max-ideal )
proofend;

theorem :: FILTER_2:58
for B being B_Lattice
for IB being Ideal of B st IB is_max-ideal holds
for a being Element of B holds
( a in IB iff not a ` in IB )
proofend;

theorem :: FILTER_2:59
for B being B_Lattice
for a, b being Element of B st a <> b holds
ex IB being Ideal of B st
( IB is_max-ideal &amp; ( ( a in IB &amp; not b in IB ) or ( not a in IB &amp; b in IB ) ) )
proofend;

theorem Th60: :: FILTER_2:60
for L being Lattice
for P being non empty ClosedSubset of L holds
( the L_join of L || P is BinOp of P &amp; the L_meet of L || P is BinOp of P )
proofend;

theorem Th61: :: FILTER_2:61
for L being Lattice
for P being non empty ClosedSubset of L
for o1, o2 being BinOp of P st o1 = the L_join of L || P &amp; o2 = the L_meet of L || P holds
( o1 is commutative &amp; o1 is associative &amp; o2 is commutative &amp; o2 is associative &amp; o1 absorbs o2 &amp; o2 absorbs o1 )
proofend;

definition
let L be Lattice;
let p, q be Element of L;
assume A1: p [= q ;
func[#p,q#] ->  non empty ClosedSubset of L equals :Def12: :: FILTER_2:def 12
 {  r where r is Element of L : ( p [= r &amp; r [= q )  }  ;
coherence
  {  r where r is Element of L : ( p [= r &amp; r [= q )  }  is non empty ClosedSubset of L
proofend;
end;

:: deftheorem Def12 defines [# FILTER_2:def_12_:_
 for L being Lattice
for p, q being Element of L st p [= q holds
[#p,q#] =  {  r where r is Element of L : ( p [= r &amp; r [= q )  }  ;

theorem Th62: :: FILTER_2:62
for L being Lattice
for p, q, r being Element of L st p [= q holds
( r in [#p,q#] iff ( p [= r &amp; r [= q ) )
proofend;

theorem :: FILTER_2:63
for L being Lattice
for p, q being Element of L st p [= q holds
( p in [#p,q#] &amp; q in [#p,q#] ) by Th62;

theorem :: FILTER_2:64
for L being Lattice
for p being Element of L holds [#p,p#] = {p}
proofend;

theorem :: FILTER_2:65
for L being Lattice
for p being Element of L st L is upper-bounded holds
<.p.) = [#p,(Top L)#]
proofend;

theorem :: FILTER_2:66
for L being Lattice
for p being Element of L st L is lower-bounded holds
(.p.> = [#(Bottom L),p#]
proofend;

theorem :: FILTER_2:67
for L1, L2 being Lattice
for F1 being Filter of L1
for F2 being Filter 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 #) &amp; F1 = F2 holds
latt F1 = latt F2
proofend;

begin

notation
let L be Lattice;
synonym  Sublattice of L for  SubLattice of L;
end;

definition
let L be Lattice;
redefine mode SubLattice of L means :Def13: :: FILTER_2:def 13
 ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P &amp; o2 = the L_meet of L || P &amp; 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 &amp; o2 = the L_meet of L || P &amp; LattStr(# the carrier of b1, the L_join of b1, the L_meet of b1 #) = LattStr(# P,o1,o2 #) ) )
proofend;
end;

:: deftheorem Def13 defines Sublattice FILTER_2:def_13_:_
 for L being Lattice
for b2 being LattStr holds
( b2 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 &amp; o2 = the L_meet of L || P &amp; LattStr(# the carrier of b2, the L_join of b2, the L_meet of b2 #) = LattStr(# P,o1,o2 #) ) );

theorem Th68: :: FILTER_2:68
for L being Lattice
for K being Sublattice of L
for a being Element of K holds a is Element of L
proofend;

definition
let L be Lattice;
let P be non empty ClosedSubset of L;
func latt (L,P) ->  Sublattice of L means :Def14: :: FILTER_2:def 14
 ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P &amp; o2 = the L_meet of L || P &amp; 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 &amp; o2 = the L_meet of L || P &amp; b1 = LattStr(# P,o1,o2 #) )
proofend;
uniqueness
 for b1, b2 being Sublattice of L st ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P &amp; o2 = the L_meet of L || P &amp; b1 = LattStr(# P,o1,o2 #) ) &amp; ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P &amp; o2 = the L_meet of L || P &amp; b2 = LattStr(# P,o1,o2 #) ) holds
b1 = b2 ;
end;

:: deftheorem Def14 defines latt FILTER_2:def_14_:_
 for L being Lattice
for P being non empty ClosedSubset of L
for b3 being Sublattice of L holds
( b3 = latt (L,P) iff ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P &amp; o2 = the L_meet of L || P &amp; b3 = LattStr(# P,o1,o2 #) ) );

registration
let L be Lattice;
let P be non empty ClosedSubset of L;
cluster latt (L,P) ->  strict ;
coherence
 latt (L,P) is strict
proofend;
end;

definition
let L be Lattice;
let l be Sublattice of L;
:: original:.:
redefine funcl .:  ->  strict Sublattice of L .: ;
coherence
 l .: is strict Sublattice of L .:
proofend;
end;

theorem Th69: :: FILTER_2:69
for L being Lattice
for F being Filter of L holds latt F = latt (L,F)
proofend;

theorem Th70: :: FILTER_2:70
for L being Lattice
for P being non empty ClosedSubset of L holds latt (L,P) = (latt ((L .:),(P .:))) .:
proofend;

theorem :: FILTER_2:71
for L being Lattice holds
( latt (L,(.L.>) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) &amp; latt (L,<.L.)) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) )
proofend;

theorem Th72: :: FILTER_2:72
for L being Lattice
for P being non empty ClosedSubset of L holds
( the carrier of (latt (L,P)) = P &amp; the L_join of (latt (L,P)) = the L_join of L || P &amp; the L_meet of (latt (L,P)) = the L_meet of L || P )
proofend;

theorem Th73: :: FILTER_2:73
for L being Lattice
for P being non empty ClosedSubset of L
for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 &amp; q = q9 holds
( p "\/" q = p9 "\/" q9 &amp; p "/\" q = p9 "/\" q9 )
proofend;

theorem Th74: :: FILTER_2:74
for L being Lattice
for P being non empty ClosedSubset of L
for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 &amp; q = q9 holds
( p [= q iff p9 [= q9 )
proofend;

theorem :: FILTER_2:75
for L being Lattice
for I being Ideal of L st L is lower-bounded holds
latt (L,I) is lower-bounded
proofend;

theorem :: FILTER_2:76
for L being Lattice
for P being non empty ClosedSubset of L st L is modular holds
latt (L,P) is modular
proofend;

theorem Th77: :: FILTER_2:77
for L being Lattice
for P being non empty ClosedSubset of L st L is distributive holds
latt (L,P) is distributive
proofend;

theorem :: FILTER_2:78
for L being Lattice
for p, q being Element of L st L is implicative &amp; p [= q holds
latt (L,[#p,q#]) is implicative
proofend;

registration
let L be Lattice;
let p be Element of L;
cluster latt (L,(.p.>) ->  upper-bounded ;
coherence
 latt (L,(.p.>) is upper-bounded
proofend;
end;

theorem Th79: :: FILTER_2:79
for L being Lattice
for p being Element of L holds Top (latt (L,(.p.>)) = p
proofend;

theorem Th80: :: FILTER_2:80
for L being Lattice
for p being Element of L st L is lower-bounded holds
( latt (L,(.p.>) is lower-bounded &amp; Bottom (latt (L,(.p.>)) = Bottom L )
proofend;

theorem Th81: :: FILTER_2:81
for L being Lattice
for p being Element of L st L is lower-bounded holds
latt (L,(.p.>) is bounded
proofend;

theorem Th82: :: FILTER_2:82
for L being Lattice
for p, q being Element of L st p [= q holds
( latt (L,[#p,q#]) is bounded &amp; Top (latt (L,[#p,q#])) = q &amp; Bottom (latt (L,[#p,q#])) = p )
proofend;

theorem :: FILTER_2:83
for L being Lattice
for p being Element of L st L is C_Lattice &amp; L is modular holds
latt (L,(.p.>) is C_Lattice
proofend;

theorem Th84: :: FILTER_2:84
for L being Lattice
for p, q being Element of L st L is C_Lattice &amp; L is modular &amp; p [= q holds
latt (L,[#p,q#]) is C_Lattice
proofend;

theorem :: FILTER_2:85
for L being Lattice
for p, q being Element of L st L is B_Lattice &amp; p [= q holds
latt (L,[#p,q#]) is B_Lattice
proofend;

theorem :: FILTER_2:86
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 &amp; q in S ) iff p "\/" q in S ) ) by Lm1;