:: Homomorphisms of Lattices \\ Finite Join and Finite Meet
:: by Jolanta Kamie\'nska and Jaros\l aw Stanis\l aw Walijewski
::
:: Received July 14, 1993
:: Copyright (c) 1993 Association of Mizar Users
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 ) )
theorem :: LATTICE4:4
theorem :: LATTICE4:5
theorem :: LATTICE4:6
:: deftheorem Def1 defines Homomorphism LATTICE4:def 1 :
theorem Th7: :: LATTICE4:7
theorem Th8: :: LATTICE4:8
theorem Th9: :: LATTICE4:9
:: deftheorem LATTICE4:def 2 :
canceled;
:: deftheorem LATTICE4:def 3 :
canceled;
:: deftheorem LATTICE4:def 4 :
canceled;
:: deftheorem defines are_isomorphic LATTICE4:def 5 :
:: 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 :
:: deftheorem Def10 defines ClosedSubset LATTICE4:def 10 :
theorem Th10: :: LATTICE4:10
theorem :: LATTICE4:11
:: deftheorem LATTICE4:def 11 :
canceled;
:: deftheorem defines FinJoin LATTICE4:def 12 :
:: deftheorem defines FinMeet LATTICE4:def 13 :
theorem :: LATTICE4:12
canceled;
theorem :: LATTICE4:13
canceled;
theorem :: LATTICE4:14
canceled;
theorem :: LATTICE4:15
canceled;
theorem Th16: :: LATTICE4:16
theorem Th17: :: LATTICE4:17
theorem Th18: :: LATTICE4:18
theorem Th19: :: LATTICE4:19
theorem Th20: :: LATTICE4:20
theorem Th21: :: LATTICE4:21
theorem :: LATTICE4:22
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
theorem :: LATTICE4:23
theorem Th24: :: LATTICE4:24
theorem Th25: :: LATTICE4:25
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
theorem :: LATTICE4:26
theorem Th27: :: LATTICE4:27
theorem Th28: :: LATTICE4:28
theorem Th29: :: LATTICE4:29
theorem Th30: :: LATTICE4:30
theorem Th31: :: LATTICE4:31
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)
theorem Th32: :: LATTICE4:32
theorem Th33: :: LATTICE4:33
theorem Th34: :: LATTICE4:34
theorem :: LATTICE4:35
theorem Th36: :: LATTICE4:36
theorem Th37: :: LATTICE4:37
theorem :: LATTICE4:38
:: deftheorem Def14 defines Field LATTICE4:def 14 :
theorem Th39: :: LATTICE4:39
theorem Th40: :: LATTICE4:40
theorem Th41: :: LATTICE4:41
theorem Th42: :: LATTICE4:42
:: deftheorem Def15 defines field_by LATTICE4:def 15 :
:: deftheorem defines SetImp LATTICE4:def 16 :
theorem :: LATTICE4:43
theorem Th44: :: LATTICE4:44
:: deftheorem Def17 defines comp LATTICE4:def 17 :
theorem Th45: :: LATTICE4:45
theorem :: LATTICE4:46
theorem :: LATTICE4:47
theorem Th48: :: LATTICE4:48
theorem Th49: :: LATTICE4:49
theorem :: LATTICE4:50