The abstract of the Mizar article:

Duality in Relation Structures

by

Grzegorz Bancerek

Received November 12, 1996

MML identifier: YELLOW_7

[ Mizar article, MML identifier index ]

environ

 vocabulary ORDERS_1, RELAT_1, OPPCAT_1, RELAT_2, LATTICE3, YELLOW_0, LATTICES,
      BHSP_3, WAYBEL_0, FINSET_1, QUANTAL1, BOOLE, ZF_LANG, PRE_TOPC, FUNCT_1,
      CAT_1, WELLORD1, SEQM_3, WAYBEL_1, PBOOLE, WAYBEL_5, FUNCT_6, FUNCOP_1,
      ZF_REFLE, FINSEQ_4, YELLOW_2, ORDINAL2, CARD_3, PRALG_1, REALSET1,
      YELLOW_7;
 notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, RELSET_1, FUNCT_1,
      FUNCT_2, FINSET_1, CARD_3, FUNCT_6, REALSET1, PRE_TOPC, PRALG_1, PBOOLE,
      STRUCT_0, ORDERS_1, LATTICE3, YELLOW_0, YELLOW_2, WAYBEL_1, WAYBEL_0,
      WAYBEL_5;
 constructors LATTICE3, WAYBEL_1, ORDERS_3, WAYBEL_5, PRALG_2;
 clusters RELSET_1, STRUCT_0, PRALG_1, MSUALG_1, LATTICE3, YELLOW_0, WAYBEL_0,
      WAYBEL_1, WAYBEL_5, FINSET_1, PBOOLE, PRVECT_1, CANTOR_1, SUBSET_1,
      FRAENKEL, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

definition
 let L be RelStr;
 redefine func L~; synonym L opp;
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;

definition
 let L be reflexive RelStr;
 cluster L opp -> reflexive;
end;

definition
 let L be transitive RelStr;
 cluster L opp -> transitive;
end;

definition
 let L be antisymmetric RelStr;
 cluster L opp -> antisymmetric;
end;

definition
 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;

definition
 let L be with_infima RelStr;
 cluster L opp -> with_suprema;
end;

definition
 let L be with_suprema RelStr;
 cluster L opp -> with_infima;
end;

definition
 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;

definition
 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;

definition
 let L be lower-bounded RelStr;
 cluster L opp -> upper-bounded;
end;

definition
 let L be upper-bounded RelStr;
 cluster L opp -> lower-bounded;
end;

definition
 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 -> map of L, L opp means
:: YELLOW_7:def 1

  for x being Element of L holds it.x = 'not' x;
end;

definition
 let L be Boolean LATTICE;
 cluster ComplMap L -> one-to-one;
end;

definition
 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 map of S,T iff f is map of S opp,T) &
   (f is map of S,T iff f is map of S,T opp) &
   (f is map of S,T iff f is map of S opp,T opp);

theorem :: YELLOW_7:40
   for S,T being non empty RelStr
 for f being map of S,T, g being map 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 map of S,T opp, g being map 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 map of S,T, g being map 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 map of S,T, g1 being map of T,S
 for f2 being map of S~,T~, g2 being map 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);

definition
 cluster completely-distributive -> complete (non empty RelStr);
end;

definition
 cluster completely-distributive trivial strict (non empty Poset);
end;

theorem :: YELLOW_7:51
   for L being non empty Poset holds
   L is completely-distributive iff L opp is completely-distributive;