:: Introduction to Lattice Theory
:: by Stanis{\l}aw \.Zukowski
::
:: Received April 14, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, BINOP_1, XBOOLE_0, ZFMISC_1, SUBSET_1, EQREL_1,
FUNCT_1, PBOOLE, XXREAL_2, CAT_1, LATTICES, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, CARD_1, STRUCT_0, BINOP_1;
constructors BINOP_1, STRUCT_0;
registrations XBOOLE_0, SUBSET_1, CARD_1, STRUCT_0;
requirements SUBSET, BOOLE;
equalities STRUCT_0;
expansions STRUCT_0;
theorems ZFMISC_1, SUBSET_1;
begin
definition
struct(1-sorted) /\-SemiLattStr (# carrier -> set, L_meet -> BinOp of the
carrier #);
end;
definition
struct (1-sorted) \/-SemiLattStr (# carrier -> set, L_join -> BinOp of the
carrier #);
end;
definition
struct (/\-SemiLattStr,\/-SemiLattStr) LattStr (# carrier -> set, L_join,
L_meet -> BinOp of the carrier #);
end;
registration
let D be non empty set, u be BinOp of D;
cluster \/-SemiLattStr (# D, u #) -> non empty;
coherence;
cluster /\-SemiLattStr (# D, u #) -> non empty;
coherence;
end;
registration
let D be non empty set, u,n be BinOp of D;
cluster LattStr (# D, u, n #) -> non empty;
coherence;
end;
registration
cluster 1-element strict for \/-SemiLattStr;
existence
proof
set u = the BinOp of bool {};
take L = \/-SemiLattStr (# bool {}, u #);
thus thesis by ZFMISC_1:1;
end;
cluster 1-element strict for /\-SemiLattStr;
existence
proof
set u = the BinOp of bool {};
take L = /\-SemiLattStr (# bool {}, u #);
thus thesis by ZFMISC_1:1;
end;
cluster 1-element strict for LattStr;
existence
proof
set u = the BinOp of bool {};
take L = LattStr (# bool {}, u, u #);
thus thesis by ZFMISC_1:1;
end;
end;
definition
let G be non empty \/-SemiLattStr, p, q be Element of G;
func p"\/"q -> Element of G equals
(the L_join of G).(p,q);
coherence;
end;
definition
let G be non empty /\-SemiLattStr, p, q be Element of G;
func p"/\"q -> Element of G equals
(the L_meet of G).(p,q);
coherence;
end;
definition
let G be non empty \/-SemiLattStr, p, q be Element of G;
pred p [= q means
:Def3:
p"\/"q = q;
end;
Lm1: for uu,nn being BinOp of bool {}, x,y being Element of LattStr(#bool {},
uu,nn#) holds x = y
proof
let uu,nn be BinOp of bool {}, x,y be Element of LattStr(#bool {},uu,nn#);
x = {};
hence thesis;
end;
Lm2: for n being BinOp of bool {}, x,y being Element of \/-SemiLattStr (#bool
{}, n#) holds x = y
proof
let n be BinOp of bool {};
let x,y be Element of \/-SemiLattStr (#bool {}, n#);
x = {};
hence thesis;
end;
Lm3: for n being BinOp of bool {}, x,y being Element of /\-SemiLattStr (#bool
{}, n#) holds x = y
proof
let n be BinOp of bool {};
let x,y be Element of /\-SemiLattStr (#bool {}, n#);
x = {};
hence thesis;
end;
definition
let IT be non empty \/-SemiLattStr;
attr IT is join-commutative means
:Def4:
for a,b being Element of IT holds a "\/"b = b"\/"a;
attr IT is join-associative means
:Def5:
for a,b,c being Element of IT holds a"\/"(b"\/"c) = (a"\/"b)"\/"c;
end;
definition
let IT be non empty /\-SemiLattStr;
attr IT is meet-commutative means
:Def6:
for a,b being Element of IT holds a "/\"b = b"/\"a;
attr IT is meet-associative means
:Def7:
for a,b,c being Element of IT holds a"/\"(b"/\"c) = (a"/\"b)"/\"c;
end;
definition
let IT be non empty LattStr;
attr IT is meet-absorbing means
:Def8:
for a,b being Element of IT holds (a "/\"b)"\/"b = b;
attr IT is join-absorbing means
:Def9:
for a,b being Element of IT holds a "/\"(a"\/"b)=a;
end;
definition
let IT be non empty LattStr;
attr IT is Lattice-like means
IT is join-commutative
join-associative meet-absorbing meet-commutative meet-associative
join-absorbing;
end;
registration
cluster Lattice-like -> join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing for non empty LattStr;
coherence;
cluster join-commutative join-associative meet-absorbing meet-commutative
meet-associative join-absorbing -> Lattice-like for non empty LattStr;
coherence;
end;
registration
cluster strict join-commutative join-associative for
non empty \/-SemiLattStr;
existence
proof
set u = the BinOp of bool {};
take GGj = \/-SemiLattStr(#bool {},u#);
( for x,y being Element of GGj holds x"\/"y = y"\/"x)& for x,y,z being
Element of GGj holds x"\/"(y"\/"z) = (x"\/"y)"\/"z by Lm2;
hence thesis;
end;
cluster strict meet-commutative meet-associative for
non empty /\-SemiLattStr;
existence
proof
set u = the BinOp of bool {};
take GGm = /\-SemiLattStr(#bool {},u#);
( for x,y being Element of GGm holds x"/\"y = y"/\"x)& for x,y,z being
Element of GGm holds x"/\"(y"/\"z) = (x"/\"y)"/\"z by Lm3;
hence thesis;
end;
cluster strict Lattice-like for non empty LattStr;
existence
proof
set u = the BinOp of bool {};
take GG = LattStr(#bool {},u,u#);
A1: ( for x,y being Element of GG holds (x"/\"y)"\/"y = y)& for x,y being
Element of GG holds x"/\"y = y"/\"x by Lm1;
A2: ( for x,y,z being Element of GG holds x"/\"(y"/\"z) = (x"/\"y)"/\"z)&
for x,y being Element of GG holds x"/\"(x"\/"y) = x by Lm1;
( for x,y being Element of GG holds x"\/"y = y"\/"x)& for x,y,z being
Element of GG holds x"\/"(y"\/"z) = (x"\/"y)"\/"z by Lm1;
then GG is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing by A1,A2;
hence thesis;
end;
end;
definition
mode Lattice is Lattice-like non empty LattStr;
end;
definition
let L be join-commutative non empty \/-SemiLattStr, a, b be Element of L;
redefine func a"\/"b; :: redefines "\/" (LATTICES, definition)
commutativity by Def4;
end;
definition
let L be meet-commutative non empty /\-SemiLattStr, a, b be Element of L;
redefine func a"/\"b; :: redefines "/\" (LATTICES, definition)
commutativity by Def6;
end;
definition
let IT be non empty LattStr;
attr IT is distributive means
:Def11:
for a,b,c being Element of IT holds a "/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c);
end;
definition
let IT be non empty LattStr;
attr IT is modular means
for a,b,c being Element of IT st a [= c holds a"\/"(b"/\"c) = (a"\/"b)"/\"c;
end;
definition
let IT be non empty /\-SemiLattStr;
attr IT is lower-bounded means
:Def13:
ex c being Element of IT st for a
being Element of IT holds c"/\"a = c & a"/\"c = c;
end;
definition
let IT be non empty \/-SemiLattStr;
attr IT is upper-bounded means
:Def14:
ex c being Element of IT st for a
being Element of IT holds c"\/"a = c & a"\/"c = c;
end;
Lm4: for n,u being BinOp of bool {} holds LattStr (#bool {},n,u#) is Lattice
proof
let n,u be BinOp of bool {};
set G = LattStr (#bool {},n,u#);
for x,y,z being Element of G holds x"\/"(y"\/"z) = (x"\/"y)"\/"z by Lm1;
then
A1: G is join-associative;
for x,y being Element of G holds (x"/\"y)"\/"y = y by Lm1;
then
A2: G is meet-absorbing;
for x,y being Element of G holds x"/\"(x"\/"y) = x by Lm1;
then
A3: G is join-absorbing;
for x,y,z being Element of G holds x"/\"(y"/\"z) = (x"/\"y)"/\"z by Lm1;
then
A4: G is meet-associative;
for x,y being Element of G holds x"/\"y = y"/\"x by Lm1;
then
A5: G is meet-commutative;
for x,y being Element of G holds x"\/"y = y"\/"x by Lm1;
then G is join-commutative;
hence thesis by A1,A2,A5,A4,A3;
end;
registration
cluster strict distributive lower-bounded upper-bounded modular for Lattice;
existence
proof
set uu = the BinOp of bool {};
set GG=LattStr(#bool {},uu,uu#);
reconsider GG as Lattice by Lm4;
reconsider 0GG={}, D = {} as Element of GG by ZFMISC_1:def 1;
for x being Element of GG holds 0GG"/\"x = 0GG & x"/\"0GG = 0GG;
then
A1: GG is lower-bounded;
for x being Element of GG holds D"\/"x = D & x"\/"D = D;
then
A2: GG is upper-bounded;
for x,y,z being Element of GG holds x"/\"(y"\/"z) = (x"/\"y)"\/"(x"/\"
z) by Lm1;
then
A3: GG is distributive;
for x,y,z being Element of GG holds x [= z implies x"\/"(y"/\"z) = (x
"\/"y)"/\"z by Lm1;
then GG is modular;
hence thesis by A1,A3,A2;
end;
end;
definition
mode D_Lattice is distributive Lattice;
mode M_Lattice is modular Lattice;
mode 0_Lattice is lower-bounded Lattice;
mode 1_Lattice is upper-bounded Lattice;
end;
Lm5: for n,u being BinOp of bool {} holds LattStr (#bool {},n,u#) is 0_Lattice
proof
let n,u be BinOp of bool {};
set G = LattStr (#bool {},n,u#);
reconsider G as Lattice by Lm4;
reconsider D={} as Element of G by ZFMISC_1:def 1;
for x being Element of G holds D"/\"x = D & x"/\"D = D;
hence thesis by Def13;
end;
Lm6: for n,u being BinOp of bool {} holds LattStr (#bool {},n,u#) is 1_Lattice
proof
let n,u be BinOp of bool {};
set G = LattStr (#bool {},n,u#);
reconsider G as Lattice by Lm4;
reconsider D={} as Element of G by ZFMISC_1:def 1;
for x being Element of G holds D"\/"x = D & x"\/"D = D;
hence thesis by Def14;
end;
definition
let IT be non empty LattStr;
attr IT is bounded means
IT is lower-bounded upper-bounded;
end;
registration
cluster lower-bounded upper-bounded -> bounded for non empty LattStr;
coherence;
cluster bounded -> lower-bounded upper-bounded for non empty LattStr;
coherence;
end;
registration
cluster bounded strict for Lattice;
existence
proof
set uu = the BinOp of bool {};
set G=LattStr(#bool {},uu,uu#);
reconsider G as Lattice by Lm4;
G is 0_Lattice & G is 1_Lattice by Lm5,Lm6;
hence thesis;
end;
end;
definition
mode 01_Lattice is bounded Lattice;
end;
definition
let L be non empty /\-SemiLattStr;
assume
A1: L is lower-bounded;
func Bottom L -> Element of L means
:Def16:
for a being Element of L holds it "/\" a = it & a "/\" it = it;
existence by A1;
uniqueness
proof
let c1,c2 be Element of L such that
A2: for a being Element of L holds c1"/\"a = c1 & a"/\"c1 = c1 and
A3: for a being Element of L holds c2"/\"a = c2 & a"/\"c2 = c2;
thus c1 = c2"/\"c1 by A2
.= c2 by A3;
end;
end;
definition
let L be non empty \/-SemiLattStr;
assume
A1: L is upper-bounded;
func Top L -> Element of L means
:Def17:
for a being Element of L holds it "\/" a = it & a "\/" it = it;
existence by A1;
uniqueness
proof
let c1,c2 be Element of L such that
A2: for a being Element of L holds c1"\/"a = c1 & a"\/"c1 = c1 and
A3: for a being Element of L holds c2"\/"a = c2 & a"\/"c2 = c2;
thus c1 = c2"\/"c1 by A2
.= c2 by A3;
end;
end;
definition
let L be non empty LattStr, a, b be Element of L;
pred a is_a_complement_of b means
a"\/"b = Top L & b"\/"a = Top L & a"/\"b = Bottom L & b"/\"a = Bottom L;
end;
definition
let IT be non empty LattStr;
attr IT is complemented means
:Def19:
for b being Element of IT ex a being Element of IT st a is_a_complement_of b;
end;
registration
cluster bounded complemented strict for Lattice;
existence
proof
set n = the BinOp of bool {};
reconsider GG = LattStr (#bool {},n,n#) as strict Lattice by Lm4;
take GG;
GG is 0_Lattice & GG is 1_Lattice by Lm5,Lm6;
hence GG is bounded;
thus GG is complemented
proof
set a = the Element of GG;
let b be Element of GG;
take a;
thus a"\/"b = Top GG & b"\/"a = Top GG by Lm1;
thus a"/\"b = Bottom GG & b"/\"a = Bottom GG by Lm1;
end;
thus thesis;
end;
end;
definition
mode C_Lattice is complemented 01_Lattice;
end;
definition
let IT be non empty LattStr;
attr IT is Boolean means
IT is bounded complemented distributive;
end;
registration
cluster Boolean -> bounded complemented distributive for non empty LattStr;
coherence;
cluster bounded complemented distributive -> Boolean for non empty LattStr;
coherence;
end;
registration
cluster Boolean strict for Lattice;
existence
proof
set n = the BinOp of bool {};
reconsider G = LattStr (#bool {},n,n#) as strict Lattice by Lm4;
A1: G is complemented
proof
let b be Element of G;
take b;
thus b"\/"b = Top G & b"\/"b = Top G by Lm1;
thus b"/\"b = Bottom G & b"/\"b = Bottom G by Lm1;
end;
G is 0_Lattice & G is 1_Lattice by Lm5,Lm6;
then reconsider G as C_Lattice by A1;
for x,y,z being Element of G holds x"/\"(y"\/"z) = (x"/\"y)"\/"(x"/\"z
) by Lm1;
then G is distributive;
hence thesis;
end;
end;
definition
mode B_Lattice is Boolean Lattice;
end;
registration
let L be meet-absorbing join-absorbing meet-commutative non empty LattStr,
a be Element of L;
reduce a "\/" a to a;
reducibility
proof
thus a"\/"a = ( a "/\" ( a"\/"a ) ) "\/" a by Def9
.= a by Def8;
end;
end;
registration
let L be meet-absorbing join-absorbing meet-commutative non empty LattStr,
a be Element of L;
reduce a "/\" a to a;
reducibility
proof
a"/\"( a"\/"a ) = a by Def9;
hence thesis;
end;
end;
::$CT 2
theorem Th1:
for L being Lattice holds (for a,b,c being Element of L holds a
"/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c)) iff for a,b,c being Element of L holds a
"\/"(b"/\"c) = (a"\/"b)"/\"(a"\/"c)
proof
let L be Lattice;
hereby
assume
A1: for a,b,c be Element of L holds a"/\"(b"\/"c)=(a"/\"b)"\/"(a"/\"c);
let a,b,c be Element of L;
thus a"\/"(b"/\"c)=(a"\/"(c"/\"a))"\/"(c"/\"b) by Def8
.=a"\/"((c"/\"a)"\/"(c"/\"b)) by Def5
.=a"\/"((a"\/"b)"/\"c) by A1
.=((a"\/"b)"/\"a)"\/"((a"\/"b)"/\"c) by Def9
.=(a"\/"b)"/\"(a"\/"c) by A1;
end;
assume
A2: for a,b,c be Element of L holds a"\/"(b"/\"c)=(a"\/"b)"/\"(a"\/"c);
let a,b,c be Element of L;
thus a"/\"(b"\/"c)=(a"/\"(c"\/"a))"/\"(c"\/"b) by Def9
.=a"/\"((c"\/"a)"/\"(c"\/"b)) by Def7
.=a"/\"((a"/\"b)"\/"c) by A2
.=((a"/\"b)"\/"a)"/\"((a"/\"b)"\/"c) by Def8
.=(a"/\"b)"\/"(a"/\"c) by A2;
end;
theorem Th2:
for L being meet-absorbing join-absorbing non empty LattStr,
a, b being Element of L holds a [= b iff a"/\"b = a by Def8,Def9;
theorem Th3:
for L being meet-absorbing join-absorbing join-associative
meet-commutative non empty LattStr, a, b being Element of L holds a [= a"\/"b
proof
let L be meet-absorbing join-absorbing join-associative
meet-commutative
non empty LattStr, a, b be Element of L;
thus a"\/"( a"\/"b) = (a"\/"a)"\/"b by Def5
.= a"\/"b;
end;
theorem Th4:
for L being meet-absorbing meet-commutative non empty LattStr,
a, b being Element of L holds a"/\"b [= a by Def8;
definition
let L be meet-absorbing join-absorbing meet-commutative non empty LattStr,
a, b be Element of L;
redefine pred a [= b; :: redefines [= (LATTICES, definition)
reflexivity;
end;
theorem
for L being join-associative non empty \/-SemiLattStr, a, b, c being
Element of L holds a [= b & b [= c implies a [= c
by Def5;
theorem Th6:
for L being join-commutative non empty \/-SemiLattStr, a, b
being Element of L holds a [= b & b [= a implies a=b
proof
let L be join-commutative non empty \/-SemiLattStr, a, b be Element of L;
assume a"\/"b = b & b"\/"a =a;
hence thesis;
end;
theorem Th7:
for L being meet-absorbing join-absorbing meet-associative non
empty LattStr, a, b, c being Element of L holds a [= b implies a"/\"c [= b"/\"
c
proof
let L be meet-absorbing join-absorbing meet-associative non empty LattStr,
a, b, c be Element of L;
assume a [= b;
hence (a"/\"c)"\/"(b"/\"c) = ((a"/\"b)"/\"c)"\/"(b"/\"c) by Th2
.= (a"/\"(b"/\"c))"\/"(b"/\"c) by Def7
.= b"/\"c by Def8;
end;
theorem
for L being Lattice holds (for a,b,c being Element of L holds (a"/\"b)
"\/"(b"/\"c)"\/"(c"/\"a) = (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a)) implies L is
distributive
proof
let L be Lattice;
assume
A1: for a,b,c being Element of L holds (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a)
= (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a);
A2: now
let a,b,c be Element of L;
assume
A3: c [= a;
thus a"/\"(b"\/"c) = (b"\/"c)"/\"(a"/\"(a"\/"b)) by Def9
.= (a"\/"b)"/\"((b"\/"c)"/\"a) by Def7
.= (a"\/"b)"/\"((b"\/"c)"/\"(c"\/"a)) by A3
.= (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a) by Def7
.= (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a) by A1
.= (a"/\"b)"\/"((b"/\"c)"\/"(c"/\"a)) by Def5
.= (a"/\"b)"\/"((b"/\"c)"\/"c) by A3,Th2
.= (a"/\"b)"\/"c by Def8;
end;
let a,b,c be Element of L;
A4: ((a"/\"b)"\/"(c"/\"a))"\/"a = (a"/\"b)"\/"((c"/\"a)"\/"a) by Def5
.= (a"/\"b)"\/"a by Def8
.= a by Def8;
thus a"/\"(b"\/"c) = (a"/\"(c"\/"a))"/\"(b"\/"c) by Def9
.= a"/\"((c"\/"a)"/\"(b"\/"c)) by Def7
.= (a"/\"(a"\/"b))"/\"((c"\/"a)"/\"(b"\/"c)) by Def9
.= a"/\"((a"\/"b)"/\"((b"\/"c)"/\"(c"\/"a))) by Def7
.= a"/\"((a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a)) by Def7
.= a"/\"((b"/\"c)"\/"(a"/\"b)"\/"(c"/\"a)) by A1
.= a"/\"((b"/\"c)"\/"((a"/\"b)"\/"(c"/\"a))) by Def5
.= (a"/\"(b"/\"c))"\/"((a"/\"b)"\/"(c"/\"a)) by A2,A4,Def3
.= (a"/\"b"/\"c)"\/"((a"/\"b)"\/"(c"/\"a)) by Def7
.= ((a"/\"b"/\"c)"\/"(a"/\"b))"\/"(c"/\"a) by Def5
.= (a"/\"b)"\/"(a"/\"c) by Def8;
end;
reserve L for D_Lattice;
reserve a, b, c for Element of L;
theorem Th9:
a"\/"(b"/\"c) = (a"\/"b)"/\"(a"\/"c)
proof
for a,b,c holds a"/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c) by Def11;
hence thesis by Th1;
end;
theorem Th10:
c"/\"a = c"/\"b & c"\/"a = c"\/"b implies a=b
proof
assume that
A1: c"/\"a = c"/\"b and
A2: c"\/"a = c"\/"b;
thus a = a"/\"( c"\/"a ) by Def9
.= ( b"/\"c )"\/"( b"/\"a ) by A1,A2,Def11
.= b"/\"( c"\/"a ) by Def11
.= b by A2,Def9;
end;
theorem
(a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a) = (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a)
proof
thus (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a) = (((a"\/"b)"/\"(b"\/"c))"/\"c)"\/"(((
a"\/"b)"/\"(b"\/"c))"/\"a) by Def11
.= ((a"\/"b)"/\"((b"\/"c)"/\"c))"\/"(((a"\/"b)"/\"(b"\/"c))"/\"a) by Def7
.= ((a"\/"b)"/\"c)"\/"(a"/\"((a"\/"b)"/\"(b"\/"c))) by Def9
.= ((a"\/"b)"/\"c)"\/"((a"/\"(a"\/"b))"/\"(b"\/"c)) by Def7
.= (c"/\"(a"\/"b))"\/"(a"/\"(b"\/"c)) by Def9
.= ((c"/\"a)"\/"(c"/\"b))"\/"(a"/\"(b"\/"c)) by Def11
.= ((a"/\"b)"\/"(c"/\"a))"\/"((c"/\"a)"\/"(b"/\"c)) by Def11
.= (a"/\"b)"\/"((c"/\"a)"\/"((c"/\"a)"\/"(b"/\"c))) by Def5
.= (a"/\"b)"\/"(((c"/\"a)"\/"(c"/\"a))"\/"(b"/\"c)) by Def5
.= (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a) by Def5;
end;
registration
cluster distributive -> modular for Lattice;
coherence
proof
let L be Lattice;
assume
A1: L is distributive;
let a,b,c be Element of L;
assume a"\/"c = c;
hence a"\/"(b"/\"c) = (a"\/"b)"/\"c by A1,Th9;
end;
end;
registration
let L be 0_Lattice, a be Element of L;
reduce Bottom L "\/" a to a;
reducibility
proof
thus Bottom L"\/"a = ( Bottom L"/\"a )"\/"a by Def16
.= a by Def8;
end;
reduce Bottom L "/\" a to Bottom L;
reducibility by Def16;
end;
theorem
for L being 0_Lattice, a being Element of L holds Bottom L "\/" a = a;
theorem
for L being 0_Lattice, a being Element of L holds Bottom L "/\" a = Bottom L;
theorem
for L being 0_Lattice, a being Element of L holds Bottom L [= a;
registration
let L be 1_Lattice, a be Element of L;
reduce Top L"/\"a to a;
reducibility
proof
thus Top L"/\"a = ( Top L"\/"a )"/\"a by Def17
.= a by Def9;
end;
reduce Top L"\/"a to Top L;
reducibility by Def17;
end;
theorem
for L being 1_Lattice, a being Element of L holds Top L"/\"a = a;
theorem
for L being 1_Lattice, a being Element of L holds Top L"\/"a = Top L;
theorem
for L being 1_Lattice, a being Element of L holds a [= Top L
proof
let L be 1_Lattice, a be Element of L;
Top L"/\"a [= Top L by Th4;
hence thesis;
end;
definition
let L be non empty LattStr, x be Element of L;
assume
A1: L is complemented D_Lattice;
func x` -> Element of L means
:Def21:
it is_a_complement_of x;
existence by A1,Def19;
uniqueness
by A1,Th10;
end;
reserve L for B_Lattice;
reserve a, b for Element of L;
theorem Th18:
a`"/\"a = Bottom L
proof
a` is_a_complement_of a by Def21;
hence thesis;
end;
theorem Th19:
a`"\/"a = Top L
proof
a` is_a_complement_of a by Def21;
hence thesis;
end;
registration let L,a;
reduce a`` to a;
reducibility
proof
a` is_a_complement_of a by Def21;
then
A1: a"\/"a` =Top L & a "/\"a`= Bottom L;
a`` is_a_complement_of a` by Def21;
then a``"\/"a` = Top L & a``"/\"a` = Bottom L;
hence thesis by A1,Th10;
end;
end;
theorem
a`` = a;
theorem Th21:
( a"/\"b )` = a`"\/" b`
proof
A1: (a`"\/"b`)"/\"(a"/\"b) = (a"/\"b)"/\"(a`"\/"b`) &
(a`"\/"b`)"\/"(a"/\"b) = (a"/\"b)"\/"(a`"\/"b`);
A2: (a`"\/"b`)"/\"(a"/\"b) = ((a`"\/"b`)"/\"a)"/\"b by Def7
.= ((a`"/\"a)"\/"(b`"/\"a))"/\"b by Def11
.= (Bottom L"\/"(b`"/\"a))"/\"b by Th18
.= (b"/\"b`)"/\"a by Def7
.= Bottom L"/\"a by Th18
.= Bottom L;
(a`"\/"b`)"\/"(a"/\"b) = a`"\/"(b`"\/"(a"/\"b)) by Def5
.= a`"\/"((b`"\/"a)"/\"(b`"\/"b)) by Th9
.= a`"\/"((b`"\/"a)"/\"Top L) by Th19
.= b`"\/"(a"\/"a`) by Def5
.= b`"\/"Top L by Th19
.= Top L;
then a`"\/"b` is_a_complement_of a"/\"b by A1,A2;
hence thesis by Def21;
end;
theorem
( a"\/"b )` = a`"/\" b`
proof
thus (a"\/"b)` = (a``"\/"b``)`
.= (a`"/\"b`)`` by Th21
.= a`"/\"b`;
end;
theorem Th23:
b"/\"a = Bottom L iff b [= a`
proof
thus b"/\"a = Bottom L implies b [= a`
proof
assume
A1: b"/\"a = Bottom L;
b = b"/\"Top L
.= b"/\"(a"\/"a`) by Th19
.= Bottom L"\/"(b"/\"a`) by A1,Def11
.= b"/\"a`;
then b"\/"a` = a` by Def8;
hence thesis;
end;
thus thesis
proof
assume b [= a`;
then b"/\"a [= a`"/\"a by Th7;
then
A2: b"/\"a [= Bottom L by Th18;
Bottom L [= b"/\"a;
hence thesis by A2,Th6;
end;
end;
theorem
a [= b implies b` [= a`
proof
assume a [= b;
then b`"/\"a [= b`"/\"b by Th7;
then
A1: b`"/\"a [= Bottom L by Th18;
Bottom L [= b`"/\"a;
then b `"/\"a = Bottom L by A1,Th6;
hence thesis by Th23;
end;
begin :: Addenda
:: missing, 2009.07.28, A.T.
definition let L be non empty LattStr, S be Subset of L;
attr S is initial means
:Def22: for p,q being Element of L st p [= q & q in S holds p in S;
attr S is final means
:Def23: for p,q being Element of L st p [= q & p in S holds q in S;
attr S is meet-closed means
for p,q being Element of L st p in S & q in S holds p "/\" q in S;
attr S is join-closed means
for p,q being Element of L st p in S & q in S holds p "\/" q in S;
end;
registration let L be non empty LattStr;
cluster [#]L -> initial final non empty;
coherence;
end;
registration let L be non empty LattStr;
cluster initial final non empty for Subset of L;
existence
proof
take [#]L;
thus thesis;
end;
cluster empty -> initial final for Subset of L;
coherence;
end;
registration let L be Lattice;
cluster initial final non empty for Subset of L;
existence
proof
take [#]L;
thus thesis;
end;
end;
registration
let L be meet-absorbing meet-commutative non empty LattStr;
cluster initial -> meet-closed for Subset of L;
coherence by Th4;
end;
registration
let L be meet-absorbing join-absorbing join-associative
meet-commutative non empty LattStr;
cluster final -> join-closed for Subset of L;
coherence by Th3;
end;
theorem
for L being Lattice, S being initial final non empty Subset of L
holds S = [#]L
proof let L be Lattice, S be initial final non empty Subset of L;
consider p being Element of L such that
A1: p in S by SUBSET_1:4;
for x being Element of L holds x in S iff x in [#]L
proof let x be Element of L;
thus x in S implies x in [#]L;
assume x in [#]L;
A2: x "/\" p in S by A1,Def22,Th4;
thus x in S by A2,Def23,Th4;
end;
hence S = [#]L by SUBSET_1:3;
end;