:: by Jolanta Kamie\'nska and Jaros\l aw Stanis\l aw Walijewski

::

:: Received July 14, 1993

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

begin

theorem :: LATTICE4:1

for X being set st X <> {} & ( for Z being set st Z <> {} & Z c= X & Z is c=-linear holds

ex Y being set st

( Y in X & ( for X1 being set st X1 in Z holds

X1 c= Y ) ) ) holds

ex Y being set st

( Y in X & ( for Z being set st Z in X & Z <> Y holds

not Y c= Z ) )

ex Y being set st

( Y in X & ( for X1 being set st X1 in Z holds

X1 c= Y ) ) ) holds

ex Y being set st

( Y in X & ( for Z being set st Z in X & Z <> Y holds

not Y c= Z ) )

proof end;

begin

theorem :: LATTICE4:3

for L being Lattice

for F being Filter of L

for p, q being Element of L st p in <.(<.q.) \/ F).) holds

ex r being Element of L st

( r in F & q "/\" r [= p )

for F being Filter of L

for p, q being Element of L st p in <.(<.q.) \/ F).) holds

ex r being Element of L st

( r in F & q "/\" r [= p )

proof end;

definition

let L1, L2 be Lattice;

ex b_{1} being Function of the carrier of L1, the carrier of L2 st

for a1, b1 being Element of L1 holds

( b_{1} . (a1 "\/" b1) = (b_{1} . a1) "\/" (b_{1} . b1) & b_{1} . (a1 "/\" b1) = (b_{1} . a1) "/\" (b_{1} . b1) )

end;
mode Homomorphism of L1,L2 -> Function of the carrier of L1, the carrier of L2 means :Def1: :: LATTICE4:def 1

for a1, b1 being Element of L1 holds

( it . (a1 "\/" b1) = (it . a1) "\/" (it . b1) & it . (a1 "/\" b1) = (it . a1) "/\" (it . b1) );

existence for a1, b1 being Element of L1 holds

( it . (a1 "\/" b1) = (it . a1) "\/" (it . b1) & it . (a1 "/\" b1) = (it . a1) "/\" (it . b1) );

ex b

for a1, b1 being Element of L1 holds

( b

proof end;

:: deftheorem Def1 defines Homomorphism LATTICE4:def 1 :

for L1, L2 being Lattice

for b_{3} being Function of the carrier of L1, the carrier of L2 holds

( b_{3} is Homomorphism of L1,L2 iff for a1, b1 being Element of L1 holds

( b_{3} . (a1 "\/" b1) = (b_{3} . a1) "\/" (b_{3} . b1) & b_{3} . (a1 "/\" b1) = (b_{3} . a1) "/\" (b_{3} . b1) ) );

for L1, L2 being Lattice

for b

( b

( b

theorem Th4: :: LATTICE4:4

for L1, L2 being Lattice

for a1, b1 being Element of L1

for f being Homomorphism of L1,L2 st a1 [= b1 holds

f . a1 [= f . b1

for a1, b1 being Element of L1

for f being Homomorphism of L1,L2 st a1 [= b1 holds

f . a1 [= f . b1

proof end;

theorem Th5: :: LATTICE4:5

for L1, L2 being Lattice

for a1, b1 being Element of L1

for f being Homomorphism of L1,L2 st f is one-to-one holds

( a1 [= b1 iff f . a1 [= f . b1 )

for a1, b1 being Element of L1

for f being Homomorphism of L1,L2 st f is one-to-one holds

( a1 [= b1 iff f . a1 [= f . b1 )

proof end;

theorem Th6: :: LATTICE4:6

for L1, L2 being Lattice

for f being Function of the carrier of L1, the carrier of L2 st f is onto holds

for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1

for f being Function of the carrier of L1, the carrier of L2 st f is onto holds

for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1

proof end;

definition

let L1, L2 be Lattice;

( L1,L2 are_isomorphic iff ex f being Homomorphism of L1,L2 st f is bijective )

end;
redefine pred L1,L2 are_isomorphic means :: LATTICE4:def 2

ex f being Homomorphism of L1,L2 st f is bijective ;

compatibility ex f being Homomorphism of L1,L2 st f is bijective ;

( L1,L2 are_isomorphic iff ex f being Homomorphism of L1,L2 st f is bijective )

proof end;

:: deftheorem defines are_isomorphic LATTICE4:def 2 :

for L1, L2 being Lattice holds

( L1,L2 are_isomorphic iff ex f being Homomorphism of L1,L2 st f is bijective );

for L1, L2 being Lattice holds

( L1,L2 are_isomorphic iff ex f being Homomorphism of L1,L2 st f is bijective );

definition

let L1, L2 be Lattice;

let f be Homomorphism of L1,L2;

end;
let f be Homomorphism of L1,L2;

pred f preserves_implication means :Def3: :: LATTICE4:def 3

for a1, b1 being Element of L1 holds f . (a1 => b1) = (f . a1) => (f . b1);

for a1, b1 being Element of L1 holds f . (a1 => b1) = (f . a1) => (f . b1);

pred f preserves_complement means :Def6: :: LATTICE4:def 6

for a1 being Element of L1 holds f . (a1 `) = (f . a1) ` ;

for a1 being Element of L1 holds f . (a1 `) = (f . a1) ` ;

:: deftheorem Def3 defines preserves_implication LATTICE4:def 3 :

for L1, L2 being Lattice

for f being Homomorphism of L1,L2 holds

( f preserves_implication iff for a1, b1 being Element of L1 holds f . (a1 => b1) = (f . a1) => (f . b1) );

for L1, L2 being Lattice

for f being Homomorphism of L1,L2 holds

( f preserves_implication iff for a1, b1 being Element of L1 holds f . (a1 => b1) = (f . a1) => (f . b1) );

:: deftheorem Def4 defines preserves_top LATTICE4:def 4 :

for L1, L2 being Lattice

for f being Homomorphism of L1,L2 holds

( f preserves_top iff f . (Top L1) = Top L2 );

for L1, L2 being Lattice

for f being Homomorphism of L1,L2 holds

( f preserves_top iff f . (Top L1) = Top L2 );

:: deftheorem Def5 defines preserves_bottom LATTICE4:def 5 :

for L1, L2 being Lattice

for f being Homomorphism of L1,L2 holds

( f preserves_bottom iff f . (Bottom L1) = Bottom L2 );

for L1, L2 being Lattice

for f being Homomorphism of L1,L2 holds

( f preserves_bottom iff f . (Bottom L1) = Bottom L2 );

:: deftheorem Def6 defines preserves_complement LATTICE4:def 6 :

for L1, L2 being Lattice

for f being Homomorphism of L1,L2 holds

( f preserves_complement iff for a1 being Element of L1 holds f . (a1 `) = (f . a1) ` );

for L1, L2 being Lattice

for f being Homomorphism of L1,L2 holds

( f preserves_complement iff for a1 being Element of L1 holds f . (a1 `) = (f . a1) ` );

registration
end;

definition

let L be Lattice;

let B be Finite_Subset of the carrier of L;

coherence

FinJoin (B,(id L)) is Element of L ;

coherence

FinMeet (B,(id L)) is Element of L ;

end;
let B be Finite_Subset of the carrier of L;

coherence

FinJoin (B,(id L)) is Element of L ;

coherence

FinMeet (B,(id L)) is Element of L ;

:: deftheorem defines FinJoin LATTICE4:def 7 :

for L being Lattice

for B being Finite_Subset of the carrier of L holds FinJoin B = FinJoin (B,(id L));

for L being Lattice

for B being Finite_Subset of the carrier of L holds FinJoin B = FinJoin (B,(id L));

:: deftheorem defines FinMeet LATTICE4:def 8 :

for L being Lattice

for B being Finite_Subset of the carrier of L holds FinMeet B = FinMeet (B,(id L));

for L being Lattice

for B being Finite_Subset of the carrier of L holds FinMeet B = FinMeet (B,(id L));

begin

theorem Th11: :: LATTICE4:11

for L2 being Lattice

for DL being distributive Lattice

for f being Homomorphism of DL,L2 st f is onto holds

L2 is distributive

for DL being distributive Lattice

for f being Homomorphism of DL,L2 st f is onto holds

L2 is distributive

proof end;

begin

theorem Th12: :: LATTICE4:12

for L2 being Lattice

for 0L being lower-bounded Lattice

for f being Homomorphism of 0L,L2 st f is onto holds

( L2 is lower-bounded & f preserves_bottom )

for 0L being lower-bounded Lattice

for f being Homomorphism of 0L,L2 st f is onto holds

( L2 is lower-bounded & f preserves_bottom )

proof end;

theorem Th13: :: LATTICE4:13

for 0L being lower-bounded Lattice

for B being Finite_Subset of the carrier of 0L

for b being Element of 0L

for f being UnOp of the carrier of 0L holds FinJoin ((B \/ {.b.}),f) = (FinJoin (B,f)) "\/" (f . b)

for B being Finite_Subset of the carrier of 0L

for b being Element of 0L

for f being UnOp of the carrier of 0L holds FinJoin ((B \/ {.b.}),f) = (FinJoin (B,f)) "\/" (f . b)

proof end;

theorem Th14: :: LATTICE4:14

for 0L being lower-bounded Lattice

for B being Finite_Subset of the carrier of 0L

for b being Element of 0L holds FinJoin (B \/ {.b.}) = (FinJoin B) "\/" b

for B being Finite_Subset of the carrier of 0L

for b being Element of 0L holds FinJoin (B \/ {.b.}) = (FinJoin B) "\/" b

proof end;

theorem :: LATTICE4:15

for 0L being lower-bounded Lattice

for B1, B2 being Finite_Subset of the carrier of 0L holds (FinJoin B1) "\/" (FinJoin B2) = FinJoin (B1 \/ B2)

for B1, B2 being Finite_Subset of the carrier of 0L holds (FinJoin B1) "\/" (FinJoin B2) = FinJoin (B1 \/ B2)

proof end;

Lm1: for 0L being lower-bounded Lattice

for f being Function of the carrier of 0L, the carrier of 0L holds FinJoin (({}. the carrier of 0L),f) = Bottom 0L

proof end;

theorem :: LATTICE4:16

theorem Th17: :: LATTICE4:17

for 0L being lower-bounded Lattice

for A being ClosedSubset of 0L st Bottom 0L in A holds

for B being Finite_Subset of the carrier of 0L st B c= A holds

FinJoin B in A

for A being ClosedSubset of 0L st Bottom 0L in A holds

for B being Finite_Subset of the carrier of 0L st B c= A holds

FinJoin B in A

proof end;

begin

theorem Th18: :: LATTICE4:18

for L2 being Lattice

for 1L being upper-bounded Lattice

for f being Homomorphism of 1L,L2 st f is onto holds

( L2 is upper-bounded & f preserves_top )

for 1L being upper-bounded Lattice

for f being Homomorphism of 1L,L2 st f is onto holds

( L2 is upper-bounded & f preserves_top )

proof end;

Lm2: for 1L being upper-bounded Lattice

for f being Function of the carrier of 1L, the carrier of 1L holds FinMeet (({}. the carrier of 1L),f) = Top 1L

proof end;

theorem :: LATTICE4:19

theorem Th20: :: LATTICE4:20

for 1L being upper-bounded Lattice

for B being Finite_Subset of the carrier of 1L

for b being Element of 1L

for f being UnOp of the carrier of 1L holds FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b)

for B being Finite_Subset of the carrier of 1L

for b being Element of 1L

for f being UnOp of the carrier of 1L holds FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b)

proof end;

theorem Th21: :: LATTICE4:21

for 1L being upper-bounded Lattice

for B being Finite_Subset of the carrier of 1L

for b being Element of 1L holds FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b

for B being Finite_Subset of the carrier of 1L

for b being Element of 1L holds FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b

proof end;

theorem Th22: :: LATTICE4:22

for 1L being upper-bounded Lattice

for B being Finite_Subset of the carrier of 1L

for f, g being UnOp of the carrier of 1L holds FinMeet ((f .: B),g) = FinMeet (B,(g * f))

for B being Finite_Subset of the carrier of 1L

for f, g being UnOp of the carrier of 1L holds FinMeet ((f .: B),g) = FinMeet (B,(g * f))

proof end;

theorem Th23: :: LATTICE4:23

for 1L being upper-bounded Lattice

for B1, B2 being Finite_Subset of the carrier of 1L holds (FinMeet B1) "/\" (FinMeet B2) = FinMeet (B1 \/ B2)

for B1, B2 being Finite_Subset of the carrier of 1L holds (FinMeet B1) "/\" (FinMeet B2) = FinMeet (B1 \/ B2)

proof end;

theorem Th24: :: LATTICE4:24

for 1L being upper-bounded Lattice

for F being ClosedSubset of 1L st Top 1L in F holds

for B being Finite_Subset of the carrier of 1L st B c= F holds

FinMeet B in F

for F being ClosedSubset of 1L st Top 1L in F holds

for B being Finite_Subset of the carrier of 1L st B c= F holds

FinMeet B in F

proof end;

begin

Lm3: for DL being distributive upper-bounded Lattice

for B being Finite_Subset of the carrier of DL

for p being Element of DL

for f being UnOp of the carrier of DL holds the L_join of DL . (( the L_meet of DL $$ (B,f)),p) = the L_meet of DL $$ (B,( the L_join of DL [:] (f,p)))

proof end;

theorem Th25: :: LATTICE4:25

for DL being distributive upper-bounded Lattice

for B being Finite_Subset of the carrier of DL

for p being Element of DL holds (FinMeet B) "\/" p = FinMeet (( the L_join of DL [:] ((id DL),p)) .: B)

for B being Finite_Subset of the carrier of DL

for p being Element of DL holds (FinMeet B) "\/" p = FinMeet (( the L_join of DL [:] ((id DL),p)) .: B)

proof end;

begin

theorem Th26: :: LATTICE4:26

for CL being C_Lattice

for IL being implicative Lattice

for f being Homomorphism of IL,CL

for i, j being Element of IL holds (f . i) "/\" (f . (i => j)) [= f . j

for IL being implicative Lattice

for f being Homomorphism of IL,CL

for i, j being Element of IL holds (f . i) "/\" (f . (i => j)) [= f . j

proof end;

theorem Th27: :: LATTICE4:27

for CL being C_Lattice

for IL being implicative Lattice

for f being Homomorphism of IL,CL

for i, k, j being Element of IL st f is one-to-one & (f . i) "/\" (f . k) [= f . j holds

f . k [= f . (i => j)

for IL being implicative Lattice

for f being Homomorphism of IL,CL

for i, k, j being Element of IL st f is one-to-one & (f . i) "/\" (f . k) [= f . j holds

f . k [= f . (i => j)

proof end;

theorem :: LATTICE4:28

for CL being C_Lattice

for IL being implicative Lattice

for f being Homomorphism of IL,CL st f is bijective holds

( CL is implicative & f preserves_implication )

for IL being implicative Lattice

for f being Homomorphism of IL,CL st f is bijective holds

( CL is implicative & f preserves_implication )

proof end;

begin

theorem :: LATTICE4:31

for CL being C_Lattice

for BL being Boolean Lattice

for f being Homomorphism of BL,CL st f is onto holds

( CL is Boolean & f preserves_complement )

for BL being Boolean Lattice

for f being Homomorphism of BL,CL st f is onto holds

( CL is Boolean & f preserves_complement )

proof end;

definition

let BL be Boolean Lattice;

ex b_{1} being non empty Subset of BL st

for a, b being Element of BL st a in b_{1} & b in b_{1} holds

( a "/\" b in b_{1} & a ` in b_{1} )

end;
mode Field of BL -> non empty Subset of BL means :Def9: :: LATTICE4:def 9

for a, b being Element of BL st a in it & b in it holds

( a "/\" b in it & a ` in it );

existence for a, b being Element of BL st a in it & b in it holds

( a "/\" b in it & a ` in it );

ex b

for a, b being Element of BL st a in b

( a "/\" b in b

proof end;

:: deftheorem Def9 defines Field LATTICE4:def 9 :

for BL being Boolean Lattice

for b_{2} being non empty Subset of BL holds

( b_{2} is Field of BL iff for a, b being Element of BL st a in b_{2} & b in b_{2} holds

( a "/\" b in b_{2} & a ` in b_{2} ) );

for BL being Boolean Lattice

for b

( b

( a "/\" b in b

theorem Th32: :: LATTICE4:32

for BL being Boolean Lattice

for a, b being Element of BL

for F being Field of BL st a in F & b in F holds

a "\/" b in F

for a, b being Element of BL

for F being Field of BL st a in F & b in F holds

a "\/" b in F

proof end;

theorem Th33: :: LATTICE4:33

for BL being Boolean Lattice

for a, b being Element of BL

for F being Field of BL st a in F & b in F holds

a => b in F

for a, b being Element of BL

for F being Field of BL st a in F & b in F holds

a => b in F

proof end;

definition

let BL be Boolean Lattice;

let A be non empty Subset of BL;

ex b_{1} being Field of BL st

( A c= b_{1} & ( for F being Field of BL st A c= F holds

b_{1} c= F ) )

for b_{1}, b_{2} being Field of BL st A c= b_{1} & ( for F being Field of BL st A c= F holds

b_{1} c= F ) & A c= b_{2} & ( for F being Field of BL st A c= F holds

b_{2} c= F ) holds

b_{1} = b_{2}

end;
let A be non empty Subset of BL;

func field_by A -> Field of BL means :Def10: :: LATTICE4:def 10

( A c= it & ( for F being Field of BL st A c= F holds

it c= F ) );

existence ( A c= it & ( for F being Field of BL st A c= F holds

it c= F ) );

ex b

( A c= b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def10 defines field_by LATTICE4:def 10 :

for BL being Boolean Lattice

for A being non empty Subset of BL

for b_{3} being Field of BL holds

( b_{3} = field_by A iff ( A c= b_{3} & ( for F being Field of BL st A c= F holds

b_{3} c= F ) ) );

for BL being Boolean Lattice

for A being non empty Subset of BL

for b

( b

b

definition

let BL be Boolean Lattice;

let A be non empty Subset of BL;

{ (a => b) where a, b is Element of BL : ( a in A & b in A ) } is Subset of BL

end;
let A be non empty Subset of BL;

func SetImp A -> Subset of BL equals :: LATTICE4:def 11

{ (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;

coherence { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;

{ (a => b) where a, b is Element of BL : ( a in A & b in A ) } is Subset of BL

proof end;

:: deftheorem defines SetImp LATTICE4:def 11 :

for BL being Boolean Lattice

for A being non empty Subset of BL holds SetImp A = { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;

for BL being Boolean Lattice

for A being non empty Subset of BL holds SetImp A = { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;

registration

let BL be Boolean Lattice;

let A be non empty Subset of BL;

coherence

not SetImp A is empty

end;
let A be non empty Subset of BL;

coherence

not SetImp A is empty

proof end;

theorem :: LATTICE4:36

theorem Th37: :: LATTICE4:37

for BL being Boolean Lattice

for A being non empty Subset of BL

for c being Element of BL holds

( c in SetImp A iff ex p, q being Element of BL st

( c = (p `) "\/" q & p in A & q in A ) )

for A being non empty Subset of BL

for c being Element of BL holds

( c in SetImp A iff ex p, q being Element of BL st

( c = (p `) "\/" q & p in A & q in A ) )

proof end;

definition

let BL be Boolean Lattice;

deffunc H_{1}( Element of BL) -> Element of the carrier of BL = $1 ` ;

ex b_{1} being Function of the carrier of BL, the carrier of BL st

for a being Element of BL holds b_{1} . a = a `

for b_{1}, b_{2} being Function of the carrier of BL, the carrier of BL st ( for a being Element of BL holds b_{1} . a = a ` ) & ( for a being Element of BL holds b_{2} . a = a ` ) holds

b_{1} = b_{2}

end;
deffunc H

func comp BL -> Function of the carrier of BL, the carrier of BL means :Def12: :: LATTICE4:def 12

for a being Element of BL holds it . a = a ` ;

existence for a being Element of BL holds it . a = a ` ;

ex b

for a being Element of BL holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def12 defines comp LATTICE4:def 12 :

for BL being Boolean Lattice

for b_{2} being Function of the carrier of BL, the carrier of BL holds

( b_{2} = comp BL iff for a being Element of BL holds b_{2} . a = a ` );

for BL being Boolean Lattice

for b

( b

theorem Th38: :: LATTICE4:38

for BL being Boolean Lattice

for b being Element of BL

for B being Finite_Subset of the carrier of BL holds FinJoin ((B \/ {.b.}),(comp BL)) = (FinJoin (B,(comp BL))) "\/" (b `)

for b being Element of BL

for B being Finite_Subset of the carrier of BL holds FinJoin ((B \/ {.b.}),(comp BL)) = (FinJoin (B,(comp BL))) "\/" (b `)

proof end;

theorem :: LATTICE4:39

for BL being Boolean Lattice

for B being Finite_Subset of the carrier of BL holds (FinJoin B) ` = FinMeet (B,(comp BL))

for B being Finite_Subset of the carrier of BL holds (FinJoin B) ` = FinMeet (B,(comp BL))

proof end;

theorem :: LATTICE4:40

for BL being Boolean Lattice

for b being Element of BL

for B being Finite_Subset of the carrier of BL holds FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" (b `)

for b being Element of BL

for B being Finite_Subset of the carrier of BL holds FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" (b `)

proof end;

theorem Th41: :: LATTICE4:41

for BL being Boolean Lattice

for B being Finite_Subset of the carrier of BL holds (FinMeet B) ` = FinJoin (B,(comp BL))

for B being Finite_Subset of the carrier of BL holds (FinMeet B) ` = FinJoin (B,(comp BL))

proof end;

theorem Th42: :: LATTICE4:42

for BL being Boolean Lattice

for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds

for B being Finite_Subset of the carrier of BL st B c= SetImp AF holds

ex B0 being Finite_Subset of the carrier of BL st

( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )

for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds

for B being Finite_Subset of the carrier of BL st B c= SetImp AF holds

ex B0 being Finite_Subset of the carrier of BL st

( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )

proof end;

theorem :: LATTICE4:43

for BL being Boolean Lattice

for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds

{ (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } = field_by AF

for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds

{ (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } = field_by AF

proof end;