:: Duality in Relation Structures :: by Grzegorz Bancerek :: :: Received November 12, 1996 :: Copyright (c) 1996-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 ORDERS_2, ARYTM_0, RELAT_1, SUBSET_1, XXREAL_0, XBOOLE_0, RELAT_2, STRUCT_0, LATTICE3, YELLOW_0, EQREL_1, LATTICES, REWRITE1, WAYBEL_0, TARSKI, FINSET_1, XXREAL_2, XBOOLEAN, FUNCT_1, CAT_1, WELLORD1, SEQM_3, WAYBEL_1, PBOOLE, WAYBEL_5, FUNCT_6, FUNCOP_1, FINSEQ_4, YELLOW_2, ORDINAL2, CARD_3, YELLOW_7, CARD_1; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, CARD_3, FUNCT_6, PRALG_1, PBOOLE, FUNCOP_1, STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, YELLOW_2, WAYBEL_1, WAYBEL_0, WAYBEL_5; constructors DOMAIN_1, LATTICE3, PRALG_1, PRALG_2, ORDERS_3, WAYBEL_1, WAYBEL_5, RELSET_1; registrations RELSET_1, FUNCOP_1, FINSET_1, CARD_3, PBOOLE, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, WAYBEL_5, FUNCT_1; requirements SUBSET, BOOLE; begin notation let L be RelStr; synonym L opp for L~; end; theorem :: YELLOW_7:1 for L being RelStr, x,y being Element of L opp holds x <= y iff ~ x >= ~y; theorem :: YELLOW_7:2 for L being RelStr, x being Element of L, y being Element of L opp holds (x <= ~y iff x~ >= y) & (x >= ~y iff x~ <= y); theorem :: YELLOW_7:3 for L being RelStr holds L is empty iff L opp is empty; theorem :: YELLOW_7:4 for L being RelStr holds L is reflexive iff L opp is reflexive; theorem :: YELLOW_7:5 for L being RelStr holds L is antisymmetric iff L opp is antisymmetric; theorem :: YELLOW_7:6 for L being RelStr holds L is transitive iff L opp is transitive; theorem :: YELLOW_7:7 for L being non empty RelStr holds L is connected iff L opp is connected; registration let L be reflexive RelStr; cluster L opp -> reflexive; end; registration let L be transitive RelStr; cluster L opp -> transitive; end; registration let L be antisymmetric RelStr; cluster L opp -> antisymmetric; end; registration let L be connected non empty RelStr; cluster L opp -> connected; end; theorem :: YELLOW_7:8 for L being RelStr, x being Element of L, X being set holds (x is_<=_than X iff x~ is_>=_than X) & (x is_>=_than X iff x~ is_<=_than X); theorem :: YELLOW_7:9 for L being RelStr, x being Element of L opp, X being set holds ( x is_<=_than X iff ~x is_>=_than X) & (x is_>=_than X iff ~x is_<=_than X); theorem :: YELLOW_7:10 for L being RelStr, X being set holds ex_sup_of X,L iff ex_inf_of X,L opp; theorem :: YELLOW_7:11 for L being RelStr, X being set holds ex_sup_of X,L opp iff ex_inf_of X,L; theorem :: YELLOW_7:12 for L being non empty RelStr, X being set st ex_sup_of X,L or ex_inf_of X,L opp holds "\/"(X,L) = "/\"(X,L opp); theorem :: YELLOW_7:13 for L being non empty RelStr, X being set st ex_inf_of X,L or ex_sup_of X,L opp holds "/\"(X,L) = "\/"(X,L opp); theorem :: YELLOW_7:14 for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2 & L1 is with_infima holds L2 is with_infima; theorem :: YELLOW_7:15 for L1,L2 being RelStr st the RelStr of L1 = the RelStr of L2 & L1 is with_suprema holds L2 is with_suprema; theorem :: YELLOW_7:16 for L being RelStr holds L is with_infima iff L opp is with_suprema; :: LATTICE3:10 :: for L being RelStr holds L opp is with_infima iff L is with_suprema; theorem :: YELLOW_7:17 for L being non empty RelStr holds L is complete iff L opp is complete; registration let L be with_infima RelStr; cluster L opp -> with_suprema; end; registration let L be with_suprema RelStr; cluster L opp -> with_infima; end; registration let L be complete non empty RelStr; cluster L opp -> complete; end; theorem :: YELLOW_7:18 for L being non empty RelStr for X being Subset of L, Y being Subset of L opp st X = Y holds fininfs X = finsups Y & finsups X = fininfs Y; theorem :: YELLOW_7:19 for L being RelStr for X being Subset of L, Y being Subset of L opp st X = Y holds downarrow X = uparrow Y & uparrow X = downarrow Y; theorem :: YELLOW_7:20 for L being non empty RelStr for x being Element of L, y being Element of L opp st x = y holds downarrow x = uparrow y & uparrow x = downarrow y; theorem :: YELLOW_7:21 for L being with_infima Poset, x,y being Element of L holds x "/\"y = (x~)"\/"(y~); theorem :: YELLOW_7:22 for L being with_infima Poset, x,y being Element of L opp holds (~x)"/\"(~y) = x"\/"y; theorem :: YELLOW_7:23 for L being with_suprema Poset, x,y being Element of L holds x "\/"y = (x~)"/\"(y~); theorem :: YELLOW_7:24 for L being with_suprema Poset, x,y being Element of L opp holds (~x)"\/"(~y) = x"/\"y; theorem :: YELLOW_7:25 for L being LATTICE holds L is distributive iff L opp is distributive; registration let L be distributive LATTICE; cluster L opp -> distributive; end; theorem :: YELLOW_7:26 for L being RelStr, x be set holds x is directed Subset of L iff x is filtered Subset of L opp; theorem :: YELLOW_7:27 for L being RelStr, x be set holds x is directed Subset of L opp iff x is filtered Subset of L; theorem :: YELLOW_7:28 for L being RelStr, x be set holds x is lower Subset of L iff x is upper Subset of L opp; theorem :: YELLOW_7:29 for L being RelStr, x be set holds x is lower Subset of L opp iff x is upper Subset of L; theorem :: YELLOW_7:30 for L being RelStr holds L is lower-bounded iff L opp is upper-bounded; theorem :: YELLOW_7:31 for L being RelStr holds L opp is lower-bounded iff L is upper-bounded; theorem :: YELLOW_7:32 for L being RelStr holds L is bounded iff L opp is bounded; theorem :: YELLOW_7:33 for L being lower-bounded antisymmetric non empty RelStr holds (Bottom L)~ = Top (L opp) & ~Top (L opp) = Bottom L; theorem :: YELLOW_7:34 for L being upper-bounded antisymmetric non empty RelStr holds (Top L) ~ = Bottom (L opp) & ~Bottom (L opp) = Top L; theorem :: YELLOW_7:35 for L being bounded LATTICE, x,y being Element of L holds y is_a_complement_of x iff y~ is_a_complement_of x~; theorem :: YELLOW_7:36 for L being bounded LATTICE holds L is complemented iff L opp is complemented ; registration let L be lower-bounded RelStr; cluster L opp -> upper-bounded; end; registration let L be upper-bounded RelStr; cluster L opp -> lower-bounded; end; registration let L be complemented bounded LATTICE; cluster L opp -> complemented; end; :: Collorary: L is Boolean -> L opp is Boolean theorem :: YELLOW_7:37 for L being Boolean LATTICE, x being Element of L holds 'not'(x~) = 'not' x; definition let L be non empty RelStr; func ComplMap L -> Function of L, L opp means :: YELLOW_7:def 1 for x being Element of L holds it.x = 'not' x; end; registration let L be Boolean LATTICE; cluster ComplMap L -> one-to-one; end; registration let L be Boolean LATTICE; cluster ComplMap L -> isomorphic; end; theorem :: YELLOW_7:38 for L being Boolean LATTICE holds L, L opp are_isomorphic; theorem :: YELLOW_7:39 for S,T being non empty RelStr, f be set holds (f is Function of S,T iff f is Function of S opp,T) & (f is Function of S,T iff f is Function of S,T opp) & (f is Function of S,T iff f is Function of S opp,T opp); theorem :: YELLOW_7:40 for S,T being non empty RelStr for f being Function of S,T, g being Function of S,T opp st f = g holds (f is monotone iff g is antitone) & (f is antitone iff g is monotone); theorem :: YELLOW_7:41 for S,T being non empty RelStr for f being Function of S,T opp, g being Function of S opp,T st f = g holds (f is monotone iff g is monotone) & (f is antitone iff g is antitone); theorem :: YELLOW_7:42 for S,T being non empty RelStr for f being Function of S,T, g being Function of S opp,T opp st f = g holds (f is monotone iff g is monotone) & (f is antitone iff g is antitone); theorem :: YELLOW_7:43 for S,T being non empty RelStr, f be set holds (f is Connection of S,T iff f is Connection of S~,T) & (f is Connection of S,T iff f is Connection of S ,T~) & (f is Connection of S,T iff f is Connection of S~,T~); theorem :: YELLOW_7:44 for S,T being non empty Poset for f1 being Function of S,T, g1 being Function of T,S for f2 being Function of S~,T~, g2 being Function of T~,S~ st f1 = f2 & g1 = g2 holds [f1,g1] is Galois iff [g2,f2] is Galois; theorem :: YELLOW_7:45 for J being set, D being non empty set, K being ManySortedSet of J for F being DoubleIndexedSet of K,D holds doms F = K; definition let J, D be non empty set, K be non-empty ManySortedSet of J; let F be DoubleIndexedSet of K, D; let j be Element of J; let k be Element of K.j; redefine func F..(j,k) -> Element of D; end; theorem :: YELLOW_7:46 for L being non empty RelStr for J being set, K being ManySortedSet of J for x being set holds x is DoubleIndexedSet of K,L iff x is DoubleIndexedSet of K,L opp; theorem :: YELLOW_7:47 for L being complete LATTICE for J being non empty set, K being non-empty ManySortedSet of J for F being DoubleIndexedSet of K,L holds Sup Infs F <= Inf Sups Frege F; theorem :: YELLOW_7:48 for L being complete LATTICE holds L is completely-distributive iff for J being non empty set, K being non-empty ManySortedSet of J for F being DoubleIndexedSet of K,L holds Sup Infs F = Inf Sups Frege F; theorem :: YELLOW_7:49 for L being complete antisymmetric non empty RelStr, F be Function holds \\/(F, L) = //\(F, L opp) & //\(F, L) = \\/(F, L opp); theorem :: YELLOW_7:50 for L being complete antisymmetric non empty RelStr for F be Function-yielding Function holds \//(F, L) = /\\(F, L opp) & /\\(F, L) = \//(F, L opp); registration cluster completely-distributive -> complete for non empty RelStr; end; registration cluster completely-distributive strict for 1-element Poset; end; theorem :: YELLOW_7:51 for L being non empty Poset holds L is completely-distributive iff L opp is completely-distributive;