:: LATTICE4 semantic presentation

theorem :: LATTICE4:1

canceled;

theorem :: LATTICE4:2

canceled;

theorem :: LATTICE4:3

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

proof end;

theorem :: LATTICE4:4

for L being Lattice holds <.L.) is prime

proof end;

theorem :: LATTICE4:5

for L being Lattice
for F, H being Filter of L holds
( F c= <.(F \/ H).) & H c= <.(F \/ H).) )

proof end;

theorem :: LATTICE4:6

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 )

proof end;

definition

let L1, L2 be Lattice;
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

proof end;

end;

:: deftheorem Def1 defines Homomorphism LATTICE4:def 1 :

theorem Th7: :: LATTICE4:7

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

proof end;

definition

let L1, L2 be Lattice;
let f be Function of the carrier of L1,the carrier of L2;
attr f is monomorphism means :Def2: :: LATTICE4:def 2
f is one-to-one;
attr f is epimorphism means :Def3: :: LATTICE4:def 3
rng f = the carrier of L2;

end;

:: deftheorem Def2 defines monomorphism LATTICE4:def 2 :

:: deftheorem Def3 defines epimorphism LATTICE4:def 3 :

theorem Th8: :: LATTICE4:8

for L1, L2 being Lattice
for a1, b1 being Element of L1
for f being Homomorphism of L1,L2 st f is monomorphism holds
( a1 [= b1 iff f . a1 [= f . b1 )

proof end;

theorem Th9: :: LATTICE4:9

for L1, L2 being Lattice
for f being Function of the carrier of L1,the carrier of L2 st f is epimorphism 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;
let f be Homomorphism of L1,L2;
attr f is isomorphism means :Def4: :: LATTICE4:def 4
( f is monomorphism & f is epimorphism );

end;

:: deftheorem Def4 defines isomorphism LATTICE4:def 4 :

definition

let L1, L2 be Lattice;
redefine pred L1,L2 are_isomorphic means :: LATTICE4:def 5
ex f being Homomorphism of L1,L2 st f is isomorphism;
compatibility

proof end;

end;

:: deftheorem defines are_isomorphic LATTICE4:def 5 :

definition

let L1, L2 be Lattice;
let f be Homomorphism of L1,L2;
pred f preserves_implication means :Def6: :: LATTICE4:def 6
for a1, b1 being Element of L1 holds f . (a1 => b1) = (f . a1) => (f . b1);
pred f preserves_top means :Def7: :: LATTICE4:def 7
f . (Top L1) = Top L2;
pred f preserves_bottom means :Def8: :: LATTICE4:def 8
f . (Bottom L1) = Bottom L2;
pred f preserves_complement means :Def9: :: LATTICE4:def 9
for a1 being Element of L1 holds f . (a1 ` ) = (f . a1) ` ;

end;

:: deftheorem Def6 defines preserves_implication LATTICE4:def 6 :

:: deftheorem Def7 defines preserves_top LATTICE4:def 7 :

:: deftheorem Def8 defines preserves_bottom LATTICE4:def 8 :

:: deftheorem Def9 defines preserves_complement LATTICE4:def 9 :

definition

let L be Lattice;
mode ClosedSubset of L -> Subset of L means :Def10: :: LATTICE4:def 10
for p, q being Element of L st p in it & q in it holds
( p "/\" q in it & p "\/" q in it );
existence

proof end;

end;

:: deftheorem Def10 defines ClosedSubset LATTICE4:def 10 :

theorem Th10: :: LATTICE4:10

for L being Lattice holds the carrier of L is ClosedSubset of L

proof end;

registration

let L be Lattice;
cluster non empty ClosedSubset of L;
existence

proof end;

end;

theorem :: LATTICE4:11

for L being Lattice
for F being Filter of L holds F is ClosedSubset of L

proof end;

definition

let L be Lattice;
let B be Finite_Subset of the carrier of L;
canceled;
func FinJoin B -> Element of L equals :: LATTICE4:def 12
FinJoin B,(id L);
coherence ;
func FinMeet B -> Element of L equals :: LATTICE4:def 13
FinMeet B,(id L);
coherence ;

end;

:: deftheorem LATTICE4:def 11 :

:: deftheorem defines FinJoin LATTICE4:def 12 :

:: deftheorem defines FinMeet LATTICE4:def 13 :

theorem :: LATTICE4:12

canceled;

theorem :: LATTICE4:13

canceled;

theorem Th14: :: LATTICE4:14

for L being Lattice
for B being Finite_Subset of the carrier of L holds FinMeet B = the L_meet of L $$ B,(id L) by LATTICE2:def 4;

theorem Th15: :: LATTICE4:15

for L being Lattice
for B being Finite_Subset of the carrier of L holds FinJoin B = the L_join of L $$ B,(id L) by LATTICE2:def 3;

theorem Th16: :: LATTICE4:16

for L being Lattice
for p being Element of L holds FinJoin {p} = p

proof end;

theorem Th17: :: LATTICE4:17

for L being Lattice
for p being Element of L holds FinMeet {p} = p

proof end;

theorem Th18: :: LATTICE4:18

for L2 being Lattice
for DL being distributive Lattice
for f being Homomorphism of DL,L2 st f is epimorphism holds
L2 is distributive

proof end;

theorem Th19: :: LATTICE4:19

for L2 being Lattice
for 0L being lower-bounded Lattice
for f being Homomorphism of 0L,L2 st f is epimorphism holds
( L2 is lower-bounded & f preserves_bottom )

proof end;

theorem Th20: :: LATTICE4:20

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)

proof end;

theorem Th21: :: LATTICE4:21

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

proof end;

theorem :: LATTICE4:22

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)

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 Th23: :: LATTICE4:23

for 0L being lower-bounded Lattice holds FinJoin ({}. the carrier of 0L) = Bottom 0L by Lm1;

theorem Th24: :: LATTICE4:24

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

proof end;

theorem Th25: :: LATTICE4:25

for L2 being Lattice
for 1L being upper-bounded Lattice
for f being Homomorphism of 1L,L2 st f is epimorphism 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 Th26: :: LATTICE4:26

for 1L being upper-bounded Lattice holds FinMeet ({}. the carrier of 1L) = Top 1L by Lm2;

theorem Th27: :: LATTICE4:27

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)

proof end;

theorem Th28: :: LATTICE4:28

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

proof end;

theorem Th29: :: LATTICE4:29

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)

proof end;

theorem Th30: :: LATTICE4:30

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)

proof end;

theorem Th31: :: LATTICE4:31

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

proof end;

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 Th32: :: LATTICE4:32

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)

proof end;

theorem Th33: :: LATTICE4:33

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

proof end;

theorem Th34: :: LATTICE4:34

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 monomorphism & (f . i) "/\" (f . k) [= f . j holds
f . k [= f . (i => j)

proof end;

theorem :: LATTICE4:35

for CL being C_Lattice
for IL being implicative Lattice
for f being Homomorphism of IL,CL st f is isomorphism holds
( CL is implicative & f preserves_implication )

proof end;

theorem Th36: :: LATTICE4:36

for BL being Boolean Lattice holds (Top BL) ` = Bottom BL

proof end;

theorem Th37: :: LATTICE4:37

for BL being Boolean Lattice holds (Bottom BL) ` = Top BL

proof end;

theorem :: LATTICE4:38

for CL being C_Lattice
for BL being Boolean Lattice
for f being Homomorphism of BL,CL st f is epimorphism holds
( CL is Boolean & f preserves_complement )

proof end;

definition

let BL be Boolean Lattice;
mode Field of BL -> non empty Subset of BL means :Def14: :: LATTICE4:def 14
for a, b being Element of BL st a in it & b in it holds
( a "/\" b in it & a ` in it );
existence

proof end;

end;

:: deftheorem Def14 defines Field LATTICE4:def 14 :

theorem Th39: :: LATTICE4:39

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

proof end;

theorem Th40: :: LATTICE4:40

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

proof end;

theorem Th41: :: LATTICE4:41

for BL being Boolean Lattice holds the carrier of BL is Field of BL

proof end;

theorem Th42: :: LATTICE4:42

for BL being Boolean Lattice
for F being Field of BL holds F is ClosedSubset of BL

proof end;

definition

let BL be Boolean Lattice;
let A be non empty Subset of BL;
func field_by A -> Field of BL means :Def15: :: LATTICE4:def 15
( A c= it & ( for F being Field of BL st A c= F holds
it c= F ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines field_by LATTICE4:def 15 :

definition

let BL be Boolean Lattice;
let A be non empty Subset of BL;
func SetImp A -> Subset of BL equals :: LATTICE4:def 16
{ (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;
coherence

proof end;

end;

:: deftheorem defines SetImp LATTICE4:def 16 :

registration

let BL be Boolean Lattice;
let A be non empty Subset of BL;
cluster SetImp A -> non empty ;
coherence

proof end;

end;

theorem :: LATTICE4:43

for x being set
for BL being Boolean Lattice
for A being non empty Subset of BL holds
( x in SetImp A iff ex p, q being Element of BL st
( x = p => q & p in A & q in A ) ) ;

theorem Th44: :: LATTICE4:44

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

proof end;

definition

let BL be Boolean Lattice;
deffunc H₁( Element of BL) -> Element of the carrier of BL = $1 ` ;
func comp BL -> Function of the carrier of BL,the carrier of BL means :Def17: :: LATTICE4:def 17
for a being Element of BL holds it . a = a ` ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines comp LATTICE4:def 17 :

theorem Th45: :: LATTICE4:45

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

proof end;

theorem :: LATTICE4:46

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

proof end;

theorem :: LATTICE4:47

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

proof end;

theorem Th48: :: LATTICE4:48

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

proof end;

theorem Th49: :: LATTICE4:49

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 )

proof end;

theorem :: LATTICE4:50

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

proof end;