:: by Grzegorz Bancerek

::

:: Received April 19, 1991

:: Copyright (c) 1991-2021 Association of Mizar Users

deffunc H

deffunc H

definition

let L be Lattice;

let F1, F2 be Filter of L;

:: original: /\

redefine func F1 /\ F2 -> Filter of L;

coherence

F1 /\ F2 is Filter of L by Th1;

end;
let F1, F2 be Filter of L;

:: original: /\

redefine func F1 /\ F2 -> Filter of L;

coherence

F1 /\ F2 is Filter of L by Th1;

definition

let D be non empty set ;

let R be Relation;

ex b_{1} being UnOp of D st

for x, y being Element of D st [x,y] in R holds

[(b_{1} . x),(b_{1} . y)] in R

ex b_{1} being BinOp of D st

for x1, y1, x2, y2 being Element of D st [x1,y1] in R & [x2,y2] in R holds

[(b_{1} . (x1,x2)),(b_{1} . (y1,y2))] in R

end;
let R be Relation;

mode UnOp of D,R -> UnOp of D means :Def1: :: FILTER_1:def 1

for x, y being Element of D st [x,y] in R holds

[(it . x),(it . y)] in R;

existence for x, y being Element of D st [x,y] in R holds

[(it . x),(it . y)] in R;

ex b

for x, y being Element of D st [x,y] in R holds

[(b

proof end;

mode BinOp of D,R -> BinOp of D means :Def2: :: FILTER_1:def 2

for x1, y1, x2, y2 being Element of D st [x1,y1] in R & [x2,y2] in R holds

[(it . (x1,x2)),(it . (y1,y2))] in R;

existence for x1, y1, x2, y2 being Element of D st [x1,y1] in R & [x2,y2] in R holds

[(it . (x1,x2)),(it . (y1,y2))] in R;

ex b

for x1, y1, x2, y2 being Element of D st [x1,y1] in R & [x2,y2] in R holds

[(b

proof end;

:: deftheorem Def1 defines UnOp FILTER_1:def 1 :

for D being non empty set

for R being Relation

for b_{3} being UnOp of D holds

( b_{3} is UnOp of D,R iff for x, y being Element of D st [x,y] in R holds

[(b_{3} . x),(b_{3} . y)] in R );

for D being non empty set

for R being Relation

for b

( b

[(b

:: deftheorem Def2 defines BinOp FILTER_1:def 2 :

for D being non empty set

for R being Relation

for b_{3} being BinOp of D holds

( b_{3} is BinOp of D,R iff for x1, y1, x2, y2 being Element of D st [x1,y1] in R & [x2,y2] in R holds

[(b_{3} . (x1,x2)),(b_{3} . (y1,y2))] in R );

for D being non empty set

for R being Relation

for b

( b

[(b

definition

let D be non empty set ;

let R be Equivalence_Relation of D;

mode UnOp of R is UnOp of D,R;

mode BinOp of R is BinOp of D,R;

end;
let R be Equivalence_Relation of D;

mode UnOp of R is UnOp of D,R;

mode BinOp of R is BinOp of D,R;

definition

let D be non empty set ;

let R be Equivalence_Relation of D;

let u be UnOp of D;

assume A1: u is UnOp of D,R ;

ex b_{1} being UnOp of (Class R) st

for x, y being set st x in Class R & y in x holds

b_{1} . x = Class (R,(u . y))

for b_{1}, b_{2} being UnOp of (Class R) st ( for x, y being set st x in Class R & y in x holds

b_{1} . x = Class (R,(u . y)) ) & ( for x, y being set st x in Class R & y in x holds

b_{2} . x = Class (R,(u . y)) ) holds

b_{1} = b_{2}

end;
let R be Equivalence_Relation of D;

let u be UnOp of D;

assume A1: u is UnOp of D,R ;

func u /\/ R -> UnOp of (Class R) means :: FILTER_1:def 3

for x, y being set st x in Class R & y in x holds

it . x = Class (R,(u . y));

existence for x, y being set st x in Class R & y in x holds

it . x = Class (R,(u . y));

ex b

for x, y being set st x in Class R & y in x holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines /\/ FILTER_1:def 3 :

for D being non empty set

for R being Equivalence_Relation of D

for u being UnOp of D st u is UnOp of D,R holds

for b_{4} being UnOp of (Class R) holds

( b_{4} = u /\/ R iff for x, y being set st x in Class R & y in x holds

b_{4} . x = Class (R,(u . y)) );

for D being non empty set

for R being Equivalence_Relation of D

for u being UnOp of D st u is UnOp of D,R holds

for b

( b

b

definition

let D be non empty set ;

let R be Equivalence_Relation of D;

let b be BinOp of D;

assume A1: b is BinOp of D,R ;

ex b_{1} being BinOp of (Class R) st

for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds

b_{1} . (x,y) = Class (R,(b . (x1,y1)))

for b_{1}, b_{2} being BinOp of (Class R) st ( for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds

b_{1} . (x,y) = Class (R,(b . (x1,y1))) ) & ( for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds

b_{2} . (x,y) = Class (R,(b . (x1,y1))) ) holds

b_{1} = b_{2}

end;
let R be Equivalence_Relation of D;

let b be BinOp of D;

assume A1: b is BinOp of D,R ;

func b /\/ R -> BinOp of (Class R) means :Def4: :: FILTER_1:def 4

for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds

it . (x,y) = Class (R,(b . (x1,y1)));

existence for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds

it . (x,y) = Class (R,(b . (x1,y1)));

ex b

for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines /\/ FILTER_1:def 4 :

for D being non empty set

for R being Equivalence_Relation of D

for b being BinOp of D st b is BinOp of D,R holds

for b_{4} being BinOp of (Class R) holds

( b_{4} = b /\/ R iff for x, y, x1, y1 being set st x in Class R & y in Class R & x1 in x & y1 in y holds

b_{4} . (x,y) = Class (R,(b . (x1,y1))) );

for D being non empty set

for R being Equivalence_Relation of D

for b being BinOp of D st b is BinOp of D,R holds

for b

( b

b

theorem Th3: :: FILTER_1:3

for D being non empty set

for RD being Equivalence_Relation of D

for a, b being Element of D

for F being BinOp of D,RD holds (F /\/ RD) . ((Class (RD,a)),(Class (RD,b))) = Class (RD,(F . (a,b)))

for RD being Equivalence_Relation of D

for a, b being Element of D

for F being BinOp of D,RD holds (F /\/ RD) . ((Class (RD,a)),(Class (RD,b))) = Class (RD,(F . (a,b)))

proof end;

scheme :: FILTER_1:sch 1

SchAux1{ F_{1}() -> non empty set , F_{2}() -> Equivalence_Relation of F_{1}(), P_{1}[ set ] } :

provided

SchAux1{ F

provided

proof end;

theorem Th4: :: FILTER_1:4

for D being non empty set

for RD being Equivalence_Relation of D

for F being BinOp of D,RD st F is commutative holds

F /\/ RD is commutative

for RD being Equivalence_Relation of D

for F being BinOp of D,RD st F is commutative holds

F /\/ RD is commutative

proof end;

theorem Th5: :: FILTER_1:5

for D being non empty set

for RD being Equivalence_Relation of D

for F being BinOp of D,RD st F is associative holds

F /\/ RD is associative

for RD being Equivalence_Relation of D

for F being BinOp of D,RD st F is associative holds

F /\/ RD is associative

proof end;

theorem Th6: :: FILTER_1:6

for D being non empty set

for RD being Equivalence_Relation of D

for d being Element of D

for F being BinOp of D,RD st d is_a_left_unity_wrt F holds

EqClass (RD,d) is_a_left_unity_wrt F /\/ RD

for RD being Equivalence_Relation of D

for d being Element of D

for F being BinOp of D,RD st d is_a_left_unity_wrt F holds

EqClass (RD,d) is_a_left_unity_wrt F /\/ RD

proof end;

theorem Th7: :: FILTER_1:7

for D being non empty set

for RD being Equivalence_Relation of D

for d being Element of D

for F being BinOp of D,RD st d is_a_right_unity_wrt F holds

EqClass (RD,d) is_a_right_unity_wrt F /\/ RD

for RD being Equivalence_Relation of D

for d being Element of D

for F being BinOp of D,RD st d is_a_right_unity_wrt F holds

EqClass (RD,d) is_a_right_unity_wrt F /\/ RD

proof end;

theorem :: FILTER_1:8

for D being non empty set

for RD being Equivalence_Relation of D

for d being Element of D

for F being BinOp of D,RD st d is_a_unity_wrt F holds

EqClass (RD,d) is_a_unity_wrt F /\/ RD by Th6, Th7;

for RD being Equivalence_Relation of D

for d being Element of D

for F being BinOp of D,RD st d is_a_unity_wrt F holds

EqClass (RD,d) is_a_unity_wrt F /\/ RD by Th6, Th7;

theorem Th9: :: FILTER_1:9

for D being non empty set

for RD being Equivalence_Relation of D

for F, G being BinOp of D,RD st F is_left_distributive_wrt G holds

F /\/ RD is_left_distributive_wrt G /\/ RD

for RD being Equivalence_Relation of D

for F, G being BinOp of D,RD st F is_left_distributive_wrt G holds

F /\/ RD is_left_distributive_wrt G /\/ RD

proof end;

theorem Th10: :: FILTER_1:10

for D being non empty set

for RD being Equivalence_Relation of D

for F, G being BinOp of D,RD st F is_right_distributive_wrt G holds

F /\/ RD is_right_distributive_wrt G /\/ RD

for RD being Equivalence_Relation of D

for F, G being BinOp of D,RD st F is_right_distributive_wrt G holds

F /\/ RD is_right_distributive_wrt G /\/ RD

proof end;

theorem :: FILTER_1:11

for D being non empty set

for RD being Equivalence_Relation of D

for F, G being BinOp of D,RD st F is_distributive_wrt G holds

F /\/ RD is_distributive_wrt G /\/ RD by Th9, Th10;

for RD being Equivalence_Relation of D

for F, G being BinOp of D,RD st F is_distributive_wrt G holds

F /\/ RD is_distributive_wrt G /\/ RD by Th9, Th10;

theorem Th12: :: FILTER_1:12

for D being non empty set

for RD being Equivalence_Relation of D

for F, G being BinOp of D,RD st F absorbs G holds

F /\/ RD absorbs G /\/ RD

for RD being Equivalence_Relation of D

for F, G being BinOp of D,RD st F absorbs G holds

F /\/ RD absorbs G /\/ RD

proof end;

theorem Th13: :: FILTER_1:13

for I being I_Lattice

for FI being Filter of I holds the L_join of I is BinOp of the carrier of I, equivalence_wrt FI

for FI being Filter of I holds the L_join of I is BinOp of the carrier of I, equivalence_wrt FI

proof end;

theorem Th14: :: FILTER_1:14

for I being I_Lattice

for FI being Filter of I holds the L_meet of I is BinOp of the carrier of I, equivalence_wrt FI

for FI being Filter of I holds the L_meet of I is BinOp of the carrier of I, equivalence_wrt FI

proof end;

definition

let L be Lattice;

let F be Filter of L;

assume A1: L is I_Lattice ;

ex b_{1} being strict Lattice st

for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

b_{1} = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #)

for b_{1}, b_{2} being strict Lattice st ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

b_{1} = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) ) & ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

b_{2} = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) ) holds

b_{1} = b_{2}

end;
let F be Filter of L;

assume A1: L is I_Lattice ;

func L /\/ F -> strict Lattice means :Def5: :: FILTER_1:def 5

for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

it = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #);

existence for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

it = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #);

ex b

for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines /\/ FILTER_1:def 5 :

for L being Lattice

for F being Filter of L st L is I_Lattice holds

for b_{3} being strict Lattice holds

( b_{3} = L /\/ F iff for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

b_{3} = LattStr(# (Class R),( the L_join of L /\/ R),( the L_meet of L /\/ R) #) );

for L being Lattice

for F being Filter of L st L is I_Lattice holds

for b

( b

b

definition

let L be Lattice;

let F be Filter of L;

let a be Element of L;

assume A1: L is I_Lattice ;

ex b_{1} being Element of (L /\/ F) st

for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

b_{1} = Class (R,a)

for b_{1}, b_{2} being Element of (L /\/ F) st ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

b_{1} = Class (R,a) ) & ( for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

b_{2} = Class (R,a) ) holds

b_{1} = b_{2}

end;
let F be Filter of L;

let a be Element of L;

assume A1: L is I_Lattice ;

func a /\/ F -> Element of (L /\/ F) means :Def6: :: FILTER_1:def 6

for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

it = Class (R,a);

existence for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

it = Class (R,a);

ex b

for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines /\/ FILTER_1:def 6 :

for L being Lattice

for F being Filter of L

for a being Element of L st L is I_Lattice holds

for b_{4} being Element of (L /\/ F) holds

( b_{4} = a /\/ F iff for R being Equivalence_Relation of the carrier of L st R = equivalence_wrt F holds

b_{4} = Class (R,a) );

for L being Lattice

for F being Filter of L

for a being Element of L st L is I_Lattice holds

for b

( b

b

theorem Th15: :: FILTER_1:15

for I being I_Lattice

for FI being Filter of I

for i, j being Element of I holds

( (i /\/ FI) "\/" (j /\/ FI) = (i "\/" j) /\/ FI & (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI )

for FI being Filter of I

for i, j being Element of I holds

( (i /\/ FI) "\/" (j /\/ FI) = (i "\/" j) /\/ FI & (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI )

proof end;

theorem Th16: :: FILTER_1:16

for I being I_Lattice

for FI being Filter of I

for i, j being Element of I holds

( i /\/ FI [= j /\/ FI iff i => j in FI )

for FI being Filter of I

for i, j being Element of I holds

( i /\/ FI [= j /\/ FI iff i => j in FI )

proof end;

theorem Th18: :: FILTER_1:18

for I being I_Lattice

for FI being Filter of I st I is lower-bounded holds

( I /\/ FI is 0_Lattice & Bottom (I /\/ FI) = (Bottom I) /\/ FI )

for FI being Filter of I st I is lower-bounded holds

( I /\/ FI is 0_Lattice & Bottom (I /\/ FI) = (Bottom I) /\/ FI )

proof end;

theorem Th19: :: FILTER_1:19

for I being I_Lattice

for FI being Filter of I holds

( I /\/ FI is 1_Lattice & Top (I /\/ FI) = (Top I) /\/ FI )

for FI being Filter of I holds

( I /\/ FI is 1_Lattice & Top (I /\/ FI) = (Top I) /\/ FI )

proof end;

registration
end;

definition

let D1, D2 be set ;

let f1 be BinOp of D1;

let f2 be BinOp of D2;

:: original: |:

redefine func |:f1,f2:| -> BinOp of [:D1,D2:];

coherence

|:f1,f2:| is BinOp of [:D1,D2:]

end;
let f1 be BinOp of D1;

let f2 be BinOp of D2;

:: original: |:

redefine func |:f1,f2:| -> BinOp of [:D1,D2:];

coherence

|:f1,f2:| is BinOp of [:D1,D2:]

proof end;

theorem Th21: :: FILTER_1:21

for D1, D2 being non empty set

for a1, b1 being Element of D1

for a2, b2 being Element of D2

for f1 being BinOp of D1

for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]

for a1, b1 being Element of D1

for a2, b2 being Element of D2

for f1 being BinOp of D1

for f2 being BinOp of D2 holds |:f1,f2:| . ([a1,a2],[b1,b2]) = [(f1 . (a1,b1)),(f2 . (a2,b2))]

proof end;

theorem Th22: :: FILTER_1:22

for D1, D2 being non empty set

for f1 being BinOp of D1

for f2 being BinOp of D2 holds

( ( f1 is commutative & f2 is commutative ) iff |:f1,f2:| is commutative )

for f1 being BinOp of D1

for f2 being BinOp of D2 holds

( ( f1 is commutative & f2 is commutative ) iff |:f1,f2:| is commutative )

proof end;

theorem Th23: :: FILTER_1:23

for D1, D2 being non empty set

for f1 being BinOp of D1

for f2 being BinOp of D2 holds

( ( f1 is associative & f2 is associative ) iff |:f1,f2:| is associative )

for f1 being BinOp of D1

for f2 being BinOp of D2 holds

( ( f1 is associative & f2 is associative ) iff |:f1,f2:| is associative )

proof end;

theorem Th24: :: FILTER_1:24

for D1, D2 being non empty set

for a1 being Element of D1

for a2 being Element of D2

for f1 being BinOp of D1

for f2 being BinOp of D2 holds

( ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) iff [a1,a2] is_a_left_unity_wrt |:f1,f2:| )

for a1 being Element of D1

for a2 being Element of D2

for f1 being BinOp of D1

for f2 being BinOp of D2 holds

( ( a1 is_a_left_unity_wrt f1 & a2 is_a_left_unity_wrt f2 ) iff [a1,a2] is_a_left_unity_wrt |:f1,f2:| )

proof end;

theorem Th25: :: FILTER_1:25

for D1, D2 being non empty set

for a1 being Element of D1

for a2 being Element of D2

for f1 being BinOp of D1

for f2 being BinOp of D2 holds

( ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_unity_wrt |:f1,f2:| )

for a1 being Element of D1

for a2 being Element of D2

for f1 being BinOp of D1

for f2 being BinOp of D2 holds

( ( a1 is_a_right_unity_wrt f1 & a2 is_a_right_unity_wrt f2 ) iff [a1,a2] is_a_right_unity_wrt |:f1,f2:| )

proof end;

theorem :: FILTER_1:26

for D1, D2 being non empty set

for a1 being Element of D1

for a2 being Element of D2

for f1 being BinOp of D1

for f2 being BinOp of D2 holds

( ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) iff [a1,a2] is_a_unity_wrt |:f1,f2:| ) by Th24, Th25;

for a1 being Element of D1

for a2 being Element of D2

for f1 being BinOp of D1

for f2 being BinOp of D2 holds

( ( a1 is_a_unity_wrt f1 & a2 is_a_unity_wrt f2 ) iff [a1,a2] is_a_unity_wrt |:f1,f2:| ) by Th24, Th25;

theorem Th27: :: FILTER_1:27

for D1, D2 being non empty set

for f1, g1 being BinOp of D1

for f2, g2 being BinOp of D2 holds

( ( f1 is_left_distributive_wrt g1 & f2 is_left_distributive_wrt g2 ) iff |:f1,f2:| is_left_distributive_wrt |:g1,g2:| )

for f1, g1 being BinOp of D1

for f2, g2 being BinOp of D2 holds

( ( f1 is_left_distributive_wrt g1 & f2 is_left_distributive_wrt g2 ) iff |:f1,f2:| is_left_distributive_wrt |:g1,g2:| )

proof end;

theorem Th28: :: FILTER_1:28

for D1, D2 being non empty set

for f1, g1 being BinOp of D1

for f2, g2 being BinOp of D2 holds

( ( f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 ) iff |:f1,f2:| is_right_distributive_wrt |:g1,g2:| )

for f1, g1 being BinOp of D1

for f2, g2 being BinOp of D2 holds

( ( f1 is_right_distributive_wrt g1 & f2 is_right_distributive_wrt g2 ) iff |:f1,f2:| is_right_distributive_wrt |:g1,g2:| )

proof end;

theorem Th29: :: FILTER_1:29

for D1, D2 being non empty set

for f1, g1 being BinOp of D1

for f2, g2 being BinOp of D2 holds

( ( f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 ) iff |:f1,f2:| is_distributive_wrt |:g1,g2:| ) by Th27, Th28;

for f1, g1 being BinOp of D1

for f2, g2 being BinOp of D2 holds

( ( f1 is_distributive_wrt g1 & f2 is_distributive_wrt g2 ) iff |:f1,f2:| is_distributive_wrt |:g1,g2:| ) by Th27, Th28;

theorem Th30: :: FILTER_1:30

for D1, D2 being non empty set

for f1, g1 being BinOp of D1

for f2, g2 being BinOp of D2 holds

( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )

for f1, g1 being BinOp of D1

for f2, g2 being BinOp of D2 holds

( ( f1 absorbs g1 & f2 absorbs g2 ) iff |:f1,f2:| absorbs |:g1,g2:| )

proof end;

definition

let L1, L2 be non empty LattStr ;

coherence

LattStr(# [: the carrier of L1, the carrier of L2:],|: the L_join of L1, the L_join of L2:|,|: the L_meet of L1, the L_meet of L2:| #) is strict LattStr ;

;

end;
func [:L1,L2:] -> strict LattStr equals :: FILTER_1:def 7

LattStr(# [: the carrier of L1, the carrier of L2:],|: the L_join of L1, the L_join of L2:|,|: the L_meet of L1, the L_meet of L2:| #);

correctness LattStr(# [: the carrier of L1, the carrier of L2:],|: the L_join of L1, the L_join of L2:|,|: the L_meet of L1, the L_meet of L2:| #);

coherence

LattStr(# [: the carrier of L1, the carrier of L2:],|: the L_join of L1, the L_join of L2:|,|: the L_meet of L1, the L_meet of L2:| #) is strict LattStr ;

;

:: deftheorem defines [: FILTER_1:def 7 :

for L1, L2 being non empty LattStr holds [:L1,L2:] = LattStr(# [: the carrier of L1, the carrier of L2:],|: the L_join of L1, the L_join of L2:|,|: the L_meet of L1, the L_meet of L2:| #);

for L1, L2 being non empty LattStr holds [:L1,L2:] = LattStr(# [: the carrier of L1, the carrier of L2:],|: the L_join of L1, the L_join of L2:|,|: the L_meet of L1, the L_meet of L2:| #);

definition
end;

:: deftheorem defines LattRel FILTER_1:def 8 :

for L being Lattice holds LattRel L = { [p,q] where p, q is Element of L : p [= q } ;

for L being Lattice holds LattRel L = { [p,q] where p, q is Element of L : p [= q } ;

theorem Th32: :: FILTER_1:32

for L being Lattice holds

( dom (LattRel L) = the carrier of L & rng (LattRel L) = the carrier of L & field (LattRel L) = the carrier of L )

( dom (LattRel L) = the carrier of L & rng (LattRel L) = the carrier of L & field (LattRel L) = the carrier of L )

proof end;

definition

let L1, L2 be Lattice;

reflexivity

for L1 being Lattice holds LattRel L1, LattRel L1 are_isomorphic by WELLORD1:38;

symmetry

for L1, L2 being Lattice st LattRel L1, LattRel L2 are_isomorphic holds

LattRel L2, LattRel L1 are_isomorphic by WELLORD1:40;

end;
reflexivity

for L1 being Lattice holds LattRel L1, LattRel L1 are_isomorphic by WELLORD1:38;

symmetry

for L1, L2 being Lattice st LattRel L1, LattRel L2 are_isomorphic holds

LattRel L2, LattRel L1 are_isomorphic by WELLORD1:40;

:: deftheorem defines are_isomorphic FILTER_1:def 9 :

for L1, L2 being Lattice holds

( L1,L2 are_isomorphic iff LattRel L1, LattRel L2 are_isomorphic );

for L1, L2 being Lattice holds

( L1,L2 are_isomorphic iff LattRel L1, LattRel L2 are_isomorphic );

theorem :: FILTER_1:33

for L1, L2, L3 being Lattice st L1,L2 are_isomorphic & L2,L3 are_isomorphic holds

L1,L3 are_isomorphic by WELLORD1:42;

L1,L3 are_isomorphic by WELLORD1:42;

definition

let L1, L2 be Lattice;

let a be Element of L1;

let b be Element of L2;

:: original: [

redefine func [a,b] -> Element of [:L1,L2:];

coherence

[a,b] is Element of [:L1,L2:]

end;
let a be Element of L1;

let b be Element of L2;

:: original: [

redefine func [a,b] -> Element of [:L1,L2:];

coherence

[a,b] is Element of [:L1,L2:]

proof end;

theorem :: FILTER_1:35

theorem Th36: :: FILTER_1:36

for L1, L2 being Lattice

for p1, q1 being Element of L1

for p2, q2 being Element of L2 holds

( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )

for p1, q1 being Element of L1

for p2, q2 being Element of L2 holds

( [p1,p2] [= [q1,q2] iff ( p1 [= q1 & p2 [= q2 ) )

proof end;

theorem Th39: :: FILTER_1:39

for L1, L2 being Lattice holds

( ( L1 is lower-bounded & L2 is lower-bounded ) iff [:L1,L2:] is lower-bounded )

( ( L1 is lower-bounded & L2 is lower-bounded ) iff [:L1,L2:] is lower-bounded )

proof end;

theorem Th40: :: FILTER_1:40

for L1, L2 being Lattice holds

( ( L1 is upper-bounded & L2 is upper-bounded ) iff [:L1,L2:] is upper-bounded )

( ( L1 is upper-bounded & L2 is upper-bounded ) iff [:L1,L2:] is upper-bounded )

proof end;

theorem Th42: :: FILTER_1:42

for L1, L2 being Lattice st L1 is 0_Lattice & L2 is 0_Lattice holds

Bottom [:L1,L2:] = [(Bottom L1),(Bottom L2)]

Bottom [:L1,L2:] = [(Bottom L1),(Bottom L2)]

proof end;

theorem Th43: :: FILTER_1:43

for L1, L2 being Lattice st L1 is 1_Lattice & L2 is 1_Lattice holds

Top [:L1,L2:] = [(Top L1),(Top L2)]

Top [:L1,L2:] = [(Top L1),(Top L2)]

proof end;

theorem Th44: :: FILTER_1:44

for L1, L2 being Lattice

for p1, q1 being Element of L1

for p2, q2 being Element of L2 st L1 is 01_Lattice & L2 is 01_Lattice holds

( ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 ) iff [p1,p2] is_a_complement_of [q1,q2] )

for p1, q1 being Element of L1

for p2, q2 being Element of L2 st L1 is 01_Lattice & L2 is 01_Lattice holds

( ( p1 is_a_complement_of q1 & p2 is_a_complement_of q2 ) iff [p1,p2] is_a_complement_of [q1,q2] )

proof end;

theorem :: FILTER_1:47

for L1, L2 being Lattice holds

( ( L1 is implicative & L2 is implicative ) iff [:L1,L2:] is implicative )

( ( L1 is implicative & L2 is implicative ) iff [:L1,L2:] is implicative )

proof end;

theorem Th50: :: FILTER_1:50

for B being B_Lattice

for a, b being Element of B holds a <=> b = (a "/\" b) "\/" ((a `) "/\" (b `))

for a, b being Element of B holds a <=> b = (a "/\" b) "\/" ((a `) "/\" (b `))

proof end;

theorem Th51: :: FILTER_1:51

for B being B_Lattice

for a, b being Element of B holds

( (a => b) ` = a "/\" (b `) & (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" b) & (a <=> b) ` = a <=> (b `) & (a <=> b) ` = (a `) <=> b )

for a, b being Element of B holds

( (a => b) ` = a "/\" (b `) & (a <=> b) ` = (a "/\" (b `)) "\/" ((a `) "/\" b) & (a <=> b) ` = a <=> (b `) & (a <=> b) ` = (a `) <=> b )

proof end;

theorem :: FILTER_1:54

for I being I_Lattice

for i, j being Element of I holds

( (i "\/" j) => i = j => i & i => (i "/\" j) = i => j )

for i, j being Element of I holds

( (i "\/" j) => i = j => i & i => (i "/\" j) = i => j )

proof end;

theorem Th55: :: FILTER_1:55

for I being I_Lattice

for i, j, k being Element of I holds

( i => j [= i => (j "\/" k) & i => j [= (i "/\" k) => j & i => j [= i => (k "\/" j) & i => j [= (k "/\" i) => j )

for i, j, k being Element of I holds

( i => j [= i => (j "\/" k) & i => j [= (i "/\" k) => j & i => j [= i => (k "\/" j) & i => j [= (k "/\" i) => j )

proof end;

Lm1: for I being I_Lattice

for FI being Filter of I

for i, j, k being Element of I st i => j in FI holds

( i => (j "\/" k) in FI & i => (k "\/" j) in FI & (i "/\" k) => j in FI & (k "/\" i) => j in FI )

proof end;

theorem Th56: :: FILTER_1:56

for I being I_Lattice

for i, j, k being Element of I holds (i => k) "/\" (j => k) [= (i "\/" j) => k

for i, j, k being Element of I holds (i => k) "/\" (j => k) [= (i "\/" j) => k

proof end;

Lm2: for I being I_Lattice

for FI being Filter of I

for i, j, k being Element of I st i => k in FI & j => k in FI holds

(i "\/" j) => k in FI

proof end;

theorem Th57: :: FILTER_1:57

for I being I_Lattice

for i, j, k being Element of I holds (i => j) "/\" (i => k) [= i => (j "/\" k)

for i, j, k being Element of I holds (i => j) "/\" (i => k) [= i => (j "/\" k)

proof end;

Lm3: for I being I_Lattice

for FI being Filter of I

for i, j, k being Element of I st i => j in FI & i => k in FI holds

i => (j "/\" k) in FI

proof end;

theorem Th58: :: FILTER_1:58

for I being I_Lattice

for FI being Filter of I

for i1, i2, j1, j2 being Element of I st i1 <=> i2 in FI & j1 <=> j2 in FI holds

( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI )

for FI being Filter of I

for i1, i2, j1, j2 being Element of I st i1 <=> i2 in FI & j1 <=> j2 in FI holds

( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI )

proof end;

Lm4: for I being I_Lattice

for FI being Filter of I

for i, j being Element of I holds

( i in Class ((equivalence_wrt FI),j) iff i <=> j in FI )

proof end;

theorem Th59: :: FILTER_1:59

for I being I_Lattice

for FI being Filter of I

for i, j, k being Element of I st i in Class ((equivalence_wrt FI),k) & j in Class ((equivalence_wrt FI),k) holds

( i "\/" j in Class ((equivalence_wrt FI),k) & i "/\" j in Class ((equivalence_wrt FI),k) )

for FI being Filter of I

for i, j, k being Element of I st i in Class ((equivalence_wrt FI),k) & j in Class ((equivalence_wrt FI),k) holds

( i "\/" j in Class ((equivalence_wrt FI),k) & i "/\" j in Class ((equivalence_wrt FI),k) )

proof end;

theorem Th60: :: FILTER_1:60

for B being B_Lattice

for c, d being Element of B holds

( c "\/" (c <=> d) in Class ((equivalence_wrt <.d.)),c) & ( for b being Element of B st b in Class ((equivalence_wrt <.d.)),c) holds

b [= c "\/" (c <=> d) ) )

for c, d being Element of B holds

( c "\/" (c <=> d) in Class ((equivalence_wrt <.d.)),c) & ( for b being Element of B st b in Class ((equivalence_wrt <.d.)),c) holds

b [= c "\/" (c <=> d) ) )

proof end;

theorem :: FILTER_1:61

for B being B_Lattice

for a being Element of B holds B,[:(B /\/ <.a.)),(latt <.a.)):] are_isomorphic

for a being Element of B holds B,[:(B /\/ <.a.)),(latt <.a.)):] are_isomorphic

proof end;