:: YELLOW_7 semantic presentation

notation
let c1 be RelStr ;
synonym c1 opp for c1 ~ ;
end;

theorem Th1: :: YELLOW_7:1
for b1 being RelStr
for b2, b3 being Element of (b1 opp ) holds
( b2 <= b3 iff ~ b2 >= ~ b3 )
proof end;

theorem Th2: :: YELLOW_7:2
for b1 being RelStr
for b2 being Element of b1
for b3 being Element of (b1 opp ) holds
( ( b2 <= ~ b3 implies b2 ~ >= b3 ) & ( b2 ~ >= b3 implies b2 <= ~ b3 ) & ( b2 >= ~ b3 implies b2 ~ <= b3 ) & ( b2 ~ <= b3 implies b2 >= ~ b3 ) )
proof end;

theorem Th3: :: YELLOW_7:3
for b1 being RelStr holds
( b1 is empty iff b1 opp is empty )
proof end;

theorem Th4: :: YELLOW_7:4
for b1 being RelStr holds
( b1 is reflexive iff b1 opp is reflexive )
proof end;

theorem Th5: :: YELLOW_7:5
for b1 being RelStr holds
( b1 is antisymmetric iff b1 opp is antisymmetric )
proof end;

theorem Th6: :: YELLOW_7:6
for b1 being RelStr holds
( b1 is transitive iff b1 opp is transitive )
proof end;

theorem Th7: :: YELLOW_7:7
for b1 being non empty RelStr holds
( b1 is connected iff b1 opp is connected )
proof end;

registration
let c1 be reflexive RelStr ;
cluster a1 opp -> reflexive ;
coherence
c1 opp is reflexive
by Th4;
end;

registration
let c1 be transitive RelStr ;
cluster a1 opp -> transitive ;
coherence
c1 opp is transitive
by Th6;
end;

registration
let c1 be antisymmetric RelStr ;
cluster a1 opp -> antisymmetric ;
coherence
c1 opp is antisymmetric
by Th5;
end;

registration
let c1 be non empty connected RelStr ;
cluster a1 opp -> connected ;
coherence
c1 opp is connected
by Th7;
end;

theorem Th8: :: YELLOW_7:8
for b1 being RelStr
for b2 being Element of b1
for b3 being set holds
( ( b2 is_<=_than b3 implies b2 ~ is_>=_than b3 ) & ( b2 ~ is_>=_than b3 implies b2 is_<=_than b3 ) & ( b2 is_>=_than b3 implies b2 ~ is_<=_than b3 ) & ( b2 ~ is_<=_than b3 implies b2 is_>=_than b3 ) )
proof end;

theorem Th9: :: YELLOW_7:9
for b1 being RelStr
for b2 being Element of (b1 opp )
for b3 being set holds
( ( b2 is_<=_than b3 implies ~ b2 is_>=_than b3 ) & ( ~ b2 is_>=_than b3 implies b2 is_<=_than b3 ) & ( b2 is_>=_than b3 implies ~ b2 is_<=_than b3 ) & ( ~ b2 is_<=_than b3 implies b2 is_>=_than b3 ) )
proof end;

theorem Th10: :: YELLOW_7:10
for b1 being RelStr
for b2 being set holds
( ex_sup_of b2,b1 iff ex_inf_of b2,b1 opp )
proof end;

theorem Th11: :: YELLOW_7:11
for b1 being RelStr
for b2 being set holds
( ex_sup_of b2,b1 opp iff ex_inf_of b2,b1 )
proof end;

theorem Th12: :: YELLOW_7:12
for b1 being non empty RelStr
for b2 being set st ( ex_sup_of b2,b1 or ex_inf_of b2,b1 opp ) holds
"\/" b2,b1 = "/\" b2,(b1 opp )
proof end;

theorem Th13: :: YELLOW_7:13
for b1 being non empty RelStr
for b2 being set st ( ex_inf_of b2,b1 or ex_sup_of b2,b1 opp ) holds
"/\" b2,b1 = "\/" b2,(b1 opp )
proof end;

theorem Th14: :: YELLOW_7:14
for b1, b2 being RelStr st RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of b2,the InternalRel of b2 #) & b1 is with_infima holds
b2 is with_infima
proof end;

theorem Th15: :: YELLOW_7:15
for b1, b2 being RelStr st RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of b2,the InternalRel of b2 #) & b1 is with_suprema holds
b2 is with_suprema
proof end;

theorem Th16: :: YELLOW_7:16
for b1 being RelStr holds
( b1 is with_infima iff b1 opp is with_suprema )
proof end;

theorem Th17: :: YELLOW_7:17
for b1 being non empty RelStr holds
( b1 is complete iff b1 opp is complete )
proof end;

registration
let c1 be with_infima RelStr ;
cluster a1 opp -> with_suprema ;
coherence
c1 opp is with_suprema
by Th16;
end;

registration
let c1 be with_suprema RelStr ;
cluster a1 opp -> with_infima ;
coherence
c1 opp is with_infima
by LATTICE3:10;
end;

registration
let c1 be non empty complete RelStr ;
cluster a1 opp -> with_suprema with_infima complete ;
coherence
c1 opp is complete
by Th17;
end;

theorem Th18: :: YELLOW_7:18
for b1 being non empty RelStr
for b2 being Subset of b1
for b3 being Subset of (b1 opp ) st b2 = b3 holds
( fininfs b2 = finsups b3 & finsups b2 = fininfs b3 )
proof end;

theorem Th19: :: YELLOW_7:19
for b1 being RelStr
for b2 being Subset of b1
for b3 being Subset of (b1 opp ) st b2 = b3 holds
( downarrow b2 = uparrow b3 & uparrow b2 = downarrow b3 )
proof end;

theorem Th20: :: YELLOW_7:20
for b1 being non empty RelStr
for b2 being Element of b1
for b3 being Element of (b1 opp ) st b2 = b3 holds
( downarrow b2 = uparrow b3 & uparrow b2 = downarrow b3 ) by Th19;

theorem Th21: :: YELLOW_7:21
for b1 being with_infima Poset
for b2, b3 being Element of b1 holds b2 "/\" b3 = (b2 ~ ) "\/" (b3 ~ )
proof end;

theorem Th22: :: YELLOW_7:22
for b1 being with_infima Poset
for b2, b3 being Element of (b1 opp ) holds (~ b2) "/\" (~ b3) = b2 "\/" b3
proof end;

theorem Th23: :: YELLOW_7:23
for b1 being with_suprema Poset
for b2, b3 being Element of b1 holds b2 "\/" b3 = (b2 ~ ) "/\" (b3 ~ )
proof end;

theorem Th24: :: YELLOW_7:24
for b1 being with_suprema Poset
for b2, b3 being Element of (b1 opp ) holds (~ b2) "\/" (~ b3) = b2 "/\" b3
proof end;

theorem Th25: :: YELLOW_7:25
for b1 being LATTICE holds
( b1 is distributive iff b1 opp is distributive )
proof end;

registration
let c1 be distributive LATTICE;
cluster a1 opp -> with_suprema with_infima distributive ;
coherence
c1 opp is distributive
by Th25;
end;

theorem Th26: :: YELLOW_7:26
for b1 being RelStr
for b2 being set holds
( b2 is directed Subset of b1 iff b2 is filtered Subset of (b1 opp ) )
proof end;

theorem Th27: :: YELLOW_7:27
for b1 being RelStr
for b2 being set holds
( b2 is directed Subset of (b1 opp ) iff b2 is filtered Subset of b1 )
proof end;

theorem Th28: :: YELLOW_7:28
for b1 being RelStr
for b2 being set holds
( b2 is lower Subset of b1 iff b2 is upper Subset of (b1 opp ) )
proof end;

theorem Th29: :: YELLOW_7:29
for b1 being RelStr
for b2 being set holds
( b2 is lower Subset of (b1 opp ) iff b2 is upper Subset of b1 )
proof end;

theorem Th30: :: YELLOW_7:30
for b1 being RelStr holds
( b1 is lower-bounded iff b1 opp is upper-bounded )
proof end;

theorem Th31: :: YELLOW_7:31
for b1 being RelStr holds
( b1 opp is lower-bounded iff b1 is upper-bounded )
proof end;

theorem Th32: :: YELLOW_7:32
for b1 being RelStr holds
( b1 is bounded iff b1 opp is bounded )
proof end;

theorem Th33: :: YELLOW_7:33
for b1 being non empty antisymmetric lower-bounded RelStr holds
( (Bottom b1) ~ = Top (b1 opp ) & ~ (Top (b1 opp )) = Bottom b1 )
proof end;

theorem Th34: :: YELLOW_7:34
for b1 being non empty antisymmetric upper-bounded RelStr holds
( (Top b1) ~ = Bottom (b1 opp ) & ~ (Bottom (b1 opp )) = Top b1 )
proof end;

theorem Th35: :: YELLOW_7:35
for b1 being bounded LATTICE
for b2, b3 being Element of b1 holds
( b3 is_a_complement_of b2 iff b3 ~ is_a_complement_of b2 ~ )
proof end;

theorem Th36: :: YELLOW_7:36
for b1 being bounded LATTICE holds
( b1 is complemented iff b1 opp is complemented )
proof end;

registration
let c1 be lower-bounded RelStr ;
cluster a1 opp -> upper-bounded ;
coherence
c1 opp is upper-bounded
by Th30;
end;

registration
let c1 be upper-bounded RelStr ;
cluster a1 opp -> lower-bounded ;
coherence
c1 opp is lower-bounded
by Th31;
end;

registration
let c1 be bounded complemented LATTICE;
cluster a1 opp -> with_suprema with_infima lower-bounded upper-bounded complemented ;
coherence
c1 opp is complemented
by Th36;
end;

theorem Th37: :: YELLOW_7:37
for b1 being Boolean LATTICE
for b2 being Element of b1 holds 'not' (b2 ~ ) = 'not' b2
proof end;

definition
let c1 be non empty RelStr ;
func ComplMap c1 -> Function of a1,(a1 opp ) means :Def1: :: YELLOW_7:def 1
for b1 being Element of a1 holds a2 . b1 = 'not' b1;
existence
ex b1 being Function of c1,(c1 opp ) st
for b2 being Element of c1 holds b1 . b2 = 'not' b2
proof end;
correctness
uniqueness
for b1, b2 being Function of c1,(c1 opp ) st ( for b3 being Element of c1 holds b1 . b3 = 'not' b3 ) & ( for b3 being Element of c1 holds b2 . b3 = 'not' b3 ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def1 defines ComplMap YELLOW_7:def 1 :
for b1 being non empty RelStr
for b2 being Function of b1,(b1 opp ) holds
( b2 = ComplMap b1 iff for b3 being Element of b1 holds b2 . b3 = 'not' b3 );

registration
let c1 be Boolean LATTICE;
cluster ComplMap a1 -> V6 ;
coherence
ComplMap c1 is one-to-one
proof end;
end;

registration
let c1 be Boolean LATTICE;
cluster ComplMap a1 -> V6 isomorphic ;
coherence
ComplMap c1 is isomorphic
proof end;
end;

theorem Th38: :: YELLOW_7:38
for b1 being Boolean LATTICE holds b1,b1 opp are_isomorphic
proof end;

theorem Th39: :: YELLOW_7:39
for b1, b2 being non empty RelStr
for b3 being set holds
( ( b3 is Function of b1,b2 implies b3 is Function of (b1 opp ),b2 ) & ( b3 is Function of (b1 opp ),b2 implies b3 is Function of b1,b2 ) & ( b3 is Function of b1,b2 implies b3 is Function of b1,(b2 opp ) ) & ( b3 is Function of b1,(b2 opp ) implies b3 is Function of b1,b2 ) & ( b3 is Function of b1,b2 implies b3 is Function of (b1 opp ),(b2 opp ) ) & ( b3 is Function of (b1 opp ),(b2 opp ) implies b3 is Function of b1,b2 ) ) ;

theorem Th40: :: YELLOW_7:40
for b1, b2 being non empty RelStr
for b3 being Function of b1,b2
for b4 being Function of b1,(b2 opp ) st b3 = b4 holds
( ( b3 is monotone implies b4 is antitone ) & ( b4 is antitone implies b3 is monotone ) & ( b3 is antitone implies b4 is monotone ) & ( b4 is monotone implies b3 is antitone ) )
proof end;

theorem Th41: :: YELLOW_7:41
for b1, b2 being non empty RelStr
for b3 being Function of b1,(b2 opp )
for b4 being Function of (b1 opp ),b2 st b3 = b4 holds
( ( b3 is monotone implies b4 is monotone ) & ( b4 is monotone implies b3 is monotone ) & ( b3 is antitone implies b4 is antitone ) & ( b4 is antitone implies b3 is antitone ) )
proof end;

theorem Th42: :: YELLOW_7:42
for b1, b2 being non empty RelStr
for b3 being Function of b1,b2
for b4 being Function of (b1 opp ),(b2 opp ) st b3 = b4 holds
( ( b3 is monotone implies b4 is monotone ) & ( b4 is monotone implies b3 is monotone ) & ( b3 is antitone implies b4 is antitone ) & ( b4 is antitone implies b3 is antitone ) )
proof end;

theorem Th43: :: YELLOW_7:43
for b1, b2 being non empty RelStr
for b3 being set holds
( ( b3 is Connection of b1,b2 implies b3 is Connection of b1 ~ ,b2 ) & ( b3 is Connection of b1 ~ ,b2 implies b3 is Connection of b1,b2 ) & ( b3 is Connection of b1,b2 implies b3 is Connection of b1,b2 ~ ) & ( b3 is Connection of b1,b2 ~ implies b3 is Connection of b1,b2 ) & ( b3 is Connection of b1,b2 implies b3 is Connection of b1 ~ ,b2 ~ ) & ( b3 is Connection of b1 ~ ,b2 ~ implies b3 is Connection of b1,b2 ) )
proof end;

theorem Th44: :: YELLOW_7:44
for b1, b2 being non empty Poset
for b3 being Function of b1,b2
for b4 being Function of b2,b1
for b5 being Function of (b1 ~ ),(b2 ~ )
for b6 being Function of (b2 ~ ),(b1 ~ ) st b3 = b5 & b4 = b6 holds
( [b3,b4] is Galois iff [b6,b5] is Galois )
proof end;

theorem Th45: :: YELLOW_7:45
for b1 being set
for b2 being non empty set
for b3 being ManySortedSet of b1
for b4 being DoubleIndexedSet of b3,b2 holds doms b4 = b3
proof end;

definition
let c1, c2 be non empty set ;
let c3 be V3 ManySortedSet of c1;
let c4 be DoubleIndexedSet of c3,c2;
let c5 be Element of c1;
let c6 be Element of c3 . c5;
redefine func .. as c4 .. c5,c6 -> Element of a2;
coherence
c4 .. c5,c6 is Element of c2
proof end;
end;

theorem Th46: :: YELLOW_7:46
for b1 being non empty RelStr
for b2 being set
for b3 being ManySortedSet of b2
for b4 being set holds
( b4 is DoubleIndexedSet of b3,b1 iff b4 is DoubleIndexedSet of b3,(b1 opp ) ) ;

theorem Th47: :: YELLOW_7:47
for b1 being complete LATTICE
for b2 being non empty set
for b3 being V3 ManySortedSet of b2
for b4 being DoubleIndexedSet of b3,b1 holds Sup <= Inf
proof end;

theorem Th48: :: YELLOW_7:48
for b1 being complete LATTICE holds
( b1 is completely-distributive iff for b2 being non empty set
for b3 being V3 ManySortedSet of b2
for b4 being DoubleIndexedSet of b3,b1 holds Sup = Inf )
proof end;

theorem Th49: :: YELLOW_7:49
for b1 being non empty antisymmetric complete RelStr
for b2 being Function holds
( \\/ b2,b1 = //\ b2,(b1 opp ) & //\ b2,b1 = \\/ b2,(b1 opp ) )
proof end;

theorem Th50: :: YELLOW_7:50
for b1 being non empty antisymmetric complete RelStr
for b2 being Function-yielding Function holds
( \// b2,b1 = /\\ b2,(b1 opp ) & /\\ b2,b1 = \// b2,(b1 opp ) )
proof end;

registration
cluster non empty completely-distributive -> non empty complete RelStr ;
coherence
for b1 being non empty RelStr st b1 is completely-distributive holds
b1 is complete
by WAYBEL_5:def 3;
end;

registration
cluster non empty strict complete completely-distributive trivial RelStr ;
existence
ex b1 being non empty Poset st
( b1 is completely-distributive & b1 is trivial & b1 is strict )
proof end;
end;

theorem Th51: :: YELLOW_7:51
for b1 being non empty Poset holds
( b1 is completely-distributive iff b1 opp is completely-distributive )
proof end;