:: by Grzegorz Bancerek

::

:: Received July 3, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

theorem Th1: :: FILTER_0:1

for L being non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr

for p, q, r being Element of L st p [= q holds

r "\/" p [= r "\/" q

for p, q, r being Element of L st p [= q holds

r "\/" p [= r "\/" q

proof end;

theorem Th4: :: FILTER_0:4

for L being non empty join-commutative join-associative join-absorbing LattStr

for a, b, c, d being Element of L st a [= b & c [= d holds

a "\/" c [= b "\/" d

for a, b, c, d being Element of L st a [= b & c [= d holds

a "\/" c [= b "\/" d

proof end;

theorem Th5: :: FILTER_0:5

for L being non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr

for a, b, c, d being Element of L st a [= b & c [= d holds

a "/\" c [= b "/\" d

for a, b, c, d being Element of L st a [= b & c [= d holds

a "/\" c [= b "/\" d

proof end;

theorem Th6: :: FILTER_0:6

for L being non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr

for a, b, c being Element of L st a [= c & b [= c holds

a "\/" b [= c

for a, b, c being Element of L st a [= c & b [= c holds

a "\/" b [= c

proof end;

theorem Th7: :: FILTER_0:7

for L being non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr

for a, b, c being Element of L st a [= b & a [= c holds

a [= b "/\" c

for a, b, c being Element of L st a [= b & a [= c holds

a [= b "/\" c

proof end;

theorem Th8: :: FILTER_0:8

for L being Lattice

for S being non empty Subset of L holds

( S is Filter of L iff for p, q being Element of L holds

( ( p in S & q in S ) iff p "/\" q in S ) )

for S being non empty Subset of L holds

( S is Filter 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 Th9: :: FILTER_0:9

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

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

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 )

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;

definition

let L be Lattice;

let p be Element of L;

coherence

{ q where q is Element of L : p [= q } is Filter of L

end;
let p be Element of L;

coherence

{ q where q is Element of L : p [= q } is Filter of L

proof end;

:: deftheorem defines <. FILTER_0:def 2 :

for L being Lattice

for p being Element of L holds <.p.) = { q where q is Element of L : p [= q } ;

for L being Lattice

for p being Element of L holds <.p.) = { q where q is Element of L : p [= q } ;

theorem Th16: :: FILTER_0:16

for L being Lattice

for p, q being Element of L holds

( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) )

for p, q being Element of L holds

( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) )

proof end;

definition

let L be Lattice;

let F be Filter of L;

end;
let F be Filter of L;

attr F is being_ultrafilter means :Def3: :: FILTER_0:def 3

( F <> the carrier of L & ( for H being Filter of L st F c= H & H <> the carrier of L holds

F = H ) );

( F <> the carrier of L & ( for H being Filter of L st F c= H & H <> the carrier of L holds

F = H ) );

:: deftheorem Def3 defines being_ultrafilter FILTER_0:def 3 :

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

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

theorem Th18: :: FILTER_0:18

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 being_ultrafilter )

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 being_ultrafilter )

proof end;

theorem Th19: :: FILTER_0:19

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

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 Th20: :: FILTER_0:20

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 being_ultrafilter )

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 being_ultrafilter )

proof end;

definition

let L be Lattice;

let D be non empty Subset of L;

ex b_{1} being Filter of L st

( D c= b_{1} & ( for F being Filter of L st D c= F holds

b_{1} c= F ) )

for b_{1}, b_{2} being Filter of L st D c= b_{1} & ( for F being Filter of L st D c= F holds

b_{1} c= F ) & D c= b_{2} & ( for F being Filter of L st D c= F holds

b_{2} c= F ) holds

b_{1} = b_{2}

end;
let D be non empty Subset of L;

func <.D.) -> Filter of L means :Def4: :: FILTER_0:def 4

( D c= it & ( for F being Filter of L st D c= F holds

it c= F ) );

existence ( D c= it & ( for F being Filter of L st D c= F holds

it c= F ) );

ex b

( D c= b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines <. FILTER_0:def 4 :

for L being Lattice

for D being non empty Subset of L

for b_{3} being Filter of L holds

( b_{3} = <.D.) iff ( D c= b_{3} & ( for F being Filter of L st D c= F holds

b_{3} c= F ) ) );

for L being Lattice

for D being non empty Subset of L

for b

( b

b

theorem Th23: :: FILTER_0:23

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.)

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 Th24: :: FILTER_0:24

for L being Lattice

for p being Element of L

for D being non empty Subset of L st D = {p} holds

<.D.) = <.p.)

for p being Element of L

for D being non empty Subset of L st D = {p} holds

<.D.) = <.p.)

proof end;

theorem Th25: :: FILTER_0:25

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 )

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 Th26: :: FILTER_0:26

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 )

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;

:: deftheorem defines prime FILTER_0:def 5 :

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

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 Th27: :: FILTER_0:27

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

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;

:: deftheorem Def6 defines implicative FILTER_0:def 6 :

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

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

ex b_{1} being Lattice st

( b_{1} is strict & b_{1} is implicative )
end;

cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like implicative for LattStr ;

existence ex b

( b

proof end;

definition

let L be Lattice;

let p, q be Element of L;

assume A1: L is I_Lattice ;

ex b_{1} being Element of L st

( p "/\" b_{1} [= q & ( for r being Element of L st p "/\" r [= q holds

r [= b_{1} ) )
by A1, Def6;

correctness

uniqueness

for b_{1}, b_{2} being Element of L st p "/\" b_{1} [= q & ( for r being Element of L st p "/\" r [= q holds

r [= b_{1} ) & p "/\" b_{2} [= q & ( for r being Element of L st p "/\" r [= q holds

r [= b_{2} ) holds

b_{1} = b_{2};

end;
let p, q be Element of L;

assume A1: L is I_Lattice ;

func p => q -> Element of L means :Def7: :: FILTER_0:def 7

( p "/\" it [= q & ( for r being Element of L st p "/\" r [= q holds

r [= it ) );

existence ( p "/\" it [= q & ( for r being Element of L st p "/\" r [= q holds

r [= it ) );

ex b

( p "/\" b

r [= b

correctness

uniqueness

for b

r [= b

r [= b

b

proof end;

:: deftheorem Def7 defines => FILTER_0:def 7 :

for L being Lattice

for p, q being Element of L st L is I_Lattice holds

for b_{4} being Element of L holds

( b_{4} = p => q iff ( p "/\" b_{4} [= q & ( for r being Element of L st p "/\" r [= q holds

r [= b_{4} ) ) );

for L being Lattice

for p, q being Element of L st L is I_Lattice holds

for b

( b

r [= b

registration
end;

theorem Th29: :: FILTER_0:29

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

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 Th30: :: FILTER_0:30

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

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;

{ (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 ) } is Subset of L

end;
let D1, D2 be non empty Subset of L;

func D1 "/\" D2 -> Subset of L equals :: FILTER_0:def 8

{ (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 ) } ;

{ (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 ) } is Subset of L

proof end;

:: deftheorem defines "/\" FILTER_0:def 8 :

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

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

theorem :: FILTER_0:31

theorem :: FILTER_0:32

registration

let L be D_Lattice;

let F1, F2 be Filter of L;

coherence

( F1 "/\" F2 is final & F1 "/\" F2 is meet-closed )

end;
let F1, F2 be Filter of L;

coherence

( F1 "/\" F2 is final & F1 "/\" F2 is meet-closed )

proof end;

theorem Th34: :: FILTER_0:34

for L being Lattice

for D1, D2 being non empty Subset of L holds

( <.(D1 \/ D2).) = <.(<.D1.) \/ D2).) & <.(D1 \/ D2).) = <.(D1 \/ <.D2.)).) )

for D1, D2 being non empty Subset of L holds

( <.(D1 \/ D2).) = <.(<.D1.) \/ D2).) & <.(D1 \/ D2).) = <.(D1 \/ <.D2.)).) )

proof end;

theorem :: FILTER_0:35

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 ) }

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 Th40: :: FILTER_0:40

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.)

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 Th41: :: FILTER_0:41

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

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 Th44: :: FILTER_0:44

for B being B_Lattice

for FB being Filter of B holds

( FB is being_ultrafilter iff ( FB <> the carrier of B & ( for a being Element of B holds

( a in FB or a ` in FB ) ) ) )

for FB being Filter of B holds

( FB is being_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:45

for B being B_Lattice

for FB being Filter of B holds

( ( FB <> <.B.) & FB is prime ) iff FB is being_ultrafilter )

for FB being Filter of B holds

( ( FB <> <.B.) & FB is prime ) iff FB is being_ultrafilter )

proof end;

theorem Th46: :: FILTER_0:46

for B being B_Lattice

for FB being Filter of B st FB is being_ultrafilter holds

for a being Element of B holds

( a in FB iff not a ` in FB )

for FB being Filter of B st FB is being_ultrafilter holds

for a being Element of B holds

( a in FB iff not a ` in FB )

proof end;

theorem :: FILTER_0:47

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 being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) )

for a, b being Element of B st a <> b holds

ex FB being Filter of B st

( FB is being_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;

for b_{1}, b_{2} 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 & b_{1} = 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 & b_{2} = LattStr(# F,o1,o2 #) ) holds

b_{1} = b_{2}
;

existence

ex b_{1} being Lattice ex o1, o2 being BinOp of F st

( o1 = the L_join of L || F & o2 = the L_meet of L || F & b_{1} = LattStr(# F,o1,o2 #) )

end;
let F be Filter of L;

func latt F -> Lattice means :Def9: :: FILTER_0:def 9

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

for b

( o1 = the L_join of L || F & o2 = the L_meet of L || F & b

( o1 = the L_join of L || F & o2 = the L_meet of L || F & b

b

existence

ex b

( o1 = the L_join of L || F & o2 = the L_meet of L || F & b

proof end;

:: deftheorem Def9 defines latt FILTER_0:def 9 :

for L being Lattice

for F being Filter of L

for b_{3} being Lattice holds

( b_{3} = 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 & b_{3} = LattStr(# F,o1,o2 #) ) );

for L being Lattice

for F being Filter of L

for b

( b

( o1 = the L_join of L || F & o2 = the L_meet of L || F & b

theorem Th49: :: FILTER_0:49

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 )

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 Th50: :: FILTER_0:50

for L being Lattice

for p, q being Element of L

for F being Filter of L

for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds

( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )

for p, q being Element of L

for F being Filter of L

for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds

( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )

proof end;

theorem Th51: :: FILTER_0:51

for L being Lattice

for p, q being Element of L

for F being Filter of L

for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds

( p [= q iff p9 [= q9 )

for p, q being Element of L

for F being Filter of L

for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds

( p [= q iff p9 [= q9 )

proof end;

registration
end;

theorem Th59: :: FILTER_0:59

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

for p being Element of L st L is C_Lattice & L is M_Lattice holds

latt <.p.) is C_Lattice

proof end;

definition

let L be Lattice;

let p, q be Element of L;

correctness

coherence

(p => q) "/\" (q => p) is Element of L;

;

end;
let p, q be Element of L;

correctness

coherence

(p => q) "/\" (q => p) is Element of L;

;

:: deftheorem defines <=> FILTER_0:def 10 :

for L being Lattice

for p, q being Element of L holds p <=> q = (p => q) "/\" (q => p);

for L being Lattice

for p, q being Element of L holds p <=> q = (p => q) "/\" (q => p);

theorem Th62: :: FILTER_0:62

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

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;

ex b_{1} being Relation st

( field b_{1} c= the carrier of L & ( for p, q being Element of L holds

( [p,q] in b_{1} iff p <=> q in F ) ) )

for b_{1}, b_{2} being Relation st field b_{1} c= the carrier of L & ( for p, q being Element of L holds

( [p,q] in b_{1} iff p <=> q in F ) ) & field b_{2} c= the carrier of L & ( for p, q being Element of L holds

( [p,q] in b_{2} iff p <=> q in F ) ) holds

b_{1} = b_{2}

end;
let F be Filter of L;

func equivalence_wrt F -> Relation means :Def11: :: FILTER_0:def 11

( 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 ( field it c= the carrier of L & ( for p, q being Element of L holds

( [p,q] in it iff p <=> q in F ) ) );

ex b

( field b

( [p,q] in b

proof end;

uniqueness for b

( [p,q] in b

( [p,q] in b

b

proof end;

:: deftheorem Def11 defines equivalence_wrt FILTER_0:def 11 :

for L being Lattice

for F being Filter of L

for b_{3} being Relation holds

( b_{3} = equivalence_wrt F iff ( field b_{3} c= the carrier of L & ( for p, q being Element of L holds

( [p,q] in b_{3} iff p <=> q in F ) ) ) );

for L being Lattice

for F being Filter of L

for b

( b

( [p,q] in b

theorem Th64: :: FILTER_0:64

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

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 Th65: :: FILTER_0:65

for L being Lattice

for F being Filter of L holds equivalence_wrt F is_symmetric_in the carrier of L

for F being Filter of L holds equivalence_wrt F is_symmetric_in the carrier of L

proof end;

theorem Th66: :: FILTER_0:66

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

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 Th67: :: FILTER_0:67

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

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:68

for L being Lattice

for F being Filter of L st L is I_Lattice holds

field (equivalence_wrt F) = the carrier of L

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 Th67;

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

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

end;
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 by Th67;

:: deftheorem Def12 defines are_equivalence_wrt FILTER_0:def 12 :

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

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:69

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 )

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:70

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 )

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:71

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

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:72

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

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;

begin

:: missing, 2006.12.05, AT

theorem :: FILTER_0:73

for L being non empty join-commutative meet-commutative meet-associative meet-absorbing join-absorbing LattStr

for x, y, z being Element of L st z [= x & z [= y & ( for z9 being Element of L st z9 [= x & z9 [= y holds

z9 [= z ) holds

z = x "/\" y

for x, y, z being Element of L st z [= x & z [= y & ( for z9 being Element of L st z9 [= x & z9 [= y holds

z9 [= z ) holds

z = x "/\" y

proof end;

theorem :: FILTER_0:74

for L being non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr

for x, y, z being Element of L st x [= z & y [= z & ( for z9 being Element of L st x [= z9 & y [= z9 holds

z [= z9 ) holds

z = x "\/" y

for x, y, z being Element of L st x [= z & y [= z & ( for z9 being Element of L st x [= z9 & y [= z9 holds

z [= z9 ) holds

z = x "\/" y

proof end;