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


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 ) )
proof end;

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 ) )
proof end;

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 ) )
proof end;

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
proof end;

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
proof end;

definition
let D be non empty set ;
let X1, X2 be Subset of D;
:: original: =
redefine pred X1 = 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 ) ) ;

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
proof end;

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
proof end;

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 by Th9, Th10;

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 `
proof end;

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
proof end;

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
proof end;

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 ) )
proof end;

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
proof end;

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
proof end;

definition
let L be Lattice;
let p be Element of L;
func p .: -> 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;
func X .: -> 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;
cluster D .: -> 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;
cluster S .: -> join-closed for Subset of (L .:);
coherence
for b1 being Subset of (L .:) st b1 = S .: holds
b1 is join-closed
proof end;
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
proof end;
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
proof end;
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
proof end;
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 by LATTICE2:39, LATTICES:def 23;
end;

registration
let L be Lattice;
let F be initial Subset of L;
cluster F .: -> final for Subset of (L .:);
coherence
for b1 being Subset of (L .:) st b1 = F .: holds
b1 is final by LATTICE2:39, LATTICES:def 22;
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 by LATTICE2:38, LATTICES:def 23;
end;

registration
let L be Lattice;
let F be initial Subset of (L .:);
cluster F .: -> final for Subset of L;
coherence
for b1 being Subset of L st b1 = F .: holds
b1 is final by LATTICE2:38, LATTICES:def 22;
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 .:) )
proof end;

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 ) ) )
proof end;

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 )
proof end;

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

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

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

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
proof end;

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

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
proof end;
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 p, q being Element of L holds
( q in (.p.> iff q [= p )
proof end;

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

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

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

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

:: deftheorem defines 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 & ( for J being Ideal of L st I c= J & 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 )
proof end;

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 & J is max-ideal )
proof end;

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
proof end;

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

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 & ( 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 & ( for I being Ideal of L st D c= I holds
b1 c= I ) )
proof end;
uniqueness
for b1, b2 being Ideal of L st D c= b1 & ( for I being Ideal of L st D c= I holds
b1 c= I ) & D c= b2 & ( for I being Ideal of L st D c= I holds
b2 c= I ) holds
b1 = b2 ;
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 & ( 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 #) & D1 = D2 holds
( <.D1.) = <.D2.) & (.D1.> = (.D2.> )
proof end;

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.> & <.D.) = (.(D .:).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> )
proof end;

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

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.> ) & (.(.D.>.> c= (.D.> )
proof end;

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.>
proof end;

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.>
proof end;

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

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

definition
let L be Lattice;
let I be Ideal of L;
attr I 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 )
proof end;

definition
let L be Lattice;
let D1, D2 be non empty Subset of L;
func D1 "\/" D2 -> Subset of L equals :: FILTER_2:def 11
 { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ;
coherence
{ (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } is Subset of L
proof end;
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 & q in D2 ) } ;

registration
let L be Lattice;
let D1, D2 be non empty Subset of L;
cluster D1 "\/" D2 -> non empty ;
coherence
not D1 "\/" D2 is empty
proof end;
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 #) & D1 = D2 & E1 = E2 holds
D1 "/\" E1 = D2 "/\" E2
proof end;

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 .:) & (D1 .:) "\/" (D2 .:) = D1 "/\" D2 & D19 "\/" D29 = (.: D19) "/\" (.: D29) & (.: D19) "\/" (.: D29) = D19 "/\" D29 )
proof end;

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 & q in D2 holds
( p "\/" q in D1 "\/" D2 & 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 & p in D1 & 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
proof end;

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

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

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 & p in I & q in J ) }
proof end;

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

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

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

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

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

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

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 ` & (.: a9) ` = a9 ` )
proof end;

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

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 & ( for a being Element of B holds
( a in IB or a ` in IB ) ) ) )
proof end;

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

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 )
proof end;

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 & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) )
proof end;

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 & the L_meet of L || P is BinOp of P )
proof end;

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 & o2 = the L_meet of L || P holds
( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 ) by Th1, Th5, LATTICE2:26, LATTICE2:27;

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 & r [= q ) } ;
coherence
{ r where r is Element of L : ( p [= r & r [= q ) } is non empty ClosedSubset of L
proof end;
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 & 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 & r [= q ) )
proof end;

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

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

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

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

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 #) & F1 = F2 holds
latt F1 = latt F2
proof end;

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 & 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 #) ) )
proof end;
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 & o2 = the L_meet of L || P & 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 by NAT_LAT:def 12, TARSKI:def 3;

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 & 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 #) )
proof end;
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 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 & o2 = the L_meet of L || P & 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
proof end;
end;

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

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

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

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 #) & latt (L,<.L.)) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) )
proof end;

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 & the L_join of (latt (L,P)) = the L_join of L || P & the L_meet of (latt (L,P)) = the L_meet of L || P )
proof end;

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 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
proof end;

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 & q = q9 holds
( p [= q iff p9 [= q9 ) by Th73;

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
proof end;

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
proof end;

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
proof end;

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

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

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

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 & Bottom (latt (L,(.p.>)) = Bottom L )
proof end;

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 by Th80;

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 & Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p )
proof end;

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

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

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

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