:: by Grzegorz Bancerek

::

:: Received November 12, 1996

:: Copyright (c) 1996-2021 Association of Mizar Users

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 ) )

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;

registration
end;

registration
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 ) )

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 ) )

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 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))

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))

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

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

L2 is with_suprema

proof 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 )

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 )

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

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) )

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 )

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) )

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 )

for x being set holds

( x is lower Subset of (L opp) iff x is upper Subset of L )

proof end;

theorem :: YELLOW_7:32

theorem :: YELLOW_7:33

theorem :: YELLOW_7:34

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 ~ )

for x, y being Element of L holds

( y is_a_complement_of x iff y ~ is_a_complement_of x ~ )

proof end;

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

definition

let L be non empty RelStr ;

ex b_{1} being Function of L,(L opp) st

for x being Element of L holds b_{1} . x = 'not' x

uniqueness

for b_{1}, b_{2} being Function of L,(L opp) st ( for x being Element of L holds b_{1} . x = 'not' x ) & ( for x being Element of L holds b_{2} . x = 'not' x ) holds

b_{1} = b_{2};

end;
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 for x being Element of L holds it . x = 'not' x;

ex b

for x being Element of L holds b

proof end;

correctness uniqueness

for b

b

proof end;

:: deftheorem Def1 defines ComplMap YELLOW_7:def 1 :

for L being non empty RelStr

for b_{2} being Function of L,(L opp) holds

( b_{2} = ComplMap L iff for x being Element of L holds b_{2} . x = 'not' x );

for L being non empty RelStr

for b

( b

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

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 ) )

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 ) )

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 ) )

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 ) )

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 )

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

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

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

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

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

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 )

( 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)) )

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)) )

for F being Function-yielding Function holds

( \// (F,L) = /\\ (F,(L opp)) & /\\ (F,L) = \// (F,(L opp)) )

proof end;

registration

coherence

for b_{1} being non empty RelStr st b_{1} is completely-distributive holds

b_{1} is complete
by WAYBEL_5:def 3;

end;
for b

b

registration

ex b_{1} being 1 -element Poset st

( b_{1} is completely-distributive & b_{1} is strict )
end;

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

( b

proof end;

theorem :: YELLOW_7:51

for L being non empty Poset holds

( L is completely-distributive iff L opp is completely-distributive )

( L is completely-distributive iff L opp is completely-distributive )

proof end;

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