:: LATTICE4 semantic presentation

theorem Th1: :: LATTICE4:1

canceled;

theorem Th2: :: LATTICE4:2

canceled;

theorem Th3: :: LATTICE4:3

for b₁ being set st b₁ <> {} & ( for b₂ being set st b₂ <> {} & b₂ c= b₁ & b₂ is c=-linear holds
ex b₃ being set st
( b₃ in b₁ & ( for b₄ being set st b₄ in b₂ holds
b₄ c= b₃ ) ) ) holds
ex b₂ being set st
( b₂ in b₁ & ( for b₃ being set st b₃ in b₁ & b₃ <> b₂ holds
not b₂ c= b₃ ) )

proof end;

theorem Th4: :: LATTICE4:4

for b₁ being Lattice holds <.b₁.) is prime

proof end;

theorem Th5: :: LATTICE4:5

for b₁ being Lattice
for b₂, b₃ being Filter of b₁ holds
( b₂ c= <.(b₂ \/ b₃).) & b₃ c= <.(b₂ \/ b₃).) )

proof end;

theorem Th6: :: LATTICE4:6

for b₁ being Lattice
for b₂ being Filter of b₁
for b₃, b₄ being Element of b₁ st b₃ in <.(<.b₄.) \/ b₂).) holds
ex b₅ being Element of b₁ st
( b₅ in b₂ & b₄ "/\" b₅ [= b₃ )

proof end;

definition

let c₁, c₂ be Lattice;
mode Homomorphism of c₁,c₂ -> Function of the carrier of a₁,the carrier of a₂ means :Def1: :: LATTICE4:def 1
for b₁, b₂ being Element of a₁ holds
( a₃ . (b₁ "\/" b₂) = (a₃ . b₁) "\/" (a₃ . b₂) & a₃ . (b₁ "/\" b₂) = (a₃ . b₁) "/\" (a₃ . b₂) );
existence

proof end;

end;

:: deftheorem Def1 defines Homomorphism LATTICE4:def 1 :

theorem Th7: :: LATTICE4:7

for b₁, b₂ being Lattice
for b₃, b₄ being Element of b₁
for b₅ being Homomorphism of b₁,b₂ st b₃ [= b₄ holds
b₅ . b₃ [= b₅ . b₄

proof end;

definition

let c₁, c₂ be Lattice;
let c₃ be Function of the carrier of c₁,the carrier of c₂;
attr a₃ is monomorphism means :Def2: :: LATTICE4:def 2
a₃ is one-to-one;
attr a₃ is epimorphism means :Def3: :: LATTICE4:def 3
rng a₃ = the carrier of a₂;

end;

:: deftheorem Def2 defines monomorphism LATTICE4:def 2 :

:: deftheorem Def3 defines epimorphism LATTICE4:def 3 :

theorem Th8: :: LATTICE4:8

for b₁, b₂ being Lattice
for b₃, b₄ being Element of b₁
for b₅ being Homomorphism of b₁,b₂ st b₅ is monomorphism holds
( b₃ [= b₄ iff b₅ . b₃ [= b₅ . b₄ )

proof end;

theorem Th9: :: LATTICE4:9

for b₁, b₂ being Lattice
for b₃ being Function of the carrier of b₁,the carrier of b₂ st b₃ is epimorphism holds
for b₄ being Element of b₂ ex b₅ being Element of b₁ st b₄ = b₃ . b₅

proof end;

definition

let c₁, c₂ be Lattice;
let c₃ be Homomorphism of c₁,c₂;
attr a₃ is isomorphism means :Def4: :: LATTICE4:def 4
( a₃ is monomorphism & a₃ is epimorphism );

end;

:: deftheorem Def4 defines isomorphism LATTICE4:def 4 :

definition

let c₁, c₂ be Lattice;
redefine pred c₁,c₂ are_isomorphic means :: LATTICE4:def 5
ex b₁ being Homomorphism of a₁,a₂ st b₁ is isomorphism;
compatibility

proof end;

end;

:: deftheorem Def5 defines are_isomorphic LATTICE4:def 5 :

definition

let c₁, c₂ be Lattice;
let c₃ be Homomorphism of c₁,c₂;
pred c₃ preserves_implication means :Def6: :: LATTICE4:def 6
for b₁, b₂ being Element of a₁ holds a₃ . (b₁ => b₂) = (a₃ . b₁) => (a₃ . b₂);
pred c₃ preserves_top means :Def7: :: LATTICE4:def 7
a₃ . (Top a₁) = Top a₂;
pred c₃ preserves_bottom means :Def8: :: LATTICE4:def 8
a₃ . (Bottom a₁) = Bottom a₂;
pred c₃ preserves_complement means :Def9: :: LATTICE4:def 9
for b₁ being Element of a₁ holds a₃ . (b₁ ` ) = (a₃ . b₁) ` ;

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 c₁ be Lattice;
mode ClosedSubset of c₁ -> Subset of a₁ means :Def10: :: LATTICE4:def 10
for b₁, b₂ being Element of a₁ st b₁ in a₂ & b₂ in a₂ holds
( b₁ "/\" b₂ in a₂ & b₁ "\/" b₂ in a₂ );
existence

proof end;

end;

:: deftheorem Def10 defines ClosedSubset LATTICE4:def 10 :

theorem Th10: :: LATTICE4:10

for b₁ being Lattice holds the carrier of b₁ is ClosedSubset of b₁

proof end;

registration

let c₁ be Lattice;
cluster non empty ClosedSubset of a₁;
existence

proof end;

end;

theorem Th11: :: LATTICE4:11

for b₁ being Lattice
for b₂ being Filter of b₁ holds b₂ is ClosedSubset of b₁

proof end;

definition

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

end;

:: deftheorem Def11 LATTICE4:def 11 :

:: deftheorem Def12 defines FinJoin LATTICE4:def 12 :

:: deftheorem Def13 defines FinMeet LATTICE4:def 13 :

theorem Th12: :: LATTICE4:12

canceled;

theorem Th13: :: LATTICE4:13

canceled;

theorem Th14: :: LATTICE4:14

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

theorem Th15: :: LATTICE4:15

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

theorem Th16: :: LATTICE4:16

for b₁ being Lattice
for b₂ being Element of b₁ holds FinJoin {b₂} = b₂

proof end;

theorem Th17: :: LATTICE4:17

for b₁ being Lattice
for b₂ being Element of b₁ holds FinMeet {b₂} = b₂

proof end;

theorem Th18: :: LATTICE4:18

for b₁ being Lattice
for b₂ being distributive Lattice
for b₃ being Homomorphism of b₂,b₁ st b₃ is epimorphism holds
b₁ is distributive

proof end;

theorem Th19: :: LATTICE4:19

for b₁ being Lattice
for b₂ being lower-bounded Lattice
for b₃ being Homomorphism of b₂,b₁ st b₃ is epimorphism holds
( b₁ is lower-bounded & b₃ preserves_bottom )

proof end;

theorem Th20: :: LATTICE4:20

for b₁ being lower-bounded Lattice
for b₂ being Finite_Subset of the carrier of b₁
for b₃ being Element of b₁
for b₄ being UnOp of the carrier of b₁ holds FinJoin (b₂ \/ {b₃}),b₄ = (FinJoin b₂,b₄) "\/" (b₄ . b₃)

proof end;

theorem Th21: :: LATTICE4:21

for b₁ being lower-bounded Lattice
for b₂ being Finite_Subset of the carrier of b₁
for b₃ being Element of b₁ holds FinJoin (b₂ \/ {b₃}) = (FinJoin b₂) "\/" b₃

proof end;

theorem Th22: :: LATTICE4:22

for b₁ being lower-bounded Lattice
for b₂, b₃ being Finite_Subset of the carrier of b₁ holds (FinJoin b₂) "\/" (FinJoin b₃) = FinJoin (b₂ \/ b₃)

proof end;

Lemma22: for b₁ being lower-bounded Lattice
for b₂ being Function of the carrier of b₁,the carrier of b₁ holds FinJoin ({}. the carrier of b₁),b₂ = Bottom b₁

proof end;

theorem Th23: :: LATTICE4:23

for b₁ being lower-bounded Lattice holds FinJoin ({}. the carrier of b₁) = Bottom b₁ by Lemma22;

theorem Th24: :: LATTICE4:24

for b₁ being lower-bounded Lattice
for b₂ being ClosedSubset of b₁ st Bottom b₁ in b₂ holds
for b₃ being Finite_Subset of the carrier of b₁ st b₃ c= b₂ holds
FinJoin b₃ in b₂

proof end;

theorem Th25: :: LATTICE4:25

for b₁ being Lattice
for b₂ being upper-bounded Lattice
for b₃ being Homomorphism of b₂,b₁ st b₃ is epimorphism holds
( b₁ is upper-bounded & b₃ preserves_top )

proof end;

Lemma26: for b₁ being upper-bounded Lattice
for b₂ being Function of the carrier of b₁,the carrier of b₁ holds FinMeet ({}. the carrier of b₁),b₂ = Top b₁

proof end;

theorem Th26: :: LATTICE4:26

for b₁ being upper-bounded Lattice holds FinMeet ({}. the carrier of b₁) = Top b₁ by Lemma26;

theorem Th27: :: LATTICE4:27

for b₁ being upper-bounded Lattice
for b₂ being Finite_Subset of the carrier of b₁
for b₃ being Element of b₁
for b₄ being UnOp of the carrier of b₁ holds FinMeet (b₂ \/ {b₃}),b₄ = (FinMeet b₂,b₄) "/\" (b₄ . b₃)

proof end;

theorem Th28: :: LATTICE4:28

for b₁ being upper-bounded Lattice
for b₂ being Finite_Subset of the carrier of b₁
for b₃ being Element of b₁ holds FinMeet (b₂ \/ {b₃}) = (FinMeet b₂) "/\" b₃

proof end;

theorem Th29: :: LATTICE4:29

for b₁ being upper-bounded Lattice
for b₂ being Finite_Subset of the carrier of b₁
for b₃, b₄ being UnOp of the carrier of b₁ holds FinMeet (b₃ .: b₂),b₄ = FinMeet b₂,(b₄ * b₃)

proof end;

theorem Th30: :: LATTICE4:30

for b₁ being upper-bounded Lattice
for b₂, b₃ being Finite_Subset of the carrier of b₁ holds (FinMeet b₂) "/\" (FinMeet b₃) = FinMeet (b₂ \/ b₃)

proof end;

theorem Th31: :: LATTICE4:31

for b₁ being upper-bounded Lattice
for b₂ being ClosedSubset of b₁ st Top b₁ in b₂ holds
for b₃ being Finite_Subset of the carrier of b₁ st b₃ c= b₂ holds
FinMeet b₃ in b₂

proof end;

Lemma33: for b₁ being distributive upper-bounded Lattice
for b₂ being Finite_Subset of the carrier of b₁
for b₃ being Element of b₁
for b₄ being UnOp of the carrier of b₁ holds the L_join of b₁ . (the L_meet of b₁ $$ b₂,b₄),b₃ = the L_meet of b₁ $$ b₂,(the L_join of b₁ [:] b₄,b₃)

proof end;

theorem Th32: :: LATTICE4:32

for b₁ being distributive upper-bounded Lattice
for b₂ being Finite_Subset of the carrier of b₁
for b₃ being Element of b₁ holds (FinMeet b₂) "\/" b₃ = FinMeet ((the L_join of b₁ [:] (id b₁),b₃) .: b₂)

proof end;

theorem Th33: :: LATTICE4:33

for b₁ being C_Lattice
for b₂ being implicative Lattice
for b₃ being Homomorphism of b₂,b₁
for b₄, b₅ being Element of b₂ holds (b₃ . b₄) "/\" (b₃ . (b₄ => b₅)) [= b₃ . b₅

proof end;

theorem Th34: :: LATTICE4:34

for b₁ being C_Lattice
for b₂ being implicative Lattice
for b₃ being Homomorphism of b₂,b₁
for b₄, b₅, b₆ being Element of b₂ st b₃ is monomorphism & (b₃ . b₄) "/\" (b₃ . b₅) [= b₃ . b₆ holds
b₃ . b₅ [= b₃ . (b₄ => b₆)

proof end;

theorem Th35: :: LATTICE4:35

for b₁ being C_Lattice
for b₂ being implicative Lattice
for b₃ being Homomorphism of b₂,b₁ st b₃ is isomorphism holds
( b₁ is implicative & b₃ preserves_implication )

proof end;

theorem Th36: :: LATTICE4:36

for b₁ being Boolean Lattice holds (Top b₁) ` = Bottom b₁

proof end;

theorem Th37: :: LATTICE4:37

for b₁ being Boolean Lattice holds (Bottom b₁) ` = Top b₁

proof end;

theorem Th38: :: LATTICE4:38

for b₁ being C_Lattice
for b₂ being Boolean Lattice
for b₃ being Homomorphism of b₂,b₁ st b₃ is epimorphism holds
( b₁ is Boolean & b₃ preserves_complement )

proof end;

definition

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

proof end;

end;

:: deftheorem Def14 defines Field LATTICE4:def 14 :

theorem Th39: :: LATTICE4:39

for b₁ being Boolean Lattice
for b₂, b₃ being Element of b₁
for b₄ being Field of b₁ st b₂ in b₄ & b₃ in b₄ holds
b₂ "\/" b₃ in b₄

proof end;

theorem Th40: :: LATTICE4:40

for b₁ being Boolean Lattice
for b₂, b₃ being Element of b₁
for b₄ being Field of b₁ st b₂ in b₄ & b₃ in b₄ holds
b₂ => b₃ in b₄

proof end;

theorem Th41: :: LATTICE4:41

for b₁ being Boolean Lattice holds the carrier of b₁ is Field of b₁

proof end;

theorem Th42: :: LATTICE4:42

for b₁ being Boolean Lattice
for b₂ being Field of b₁ holds b₂ is ClosedSubset of b₁

proof end;

definition

let c₁ be Boolean Lattice;
let c₂ be non empty Subset of c₁;
func field_by c₂ -> Field of a₁ means :Def15: :: LATTICE4:def 15
( a₂ c= a₃ & ( for b₁ being Field of a₁ st a₂ c= b₁ holds
a₃ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines field_by LATTICE4:def 15 :

definition

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

proof end;

end;

:: deftheorem Def16 defines SetImp LATTICE4:def 16 :

registration

let c₁ be Boolean Lattice;
let c₂ be non empty Subset of c₁;
cluster SetImp a₂ -> non empty ;
coherence

proof end;

end;

theorem Th43: :: LATTICE4:43

for b₁ being set
for b₂ being Boolean Lattice
for b₃ being non empty Subset of b₂ holds
( b₁ in SetImp b₃ iff ex b₄, b₅ being Element of b₂ st
( b₁ = b₄ => b₅ & b₄ in b₃ & b₅ in b₃ ) ) ;

theorem Th44: :: LATTICE4:44

for b₁ being Boolean Lattice
for b₂ being non empty Subset of b₁
for b₃ being Element of b₁ holds
( b₃ in SetImp b₂ iff ex b₄, b₅ being Element of b₁ st
( b₃ = (b₄ ` ) "\/" b₅ & b₄ in b₂ & b₅ in b₂ ) )

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines comp LATTICE4:def 17 :

theorem Th45: :: LATTICE4:45

for b₁ being Boolean Lattice
for b₂ being Element of b₁
for b₃ being Finite_Subset of the carrier of b₁ holds FinJoin (b₃ \/ {b₂}),(comp b₁) = (FinJoin b₃,(comp b₁)) "\/" (b₂ ` )

proof end;

theorem Th46: :: LATTICE4:46

for b₁ being Boolean Lattice
for b₂ being Finite_Subset of the carrier of b₁ holds (FinJoin b₂) ` = FinMeet b₂,(comp b₁)

proof end;

theorem Th47: :: LATTICE4:47

for b₁ being Boolean Lattice
for b₂ being Element of b₁
for b₃ being Finite_Subset of the carrier of b₁ holds FinMeet (b₃ \/ {b₂}),(comp b₁) = (FinMeet b₃,(comp b₁)) "/\" (b₂ ` )

proof end;

theorem Th48: :: LATTICE4:48

for b₁ being Boolean Lattice
for b₂ being Finite_Subset of the carrier of b₁ holds (FinMeet b₂) ` = FinJoin b₂,(comp b₁)

proof end;

theorem Th49: :: LATTICE4:49

for b₁ being Boolean Lattice
for b₂ being non empty ClosedSubset of b₁ st Bottom b₁ in b₂ & Top b₁ in b₂ holds
for b₃ being Finite_Subset of the carrier of b₁ st b₃ c= SetImp b₂ holds
ex b₄ being Finite_Subset of the carrier of b₁ st
( b₄ c= SetImp b₂ & FinJoin b₃,(comp b₁) = FinMeet b₄ )

proof end;

theorem Th50: :: LATTICE4:50

for b₁ being Boolean Lattice
for b₂ being non empty ClosedSubset of b₁ st Bottom b₁ in b₂ & Top b₁ in b₂ holds
{ (FinMeet b₃) where B is Finite_Subset of the carrier of b₁ : b₃ c= SetImp b₂ } = field_by b₂

proof end;