let C be complete Lattice; ( C is \/-distributive iff for X being set
for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) )
thus
( C is \/-distributive implies for X being set
for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) )
( ( for X being set
for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C) ) implies C is \/-distributive )proof
assume A1:
for
X being
set for
a,
b,
c being
Element of
C st
X is_less_than a & ( for
d being
Element of
C st
X is_less_than d holds
a [= d ) &
{ (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for
d being
Element of
C st
{ (b "/\" b9) where b9 is Element of C : b9 in X } is_less_than d holds
c [= d ) holds
b "/\" a [= c
;
LATTICE3:def 19 for X being set
for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C)
let X be
set ;
for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C)let a be
Element of
C;
a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C)
set Y =
{ (a "/\" b) where b is Element of C : b in X } ;
A2:
X is_less_than "\/" (
X,
C)
by Def21;
A3:
for
d being
Element of
C st
X is_less_than d holds
"\/" (
X,
C)
[= d
by Def21;
A4:
{ (a "/\" b) where b is Element of C : b in X } is_less_than "\/" (
{ (a "/\" b) where b is Element of C : b in X } ,
C)
by Def21;
for
d being
Element of
C st
{ (a "/\" b) where b is Element of C : b in X } is_less_than d holds
"\/" (
{ (a "/\" b) where b is Element of C : b in X } ,
C)
[= d
by Def21;
hence
a "/\" ("\/" (X,C)) [= "\/" (
{ (a "/\" b) where b is Element of C : b in X } ,
C)
by A1, A2, A3, A4;
verum
end;
assume A5:
for X being set
for a being Element of C holds a "/\" ("\/" (X,C)) [= "\/" ( { (a "/\" b) where b is Element of C : b in X } ,C)
; C is \/-distributive
let X be set ; LATTICE3:def 19 for a, b, c being Element of C st X is_less_than a & ( for d being Element of C st X is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than d holds
c [= d ) holds
b "/\" a [= c
let a, b, c be Element of C; ( X is_less_than a & ( for d being Element of C st X is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than d holds
c [= d ) implies b "/\" a [= c )
assume A6:
( X is_less_than a & ( for d being Element of C st X is_less_than d holds
a [= d ) & { (b "/\" a9) where a9 is Element of C : a9 in X } is_less_than c & ( for d being Element of C st { (b "/\" b9) where b9 is Element of C : b9 in X } is_less_than d holds
c [= d ) )
; b "/\" a [= c
then A7:
a = "\/" (X,C)
by Def21;
c = "\/" ( { (b "/\" a9) where a9 is Element of C : a9 in X } ,C)
by A6, Def21;
hence
b "/\" a [= c
by A5, A7; verum