:: YELLOW_7 semantic presentation

notation

let c₁ be RelStr ;
synonym c₁ opp for c₁ ~ ;

end;

theorem Th1: :: YELLOW_7:1

for b₁ being RelStr
for b₂, b₃ being Element of (b₁ opp ) holds
( b₂ <= b₃ iff ~ b₂ >= ~ b₃ )

proof end;

theorem Th2: :: YELLOW_7:2

for b₁ being RelStr
for b₂ being Element of b₁
for b₃ being Element of (b₁ opp ) holds
( ( b₂ <= ~ b₃ implies b₂ ~ >= b₃ ) & ( b₂ ~ >= b₃ implies b₂ <= ~ b₃ ) & ( b₂ >= ~ b₃ implies b₂ ~ <= b₃ ) & ( b₂ ~ <= b₃ implies b₂ >= ~ b₃ ) )

proof end;

theorem Th3: :: YELLOW_7:3

for b₁ being RelStr holds
( b₁ is empty iff b₁ opp is empty )

proof end;

theorem Th4: :: YELLOW_7:4

for b₁ being RelStr holds
( b₁ is reflexive iff b₁ opp is reflexive )

proof end;

theorem Th5: :: YELLOW_7:5

for b₁ being RelStr holds
( b₁ is antisymmetric iff b₁ opp is antisymmetric )

proof end;

theorem Th6: :: YELLOW_7:6

for b₁ being RelStr holds
( b₁ is transitive iff b₁ opp is transitive )

proof end;

theorem Th7: :: YELLOW_7:7

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

proof end;

registration

let c₁ be reflexive RelStr ;
cluster a₁ opp -> reflexive ;
coherence by Th4;

end;

registration

let c₁ be transitive RelStr ;
cluster a₁ opp -> transitive ;
coherence by Th6;

end;

registration

let c₁ be antisymmetric RelStr ;
cluster a₁ opp -> antisymmetric ;
coherence by Th5;

end;

registration

let c₁ be non empty connected RelStr ;
cluster a₁ opp -> connected ;
coherence by Th7;

end;

theorem Th8: :: YELLOW_7:8

for b₁ being RelStr
for b₂ being Element of b₁
for b₃ being set holds
( ( b₂ is_<=_than b₃ implies b₂ ~ is_>=_than b₃ ) & ( b₂ ~ is_>=_than b₃ implies b₂ is_<=_than b₃ ) & ( b₂ is_>=_than b₃ implies b₂ ~ is_<=_than b₃ ) & ( b₂ ~ is_<=_than b₃ implies b₂ is_>=_than b₃ ) )

proof end;

theorem Th9: :: YELLOW_7:9

for b₁ being RelStr
for b₂ being Element of (b₁ opp )
for b₃ being set holds
( ( b₂ is_<=_than b₃ implies ~ b₂ is_>=_than b₃ ) & ( ~ b₂ is_>=_than b₃ implies b₂ is_<=_than b₃ ) & ( b₂ is_>=_than b₃ implies ~ b₂ is_<=_than b₃ ) & ( ~ b₂ is_<=_than b₃ implies b₂ is_>=_than b₃ ) )

proof end;

theorem Th10: :: YELLOW_7:10

for b₁ being RelStr
for b₂ being set holds
( ex_sup_of b₂,b₁ iff ex_inf_of b₂,b₁ opp )

proof end;

theorem Th11: :: YELLOW_7:11

for b₁ being RelStr
for b₂ being set holds
( ex_sup_of b₂,b₁ opp iff ex_inf_of b₂,b₁ )

proof end;

theorem Th12: :: YELLOW_7:12

for b₁ being non empty RelStr
for b₂ being set st ( ex_sup_of b₂,b₁ or ex_inf_of b₂,b₁ opp ) holds
"\/" b₂,b₁ = "/\" b₂,(b₁ opp )

proof end;

theorem Th13: :: YELLOW_7:13

for b₁ being non empty RelStr
for b₂ being set st ( ex_inf_of b₂,b₁ or ex_sup_of b₂,b₁ opp ) holds
"/\" b₂,b₁ = "\/" b₂,(b₁ opp )

proof end;

theorem Th14: :: YELLOW_7:14

for b₁, b₂ being RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₁ is with_infima holds
b₂ is with_infima

proof end;

theorem Th15: :: YELLOW_7:15

for b₁, b₂ being RelStr st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₁ is with_suprema holds
b₂ is with_suprema

proof end;

theorem Th16: :: YELLOW_7:16

for b₁ being RelStr holds
( b₁ is with_infima iff b₁ opp is with_suprema )

proof end;

theorem Th17: :: YELLOW_7:17

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

proof end;

registration

let c₁ be with_infima RelStr ;
cluster a₁ opp -> with_suprema ;
coherence by Th16;

end;

registration

let c₁ be with_suprema RelStr ;
cluster a₁ opp -> with_infima ;
coherence by LATTICE3:10;

end;

registration

let c₁ be non empty complete RelStr ;
cluster a₁ opp -> with_suprema with_infima complete ;
coherence by Th17;

end;

theorem Th18: :: YELLOW_7:18

for b₁ being non empty RelStr
for b₂ being Subset of b₁
for b₃ being Subset of (b₁ opp ) st b₂ = b₃ holds
( fininfs b₂ = finsups b₃ & finsups b₂ = fininfs b₃ )

proof end;

theorem Th19: :: YELLOW_7:19

for b₁ being RelStr
for b₂ being Subset of b₁
for b₃ being Subset of (b₁ opp ) st b₂ = b₃ holds
( downarrow b₂ = uparrow b₃ & uparrow b₂ = downarrow b₃ )

proof end;

theorem Th20: :: YELLOW_7:20

for b₁ being non empty RelStr
for b₂ being Element of b₁
for b₃ being Element of (b₁ opp ) st b₂ = b₃ holds
( downarrow b₂ = uparrow b₃ & uparrow b₂ = downarrow b₃ ) by Th19;

theorem Th21: :: YELLOW_7:21

for b₁ being with_infima Poset
for b₂, b₃ being Element of b₁ holds b₂ "/\" b₃ = (b₂ ~ ) "\/" (b₃ ~ )

proof end;

theorem Th22: :: YELLOW_7:22

for b₁ being with_infima Poset
for b₂, b₃ being Element of (b₁ opp ) holds (~ b₂) "/\" (~ b₃) = b₂ "\/" b₃

proof end;

theorem Th23: :: YELLOW_7:23

for b₁ being with_suprema Poset
for b₂, b₃ being Element of b₁ holds b₂ "\/" b₃ = (b₂ ~ ) "/\" (b₃ ~ )

proof end;

theorem Th24: :: YELLOW_7:24

for b₁ being with_suprema Poset
for b₂, b₃ being Element of (b₁ opp ) holds (~ b₂) "\/" (~ b₃) = b₂ "/\" b₃

proof end;

theorem Th25: :: YELLOW_7:25

for b₁ being LATTICE holds
( b₁ is distributive iff b₁ opp is distributive )

proof end;

registration

let c₁ be distributive LATTICE;
cluster a₁ opp -> with_suprema with_infima distributive ;
coherence by Th25;

end;

theorem Th26: :: YELLOW_7:26

for b₁ being RelStr
for b₂ being set holds
( b₂ is directed Subset of b₁ iff b₂ is filtered Subset of (b₁ opp ) )

proof end;

theorem Th27: :: YELLOW_7:27

for b₁ being RelStr
for b₂ being set holds
( b₂ is directed Subset of (b₁ opp ) iff b₂ is filtered Subset of b₁ )

proof end;

theorem Th28: :: YELLOW_7:28

for b₁ being RelStr
for b₂ being set holds
( b₂ is lower Subset of b₁ iff b₂ is upper Subset of (b₁ opp ) )

proof end;

theorem Th29: :: YELLOW_7:29

for b₁ being RelStr
for b₂ being set holds
( b₂ is lower Subset of (b₁ opp ) iff b₂ is upper Subset of b₁ )

proof end;

theorem Th30: :: YELLOW_7:30

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

proof end;

theorem Th31: :: YELLOW_7:31

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

proof end;

theorem Th32: :: YELLOW_7:32

for b₁ being RelStr holds
( b₁ is bounded iff b₁ opp is bounded )

proof end;

theorem Th33: :: YELLOW_7:33

for b₁ being non empty antisymmetric lower-bounded RelStr holds
( (Bottom b₁) ~ = Top (b₁ opp ) & ~ (Top (b₁ opp )) = Bottom b₁ )

proof end;

theorem Th34: :: YELLOW_7:34

for b₁ being non empty antisymmetric upper-bounded RelStr holds
( (Top b₁) ~ = Bottom (b₁ opp ) & ~ (Bottom (b₁ opp )) = Top b₁ )

proof end;

theorem Th35: :: YELLOW_7:35

for b₁ being bounded LATTICE
for b₂, b₃ being Element of b₁ holds
( b₃ is_a_complement_of b₂ iff b₃ ~ is_a_complement_of b₂ ~ )

proof end;

theorem Th36: :: YELLOW_7:36

for b₁ being bounded LATTICE holds
( b₁ is complemented iff b₁ opp is complemented )

proof end;

registration

let c₁ be lower-bounded RelStr ;
cluster a₁ opp -> upper-bounded ;
coherence by Th30;

end;

registration

let c₁ be upper-bounded RelStr ;
cluster a₁ opp -> lower-bounded ;
coherence by Th31;

end;

registration

let c₁ be bounded complemented LATTICE;
cluster a₁ opp -> with_suprema with_infima lower-bounded upper-bounded complemented ;
coherence by Th36;

end;

theorem Th37: :: YELLOW_7:37

for b₁ being Boolean LATTICE
for b₂ being Element of b₁ holds 'not' (b₂ ~ ) = 'not' b₂

proof end;

definition

let c₁ be non empty RelStr ;
func ComplMap c₁ -> Function of a₁,(a₁ opp ) means :Def1: :: YELLOW_7:def 1
for b₁ being Element of a₁ holds a₂ . b₁ = 'not' b₁;
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def1 defines ComplMap YELLOW_7:def 1 :

registration

let c₁ be Boolean LATTICE;
cluster ComplMap a₁ -> V6 ;
coherence

proof end;

end;

registration

let c₁ be Boolean LATTICE;
cluster ComplMap a₁ -> V6 isomorphic ;
coherence

proof end;

end;

theorem Th38: :: YELLOW_7:38

for b₁ being Boolean LATTICE holds b₁,b₁ opp are_isomorphic

proof end;

theorem Th39: :: YELLOW_7:39

for b₁, b₂ being non empty RelStr
for b₃ being set holds
( ( b₃ is Function of b₁,b₂ implies b₃ is Function of (b₁ opp ),b₂ ) & ( b₃ is Function of (b₁ opp ),b₂ implies b₃ is Function of b₁,b₂ ) & ( b₃ is Function of b₁,b₂ implies b₃ is Function of b₁,(b₂ opp ) ) & ( b₃ is Function of b₁,(b₂ opp ) implies b₃ is Function of b₁,b₂ ) & ( b₃ is Function of b₁,b₂ implies b₃ is Function of (b₁ opp ),(b₂ opp ) ) & ( b₃ is Function of (b₁ opp ),(b₂ opp ) implies b₃ is Function of b₁,b₂ ) ) ;

theorem Th40: :: YELLOW_7:40

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂
for b₄ being Function of b₁,(b₂ opp ) st b₃ = b₄ holds
( ( b₃ is monotone implies b₄ is antitone ) & ( b₄ is antitone implies b₃ is monotone ) & ( b₃ is antitone implies b₄ is monotone ) & ( b₄ is monotone implies b₃ is antitone ) )

proof end;

theorem Th41: :: YELLOW_7:41

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,(b₂ opp )
for b₄ being Function of (b₁ opp ),b₂ st b₃ = b₄ holds
( ( b₃ is monotone implies b₄ is monotone ) & ( b₄ is monotone implies b₃ is monotone ) & ( b₃ is antitone implies b₄ is antitone ) & ( b₄ is antitone implies b₃ is antitone ) )

proof end;

theorem Th42: :: YELLOW_7:42

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂
for b₄ being Function of (b₁ opp ),(b₂ opp ) st b₃ = b₄ holds
( ( b₃ is monotone implies b₄ is monotone ) & ( b₄ is monotone implies b₃ is monotone ) & ( b₃ is antitone implies b₄ is antitone ) & ( b₄ is antitone implies b₃ is antitone ) )

proof end;

theorem Th43: :: YELLOW_7:43

for b₁, b₂ being non empty RelStr
for b₃ being set holds
( ( b₃ is Connection of b₁,b₂ implies b₃ is Connection of b₁ ~ ,b₂ ) & ( b₃ is Connection of b₁ ~ ,b₂ implies b₃ is Connection of b₁,b₂ ) & ( b₃ is Connection of b₁,b₂ implies b₃ is Connection of b₁,b₂ ~ ) & ( b₃ is Connection of b₁,b₂ ~ implies b₃ is Connection of b₁,b₂ ) & ( b₃ is Connection of b₁,b₂ implies b₃ is Connection of b₁ ~ ,b₂ ~ ) & ( b₃ is Connection of b₁ ~ ,b₂ ~ implies b₃ is Connection of b₁,b₂ ) )

proof end;

theorem Th44: :: YELLOW_7:44

for b₁, b₂ being non empty Poset
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁
for b₅ being Function of (b₁ ~ ),(b₂ ~ )
for b₆ being Function of (b₂ ~ ),(b₁ ~ ) st b₃ = b₅ & b₄ = b₆ holds
( [b₃,b₄] is Galois iff [b₆,b₅] is Galois )

proof end;

theorem Th45: :: YELLOW_7:45

for b₁ being set
for b₂ being non empty set
for b₃ being ManySortedSet of b₁
for b₄ being DoubleIndexedSet of b₃,b₂ holds doms b₄ = b₃

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be V3 ManySortedSet of c₁;
let c₄ be DoubleIndexedSet of c₃,c₂;
let c₅ be Element of c₁;
let c₆ be Element of c₃ . c₅;
redefine func .. as c₄ .. c₅,c₆ -> Element of a₂;
coherence

proof end;

end;

theorem Th46: :: YELLOW_7:46

for b₁ being non empty RelStr
for b₂ being set
for b₃ being ManySortedSet of b₂
for b₄ being set holds
( b₄ is DoubleIndexedSet of b₃,b₁ iff b₄ is DoubleIndexedSet of b₃,(b₁ opp ) ) ;

theorem Th47: :: YELLOW_7:47

for b₁ being complete LATTICE
for b₂ being non empty set
for b₃ being V3 ManySortedSet of b₂
for b₄ being DoubleIndexedSet of b₃,b₁ holds Sup <= Inf

proof end;

theorem Th48: :: YELLOW_7:48

for b₁ being complete LATTICE holds
( b₁ is completely-distributive iff for b₂ being non empty set
for b₃ being V3 ManySortedSet of b₂
for b₄ being DoubleIndexedSet of b₃,b₁ holds Sup = Inf )

proof end;

theorem Th49: :: YELLOW_7:49

for b₁ being non empty antisymmetric complete RelStr
for b₂ being Function holds
( \\/ b₂,b₁ = //\ b₂,(b₁ opp ) & //\ b₂,b₁ = \\/ b₂,(b₁ opp ) )

proof end;

theorem Th50: :: YELLOW_7:50

for b₁ being non empty antisymmetric complete RelStr
for b₂ being Function-yielding Function holds
( \// b₂,b₁ = /\\ b₂,(b₁ opp ) & /\\ b₂,b₁ = \// b₂,(b₁ opp ) )

proof end;

registration

cluster non empty completely-distributive -> non empty complete RelStr ;
coherence by WAYBEL_5:def 3;

end;

registration

cluster non empty strict complete completely-distributive trivial RelStr ;
existence

proof end;

end;

theorem Th51: :: YELLOW_7:51

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

proof end;