:: Boolean Properties of Lattices
:: by Agnieszka Julia Marasik
::
:: Received March 28, 1994
:: Copyright (c) 1994-2018 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 LATTICES, SUBSET_1, XBOOLE_0, EQREL_1, PBOOLE;
notations STRUCT_0, LATTICES;
constructors LATTICES;
registrations LATTICES;
begin :: General Lattices
reserve L for Lattice;
reserve X,Y,Z,V for Element of L;
definition
let L,X,Y;
func X \ Y -> Element of L equals
:: BOOLEALG:def 1
X "/\" Y`;
end;
definition
let L,X,Y;
func X \+\ Y -> Element of L equals
:: BOOLEALG:def 2
(X \ Y) "\/" (Y \ X);
end;
definition
let L,X,Y;
redefine pred X = Y means
:: BOOLEALG:def 3
X [= Y & Y [= X;
end;
definition
let L,X,Y;
pred X meets Y means
:: BOOLEALG:def 4
X "/\" Y <> Bottom L;
end;
notation
let L,X,Y;
antonym X misses Y for X meets Y;
end;
theorem :: BOOLEALG:1
X "\/" Y [= Z implies X [= Z;
theorem :: BOOLEALG:2
X "/\" Y [= X "\/" Z;
theorem :: BOOLEALG:3
X [= Z implies X \ Y [= Z;
theorem :: BOOLEALG:4
X \ Y [= Z & Y \ X [= Z implies X \+\ Y [= Z;
theorem :: BOOLEALG:5
X = Y "\/" Z iff Y [= X & Z [= X & for V st Y [= V & Z [= V holds X [= V;
theorem :: BOOLEALG:6
X = Y "/\" Z iff X [= Y & X [= Z & for V st V [= Y & V [= Z holds V [= X;
theorem :: BOOLEALG:7
X meets X iff X <> Bottom L;
definition
let L, X, Y;
redefine pred X meets Y;
symmetry;
redefine func X \+\ Y;
commutativity;
redefine pred X misses Y;
symmetry;
end;
begin
begin :: Distributive Lattices
reserve L for D_Lattice;
reserve X,Y,Z for Element of L;
theorem :: BOOLEALG:8
(X "/\" Y) "\/" (X "/\" Z) = X implies X [= Y "\/" Z;
begin :: Distributive Bounded Lattices
reserve L for 0_Lattice;
reserve X,Y,Z for Element of L;
theorem :: BOOLEALG:9
X [= Bottom L implies X = Bottom L;
theorem :: BOOLEALG:10
X [= Y & X [= Z & Y "/\" Z = Bottom L implies X = Bottom L;
theorem :: BOOLEALG:11
X "\/" Y = Bottom L iff X = Bottom L & Y = Bottom L;
theorem :: BOOLEALG:12
X [= Y & Y "/\" Z = Bottom L implies X "/\" Z = Bottom L;
theorem :: BOOLEALG:13
X meets Y & Y [= Z implies X meets Z;
theorem :: BOOLEALG:14
X meets Y "/\" Z implies X meets Y & X meets Z;
theorem :: BOOLEALG:15
X meets Y \ Z implies X meets Y;
theorem :: BOOLEALG:16
X misses Bottom L;
theorem :: BOOLEALG:17
X misses Z & Y [= Z implies X misses Y;
theorem :: BOOLEALG:18
X misses Y or X misses Z implies X misses Y "/\" Z;
theorem :: BOOLEALG:19
X [= Y & X [= Z & Y misses Z implies X = Bottom L;
theorem :: BOOLEALG:20
X misses Y implies (Z "/\" X) misses (Z "/\" Y);
begin :: Boolean Lattices
reserve L for B_Lattice;
reserve X,Y,Z,V for Element of L;
theorem :: BOOLEALG:21
X \ Y [= Z implies X [= Y "\/" Z;
theorem :: BOOLEALG:22
X [= Y implies Z \ Y [= Z \ X;
theorem :: BOOLEALG:23
X [= Y & Z [= V implies X \ V [= Y \ Z;
theorem :: BOOLEALG:24
X [= Y "\/" Z implies X \ Y [= Z;
theorem :: BOOLEALG:25
X` [= (X "/\" Y)`;
theorem :: BOOLEALG:26
(X "\/" Y)` [= X`;
theorem :: BOOLEALG:27
X [= Y \ X implies X = Bottom L;
theorem :: BOOLEALG:28
X [= Y implies Y = X "\/" (Y \ X);
theorem :: BOOLEALG:29
X \ Y = Bottom L iff X [= Y;
theorem :: BOOLEALG:30
X [= (Y "\/" Z) & X "/\" Z = Bottom L implies X [= Y;
theorem :: BOOLEALG:31
X "\/" Y = (X \ Y) "\/" Y;
theorem :: BOOLEALG:32
X \ (X "\/" Y) = Bottom L;
theorem :: BOOLEALG:33
X \ X "/\" Y = X \ Y;
theorem :: BOOLEALG:34
(X \ Y) "/\" Y = Bottom L;
theorem :: BOOLEALG:35
X "\/" (Y \ X) = X "\/" Y;
theorem :: BOOLEALG:36
(X "/\" Y) "\/" (X \ Y) = X;
theorem :: BOOLEALG:37
X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z);
theorem :: BOOLEALG:38
X \ (X \ Y) = X "/\" Y;
theorem :: BOOLEALG:39
(X "\/" Y) \ Y = X \ Y;
theorem :: BOOLEALG:40
X "/\" Y = Bottom L iff X \ Y = X;
theorem :: BOOLEALG:41
X \ (Y "\/" Z) = (X \ Y) "/\" (X \ Z);
theorem :: BOOLEALG:42
X \ (Y "/\" Z) = (X \ Y) "\/" (X \ Z);
theorem :: BOOLEALG:43
X "/\" (Y \ Z) = X "/\" Y \ X "/\" Z;
theorem :: BOOLEALG:44
(X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X);
theorem :: BOOLEALG:45
(X \ Y) \ Z = X \ (Y "\/" Z);
theorem :: BOOLEALG:46
X \ Y = Y \ X implies X = Y;
theorem :: BOOLEALG:47
X \ Bottom L = X;
theorem :: BOOLEALG:48
(X \ Y)` = X` "\/" Y;
theorem :: BOOLEALG:49
X meets Y "\/" Z iff X meets Y or X meets Z;
theorem :: BOOLEALG:50
X "/\" Y misses X \ Y;
theorem :: BOOLEALG:51
X misses Y "\/" Z iff X misses Y & X misses Z;
theorem :: BOOLEALG:52
(X \ Y) misses Y;
theorem :: BOOLEALG:53
X misses Y implies (X "\/" Y) \ Y = X;
theorem :: BOOLEALG:54
X` "\/" Y` = X "\/" Y & X misses X` & Y misses Y` implies X = Y` & Y = X`;
theorem :: BOOLEALG:55
X` "\/" Y` = X "\/" Y & Y misses X` & X misses Y` implies X = X` & Y = Y`;
theorem :: BOOLEALG:56
X \+\ Bottom L = X;
theorem :: BOOLEALG:57
X \+\ X = Bottom L;
theorem :: BOOLEALG:58
X "/\" Y misses X \+\ Y;
theorem :: BOOLEALG:59
X "\/" Y = X \+\ (Y \ X);
theorem :: BOOLEALG:60
X \+\ (X "/\" Y) = X \ Y;
theorem :: BOOLEALG:61
X "\/" Y = (X \+\ Y) "\/" (X "/\" Y);
theorem :: BOOLEALG:62
(X \+\ Y) \+\ (X "/\" Y) = X "\/" Y;
theorem :: BOOLEALG:63
(X \+\ Y) \+\ (X "\/" Y) = X "/\" Y;
theorem :: BOOLEALG:64
X \+\ Y = (X "\/" Y) \ (X "/\" Y);
theorem :: BOOLEALG:65
(X \+\ Y) \ Z = (X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z));
theorem :: BOOLEALG:66
X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" (X "/\" Y "/\" Z);
theorem :: BOOLEALG:67
(X \+\ Y) \+\ Z = X \+\ (Y \+\ Z);
theorem :: BOOLEALG:68
(X \+\ Y)` = (X "/\" Y) "\/" (X` "/\" Y`);