:: Formalization of Ortholattices via Orthoposets :: by Adam Grabowski and Markus Moschner :: :: Received December 28, 2004 :: Copyright (c) 2004-2021 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 XBOOLE_0, LATTICES, SUBSET_1, EQREL_1, SHEFFER1, ROBBINS1, OPOSET_1, QMAX_1, FUNCT_1, WAYBEL_0, XXREAL_0, LATTICE3, STRUCT_0, ORDERS_2, BINOP_1, RELAT_1, FUNCT_5, ZFMISC_1, RELAT_2, FILTER_1, ORDERS_1, PBOOLE, TARSKI, YELLOW_0, WAYBEL_1, ROBBINS3, CARD_1; notations TARSKI, XBOOLE_0, ZFMISC_1, BINOP_1, RELAT_1, RELSET_1, PARTFUN1, RELAT_2, FUNCT_2, FUNCT_5, ORDINAL1, CARD_1, STRUCT_0, LATTICE3, LATTICES, ORDERS_1, ORDERS_2, FILTER_1, ROBBINS1, QMAX_1, OPOSET_1, WAYBEL_0, WAYBEL_1, YELLOW_0, SHEFFER1, PARTIT_2; constructors BINOP_1, REALSET2, LATTICE3, WAYBEL_1, YELLOW_6, OPOSET_1, SHEFFER1, FUNCT_5, RELSET_1, PARTIT_2; registrations RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0, LATTICES, YELLOW_0, YELLOW_1, ROBBINS1, OPOSET_1, SHEFFER1, PARTIT_2, CARD_1; requirements SUBSET, BOOLE; begin :: Another short axiomatization of lattices :: Originally proved by McCune with the help of OTTER definition let L be non empty \/-SemiLattStr; attr L is join-Associative means :: ROBBINS3:def 1 for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z); end; definition let L be non empty /\-SemiLattStr; attr L is meet-Associative means :: ROBBINS3:def 2 for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z); end; definition let L be non empty LattStr; attr L is meet-Absorbing means :: ROBBINS3:def 3 for x, y being Element of L holds x "\/" (x "/\" y) = x; end; theorem :: ROBBINS3:1 for L being non empty LattStr holds L is meet-Associative join-Associative meet-Absorbing join-absorbing implies L is meet-idempotent join-idempotent; theorem :: ROBBINS3:2 for L being non empty LattStr holds L is meet-Associative join-Associative meet-Absorbing join-absorbing implies L is meet-commutative join-commutative; theorem :: ROBBINS3:3 for L being non empty LattStr holds L is meet-Associative join-Associative meet-Absorbing join-absorbing implies L is meet-absorbing; theorem :: ROBBINS3:4 for L being non empty LattStr holds L is meet-Associative join-Associative meet-Absorbing join-absorbing implies L is meet-associative join-associative; theorem :: ROBBINS3:5 for L being non empty LattStr holds L is Lattice-like iff L is meet-Associative join-Associative meet-Absorbing join-absorbing; registration cluster Lattice-like -> meet-Associative join-Associative meet-Absorbing for non empty LattStr; cluster meet-Associative join-Associative meet-Absorbing join-absorbing -> Lattice-like for non empty LattStr; end; begin :: Orthoposets registration cluster OrderInvolutive -> Dneg for PartialOrdered non empty OrthoRelStr; end; theorem :: ROBBINS3:6 for L being Dneg non empty OrthoRelStr, x being Element of L holds x`` = x; theorem :: ROBBINS3:7 for O being OrderInvolutive PartialOrdered non empty OrthoRelStr , x, y being Element of O holds x <= y implies y` <= x`; registration cluster with_infima with_suprema strict for PreOrthoPoset; end; notation let L be non empty \/-SemiLattStr, x, y be Element of L; synonym x |_| y for x "\/" y; end; notation let L be non empty /\-SemiLattStr, x, y be Element of L; synonym x |^| y for x "/\" y; end; notation let L be non empty RelStr, x, y be Element of L; synonym x "|^|" y for x "/\" y; synonym x "|_|" y for x "\/" y; end; begin :: Merging relational structures and lattice structures together definition struct (\/-SemiLattStr, RelStr) \/-SemiLattRelStr (# carrier -> set, L_join -> (BinOp of the carrier), InternalRel -> Relation of the carrier #); end; definition struct (/\-SemiLattStr, RelStr) /\-SemiLattRelStr (# carrier -> set, L_meet -> (BinOp of the carrier), InternalRel -> Relation of the carrier #); end; definition struct (/\-SemiLattRelStr, \/-SemiLattRelStr, LattStr) LattRelStr (# carrier -> set, L_join, L_meet -> (BinOp of the carrier), InternalRel -> Relation of the carrier #); end; definition func TrivLattRelStr -> LattRelStr equals :: ROBBINS3:def 4 LattRelStr (# {0}, op2, op2, id{0} #); end; registration cluster TrivLattRelStr -> 1-element; end; registration cluster non empty for \/-SemiLattRelStr; cluster non empty for /\-SemiLattRelStr; cluster non empty for LattRelStr; end; theorem :: ROBBINS3:8 for R being non empty RelStr st the InternalRel of R is_reflexive_in the carrier of R & the InternalRel of R is antisymmetric transitive holds R is reflexive antisymmetric transitive; registration cluster TrivLattRelStr -> reflexive; end; registration cluster antisymmetric reflexive transitive with_suprema with_infima for LattRelStr; end; registration cluster TrivLattRelStr -> meet-Absorbing; end; registration cluster Lattice-like for non empty LattRelStr; end; definition let L be Lattice; redefine func LattRel L -> Order of the carrier of L; end; begin :: Binary approach to ortholattices definition struct (LattRelStr, OrthoLattStr, OrthoRelStr) OrthoLattRelStr (# carrier -> set, L_join, L_meet -> (BinOp of the carrier), InternalRel -> (Relation of the carrier), Compl -> UnOp of the carrier #); end; definition func TrivCLRelStr -> OrthoLattRelStr equals :: ROBBINS3:def 5 OrthoLattRelStr (# {0}, op2, op2, id {0}, op1 #); end; :: Axiomatics for ortholattices is the classical one for lattices extended :: by the three following: :: x ^ y = c(c(x) v c(y)). % DM de_Morgan from ROBBINS1 :: c(c(x)) = x. % CC involutive from OPOSET_1, too specific :: x v c(x) = y v c(y). % ONE definition let L be non empty ComplStr; attr L is involutive means :: ROBBINS3:def 6 for x being Element of L holds x`` = x; end; definition let L be non empty ComplLLattStr; attr L is with_Top means :: ROBBINS3:def 7 for x, y being Element of L holds x |_| x` = y |_| y`; end; registration cluster TrivOrtLat -> involutive with_Top; end; registration cluster TrivCLRelStr -> 1-element; end; registration cluster TrivCLRelStr -> reflexive; end; registration cluster TrivCLRelStr -> involutive with_Top; end; registration cluster involutive with_Top de_Morgan Lattice-like for 1-element OrthoLattStr; end; definition mode Ortholattice is involutive with_Top de_Morgan Lattice-like non empty OrthoLattStr; end; begin :: Lemmas theorem :: ROBBINS3:9 for K, L being non empty LattStr st the LattStr of K = the LattStr of L & K is join-commutative holds L is join-commutative; theorem :: ROBBINS3:10 for K, L being non empty LattStr st the LattStr of K = the LattStr of L & K is meet-commutative holds L is meet-commutative; theorem :: ROBBINS3:11 for K, L being non empty LattStr st the LattStr of K = the LattStr of L & K is join-associative holds L is join-associative; theorem :: ROBBINS3:12 for K, L being non empty LattStr st the LattStr of K = the LattStr of L & K is meet-associative holds L is meet-associative; theorem :: ROBBINS3:13 for K, L being non empty LattStr st the LattStr of K = the LattStr of L & K is join-absorbing holds L is join-absorbing; theorem :: ROBBINS3:14 for K, L being non empty LattStr st the LattStr of K = the LattStr of L & K is meet-absorbing holds L is meet-absorbing; theorem :: ROBBINS3:15 for K, L being non empty LattStr st the LattStr of K = the LattStr of L & K is Lattice-like holds L is Lattice-like; theorem :: ROBBINS3:16 for L1,L2 being non empty \/-SemiLattStr st the \/-SemiLattStr of L1 = the \/-SemiLattStr of L2 for a1,b1 being Element of L1, a2,b2 being Element of L2 st a1 = a2 & b1 = b2 holds a1 "\/" b1 = a2 "\/" b2; theorem :: ROBBINS3:17 for L1,L2 being non empty /\-SemiLattStr st the /\-SemiLattStr of L1 = the /\-SemiLattStr of L2 for a1,b1 being Element of L1, a2,b2 being Element of L2 st a1 = a2 & b1 = b2 holds a1 "/\" b1 = a2 "/\" b2; theorem :: ROBBINS3:18 for K, L being non empty ComplStr, x being Element of K, y being Element of L st the Compl of K = the Compl of L & x = y holds x` = y`; theorem :: ROBBINS3:19 for K, L being non empty ComplLLattStr st the ComplLLattStr of K = the ComplLLattStr of L & K is with_Top holds L is with_Top; theorem :: ROBBINS3:20 for K, L being non empty OrthoLattStr st the OrthoLattStr of K = the OrthoLattStr of L & K is de_Morgan holds L is de_Morgan; theorem :: ROBBINS3:21 for K, L being non empty OrthoLattStr st the OrthoLattStr of K = the OrthoLattStr of L & K is involutive holds L is involutive; begin :: Structure Extensions definition let R be RelStr; mode RelAugmentation of R -> LattRelStr means :: ROBBINS3:def 8 the RelStr of it = the RelStr of R; end; definition let R be LattStr; mode LatAugmentation of R -> LattRelStr means :: ROBBINS3:def 9 the LattStr of it = the LattStr of R; end; registration let L be non empty LattStr; cluster -> non empty for LatAugmentation of L; end; registration let L be meet-associative non empty LattStr; cluster -> meet-associative for LatAugmentation of L; end; registration let L be join-associative non empty LattStr; cluster -> join-associative for LatAugmentation of L; end; registration let L be meet-commutative non empty LattStr; cluster -> meet-commutative for LatAugmentation of L; end; registration let L be join-commutative non empty LattStr; cluster -> join-commutative for LatAugmentation of L; end; registration let L be join-absorbing non empty LattStr; cluster -> join-absorbing for LatAugmentation of L; end; registration let L be meet-absorbing non empty LattStr; cluster -> meet-absorbing for LatAugmentation of L; end; definition let L be non empty \/-SemiLattRelStr; attr L is naturally_sup-generated means :: ROBBINS3:def 10 for x, y being Element of L holds x <= y iff x |_| y = y; end; definition let L be non empty /\-SemiLattRelStr; attr L is naturally_inf-generated means :: ROBBINS3:def 11 for x, y being Element of L holds x <= y iff x |^| y = x; end; registration let L be Lattice; cluster naturally_sup-generated naturally_inf-generated Lattice-like for LatAugmentation of L; end; registration cluster 1-element reflexive for LattRelStr; end; registration cluster 1-element reflexive for OrthoLattRelStr; end; registration cluster 1-element reflexive for OrthoRelStr; end; registration cluster -> involutive with_Top de_Morgan well-complemented for 1-element OrthoLattStr; end; registration cluster -> OrderInvolutive Pure PartialOrdered for 1-element reflexive OrthoRelStr; end; registration cluster -> naturally_sup-generated naturally_inf-generated for 1-element reflexive LattRelStr; end; registration cluster with_infima with_suprema naturally_sup-generated naturally_inf-generated de_Morgan Lattice-like OrderInvolutive Pure PartialOrdered for non empty OrthoLattRelStr; end; registration cluster with_infima with_suprema naturally_sup-generated naturally_inf-generated Lattice-like for non empty LattRelStr; end; theorem :: ROBBINS3:22 for L being naturally_sup-generated non empty LattRelStr, x, y being Element of L holds x <= y iff x [= y; theorem :: ROBBINS3:23 for L being naturally_sup-generated Lattice-like non empty LattRelStr holds the RelStr of L = LattPOSet L; registration cluster naturally_sup-generated Lattice-like -> with_infima with_suprema for non empty LattRelStr; end; begin :: Extending OrthoLattStr definition let R be OrthoLattStr; mode CLatAugmentation of R -> OrthoLattRelStr means :: ROBBINS3:def 12 the OrthoLattStr of it = the OrthoLattStr of R; end; registration let L be non empty OrthoLattStr; cluster -> non empty for CLatAugmentation of L; end; registration let L be meet-associative non empty OrthoLattStr; cluster -> meet-associative for CLatAugmentation of L; end; registration let L be join-associative non empty OrthoLattStr; cluster -> join-associative for CLatAugmentation of L; end; registration let L be meet-commutative non empty OrthoLattStr; cluster -> meet-commutative for CLatAugmentation of L; end; registration let L be join-commutative non empty OrthoLattStr; cluster -> join-commutative for CLatAugmentation of L; end; registration let L be meet-absorbing non empty OrthoLattStr; cluster -> meet-absorbing for CLatAugmentation of L; end; registration let L be join-absorbing non empty OrthoLattStr; cluster -> join-absorbing for CLatAugmentation of L; end; registration let L be with_Top non empty OrthoLattStr; cluster -> with_Top for CLatAugmentation of L; end; registration let L be non empty Ortholattice; cluster naturally_sup-generated naturally_inf-generated Lattice-like for CLatAugmentation of L; end; registration cluster involutive with_Top de_Morgan Lattice-like naturally_sup-generated well-complemented for non empty OrthoLattRelStr; end; theorem :: ROBBINS3:24 for L being with_infima with_suprema PartialOrdered non empty OrthoRelStr for x,y being Element of L holds x <= y implies y = x "|_|" y & x = x "|^|" y; definition let L be meet-commutative non empty /\-SemiLattStr, a, b be Element of L; redefine func a |^| b; commutativity; end; definition let L be join-commutative non empty \/-SemiLattStr, a, b be Element of L; redefine func a |_| b; commutativity; end; registration cluster meet-absorbing join-absorbing meet-commutative naturally_sup-generated -> reflexive for non empty LattRelStr; end; registration cluster join-associative naturally_sup-generated -> transitive for non empty LattRelStr; end; registration cluster join-commutative naturally_sup-generated -> antisymmetric for non empty LattRelStr; end; theorem :: ROBBINS3:25 for L being with_infima with_suprema naturally_sup-generated Lattice-like non empty OrthoLattRelStr, x, y being Element of L holds x "|_|" y = x |_| y; theorem :: ROBBINS3:26 for L being with_infima with_suprema naturally_sup-generated Lattice-like non empty OrthoLattRelStr, x, y being Element of L holds x "|^|" y = x |^| y; theorem :: ROBBINS3:27 for L being with_infima with_suprema naturally_sup-generated naturally_inf-generated Lattice-like OrderInvolutive PartialOrdered non empty OrthoLattRelStr holds L is de_Morgan; registration let L be Ortholattice; cluster -> involutive for CLatAugmentation of L; end; registration let L be Ortholattice; cluster -> de_Morgan for CLatAugmentation of L; end; theorem :: ROBBINS3:28 for L being non empty OrthoLattRelStr st L is involutive with_Top de_Morgan Lattice-like naturally_sup-generated holds L is Orthocomplemented PartialOrdered; theorem :: ROBBINS3:29 for L being Ortholattice, E being naturally_sup-generated CLatAugmentation of L holds E is Orthocomplemented; registration let L be Ortholattice; cluster -> Orthocomplemented for naturally_sup-generated CLatAugmentation of L; end; theorem :: ROBBINS3:30 for L being non empty OrthoLattStr st L is Boolean well-complemented Lattice-like holds L is Ortholattice; registration cluster Boolean well-complemented Lattice-like -> involutive with_Top de_Morgan for non empty OrthoLattStr; end;