:: WAYBEL_0 semantic presentation
begin
definition
let L be RelStr ;
let X be Subset of L;
attrX is directed means :Def1: :: WAYBEL_0:def 1
for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x <= z & y <= z );
attrX is filtered means :Def2: :: WAYBEL_0:def 2
for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & z <= x & z <= y );
end;
:: deftheorem Def1 defines directed WAYBEL_0:def_1_:_
for L being RelStr
for X being Subset of L holds
( X is directed iff for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x <= z & y <= z ) );
:: deftheorem Def2 defines filtered WAYBEL_0:def_2_:_
for L being RelStr
for X being Subset of L holds
( X is filtered iff for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & z <= x & z <= y ) );
theorem Th1: :: WAYBEL_0:1
for L being non empty transitive RelStr
for X being Subset of L holds
( ( not X is empty & X is directed ) iff for Y being finite Subset of X ex x being Element of L st
( x in X & x is_>=_than Y ) )
proof
let L be non empty transitive RelStr ; ::_thesis: for X being Subset of L holds
( ( not X is empty & X is directed ) iff for Y being finite Subset of X ex x being Element of L st
( x in X & x is_>=_than Y ) )
let X be Subset of L; ::_thesis: ( ( not X is empty & X is directed ) iff for Y being finite Subset of X ex x being Element of L st
( x in X & x is_>=_than Y ) )
hereby ::_thesis: ( ( for Y being finite Subset of X ex x being Element of L st
( x in X & x is_>=_than Y ) ) implies ( not X is empty & X is directed ) )
assume not X is empty ; ::_thesis: ( X is directed implies for Y being finite Subset of X holds S1[Y] )
then reconsider X9 = X as non empty set ;
assume A1: X is directed ; ::_thesis: for Y being finite Subset of X holds S1[Y]
let Y be finite Subset of X; ::_thesis: S1[Y]
defpred S1[ set ] means ex x being Element of L st
( x in X & x is_>=_than $1 );
A2: Y is finite ;
set x = the Element of X9;
the Element of X9 in X ;
then reconsider x = the Element of X9 as Element of L ;
x is_>=_than {} by YELLOW_0:6;
then A3: S1[ {} ] ;
A4: now__::_thesis:_for_x,_B_being_set_st_x_in_Y_&_B_c=_Y_&_S1[B]_holds_
S1[B_\/_{x}]
let x, B be set ; ::_thesis: ( x in Y & B c= Y & S1[B] implies S1[B \/ {x}] )
assume that
A5: x in Y and
B c= Y ; ::_thesis: ( S1[B] implies S1[B \/ {x}] )
assume S1[B] ; ::_thesis: S1[B \/ {x}]
then consider y being Element of L such that
A6: y in X and
A7: y is_>=_than B ;
x in X by A5;
then reconsider x9 = x as Element of L ;
consider z being Element of L such that
A8: z in X and
A9: x9 <= z and
A10: y <= z by A1, A5, A6, Def1;
thus S1[B \/ {x}] ::_thesis: verum
proof
take z ; ::_thesis: ( z in X & z is_>=_than B \/ {x} )
thus z in X by A8; ::_thesis: z is_>=_than B \/ {x}
let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in B \/ {x} or a <= z )
reconsider a9 = a as Element of L ;
assume a in B \/ {x} ; ::_thesis: a <= z
then ( a9 in B or a9 in {x} ) by XBOOLE_0:def_3;
then ( y >= a9 or a9 = x ) by A7, LATTICE3:def_9, TARSKI:def_1;
hence a <= z by A9, A10, ORDERS_2:3; ::_thesis: verum
end;
end;
thus S1[Y] from FINSET_1:sch_2(A2, A3, A4); ::_thesis: verum
end;
assume A11: for Y being finite Subset of X ex x being Element of L st
( x in X & x is_>=_than Y ) ; ::_thesis: ( not X is empty & X is directed )
{} c= X by XBOOLE_1:2;
then ex x being Element of L st
( x in X & x is_>=_than {} ) by A11;
hence not X is empty ; ::_thesis: X is directed
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & x <= z & y <= z ) )
assume that
A12: x in X and
A13: y in X ; ::_thesis: ex z being Element of L st
( z in X & x <= z & y <= z )
{x,y} c= X by A12, A13, ZFMISC_1:32;
then consider z being Element of L such that
A14: z in X and
A15: z is_>=_than {x,y} by A11;
take z ; ::_thesis: ( z in X & x <= z & y <= z )
A16: x in {x,y} by TARSKI:def_2;
y in {x,y} by TARSKI:def_2;
hence ( z in X & x <= z & y <= z ) by A14, A15, A16, LATTICE3:def_9; ::_thesis: verum
end;
theorem Th2: :: WAYBEL_0:2
for L being non empty transitive RelStr
for X being Subset of L holds
( ( not X is empty & X is filtered ) iff for Y being finite Subset of X ex x being Element of L st
( x in X & x is_<=_than Y ) )
proof
let L be non empty transitive RelStr ; ::_thesis: for X being Subset of L holds
( ( not X is empty & X is filtered ) iff for Y being finite Subset of X ex x being Element of L st
( x in X & x is_<=_than Y ) )
let X be Subset of L; ::_thesis: ( ( not X is empty & X is filtered ) iff for Y being finite Subset of X ex x being Element of L st
( x in X & x is_<=_than Y ) )
hereby ::_thesis: ( ( for Y being finite Subset of X ex x being Element of L st
( x in X & x is_<=_than Y ) ) implies ( not X is empty & X is filtered ) )
assume not X is empty ; ::_thesis: ( X is filtered implies for Y being finite Subset of X holds S1[Y] )
then reconsider X9 = X as non empty set ;
assume A1: X is filtered ; ::_thesis: for Y being finite Subset of X holds S1[Y]
let Y be finite Subset of X; ::_thesis: S1[Y]
defpred S1[ set ] means ex x being Element of L st
( x in X & x is_<=_than $1 );
A2: Y is finite ;
set x = the Element of X9;
the Element of X9 in X ;
then reconsider x = the Element of X9 as Element of L ;
x is_<=_than {} by YELLOW_0:6;
then A3: S1[ {} ] ;
A4: now__::_thesis:_for_x,_B_being_set_st_x_in_Y_&_B_c=_Y_&_S1[B]_holds_
S1[B_\/_{x}]
let x, B be set ; ::_thesis: ( x in Y & B c= Y & S1[B] implies S1[B \/ {x}] )
assume that
A5: x in Y and
B c= Y ; ::_thesis: ( S1[B] implies S1[B \/ {x}] )
assume S1[B] ; ::_thesis: S1[B \/ {x}]
then consider y being Element of L such that
A6: y in X and
A7: y is_<=_than B ;
x in X by A5;
then reconsider x9 = x as Element of L ;
consider z being Element of L such that
A8: z in X and
A9: x9 >= z and
A10: y >= z by A1, A5, A6, Def2;
thus S1[B \/ {x}] ::_thesis: verum
proof
take z ; ::_thesis: ( z in X & z is_<=_than B \/ {x} )
thus z in X by A8; ::_thesis: z is_<=_than B \/ {x}
let a be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not a in B \/ {x} or z <= a )
reconsider a9 = a as Element of L ;
assume a in B \/ {x} ; ::_thesis: z <= a
then ( a9 in B or a9 in {x} ) by XBOOLE_0:def_3;
then ( y <= a9 or a9 = x ) by A7, LATTICE3:def_8, TARSKI:def_1;
hence z <= a by A9, A10, ORDERS_2:3; ::_thesis: verum
end;
end;
thus S1[Y] from FINSET_1:sch_2(A2, A3, A4); ::_thesis: verum
end;
assume A11: for Y being finite Subset of X ex x being Element of L st
( x in X & x is_<=_than Y ) ; ::_thesis: ( not X is empty & X is filtered )
{} c= X by XBOOLE_1:2;
then ex x being Element of L st
( x in X & x is_<=_than {} ) by A11;
hence not X is empty ; ::_thesis: X is filtered
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & z <= x & z <= y ) )
assume that
A12: x in X and
A13: y in X ; ::_thesis: ex z being Element of L st
( z in X & z <= x & z <= y )
{x,y} c= X by A12, A13, ZFMISC_1:32;
then consider z being Element of L such that
A14: z in X and
A15: z is_<=_than {x,y} by A11;
take z ; ::_thesis: ( z in X & z <= x & z <= y )
A16: x in {x,y} by TARSKI:def_2;
y in {x,y} by TARSKI:def_2;
hence ( z in X & z <= x & z <= y ) by A14, A15, A16, LATTICE3:def_8; ::_thesis: verum
end;
registration
let L be RelStr ;
cluster empty -> directed filtered for Element of K10( the carrier of L);
coherence
for b1 being Subset of L st b1 is empty holds
( b1 is directed & b1 is filtered )
proof
let S be Subset of L; ::_thesis: ( S is empty implies ( S is directed & S is filtered ) )
assume S is empty ; ::_thesis: ( S is directed & S is filtered )
then A1: S = {} L ;
thus S is directed ::_thesis: S is filtered
proof
let x be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: for y being Element of L st x in S & y in S holds
ex z being Element of L st
( z in S & x <= z & y <= z )
thus for y being Element of L st x in S & y in S holds
ex z being Element of L st
( z in S & x <= z & y <= z ) by A1; ::_thesis: verum
end;
let x be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: for y being Element of L st x in S & y in S holds
ex z being Element of L st
( z in S & z <= x & z <= y )
thus for y being Element of L st x in S & y in S holds
ex z being Element of L st
( z in S & z <= x & z <= y ) by A1; ::_thesis: verum
end;
end;
registration
let L be RelStr ;
cluster directed filtered for Element of K10( the carrier of L);
existence
ex b1 being Subset of L st
( b1 is directed & b1 is filtered )
proof
take {} L ; ::_thesis: ( {} L is directed & {} L is filtered )
thus ( {} L is directed & {} L is filtered ) ; ::_thesis: verum
end;
end;
theorem Th3: :: WAYBEL_0:3
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 & X1 is directed holds
X2 is directed
proof
let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 & X1 is directed holds
X2 is directed )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 & X1 is directed holds
X2 is directed
let X1 be Subset of L1; ::_thesis: for X2 being Subset of L2 st X1 = X2 & X1 is directed holds
X2 is directed
let X2 be Subset of L2; ::_thesis: ( X1 = X2 & X1 is directed implies X2 is directed )
assume A2: X1 = X2 ; ::_thesis: ( not X1 is directed or X2 is directed )
assume A3: for x, y being Element of L1 st x in X1 & y in X1 holds
ex z being Element of L1 st
( z in X1 & x <= z & y <= z ) ; :: according to WAYBEL_0:def_1 ::_thesis: X2 is directed
let x, y be Element of L2; :: according to WAYBEL_0:def_1 ::_thesis: ( x in X2 & y in X2 implies ex z being Element of L2 st
( z in X2 & x <= z & y <= z ) )
reconsider x9 = x, y9 = y as Element of L1 by A1;
assume that
A4: x in X2 and
A5: y in X2 ; ::_thesis: ex z being Element of L2 st
( z in X2 & x <= z & y <= z )
consider z9 being Element of L1 such that
A6: z9 in X1 and
A7: x9 <= z9 and
A8: y9 <= z9 by A2, A3, A4, A5;
reconsider z = z9 as Element of L2 by A1;
take z ; ::_thesis: ( z in X2 & x <= z & y <= z )
thus ( z in X2 & x <= z & y <= z ) by A1, A2, A6, A7, A8, YELLOW_0:1; ::_thesis: verum
end;
theorem :: WAYBEL_0:4
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 & X1 is filtered holds
X2 is filtered
proof
let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 & X1 is filtered holds
X2 is filtered )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 & X1 is filtered holds
X2 is filtered
let X1 be Subset of L1; ::_thesis: for X2 being Subset of L2 st X1 = X2 & X1 is filtered holds
X2 is filtered
let X2 be Subset of L2; ::_thesis: ( X1 = X2 & X1 is filtered implies X2 is filtered )
assume A2: X1 = X2 ; ::_thesis: ( not X1 is filtered or X2 is filtered )
assume A3: for x, y being Element of L1 st x in X1 & y in X1 holds
ex z being Element of L1 st
( z in X1 & x >= z & y >= z ) ; :: according to WAYBEL_0:def_2 ::_thesis: X2 is filtered
let x, y be Element of L2; :: according to WAYBEL_0:def_2 ::_thesis: ( x in X2 & y in X2 implies ex z being Element of L2 st
( z in X2 & z <= x & z <= y ) )
reconsider x9 = x, y9 = y as Element of L1 by A1;
assume that
A4: x in X2 and
A5: y in X2 ; ::_thesis: ex z being Element of L2 st
( z in X2 & z <= x & z <= y )
consider z9 being Element of L1 such that
A6: z9 in X1 and
A7: x9 >= z9 and
A8: y9 >= z9 by A2, A3, A4, A5;
reconsider z = z9 as Element of L2 by A1;
take z ; ::_thesis: ( z in X2 & z <= x & z <= y )
thus ( z in X2 & z <= x & z <= y ) by A1, A2, A6, A7, A8, YELLOW_0:1; ::_thesis: verum
end;
theorem Th5: :: WAYBEL_0:5
for L being non empty reflexive RelStr
for x being Element of L holds
( {x} is directed & {x} is filtered )
proof
let L be non empty reflexive RelStr ; ::_thesis: for x being Element of L holds
( {x} is directed & {x} is filtered )
let x be Element of L; ::_thesis: ( {x} is directed & {x} is filtered )
set X = {x};
hereby :: according to WAYBEL_0:def_1 ::_thesis: {x} is filtered
let z, y be Element of L; ::_thesis: ( z in {x} & y in {x} implies ex x being Element of L st
( x in {x} & z <= x & y <= x ) )
assume that
A1: z in {x} and
A2: y in {x} ; ::_thesis: ex x being Element of L st
( x in {x} & z <= x & y <= x )
take x = x; ::_thesis: ( x in {x} & z <= x & y <= x )
thus ( x in {x} & z <= x & y <= x ) by A1, A2, TARSKI:def_1; ::_thesis: verum
end;
hereby :: according to WAYBEL_0:def_2 ::_thesis: verum
let z, y be Element of L; ::_thesis: ( z in {x} & y in {x} implies ex x being Element of L st
( x in {x} & x <= z & x <= y ) )
assume that
A3: z in {x} and
A4: y in {x} ; ::_thesis: ex x being Element of L st
( x in {x} & x <= z & x <= y )
take x = x; ::_thesis: ( x in {x} & x <= z & x <= y )
thus ( x in {x} & x <= z & x <= y ) by A3, A4, TARSKI:def_1; ::_thesis: verum
end;
end;
registration
let L be non empty reflexive RelStr ;
cluster non empty finite directed filtered for Element of K10( the carrier of L);
existence
ex b1 being Subset of L st
( b1 is directed & b1 is filtered & not b1 is empty & b1 is finite )
proof
set x = the Element of L;
take { the Element of L} ; ::_thesis: ( { the Element of L} is directed & { the Element of L} is filtered & not { the Element of L} is empty & { the Element of L} is finite )
thus ( { the Element of L} is directed & { the Element of L} is filtered & not { the Element of L} is empty & { the Element of L} is finite ) by Th5; ::_thesis: verum
end;
end;
registration
let L be with_suprema RelStr ;
cluster [#] L -> directed ;
coherence
[#] L is directed
proof
set X = [#] L;
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in [#] L & y in [#] L implies ex z being Element of L st
( z in [#] L & x <= z & y <= z ) )
assume that
x in [#] L and
y in [#] L ; ::_thesis: ex z being Element of L st
( z in [#] L & x <= z & y <= z )
ex z being Element of L st
( x <= z & y <= z & ( for z9 being Element of L st x <= z9 & y <= z9 holds
z <= z9 ) ) by LATTICE3:def_10;
hence ex z being Element of L st
( z in [#] L & x <= z & y <= z ) ; ::_thesis: verum
end;
end;
registration
let L be non empty upper-bounded RelStr ;
cluster [#] L -> directed ;
coherence
[#] L is directed
proof
set X = [#] L;
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in [#] L & y in [#] L implies ex z being Element of L st
( z in [#] L & x <= z & y <= z ) )
assume that
x in [#] L and
y in [#] L ; ::_thesis: ex z being Element of L st
( z in [#] L & x <= z & y <= z )
consider z being Element of L such that
A1: z is_>=_than [#] L by YELLOW_0:def_5;
take z ; ::_thesis: ( z in [#] L & x <= z & y <= z )
thus ( z in [#] L & x <= z & y <= z ) by A1, LATTICE3:def_9; ::_thesis: verum
end;
end;
registration
let L be with_infima RelStr ;
cluster [#] L -> filtered ;
coherence
[#] L is filtered
proof
set X = [#] L;
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in [#] L & y in [#] L implies ex z being Element of L st
( z in [#] L & z <= x & z <= y ) )
assume that
x in [#] L and
y in [#] L ; ::_thesis: ex z being Element of L st
( z in [#] L & z <= x & z <= y )
ex z being Element of L st
( z <= x & z <= y & ( for z9 being Element of L st z9 <= x & z9 <= y holds
z9 <= z ) ) by LATTICE3:def_11;
hence ex z being Element of L st
( z in [#] L & z <= x & z <= y ) ; ::_thesis: verum
end;
end;
registration
let L be non empty lower-bounded RelStr ;
cluster [#] L -> filtered ;
coherence
[#] L is filtered
proof
set X = [#] L;
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in [#] L & y in [#] L implies ex z being Element of L st
( z in [#] L & z <= x & z <= y ) )
assume that
x in [#] L and
y in [#] L ; ::_thesis: ex z being Element of L st
( z in [#] L & z <= x & z <= y )
consider z being Element of L such that
A1: z is_<=_than [#] L by YELLOW_0:def_4;
take z ; ::_thesis: ( z in [#] L & z <= x & z <= y )
thus ( z in [#] L & z <= x & z <= y ) by A1, LATTICE3:def_8; ::_thesis: verum
end;
end;
definition
let L be non empty RelStr ;
let S be SubRelStr of L;
attrS is filtered-infs-inheriting means :Def3: :: WAYBEL_0:def 3
for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds
"/\" (X,L) in the carrier of S;
attrS is directed-sups-inheriting means :Def4: :: WAYBEL_0:def 4
for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
"\/" (X,L) in the carrier of S;
end;
:: deftheorem Def3 defines filtered-infs-inheriting WAYBEL_0:def_3_:_
for L being non empty RelStr
for S being SubRelStr of L holds
( S is filtered-infs-inheriting iff for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds
"/\" (X,L) in the carrier of S );
:: deftheorem Def4 defines directed-sups-inheriting WAYBEL_0:def_4_:_
for L being non empty RelStr
for S being SubRelStr of L holds
( S is directed-sups-inheriting iff for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
"\/" (X,L) in the carrier of S );
registration
let L be non empty RelStr ;
cluster infs-inheriting -> filtered-infs-inheriting for SubRelStr of L;
coherence
for b1 being SubRelStr of L st b1 is infs-inheriting holds
b1 is filtered-infs-inheriting
proof
let S be SubRelStr of L; ::_thesis: ( S is infs-inheriting implies S is filtered-infs-inheriting )
assume A1: for X being Subset of S st ex_inf_of X,L holds
"/\" (X,L) in the carrier of S ; :: according to YELLOW_0:def_18 ::_thesis: S is filtered-infs-inheriting
let X be filtered Subset of S; :: according to WAYBEL_0:def_3 ::_thesis: ( X <> {} & ex_inf_of X,L implies "/\" (X,L) in the carrier of S )
thus ( X <> {} & ex_inf_of X,L implies "/\" (X,L) in the carrier of S ) by A1; ::_thesis: verum
end;
cluster sups-inheriting -> directed-sups-inheriting for SubRelStr of L;
coherence
for b1 being SubRelStr of L st b1 is sups-inheriting holds
b1 is directed-sups-inheriting
proof
let S be SubRelStr of L; ::_thesis: ( S is sups-inheriting implies S is directed-sups-inheriting )
assume A2: for X being Subset of S st ex_sup_of X,L holds
"\/" (X,L) in the carrier of S ; :: according to YELLOW_0:def_19 ::_thesis: S is directed-sups-inheriting
let X be directed Subset of S; :: according to WAYBEL_0:def_4 ::_thesis: ( X <> {} & ex_sup_of X,L implies "\/" (X,L) in the carrier of S )
thus ( X <> {} & ex_sup_of X,L implies "\/" (X,L) in the carrier of S ) by A2; ::_thesis: verum
end;
end;
registration
let L be non empty RelStr ;
cluster non empty strict full infs-inheriting sups-inheriting for SubRelStr of L;
existence
ex b1 being SubRelStr of L st
( b1 is infs-inheriting & b1 is sups-inheriting & not b1 is empty & b1 is full & b1 is strict )
proof
set S = the non empty strict full infs-inheriting sups-inheriting SubRelStr of L;
take the non empty strict full infs-inheriting sups-inheriting SubRelStr of L ; ::_thesis: ( the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is infs-inheriting & the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is sups-inheriting & not the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is empty & the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is full & the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is strict )
thus ( the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is infs-inheriting & the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is sups-inheriting & not the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is empty & the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is full & the non empty strict full infs-inheriting sups-inheriting SubRelStr of L is strict ) ; ::_thesis: verum
end;
end;
theorem :: WAYBEL_0:6
for L being non empty transitive RelStr
for S being non empty full filtered-infs-inheriting SubRelStr of L
for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds
( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) )
proof
let L be non empty transitive RelStr ; ::_thesis: for S being non empty full filtered-infs-inheriting SubRelStr of L
for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds
( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) )
let S be non empty full filtered-infs-inheriting SubRelStr of L; ::_thesis: for X being filtered Subset of S st X <> {} & ex_inf_of X,L holds
( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) )
let X be filtered Subset of S; ::_thesis: ( X <> {} & ex_inf_of X,L implies ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) ) )
assume that
A1: X <> {} and
A2: ex_inf_of X,L ; ::_thesis: ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) )
"/\" (X,L) in the carrier of S by A1, A2, Def3;
hence ( ex_inf_of X,S & "/\" (X,S) = "/\" (X,L) ) by A2, YELLOW_0:63; ::_thesis: verum
end;
theorem :: WAYBEL_0:7
for L being non empty transitive RelStr
for S being non empty full directed-sups-inheriting SubRelStr of L
for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) )
proof
let L be non empty transitive RelStr ; ::_thesis: for S being non empty full directed-sups-inheriting SubRelStr of L
for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) )
let S be non empty full directed-sups-inheriting SubRelStr of L; ::_thesis: for X being directed Subset of S st X <> {} & ex_sup_of X,L holds
( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) )
let X be directed Subset of S; ::_thesis: ( X <> {} & ex_sup_of X,L implies ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) )
assume that
A1: X <> {} and
A2: ex_sup_of X,L ; ::_thesis: ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) )
"\/" (X,L) in the carrier of S by A1, A2, Def4;
hence ( ex_sup_of X,S & "\/" (X,S) = "\/" (X,L) ) by A2, YELLOW_0:64; ::_thesis: verum
end;
begin
definition
let L1, L2 be RelStr ;
let f be Function of L1,L2;
attrf is antitone means :: WAYBEL_0:def 5
for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x & b = f . y holds
a >= b;
end;
:: deftheorem defines antitone WAYBEL_0:def_5_:_
for L1, L2 being RelStr
for f being Function of L1,L2 holds
( f is antitone iff for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x & b = f . y holds
a >= b );
definition
let L be 1-sorted ;
attrc2 is strict ;
struct NetStr over L -> RelStr ;
aggrNetStr(# carrier, InternalRel, mapping #) -> NetStr over L;
sel mapping c2 -> Function of the carrier of c2, the carrier of L;
end;
registration
let L be 1-sorted ;
let X be non empty set ;
let O be Relation of X;
let F be Function of X, the carrier of L;
cluster NetStr(# X,O,F #) -> non empty ;
coherence
not NetStr(# X,O,F #) is empty ;
end;
definition
let N be RelStr ;
attrN is directed means :Def6: :: WAYBEL_0:def 6
[#] N is directed ;
end;
:: deftheorem Def6 defines directed WAYBEL_0:def_6_:_
for N being RelStr holds
( N is directed iff [#] N is directed );
registration
let L be 1-sorted ;
cluster non empty reflexive transitive antisymmetric strict directed for NetStr over L;
existence
ex b1 being strict NetStr over L st
( not b1 is empty & b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is directed )
proof
set X = the with_suprema Poset;
set M = the Function of the carrier of the with_suprema Poset, the carrier of L;
take N = NetStr(# the carrier of the with_suprema Poset, the InternalRel of the with_suprema Poset, the Function of the carrier of the with_suprema Poset, the carrier of L #); ::_thesis: ( not N is empty & N is reflexive & N is transitive & N is antisymmetric & N is directed )
thus not N is empty ; ::_thesis: ( N is reflexive & N is transitive & N is antisymmetric & N is directed )
A1: the InternalRel of N is_reflexive_in the carrier of N by ORDERS_2:def_2;
A2: the InternalRel of N is_transitive_in the carrier of N by ORDERS_2:def_3;
the InternalRel of N is_antisymmetric_in the carrier of N by ORDERS_2:def_4;
hence ( N is reflexive & N is transitive & N is antisymmetric ) by A1, A2, ORDERS_2:def_2, ORDERS_2:def_3, ORDERS_2:def_4; ::_thesis: N is directed
A3: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of the with_suprema Poset, the InternalRel of the with_suprema Poset #) ;
[#] the with_suprema Poset = [#] N ;
hence [#] N is directed by A3, Th3; :: according to WAYBEL_0:def_6 ::_thesis: verum
end;
end;
definition
let L be 1-sorted ;
mode prenet of L is non empty directed NetStr over L;
end;
definition
let L be 1-sorted ;
mode net of L is transitive prenet of L;
end;
definition
let L be non empty 1-sorted ;
let N be non empty NetStr over L;
func netmap (N,L) -> Function of N,L equals :: WAYBEL_0:def 7
the mapping of N;
coherence
the mapping of N is Function of N,L ;
let i be Element of N;
funcN . i -> Element of L equals :: WAYBEL_0:def 8
the mapping of N . i;
correctness
coherence
the mapping of N . i is Element of L;
;
end;
:: deftheorem defines netmap WAYBEL_0:def_7_:_
for L being non empty 1-sorted
for N being non empty NetStr over L holds netmap (N,L) = the mapping of N;
:: deftheorem defines . WAYBEL_0:def_8_:_
for L being non empty 1-sorted
for N being non empty NetStr over L
for i being Element of N holds N . i = the mapping of N . i;
definition
let L be non empty RelStr ;
let N be non empty NetStr over L;
attrN is monotone means :: WAYBEL_0:def 9
netmap (N,L) is monotone ;
attrN is antitone means :: WAYBEL_0:def 10
netmap (N,L) is antitone ;
end;
:: deftheorem defines monotone WAYBEL_0:def_9_:_
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is monotone iff netmap (N,L) is monotone );
:: deftheorem defines antitone WAYBEL_0:def_10_:_
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is antitone iff netmap (N,L) is antitone );
definition
let L be non empty 1-sorted ;
let N be non empty NetStr over L;
let X be set ;
predN is_eventually_in X means :Def11: :: WAYBEL_0:def 11
ex i being Element of N st
for j being Element of N st i <= j holds
N . j in X;
predN is_often_in X means :: WAYBEL_0:def 12
for i being Element of N ex j being Element of N st
( i <= j & N . j in X );
end;
:: deftheorem Def11 defines is_eventually_in WAYBEL_0:def_11_:_
for L being non empty 1-sorted
for N being non empty NetStr over L
for X being set holds
( N is_eventually_in X iff ex i being Element of N st
for j being Element of N st i <= j holds
N . j in X );
:: deftheorem defines is_often_in WAYBEL_0:def_12_:_
for L being non empty 1-sorted
for N being non empty NetStr over L
for X being set holds
( N is_often_in X iff for i being Element of N ex j being Element of N st
( i <= j & N . j in X ) );
theorem :: WAYBEL_0:8
for L being non empty 1-sorted
for N being non empty NetStr over L
for X, Y being set st X c= Y holds
( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) )
proof
let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L
for X, Y being set st X c= Y holds
( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) )
let N be non empty NetStr over L; ::_thesis: for X, Y being set st X c= Y holds
( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) )
let X, Y be set ; ::_thesis: ( X c= Y implies ( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) ) )
assume A1: X c= Y ; ::_thesis: ( ( N is_eventually_in X implies N is_eventually_in Y ) & ( N is_often_in X implies N is_often_in Y ) )
hereby ::_thesis: ( N is_often_in X implies N is_often_in Y )
assume N is_eventually_in X ; ::_thesis: N is_eventually_in Y
then consider i being Element of N such that
A2: for j being Element of N st i <= j holds
N . j in X by Def11;
thus N is_eventually_in Y ::_thesis: verum
proof
take i ; :: according to WAYBEL_0:def_11 ::_thesis: for j being Element of N st i <= j holds
N . j in Y
let j be Element of N; ::_thesis: ( i <= j implies N . j in Y )
assume i <= j ; ::_thesis: N . j in Y
then N . j in X by A2;
hence N . j in Y by A1; ::_thesis: verum
end;
end;
assume A3: for i being Element of N ex j being Element of N st
( i <= j & N . j in X ) ; :: according to WAYBEL_0:def_12 ::_thesis: N is_often_in Y
let i be Element of N; :: according to WAYBEL_0:def_12 ::_thesis: ex j being Element of N st
( i <= j & N . j in Y )
consider j being Element of N such that
A4: i <= j and
A5: N . j in X by A3;
take j ; ::_thesis: ( i <= j & N . j in Y )
thus ( i <= j & N . j in Y ) by A1, A4, A5; ::_thesis: verum
end;
theorem :: WAYBEL_0:9
for L being non empty 1-sorted
for N being non empty NetStr over L
for X being set holds
( N is_eventually_in X iff not N is_often_in the carrier of L \ X )
proof
let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L
for X being set holds
( N is_eventually_in X iff not N is_often_in the carrier of L \ X )
let N be non empty NetStr over L; ::_thesis: for X being set holds
( N is_eventually_in X iff not N is_often_in the carrier of L \ X )
let X be set ; ::_thesis: ( N is_eventually_in X iff not N is_often_in the carrier of L \ X )
set Y = the carrier of L \ X;
thus ( N is_eventually_in X implies not N is_often_in the carrier of L \ X ) ::_thesis: ( not N is_often_in the carrier of L \ X implies N is_eventually_in X )
proof
given i being Element of N such that A1: for j being Element of N st i <= j holds
N . j in X ; :: according to WAYBEL_0:def_11 ::_thesis: not N is_often_in the carrier of L \ X
take i ; :: according to WAYBEL_0:def_12 ::_thesis: for j being Element of N holds
( not i <= j or not N . j in the carrier of L \ X )
let j be Element of N; ::_thesis: ( not i <= j or not N . j in the carrier of L \ X )
assume i <= j ; ::_thesis: not N . j in the carrier of L \ X
then N . j in X by A1;
hence not N . j in the carrier of L \ X by XBOOLE_0:def_5; ::_thesis: verum
end;
given i being Element of N such that A2: for j being Element of N st i <= j holds
not N . j in the carrier of L \ X ; :: according to WAYBEL_0:def_12 ::_thesis: N is_eventually_in X
take i ; :: according to WAYBEL_0:def_11 ::_thesis: for j being Element of N st i <= j holds
N . j in X
let j be Element of N; ::_thesis: ( i <= j implies N . j in X )
assume i <= j ; ::_thesis: N . j in X
then not N . j in the carrier of L \ X by A2;
hence N . j in X by XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: WAYBEL_0:10
for L being non empty 1-sorted
for N being non empty NetStr over L
for X being set holds
( N is_often_in X iff not N is_eventually_in the carrier of L \ X )
proof
let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L
for X being set holds
( N is_often_in X iff not N is_eventually_in the carrier of L \ X )
let N be non empty NetStr over L; ::_thesis: for X being set holds
( N is_often_in X iff not N is_eventually_in the carrier of L \ X )
let X be set ; ::_thesis: ( N is_often_in X iff not N is_eventually_in the carrier of L \ X )
set Y = the carrier of L \ X;
thus ( N is_often_in X implies not N is_eventually_in the carrier of L \ X ) ::_thesis: ( not N is_eventually_in the carrier of L \ X implies N is_often_in X )
proof
assume A1: for i being Element of N ex j being Element of N st
( i <= j & N . j in X ) ; :: according to WAYBEL_0:def_12 ::_thesis: not N is_eventually_in the carrier of L \ X
let i be Element of N; :: according to WAYBEL_0:def_11 ::_thesis: ex j being Element of N st
( i <= j & not N . j in the carrier of L \ X )
consider j being Element of N such that
A2: i <= j and
A3: N . j in X by A1;
take j ; ::_thesis: ( i <= j & not N . j in the carrier of L \ X )
thus ( i <= j & not N . j in the carrier of L \ X ) by A2, A3, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A4: for i being Element of N ex j being Element of N st
( i <= j & not N . j in the carrier of L \ X ) ; :: according to WAYBEL_0:def_11 ::_thesis: N is_often_in X
let i be Element of N; :: according to WAYBEL_0:def_12 ::_thesis: ex j being Element of N st
( i <= j & N . j in X )
consider j being Element of N such that
A5: i <= j and
A6: not N . j in the carrier of L \ X by A4;
take j ; ::_thesis: ( i <= j & N . j in X )
thus ( i <= j & N . j in X ) by A5, A6, XBOOLE_0:def_5; ::_thesis: verum
end;
scheme :: WAYBEL_0:sch 1
HoldsEventually{ F1() -> non empty RelStr , F2() -> non empty NetStr over F1(), P1[ set ] } :
( F2() is_eventually_in { (F2() . k) where k is Element of F2() : P1[F2() . k] } iff ex i being Element of F2() st
for j being Element of F2() st i <= j holds
P1[F2() . j] )
proof
set X = { (F2() . k) where k is Element of F2() : P1[F2() . k] } ;
hereby ::_thesis: ( ex i being Element of F2() st
for j being Element of F2() st i <= j holds
P1[F2() . j] implies F2() is_eventually_in { (F2() . k) where k is Element of F2() : P1[F2() . k] } )
assume F2() is_eventually_in { (F2() . k) where k is Element of F2() : P1[F2() . k] } ; ::_thesis: ex i being Element of F2() st
for j being Element of F2() st i <= j holds
P1[F2() . j]
then consider i being Element of F2() such that
A1: for j being Element of F2() st i <= j holds
F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] } by Def11;
take i = i; ::_thesis: for j being Element of F2() st i <= j holds
P1[F2() . j]
let j be Element of F2(); ::_thesis: ( i <= j implies P1[F2() . j] )
assume i <= j ; ::_thesis: P1[F2() . j]
then F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] } by A1;
then ex k being Element of F2() st
( F2() . j = F2() . k & P1[F2() . k] ) ;
hence P1[F2() . j] ; ::_thesis: verum
end;
given i being Element of F2() such that A2: for j being Element of F2() st i <= j holds
P1[F2() . j] ; ::_thesis: F2() is_eventually_in { (F2() . k) where k is Element of F2() : P1[F2() . k] }
take i ; :: according to WAYBEL_0:def_11 ::_thesis: for j being Element of F2() st i <= j holds
F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] }
let j be Element of F2(); ::_thesis: ( i <= j implies F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] } )
assume i <= j ; ::_thesis: F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] }
then P1[F2() . j] by A2;
hence F2() . j in { (F2() . k) where k is Element of F2() : P1[F2() . k] } ; ::_thesis: verum
end;
definition
let L be non empty RelStr ;
let N be non empty NetStr over L;
attrN is eventually-directed means :Def13: :: WAYBEL_0:def 13
for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } ;
attrN is eventually-filtered means :Def14: :: WAYBEL_0:def 14
for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j } ;
end;
:: deftheorem Def13 defines eventually-directed WAYBEL_0:def_13_:_
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is eventually-directed iff for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } );
:: deftheorem Def14 defines eventually-filtered WAYBEL_0:def_14_:_
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is eventually-filtered iff for i being Element of N holds N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j } );
theorem Th11: :: WAYBEL_0:11
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is eventually-directed iff for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k )
proof
let L be non empty RelStr ; ::_thesis: for N being non empty NetStr over L holds
( N is eventually-directed iff for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k )
let N be non empty NetStr over L; ::_thesis: ( N is eventually-directed iff for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k )
A1: now__::_thesis:_for_i_being_Element_of_N_holds_
(_N_is_eventually_in__{__(N_._j)_where_j_is_Element_of_N_:_S1[N_._j]__}__iff_ex_k_being_Element_of_N_st_
for_l_being_Element_of_N_st_k_<=_l_holds_
S1[N_._l]_)
let i be Element of N; ::_thesis: ( N is_eventually_in { (N . j) where j is Element of N : S1[N . j] } iff ex k being Element of N st
for l being Element of N st k <= l holds
S1[N . l] )
defpred S1[ Element of L] means N . i <= $1;
thus ( N is_eventually_in { (N . j) where j is Element of N : S1[N . j] } iff ex k being Element of N st
for l being Element of N st k <= l holds
S1[N . l] ) from WAYBEL_0:sch_1(); ::_thesis: verum
end;
hereby ::_thesis: ( ( for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k ) implies N is eventually-directed )
assume A2: N is eventually-directed ; ::_thesis: for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k
let i be Element of N; ::_thesis: ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k
N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } by A2, Def13;
hence ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k by A1; ::_thesis: verum
end;
assume A3: for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k ; ::_thesis: N is eventually-directed
let i be Element of N; :: according to WAYBEL_0:def_13 ::_thesis: N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j }
ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k by A3;
hence N is_eventually_in { (N . j) where j is Element of N : N . i <= N . j } by A1; ::_thesis: verum
end;
theorem Th12: :: WAYBEL_0:12
for L being non empty RelStr
for N being non empty NetStr over L holds
( N is eventually-filtered iff for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i >= N . k )
proof
let L be non empty RelStr ; ::_thesis: for N being non empty NetStr over L holds
( N is eventually-filtered iff for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i >= N . k )
let N be non empty NetStr over L; ::_thesis: ( N is eventually-filtered iff for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i >= N . k )
A1: now__::_thesis:_for_i_being_Element_of_N_holds_
(_N_is_eventually_in__{__(N_._j)_where_j_is_Element_of_N_:_S1[N_._j]__}__iff_ex_k_being_Element_of_N_st_
for_l_being_Element_of_N_st_k_<=_l_holds_
S1[N_._l]_)
let i be Element of N; ::_thesis: ( N is_eventually_in { (N . j) where j is Element of N : S1[N . j] } iff ex k being Element of N st
for l being Element of N st k <= l holds
S1[N . l] )
defpred S1[ Element of L] means N . i >= $1;
thus ( N is_eventually_in { (N . j) where j is Element of N : S1[N . j] } iff ex k being Element of N st
for l being Element of N st k <= l holds
S1[N . l] ) from WAYBEL_0:sch_1(); ::_thesis: verum
end;
hereby ::_thesis: ( ( for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i >= N . k ) implies N is eventually-filtered )
assume A2: N is eventually-filtered ; ::_thesis: for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i >= N . k
let i be Element of N; ::_thesis: ex j being Element of N st
for k being Element of N st j <= k holds
N . i >= N . k
N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j } by A2, Def14;
hence ex j being Element of N st
for k being Element of N st j <= k holds
N . i >= N . k by A1; ::_thesis: verum
end;
assume A3: for i being Element of N ex j being Element of N st
for k being Element of N st j <= k holds
N . i >= N . k ; ::_thesis: N is eventually-filtered
let i be Element of N; :: according to WAYBEL_0:def_14 ::_thesis: N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j }
ex j being Element of N st
for k being Element of N st j <= k holds
N . i >= N . k by A3;
hence N is_eventually_in { (N . j) where j is Element of N : N . i >= N . j } by A1; ::_thesis: verum
end;
registration
let L be non empty RelStr ;
cluster non empty directed monotone -> eventually-directed for NetStr over L;
coherence
for b1 being prenet of L st b1 is monotone holds
b1 is eventually-directed
proof
let N be prenet of L; ::_thesis: ( N is monotone implies N is eventually-directed )
assume A1: for i, j being Element of N st i <= j holds
for a, b being Element of L st a = (netmap (N,L)) . i & b = (netmap (N,L)) . j holds
a <= b ; :: according to ORDERS_3:def_5,WAYBEL_0:def_9 ::_thesis: N is eventually-directed
now__::_thesis:_for_i_being_Element_of_N_ex_j_being_Element_of_N_st_
for_k_being_Element_of_N_st_j_<=_k_holds_
N_._i_<=_N_._k
let i be Element of N; ::_thesis: ex j being Element of N st
for k being Element of N st j <= k holds
N . i <= N . k
take j = i; ::_thesis: for k being Element of N st j <= k holds
N . i <= N . k
let k be Element of N; ::_thesis: ( j <= k implies N . i <= N . k )
assume j <= k ; ::_thesis: N . i <= N . k
hence N . i <= N . k by A1; ::_thesis: verum
end;
hence N is eventually-directed by Th11; ::_thesis: verum
end;
cluster non empty directed antitone -> eventually-filtered for NetStr over L;
coherence
for b1 being prenet of L st b1 is antitone holds
b1 is eventually-filtered
proof
let N be prenet of L; ::_thesis: ( N is antitone implies N is eventually-filtered )
assume A2: for i, j being Element of N st i <= j holds
for a, b being Element of L st a = (netmap (N,L)) . i & b = (netmap (N,L)) . j holds
a >= b ; :: according to WAYBEL_0:def_5,WAYBEL_0:def_10 ::_thesis: N is eventually-filtered
now__::_thesis:_for_i_being_Element_of_N_ex_j_being_Element_of_N_st_
for_k_being_Element_of_N_st_j_<=_k_holds_
N_._i_>=_N_._k
let i be Element of N; ::_thesis: ex j being Element of N st
for k being Element of N st j <= k holds
N . i >= N . k
take j = i; ::_thesis: for k being Element of N st j <= k holds
N . i >= N . k
let k be Element of N; ::_thesis: ( j <= k implies N . i >= N . k )
assume j <= k ; ::_thesis: N . i >= N . k
hence N . i >= N . k by A2; ::_thesis: verum
end;
hence N is eventually-filtered by Th12; ::_thesis: verum
end;
end;
registration
let L be non empty reflexive RelStr ;
cluster non empty strict directed monotone antitone for NetStr over L;
existence
ex b1 being prenet of L st
( b1 is monotone & b1 is antitone & b1 is strict )
proof
set J = the non empty upper-bounded Poset;
set x = the Element of L;
set M = the carrier of the non empty upper-bounded Poset --> the Element of L;
reconsider M = the carrier of the non empty upper-bounded Poset --> the Element of L as Function of the carrier of the non empty upper-bounded Poset, the carrier of L ;
set N = NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #);
A1: RelStr(# the carrier of NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #), the InternalRel of NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #) #) = RelStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset #) ;
[#] the non empty upper-bounded Poset = [#] NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #) ;
then [#] NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #) is directed by A1, Th3;
then reconsider N = NetStr(# the carrier of the non empty upper-bounded Poset, the InternalRel of the non empty upper-bounded Poset,M #) as prenet of L by Def6;
take N ; ::_thesis: ( N is monotone & N is antitone & N is strict )
thus N is monotone ::_thesis: ( N is antitone & N is strict )
proof
let i, j be Element of N; :: according to ORDERS_3:def_5,WAYBEL_0:def_9 ::_thesis: ( not i <= j or for b1, b2 being Element of the carrier of L holds
( not b1 = (netmap (N,L)) . i or not b2 = (netmap (N,L)) . j or b1 <= b2 ) )
assume i <= j ; ::_thesis: for b1, b2 being Element of the carrier of L holds
( not b1 = (netmap (N,L)) . i or not b2 = (netmap (N,L)) . j or b1 <= b2 )
let a, b be Element of L; ::_thesis: ( not a = (netmap (N,L)) . i or not b = (netmap (N,L)) . j or a <= b )
assume that
A2: a = (netmap (N,L)) . i and
A3: b = (netmap (N,L)) . j ; ::_thesis: a <= b
A4: a = the Element of L by A2, FUNCOP_1:7;
the Element of L <= the Element of L ;
hence a <= b by A3, A4, FUNCOP_1:7; ::_thesis: verum
end;
thus N is antitone ::_thesis: N is strict
proof
let i, j be Element of N; :: according to WAYBEL_0:def_5,WAYBEL_0:def_10 ::_thesis: ( i <= j implies for a, b being Element of L st a = (netmap (N,L)) . i & b = (netmap (N,L)) . j holds
a >= b )
assume i <= j ; ::_thesis: for a, b being Element of L st a = (netmap (N,L)) . i & b = (netmap (N,L)) . j holds
a >= b
let a, b be Element of L; ::_thesis: ( a = (netmap (N,L)) . i & b = (netmap (N,L)) . j implies a >= b )
assume that
A5: a = (netmap (N,L)) . i and
A6: b = (netmap (N,L)) . j ; ::_thesis: a >= b
A7: a = the Element of L by A5, FUNCOP_1:7;
the Element of L <= the Element of L ;
hence a >= b by A6, A7, FUNCOP_1:7; ::_thesis: verum
end;
thus N is strict ; ::_thesis: verum
end;
end;
begin
definition
let L be RelStr ;
let X be Subset of L;
func downarrow X -> Subset of L means :Def15: :: WAYBEL_0:def 15
for x being Element of L holds
( x in it iff ex y being Element of L st
( y >= x & y in X ) );
existence
ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y >= x & y in X ) )
proof
defpred S1[ set ] means ex a, y being Element of L st
( a = $1 & y >= a & y in X );
consider S being set such that
A1: for x being set holds
( x in S iff ( x in the carrier of L & S1[x] ) ) from XBOOLE_0:sch_1();
S c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in the carrier of L )
thus ( not x in S or x in the carrier of L ) by A1; ::_thesis: verum
end;
then reconsider S = S as Subset of L ;
take S ; ::_thesis: for x being Element of L holds
( x in S iff ex y being Element of L st
( y >= x & y in X ) )
let x be Element of L; ::_thesis: ( x in S iff ex y being Element of L st
( y >= x & y in X ) )
hereby ::_thesis: ( ex y being Element of L st
( y >= x & y in X ) implies x in S )
assume x in S ; ::_thesis: ex y being Element of L st
( y >= x & y in X )
then ex a, y being Element of L st
( a = x & y >= a & y in X ) by A1;
hence ex y being Element of L st
( y >= x & y in X ) ; ::_thesis: verum
end;
thus ( ex y being Element of L st
( y >= x & y in X ) implies x in S ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y >= x & y in X ) ) ) & ( for x being Element of L holds
( x in b2 iff ex y being Element of L st
( y >= x & y in X ) ) ) holds
b1 = b2
proof
let S1, S2 be Subset of L; ::_thesis: ( ( for x being Element of L holds
( x in S1 iff ex y being Element of L st
( y >= x & y in X ) ) ) & ( for x being Element of L holds
( x in S2 iff ex y being Element of L st
( y >= x & y in X ) ) ) implies S1 = S2 )
assume that
A2: for x being Element of L holds
( x in S1 iff ex y being Element of L st
( y >= x & y in X ) ) and
A3: for x being Element of L holds
( x in S2 iff ex y being Element of L st
( y >= x & y in X ) ) ; ::_thesis: S1 = S2
thus S1 c= S2 :: according to XBOOLE_0:def_10 ::_thesis: S2 c= S1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S1 or x in S2 )
assume A4: x in S1 ; ::_thesis: x in S2
then reconsider x = x as Element of L ;
ex y being Element of L st
( y >= x & y in X ) by A2, A4;
hence x in S2 by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S2 or x in S1 )
assume A5: x in S2 ; ::_thesis: x in S1
then reconsider x = x as Element of L ;
ex y being Element of L st
( y >= x & y in X ) by A3, A5;
hence x in S1 by A2; ::_thesis: verum
end;
func uparrow X -> Subset of L means :Def16: :: WAYBEL_0:def 16
for x being Element of L holds
( x in it iff ex y being Element of L st
( y <= x & y in X ) );
existence
ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y <= x & y in X ) )
proof
defpred S1[ set ] means ex a, y being Element of L st
( a = $1 & y <= a & y in X );
consider S being set such that
A6: for x being set holds
( x in S iff ( x in the carrier of L & S1[x] ) ) from XBOOLE_0:sch_1();
S c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in the carrier of L )
thus ( not x in S or x in the carrier of L ) by A6; ::_thesis: verum
end;
then reconsider S = S as Subset of L ;
take S ; ::_thesis: for x being Element of L holds
( x in S iff ex y being Element of L st
( y <= x & y in X ) )
let x be Element of L; ::_thesis: ( x in S iff ex y being Element of L st
( y <= x & y in X ) )
hereby ::_thesis: ( ex y being Element of L st
( y <= x & y in X ) implies x in S )
assume x in S ; ::_thesis: ex y being Element of L st
( y <= x & y in X )
then ex a, y being Element of L st
( a = x & y <= a & y in X ) by A6;
hence ex y being Element of L st
( y <= x & y in X ) ; ::_thesis: verum
end;
thus ( ex y being Element of L st
( y <= x & y in X ) implies x in S ) by A6; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff ex y being Element of L st
( y <= x & y in X ) ) ) & ( for x being Element of L holds
( x in b2 iff ex y being Element of L st
( y <= x & y in X ) ) ) holds
b1 = b2;
proof
let S1, S2 be Subset of L; ::_thesis: ( ( for x being Element of L holds
( x in S1 iff ex y being Element of L st
( y <= x & y in X ) ) ) & ( for x being Element of L holds
( x in S2 iff ex y being Element of L st
( y <= x & y in X ) ) ) implies S1 = S2 )
assume that
A7: for x being Element of L holds
( x in S1 iff ex y being Element of L st
( y <= x & y in X ) ) and
A8: for x being Element of L holds
( x in S2 iff ex y being Element of L st
( y <= x & y in X ) ) ; ::_thesis: S1 = S2
thus S1 c= S2 :: according to XBOOLE_0:def_10 ::_thesis: S2 c= S1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S1 or x in S2 )
assume A9: x in S1 ; ::_thesis: x in S2
then reconsider x = x as Element of L ;
ex y being Element of L st
( y <= x & y in X ) by A7, A9;
hence x in S2 by A8; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S2 or x in S1 )
assume A10: x in S2 ; ::_thesis: x in S1
then reconsider x = x as Element of L ;
ex y being Element of L st
( y <= x & y in X ) by A8, A10;
hence x in S1 by A7; ::_thesis: verum
end;
end;
:: deftheorem Def15 defines downarrow WAYBEL_0:def_15_:_
for L being RelStr
for X, b3 being Subset of L holds
( b3 = downarrow X iff for x being Element of L holds
( x in b3 iff ex y being Element of L st
( y >= x & y in X ) ) );
:: deftheorem Def16 defines uparrow WAYBEL_0:def_16_:_
for L being RelStr
for X, b3 being Subset of L holds
( b3 = uparrow X iff for x being Element of L holds
( x in b3 iff ex y being Element of L st
( y <= x & y in X ) ) );
theorem Th13: :: WAYBEL_0:13
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X being Subset of L1
for Y being Subset of L2 st X = Y holds
( downarrow X = downarrow Y & uparrow X = uparrow Y )
proof
let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X being Subset of L1
for Y being Subset of L2 st X = Y holds
( downarrow X = downarrow Y & uparrow X = uparrow Y ) )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for X being Subset of L1
for Y being Subset of L2 st X = Y holds
( downarrow X = downarrow Y & uparrow X = uparrow Y )
let X be Subset of L1; ::_thesis: for Y being Subset of L2 st X = Y holds
( downarrow X = downarrow Y & uparrow X = uparrow Y )
let Y be Subset of L2; ::_thesis: ( X = Y implies ( downarrow X = downarrow Y & uparrow X = uparrow Y ) )
assume A2: X = Y ; ::_thesis: ( downarrow X = downarrow Y & uparrow X = uparrow Y )
thus downarrow X c= downarrow Y :: according to XBOOLE_0:def_10 ::_thesis: ( downarrow Y c= downarrow X & uparrow X = uparrow Y )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow X or x in downarrow Y )
assume A3: x in downarrow X ; ::_thesis: x in downarrow Y
then reconsider x = x as Element of L1 ;
reconsider x9 = x as Element of L2 by A1;
consider y being Element of L1 such that
A4: y >= x and
A5: y in X by A3, Def15;
reconsider y9 = y as Element of L2 by A1;
y9 >= x9 by A1, A4, YELLOW_0:1;
hence x in downarrow Y by A2, A5, Def15; ::_thesis: verum
end;
thus downarrow Y c= downarrow X ::_thesis: uparrow X = uparrow Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow Y or x in downarrow X )
assume A6: x in downarrow Y ; ::_thesis: x in downarrow X
then reconsider x = x as Element of L2 ;
reconsider x9 = x as Element of L1 by A1;
consider y being Element of L2 such that
A7: y >= x and
A8: y in Y by A6, Def15;
reconsider y9 = y as Element of L1 by A1;
y9 >= x9 by A1, A7, YELLOW_0:1;
hence x in downarrow X by A2, A8, Def15; ::_thesis: verum
end;
thus uparrow X c= uparrow Y :: according to XBOOLE_0:def_10 ::_thesis: uparrow Y c= uparrow X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow X or x in uparrow Y )
assume A9: x in uparrow X ; ::_thesis: x in uparrow Y
then reconsider x = x as Element of L1 ;
reconsider x9 = x as Element of L2 by A1;
consider y being Element of L1 such that
A10: y <= x and
A11: y in X by A9, Def16;
reconsider y9 = y as Element of L2 by A1;
y9 <= x9 by A1, A10, YELLOW_0:1;
hence x in uparrow Y by A2, A11, Def16; ::_thesis: verum
end;
thus uparrow Y c= uparrow X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow Y or x in uparrow X )
assume A12: x in uparrow Y ; ::_thesis: x in uparrow X
then reconsider x = x as Element of L2 ;
reconsider x9 = x as Element of L1 by A1;
consider y being Element of L2 such that
A13: y <= x and
A14: y in Y by A12, Def16;
reconsider y9 = y as Element of L1 by A1;
y9 <= x9 by A1, A13, YELLOW_0:1;
hence x in uparrow X by A2, A14, Def16; ::_thesis: verum
end;
end;
theorem Th14: :: WAYBEL_0:14
for L being non empty RelStr
for X being Subset of L holds downarrow X = { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) }
proof
let L be non empty RelStr ; ::_thesis: for X being Subset of L holds downarrow X = { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) }
let X be Subset of L; ::_thesis: downarrow X = { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) }
set Y = { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) } ;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) } c= downarrow X
let x be set ; ::_thesis: ( x in downarrow X implies x in { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) } )
assume A1: x in downarrow X ; ::_thesis: x in { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) }
then reconsider y = x as Element of L ;
ex z being Element of L st
( z >= y & z in X ) by A1, Def15;
hence x in { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) } ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) } or x in downarrow X )
assume x in { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) } ; ::_thesis: x in downarrow X
then ex a being Element of L st
( a = x & ex y being Element of L st
( a <= y & y in X ) ) ;
hence x in downarrow X by Def15; ::_thesis: verum
end;
theorem Th15: :: WAYBEL_0:15
for L being non empty RelStr
for X being Subset of L holds uparrow X = { x where x is Element of L : ex y being Element of L st
( x >= y & y in X ) }
proof
let L be non empty RelStr ; ::_thesis: for X being Subset of L holds uparrow X = { x where x is Element of L : ex y being Element of L st
( x >= y & y in X ) }
let X be Subset of L; ::_thesis: uparrow X = { x where x is Element of L : ex y being Element of L st
( x >= y & y in X ) }
set Y = { x where x is Element of L : ex y being Element of L st
( x >= y & y in X ) } ;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { x where x is Element of L : ex y being Element of L st
( x >= y & y in X ) } c= uparrow X
let x be set ; ::_thesis: ( x in uparrow X implies x in { x where x is Element of L : ex y being Element of L st
( x >= y & y in X ) } )
assume A1: x in uparrow X ; ::_thesis: x in { x where x is Element of L : ex y being Element of L st
( x >= y & y in X ) }
then reconsider y = x as Element of L ;
ex z being Element of L st
( z <= y & z in X ) by A1, Def16;
hence x in { x where x is Element of L : ex y being Element of L st
( x >= y & y in X ) } ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { x where x is Element of L : ex y being Element of L st
( x >= y & y in X ) } or x in uparrow X )
assume x in { x where x is Element of L : ex y being Element of L st
( x >= y & y in X ) } ; ::_thesis: x in uparrow X
then ex a being Element of L st
( a = x & ex y being Element of L st
( a >= y & y in X ) ) ;
hence x in uparrow X by Def16; ::_thesis: verum
end;
registration
let L be non empty reflexive RelStr ;
let X be non empty Subset of L;
cluster downarrow X -> non empty ;
coherence
not downarrow X is empty
proof
set x = the Element of X;
reconsider x9 = the Element of X as Element of L ;
x9 <= x9 ;
hence not downarrow X is empty by Def15; ::_thesis: verum
end;
cluster uparrow X -> non empty ;
coherence
not uparrow X is empty
proof
set x = the Element of X;
reconsider x9 = the Element of X as Element of L ;
x9 <= x9 ;
hence not uparrow X is empty by Def16; ::_thesis: verum
end;
end;
theorem Th16: :: WAYBEL_0:16
for L being reflexive RelStr
for X being Subset of L holds
( X c= downarrow X & X c= uparrow X )
proof
let L be reflexive RelStr ; ::_thesis: for X being Subset of L holds
( X c= downarrow X & X c= uparrow X )
let X be Subset of L; ::_thesis: ( X c= downarrow X & X c= uparrow X )
A1: the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def_2;
hereby :: according to TARSKI:def_3 ::_thesis: X c= uparrow X
let x be set ; ::_thesis: ( x in X implies x in downarrow X )
assume A2: x in X ; ::_thesis: x in downarrow X
then reconsider y = x as Element of L ;
[y,y] in the InternalRel of L by A1, A2, RELAT_2:def_1;
then y <= y by ORDERS_2:def_5;
hence x in downarrow X by A2, Def15; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in uparrow X )
assume A3: x in X ; ::_thesis: x in uparrow X
then reconsider y = x as Element of L ;
[y,y] in the InternalRel of L by A1, A3, RELAT_2:def_1;
then y <= y by ORDERS_2:def_5;
hence x in uparrow X by A3, Def16; ::_thesis: verum
end;
definition
let L be non empty RelStr ;
let x be Element of L;
func downarrow x -> Subset of L equals :: WAYBEL_0:def 17
downarrow {x};
correctness
coherence
downarrow {x} is Subset of L;
;
func uparrow x -> Subset of L equals :: WAYBEL_0:def 18
uparrow {x};
correctness
coherence
uparrow {x} is Subset of L;
;
end;
:: deftheorem defines downarrow WAYBEL_0:def_17_:_
for L being non empty RelStr
for x being Element of L holds downarrow x = downarrow {x};
:: deftheorem defines uparrow WAYBEL_0:def_18_:_
for L being non empty RelStr
for x being Element of L holds uparrow x = uparrow {x};
theorem Th17: :: WAYBEL_0:17
for L being non empty RelStr
for x, y being Element of L holds
( y in downarrow x iff y <= x )
proof
let L be non empty RelStr ; ::_thesis: for x, y being Element of L holds
( y in downarrow x iff y <= x )
let x, y be Element of L; ::_thesis: ( y in downarrow x iff y <= x )
A1: downarrow x = { z where z is Element of L : ex v being Element of L st
( z <= v & v in {x} ) } by Th14;
then ( y in downarrow x iff ex z being Element of L st
( y = z & ex v being Element of L st
( z <= v & v in {x} ) ) ) ;
hence ( y in downarrow x implies y <= x ) by TARSKI:def_1; ::_thesis: ( y <= x implies y in downarrow x )
x in {x} by TARSKI:def_1;
hence ( y <= x implies y in downarrow x ) by A1; ::_thesis: verum
end;
theorem Th18: :: WAYBEL_0:18
for L being non empty RelStr
for x, y being Element of L holds
( y in uparrow x iff x <= y )
proof
let L be non empty RelStr ; ::_thesis: for x, y being Element of L holds
( y in uparrow x iff x <= y )
let x, y be Element of L; ::_thesis: ( y in uparrow x iff x <= y )
A1: uparrow x = { z where z is Element of L : ex v being Element of L st
( z >= v & v in {x} ) } by Th15;
then ( y in uparrow x iff ex z being Element of L st
( y = z & ex v being Element of L st
( z >= v & v in {x} ) ) ) ;
hence ( y in uparrow x implies y >= x ) by TARSKI:def_1; ::_thesis: ( x <= y implies y in uparrow x )
x in {x} by TARSKI:def_1;
hence ( x <= y implies y in uparrow x ) by A1; ::_thesis: verum
end;
theorem :: WAYBEL_0:19
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st downarrow x = downarrow y holds
x = y
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for x, y being Element of L st downarrow x = downarrow y holds
x = y
let x, y be Element of L; ::_thesis: ( downarrow x = downarrow y implies x = y )
reconsider x9 = x, y9 = y as Element of L ;
A1: x9 <= x9 ;
A2: y9 <= y9 ;
assume A3: downarrow x = downarrow y ; ::_thesis: x = y
then A4: y in downarrow x by A2, Th17;
x in downarrow y by A1, A3, Th17;
then A5: x9 <= y9 by Th17;
x9 >= y9 by A4, Th17;
hence x = y by A5, ORDERS_2:2; ::_thesis: verum
end;
theorem :: WAYBEL_0:20
for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st uparrow x = uparrow y holds
x = y
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for x, y being Element of L st uparrow x = uparrow y holds
x = y
let x, y be Element of L; ::_thesis: ( uparrow x = uparrow y implies x = y )
reconsider x9 = x, y9 = y as Element of L ;
A1: x9 <= x9 ;
A2: y9 <= y9 ;
assume A3: uparrow x = uparrow y ; ::_thesis: x = y
then A4: y in uparrow x by A2, Th18;
A5: x in uparrow y by A1, A3, Th18;
A6: x9 <= y9 by A4, Th18;
x9 >= y9 by A5, Th18;
hence x = y by A6, ORDERS_2:2; ::_thesis: verum
end;
theorem Th21: :: WAYBEL_0:21
for L being non empty transitive RelStr
for x, y being Element of L st x <= y holds
downarrow x c= downarrow y
proof
let L be non empty transitive RelStr ; ::_thesis: for x, y being Element of L st x <= y holds
downarrow x c= downarrow y
let x, y be Element of L; ::_thesis: ( x <= y implies downarrow x c= downarrow y )
assume A1: x <= y ; ::_thesis: downarrow x c= downarrow y
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in downarrow x or z in downarrow y )
assume A2: z in downarrow x ; ::_thesis: z in downarrow y
then reconsider z = z as Element of L ;
z <= x by A2, Th17;
then z <= y by A1, ORDERS_2:3;
hence z in downarrow y by Th17; ::_thesis: verum
end;
theorem Th22: :: WAYBEL_0:22
for L being non empty transitive RelStr
for x, y being Element of L st x <= y holds
uparrow y c= uparrow x
proof
let L be non empty transitive RelStr ; ::_thesis: for x, y being Element of L st x <= y holds
uparrow y c= uparrow x
let x, y be Element of L; ::_thesis: ( x <= y implies uparrow y c= uparrow x )
assume A1: x <= y ; ::_thesis: uparrow y c= uparrow x
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in uparrow y or z in uparrow x )
assume A2: z in uparrow y ; ::_thesis: z in uparrow x
then reconsider z = z as Element of L ;
y <= z by A2, Th18;
then x <= z by A1, ORDERS_2:3;
hence z in uparrow x by Th18; ::_thesis: verum
end;
registration
let L be non empty reflexive RelStr ;
let x be Element of L;
cluster downarrow x -> non empty directed ;
coherence
( not downarrow x is empty & downarrow x is directed )
proof
reconsider x9 = x as Element of L ;
thus not downarrow x is empty ; ::_thesis: downarrow x is directed
let z, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( z in downarrow x & y in downarrow x implies ex z being Element of L st
( z in downarrow x & z <= z & y <= z ) )
assume that
A1: z in downarrow x and
A2: y in downarrow x ; ::_thesis: ex z being Element of L st
( z in downarrow x & z <= z & y <= z )
take x9 ; ::_thesis: ( x9 in downarrow x & z <= x9 & y <= x9 )
x9 <= x9 ;
hence ( x9 in downarrow x & z <= x9 & y <= x9 ) by A1, A2, Th17; ::_thesis: verum
end;
cluster uparrow x -> non empty filtered ;
coherence
( not uparrow x is empty & uparrow x is filtered )
proof
reconsider x9 = x as Element of L ;
thus not uparrow x is empty ; ::_thesis: uparrow x is filtered
let z, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( z in uparrow x & y in uparrow x implies ex z being Element of L st
( z in uparrow x & z <= z & z <= y ) )
assume that
A3: z in uparrow x and
A4: y in uparrow x ; ::_thesis: ex z being Element of L st
( z in uparrow x & z <= z & z <= y )
take x9 ; ::_thesis: ( x9 in uparrow x & x9 <= z & x9 <= y )
x9 <= x9 ;
hence ( x9 in uparrow x & x9 <= z & x9 <= y ) by A3, A4, Th18; ::_thesis: verum
end;
end;
definition
let L be RelStr ;
let X be Subset of L;
attrX is lower means :Def19: :: WAYBEL_0:def 19
for x, y being Element of L st x in X & y <= x holds
y in X;
attrX is upper means :Def20: :: WAYBEL_0:def 20
for x, y being Element of L st x in X & x <= y holds
y in X;
end;
:: deftheorem Def19 defines lower WAYBEL_0:def_19_:_
for L being RelStr
for X being Subset of L holds
( X is lower iff for x, y being Element of L st x in X & y <= x holds
y in X );
:: deftheorem Def20 defines upper WAYBEL_0:def_20_:_
for L being RelStr
for X being Subset of L holds
( X is upper iff for x, y being Element of L st x in X & x <= y holds
y in X );
registration
let L be RelStr ;
cluster lower upper for Element of K10( the carrier of L);
existence
ex b1 being Subset of L st
( b1 is lower & b1 is upper )
proof
the carrier of L c= the carrier of L ;
then reconsider S = the carrier of L as Subset of L ;
take S ; ::_thesis: ( S is lower & S is upper )
thus S is lower ::_thesis: S is upper
proof
let x be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: for y being Element of L st x in S & y <= x holds
y in S
thus for y being Element of L st x in S & y <= x holds
y in S ; ::_thesis: verum
end;
let x be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: for y being Element of L st x in S & x <= y holds
y in S
thus for y being Element of L st x in S & x <= y holds
y in S ; ::_thesis: verum
end;
end;
theorem Th23: :: WAYBEL_0:23
for L being RelStr
for X being Subset of L holds
( X is lower iff downarrow X c= X )
proof
let L be RelStr ; ::_thesis: for X being Subset of L holds
( X is lower iff downarrow X c= X )
let X be Subset of L; ::_thesis: ( X is lower iff downarrow X c= X )
hereby ::_thesis: ( downarrow X c= X implies X is lower )
assume A1: X is lower ; ::_thesis: downarrow X c= X
thus downarrow X c= X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow X or x in X )
assume A2: x in downarrow X ; ::_thesis: x in X
then reconsider x9 = x as Element of L ;
ex y being Element of L st
( x9 <= y & y in X ) by A2, Def15;
hence x in X by A1, Def19; ::_thesis: verum
end;
end;
assume A3: downarrow X c= X ; ::_thesis: X is lower
let x, y be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: ( x in X & y <= x implies y in X )
assume that
A4: x in X and
A5: y <= x ; ::_thesis: y in X
y in downarrow X by A4, A5, Def15;
hence y in X by A3; ::_thesis: verum
end;
theorem Th24: :: WAYBEL_0:24
for L being RelStr
for X being Subset of L holds
( X is upper iff uparrow X c= X )
proof
let L be RelStr ; ::_thesis: for X being Subset of L holds
( X is upper iff uparrow X c= X )
let X be Subset of L; ::_thesis: ( X is upper iff uparrow X c= X )
hereby ::_thesis: ( uparrow X c= X implies X is upper )
assume A1: X is upper ; ::_thesis: uparrow X c= X
thus uparrow X c= X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow X or x in X )
assume A2: x in uparrow X ; ::_thesis: x in X
then reconsider x9 = x as Element of L ;
ex y being Element of L st
( x9 >= y & y in X ) by A2, Def16;
hence x in X by A1, Def20; ::_thesis: verum
end;
end;
assume A3: uparrow X c= X ; ::_thesis: X is upper
let x, y be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( x in X & x <= y implies y in X )
assume that
A4: x in X and
A5: y >= x ; ::_thesis: y in X
y in uparrow X by A4, A5, Def16;
hence y in X by A3; ::_thesis: verum
end;
theorem :: WAYBEL_0:25
for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds
for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 holds
( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) )
proof
let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 holds
( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) ) )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: for X1 being Subset of L1
for X2 being Subset of L2 st X1 = X2 holds
( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) )
let X1 be Subset of L1; ::_thesis: for X2 being Subset of L2 st X1 = X2 holds
( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) )
let X2 be Subset of L2; ::_thesis: ( X1 = X2 implies ( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) ) )
assume A2: X1 = X2 ; ::_thesis: ( ( X1 is lower implies X2 is lower ) & ( X1 is upper implies X2 is upper ) )
hereby ::_thesis: ( X1 is upper implies X2 is upper )
assume A3: X1 is lower ; ::_thesis: X2 is lower
A4: downarrow X1 = downarrow X2 by A1, A2, Th13;
downarrow X1 c= X1 by A3, Th23;
hence X2 is lower by A2, A4, Th23; ::_thesis: verum
end;
assume A5: X1 is upper ; ::_thesis: X2 is upper
A6: uparrow X1 = uparrow X2 by A1, A2, Th13;
uparrow X1 c= X1 by A5, Th24;
hence X2 is upper by A2, A6, Th24; ::_thesis: verum
end;
theorem :: WAYBEL_0:26
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is lower ) holds
union A is lower Subset of L
proof
let L be RelStr ; ::_thesis: for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is lower ) holds
union A is lower Subset of L
let A be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in A holds
X is lower ) implies union A is lower Subset of L )
assume A1: for X being Subset of L st X in A holds
X is lower ; ::_thesis: union A is lower Subset of L
reconsider A = A as Subset-Family of L ;
reconsider X = union A as Subset of L ;
X is lower
proof
let x, y be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: ( x in X & y <= x implies y in X )
assume x in X ; ::_thesis: ( not y <= x or y in X )
then consider Y being set such that
A2: x in Y and
A3: Y in A by TARSKI:def_4;
reconsider Y = Y as Subset of L by A3;
A4: Y is lower by A1, A3;
assume y <= x ; ::_thesis: y in X
then y in Y by A2, A4, Def19;
hence y in X by A3, TARSKI:def_4; ::_thesis: verum
end;
hence union A is lower Subset of L ; ::_thesis: verum
end;
theorem Th27: :: WAYBEL_0:27
for L being RelStr
for X, Y being Subset of L st X is lower & Y is lower holds
( X /\ Y is lower & X \/ Y is lower )
proof
let L be RelStr ; ::_thesis: for X, Y being Subset of L st X is lower & Y is lower holds
( X /\ Y is lower & X \/ Y is lower )
let X, Y be Subset of L; ::_thesis: ( X is lower & Y is lower implies ( X /\ Y is lower & X \/ Y is lower ) )
assume that
A1: for x, y being Element of L st x in X & y <= x holds
y in X and
A2: for x, y being Element of L st x in Y & y <= x holds
y in Y ; :: according to WAYBEL_0:def_19 ::_thesis: ( X /\ Y is lower & X \/ Y is lower )
hereby :: according to WAYBEL_0:def_19 ::_thesis: X \/ Y is lower
let x, y be Element of L; ::_thesis: ( x in X /\ Y & y <= x implies y in X /\ Y )
assume A3: x in X /\ Y ; ::_thesis: ( y <= x implies y in X /\ Y )
then A4: x in X by XBOOLE_0:def_4;
A5: x in Y by A3, XBOOLE_0:def_4;
assume A6: y <= x ; ::_thesis: y in X /\ Y
then A7: y in X by A1, A4;
y in Y by A2, A5, A6;
hence y in X /\ Y by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
let x, y be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: ( x in X \/ Y & y <= x implies y in X \/ Y )
assume x in X \/ Y ; ::_thesis: ( not y <= x or y in X \/ Y )
then A8: ( x in X or x in Y ) by XBOOLE_0:def_3;
assume y <= x ; ::_thesis: y in X \/ Y
then ( y in X or y in Y ) by A1, A2, A8;
hence y in X \/ Y by XBOOLE_0:def_3; ::_thesis: verum
end;
theorem :: WAYBEL_0:28
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is upper ) holds
union A is upper Subset of L
proof
let L be RelStr ; ::_thesis: for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is upper ) holds
union A is upper Subset of L
let A be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in A holds
X is upper ) implies union A is upper Subset of L )
assume A1: for X being Subset of L st X in A holds
X is upper ; ::_thesis: union A is upper Subset of L
reconsider A = A as Subset-Family of L ;
reconsider X = union A as Subset of L ;
X is upper
proof
let x, y be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( x in X & x <= y implies y in X )
assume x in X ; ::_thesis: ( not x <= y or y in X )
then consider Y being set such that
A2: x in Y and
A3: Y in A by TARSKI:def_4;
reconsider Y = Y as Subset of L by A3;
A4: Y is upper by A1, A3;
assume y >= x ; ::_thesis: y in X
then y in Y by A2, A4, Def20;
hence y in X by A3, TARSKI:def_4; ::_thesis: verum
end;
hence union A is upper Subset of L ; ::_thesis: verum
end;
theorem Th29: :: WAYBEL_0:29
for L being RelStr
for X, Y being Subset of L st X is upper & Y is upper holds
( X /\ Y is upper & X \/ Y is upper )
proof
let L be RelStr ; ::_thesis: for X, Y being Subset of L st X is upper & Y is upper holds
( X /\ Y is upper & X \/ Y is upper )
let X, Y be Subset of L; ::_thesis: ( X is upper & Y is upper implies ( X /\ Y is upper & X \/ Y is upper ) )
assume that
A1: for x, y being Element of L st x in X & y >= x holds
y in X and
A2: for x, y being Element of L st x in Y & y >= x holds
y in Y ; :: according to WAYBEL_0:def_20 ::_thesis: ( X /\ Y is upper & X \/ Y is upper )
hereby :: according to WAYBEL_0:def_20 ::_thesis: X \/ Y is upper
let x, y be Element of L; ::_thesis: ( x in X /\ Y & y >= x implies y in X /\ Y )
assume A3: x in X /\ Y ; ::_thesis: ( y >= x implies y in X /\ Y )
then A4: x in X by XBOOLE_0:def_4;
A5: x in Y by A3, XBOOLE_0:def_4;
assume A6: y >= x ; ::_thesis: y in X /\ Y
then A7: y in X by A1, A4;
y in Y by A2, A5, A6;
hence y in X /\ Y by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
let x, y be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( x in X \/ Y & x <= y implies y in X \/ Y )
assume x in X \/ Y ; ::_thesis: ( not x <= y or y in X \/ Y )
then A8: ( x in X or x in Y ) by XBOOLE_0:def_3;
assume y >= x ; ::_thesis: y in X \/ Y
then ( y in X or y in Y ) by A1, A2, A8;
hence y in X \/ Y by XBOOLE_0:def_3; ::_thesis: verum
end;
registration
let L be non empty transitive RelStr ;
let X be Subset of L;
cluster downarrow X -> lower ;
coherence
downarrow X is lower
proof
let y, z be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: ( y in downarrow X & z <= y implies z in downarrow X )
assume y in downarrow X ; ::_thesis: ( not z <= y or z in downarrow X )
then consider x being Element of L such that
A1: y <= x and
A2: x in X by Def15;
assume z <= y ; ::_thesis: z in downarrow X
then z <= x by A1, ORDERS_2:3;
hence z in downarrow X by A2, Def15; ::_thesis: verum
end;
cluster uparrow X -> upper ;
coherence
uparrow X is upper
proof
let y, z be Element of L; :: according to WAYBEL_0:def_20 ::_thesis: ( y in uparrow X & y <= z implies z in uparrow X )
assume y in uparrow X ; ::_thesis: ( not y <= z or z in uparrow X )
then consider x being Element of L such that
A3: y >= x and
A4: x in X by Def16;
assume z >= y ; ::_thesis: z in uparrow X
then z >= x by A3, ORDERS_2:3;
hence z in uparrow X by A4, Def16; ::_thesis: verum
end;
end;
registration
let L be non empty transitive RelStr ;
let x be Element of L;
cluster downarrow x -> lower ;
coherence
downarrow x is lower ;
cluster uparrow x -> upper ;
coherence
uparrow x is upper ;
end;
registration
let L be non empty RelStr ;
cluster [#] L -> lower upper ;
coherence
( [#] L is lower & [#] L is upper )
proof
set X = [#] L;
thus for x, y being Element of L st x in [#] L & y <= x holds
y in [#] L ; :: according to WAYBEL_0:def_19 ::_thesis: [#] L is upper
thus for x, y being Element of L st x in [#] L & x <= y holds
y in [#] L ; :: according to WAYBEL_0:def_20 ::_thesis: verum
end;
end;
registration
let L be non empty RelStr ;
cluster non empty lower upper for Element of K10( the carrier of L);
existence
ex b1 being Subset of L st
( not b1 is empty & b1 is lower & b1 is upper )
proof
take [#] L ; ::_thesis: ( not [#] L is empty & [#] L is lower & [#] L is upper )
thus ( not [#] L is empty & [#] L is lower & [#] L is upper ) ; ::_thesis: verum
end;
end;
registration
let L be non empty reflexive transitive RelStr ;
cluster non empty directed lower for Element of K10( the carrier of L);
existence
ex b1 being Subset of L st
( not b1 is empty & b1 is lower & b1 is directed )
proof
set x = the Element of L;
take downarrow the Element of L ; ::_thesis: ( not downarrow the Element of L is empty & downarrow the Element of L is lower & downarrow the Element of L is directed )
thus ( not downarrow the Element of L is empty & downarrow the Element of L is lower & downarrow the Element of L is directed ) ; ::_thesis: verum
end;
cluster non empty filtered upper for Element of K10( the carrier of L);
existence
ex b1 being Subset of L st
( not b1 is empty & b1 is upper & b1 is filtered )
proof
set x = the Element of L;
take uparrow the Element of L ; ::_thesis: ( not uparrow the Element of L is empty & uparrow the Element of L is upper & uparrow the Element of L is filtered )
thus ( not uparrow the Element of L is empty & uparrow the Element of L is upper & uparrow the Element of L is filtered ) ; ::_thesis: verum
end;
end;
registration
let L be with_suprema with_infima Poset;
cluster non empty directed filtered lower upper for Element of K10( the carrier of L);
existence
ex b1 being Subset of L st
( not b1 is empty & b1 is directed & b1 is filtered & b1 is lower & b1 is upper )
proof
take [#] L ; ::_thesis: ( not [#] L is empty & [#] L is directed & [#] L is filtered & [#] L is lower & [#] L is upper )
thus ( not [#] L is empty & [#] L is directed & [#] L is filtered & [#] L is lower & [#] L is upper ) ; ::_thesis: verum
end;
end;
theorem Th30: :: WAYBEL_0:30
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( X is directed iff downarrow X is directed )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L holds
( X is directed iff downarrow X is directed )
let X be Subset of L; ::_thesis: ( X is directed iff downarrow X is directed )
thus ( X is directed implies downarrow X is directed ) ::_thesis: ( downarrow X is directed implies X is directed )
proof
assume A1: for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x <= z & y <= z ) ; :: according to WAYBEL_0:def_1 ::_thesis: downarrow X is directed
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in downarrow X & y in downarrow X implies ex z being Element of L st
( z in downarrow X & x <= z & y <= z ) )
assume that
A2: x in downarrow X and
A3: y in downarrow X ; ::_thesis: ex z being Element of L st
( z in downarrow X & x <= z & y <= z )
consider x9 being Element of L such that
A4: x <= x9 and
A5: x9 in X by A2, Def15;
consider y9 being Element of L such that
A6: y <= y9 and
A7: y9 in X by A3, Def15;
consider z being Element of L such that
A8: z in X and
A9: x9 <= z and
A10: y9 <= z by A1, A5, A7;
take z ; ::_thesis: ( z in downarrow X & x <= z & y <= z )
z <= z ;
hence z in downarrow X by A8, Def15; ::_thesis: ( x <= z & y <= z )
thus ( x <= z & y <= z ) by A4, A6, A9, A10, ORDERS_2:3; ::_thesis: verum
end;
set Y = downarrow X;
assume A11: for x, y being Element of L st x in downarrow X & y in downarrow X holds
ex z being Element of L st
( z in downarrow X & x <= z & y <= z ) ; :: according to WAYBEL_0:def_1 ::_thesis: X is directed
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & x <= z & y <= z ) )
assume that
A12: x in X and
A13: y in X ; ::_thesis: ex z being Element of L st
( z in X & x <= z & y <= z )
A14: x <= x ;
A15: y <= y ;
A16: x in downarrow X by A12, A14, Def15;
y in downarrow X by A13, A15, Def15;
then consider z being Element of L such that
A17: z in downarrow X and
A18: x <= z and
A19: y <= z by A11, A16;
consider z9 being Element of L such that
A20: z <= z9 and
A21: z9 in X by A17, Def15;
take z9 ; ::_thesis: ( z9 in X & x <= z9 & y <= z9 )
thus z9 in X by A21; ::_thesis: ( x <= z9 & y <= z9 )
thus ( x <= z9 & y <= z9 ) by A18, A19, A20, ORDERS_2:3; ::_thesis: verum
end;
registration
let L be non empty reflexive transitive RelStr ;
let X be directed Subset of L;
cluster downarrow X -> directed ;
coherence
downarrow X is directed by Th30;
end;
theorem Th31: :: WAYBEL_0:31
for L being non empty reflexive transitive RelStr
for X being Subset of L
for x being Element of L holds
( x is_>=_than X iff x is_>=_than downarrow X )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L
for x being Element of L holds
( x is_>=_than X iff x is_>=_than downarrow X )
let X be Subset of L; ::_thesis: for x being Element of L holds
( x is_>=_than X iff x is_>=_than downarrow X )
let x be Element of L; ::_thesis: ( x is_>=_than X iff x is_>=_than downarrow X )
thus ( x is_>=_than X implies x is_>=_than downarrow X ) ::_thesis: ( x is_>=_than downarrow X implies x is_>=_than X )
proof
assume A1: for y being Element of L st y in X holds
x >= y ; :: according to LATTICE3:def_9 ::_thesis: x is_>=_than downarrow X
let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in downarrow X or y <= x )
assume y in downarrow X ; ::_thesis: y <= x
then consider z being Element of L such that
A2: y <= z and
A3: z in X by Def15;
x >= z by A1, A3;
hence y <= x by A2, ORDERS_2:3; ::_thesis: verum
end;
assume A4: for y being Element of L st y in downarrow X holds
x >= y ; :: according to LATTICE3:def_9 ::_thesis: x is_>=_than X
let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in X or y <= x )
assume A5: y in X ; ::_thesis: y <= x
y <= y ;
then y in downarrow X by A5, Def15;
hence y <= x by A4; ::_thesis: verum
end;
theorem Th32: :: WAYBEL_0:32
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( ex_sup_of X,L iff ex_sup_of downarrow X,L )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L holds
( ex_sup_of X,L iff ex_sup_of downarrow X,L )
let X be Subset of L; ::_thesis: ( ex_sup_of X,L iff ex_sup_of downarrow X,L )
for x being Element of L holds
( x is_>=_than X iff x is_>=_than downarrow X ) by Th31;
hence ( ex_sup_of X,L iff ex_sup_of downarrow X,L ) by YELLOW_0:46; ::_thesis: verum
end;
theorem Th33: :: WAYBEL_0:33
for L being non empty reflexive transitive RelStr
for X being Subset of L st ex_sup_of X,L holds
sup X = sup (downarrow X)
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L st ex_sup_of X,L holds
sup X = sup (downarrow X)
let X be Subset of L; ::_thesis: ( ex_sup_of X,L implies sup X = sup (downarrow X) )
for x being Element of L holds
( x is_>=_than X iff x is_>=_than downarrow X ) by Th31;
hence ( ex_sup_of X,L implies sup X = sup (downarrow X) ) by YELLOW_0:47; ::_thesis: verum
end;
theorem :: WAYBEL_0:34
for L being non empty Poset
for x being Element of L holds
( ex_sup_of downarrow x,L & sup (downarrow x) = x )
proof
let L be non empty Poset; ::_thesis: for x being Element of L holds
( ex_sup_of downarrow x,L & sup (downarrow x) = x )
let x be Element of L; ::_thesis: ( ex_sup_of downarrow x,L & sup (downarrow x) = x )
ex_sup_of {x},L by YELLOW_0:38;
hence ex_sup_of downarrow x,L by Th32; ::_thesis: sup (downarrow x) = x
thus sup (downarrow x) = sup {x} by Th33, YELLOW_0:38
.= x by YELLOW_0:39 ; ::_thesis: verum
end;
theorem Th35: :: WAYBEL_0:35
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( X is filtered iff uparrow X is filtered )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L holds
( X is filtered iff uparrow X is filtered )
let X be Subset of L; ::_thesis: ( X is filtered iff uparrow X is filtered )
thus ( X is filtered implies uparrow X is filtered ) ::_thesis: ( uparrow X is filtered implies X is filtered )
proof
assume A1: for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x >= z & y >= z ) ; :: according to WAYBEL_0:def_2 ::_thesis: uparrow X is filtered
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in uparrow X & y in uparrow X implies ex z being Element of L st
( z in uparrow X & z <= x & z <= y ) )
assume that
A2: x in uparrow X and
A3: y in uparrow X ; ::_thesis: ex z being Element of L st
( z in uparrow X & z <= x & z <= y )
consider x9 being Element of L such that
A4: x >= x9 and
A5: x9 in X by A2, Def16;
consider y9 being Element of L such that
A6: y >= y9 and
A7: y9 in X by A3, Def16;
consider z being Element of L such that
A8: z in X and
A9: x9 >= z and
A10: y9 >= z by A1, A5, A7;
take z ; ::_thesis: ( z in uparrow X & z <= x & z <= y )
z >= z by ORDERS_2:1;
hence z in uparrow X by A8, Def16; ::_thesis: ( z <= x & z <= y )
thus ( z <= x & z <= y ) by A4, A6, A9, A10, ORDERS_2:3; ::_thesis: verum
end;
set Y = uparrow X;
assume A11: for x, y being Element of L st x in uparrow X & y in uparrow X holds
ex z being Element of L st
( z in uparrow X & x >= z & y >= z ) ; :: according to WAYBEL_0:def_2 ::_thesis: X is filtered
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & z <= x & z <= y ) )
assume that
A12: x in X and
A13: y in X ; ::_thesis: ex z being Element of L st
( z in X & z <= x & z <= y )
A14: x >= x by ORDERS_2:1;
A15: y >= y by ORDERS_2:1;
A16: x in uparrow X by A12, A14, Def16;
y in uparrow X by A13, A15, Def16;
then consider z being Element of L such that
A17: z in uparrow X and
A18: x >= z and
A19: y >= z by A11, A16;
consider z9 being Element of L such that
A20: z >= z9 and
A21: z9 in X by A17, Def16;
take z9 ; ::_thesis: ( z9 in X & z9 <= x & z9 <= y )
thus z9 in X by A21; ::_thesis: ( z9 <= x & z9 <= y )
thus ( z9 <= x & z9 <= y ) by A18, A19, A20, ORDERS_2:3; ::_thesis: verum
end;
registration
let L be non empty reflexive transitive RelStr ;
let X be filtered Subset of L;
cluster uparrow X -> filtered ;
coherence
uparrow X is filtered by Th35;
end;
theorem Th36: :: WAYBEL_0:36
for L being non empty reflexive transitive RelStr
for X being Subset of L
for x being Element of L holds
( x is_<=_than X iff x is_<=_than uparrow X )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L
for x being Element of L holds
( x is_<=_than X iff x is_<=_than uparrow X )
let X be Subset of L; ::_thesis: for x being Element of L holds
( x is_<=_than X iff x is_<=_than uparrow X )
let x be Element of L; ::_thesis: ( x is_<=_than X iff x is_<=_than uparrow X )
thus ( x is_<=_than X implies x is_<=_than uparrow X ) ::_thesis: ( x is_<=_than uparrow X implies x is_<=_than X )
proof
assume A1: for y being Element of L st y in X holds
x <= y ; :: according to LATTICE3:def_8 ::_thesis: x is_<=_than uparrow X
let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in uparrow X or x <= y )
assume y in uparrow X ; ::_thesis: x <= y
then consider z being Element of L such that
A2: y >= z and
A3: z in X by Def16;
x <= z by A1, A3;
hence x <= y by A2, ORDERS_2:3; ::_thesis: verum
end;
assume A4: for y being Element of L st y in uparrow X holds
x <= y ; :: according to LATTICE3:def_8 ::_thesis: x is_<=_than X
let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in X or x <= y )
assume A5: y in X ; ::_thesis: x <= y
y <= y ;
then y in uparrow X by A5, Def16;
hence x <= y by A4; ::_thesis: verum
end;
theorem Th37: :: WAYBEL_0:37
for L being non empty reflexive transitive RelStr
for X being Subset of L holds
( ex_inf_of X,L iff ex_inf_of uparrow X,L )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L holds
( ex_inf_of X,L iff ex_inf_of uparrow X,L )
let X be Subset of L; ::_thesis: ( ex_inf_of X,L iff ex_inf_of uparrow X,L )
for x being Element of L holds
( x is_<=_than X iff x is_<=_than uparrow X ) by Th36;
hence ( ex_inf_of X,L iff ex_inf_of uparrow X,L ) by YELLOW_0:48; ::_thesis: verum
end;
theorem Th38: :: WAYBEL_0:38
for L being non empty reflexive transitive RelStr
for X being Subset of L st ex_inf_of X,L holds
inf X = inf (uparrow X)
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for X being Subset of L st ex_inf_of X,L holds
inf X = inf (uparrow X)
let X be Subset of L; ::_thesis: ( ex_inf_of X,L implies inf X = inf (uparrow X) )
for x being Element of L holds
( x is_<=_than X iff x is_<=_than uparrow X ) by Th36;
hence ( ex_inf_of X,L implies inf X = inf (uparrow X) ) by YELLOW_0:49; ::_thesis: verum
end;
theorem :: WAYBEL_0:39
for L being non empty Poset
for x being Element of L holds
( ex_inf_of uparrow x,L & inf (uparrow x) = x )
proof
let L be non empty Poset; ::_thesis: for x being Element of L holds
( ex_inf_of uparrow x,L & inf (uparrow x) = x )
let x be Element of L; ::_thesis: ( ex_inf_of uparrow x,L & inf (uparrow x) = x )
ex_inf_of {x},L by YELLOW_0:38;
hence ex_inf_of uparrow x,L by Th37; ::_thesis: inf (uparrow x) = x
thus inf (uparrow x) = inf {x} by Th38, YELLOW_0:38
.= x by YELLOW_0:39 ; ::_thesis: verum
end;
begin
definition
let L be non empty reflexive transitive RelStr ;
mode Ideal of L is non empty directed lower Subset of L;
mode Filter of L is non empty filtered upper Subset of L;
end;
theorem Th40: :: WAYBEL_0:40
for L being antisymmetric with_suprema RelStr
for X being lower Subset of L holds
( X is directed iff for x, y being Element of L st x in X & y in X holds
x "\/" y in X )
proof
let L be antisymmetric with_suprema RelStr ; ::_thesis: for X being lower Subset of L holds
( X is directed iff for x, y being Element of L st x in X & y in X holds
x "\/" y in X )
let X be lower Subset of L; ::_thesis: ( X is directed iff for x, y being Element of L st x in X & y in X holds
x "\/" y in X )
thus ( X is directed implies for x, y being Element of L st x in X & y in X holds
x "\/" y in X ) ::_thesis: ( ( for x, y being Element of L st x in X & y in X holds
x "\/" y in X ) implies X is directed )
proof
assume A1: for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x <= z & y <= z ) ; :: according to WAYBEL_0:def_1 ::_thesis: for x, y being Element of L st x in X & y in X holds
x "\/" y in X
let x, y be Element of L; ::_thesis: ( x in X & y in X implies x "\/" y in X )
assume that
A2: x in X and
A3: y in X ; ::_thesis: x "\/" y in X
consider z being Element of L such that
A4: z in X and
A5: x <= z and
A6: y <= z by A1, A2, A3;
x "\/" y <= z by A5, A6, YELLOW_0:22;
hence x "\/" y in X by A4, Def19; ::_thesis: verum
end;
assume A7: for x, y being Element of L st x in X & y in X holds
x "\/" y in X ; ::_thesis: X is directed
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & x <= z & y <= z ) )
assume that
A8: x in X and
A9: y in X ; ::_thesis: ex z being Element of L st
( z in X & x <= z & y <= z )
A10: x <= x "\/" y by YELLOW_0:22;
y <= x "\/" y by YELLOW_0:22;
hence ex z being Element of L st
( z in X & x <= z & y <= z ) by A7, A8, A9, A10; ::_thesis: verum
end;
theorem Th41: :: WAYBEL_0:41
for L being antisymmetric with_infima RelStr
for X being upper Subset of L holds
( X is filtered iff for x, y being Element of L st x in X & y in X holds
x "/\" y in X )
proof
let L be antisymmetric with_infima RelStr ; ::_thesis: for X being upper Subset of L holds
( X is filtered iff for x, y being Element of L st x in X & y in X holds
x "/\" y in X )
let X be upper Subset of L; ::_thesis: ( X is filtered iff for x, y being Element of L st x in X & y in X holds
x "/\" y in X )
thus ( X is filtered implies for x, y being Element of L st x in X & y in X holds
x "/\" y in X ) ::_thesis: ( ( for x, y being Element of L st x in X & y in X holds
x "/\" y in X ) implies X is filtered )
proof
assume A1: for x, y being Element of L st x in X & y in X holds
ex z being Element of L st
( z in X & x >= z & y >= z ) ; :: according to WAYBEL_0:def_2 ::_thesis: for x, y being Element of L st x in X & y in X holds
x "/\" y in X
let x, y be Element of L; ::_thesis: ( x in X & y in X implies x "/\" y in X )
assume that
A2: x in X and
A3: y in X ; ::_thesis: x "/\" y in X
consider z being Element of L such that
A4: z in X and
A5: x >= z and
A6: y >= z by A1, A2, A3;
x "/\" y >= z by A5, A6, YELLOW_0:23;
hence x "/\" y in X by A4, Def20; ::_thesis: verum
end;
assume A7: for x, y being Element of L st x in X & y in X holds
x "/\" y in X ; ::_thesis: X is filtered
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & z <= x & z <= y ) )
assume that
A8: x in X and
A9: y in X ; ::_thesis: ex z being Element of L st
( z in X & z <= x & z <= y )
A10: x >= x "/\" y by YELLOW_0:23;
y >= x "/\" y by YELLOW_0:23;
hence ex z being Element of L st
( z in X & z <= x & z <= y ) by A7, A8, A9, A10; ::_thesis: verum
end;
theorem Th42: :: WAYBEL_0:42
for L being with_suprema Poset
for X being non empty lower Subset of L holds
( X is directed iff for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in X )
proof
let L be with_suprema Poset; ::_thesis: for X being non empty lower Subset of L holds
( X is directed iff for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in X )
let X be non empty lower Subset of L; ::_thesis: ( X is directed iff for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in X )
thus ( X is directed implies for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in X ) ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in X ) implies X is directed )
proof
assume A1: X is directed ; ::_thesis: for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in X
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "\/" (Y,L) in X )
assume A2: Y <> {} ; ::_thesis: "\/" (Y,L) in X
consider z being Element of L such that
A3: z in X and
A4: Y is_<=_than z by A1, Th1;
Y c= the carrier of L by XBOOLE_1:1;
then ex_sup_of Y,L by A2, YELLOW_0:54;
then "\/" (Y,L) <= z by A4, YELLOW_0:30;
hence "\/" (Y,L) in X by A3, Def19; ::_thesis: verum
end;
assume A5: for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in X ; ::_thesis: X is directed
set x = the Element of X;
reconsider x = the Element of X as Element of L ;
now__::_thesis:_for_Y_being_finite_Subset_of_X_ex_x_being_Element_of_L_st_
(_x_in_X_&_x_is_>=_than_Y_)
let Y be finite Subset of X; ::_thesis: ex x being Element of L st
( b2 in X & b2 is_>=_than x )
percases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; ::_thesis: ex x being Element of L st
( b2 in X & b2 is_>=_than x )
then x is_>=_than Y by YELLOW_0:6;
hence ex x being Element of L st
( x in X & x is_>=_than Y ) ; ::_thesis: verum
end;
supposeA6: Y <> {} ; ::_thesis: ex x being Element of L st
( b2 in X & b2 is_>=_than x )
Y c= the carrier of L by XBOOLE_1:1;
then ex_sup_of Y,L by A6, YELLOW_0:54;
then "\/" (Y,L) is_>=_than Y by YELLOW_0:30;
hence ex x being Element of L st
( x in X & x is_>=_than Y ) by A5, A6; ::_thesis: verum
end;
end;
end;
hence X is directed by Th1; ::_thesis: verum
end;
theorem Th43: :: WAYBEL_0:43
for L being with_infima Poset
for X being non empty upper Subset of L holds
( X is filtered iff for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X )
proof
let L be with_infima Poset; ::_thesis: for X being non empty upper Subset of L holds
( X is filtered iff for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X )
let X be non empty upper Subset of L; ::_thesis: ( X is filtered iff for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X )
thus ( X is filtered implies for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X ) ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X ) implies X is filtered )
proof
assume A1: X is filtered ; ::_thesis: for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "/\" (Y,L) in X )
assume A2: Y <> {} ; ::_thesis: "/\" (Y,L) in X
consider z being Element of L such that
A3: z in X and
A4: Y is_>=_than z by A1, Th2;
Y c= the carrier of L by XBOOLE_1:1;
then ex_inf_of Y,L by A2, YELLOW_0:55;
then "/\" (Y,L) >= z by A4, YELLOW_0:31;
hence "/\" (Y,L) in X by A3, Def20; ::_thesis: verum
end;
assume A5: for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in X ; ::_thesis: X is filtered
set x = the Element of X;
reconsider x = the Element of X as Element of L ;
now__::_thesis:_for_Y_being_finite_Subset_of_X_ex_x_being_Element_of_L_st_
(_x_in_X_&_x_is_<=_than_Y_)
let Y be finite Subset of X; ::_thesis: ex x being Element of L st
( b2 in X & b2 is_<=_than x )
percases ( Y = {} or Y <> {} ) ;
suppose Y = {} ; ::_thesis: ex x being Element of L st
( b2 in X & b2 is_<=_than x )
then x is_<=_than Y by YELLOW_0:6;
hence ex x being Element of L st
( x in X & x is_<=_than Y ) ; ::_thesis: verum
end;
supposeA6: Y <> {} ; ::_thesis: ex x being Element of L st
( b2 in X & b2 is_<=_than x )
Y c= the carrier of L by XBOOLE_1:1;
then ex_inf_of Y,L by A6, YELLOW_0:55;
then "/\" (Y,L) is_<=_than Y by YELLOW_0:31;
hence ex x being Element of L st
( x in X & x is_<=_than Y ) by A5, A6; ::_thesis: verum
end;
end;
end;
hence X is filtered by Th2; ::_thesis: verum
end;
theorem :: WAYBEL_0:44
for L being non empty antisymmetric RelStr st ( L is with_suprema or L is with_infima ) holds
for X, Y being Subset of L st X is lower & X is directed & Y is lower & Y is directed holds
X /\ Y is directed
proof
let L be non empty antisymmetric RelStr ; ::_thesis: ( ( L is with_suprema or L is with_infima ) implies for X, Y being Subset of L st X is lower & X is directed & Y is lower & Y is directed holds
X /\ Y is directed )
assume A1: ( L is with_suprema or L is with_infima ) ; ::_thesis: for X, Y being Subset of L st X is lower & X is directed & Y is lower & Y is directed holds
X /\ Y is directed
let X, Y be Subset of L; ::_thesis: ( X is lower & X is directed & Y is lower & Y is directed implies X /\ Y is directed )
assume that
A2: ( X is lower & X is directed ) and
A3: ( Y is lower & Y is directed ) ; ::_thesis: X /\ Y is directed
A4: X /\ Y is lower by A2, A3, Th27;
percases ( L is with_suprema or L is with_infima ) by A1;
supposeA5: L is with_suprema ; ::_thesis: X /\ Y is directed
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_X_/\_Y_&_y_in_X_/\_Y_holds_
x_"\/"_y_in_X_/\_Y
let x, y be Element of L; ::_thesis: ( x in X /\ Y & y in X /\ Y implies x "\/" y in X /\ Y )
assume that
A6: x in X /\ Y and
A7: y in X /\ Y ; ::_thesis: x "\/" y in X /\ Y
A8: x in X by A6, XBOOLE_0:def_4;
A9: x in Y by A6, XBOOLE_0:def_4;
A10: y in X by A7, XBOOLE_0:def_4;
A11: y in Y by A7, XBOOLE_0:def_4;
A12: x "\/" y in X by A2, A5, A8, A10, Th40;
x "\/" y in Y by A3, A5, A9, A11, Th40;
hence x "\/" y in X /\ Y by A12, XBOOLE_0:def_4; ::_thesis: verum
end;
hence X /\ Y is directed by A4, A5, Th40; ::_thesis: verum
end;
supposeA13: L is with_infima ; ::_thesis: X /\ Y is directed
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in X /\ Y & y in X /\ Y implies ex z being Element of L st
( z in X /\ Y & x <= z & y <= z ) )
assume that
A14: x in X /\ Y and
A15: y in X /\ Y ; ::_thesis: ex z being Element of L st
( z in X /\ Y & x <= z & y <= z )
A16: x in X by A14, XBOOLE_0:def_4;
A17: x in Y by A14, XBOOLE_0:def_4;
A18: y in X by A15, XBOOLE_0:def_4;
A19: y in Y by A15, XBOOLE_0:def_4;
consider zx being Element of L such that
A20: zx in X and
A21: x <= zx and
A22: y <= zx by A2, A16, A18, Def1;
consider zy being Element of L such that
A23: zy in Y and
A24: x <= zy and
A25: y <= zy by A3, A17, A19, Def1;
take z = zx "/\" zy; ::_thesis: ( z in X /\ Y & x <= z & y <= z )
A26: z <= zx by A13, YELLOW_0:23;
A27: z <= zy by A13, YELLOW_0:23;
A28: z in X by A2, A20, A26, Def19;
z in Y by A3, A23, A27, Def19;
hence z in X /\ Y by A28, XBOOLE_0:def_4; ::_thesis: ( x <= z & y <= z )
thus ( x <= z & y <= z ) by A13, A21, A22, A24, A25, YELLOW_0:23; ::_thesis: verum
end;
end;
end;
theorem :: WAYBEL_0:45
for L being non empty antisymmetric RelStr st ( L is with_suprema or L is with_infima ) holds
for X, Y being Subset of L st X is upper & X is filtered & Y is upper & Y is filtered holds
X /\ Y is filtered
proof
let L be non empty antisymmetric RelStr ; ::_thesis: ( ( L is with_suprema or L is with_infima ) implies for X, Y being Subset of L st X is upper & X is filtered & Y is upper & Y is filtered holds
X /\ Y is filtered )
assume A1: ( L is with_suprema or L is with_infima ) ; ::_thesis: for X, Y being Subset of L st X is upper & X is filtered & Y is upper & Y is filtered holds
X /\ Y is filtered
let X, Y be Subset of L; ::_thesis: ( X is upper & X is filtered & Y is upper & Y is filtered implies X /\ Y is filtered )
assume that
A2: ( X is upper & X is filtered ) and
A3: ( Y is upper & Y is filtered ) ; ::_thesis: X /\ Y is filtered
A4: X /\ Y is upper by A2, A3, Th29;
percases ( L is with_infima or L is with_suprema ) by A1;
supposeA5: L is with_infima ; ::_thesis: X /\ Y is filtered
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_X_/\_Y_&_y_in_X_/\_Y_holds_
x_"/\"_y_in_X_/\_Y
let x, y be Element of L; ::_thesis: ( x in X /\ Y & y in X /\ Y implies x "/\" y in X /\ Y )
assume that
A6: x in X /\ Y and
A7: y in X /\ Y ; ::_thesis: x "/\" y in X /\ Y
A8: x in X by A6, XBOOLE_0:def_4;
A9: x in Y by A6, XBOOLE_0:def_4;
A10: y in X by A7, XBOOLE_0:def_4;
A11: y in Y by A7, XBOOLE_0:def_4;
A12: x "/\" y in X by A2, A5, A8, A10, Th41;
x "/\" y in Y by A3, A5, A9, A11, Th41;
hence x "/\" y in X /\ Y by A12, XBOOLE_0:def_4; ::_thesis: verum
end;
hence X /\ Y is filtered by A4, A5, Th41; ::_thesis: verum
end;
supposeA13: L is with_suprema ; ::_thesis: X /\ Y is filtered
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in X /\ Y & y in X /\ Y implies ex z being Element of L st
( z in X /\ Y & z <= x & z <= y ) )
assume that
A14: x in X /\ Y and
A15: y in X /\ Y ; ::_thesis: ex z being Element of L st
( z in X /\ Y & z <= x & z <= y )
A16: x in X by A14, XBOOLE_0:def_4;
A17: x in Y by A14, XBOOLE_0:def_4;
A18: y in X by A15, XBOOLE_0:def_4;
A19: y in Y by A15, XBOOLE_0:def_4;
consider zx being Element of L such that
A20: zx in X and
A21: x >= zx and
A22: y >= zx by A2, A16, A18, Def2;
consider zy being Element of L such that
A23: zy in Y and
A24: x >= zy and
A25: y >= zy by A3, A17, A19, Def2;
take z = zx "\/" zy; ::_thesis: ( z in X /\ Y & z <= x & z <= y )
A26: z >= zx by A13, YELLOW_0:22;
A27: z >= zy by A13, YELLOW_0:22;
A28: z in X by A2, A20, A26, Def20;
z in Y by A3, A23, A27, Def20;
hence z in X /\ Y by A28, XBOOLE_0:def_4; ::_thesis: ( z <= x & z <= y )
thus ( z <= x & z <= y ) by A13, A21, A22, A24, A25, YELLOW_0:22; ::_thesis: verum
end;
end;
end;
theorem :: WAYBEL_0:46
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is directed ) & ( for X, Y being Subset of L st X in A & Y in A holds
ex Z being Subset of L st
( Z in A & X \/ Y c= Z ) ) holds
for X being Subset of L st X = union A holds
X is directed
proof
let L be RelStr ; ::_thesis: for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is directed ) & ( for X, Y being Subset of L st X in A & Y in A holds
ex Z being Subset of L st
( Z in A & X \/ Y c= Z ) ) holds
for X being Subset of L st X = union A holds
X is directed
let A be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in A holds
X is directed ) & ( for X, Y being Subset of L st X in A & Y in A holds
ex Z being Subset of L st
( Z in A & X \/ Y c= Z ) ) implies for X being Subset of L st X = union A holds
X is directed )
assume that
A1: for X being Subset of L st X in A holds
X is directed and
A2: for X, Y being Subset of L st X in A & Y in A holds
ex Z being Subset of L st
( Z in A & X \/ Y c= Z ) ; ::_thesis: for X being Subset of L st X = union A holds
X is directed
let Z be Subset of L; ::_thesis: ( Z = union A implies Z is directed )
assume A3: Z = union A ; ::_thesis: Z is directed
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in Z & y in Z implies ex z being Element of L st
( z in Z & x <= z & y <= z ) )
assume x in Z ; ::_thesis: ( not y in Z or ex z being Element of L st
( z in Z & x <= z & y <= z ) )
then consider X being set such that
A4: x in X and
A5: X in A by A3, TARSKI:def_4;
assume y in Z ; ::_thesis: ex z being Element of L st
( z in Z & x <= z & y <= z )
then consider Y being set such that
A6: y in Y and
A7: Y in A by A3, TARSKI:def_4;
reconsider X = X, Y = Y as Subset of L by A5, A7;
consider W being Subset of L such that
A8: W in A and
A9: X \/ Y c= W by A2, A5, A7;
A10: X c= X \/ Y by XBOOLE_1:7;
A11: Y c= X \/ Y by XBOOLE_1:7;
A12: x in X \/ Y by A4, A10;
A13: y in X \/ Y by A6, A11;
W is directed by A1, A8;
then consider z being Element of L such that
A14: z in W and
A15: x <= z and
A16: y <= z by A9, A12, A13, Def1;
take z ; ::_thesis: ( z in Z & x <= z & y <= z )
thus ( z in Z & x <= z & y <= z ) by A3, A8, A14, A15, A16, TARSKI:def_4; ::_thesis: verum
end;
theorem :: WAYBEL_0:47
for L being RelStr
for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is filtered ) & ( for X, Y being Subset of L st X in A & Y in A holds
ex Z being Subset of L st
( Z in A & X \/ Y c= Z ) ) holds
for X being Subset of L st X = union A holds
X is filtered
proof
let L be RelStr ; ::_thesis: for A being Subset-Family of L st ( for X being Subset of L st X in A holds
X is filtered ) & ( for X, Y being Subset of L st X in A & Y in A holds
ex Z being Subset of L st
( Z in A & X \/ Y c= Z ) ) holds
for X being Subset of L st X = union A holds
X is filtered
let A be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in A holds
X is filtered ) & ( for X, Y being Subset of L st X in A & Y in A holds
ex Z being Subset of L st
( Z in A & X \/ Y c= Z ) ) implies for X being Subset of L st X = union A holds
X is filtered )
assume that
A1: for X being Subset of L st X in A holds
X is filtered and
A2: for X, Y being Subset of L st X in A & Y in A holds
ex Z being Subset of L st
( Z in A & X \/ Y c= Z ) ; ::_thesis: for X being Subset of L st X = union A holds
X is filtered
let Z be Subset of L; ::_thesis: ( Z = union A implies Z is filtered )
assume A3: Z = union A ; ::_thesis: Z is filtered
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in Z & y in Z implies ex z being Element of L st
( z in Z & z <= x & z <= y ) )
assume x in Z ; ::_thesis: ( not y in Z or ex z being Element of L st
( z in Z & z <= x & z <= y ) )
then consider X being set such that
A4: x in X and
A5: X in A by A3, TARSKI:def_4;
assume y in Z ; ::_thesis: ex z being Element of L st
( z in Z & z <= x & z <= y )
then consider Y being set such that
A6: y in Y and
A7: Y in A by A3, TARSKI:def_4;
reconsider X = X, Y = Y as Subset of L by A5, A7;
consider W being Subset of L such that
A8: W in A and
A9: X \/ Y c= W by A2, A5, A7;
A10: X c= X \/ Y by XBOOLE_1:7;
A11: Y c= X \/ Y by XBOOLE_1:7;
A12: x in X \/ Y by A4, A10;
A13: y in X \/ Y by A6, A11;
W is filtered by A1, A8;
then consider z being Element of L such that
A14: z in W and
A15: x >= z and
A16: y >= z by A9, A12, A13, Def2;
take z ; ::_thesis: ( z in Z & z <= x & z <= y )
thus ( z in Z & z <= x & z <= y ) by A3, A8, A14, A15, A16, TARSKI:def_4; ::_thesis: verum
end;
definition
let L be non empty reflexive transitive RelStr ;
let I be Ideal of L;
attrI is principal means :: WAYBEL_0:def 21
ex x being Element of L st
( x in I & x is_>=_than I );
end;
:: deftheorem defines principal WAYBEL_0:def_21_:_
for L being non empty reflexive transitive RelStr
for I being Ideal of L holds
( I is principal iff ex x being Element of L st
( x in I & x is_>=_than I ) );
definition
let L be non empty reflexive transitive RelStr ;
let F be Filter of L;
attrF is principal means :: WAYBEL_0:def 22
ex x being Element of L st
( x in F & x is_<=_than F );
end;
:: deftheorem defines principal WAYBEL_0:def_22_:_
for L being non empty reflexive transitive RelStr
for F being Filter of L holds
( F is principal iff ex x being Element of L st
( x in F & x is_<=_than F ) );
theorem :: WAYBEL_0:48
for L being non empty reflexive transitive RelStr
for I being Ideal of L holds
( I is principal iff ex x being Element of L st I = downarrow x )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for I being Ideal of L holds
( I is principal iff ex x being Element of L st I = downarrow x )
let I be Ideal of L; ::_thesis: ( I is principal iff ex x being Element of L st I = downarrow x )
thus ( I is principal implies ex x being Element of L st I = downarrow x ) ::_thesis: ( ex x being Element of L st I = downarrow x implies I is principal )
proof
given x being Element of L such that A1: x in I and
A2: x is_>=_than I ; :: according to WAYBEL_0:def_21 ::_thesis: ex x being Element of L st I = downarrow x
take x ; ::_thesis: I = downarrow x
thus I c= downarrow x :: according to XBOOLE_0:def_10 ::_thesis: downarrow x c= I
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in I or y in downarrow x )
assume A3: y in I ; ::_thesis: y in downarrow x
then reconsider y = y as Element of L ;
x >= y by A2, A3, LATTICE3:def_9;
hence y in downarrow x by Th17; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in downarrow x or z in I )
assume A4: z in downarrow x ; ::_thesis: z in I
then reconsider z = z as Element of L ;
z <= x by A4, Th17;
hence z in I by A1, Def19; ::_thesis: verum
end;
given x being Element of L such that A5: I = downarrow x ; ::_thesis: I is principal
take x ; :: according to WAYBEL_0:def_21 ::_thesis: ( x in I & x is_>=_than I )
x <= x ;
hence x in I by A5, Th17; ::_thesis: x is_>=_than I
let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in I or y <= x )
thus ( not y in I or y <= x ) by A5, Th17; ::_thesis: verum
end;
theorem :: WAYBEL_0:49
for L being non empty reflexive transitive RelStr
for F being Filter of L holds
( F is principal iff ex x being Element of L st F = uparrow x )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for F being Filter of L holds
( F is principal iff ex x being Element of L st F = uparrow x )
let I be Filter of L; ::_thesis: ( I is principal iff ex x being Element of L st I = uparrow x )
thus ( I is principal implies ex x being Element of L st I = uparrow x ) ::_thesis: ( ex x being Element of L st I = uparrow x implies I is principal )
proof
given x being Element of L such that A1: x in I and
A2: x is_<=_than I ; :: according to WAYBEL_0:def_22 ::_thesis: ex x being Element of L st I = uparrow x
take x ; ::_thesis: I = uparrow x
thus I c= uparrow x :: according to XBOOLE_0:def_10 ::_thesis: uparrow x c= I
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in I or y in uparrow x )
assume A3: y in I ; ::_thesis: y in uparrow x
then reconsider y = y as Element of L ;
x <= y by A2, A3, LATTICE3:def_8;
hence y in uparrow x by Th18; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in uparrow x or z in I )
assume A4: z in uparrow x ; ::_thesis: z in I
then reconsider z = z as Element of L ;
z >= x by A4, Th18;
hence z in I by A1, Def20; ::_thesis: verum
end;
given x being Element of L such that A5: I = uparrow x ; ::_thesis: I is principal
take x ; :: according to WAYBEL_0:def_22 ::_thesis: ( x in I & x is_<=_than I )
x <= x ;
hence x in I by A5, Th18; ::_thesis: x is_<=_than I
let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in I or x <= y )
thus ( not y in I or x <= y ) by A5, Th18; ::_thesis: verum
end;
definition
let L be non empty reflexive transitive RelStr ;
func Ids L -> set equals :: WAYBEL_0:def 23
{ X where X is Ideal of L : verum } ;
correctness
coherence
{ X where X is Ideal of L : verum } is set ;
;
func Filt L -> set equals :: WAYBEL_0:def 24
{ X where X is Filter of L : verum } ;
correctness
coherence
{ X where X is Filter of L : verum } is set ;
;
end;
:: deftheorem defines Ids WAYBEL_0:def_23_:_
for L being non empty reflexive transitive RelStr holds Ids L = { X where X is Ideal of L : verum } ;
:: deftheorem defines Filt WAYBEL_0:def_24_:_
for L being non empty reflexive transitive RelStr holds Filt L = { X where X is Filter of L : verum } ;
definition
let L be non empty reflexive transitive RelStr ;
func Ids_0 L -> set equals :: WAYBEL_0:def 25
(Ids L) \/ {{}};
correctness
coherence
(Ids L) \/ {{}} is set ;
;
func Filt_0 L -> set equals :: WAYBEL_0:def 26
(Filt L) \/ {{}};
correctness
coherence
(Filt L) \/ {{}} is set ;
;
end;
:: deftheorem defines Ids_0 WAYBEL_0:def_25_:_
for L being non empty reflexive transitive RelStr holds Ids_0 L = (Ids L) \/ {{}};
:: deftheorem defines Filt_0 WAYBEL_0:def_26_:_
for L being non empty reflexive transitive RelStr holds Filt_0 L = (Filt L) \/ {{}};
definition
let L be non empty RelStr ;
let X be Subset of L;
set D = { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } ;
A1: { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } or x in the carrier of L )
assume x in { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } ; ::_thesis: x in the carrier of L
then ex Y being finite Subset of X st
( x = "\/" (Y,L) & ex_sup_of Y,L ) ;
hence x in the carrier of L ; ::_thesis: verum
end;
func finsups X -> Subset of L equals :: WAYBEL_0:def 27
{ ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } ;
correctness
coherence
{ ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } is Subset of L;
by A1;
set D = { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ;
A2: { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } or x in the carrier of L )
assume x in { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ; ::_thesis: x in the carrier of L
then ex Y being finite Subset of X st
( x = "/\" (Y,L) & ex_inf_of Y,L ) ;
hence x in the carrier of L ; ::_thesis: verum
end;
func fininfs X -> Subset of L equals :: WAYBEL_0:def 28
{ ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ;
correctness
coherence
{ ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } is Subset of L;
by A2;
end;
:: deftheorem defines finsups WAYBEL_0:def_27_:_
for L being non empty RelStr
for X being Subset of L holds finsups X = { ("\/" (Y,L)) where Y is finite Subset of X : ex_sup_of Y,L } ;
:: deftheorem defines fininfs WAYBEL_0:def_28_:_
for L being non empty RelStr
for X being Subset of L holds fininfs X = { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ;
registration
let L be non empty antisymmetric lower-bounded RelStr ;
let X be Subset of L;
cluster finsups X -> non empty ;
coherence
not finsups X is empty
proof
ex_sup_of {} ,L by YELLOW_0:42;
then "\/" (({} X),L) in finsups X ;
hence not finsups X is empty ; ::_thesis: verum
end;
end;
registration
let L be non empty antisymmetric upper-bounded RelStr ;
let X be Subset of L;
cluster fininfs X -> non empty ;
coherence
not fininfs X is empty
proof
ex_inf_of {} ,L by YELLOW_0:43;
then "/\" (({} X),L) in fininfs X ;
hence not fininfs X is empty ; ::_thesis: verum
end;
end;
registration
let L be non empty reflexive antisymmetric RelStr ;
let X be non empty Subset of L;
cluster finsups X -> non empty ;
coherence
not finsups X is empty
proof
set x = the Element of X;
reconsider y = the Element of X as Element of L ;
reconsider Z = {y} as finite Subset of X by ZFMISC_1:31;
ex_sup_of Z,L by YELLOW_0:38;
then "\/" (Z,L) in finsups X ;
hence not finsups X is empty ; ::_thesis: verum
end;
cluster fininfs X -> non empty ;
coherence
not fininfs X is empty
proof
set x = the Element of X;
reconsider y = the Element of X as Element of L ;
reconsider Z = {y} as finite Subset of X by ZFMISC_1:31;
ex_inf_of Z,L by YELLOW_0:38;
then "/\" (Z,L) in fininfs X ;
hence not fininfs X is empty ; ::_thesis: verum
end;
end;
theorem Th50: :: WAYBEL_0:50
for L being non empty reflexive antisymmetric RelStr
for X being Subset of L holds
( X c= finsups X & X c= fininfs X )
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: for X being Subset of L holds
( X c= finsups X & X c= fininfs X )
let X be Subset of L; ::_thesis: ( X c= finsups X & X c= fininfs X )
hereby :: according to TARSKI:def_3 ::_thesis: X c= fininfs X
let x be set ; ::_thesis: ( x in X implies x in finsups X )
assume A1: x in X ; ::_thesis: x in finsups X
then reconsider y = x as Element of L ;
reconsider Y = {x} as finite Subset of X by A1, ZFMISC_1:31;
A2: y = "\/" (Y,L) by YELLOW_0:39;
ex_sup_of {y},L by YELLOW_0:38;
hence x in finsups X by A2; ::_thesis: verum
end;
hereby :: according to TARSKI:def_3 ::_thesis: verum
let x be set ; ::_thesis: ( x in X implies x in fininfs X )
assume A3: x in X ; ::_thesis: x in fininfs X
then reconsider y = x as Element of L ;
reconsider Y = {x} as finite Subset of X by A3, ZFMISC_1:31;
A4: y = "/\" (Y,L) by YELLOW_0:39;
ex_inf_of {y},L by YELLOW_0:38;
hence x in fininfs X by A4; ::_thesis: verum
end;
end;
theorem Th51: :: WAYBEL_0:51
for L being non empty transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) holds
F is directed
proof
let L be non empty transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) holds
F is directed
let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) implies F is directed )
assume that
A1: for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L and
A2: for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) and
A3: for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ; ::_thesis: F is directed
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in F & y in F implies ex z being Element of L st
( z in F & x <= z & y <= z ) )
assume A4: x in F ; ::_thesis: ( not y in F or ex z being Element of L st
( z in F & x <= z & y <= z ) )
then consider Y1 being finite Subset of X such that
A5: ex_sup_of Y1,L and
A6: x = "\/" (Y1,L) by A2;
assume y in F ; ::_thesis: ex z being Element of L st
( z in F & x <= z & y <= z )
then consider Y2 being finite Subset of X such that
A7: ex_sup_of Y2,L and
A8: y = "\/" (Y2,L) by A2;
take z = "\/" ((Y1 \/ Y2),L); ::_thesis: ( z in F & x <= z & y <= z )
A9: ( ( Y1 = {} & Y2 = {} & {} \/ {} = {} ) or Y1 \/ Y2 <> {} ) ;
hence z in F by A3, A4, A6; ::_thesis: ( x <= z & y <= z )
ex_sup_of Y1 \/ Y2,L by A1, A5, A9;
hence ( x <= z & y <= z ) by A5, A6, A7, A8, XBOOLE_1:7, YELLOW_0:34; ::_thesis: verum
end;
registration
let L be with_suprema Poset;
let X be Subset of L;
cluster finsups X -> directed ;
coherence
finsups X is directed
proof
reconsider X = X as Subset of L ;
A1: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
ex_sup_of_Y,L
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies ex_sup_of Y,L )
Y c= the carrier of L by XBOOLE_1:1;
hence ( Y <> {} implies ex_sup_of Y,L ) by YELLOW_0:54; ::_thesis: verum
end;
A2: now__::_thesis:_for_x_being_Element_of_L_st_x_in_finsups_X_holds_
ex_Y_being_finite_Subset_of_X_st_
(_ex_sup_of_Y,L_&_x_=_"\/"_(Y,L)_)
let x be Element of L; ::_thesis: ( x in finsups X implies ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) )
assume x in finsups X ; ::_thesis: ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) )
then ex Y being finite Subset of X st
( x = "\/" (Y,L) & ex_sup_of Y,L ) ;
hence ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ; ::_thesis: verum
end;
now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
"\/"_(Y,L)_in_finsups_X
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "\/" (Y,L) in finsups X )
reconsider Z = Y as Subset of L by XBOOLE_1:1;
assume Y <> {} ; ::_thesis: "\/" (Y,L) in finsups X
then ex_sup_of Z,L by YELLOW_0:54;
hence "\/" (Y,L) in finsups X ; ::_thesis: verum
end;
hence finsups X is directed by A1, A2, Th51; ::_thesis: verum
end;
end;
theorem Th52: :: WAYBEL_0:52
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) holds
for x being Element of L holds
( x is_>=_than X iff x is_>=_than F )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) holds
for x being Element of L holds
( x is_>=_than X iff x is_>=_than F )
let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) implies for x being Element of L holds
( x is_>=_than X iff x is_>=_than F ) )
assume that
A1: for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L and
A2: for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) and
A3: for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ; ::_thesis: for x being Element of L holds
( x is_>=_than X iff x is_>=_than F )
let x be Element of L; ::_thesis: ( x is_>=_than X iff x is_>=_than F )
thus ( x is_>=_than X implies x is_>=_than F ) ::_thesis: ( x is_>=_than F implies x is_>=_than X )
proof
assume A4: x is_>=_than X ; ::_thesis: x is_>=_than F
let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in F or y <= x )
assume y in F ; ::_thesis: y <= x
then consider Y being finite Subset of X such that
A5: ex_sup_of Y,L and
A6: y = "\/" (Y,L) by A2;
x is_>=_than Y by A4, YELLOW_0:9;
hence y <= x by A5, A6, YELLOW_0:def_9; ::_thesis: verum
end;
assume A7: x is_>=_than F ; ::_thesis: x is_>=_than X
let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in X or y <= x )
assume y in X ; ::_thesis: y <= x
then A8: {y} c= X by ZFMISC_1:31;
then A9: sup {y} in F by A3;
ex_sup_of {y},L by A1, A8;
then A10: {y} is_<=_than sup {y} by YELLOW_0:def_9;
A11: sup {y} <= x by A7, A9, LATTICE3:def_9;
y <= sup {y} by A10, YELLOW_0:7;
hence y <= x by A11, ORDERS_2:3; ::_thesis: verum
end;
theorem Th53: :: WAYBEL_0:53
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) holds
( ex_sup_of X,L iff ex_sup_of F,L )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) holds
( ex_sup_of X,L iff ex_sup_of F,L )
let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) implies ( ex_sup_of X,L iff ex_sup_of F,L ) )
assume that
A1: for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L and
A2: for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) and
A3: for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ; ::_thesis: ( ex_sup_of X,L iff ex_sup_of F,L )
for x being Element of L holds
( x is_>=_than X iff x is_>=_than F ) by A1, A2, A3, Th52;
hence ( ex_sup_of X,L iff ex_sup_of F,L ) by YELLOW_0:46; ::_thesis: verum
end;
theorem Th54: :: WAYBEL_0:54
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) & ex_sup_of X,L holds
sup F = sup X
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) & ex_sup_of X,L holds
sup F = sup X
let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ) & ex_sup_of X,L implies sup F = sup X )
assume that
A1: for Y being finite Subset of X st Y <> {} holds
ex_sup_of Y,L and
A2: for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) and
A3: for Y being finite Subset of X st Y <> {} holds
"\/" (Y,L) in F ; ::_thesis: ( not ex_sup_of X,L or sup F = sup X )
for x being Element of L holds
( x is_>=_than X iff x is_>=_than F ) by A1, A2, A3, Th52;
hence ( not ex_sup_of X,L or sup F = sup X ) by YELLOW_0:47; ::_thesis: verum
end;
theorem :: WAYBEL_0:55
for L being with_suprema Poset
for X being Subset of L st ( ex_sup_of X,L or L is complete ) holds
sup X = sup (finsups X)
proof
let L be with_suprema Poset; ::_thesis: for X being Subset of L st ( ex_sup_of X,L or L is complete ) holds
sup X = sup (finsups X)
let X be Subset of L; ::_thesis: ( ( ex_sup_of X,L or L is complete ) implies sup X = sup (finsups X) )
assume ( ex_sup_of X,L or L is complete ) ; ::_thesis: sup X = sup (finsups X)
then A1: ex_sup_of X,L by YELLOW_0:17;
A2: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
ex_sup_of_Y,L
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies ex_sup_of Y,L )
Y c= the carrier of L by XBOOLE_1:1;
hence ( Y <> {} implies ex_sup_of Y,L ) by YELLOW_0:54; ::_thesis: verum
end;
A3: now__::_thesis:_for_x_being_Element_of_L_st_x_in_finsups_X_holds_
ex_Y_being_finite_Subset_of_X_st_
(_ex_sup_of_Y,L_&_x_=_"\/"_(Y,L)_)
let x be Element of L; ::_thesis: ( x in finsups X implies ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) )
assume x in finsups X ; ::_thesis: ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) )
then ex Y being finite Subset of X st
( x = "\/" (Y,L) & ex_sup_of Y,L ) ;
hence ex Y being finite Subset of X st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ; ::_thesis: verum
end;
now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
"\/"_(Y,L)_in_finsups_X
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "\/" (Y,L) in finsups X )
reconsider Z = Y as Subset of L by XBOOLE_1:1;
assume Y <> {} ; ::_thesis: "\/" (Y,L) in finsups X
then ex_sup_of Z,L by YELLOW_0:54;
hence "\/" (Y,L) in finsups X ; ::_thesis: verum
end;
hence sup X = sup (finsups X) by A1, A2, A3, Th54; ::_thesis: verum
end;
theorem Th56: :: WAYBEL_0:56
for L being non empty transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) holds
F is filtered
proof
let L be non empty transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) holds
F is filtered
let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) implies F is filtered )
assume that
A1: for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L and
A2: for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) and
A3: for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ; ::_thesis: F is filtered
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in F & y in F implies ex z being Element of L st
( z in F & z <= x & z <= y ) )
assume A4: x in F ; ::_thesis: ( not y in F or ex z being Element of L st
( z in F & z <= x & z <= y ) )
then consider Y1 being finite Subset of X such that
A5: ex_inf_of Y1,L and
A6: x = "/\" (Y1,L) by A2;
assume y in F ; ::_thesis: ex z being Element of L st
( z in F & z <= x & z <= y )
then consider Y2 being finite Subset of X such that
A7: ex_inf_of Y2,L and
A8: y = "/\" (Y2,L) by A2;
take z = "/\" ((Y1 \/ Y2),L); ::_thesis: ( z in F & z <= x & z <= y )
A9: ( ( Y1 = {} & Y2 = {} & {} \/ {} = {} ) or Y1 \/ Y2 <> {} ) ;
hence z in F by A3, A4, A6; ::_thesis: ( z <= x & z <= y )
ex_inf_of Y1 \/ Y2,L by A1, A5, A9;
hence ( z <= x & z <= y ) by A5, A6, A7, A8, XBOOLE_1:7, YELLOW_0:35; ::_thesis: verum
end;
registration
let L be with_infima Poset;
let X be Subset of L;
cluster fininfs X -> filtered ;
coherence
fininfs X is filtered
proof
reconsider X = X as Subset of L ;
A1: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
ex_inf_of_Y,L
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies ex_inf_of Y,L )
Y c= the carrier of L by XBOOLE_1:1;
hence ( Y <> {} implies ex_inf_of Y,L ) by YELLOW_0:55; ::_thesis: verum
end;
A2: now__::_thesis:_for_x_being_Element_of_L_st_x_in_fininfs_X_holds_
ex_Y_being_finite_Subset_of_X_st_
(_ex_inf_of_Y,L_&_x_=_"/\"_(Y,L)_)
let x be Element of L; ::_thesis: ( x in fininfs X implies ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) )
assume x in fininfs X ; ::_thesis: ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) )
then ex Y being finite Subset of X st
( x = "/\" (Y,L) & ex_inf_of Y,L ) ;
hence ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ; ::_thesis: verum
end;
now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
"/\"_(Y,L)_in_fininfs_X
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "/\" (Y,L) in fininfs X )
reconsider Z = Y as Subset of L by XBOOLE_1:1;
assume Y <> {} ; ::_thesis: "/\" (Y,L) in fininfs X
then ex_inf_of Z,L by YELLOW_0:55;
hence "/\" (Y,L) in fininfs X ; ::_thesis: verum
end;
hence fininfs X is filtered by A1, A2, Th56; ::_thesis: verum
end;
end;
theorem Th57: :: WAYBEL_0:57
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) holds
for x being Element of L holds
( x is_<=_than X iff x is_<=_than F )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) holds
for x being Element of L holds
( x is_<=_than X iff x is_<=_than F )
let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) implies for x being Element of L holds
( x is_<=_than X iff x is_<=_than F ) )
assume that
A1: for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L and
A2: for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) and
A3: for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ; ::_thesis: for x being Element of L holds
( x is_<=_than X iff x is_<=_than F )
let x be Element of L; ::_thesis: ( x is_<=_than X iff x is_<=_than F )
thus ( x is_<=_than X implies x is_<=_than F ) ::_thesis: ( x is_<=_than F implies x is_<=_than X )
proof
assume A4: x is_<=_than X ; ::_thesis: x is_<=_than F
let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in F or x <= y )
assume y in F ; ::_thesis: x <= y
then consider Y being finite Subset of X such that
A5: ex_inf_of Y,L and
A6: y = "/\" (Y,L) by A2;
x is_<=_than Y by A4, YELLOW_0:9;
hence x <= y by A5, A6, YELLOW_0:def_10; ::_thesis: verum
end;
assume A7: x is_<=_than F ; ::_thesis: x is_<=_than X
let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in X or x <= y )
assume y in X ; ::_thesis: x <= y
then A8: {y} c= X by ZFMISC_1:31;
then A9: inf {y} in F by A3;
ex_inf_of {y},L by A1, A8;
then A10: {y} is_>=_than inf {y} by YELLOW_0:def_10;
A11: inf {y} >= x by A7, A9, LATTICE3:def_8;
y >= inf {y} by A10, YELLOW_0:7;
hence x <= y by A11, ORDERS_2:3; ::_thesis: verum
end;
theorem Th58: :: WAYBEL_0:58
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) holds
( ex_inf_of X,L iff ex_inf_of F,L )
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) holds
( ex_inf_of X,L iff ex_inf_of F,L )
let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) implies ( ex_inf_of X,L iff ex_inf_of F,L ) )
assume that
A1: for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L and
A2: for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) and
A3: for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ; ::_thesis: ( ex_inf_of X,L iff ex_inf_of F,L )
for x being Element of L holds
( x is_<=_than X iff x is_<=_than F ) by A1, A2, A3, Th57;
hence ( ex_inf_of X,L iff ex_inf_of F,L ) by YELLOW_0:48; ::_thesis: verum
end;
theorem Th59: :: WAYBEL_0:59
for L being non empty reflexive transitive RelStr
for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) & ex_inf_of X,L holds
inf F = inf X
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for X, F being Subset of L st ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) & ex_inf_of X,L holds
inf F = inf X
let X, F be Subset of L; ::_thesis: ( ( for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L ) & ( for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ) & ( for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ) & ex_inf_of X,L implies inf F = inf X )
assume that
A1: for Y being finite Subset of X st Y <> {} holds
ex_inf_of Y,L and
A2: for x being Element of L st x in F holds
ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) and
A3: for Y being finite Subset of X st Y <> {} holds
"/\" (Y,L) in F ; ::_thesis: ( not ex_inf_of X,L or inf F = inf X )
for x being Element of L holds
( x is_<=_than X iff x is_<=_than F ) by A1, A2, A3, Th57;
hence ( not ex_inf_of X,L or inf F = inf X ) by YELLOW_0:49; ::_thesis: verum
end;
theorem :: WAYBEL_0:60
for L being with_infima Poset
for X being Subset of L st ( ex_inf_of X,L or L is complete ) holds
inf X = inf (fininfs X)
proof
let L be with_infima Poset; ::_thesis: for X being Subset of L st ( ex_inf_of X,L or L is complete ) holds
inf X = inf (fininfs X)
let X be Subset of L; ::_thesis: ( ( ex_inf_of X,L or L is complete ) implies inf X = inf (fininfs X) )
assume ( ex_inf_of X,L or L is complete ) ; ::_thesis: inf X = inf (fininfs X)
then A1: ex_inf_of X,L by YELLOW_0:17;
A2: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
ex_inf_of_Y,L
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies ex_inf_of Y,L )
Y c= the carrier of L by XBOOLE_1:1;
hence ( Y <> {} implies ex_inf_of Y,L ) by YELLOW_0:55; ::_thesis: verum
end;
A3: now__::_thesis:_for_x_being_Element_of_L_st_x_in_fininfs_X_holds_
ex_Y_being_finite_Subset_of_X_st_
(_ex_inf_of_Y,L_&_x_=_"/\"_(Y,L)_)
let x be Element of L; ::_thesis: ( x in fininfs X implies ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) )
assume x in fininfs X ; ::_thesis: ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) )
then ex Y being finite Subset of X st
( x = "/\" (Y,L) & ex_inf_of Y,L ) ;
hence ex Y being finite Subset of X st
( ex_inf_of Y,L & x = "/\" (Y,L) ) ; ::_thesis: verum
end;
now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
"/\"_(Y,L)_in_fininfs_X
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "/\" (Y,L) in fininfs X )
reconsider Z = Y as Subset of L by XBOOLE_1:1;
assume Y <> {} ; ::_thesis: "/\" (Y,L) in fininfs X
then ex_inf_of Z,L by YELLOW_0:55;
hence "/\" (Y,L) in fininfs X ; ::_thesis: verum
end;
hence inf X = inf (fininfs X) by A1, A2, A3, Th59; ::_thesis: verum
end;
theorem :: WAYBEL_0:61
for L being with_suprema Poset
for X being Subset of L holds
( X c= downarrow (finsups X) & ( for I being Ideal of L st X c= I holds
downarrow (finsups X) c= I ) )
proof
let L be with_suprema Poset; ::_thesis: for X being Subset of L holds
( X c= downarrow (finsups X) & ( for I being Ideal of L st X c= I holds
downarrow (finsups X) c= I ) )
let X be Subset of L; ::_thesis: ( X c= downarrow (finsups X) & ( for I being Ideal of L st X c= I holds
downarrow (finsups X) c= I ) )
A1: X c= finsups X by Th50;
finsups X c= downarrow (finsups X) by Th16;
hence X c= downarrow (finsups X) by A1, XBOOLE_1:1; ::_thesis: for I being Ideal of L st X c= I holds
downarrow (finsups X) c= I
let I be Ideal of L; ::_thesis: ( X c= I implies downarrow (finsups X) c= I )
assume A2: X c= I ; ::_thesis: downarrow (finsups X) c= I
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow (finsups X) or x in I )
assume A3: x in downarrow (finsups X) ; ::_thesis: x in I
then reconsider x = x as Element of L ;
consider y being Element of L such that
A4: x <= y and
A5: y in finsups X by A3, Def15;
consider Y being finite Subset of X such that
A6: y = "\/" (Y,L) and
A7: ex_sup_of Y,L by A5;
set i = the Element of I;
reconsider i = the Element of I as Element of L ;
A8: ex_sup_of {i},L by YELLOW_0:38;
A9: sup {i} = i by YELLOW_0:39;
A10: now__::_thesis:_(_ex_sup_of_{}_,L_implies_"\/"_({},L)_in_I_)
assume ex_sup_of {} ,L ; ::_thesis: "\/" ({},L) in I
then "\/" ({},L) <= sup {i} by A8, XBOOLE_1:2, YELLOW_0:34;
hence "\/" ({},L) in I by A9, Def19; ::_thesis: verum
end;
Y c= I by A2, XBOOLE_1:1;
then y in I by A6, A7, A10, Th42;
hence x in I by A4, Def19; ::_thesis: verum
end;
theorem :: WAYBEL_0:62
for L being with_infima Poset
for X being Subset of L holds
( X c= uparrow (fininfs X) & ( for F being Filter of L st X c= F holds
uparrow (fininfs X) c= F ) )
proof
let L be with_infima Poset; ::_thesis: for X being Subset of L holds
( X c= uparrow (fininfs X) & ( for F being Filter of L st X c= F holds
uparrow (fininfs X) c= F ) )
let X be Subset of L; ::_thesis: ( X c= uparrow (fininfs X) & ( for F being Filter of L st X c= F holds
uparrow (fininfs X) c= F ) )
A1: X c= fininfs X by Th50;
fininfs X c= uparrow (fininfs X) by Th16;
hence X c= uparrow (fininfs X) by A1, XBOOLE_1:1; ::_thesis: for F being Filter of L st X c= F holds
uparrow (fininfs X) c= F
let I be Filter of L; ::_thesis: ( X c= I implies uparrow (fininfs X) c= I )
assume A2: X c= I ; ::_thesis: uparrow (fininfs X) c= I
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow (fininfs X) or x in I )
assume A3: x in uparrow (fininfs X) ; ::_thesis: x in I
then reconsider x = x as Element of L ;
consider y being Element of L such that
A4: x >= y and
A5: y in fininfs X by A3, Def16;
consider Y being finite Subset of X such that
A6: y = "/\" (Y,L) and
A7: ex_inf_of Y,L by A5;
set i = the Element of I;
reconsider i = the Element of I as Element of L ;
A8: ex_inf_of {i},L by YELLOW_0:38;
A9: inf {i} = i by YELLOW_0:39;
A10: now__::_thesis:_(_ex_inf_of_{}_,L_implies_"/\"_({},L)_in_I_)
assume ex_inf_of {} ,L ; ::_thesis: "/\" ({},L) in I
then "/\" ({},L) >= inf {i} by A8, XBOOLE_1:2, YELLOW_0:35;
hence "/\" ({},L) in I by A9, Def20; ::_thesis: verum
end;
Y c= I by A2, XBOOLE_1:1;
then y in I by A6, A7, A10, Th43;
hence x in I by A4, Def20; ::_thesis: verum
end;
begin
definition
let L be non empty RelStr ;
attrL is connected means :Def29: :: WAYBEL_0:def 29
for x, y being Element of L holds
( x <= y or y <= x );
end;
:: deftheorem Def29 defines connected WAYBEL_0:def_29_:_
for L being non empty RelStr holds
( L is connected iff for x, y being Element of L holds
( x <= y or y <= x ) );
registration
cluster non empty trivial reflexive -> non empty reflexive connected for RelStr ;
coherence
for b1 being non empty reflexive RelStr st b1 is trivial holds
b1 is connected
proof
let L be non empty reflexive RelStr ; ::_thesis: ( L is trivial implies L is connected )
assume A1: for x, y being Element of L holds x = y ; :: according to STRUCT_0:def_10 ::_thesis: L is connected
let z1, z2 be Element of L; :: according to WAYBEL_0:def_29 ::_thesis: ( z1 <= z2 or z2 <= z1 )
z1 = z2 by A1;
hence ( z1 <= z2 or z2 <= z1 ) by ORDERS_2:1; ::_thesis: verum
end;
end;
registration
cluster non empty V58() reflexive transitive antisymmetric connected for RelStr ;
existence
ex b1 being non empty Poset st b1 is connected
proof
set O = the Order of {0};
take L = RelStr(# {0}, the Order of {0} #); ::_thesis: L is connected
let x, y be Element of L; :: according to WAYBEL_0:def_29 ::_thesis: ( x <= y or y <= x )
A1: x = 0 by TARSKI:def_1;
y = 0 by TARSKI:def_1;
hence ( x <= y or y <= x ) by A1, ORDERS_2:1; ::_thesis: verum
end;
end;
definition
mode Chain is non empty connected Poset;
end;
registration
let L be Chain;
clusterL ~ -> connected ;
coherence
L ~ is connected
proof
let x, y be Element of (L ~); :: according to WAYBEL_0:def_29 ::_thesis: ( x <= y or y <= x )
A1: (~ x) ~ = ~ x ;
A2: (~ y) ~ = ~ y ;
( ~ x <= ~ y or ~ x >= ~ y ) by Def29;
hence ( x <= y or y <= x ) by A1, A2, LATTICE3:9; ::_thesis: verum
end;
end;
begin
definition
mode Semilattice is with_infima Poset;
mode sup-Semilattice is with_suprema Poset;
mode LATTICE is with_suprema with_infima Poset;
end;
theorem :: WAYBEL_0:63
for L being Semilattice
for X being non empty upper Subset of L holds
( X is Filter of L iff subrelstr X is meet-inheriting )
proof
let L be Semilattice; ::_thesis: for X being non empty upper Subset of L holds
( X is Filter of L iff subrelstr X is meet-inheriting )
let X be non empty upper Subset of L; ::_thesis: ( X is Filter of L iff subrelstr X is meet-inheriting )
set S = subrelstr X;
A1: the carrier of (subrelstr X) = X by YELLOW_0:def_15;
hereby ::_thesis: ( subrelstr X is meet-inheriting implies X is Filter of L )
assume A2: X is Filter of L ; ::_thesis: subrelstr X is meet-inheriting
thus subrelstr X is meet-inheriting ::_thesis: verum
proof
let x, y be Element of L; :: according to YELLOW_0:def_16 ::_thesis: ( not x in the carrier of (subrelstr X) or not y in the carrier of (subrelstr X) or not ex_inf_of {x,y},L or "/\" ({x,y},L) in the carrier of (subrelstr X) )
assume that
A3: x in the carrier of (subrelstr X) and
A4: y in the carrier of (subrelstr X) and
A5: ex_inf_of {x,y},L ; ::_thesis: "/\" ({x,y},L) in the carrier of (subrelstr X)
consider z being Element of L such that
A6: z in X and
A7: x >= z and
A8: y >= z by A1, A2, A3, A4, Def2;
z is_<=_than {x,y} by A7, A8, YELLOW_0:8;
then z <= inf {x,y} by A5, YELLOW_0:def_10;
hence "/\" ({x,y},L) in the carrier of (subrelstr X) by A1, A6, Def20; ::_thesis: verum
end;
end;
assume A9: for x, y being Element of L st x in the carrier of (subrelstr X) & y in the carrier of (subrelstr X) & ex_inf_of {x,y},L holds
inf {x,y} in the carrier of (subrelstr X) ; :: according to YELLOW_0:def_16 ::_thesis: X is Filter of L
X is filtered
proof
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & z <= x & z <= y ) )
assume that
A10: x in X and
A11: y in X ; ::_thesis: ex z being Element of L st
( z in X & z <= x & z <= y )
take z = inf {x,y}; ::_thesis: ( z in X & z <= x & z <= y )
A12: z = x "/\" y by YELLOW_0:40;
ex_inf_of {x,y},L by YELLOW_0:21;
hence ( z in X & z <= x & z <= y ) by A1, A9, A10, A11, A12, YELLOW_0:19; ::_thesis: verum
end;
hence X is Filter of L ; ::_thesis: verum
end;
theorem :: WAYBEL_0:64
for L being sup-Semilattice
for X being non empty lower Subset of L holds
( X is Ideal of L iff subrelstr X is join-inheriting )
proof
let L be sup-Semilattice; ::_thesis: for X being non empty lower Subset of L holds
( X is Ideal of L iff subrelstr X is join-inheriting )
let X be non empty lower Subset of L; ::_thesis: ( X is Ideal of L iff subrelstr X is join-inheriting )
set S = subrelstr X;
A1: the carrier of (subrelstr X) = X by YELLOW_0:def_15;
hereby ::_thesis: ( subrelstr X is join-inheriting implies X is Ideal of L )
assume A2: X is Ideal of L ; ::_thesis: subrelstr X is join-inheriting
thus subrelstr X is join-inheriting ::_thesis: verum
proof
let x, y be Element of L; :: according to YELLOW_0:def_17 ::_thesis: ( not x in the carrier of (subrelstr X) or not y in the carrier of (subrelstr X) or not ex_sup_of {x,y},L or "\/" ({x,y},L) in the carrier of (subrelstr X) )
assume that
A3: x in the carrier of (subrelstr X) and
A4: y in the carrier of (subrelstr X) and
A5: ex_sup_of {x,y},L ; ::_thesis: "\/" ({x,y},L) in the carrier of (subrelstr X)
consider z being Element of L such that
A6: z in X and
A7: x <= z and
A8: y <= z by A1, A2, A3, A4, Def1;
z is_>=_than {x,y} by A7, A8, YELLOW_0:8;
then z >= sup {x,y} by A5, YELLOW_0:def_9;
hence "\/" ({x,y},L) in the carrier of (subrelstr X) by A1, A6, Def19; ::_thesis: verum
end;
end;
assume A9: for x, y being Element of L st x in the carrier of (subrelstr X) & y in the carrier of (subrelstr X) & ex_sup_of {x,y},L holds
sup {x,y} in the carrier of (subrelstr X) ; :: according to YELLOW_0:def_17 ::_thesis: X is Ideal of L
X is directed
proof
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & x <= z & y <= z ) )
assume that
A10: x in X and
A11: y in X ; ::_thesis: ex z being Element of L st
( z in X & x <= z & y <= z )
take z = sup {x,y}; ::_thesis: ( z in X & x <= z & y <= z )
A12: z = x "\/" y by YELLOW_0:41;
ex_sup_of {x,y},L by YELLOW_0:20;
hence ( z in X & x <= z & y <= z ) by A1, A9, A10, A11, A12, YELLOW_0:18; ::_thesis: verum
end;
hence X is Ideal of L ; ::_thesis: verum
end;
begin
definition
let S, T be non empty RelStr ;
let f be Function of S,T;
let X be Subset of S;
predf preserves_inf_of X means :Def30: :: WAYBEL_0:def 30
( ex_inf_of X,S implies ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) ) );
predf preserves_sup_of X means :Def31: :: WAYBEL_0:def 31
( ex_sup_of X,S implies ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) ) );
end;
:: deftheorem Def30 defines preserves_inf_of WAYBEL_0:def_30_:_
for S, T being non empty RelStr
for f being Function of S,T
for X being Subset of S holds
( f preserves_inf_of X iff ( ex_inf_of X,S implies ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) ) ) );
:: deftheorem Def31 defines preserves_sup_of WAYBEL_0:def_31_:_
for S, T being non empty RelStr
for f being Function of S,T
for X being Subset of S holds
( f preserves_sup_of X iff ( ex_sup_of X,S implies ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) ) ) );
theorem :: WAYBEL_0:65
for S1, S2, T1, T2 being non empty RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) & RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds
for f being Function of S1,S2
for g being Function of T1,T2 st f = g holds
for X being Subset of S1
for Y being Subset of T1 st X = Y holds
( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )
proof
let S1, S2, T1, T2 be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) & RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) implies for f being Function of S1,S2
for g being Function of T1,T2 st f = g holds
for X being Subset of S1
for Y being Subset of T1 st X = Y holds
( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) )
assume that
A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) and
A2: RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) ; ::_thesis: for f being Function of S1,S2
for g being Function of T1,T2 st f = g holds
for X being Subset of S1
for Y being Subset of T1 st X = Y holds
( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )
let f be Function of S1,S2; ::_thesis: for g being Function of T1,T2 st f = g holds
for X being Subset of S1
for Y being Subset of T1 st X = Y holds
( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )
let g be Function of T1,T2; ::_thesis: ( f = g implies for X being Subset of S1
for Y being Subset of T1 st X = Y holds
( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) )
assume A3: f = g ; ::_thesis: for X being Subset of S1
for Y being Subset of T1 st X = Y holds
( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )
let X be Subset of S1; ::_thesis: for Y being Subset of T1 st X = Y holds
( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )
let Y be Subset of T1; ::_thesis: ( X = Y implies ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) ) )
assume A4: X = Y ; ::_thesis: ( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )
thus ( f preserves_sup_of X implies g preserves_sup_of Y ) ::_thesis: ( f preserves_inf_of X implies g preserves_inf_of Y )
proof
assume A5: ( ex_sup_of X,S1 implies ( ex_sup_of f .: X,S2 & sup (f .: X) = f . (sup X) ) ) ; :: according to WAYBEL_0:def_31 ::_thesis: g preserves_sup_of Y
assume A6: ex_sup_of Y,T1 ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of g .: Y,T2 & sup (g .: Y) = g . (sup Y) )
hence ex_sup_of g .: Y,T2 by A1, A2, A3, A4, A5, YELLOW_0:14; ::_thesis: sup (g .: Y) = g . (sup Y)
sup (f .: X) = sup (g .: Y) by A1, A2, A3, A4, A5, A6, YELLOW_0:14, YELLOW_0:26;
hence sup (g .: Y) = g . (sup Y) by A1, A3, A4, A5, A6, YELLOW_0:14, YELLOW_0:26; ::_thesis: verum
end;
assume A7: ( ex_inf_of X,S1 implies ( ex_inf_of f .: X,S2 & inf (f .: X) = f . (inf X) ) ) ; :: according to WAYBEL_0:def_30 ::_thesis: g preserves_inf_of Y
assume A8: ex_inf_of Y,T1 ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of g .: Y,T2 & inf (g .: Y) = g . (inf Y) )
hence ex_inf_of g .: Y,T2 by A1, A2, A3, A4, A7, YELLOW_0:14; ::_thesis: inf (g .: Y) = g . (inf Y)
inf (f .: X) = inf (g .: Y) by A1, A2, A3, A4, A7, A8, YELLOW_0:14, YELLOW_0:27;
hence inf (g .: Y) = g . (inf Y) by A1, A3, A4, A7, A8, YELLOW_0:14, YELLOW_0:27; ::_thesis: verum
end;
definition
let L1, L2 be non empty RelStr ;
let f be Function of L1,L2;
attrf is infs-preserving means :: WAYBEL_0:def 32
for X being Subset of L1 holds f preserves_inf_of X;
attrf is sups-preserving means :: WAYBEL_0:def 33
for X being Subset of L1 holds f preserves_sup_of X;
attrf is meet-preserving means :: WAYBEL_0:def 34
for x, y being Element of L1 holds f preserves_inf_of {x,y};
attrf is join-preserving means :: WAYBEL_0:def 35
for x, y being Element of L1 holds f preserves_sup_of {x,y};
attrf is filtered-infs-preserving means :: WAYBEL_0:def 36
for X being Subset of L1 st not X is empty & X is filtered holds
f preserves_inf_of X;
attrf is directed-sups-preserving means :: WAYBEL_0:def 37
for X being Subset of L1 st not X is empty & X is directed holds
f preserves_sup_of X;
end;
:: deftheorem defines infs-preserving WAYBEL_0:def_32_:_
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is infs-preserving iff for X being Subset of L1 holds f preserves_inf_of X );
:: deftheorem defines sups-preserving WAYBEL_0:def_33_:_
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is sups-preserving iff for X being Subset of L1 holds f preserves_sup_of X );
:: deftheorem defines meet-preserving WAYBEL_0:def_34_:_
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is meet-preserving iff for x, y being Element of L1 holds f preserves_inf_of {x,y} );
:: deftheorem defines join-preserving WAYBEL_0:def_35_:_
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is join-preserving iff for x, y being Element of L1 holds f preserves_sup_of {x,y} );
:: deftheorem defines filtered-infs-preserving WAYBEL_0:def_36_:_
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is filtered-infs-preserving iff for X being Subset of L1 st not X is empty & X is filtered holds
f preserves_inf_of X );
:: deftheorem defines directed-sups-preserving WAYBEL_0:def_37_:_
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is directed-sups-preserving iff for X being Subset of L1 st not X is empty & X is directed holds
f preserves_sup_of X );
registration
let L1, L2 be non empty RelStr ;
cluster Function-like V21( the carrier of L1, the carrier of L2) infs-preserving -> meet-preserving filtered-infs-preserving for Element of K10(K11( the carrier of L1, the carrier of L2));
coherence
for b1 being Function of L1,L2 st b1 is infs-preserving holds
( b1 is filtered-infs-preserving & b1 is meet-preserving )
proof
let f be Function of L1,L2; ::_thesis: ( f is infs-preserving implies ( f is filtered-infs-preserving & f is meet-preserving ) )
assume A1: for X being Subset of L1 holds f preserves_inf_of X ; :: according to WAYBEL_0:def_32 ::_thesis: ( f is filtered-infs-preserving & f is meet-preserving )
hence for X being Subset of L1 st not X is empty & X is filtered holds
f preserves_inf_of X ; :: according to WAYBEL_0:def_36 ::_thesis: f is meet-preserving
thus for x, y being Element of L1 holds f preserves_inf_of {x,y} by A1; :: according to WAYBEL_0:def_34 ::_thesis: verum
end;
cluster Function-like V21( the carrier of L1, the carrier of L2) sups-preserving -> join-preserving directed-sups-preserving for Element of K10(K11( the carrier of L1, the carrier of L2));
coherence
for b1 being Function of L1,L2 st b1 is sups-preserving holds
( b1 is directed-sups-preserving & b1 is join-preserving )
proof
let f be Function of L1,L2; ::_thesis: ( f is sups-preserving implies ( f is directed-sups-preserving & f is join-preserving ) )
assume A2: for X being Subset of L1 holds f preserves_sup_of X ; :: according to WAYBEL_0:def_33 ::_thesis: ( f is directed-sups-preserving & f is join-preserving )
hence for X being Subset of L1 st not X is empty & X is directed holds
f preserves_sup_of X ; :: according to WAYBEL_0:def_37 ::_thesis: f is join-preserving
thus for x, y being Element of L1 holds f preserves_sup_of {x,y} by A2; :: according to WAYBEL_0:def_35 ::_thesis: verum
end;
end;
definition
let S, T be RelStr ;
let f be Function of S,T;
attrf is isomorphic means :Def38: :: WAYBEL_0:def 38
( f is one-to-one & f is monotone & ex g being Function of T,S st
( g = f " & g is monotone ) ) if ( not S is empty & not T is empty )
otherwise ( S is empty & T is empty );
correctness
consistency
verum;
;
end;
:: deftheorem Def38 defines isomorphic WAYBEL_0:def_38_:_
for S, T being RelStr
for f being Function of S,T holds
( ( not S is empty & not T is empty implies ( f is isomorphic iff ( f is one-to-one & f is monotone & ex g being Function of T,S st
( g = f " & g is monotone ) ) ) ) & ( ( S is empty or T is empty ) implies ( f is isomorphic iff ( S is empty & T is empty ) ) ) );
theorem Th66: :: WAYBEL_0:66
for S, T being non empty RelStr
for f being Function of S,T holds
( f is isomorphic iff ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) ) )
proof
let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T holds
( f is isomorphic iff ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) ) )
let f be Function of S,T; ::_thesis: ( f is isomorphic iff ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) ) )
hereby ::_thesis: ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) implies f is isomorphic )
assume A1: f is isomorphic ; ::_thesis: ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) ) ) )
hence f is one-to-one by Def38; ::_thesis: ( rng f = the carrier of T & ( for x, y being Element of S holds
( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) ) ) )
consider g being Function of T,S such that
A2: g = f " and
A3: g is monotone by A1, Def38;
A4: ( f is one-to-one & f is monotone ) by A1, Def38;
then rng f = dom g by A2, FUNCT_1:33;
hence rng f = the carrier of T by FUNCT_2:def_1; ::_thesis: for x, y being Element of S holds
( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )
let x, y be Element of S; ::_thesis: ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )
thus ( x <= y implies f . x <= f . y ) by A4, ORDERS_3:def_5; ::_thesis: ( f . x <= f . y implies x <= y )
assume A5: f . x <= f . y ; ::_thesis: x <= y
A6: g . (f . x) = x by A2, A4, FUNCT_2:26;
g . (f . y) = y by A2, A4, FUNCT_2:26;
hence x <= y by A3, A5, A6, ORDERS_3:def_5; ::_thesis: verum
end;
assume that
A7: f is one-to-one and
A8: rng f = the carrier of T and
A9: for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ; ::_thesis: f is isomorphic
percases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ;
:: according to WAYBEL_0:def_38
case ( not S is empty & not T is empty ) ; ::_thesis: ( f is one-to-one & f is monotone & ex g being Function of T,S st
( g = f " & g is monotone ) )
thus f is one-to-one by A7; ::_thesis: ( f is monotone & ex g being Function of T,S st
( g = f " & g is monotone ) )
thus for x, y being Element of S st x <= y holds
for a, b being Element of T st a = f . x & b = f . y holds
a <= b by A9; :: according to ORDERS_3:def_5 ::_thesis: ex g being Function of T,S st
( g = f " & g is monotone )
reconsider g = f " as Function of T,S by A7, A8, FUNCT_2:25;
take g ; ::_thesis: ( g = f " & g is monotone )
thus g = f " ; ::_thesis: g is monotone
let x, y be Element of T; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of S holds
( not b1 = g . x or not b2 = g . y or b1 <= b2 ) )
consider a being set such that
A10: a in dom f and
A11: x = f . a by A8, FUNCT_1:def_3;
consider b being set such that
A12: b in dom f and
A13: y = f . b by A8, FUNCT_1:def_3;
reconsider a = a, b = b as Element of S by A10, A12;
A14: g . x = a by A7, A11, FUNCT_2:26;
g . y = b by A7, A13, FUNCT_2:26;
hence ( not x <= y or for b1, b2 being Element of the carrier of S holds
( not b1 = g . x or not b2 = g . y or b1 <= b2 ) ) by A9, A11, A13, A14; ::_thesis: verum
end;
case ( S is empty or T is empty ) ; ::_thesis: ( S is empty & T is empty )
hence ( S is empty & T is empty ) ; ::_thesis: verum
end;
end;
end;
registration
let S, T be non empty RelStr ;
cluster Function-like V21( the carrier of S, the carrier of T) isomorphic -> one-to-one monotone for Element of K10(K11( the carrier of S, the carrier of T));
coherence
for b1 being Function of S,T st b1 is isomorphic holds
( b1 is one-to-one & b1 is monotone ) by Def38;
end;
theorem :: WAYBEL_0:67
for S, T being non empty RelStr
for f being Function of S,T st f is isomorphic holds
( f " is Function of T,S & rng (f ") = the carrier of S )
proof
let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T st f is isomorphic holds
( f " is Function of T,S & rng (f ") = the carrier of S )
let f be Function of S,T; ::_thesis: ( f is isomorphic implies ( f " is Function of T,S & rng (f ") = the carrier of S ) )
assume A1: f is isomorphic ; ::_thesis: ( f " is Function of T,S & rng (f ") = the carrier of S )
then A2: rng f = the carrier of T by Th66;
A3: dom f = the carrier of S by FUNCT_2:def_1;
A4: dom (f ") = the carrier of T by A1, A2, FUNCT_1:33;
rng (f ") = the carrier of S by A1, A3, FUNCT_1:33;
hence ( f " is Function of T,S & rng (f ") = the carrier of S ) by A4, FUNCT_2:1; ::_thesis: verum
end;
theorem :: WAYBEL_0:68
for S, T being non empty RelStr
for f being Function of S,T st f is isomorphic holds
for g being Function of T,S st g = f " holds
g is isomorphic
proof
let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T st f is isomorphic holds
for g being Function of T,S st g = f " holds
g is isomorphic
let f be Function of S,T; ::_thesis: ( f is isomorphic implies for g being Function of T,S st g = f " holds
g is isomorphic )
assume A1: f is isomorphic ; ::_thesis: for g being Function of T,S st g = f " holds
g is isomorphic
then A2: ex h being Function of T,S st
( h = f " & h is monotone ) by Def38;
let g be Function of T,S; ::_thesis: ( g = f " implies g is isomorphic )
assume A3: g = f " ; ::_thesis: g is isomorphic
percases ( ( not T is empty & not S is empty ) or T is empty or S is empty ) ;
:: according to WAYBEL_0:def_38
case ( not T is empty & not S is empty ) ; ::_thesis: ( g is one-to-one & g is monotone & ex g being Function of S,T st
( g = g " & g is monotone ) )
thus ( g is one-to-one & g is monotone ) by A1, A2, A3, FUNCT_1:40; ::_thesis: ex g being Function of S,T st
( g = g " & g is monotone )
(f ") " = f by A1, FUNCT_1:43;
hence ex g being Function of S,T st
( g = g " & g is monotone ) by A1, A3; ::_thesis: verum
end;
case ( T is empty or S is empty ) ; ::_thesis: ( T is empty & S is empty )
hence ( T is empty & S is empty ) ; ::_thesis: verum
end;
end;
end;
theorem Th69: :: WAYBEL_0:69
for S, T being non empty Poset
for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds
f is monotone
proof
let S, T be non empty Poset; ::_thesis: for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds
f is monotone
let f be Function of S,T; ::_thesis: ( ( for X being Filter of S holds f preserves_inf_of X ) implies f is monotone )
assume A1: for X being Filter of S holds f preserves_inf_of X ; ::_thesis: f is monotone
let x, y be Element of S; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 ) )
A2: ex_inf_of {x},S by YELLOW_0:38;
A3: ex_inf_of {y},S by YELLOW_0:38;
A4: f preserves_inf_of uparrow x by A1;
A5: f preserves_inf_of uparrow y by A1;
A6: ex_inf_of uparrow x,S by A2, Th37;
A7: ex_inf_of uparrow y,S by A3, Th37;
A8: ex_inf_of f .: (uparrow x),T by A4, A6, Def30;
A9: ex_inf_of f .: (uparrow y),T by A5, A7, Def30;
A10: inf (f .: (uparrow x)) = f . (inf (uparrow x)) by A4, A6, Def30;
A11: inf (f .: (uparrow y)) = f . (inf (uparrow y)) by A5, A7, Def30;
assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 )
then A12: uparrow y c= uparrow x by Th22;
A13: inf (f .: (uparrow x)) = f . (inf {x}) by A10, Th38, YELLOW_0:38;
A14: inf (f .: (uparrow y)) = f . (inf {y}) by A11, Th38, YELLOW_0:38;
A15: inf (f .: (uparrow x)) = f . x by A13, YELLOW_0:39;
inf (f .: (uparrow y)) = f . y by A14, YELLOW_0:39;
hence for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 ) by A8, A9, A12, A15, RELAT_1:123, YELLOW_0:35; ::_thesis: verum
end;
theorem :: WAYBEL_0:70
for S, T being non empty Poset
for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds
f is filtered-infs-preserving
proof
let S, T be non empty Poset; ::_thesis: for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds
f is filtered-infs-preserving
let f be Function of S,T; ::_thesis: ( ( for X being Filter of S holds f preserves_inf_of X ) implies f is filtered-infs-preserving )
assume A1: for X being Filter of S holds f preserves_inf_of X ; ::_thesis: f is filtered-infs-preserving
let X be Subset of S; :: according to WAYBEL_0:def_36 ::_thesis: ( not X is empty & X is filtered implies f preserves_inf_of X )
assume that
A2: ( not X is empty & X is filtered ) and
A3: ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) )
reconsider Y = X as non empty filtered Subset of S by A2;
uparrow Y is Filter of S ;
then A4: f preserves_inf_of uparrow X by A1;
A5: ex_inf_of uparrow X,S by A3, Th37;
then A6: ex_inf_of f .: (uparrow X),T by A4, Def30;
A7: inf (f .: (uparrow X)) = f . (inf (uparrow X)) by A4, A5, Def30;
A8: inf (uparrow X) = inf X by A3, Th38;
A9: f .: X c= f .: (uparrow X) by Th16, RELAT_1:123;
A10: f .: (uparrow X) is_>=_than f . (inf X) by A6, A7, A8, YELLOW_0:31;
A11: f .: X is_>=_than f . (inf X)
proof
let x be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not x in f .: X or f . (inf X) <= x )
assume x in f .: X ; ::_thesis: f . (inf X) <= x
hence f . (inf X) <= x by A9, A10, LATTICE3:def_8; ::_thesis: verum
end;
A12: now__::_thesis:_for_b_being_Element_of_T_st_f_.:_X_is_>=_than_b_holds_
f_._(inf_X)_>=_b
let b be Element of T; ::_thesis: ( f .: X is_>=_than b implies f . (inf X) >= b )
assume A13: f .: X is_>=_than b ; ::_thesis: f . (inf X) >= b
f .: (uparrow X) is_>=_than b
proof
let a be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not a in f .: (uparrow X) or b <= a )
assume a in f .: (uparrow X) ; ::_thesis: b <= a
then consider x being set such that
x in dom f and
A14: x in uparrow X and
A15: a = f . x by FUNCT_1:def_6;
uparrow X = { z where z is Element of S : ex y being Element of S st
( z >= y & y in X ) } by Th15;
then consider z being Element of S such that
A16: x = z and
A17: ex y being Element of S st
( z >= y & y in X ) by A14;
consider y being Element of S such that
A18: z >= y and
A19: y in X by A17;
A20: f is monotone by A1, Th69;
A21: f . y in f .: X by A19, FUNCT_2:35;
A22: f . z >= f . y by A18, A20, ORDERS_3:def_5;
f . y >= b by A13, A21, LATTICE3:def_8;
hence b <= a by A15, A16, A22, ORDERS_2:3; ::_thesis: verum
end;
hence f . (inf X) >= b by A6, A7, A8, YELLOW_0:31; ::_thesis: verum
end;
hence ex_inf_of f .: X,T by A11, YELLOW_0:16; ::_thesis: inf (f .: X) = f . (inf X)
hence inf (f .: X) = f . (inf X) by A11, A12, YELLOW_0:def_10; ::_thesis: verum
end;
theorem :: WAYBEL_0:71
for S being Semilattice
for T being non empty Poset
for f being Function of S,T st ( for X being finite Subset of S holds f preserves_inf_of X ) & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds
f is infs-preserving
proof
let S be Semilattice; ::_thesis: for T being non empty Poset
for f being Function of S,T st ( for X being finite Subset of S holds f preserves_inf_of X ) & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds
f is infs-preserving
let T be non empty Poset; ::_thesis: for f being Function of S,T st ( for X being finite Subset of S holds f preserves_inf_of X ) & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds
f is infs-preserving
let f be Function of S,T; ::_thesis: ( ( for X being finite Subset of S holds f preserves_inf_of X ) & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) implies f is infs-preserving )
assume that
A1: for X being finite Subset of S holds f preserves_inf_of X and
A2: for X being non empty filtered Subset of S holds f preserves_inf_of X ; ::_thesis: f is infs-preserving
let X be Subset of S; :: according to WAYBEL_0:def_32 ::_thesis: f preserves_inf_of X
assume A3: ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) )
defpred S1[ set ] means ex Y being finite Subset of X st
( ex_inf_of Y,S & $1 = "/\" (Y,S) );
consider Z being set such that
A4: for x being set holds
( x in Z iff ( x in the carrier of S & S1[x] ) ) from XBOOLE_0:sch_1();
Z c= the carrier of S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in the carrier of S )
thus ( not x in Z or x in the carrier of S ) by A4; ::_thesis: verum
end;
then reconsider Z = Z as Subset of S ;
A5: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
ex_inf_of_Y,S
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies ex_inf_of Y,S )
Y is Subset of S by XBOOLE_1:1;
hence ( Y <> {} implies ex_inf_of Y,S ) by YELLOW_0:55; ::_thesis: verum
end;
A6: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
"/\"_(Y,S)_in_Z
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "/\" (Y,S) in Z )
reconsider Y9 = Y as Subset of S by XBOOLE_1:1;
assume Y <> {} ; ::_thesis: "/\" (Y,S) in Z
then ex_inf_of Y9,S by YELLOW_0:55;
hence "/\" (Y,S) in Z by A4; ::_thesis: verum
end;
A7: for x being Element of S st x in Z holds
ex Y being finite Subset of X st
( ex_inf_of Y,S & x = "/\" (Y,S) ) by A4;
then A8: Z is filtered by A5, A6, Th56;
A9: ex_inf_of Z,S by A3, A5, A6, A7, Th58;
( Z = {} or Z <> {} ) ;
then A10: f preserves_inf_of Z by A1, A2, A8;
then A11: ex_inf_of f .: Z,T by A9, Def30;
A12: inf (f .: Z) = f . (inf Z) by A9, A10, Def30;
A13: inf Z = inf X by A3, A5, A6, A7, Th59;
X c= Z
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Z )
assume A14: x in X ; ::_thesis: x in Z
then reconsider Y = {x} as finite Subset of X by ZFMISC_1:31;
reconsider x = x as Element of S by A14;
Y is Subset of S by XBOOLE_1:1;
then A15: ex_inf_of Y,S by YELLOW_0:55;
x = "/\" (Y,S) by YELLOW_0:39;
hence x in Z by A4, A15; ::_thesis: verum
end;
then A16: f .: X c= f .: Z by RELAT_1:123;
A17: f .: Z is_>=_than f . (inf X) by A11, A12, A13, YELLOW_0:31;
A18: f .: X is_>=_than f . (inf X)
proof
let x be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not x in f .: X or f . (inf X) <= x )
assume x in f .: X ; ::_thesis: f . (inf X) <= x
hence f . (inf X) <= x by A16, A17, LATTICE3:def_8; ::_thesis: verum
end;
A19: now__::_thesis:_for_b_being_Element_of_T_st_f_.:_X_is_>=_than_b_holds_
f_._(inf_X)_>=_b
let b be Element of T; ::_thesis: ( f .: X is_>=_than b implies f . (inf X) >= b )
assume A20: f .: X is_>=_than b ; ::_thesis: f . (inf X) >= b
f .: Z is_>=_than b
proof
let a be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not a in f .: Z or b <= a )
assume a in f .: Z ; ::_thesis: b <= a
then consider x being set such that
x in dom f and
A21: x in Z and
A22: a = f . x by FUNCT_1:def_6;
consider Y being finite Subset of X such that
A23: ex_inf_of Y,S and
A24: x = "/\" (Y,S) by A4, A21;
reconsider Y = Y as Subset of S by XBOOLE_1:1;
A25: f .: Y c= f .: X by RELAT_1:123;
A26: f preserves_inf_of Y by A1;
A27: b is_<=_than f .: Y by A20, A25, YELLOW_0:9;
A28: a = "/\" ((f .: Y),T) by A22, A23, A24, A26, Def30;
ex_inf_of f .: Y,T by A23, A26, Def30;
hence b <= a by A27, A28, YELLOW_0:def_10; ::_thesis: verum
end;
hence f . (inf X) >= b by A11, A12, A13, YELLOW_0:31; ::_thesis: verum
end;
hence ex_inf_of f .: X,T by A18, YELLOW_0:16; ::_thesis: inf (f .: X) = f . (inf X)
hence inf (f .: X) = f . (inf X) by A18, A19, YELLOW_0:def_10; ::_thesis: verum
end;
theorem Th72: :: WAYBEL_0:72
for S, T being non empty Poset
for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds
f is monotone
proof
let S, T be non empty Poset; ::_thesis: for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds
f is monotone
let f be Function of S,T; ::_thesis: ( ( for X being Ideal of S holds f preserves_sup_of X ) implies f is monotone )
assume A1: for X being Ideal of S holds f preserves_sup_of X ; ::_thesis: f is monotone
let x, y be Element of S; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 ) )
A2: ex_sup_of {x},S by YELLOW_0:38;
A3: ex_sup_of {y},S by YELLOW_0:38;
A4: f preserves_sup_of downarrow x by A1;
A5: f preserves_sup_of downarrow y by A1;
A6: ex_sup_of downarrow x,S by A2, Th32;
A7: ex_sup_of downarrow y,S by A3, Th32;
A8: ex_sup_of f .: (downarrow x),T by A4, A6, Def31;
A9: ex_sup_of f .: (downarrow y),T by A5, A7, Def31;
A10: sup (f .: (downarrow x)) = f . (sup (downarrow x)) by A4, A6, Def31;
A11: sup (f .: (downarrow y)) = f . (sup (downarrow y)) by A5, A7, Def31;
assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 )
then A12: downarrow x c= downarrow y by Th21;
A13: sup (f .: (downarrow x)) = f . (sup {x}) by A10, Th33, YELLOW_0:38;
A14: sup (f .: (downarrow y)) = f . (sup {y}) by A11, Th33, YELLOW_0:38;
A15: sup (f .: (downarrow x)) = f . x by A13, YELLOW_0:39;
sup (f .: (downarrow y)) = f . y by A14, YELLOW_0:39;
hence for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 ) by A8, A9, A12, A15, RELAT_1:123, YELLOW_0:34; ::_thesis: verum
end;
theorem :: WAYBEL_0:73
for S, T being non empty Poset
for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds
f is directed-sups-preserving
proof
let S, T be non empty Poset; ::_thesis: for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds
f is directed-sups-preserving
let f be Function of S,T; ::_thesis: ( ( for X being Ideal of S holds f preserves_sup_of X ) implies f is directed-sups-preserving )
assume A1: for X being Ideal of S holds f preserves_sup_of X ; ::_thesis: f is directed-sups-preserving
let X be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( not X is empty & X is directed implies f preserves_sup_of X )
assume that
A2: ( not X is empty & X is directed ) and
A3: ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) )
reconsider Y = X as non empty directed Subset of S by A2;
downarrow Y is Ideal of S ;
then A4: f preserves_sup_of downarrow X by A1;
A5: ex_sup_of downarrow X,S by A3, Th32;
then A6: ex_sup_of f .: (downarrow X),T by A4, Def31;
A7: sup (f .: (downarrow X)) = f . (sup (downarrow X)) by A4, A5, Def31;
A8: sup (downarrow X) = sup X by A3, Th33;
A9: f .: X c= f .: (downarrow X) by Th16, RELAT_1:123;
A10: f .: (downarrow X) is_<=_than f . (sup X) by A6, A7, A8, YELLOW_0:30;
A11: f .: X is_<=_than f . (sup X)
proof
let x be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not x in f .: X or x <= f . (sup X) )
assume x in f .: X ; ::_thesis: x <= f . (sup X)
hence x <= f . (sup X) by A9, A10, LATTICE3:def_9; ::_thesis: verum
end;
A12: now__::_thesis:_for_b_being_Element_of_T_st_f_.:_X_is_<=_than_b_holds_
f_._(sup_X)_<=_b
let b be Element of T; ::_thesis: ( f .: X is_<=_than b implies f . (sup X) <= b )
assume A13: f .: X is_<=_than b ; ::_thesis: f . (sup X) <= b
f .: (downarrow X) is_<=_than b
proof
let a be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not a in f .: (downarrow X) or a <= b )
assume a in f .: (downarrow X) ; ::_thesis: a <= b
then consider x being set such that
x in dom f and
A14: x in downarrow X and
A15: a = f . x by FUNCT_1:def_6;
downarrow X = { z where z is Element of S : ex y being Element of S st
( z <= y & y in X ) } by Th14;
then consider z being Element of S such that
A16: x = z and
A17: ex y being Element of S st
( z <= y & y in X ) by A14;
consider y being Element of S such that
A18: z <= y and
A19: y in X by A17;
A20: f is monotone by A1, Th72;
A21: f . y in f .: X by A19, FUNCT_2:35;
A22: f . z <= f . y by A18, A20, ORDERS_3:def_5;
f . y <= b by A13, A21, LATTICE3:def_9;
hence a <= b by A15, A16, A22, ORDERS_2:3; ::_thesis: verum
end;
hence f . (sup X) <= b by A6, A7, A8, YELLOW_0:30; ::_thesis: verum
end;
hence ex_sup_of f .: X,T by A11, YELLOW_0:15; ::_thesis: sup (f .: X) = f . (sup X)
hence sup (f .: X) = f . (sup X) by A11, A12, YELLOW_0:def_9; ::_thesis: verum
end;
theorem :: WAYBEL_0:74
for S being sup-Semilattice
for T being non empty Poset
for f being Function of S,T st ( for X being finite Subset of S holds f preserves_sup_of X ) & ( for X being non empty directed Subset of S holds f preserves_sup_of X ) holds
f is sups-preserving
proof
let S be sup-Semilattice; ::_thesis: for T being non empty Poset
for f being Function of S,T st ( for X being finite Subset of S holds f preserves_sup_of X ) & ( for X being non empty directed Subset of S holds f preserves_sup_of X ) holds
f is sups-preserving
let T be non empty Poset; ::_thesis: for f being Function of S,T st ( for X being finite Subset of S holds f preserves_sup_of X ) & ( for X being non empty directed Subset of S holds f preserves_sup_of X ) holds
f is sups-preserving
let f be Function of S,T; ::_thesis: ( ( for X being finite Subset of S holds f preserves_sup_of X ) & ( for X being non empty directed Subset of S holds f preserves_sup_of X ) implies f is sups-preserving )
assume that
A1: for X being finite Subset of S holds f preserves_sup_of X and
A2: for X being non empty directed Subset of S holds f preserves_sup_of X ; ::_thesis: f is sups-preserving
let X be Subset of S; :: according to WAYBEL_0:def_33 ::_thesis: f preserves_sup_of X
assume A3: ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) )
defpred S1[ set ] means ex Y being finite Subset of X st
( ex_sup_of Y,S & $1 = "\/" (Y,S) );
consider Z being set such that
A4: for x being set holds
( x in Z iff ( x in the carrier of S & S1[x] ) ) from XBOOLE_0:sch_1();
Z c= the carrier of S
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in the carrier of S )
thus ( not x in Z or x in the carrier of S ) by A4; ::_thesis: verum
end;
then reconsider Z = Z as Subset of S ;
A5: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
ex_sup_of_Y,S
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies ex_sup_of Y,S )
Y is Subset of S by XBOOLE_1:1;
hence ( Y <> {} implies ex_sup_of Y,S ) by YELLOW_0:54; ::_thesis: verum
end;
A6: now__::_thesis:_for_Y_being_finite_Subset_of_X_st_Y_<>_{}_holds_
"\/"_(Y,S)_in_Z
let Y be finite Subset of X; ::_thesis: ( Y <> {} implies "\/" (Y,S) in Z )
reconsider Y9 = Y as Subset of S by XBOOLE_1:1;
assume Y <> {} ; ::_thesis: "\/" (Y,S) in Z
then ex_sup_of Y9,S by YELLOW_0:54;
hence "\/" (Y,S) in Z by A4; ::_thesis: verum
end;
A7: for x being Element of S st x in Z holds
ex Y being finite Subset of X st
( ex_sup_of Y,S & x = "\/" (Y,S) ) by A4;
then A8: Z is directed by A5, A6, Th51;
A9: ex_sup_of Z,S by A3, A5, A6, A7, Th53;
( Z = {} or Z <> {} ) ;
then A10: f preserves_sup_of Z by A1, A2, A8;
then A11: ex_sup_of f .: Z,T by A9, Def31;
A12: sup (f .: Z) = f . (sup Z) by A9, A10, Def31;
A13: sup Z = sup X by A3, A5, A6, A7, Th54;
X c= Z
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Z )
assume A14: x in X ; ::_thesis: x in Z
then reconsider Y = {x} as finite Subset of X by ZFMISC_1:31;
reconsider x = x as Element of S by A14;
Y is Subset of S by XBOOLE_1:1;
then A15: ex_sup_of Y,S by YELLOW_0:54;
x = "\/" (Y,S) by YELLOW_0:39;
hence x in Z by A4, A15; ::_thesis: verum
end;
then A16: f .: X c= f .: Z by RELAT_1:123;
A17: f .: Z is_<=_than f . (sup X) by A11, A12, A13, YELLOW_0:30;
A18: f .: X is_<=_than f . (sup X)
proof
let x be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not x in f .: X or x <= f . (sup X) )
assume x in f .: X ; ::_thesis: x <= f . (sup X)
hence x <= f . (sup X) by A16, A17, LATTICE3:def_9; ::_thesis: verum
end;
A19: now__::_thesis:_for_b_being_Element_of_T_st_f_.:_X_is_<=_than_b_holds_
f_._(sup_X)_<=_b
let b be Element of T; ::_thesis: ( f .: X is_<=_than b implies f . (sup X) <= b )
assume A20: f .: X is_<=_than b ; ::_thesis: f . (sup X) <= b
f .: Z is_<=_than b
proof
let a be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not a in f .: Z or a <= b )
assume a in f .: Z ; ::_thesis: a <= b
then consider x being set such that
x in dom f and
A21: x in Z and
A22: a = f . x by FUNCT_1:def_6;
consider Y being finite Subset of X such that
A23: ex_sup_of Y,S and
A24: x = "\/" (Y,S) by A4, A21;
reconsider Y = Y as Subset of S by XBOOLE_1:1;
A25: f .: Y c= f .: X by RELAT_1:123;
A26: f preserves_sup_of Y by A1;
A27: b is_>=_than f .: Y by A20, A25, YELLOW_0:9;
A28: a = "\/" ((f .: Y),T) by A22, A23, A24, A26, Def31;
ex_sup_of f .: Y,T by A23, A26, Def31;
hence a <= b by A27, A28, YELLOW_0:def_9; ::_thesis: verum
end;
hence f . (sup X) <= b by A11, A12, A13, YELLOW_0:30; ::_thesis: verum
end;
hence ex_sup_of f .: X,T by A18, YELLOW_0:15; ::_thesis: sup (f .: X) = f . (sup X)
hence sup (f .: X) = f . (sup X) by A18, A19, YELLOW_0:def_9; ::_thesis: verum
end;
begin
definition
let L be non empty reflexive RelStr ;
attrL is up-complete means :Def39: :: WAYBEL_0:def 39
for X being non empty directed Subset of L ex x being Element of L st
( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds
x <= y ) );
end;
:: deftheorem Def39 defines up-complete WAYBEL_0:def_39_:_
for L being non empty reflexive RelStr holds
( L is up-complete iff for X being non empty directed Subset of L ex x being Element of L st
( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds
x <= y ) ) );
registration
cluster reflexive with_suprema up-complete -> reflexive with_suprema upper-bounded for RelStr ;
coherence
for b1 being reflexive with_suprema RelStr st b1 is up-complete holds
b1 is upper-bounded
proof
let L be reflexive with_suprema RelStr ; ::_thesis: ( L is up-complete implies L is upper-bounded )
assume A1: L is up-complete ; ::_thesis: L is upper-bounded
[#] L = the carrier of L ;
then ex x being Element of L st
( x is_>=_than the carrier of L & ( for y being Element of L st y is_>=_than the carrier of L holds
x <= y ) ) by A1, Def39;
hence ex x being Element of L st x is_>=_than the carrier of L ; :: according to YELLOW_0:def_5 ::_thesis: verum
end;
end;
theorem :: WAYBEL_0:75
for L being non empty reflexive antisymmetric RelStr holds
( L is up-complete iff for X being non empty directed Subset of L holds ex_sup_of X,L )
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: ( L is up-complete iff for X being non empty directed Subset of L holds ex_sup_of X,L )
hereby ::_thesis: ( ( for X being non empty directed Subset of L holds ex_sup_of X,L ) implies L is up-complete )
assume A1: L is up-complete ; ::_thesis: for X being non empty directed Subset of L holds ex_sup_of X,L
let X be non empty directed Subset of L; ::_thesis: ex_sup_of X,L
consider x being Element of L such that
A2: x is_>=_than X and
A3: for y being Element of L st y is_>=_than X holds
x <= y by A1, Def39;
thus ex_sup_of X,L ::_thesis: verum
proof
take x ; :: according to YELLOW_0:def_7 ::_thesis: ( X is_<=_than x & ( for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or x <= b1 ) ) & ( for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or ex b2 being Element of the carrier of L st
( X is_<=_than b2 & not b1 <= b2 ) or b1 = x ) ) )
thus ( X is_<=_than x & ( for b being Element of L st X is_<=_than b holds
b >= x ) ) by A2, A3; ::_thesis: for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or ex b2 being Element of the carrier of L st
( X is_<=_than b2 & not b1 <= b2 ) or b1 = x )
let c be Element of L; ::_thesis: ( not X is_<=_than c or ex b1 being Element of the carrier of L st
( X is_<=_than b1 & not c <= b1 ) or c = x )
assume that
A4: X is_<=_than c and
A5: for b being Element of L st X is_<=_than b holds
b >= c ; ::_thesis: c = x
A6: c <= x by A2, A5;
c >= x by A3, A4;
hence c = x by A6, ORDERS_2:2; ::_thesis: verum
end;
end;
assume A7: for X being non empty directed Subset of L holds ex_sup_of X,L ; ::_thesis: L is up-complete
let X be non empty directed Subset of L; :: according to WAYBEL_0:def_39 ::_thesis: ex x being Element of L st
( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds
x <= y ) )
ex_sup_of X,L by A7;
then ex a being Element of L st
( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds
b >= a ) & ( for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds
b >= c ) holds
c = a ) ) by YELLOW_0:def_7;
hence ex x being Element of L st
( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds
x <= y ) ) ; ::_thesis: verum
end;
definition
let L be non empty reflexive RelStr ;
attrL is /\-complete means :Def40: :: WAYBEL_0:def 40
for X being non empty Subset of L ex x being Element of L st
( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds
x >= y ) );
end;
:: deftheorem Def40 defines /\-complete WAYBEL_0:def_40_:_
for L being non empty reflexive RelStr holds
( L is /\-complete iff for X being non empty Subset of L ex x being Element of L st
( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds
x >= y ) ) );
theorem Th76: :: WAYBEL_0:76
for L being non empty reflexive antisymmetric RelStr holds
( L is /\-complete iff for X being non empty Subset of L holds ex_inf_of X,L )
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: ( L is /\-complete iff for X being non empty Subset of L holds ex_inf_of X,L )
hereby ::_thesis: ( ( for X being non empty Subset of L holds ex_inf_of X,L ) implies L is /\-complete )
assume A1: L is /\-complete ; ::_thesis: for X being non empty Subset of L holds ex_inf_of X,L
let X be non empty Subset of L; ::_thesis: ex_inf_of X,L
consider x being Element of L such that
A2: x is_<=_than X and
A3: for y being Element of L st y is_<=_than X holds
x >= y by A1, Def40;
thus ex_inf_of X,L ::_thesis: verum
proof
take x ; :: according to YELLOW_0:def_8 ::_thesis: ( x is_<=_than X & ( for b1 being Element of the carrier of L holds
( not b1 is_<=_than X or b1 <= x ) ) & ( for b1 being Element of the carrier of L holds
( not b1 is_<=_than X or ex b2 being Element of the carrier of L st
( b2 is_<=_than X & not b2 <= b1 ) or b1 = x ) ) )
thus ( X is_>=_than x & ( for b being Element of L st X is_>=_than b holds
b <= x ) ) by A2, A3; ::_thesis: for b1 being Element of the carrier of L holds
( not b1 is_<=_than X or ex b2 being Element of the carrier of L st
( b2 is_<=_than X & not b2 <= b1 ) or b1 = x )
let c be Element of L; ::_thesis: ( not c is_<=_than X or ex b1 being Element of the carrier of L st
( b1 is_<=_than X & not b1 <= c ) or c = x )
assume that
A4: X is_>=_than c and
A5: for b being Element of L st X is_>=_than b holds
b <= c ; ::_thesis: c = x
A6: c <= x by A3, A4;
c >= x by A2, A5;
hence c = x by A6, ORDERS_2:2; ::_thesis: verum
end;
end;
assume A7: for X being non empty Subset of L holds ex_inf_of X,L ; ::_thesis: L is /\-complete
let X be non empty Subset of L; :: according to WAYBEL_0:def_40 ::_thesis: ex x being Element of L st
( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds
x >= y ) )
ex_inf_of X,L by A7;
then ex a being Element of L st
( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds
b <= a ) & ( for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds
b <= c ) holds
c = a ) ) by YELLOW_0:def_8;
hence ex x being Element of L st
( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds
x >= y ) ) ; ::_thesis: verum
end;
registration
cluster non empty reflexive complete -> non empty reflexive up-complete /\-complete for RelStr ;
coherence
for b1 being non empty reflexive RelStr st b1 is complete holds
( b1 is up-complete & b1 is /\-complete )
proof
let L be non empty reflexive RelStr ; ::_thesis: ( L is complete implies ( L is up-complete & L is /\-complete ) )
assume A1: L is complete ; ::_thesis: ( L is up-complete & L is /\-complete )
thus L is up-complete ::_thesis: L is /\-complete
proof
let X be non empty directed Subset of L; :: according to WAYBEL_0:def_39 ::_thesis: ex x being Element of L st
( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds
x <= y ) )
thus ex x being Element of L st
( x is_>=_than X & ( for y being Element of L st y is_>=_than X holds
x <= y ) ) by A1, LATTICE3:def_12; ::_thesis: verum
end;
let X be non empty Subset of L; :: according to WAYBEL_0:def_40 ::_thesis: ex x being Element of L st
( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds
x >= y ) )
set Y = { y where y is Element of L : y is_<=_than X } ;
consider x being Element of L such that
A2: { y where y is Element of L : y is_<=_than X } is_<=_than x and
A3: for b being Element of L st { y where y is Element of L : y is_<=_than X } is_<=_than b holds
x <= b by A1, LATTICE3:def_12;
take x ; ::_thesis: ( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds
x >= y ) )
thus x is_<=_than X ::_thesis: for y being Element of L st y is_<=_than X holds
x >= y
proof
let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in X or x <= y )
assume A4: y in X ; ::_thesis: x <= y
y is_>=_than { y where y is Element of L : y is_<=_than X }
proof
let z be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not z in { y where y is Element of L : y is_<=_than X } or z <= y )
assume z in { y where y is Element of L : y is_<=_than X } ; ::_thesis: z <= y
then ex a being Element of L st
( z = a & a is_<=_than X ) ;
hence z <= y by A4, LATTICE3:def_8; ::_thesis: verum
end;
hence x <= y by A3; ::_thesis: verum
end;
let y be Element of L; ::_thesis: ( y is_<=_than X implies x >= y )
assume y is_<=_than X ; ::_thesis: x >= y
then y in { y where y is Element of L : y is_<=_than X } ;
hence x >= y by A2, LATTICE3:def_9; ::_thesis: verum
end;
cluster non empty reflexive /\-complete -> non empty reflexive lower-bounded for RelStr ;
coherence
for b1 being non empty reflexive RelStr st b1 is /\-complete holds
b1 is lower-bounded
proof
let L be non empty reflexive RelStr ; ::_thesis: ( L is /\-complete implies L is lower-bounded )
assume L is /\-complete ; ::_thesis: L is lower-bounded
then ex x being Element of L st
( x is_<=_than [#] L & ( for y being Element of L st y is_<=_than [#] L holds
x >= y ) ) by Def40;
hence ex x being Element of L st x is_<=_than the carrier of L ; :: according to YELLOW_0:def_4 ::_thesis: verum
end;
cluster non empty reflexive transitive antisymmetric with_suprema lower-bounded up-complete -> non empty complete for RelStr ;
coherence
for b1 being non empty Poset st b1 is up-complete & b1 is with_suprema & b1 is lower-bounded holds
b1 is complete
proof
let L be non empty Poset; ::_thesis: ( L is up-complete & L is with_suprema & L is lower-bounded implies L is complete )
assume A5: ( L is up-complete & L is with_suprema & L is lower-bounded ) ; ::_thesis: L is complete
then reconsider K = L as non empty with_suprema lower-bounded Poset ;
let X be set ; :: according to LATTICE3:def_12 ::_thesis: ex b1 being Element of the carrier of L st
( X is_<=_than b1 & ( for b2 being Element of the carrier of L holds
( not X is_<=_than b2 or b1 <= b2 ) ) )
reconsider X9 = X /\ the carrier of L as Subset of L by XBOOLE_1:17;
reconsider A = X9 as Subset of K ;
A6: now__::_thesis:_for_Y_being_finite_Subset_of_X9_st_Y_<>_{}_holds_
ex_sup_of_Y,L
let Y be finite Subset of X9; ::_thesis: ( Y <> {} implies ex_sup_of Y,L )
Y c= the carrier of L by XBOOLE_1:1;
hence ( Y <> {} implies ex_sup_of Y,L ) by A5, YELLOW_0:54; ::_thesis: verum
end;
A7: now__::_thesis:_for_x_being_Element_of_L_st_x_in_finsups_X9_holds_
ex_Y_being_finite_Subset_of_X9_st_
(_ex_sup_of_Y,L_&_x_=_"\/"_(Y,L)_)
let x be Element of L; ::_thesis: ( x in finsups X9 implies ex Y being finite Subset of X9 st
( ex_sup_of Y,L & x = "\/" (Y,L) ) )
assume x in finsups X9 ; ::_thesis: ex Y being finite Subset of X9 st
( ex_sup_of Y,L & x = "\/" (Y,L) )
then ex Y being finite Subset of X9 st
( x = "\/" (Y,L) & ex_sup_of Y,L ) ;
hence ex Y being finite Subset of X9 st
( ex_sup_of Y,L & x = "\/" (Y,L) ) ; ::_thesis: verum
end;
A8: now__::_thesis:_for_Y_being_finite_Subset_of_X9_st_Y_<>_{}_holds_
"\/"_(Y,L)_in_finsups_X9
let Y be finite Subset of X9; ::_thesis: ( Y <> {} implies "\/" (Y,L) in finsups X9 )
reconsider Z = Y as Subset of L by XBOOLE_1:1;
assume Y <> {} ; ::_thesis: "\/" (Y,L) in finsups X9
then ex_sup_of Z,L by A5, YELLOW_0:54;
hence "\/" (Y,L) in finsups X9 ; ::_thesis: verum
end;
reconsider fX = finsups A as non empty directed Subset of L ;
consider x being Element of L such that
A9: fX is_<=_than x and
A10: for y being Element of L st fX is_<=_than y holds
x <= y by A5, Def39;
take x ; ::_thesis: ( X is_<=_than x & ( for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or x <= b1 ) ) )
X9 is_<=_than x by A6, A7, A8, A9, Th52;
hence X is_<=_than x by YELLOW_0:5; ::_thesis: for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or x <= b1 )
let y be Element of L; ::_thesis: ( not X is_<=_than y or x <= y )
assume y is_>=_than X ; ::_thesis: x <= y
then y is_>=_than X9 by YELLOW_0:5;
then y is_>=_than fX by A6, A7, A8, Th52;
hence x <= y by A10; ::_thesis: verum
end;
end;
registration
cluster non empty reflexive antisymmetric /\-complete -> non empty reflexive antisymmetric with_infima for RelStr ;
coherence
for b1 being non empty reflexive antisymmetric RelStr st b1 is /\-complete holds
b1 is with_infima
proof
let L be non empty reflexive antisymmetric RelStr ; ::_thesis: ( L is /\-complete implies L is with_infima )
assume L is /\-complete ; ::_thesis: L is with_infima
then for a, b being Element of L holds ex_inf_of {a,b},L by Th76;
hence L is with_infima by YELLOW_0:21; ::_thesis: verum
end;
end;
registration
cluster non empty reflexive antisymmetric upper-bounded /\-complete -> non empty reflexive antisymmetric with_suprema upper-bounded for RelStr ;
coherence
for b1 being non empty reflexive antisymmetric upper-bounded RelStr st b1 is /\-complete holds
b1 is with_suprema
proof
let L be non empty reflexive antisymmetric upper-bounded RelStr ; ::_thesis: ( L is /\-complete implies L is with_suprema )
assume A1: L is /\-complete ; ::_thesis: L is with_suprema
now__::_thesis:_for_a,_b_being_Element_of_L_holds_ex_sup_of_{a,b},L
let a, b be Element of L; ::_thesis: ex_sup_of {a,b},L
set X = { x where x is Element of L : ( x >= a & x >= b ) } ;
{ x where x is Element of L : ( x >= a & x >= b ) } c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { x where x is Element of L : ( x >= a & x >= b ) } or x in the carrier of L )
assume x in { x where x is Element of L : ( x >= a & x >= b ) } ; ::_thesis: x in the carrier of L
then ex z being Element of L st
( x = z & z >= a & z >= b ) ;
hence x in the carrier of L ; ::_thesis: verum
end;
then reconsider X = { x where x is Element of L : ( x >= a & x >= b ) } as Subset of L ;
A2: Top L >= a by YELLOW_0:45;
Top L >= b by YELLOW_0:45;
then Top L in X by A2;
then ex_inf_of X,L by A1, Th76;
then consider c being Element of L such that
A3: c is_<=_than X and
A4: for d being Element of L st d is_<=_than X holds
d <= c and
for e being Element of L st e is_<=_than X & ( for d being Element of L st d is_<=_than X holds
d <= e ) holds
e = c by YELLOW_0:def_8;
A5: c is_>=_than {a,b}
proof
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in {a,b} or x <= c )
assume A6: x in {a,b} ; ::_thesis: x <= c
x is_<=_than X
proof
let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in X or x <= y )
assume y in X ; ::_thesis: x <= y
then ex z being Element of L st
( y = z & z >= a & z >= b ) ;
hence x <= y by A6, TARSKI:def_2; ::_thesis: verum
end;
hence x <= c by A4; ::_thesis: verum
end;
now__::_thesis:_for_y_being_Element_of_L_st_y_is_>=_than_{a,b}_holds_
c_<=_y
let y be Element of L; ::_thesis: ( y is_>=_than {a,b} implies c <= y )
assume A7: y is_>=_than {a,b} ; ::_thesis: c <= y
then A8: y >= a by YELLOW_0:8;
y >= b by A7, YELLOW_0:8;
then y in X by A8;
hence c <= y by A3, LATTICE3:def_8; ::_thesis: verum
end;
hence ex_sup_of {a,b},L by A5, YELLOW_0:15; ::_thesis: verum
end;
hence L is with_suprema by YELLOW_0:20; ::_thesis: verum
end;
end;
registration
cluster non empty strict V58() reflexive transitive antisymmetric with_suprema with_infima complete for RelStr ;
existence
ex b1 being LATTICE st
( b1 is complete & b1 is strict )
proof
set L = the strict complete LATTICE;
take the strict complete LATTICE ; ::_thesis: ( the strict complete LATTICE is complete & the strict complete LATTICE is strict )
thus ( the strict complete LATTICE is complete & the strict complete LATTICE is strict ) ; ::_thesis: verum
end;
end;