:: by Grzegorz Bancerek

::

:: Received October 24, 1994

:: Copyright (c) 1994-2019 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 ) )

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

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

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

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

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;

( X1 = X2 iff for x being Element of D holds

( x in X1 iff x in X2 ) ) by SUBSET_1:3;

end;
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 redefine pred X1 = X2 means :: FILTER_2:def 1

for x being Element of D holds

( x in X1 iff x in X2 );

( X1 = X2 iff for x being Element of D holds

( x in X1 iff x in X2 ) ) by SUBSET_1:3;

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

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 H

deffunc H

deffunc H

theorem :: FILTER_2:6

theorem :: FILTER_2:7

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

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

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

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;

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 `

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

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

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;

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

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

for x being set st x is Ideal of L1 holds

x is Ideal of L2

proof end;

:: deftheorem defines .: FILTER_2:def 2 :

for L being Lattice

for p being Element of L holds p .: = p;

for L being Lattice

for p being Element of L holds p .: = p;

:: deftheorem defines .: FILTER_2:def 3 :

for L being Lattice

for p being Element of (L .:) holds .: p = p;

for L being Lattice

for p being Element of (L .:) holds .: p = p;

theorem :: FILTER_2:17

theorem :: FILTER_2:18

theorem :: FILTER_2:19

:: deftheorem defines .: FILTER_2:def 4 :

for L being Lattice

for X being Subset of L holds X .: = X;

for L being Lattice

for X being Subset of L holds X .: = X;

:: deftheorem defines .: FILTER_2:def 5 :

for L being Lattice

for X being Subset of (L .:) holds .: X = X;

for L being Lattice

for X being Subset of (L .:) holds .: X = X;

registration
end;

registration

let L be Lattice;

let S be meet-closed Subset of L;

coherence

for b_{1} being Subset of (L .:) st b_{1} = S .: holds

b_{1} is join-closed

end;
let S be meet-closed Subset of L;

coherence

for b

b

proof end;

registration

let L be Lattice;

let S be join-closed Subset of L;

coherence

for b_{1} being Subset of (L .:) st b_{1} = S .: holds

b_{1} is meet-closed

end;
let S be join-closed Subset of L;

coherence

for b

b

proof end;

registration

let L be Lattice;

let S be meet-closed Subset of (L .:);

coherence

for b_{1} being Subset of L st b_{1} = .: S holds

b_{1} is join-closed

end;
let S be meet-closed Subset of (L .:);

coherence

for b

b

proof end;

registration

let L be Lattice;

let S be join-closed Subset of (L .:);

coherence

for b_{1} being Subset of L st b_{1} = .: S holds

b_{1} is meet-closed

end;
let S be join-closed Subset of (L .:);

coherence

for b

b

proof end;

registration

let L be Lattice;

let F be final Subset of L;

coherence

for b_{1} being Subset of (L .:) st b_{1} = F .: holds

b_{1} is initial
by LATTICE2:39, LATTICES:def 23;

end;
let F be final Subset of L;

coherence

for b

b

registration

let L be Lattice;

let F be initial Subset of L;

coherence

for b_{1} being Subset of (L .:) st b_{1} = F .: holds

b_{1} is final
by LATTICE2:39, LATTICES:def 22;

end;
let F be initial Subset of L;

coherence

for b

b

registration

let L be Lattice;

let F be final Subset of (L .:);

coherence

for b_{1} being Subset of L st b_{1} = .: F holds

b_{1} is initial
by LATTICE2:38, LATTICES:def 23;

end;
let F be final Subset of (L .:);

coherence

for b

b

registration

let L be Lattice;

let F be initial Subset of (L .:);

coherence

for b_{1} being Subset of L st b_{1} = F .: holds

b_{1} is final
by LATTICE2:38, LATTICES:def 22;

end;
let F be initial Subset of (L .:);

coherence

for b

b

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

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 )

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;

definition

let L be Lattice;

let p be Element of L;

coherence

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

end;
let p be Element of L;

coherence

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

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

for L being Lattice

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

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

for p, q being Element of L holds

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

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

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

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

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 )

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;

ex b_{1} being Ideal of L st

( D c= b_{1} & ( for I being Ideal of L st D c= I holds

b_{1} c= I ) )

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

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

b_{2} c= I ) holds

b_{1} = b_{2}
;

end;
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 ( D c= it & ( for I being Ideal of L st D c= I holds

it c= I ) );

ex b

( D c= b

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def9 defines (. FILTER_2:def 9 :

for L being Lattice

for D being non empty Subset of L

for b_{3} being Ideal of L holds

( b_{3} = (.D.> iff ( D c= b_{3} & ( for I being Ideal of L st D c= I holds

b_{3} c= I ) ) );

for L being Lattice

for D being non empty Subset of L

for b

( b

b

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

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

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

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

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 )

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 )

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;

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

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

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

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

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

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;

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 )

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

theorem :: FILTER_2:46

registration

let L be D_Lattice;

let I1, I2 be Ideal of L;

coherence

( I1 "\/" I2 is initial & I1 "\/" I2 is join-closed )

end;
let I1, I2 be Ideal of L;

coherence

( I1 "\/" I2 is initial & I1 "\/" I2 is join-closed )

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

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

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;

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

for a being Element of B

for a9 being Element of (B .:) holds

( (a .:) ` = a ` & (.: a9) ` = a9 ` )

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

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 )

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 )

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

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 )

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;

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 ;

{ r where r is Element of L : ( p [= r & r [= q ) } is non empty ClosedSubset of L

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

{ r where r is Element of L : ( p [= r & r [= q ) } is non empty ClosedSubset of L

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

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

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

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

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;

definition

let L be Lattice;

for b_{1} being LattStr holds

( b_{1} 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 b_{1}, the L_join of b_{1}, the L_meet of b_{1} #) = LattStr(# P,o1,o2 #) ) )

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

for b

( b

( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of b

proof end;

:: deftheorem Def13 defines Sublattice FILTER_2:def 13 :

for L being Lattice

for b_{2} being LattStr holds

( b_{2} 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 b_{2}, the L_join of b_{2}, the L_meet of b_{2} #) = LattStr(# P,o1,o2 #) ) );

for L being Lattice

for b

( b

( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of b

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;

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;

ex b_{1} 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 & b_{1} = LattStr(# P,o1,o2 #) )

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

b_{1} = b_{2}
;

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

ex b

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

proof end;

uniqueness for b

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

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

b

:: deftheorem Def14 defines latt FILTER_2:def 14 :

for L being Lattice

for P being non empty ClosedSubset of L

for b_{3} being Sublattice of L holds

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

for L being Lattice

for P being non empty ClosedSubset of L

for b

( b

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

registration
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 .:

end;
let l be Sublattice of L;

:: original: .:

redefine func l .: -> strict Sublattice of L .: ;

coherence

l .: is strict Sublattice of L .:

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

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

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

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 )

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

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

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

for p, q being Element of L st L is implicative & p [= q holds

latt (L,[#p,q#]) is implicative

proof end;

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

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

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

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

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

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