:: Duality in Relation Structures
:: by Grzegorz Bancerek
::
:: Received November 12, 1996
:: Copyright (c) 1996-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 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, SUBSET_1, FUNCT_1;
requirements SUBSET, BOOLE, NUMERALS;
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;