:: Duality in Relation Structures
:: by Grzegorz Bancerek
::
:: Received November 12, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users

notation

let L be RelStr ;
synonym L opp for L ~ ;

end;

theorem Th1: :: YELLOW_7:1

for L being RelStr
for x, y being Element of (L opp) holds
( x <= y iff ~ x >= ~ y )

proof end;

theorem Th2: :: YELLOW_7:2

for L being RelStr
for x being Element of L
for y being Element of (L opp) holds
( ( x <= ~ y implies x ~ >= y ) & ( x ~ >= y implies x <= ~ y ) & ( x >= ~ y implies x ~ <= y ) & ( x ~ <= y implies x >= ~ y ) )

proof end;

theorem :: YELLOW_7:3

for L being RelStr holds
( L is empty iff L opp is empty ) ;

theorem Th4: :: YELLOW_7:4

for L being RelStr holds
( L is reflexive iff L opp is reflexive )

proof end;

theorem Th5: :: YELLOW_7:5

for L being RelStr holds
( L is antisymmetric iff L opp is antisymmetric )

proof end;

theorem Th6: :: YELLOW_7:6

for L being RelStr holds
( L is transitive iff L opp is transitive )

proof end;

theorem Th7: :: YELLOW_7:7

for L being non empty RelStr holds
( L is connected iff L opp is connected )

proof end;

registration

let L be reflexive RelStr ;

cluster L opp -> reflexive ;

coherence
L opp is reflexive by Th4;

end;

registration

let L be transitive RelStr ;

cluster L opp -> transitive ;

coherence
L opp is transitive by Th6;

end;

registration

let L be antisymmetric RelStr ;

cluster L opp -> antisymmetric ;

coherence
L opp is antisymmetric by Th5;

end;

registration

let L be non empty connected RelStr ;

cluster L opp -> connected ;

coherence
L opp is connected by Th7;

end;

theorem Th8: :: YELLOW_7:8

for L being RelStr
for x being Element of L
for X being set holds
( ( x is_<=_than X implies x ~ is_>=_than X ) & ( x ~ is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies x ~ is_<=_than X ) & ( x ~ is_<=_than X implies x is_>=_than X ) )

proof end;

theorem Th9: :: YELLOW_7:9

for L being RelStr
for x being Element of (L opp)
for X being set holds
( ( x is_<=_than X implies ~ x is_>=_than X ) & ( ~ x is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies ~ x is_<=_than X ) & ( ~ x is_<=_than X implies x is_>=_than X ) )

proof end;

theorem Th10: :: YELLOW_7:10

for L being RelStr
for X being set holds
( ex_sup_of X,L iff ex_inf_of X,L opp )

proof end;

theorem Th11: :: YELLOW_7:11

for L being RelStr
for X being set holds
( ex_sup_of X,L opp iff ex_inf_of X,L )

proof end;

theorem Th12: :: YELLOW_7:12

for L being non empty RelStr
for X being set st ( ex_sup_of X,L or ex_inf_of X,L opp ) holds
"\/" (X,L) = "/\" (X,(L opp))

proof end;

theorem Th13: :: YELLOW_7:13

for L being non empty RelStr
for X being set st ( ex_inf_of X,L or ex_sup_of X,L opp ) holds
"/\" (X,L) = "\/" (X,(L opp))

proof end;

theorem Th14: :: YELLOW_7:14

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is with_infima holds
L2 is with_infima

proof end;

theorem :: YELLOW_7:15

for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is with_suprema holds
L2 is with_suprema

proof end;

theorem Th16: :: YELLOW_7:16

for L being RelStr holds
( L is with_infima iff L opp is with_suprema )

proof end;

:: LATTICE3:10
:: for L being RelStr holds L opp is with_infima iff L is with_suprema;

theorem Th17: :: YELLOW_7:17

for L being non empty RelStr holds
( L is complete iff L opp is complete )

proof end;

registration

let L be with_infima RelStr ;

cluster L opp -> with_suprema ;

coherence
L opp is with_suprema by Th16;

end;

registration

let L be with_suprema RelStr ;

cluster L opp -> with_infima ;

coherence
L opp is with_infima by LATTICE3:10;

end;

registration

let L be non empty complete RelStr ;

cluster L opp -> complete ;

coherence
L opp is complete by Th17;

end;

theorem :: YELLOW_7:18

for L being non empty RelStr
for X being Subset of L
for Y being Subset of (L opp) st X = Y holds
( fininfs X = finsups Y & finsups X = fininfs Y )

proof end;

theorem Th19: :: YELLOW_7:19

for L being RelStr
for X being Subset of L
for Y being Subset of (L opp) st X = Y holds
( downarrow X = uparrow Y & uparrow X = downarrow Y )

proof end;

theorem :: YELLOW_7:20

for L being non empty RelStr
for x being Element of L
for y being Element of (L opp) st x = y holds
( downarrow x = uparrow y & uparrow x = downarrow y ) by Th19;

theorem Th21: :: YELLOW_7:21

for L being with_infima Poset
for x, y being Element of L holds x "/\" y = (x ~) "\/" (y ~)

proof end;

theorem Th22: :: YELLOW_7:22

for L being with_infima Poset
for x, y being Element of (L opp) holds (~ x) "/\" (~ y) = x "\/" y

proof end;

theorem Th23: :: YELLOW_7:23

for L being with_suprema Poset
for x, y being Element of L holds x "\/" y = (x ~) "/\" (y ~)

proof end;

theorem Th24: :: YELLOW_7:24

for L being with_suprema Poset
for x, y being Element of (L opp) holds (~ x) "\/" (~ y) = x "/\" y

proof end;

theorem Th25: :: YELLOW_7:25

for L being LATTICE holds
( L is distributive iff L opp is distributive )

proof end;

registration

let L be distributive LATTICE;

cluster L opp -> distributive ;

coherence
L opp is distributive by Th25;

end;

theorem Th26: :: YELLOW_7:26

for L being RelStr
for x being set holds
( x is directed Subset of L iff x is filtered Subset of (L opp) )

proof end;

theorem :: YELLOW_7:27

for L being RelStr
for x being set holds
( x is directed Subset of (L opp) iff x is filtered Subset of L )

proof end;

theorem Th28: :: YELLOW_7:28

for L being RelStr
for x being set holds
( x is lower Subset of L iff x is upper Subset of (L opp) )

proof end;

theorem :: YELLOW_7:29

for L being RelStr
for x being set holds
( x is lower Subset of (L opp) iff x is upper Subset of L )

proof end;

theorem Th30: :: YELLOW_7:30

for L being RelStr holds
( L is lower-bounded iff L opp is upper-bounded )

proof end;

theorem Th31: :: YELLOW_7:31

for L being RelStr holds
( L opp is lower-bounded iff L is upper-bounded )

proof end;

theorem :: YELLOW_7:32

for L being RelStr holds
( L is bounded iff L opp is bounded ) by Th30, Th31;

theorem :: YELLOW_7:33

for L being non empty antisymmetric lower-bounded RelStr holds
( (Bottom L) ~ = Top (L opp) & ~ (Top (L opp)) = Bottom L ) by Th12, YELLOW_0:42;

theorem :: YELLOW_7:34

for L being non empty antisymmetric upper-bounded RelStr holds
( (Top L) ~ = Bottom (L opp) & ~ (Bottom (L opp)) = Top L ) by Th13, YELLOW_0:43;

theorem Th35: :: YELLOW_7:35

for L being bounded LATTICE
for x, y being Element of L holds
( y is_a_complement_of x iff y ~ is_a_complement_of x ~ )

proof end;

theorem Th36: :: YELLOW_7:36

for L being bounded LATTICE holds
( L is complemented iff L opp is complemented )

proof end;

registration

let L be lower-bounded RelStr ;

cluster L opp -> upper-bounded ;

coherence
L opp is upper-bounded by Th30;

end;

registration

let L be upper-bounded RelStr ;

cluster L opp -> lower-bounded ;

coherence
L opp is lower-bounded by Th31;

end;

registration

let L be bounded complemented LATTICE;

cluster L opp -> complemented ;

coherence
L opp is complemented by Th36;

end;

:: Collorary: L is Boolean -> L opp is Boolean

theorem :: YELLOW_7:37

for L being Boolean LATTICE
for x being Element of L holds 'not' (x ~) = 'not' x

proof end;

definition

let L be non empty RelStr ;

func ComplMap L -> Function of L,(L opp) means :Def1: :: YELLOW_7:def 1
for x being Element of L holds it . x = 'not' x;

existence
ex b₁ being Function of L,(L opp) st
for x being Element of L holds b₁ . x = 'not' x

proof end;

correctness
uniqueness
for b₁, b₂ being Function of L,(L opp) st ( for x being Element of L holds b₁ . x = 'not' x ) & ( for x being Element of L holds b₂ . x = 'not' x ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def1 defines ComplMap YELLOW_7:def 1 :
for L being non empty RelStr
for b₂ being Function of L,(L opp) holds
( b₂ = ComplMap L iff for x being Element of L holds b₂ . x = 'not' x );

registration

let L be Boolean LATTICE;

cluster ComplMap L -> V13() ;

coherence
ComplMap L is one-to-one

proof end;

end;

registration

let L be Boolean LATTICE;

cluster ComplMap L -> isomorphic ;

coherence
ComplMap L is isomorphic

proof end;

end;

theorem :: YELLOW_7:38

for L being Boolean LATTICE holds L,L opp are_isomorphic

proof end;

theorem :: YELLOW_7:39

for S, T being non empty RelStr
for f being set holds
( ( f is Function of S,T implies f is Function of (S opp),T ) & ( f is Function of (S opp),T implies f is Function of S,T ) & ( f is Function of S,T implies f is Function of S,(T opp) ) & ( f is Function of S,(T opp) implies f is Function of S,T ) & ( f is Function of S,T implies f is Function of (S opp),(T opp) ) & ( f is Function of (S opp),(T opp) implies f is Function of S,T ) ) ;

theorem :: YELLOW_7:40

for S, T being non empty RelStr
for f being Function of S,T
for g being Function of S,(T opp) st f = g holds
( ( f is monotone implies g is antitone ) & ( g is antitone implies f is monotone ) & ( f is antitone implies g is monotone ) & ( g is monotone implies f is antitone ) )

proof end;

theorem :: YELLOW_7:41

for S, T being non empty RelStr
for f being Function of S,(T opp)
for g being Function of (S opp),T st f = g holds
( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) )

proof end;

theorem Th42: :: YELLOW_7:42

for S, T being non empty RelStr
for f being Function of S,T
for g being Function of (S opp),(T opp) st f = g holds
( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) )

proof end;

theorem :: YELLOW_7:43

for S, T being non empty RelStr
for f being set holds
( ( f is Connection of S,T implies f is Connection of S ~ ,T ) & ( f is Connection of S ~ ,T implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S,T ~ ) & ( f is Connection of S,T ~ implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S ~ ,T ~ ) & ( f is Connection of S ~ ,T ~ implies f is Connection of S,T ) )

proof end;

theorem :: YELLOW_7:44

for S, T being non empty Poset
for f1 being Function of S,T
for g1 being Function of T,S
for f2 being Function of (S ~),(T ~)
for g2 being Function of (T ~),(S ~) st f1 = f2 & g1 = g2 holds
( [f1,g1] is Galois iff [g2,f2] is Galois )

proof end;

theorem Th45: :: YELLOW_7:45

for J being set
for D being non empty set
for K being ManySortedSet of J
for F being DoubleIndexedSet of K,D holds doms F = K

proof end;

definition

let J, D be non empty set ;
let K be V8() ManySortedSet of J;
let F be DoubleIndexedSet of K,D;
let j be Element of J;
let k be Element of K . j;
:: original: ..
redefine func F .. (j,k) -> Element of D;
coherence
F .. (j,k) is Element of D

proof end;

end;

theorem :: YELLOW_7:46

for L being non empty RelStr
for J being set
for 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 Th47: :: YELLOW_7:47

for L being complete LATTICE
for J being non empty set
for K being V8() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup <= Inf

proof end;

theorem Th48: :: YELLOW_7:48

for L being complete LATTICE holds
( L is completely-distributive iff for J being non empty set
for K being V8() ManySortedSet of J
for F being DoubleIndexedSet of K,L holds Sup = Inf )

proof end;

theorem Th49: :: YELLOW_7:49

for L being non empty antisymmetric complete RelStr
for F being Function holds
( \\/ (F,L) = //\ (F,(L opp)) & //\ (F,L) = \\/ (F,(L opp)) )

proof end;

theorem Th50: :: YELLOW_7:50

for L being non empty antisymmetric complete RelStr
for F being Function-yielding Function holds
( \// (F,L) = /\\ (F,(L opp)) & /\\ (F,L) = \// (F,(L opp)) )

proof end;

registration

cluster non empty completely-distributive -> non empty complete for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is completely-distributive holds
b₁ is complete by WAYBEL_5:def 3;

end;

registration

cluster non empty V56() finite 1 -element strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded connected up-complete /\-complete distributive V225() completely-distributive for RelStr ;

existence
ex b₁ being 1 -element Poset st
( b₁ is completely-distributive & b₁ is strict )

proof end;

end;

theorem :: YELLOW_7:51

for L being non empty Poset holds
( L is completely-distributive iff L opp is completely-distributive )

proof end;