:: FILTER_0 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: FILTER_0:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, q, r being Element of L st p [= q holds
( r "\/" p [= r "\/" q & p "\/" r [= q "\/" r & p "\/" r [= r "\/" q & r "\/" p [= q "\/" r )
proof end;

theorem :: FILTER_0:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, r, q being Element of L st p [= r holds
( p "/\" q [= r & q "/\" p [= r )
proof end;

theorem :: FILTER_0:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, r, q being Element of L st p [= r holds
( p [= q "\/" r & p [= r "\/" q )
proof end;

theorem Th4: :: FILTER_0:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, p1, q, q1 being Element of L st p [= p1 & q [= q1 holds
( p "\/" q [= p1 "\/" q1 & p "\/" q [= q1 "\/" p1 )
proof end;

theorem Th5: :: FILTER_0:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, p1, q, q1 being Element of L st p [= p1 & q [= q1 holds
( p "/\" q [= p1 "/\" q1 & p "/\" q [= q1 "/\" p1 )
proof end;

theorem Th6: :: FILTER_0:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, r, q being Element of L st p [= r & q [= r holds
p "\/" q [= r
proof end;

theorem :: FILTER_0:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for r, p, q being Element of L st r [= p & r [= q holds
r [= p "/\" q
proof end;

definition
let L be Lattice;
mode Filter of L -> non empty Subset of L means :Def1: :: FILTER_0:def 1
for p, q being Element of L holds
( ( p in it & q in it ) iff p "/\" q in it );
existence
ex b1 being non empty Subset of L st
for p, q being Element of L holds
( ( p in b1 & q in b1 ) iff p "/\" q in b1 )
proof end;
end;

:: deftheorem Def1 defines Filter FILTER_0:def 1 :
for L being Lattice
for b2 being non empty Subset of L holds
( b2 is Filter of L iff for p, q being Element of L holds
( ( p in b2 & q in b2 ) iff p "/\" q in b2 ) );

theorem :: FILTER_0:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th9: :: FILTER_0:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for D being non empty Subset of L holds
( D is Filter 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 & p [= q holds
q in D ) ) )
proof end;

theorem Th10: :: FILTER_0:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, q being Element of L
for H being Filter of L st p in H holds
( p "\/" q in H & q "\/" p in H )
proof end;

theorem Th11: :: FILTER_0:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for H being Filter of L ex p being Element of L st p in H
proof end;

theorem Th12: :: FILTER_0:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for H being Filter of L st L is 1_Lattice holds
Top L in H
proof end;

theorem :: FILTER_0:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice st L is 1_Lattice holds
{(Top L)} is Filter of L
proof end;

theorem :: FILTER_0:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p being Element of L st {p} is Filter of L holds
L is upper-bounded
proof end;

theorem Th15: :: FILTER_0:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice holds the carrier of L is Filter of L
proof end;

definition
let L be Lattice;
func <.L.) -> Filter of L equals :: FILTER_0:def 2
the carrier of L;
coherence
the carrier of L is Filter of L
by Th15;
end;

:: deftheorem defines <. FILTER_0:def 2 :
for L being Lattice holds <.L.) = the carrier of L;

definition
let L be Lattice;
let p be Element of L;
func <.p.) -> Filter of L equals :: FILTER_0:def 3
{ q where q is Element of L : p [= q } ;
coherence
{ q where q is Element of L : p [= q } is Filter of L
proof end;
end;

:: deftheorem defines <. FILTER_0:def 3 :
for L being Lattice
for p being Element of L holds <.p.) = { q where q is Element of L : p [= q } ;

theorem :: FILTER_0:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FILTER_0:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th18: :: FILTER_0:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for q, p being Element of L holds
( q in <.p.) iff p [= q )
proof end;

theorem Th19: :: FILTER_0:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th20: :: FILTER_0:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice st L is 0_Lattice holds
<.L.) = <.(Bottom L).)
proof end;

definition
let L be Lattice;
let F be Filter of L;
attr F is being_ultrafilter means :Def4: :: FILTER_0:def 4
( F <> the carrier of L & ( for H being Filter of L st F c= H & H <> the carrier of L holds
F = H ) );
end;

:: deftheorem Def4 defines being_ultrafilter FILTER_0:def 4 :
for L being Lattice
for F being Filter of L holds
( F is being_ultrafilter iff ( F <> the carrier of L & ( for H being Filter of L st F c= H & H <> the carrier of L holds
F = H ) ) );

notation
let L be Lattice;
let F be Filter of L;
synonym F is_ultrafilter for being_ultrafilter F;
end;

theorem :: FILTER_0:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th22: :: FILTER_0:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice st L is lower-bounded holds
for F being Filter of L st F <> the carrier of L holds
ex H being Filter of L st
( F c= H & H is_ultrafilter )
proof end;

theorem Th23: :: FILTER_0:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th24: :: FILTER_0:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p being Element of L st L is 0_Lattice & p <> Bottom L holds
ex H being Filter of L st
( p in H & H is_ultrafilter )
proof end;

definition
let L be Lattice;
let D be non empty Subset of L;
func <.D.) -> Filter of L means :Def5: :: FILTER_0:def 5
( D c= it & ( for F being Filter of L st D c= F holds
it c= F ) );
existence
ex b1 being Filter of L st
( D c= b1 & ( for F being Filter of L st D c= F holds
b1 c= F ) )
proof end;
uniqueness
for b1, b2 being Filter of L st D c= b1 & ( for F being Filter of L st D c= F holds
b1 c= F ) & D c= b2 & ( for F being Filter of L st D c= F holds
b2 c= F ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines <. FILTER_0:def 5 :
for L being Lattice
for D being non empty Subset of L
for b3 being Filter of L holds
( b3 = <.D.) iff ( D c= b3 & ( for F being Filter of L st D c= F holds
b3 c= F ) ) );

theorem :: FILTER_0:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th26: :: FILTER_0:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F being Filter of L holds <.F.) = F
proof end;

theorem Th27: :: FILTER_0:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for D1, D2 being non empty Subset of L st D1 c= D2 holds
<.D1.) c= <.D2.)
proof end;

theorem :: FILTER_0:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th29: :: FILTER_0:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th30: :: FILTER_0:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th31: :: FILTER_0:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for D being non empty Subset of L st L is 0_Lattice & Bottom L in D holds
( <.D.) = <.L.) & <.D.) = the carrier of L )
proof end;

theorem Th32: :: FILTER_0:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F being Filter of L st L is 0_Lattice & Bottom L in F holds
( F = <.L.) & F = the carrier of L )
proof end;

definition
let L be Lattice;
let F be Filter of L;
attr F is prime means :: FILTER_0:def 6
for p, q being Element of L holds
( p "\/" q in F iff ( p in F or q in F ) );
end;

:: deftheorem defines prime FILTER_0:def 6 :
for L being Lattice
for F being Filter of L holds
( F is prime iff for p, q being Element of L holds
( p "\/" q in F iff ( p in F or q in F ) ) );

theorem :: FILTER_0:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th34: :: FILTER_0:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice st L is B_Lattice holds
for p, q being Element of L holds
( p "/\" ((p ` ) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds
r [= (p ` ) "\/" q ) )
proof end;

definition
let IT be non empty LattStr ;
attr IT is implicative means :Def7: :: FILTER_0:def 7
for p, q being Element of IT ex r being Element of IT st
( p "/\" r [= q & ( for r1 being Element of IT st p "/\" r1 [= q holds
r1 [= r ) );
end;

:: deftheorem Def7 defines implicative FILTER_0:def 7 :
for IT being non empty LattStr holds
( IT is implicative iff for p, q being Element of IT ex r being Element of IT st
( p "/\" r [= q & ( for r1 being Element of IT st p "/\" r1 [= q holds
r1 [= r ) ) );

registration
cluster strict implicative LattStr ;
existence
ex b1 being Lattice st
( b1 is strict & b1 is implicative )
proof end;
end;

definition
mode I_Lattice is implicative Lattice;
end;

definition
let L be Lattice;
let p, q be Element of L;
assume A1: L is I_Lattice ;
func p => q -> Element of L means :Def8: :: FILTER_0:def 8
( p "/\" it [= q & ( for r being Element of L st p "/\" r [= q holds
r [= it ) );
existence
ex b1 being Element of L st
( p "/\" b1 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= b1 ) )
by A1, Def7;
correctness
uniqueness
for b1, b2 being Element of L st p "/\" b1 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= b1 ) & p "/\" b2 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= b2 ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def8 defines => FILTER_0:def 8 :
for L being Lattice
for p, q being Element of L st L is I_Lattice holds
for b4 being Element of L holds
( b4 = p => q iff ( p "/\" b4 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= b4 ) ) );

theorem :: FILTER_0:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FILTER_0:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th37: :: FILTER_0:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice holds I is upper-bounded
proof end;

theorem Th38: :: FILTER_0:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for i being Element of I holds i => i = Top I
proof end;

theorem Th39: :: FILTER_0:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice holds I is distributive
proof end;

theorem Th40: :: FILTER_0:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice holds B is implicative
proof end;

registration
cluster implicative -> distributive LattStr ;
coherence
for b1 being Lattice st b1 is implicative holds
b1 is distributive
by Th39;
end;

theorem Th41: :: FILTER_0:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for i, j being Element of I
for FI being Filter of I st i in FI & i => j in FI holds
j in FI
proof end;

theorem Th42: :: FILTER_0:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for j, i being Element of I
for FI being Filter of I st j in FI holds
i => j in FI
proof end;

definition
let L be Lattice;
let D1, D2 be non empty Subset of L;
func D1 "/\" D2 -> Subset of L equals :: FILTER_0:def 9
{ (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_0:def 9 :
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;

theorem :: FILTER_0:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FILTER_0:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_0:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th46: :: FILTER_0:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for D1, D2 being non empty Subset of L holds D1 "/\" D2 = D2 "/\" D1
proof end;

definition
let L be D_Lattice;
let F1, F2 be Filter of L;
:: original: "/\"
redefine func F1 "/\" F2 -> Filter of L;
coherence
F1 "/\" F2 is Filter of L
proof end;
end;

definition
let L be B_Lattice;
let F1, F2 be Filter of L;
:: original: "/\"
redefine func F1 "/\" F2 -> Filter of L;
coherence
F1 "/\" F2 is Filter of L
proof end;
end;

theorem Th47: :: FILTER_0:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_0:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F, H being Filter of L holds <.(F \/ H).) = { r where r is Element of L : ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H )
}
proof end;

theorem Th49: :: FILTER_0:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F, H being Filter of L holds
( F c= F "/\" H & H c= F "/\" H )
proof end;

theorem Th50: :: FILTER_0:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F, H being Filter of L holds <.(F \/ H).) = <.(F "/\" H).)
proof end;

theorem Th51: :: FILTER_0:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for F1, F2 being Filter of I holds <.(F1 \/ F2).) = F1 "/\" F2
proof end;

theorem :: FILTER_0:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for FB, HB being Filter of B holds <.(FB \/ HB).) = FB "/\" HB
proof end;

theorem Th53: :: FILTER_0:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for j, i being Element of I
for DI being non empty Subset of I st j in <.(DI \/ {i}).) holds
i => j in <.DI.)
proof end;

theorem Th54: :: FILTER_0:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for i, j, k being Element of I
for FI being Filter of I st i => j in FI & j => k in FI holds
i => k in FI
proof end;

theorem Th55: :: FILTER_0:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for a, b being Element of B holds a => b = (a ` ) "\/" b
proof end;

theorem Th56: :: FILTER_0:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for a, b being Element of B holds
( a [= b iff a "/\" (b ` ) = Bottom B )
proof end;

theorem Th57: :: FILTER_0:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for FB being Filter of B holds
( FB is_ultrafilter iff ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) ) )
proof end;

theorem :: FILTER_0:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for FB being Filter of B holds
( ( FB <> <.B.) & FB is prime ) iff FB is_ultrafilter )
proof end;

theorem Th59: :: FILTER_0:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for FB being Filter of B st FB is_ultrafilter holds
for a being Element of B holds
( a in FB iff not a ` in FB )
proof end;

theorem :: FILTER_0:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for a, b being Element of B st a <> b holds
ex FB being Filter of B st
( FB is_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) )
proof end;

definition
let L be Lattice;
let F be Filter of L;
func latt F -> Lattice means :Def10: :: FILTER_0:def 10
ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & it = LattStr(# F,o1,o2 #) );
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 #) )
proof end;
end;

:: deftheorem Def10 defines latt FILTER_0:def 10 :
for L being Lattice
for F being Filter of L
for b3 being Lattice holds
( b3 = latt F iff ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & b3 = LattStr(# F,o1,o2 #) ) );

registration
let L be Lattice;
let F be Filter of L;
cluster latt F -> strict ;
coherence
latt F is strict
proof end;
end;

theorem :: FILTER_0:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FILTER_0:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being strict Lattice holds latt <.L.) = L
proof end;

theorem Th63: :: FILTER_0:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F being Filter of L holds
( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F )
proof end;

theorem Th64: :: FILTER_0:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, q being Element of L
for F being Filter of L
for p', q' being Element of (latt F) st p = p' & q = q' holds
( p "\/" q = p' "\/" q' & p "/\" q = p' "/\" q' )
proof end;

theorem Th65: :: FILTER_0:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, q being Element of L
for F being Filter of L
for p', q' being Element of (latt F) st p = p' & q = q' holds
( p [= q iff p' [= q' )
proof end;

theorem Th66: :: FILTER_0:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F being Filter of L st L is upper-bounded holds
latt F is upper-bounded
proof end;

theorem :: FILTER_0:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F being Filter of L st L is modular holds
latt F is modular
proof end;

theorem Th68: :: FILTER_0:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F being Filter of L st L is distributive holds
latt F is distributive
proof end;

theorem :: FILTER_0:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F being Filter of L st L is I_Lattice holds
latt F is implicative
proof end;

theorem Th70: :: FILTER_0:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p being Element of L holds latt <.p.) is lower-bounded
proof end;

theorem Th71: :: FILTER_0:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p being Element of L holds Bottom (latt <.p.)) = p
proof end;

theorem Th72: :: FILTER_0:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p being Element of L st L is upper-bounded holds
Top (latt <.p.)) = Top L
proof end;

theorem Th73: :: FILTER_0:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p being Element of L st L is 1_Lattice holds
latt <.p.) is bounded
proof end;

theorem Th74: :: FILTER_0:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p being Element of L st L is C_Lattice & L is M_Lattice holds
latt <.p.) is C_Lattice
proof end;

theorem :: FILTER_0:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p being Element of L st L is B_Lattice holds
latt <.p.) is B_Lattice
proof end;

definition
let L be Lattice;
let p, q be Element of L;
func p <=> q -> Element of L equals :: FILTER_0:def 11
(p => q) "/\" (q => p);
correctness
coherence
(p => q) "/\" (q => p) is Element of L
;
;
end;

:: deftheorem defines <=> FILTER_0:def 11 :
for L being Lattice
for p, q being Element of L holds p <=> q = (p => q) "/\" (q => p);

theorem :: FILTER_0:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FILTER_0:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, q being Element of L holds p <=> q = q <=> p ;

theorem Th78: :: FILTER_0:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being I_Lattice
for i, j, k being Element of I
for FI being Filter of I st i <=> j in FI & j <=> k in FI holds
i <=> k in FI
proof end;

definition
let L be Lattice;
let F be Filter of L;
func equivalence_wrt F -> Relation means :Def12: :: FILTER_0:def 12
( field it c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in it iff p <=> q in F ) ) );
existence
ex b1 being Relation st
( field b1 c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in b1 iff p <=> q in F ) ) )
proof end;
uniqueness
for b1, b2 being Relation st field b1 c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in b1 iff p <=> q in F ) ) & field b2 c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in b2 iff p <=> q in F ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines equivalence_wrt FILTER_0:def 12 :
for L being Lattice
for F being Filter of L
for b3 being Relation holds
( b3 = equivalence_wrt F iff ( field b3 c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in b3 iff p <=> q in F ) ) ) );

theorem :: FILTER_0:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th80: :: FILTER_0:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F being Filter of L holds equivalence_wrt F is Relation of the carrier of L
proof end;

theorem Th81: :: FILTER_0:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is_reflexive_in the carrier of L
proof end;

theorem Th82: :: FILTER_0:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F being Filter of L holds equivalence_wrt F is_symmetric_in the carrier of L
proof end;

theorem Th83: :: FILTER_0:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is_transitive_in the carrier of L
proof end;

theorem Th84: :: FILTER_0:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is Equivalence_Relation of the carrier of L
proof end;

theorem :: FILTER_0:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for F being Filter of L st L is I_Lattice holds
field (equivalence_wrt F) = the carrier of L
proof end;

definition
let I be I_Lattice;
let FI be Filter of I;
:: original: equivalence_wrt
redefine func equivalence_wrt FI -> Equivalence_Relation of the carrier of I;
coherence
equivalence_wrt FI is Equivalence_Relation of the carrier of I
by Th84;
end;

definition
let B be B_Lattice;
let FB be Filter of B;
:: original: equivalence_wrt
redefine func equivalence_wrt FB -> Equivalence_Relation of the carrier of B;
coherence
equivalence_wrt FB is Equivalence_Relation of the carrier of B
proof end;
end;

definition
let L be Lattice;
let F be Filter of L;
let p, q be Element of L;
pred p,q are_equivalence_wrt F means :Def13: :: FILTER_0:def 13
p <=> q in F;
end;

:: deftheorem Def13 defines are_equivalence_wrt FILTER_0:def 13 :
for L being Lattice
for F being Filter of L
for p, q being Element of L holds
( p,q are_equivalence_wrt F iff p <=> q in F );

theorem :: FILTER_0:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FILTER_0:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, q being Element of L
for F being Filter of L holds
( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F )
proof end;

theorem :: FILTER_0:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being B_Lattice
for FB being Filter of B
for I being I_Lattice
for i being Element of I
for FI being Filter of I
for a being Element of B holds
( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
proof end;

theorem :: FILTER_0:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for p, q being Element of L
for F being Filter of L st p,q are_equivalence_wrt F holds
q,p are_equivalence_wrt F
proof end;

theorem :: FILTER_0:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;