:: Orthomodular Lattices
:: by El\.zbieta M\c{a}dra and Adam Grabowski
::
:: Received June 27, 2008
:: Copyright (c) 2008-2016 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 NUMBERS, LATTICES, LATTICE3, SUBSET_1, FILTER_1, PBOOLE, EQREL_1,
ZFMISC_1, ROBBINS3, XBOOLE_0, ROBBINS1, OPOSET_1, ORDERS_2, YELLOW_1,
CARD_1, RELAT_2, TARSKI, STRUCT_0, XXREAL_0, FILTER_0, FUNCT_1, BINOP_1,
RVSUM_1, SYMSP_1, ROBBINS4;
notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, SUBSET_1, BINOP_1, FUNCT_1,
ORDINAL1, CARD_1, NUMBERS, FUNCT_2, STRUCT_0, LATTICE3, LATTICES,
ORDERS_2, ROBBINS1, YELLOW_1, ROBBINS3;
constructors BINOP_1, REALSET2, LATTICE3, ROBBINS3, YELLOW_1, RELSET_1;
registrations SUBSET_1, RELAT_1, STRUCT_0, LATTICES, YELLOW_1, ROBBINS1,
SHEFFER1, ROBBINS3, XBOOLE_0, ORDINAL1;
requirements SUBSET, BOOLE, NUMERALS, REAL;
begin :: Preliminaries
registration
let L be Lattice;
cluster the LattStr of L -> Lattice-like;
end;
theorem :: ROBBINS4:1
for K,L being Lattice st the LattStr of K = the LattStr of L
holds LattPOSet K = LattPOSet L;
registration
cluster -> meet-Absorbing for 1-element OrthoLattStr;
end;
registration
cluster -> lower-bounded for Ortholattice;
cluster -> upper-bounded for Ortholattice;
end;
reserve L for Ortholattice,
a, b, c for Element of L;
theorem :: ROBBINS4:2
a "\/" a` = Top L & a "/\" a` = Bottom L;
theorem :: ROBBINS4:3
for L being non empty OrthoLattStr holds L is Ortholattice iff (
for a, b, c being Element of L holds (a "\/" b) "\/" c = (c` "/\" b`)` "\/" a)
& (for a, b being Element of L holds a = a "/\" (a "\/" b)) & for a, b being
Element of L holds a = a "\/" (b "/\" b`);
theorem :: ROBBINS4:4
for L being involutive Lattice-like non empty OrthoLattStr
holds L is de_Morgan iff for a,b being Element of L st a [= b holds b` [= a`;
begin :: Orthomodularity
definition
let L be non empty OrthoLattStr;
attr L is orthomodular means
:: ROBBINS4:def 1
for x, y being Element of L st x [= y holds y = x "\/" (x` "/\" y);
end;
registration
cluster trivial orthomodular modular Boolean for Ortholattice;
end;
theorem :: ROBBINS4:5
for L being modular Ortholattice holds L is orthomodular;
definition
mode Orthomodular_Lattice is orthomodular Ortholattice;
end;
theorem :: ROBBINS4:6
for L being orthomodular meet-absorbing join-absorbing
join-associative meet-commutative non empty OrthoLattStr, x, y being Element
of L holds x "\/" (x` "/\" (x "\/" y)) = x "\/" y;
definition
let L be non empty OrthoLattStr;
attr L is Orthomodular means
:: ROBBINS4:def 2
for x, y being Element of L holds x "\/" (x` "/\" (x "\/" y)) = x "\/" y;
end;
registration
cluster Orthomodular -> orthomodular for meet-absorbing join-absorbing
join-associative meet-commutative non empty OrthoLattStr;
cluster orthomodular -> Orthomodular for meet-absorbing join-absorbing
join-associative meet-commutative non empty OrthoLattStr;
end;
registration
cluster modular -> orthomodular for Ortholattice;
end;
registration
cluster join-Associative meet-Absorbing de_Morgan orthomodular for
Ortholattice;
end;
begin :: Examples: The Benzene Ring
definition
func B_6 -> RelStr equals
:: ROBBINS4:def 3
InclPoset { 0, 1, 3 \ 1, 2, 3 \ 2, 3 };
end;
registration
cluster B_6 -> non empty;
cluster B_6 -> reflexive transitive antisymmetric;
end;
registration
cluster B_6 -> with_suprema with_infima;
end;
theorem :: ROBBINS4:7
the carrier of latt B_6 = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 };
theorem :: ROBBINS4:8
for a being set st a in the carrier of latt B_6 holds a c= Segm 3;
definition
func Benzene -> strict OrthoLattStr means
:: ROBBINS4:def 4
the LattStr of it = latt
B_6 & for x being Element of it, y being Subset of 3 st x = y
holds (the Compl of it).x = y`;
end;
theorem :: ROBBINS4:9
the carrier of Benzene = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 };
theorem :: ROBBINS4:10
the carrier of Benzene c= bool 3;
theorem :: ROBBINS4:11
for a being set st a in the carrier of Benzene holds a c= {0,1,2
};
registration
cluster Benzene -> non empty;
cluster Benzene -> Lattice-like;
end;
theorem :: ROBBINS4:12
LattPOSet the LattStr of Benzene = B_6;
theorem :: ROBBINS4:13
for a, b being Element of B_6, x, y being Element of Benzene st
a = x & b = y holds a <= b iff x [= y;
theorem :: ROBBINS4:14
for a, b being Element of B_6, x, y being Element of Benzene st
a = x & b = y holds a "\/" b = x "\/" y & a "/\" b = x "/\" y;
theorem :: ROBBINS4:15
for a, b being Element of B_6 st a = 3 \ 1 & b = 2 holds a "\/"
b = 3 & a "/\" b = 0;
theorem :: ROBBINS4:16
for a, b being Element of B_6 st a = 3 \ 2 & b = 1 holds a "\/"
b = 3 & a "/\" b = 0;
theorem :: ROBBINS4:17
for a, b being Element of B_6 st a = 3 \ 1 & b = 1 holds a "\/"
b = 3 & a "/\" b = 0;
theorem :: ROBBINS4:18
for a, b being Element of B_6 st a = 3 \ 2 & b = 2 holds a "\/"
b = 3 & a "/\" b = 0;
theorem :: ROBBINS4:19
for a, b being Element of Benzene st a = 3 \ 1 & b = 2 holds a
"\/" b = 3 & a "/\" b = 0;
theorem :: ROBBINS4:20
for a, b being Element of Benzene st a = 3 \ 2 & b = 1 holds a "\/" b = 3;
theorem :: ROBBINS4:21
for a, b being Element of Benzene st a = 3 \ 1 & b = 1 holds a "\/" b = 3;
theorem :: ROBBINS4:22
for a, b being Element of Benzene st a = 3 \ 2 & b = 2 holds a "\/" b = 3;
theorem :: ROBBINS4:23
for a being Element of Benzene holds (a = 0 implies a` = 3) & (a
= 3 implies a` = 0) & (a = 1 implies a` = 3\1) & (a = 3\1 implies a` = 1) & (a
= 2 implies a` = 3\2) & (a = 3\2 implies a` = 2);
theorem :: ROBBINS4:24
for a, b being Element of Benzene holds a [= b iff a c= b;
theorem :: ROBBINS4:25
for a, x being Element of Benzene st a = 0 holds a "/\" x = a;
theorem :: ROBBINS4:26
for a, x being Element of Benzene st a = 0 holds a "\/" x = x;
theorem :: ROBBINS4:27
for a, x being Element of Benzene st a = 3 holds a "\/" x = a;
registration
cluster Benzene -> lower-bounded;
cluster Benzene -> upper-bounded;
end;
theorem :: ROBBINS4:28
Top Benzene = 3;
theorem :: ROBBINS4:29
Bottom Benzene = 0;
registration
cluster Benzene -> involutive with_Top de_Morgan;
cluster Benzene -> non orthomodular;
end;
begin :: Orthogonality
definition
let L be Ortholattice, a,b be Element of L;
pred a, b are_orthogonal means
:: ROBBINS4:def 5
a [= b`;
end;
notation
let L be Ortholattice, a,b be Element of L;
synonym a _|_ b for a, b are_orthogonal;
end;
theorem :: ROBBINS4:30
a _|_ a iff a = Bottom L;
definition
let L be Ortholattice;
let a, b be Element of L;
redefine pred a,b are_orthogonal;
symmetry;
end;
theorem :: ROBBINS4:31
a _|_ b & a _|_ c implies a _|_ (b "/\" c) & a _|_ (b "\/" c);
begin :: Orthomodularity Conditions
theorem :: ROBBINS4:32
L is orthomodular iff for a,b being Element of L st b` [= a & a "/\" b
= Bottom L holds a = b`;
theorem :: ROBBINS4:33
L is orthomodular iff for a,b being Element of L st a _|_ b & a "\/" b
= Top L holds a = b`;
theorem :: ROBBINS4:34
L is orthomodular iff for a,b being Element of L st b [= a holds
a "/\" (a` "\/" b) = b;
theorem :: ROBBINS4:35
L is orthomodular iff for a,b holds a "/\" (a` "\/" (a "/\" b)) = a "/\" b;
theorem :: ROBBINS4:36
L is orthomodular iff for a,b being Element of L holds a "\/" b
= ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" a`);
theorem :: ROBBINS4:37
L is orthomodular iff for a,b st a [= b holds (a "\/" b) "/\" (b "\/"
a`) = (a "/\" b) "\/" (b "/\" a`);
::$N The short(est) axiomatization of orthomodular ortholattices
theorem :: ROBBINS4:38
for L being non empty OrthoLattStr holds L is Orthomodular_Lattice iff
(for a, b, c being Element of L holds (a "\/" b) "\/" c = (c` "/\" b`)` "\/" a)
& (for a, b,c being Element of L holds a "\/" b = ((a "\/" b) "/\" (a "\/" c))
"\/" ((a "\/" b) "/\" a`)) & for a, b being Element of L holds a = a "\/" (b
"/\" b`);
reserve L for join-Associative meet-Absorbing de_Morgan orthomodular
Lattice-like non empty OrthoLattStr;
reserve v0,v1,v2,v64,v65 for Element of L;
registration
cluster -> with_Top for
join-Associative meet-Absorbing de_Morgan orthomodular
Lattice-like non empty OrthoLattStr;
end;
theorem :: ROBBINS4:39
for L being non empty OrthoLattStr holds L is Orthomodular_Lattice iff
L is join-Associative meet-Absorbing de_Morgan Orthomodular;