:: YELLOW_2 semantic presentation
begin
theorem :: YELLOW_2:1
for L being non empty RelStr
for x being Element of L
for X being Subset of L holds
( X c= downarrow x iff X is_<=_than x )
proof
let L be non empty RelStr ; ::_thesis: for x being Element of L
for X being Subset of L holds
( X c= downarrow x iff X is_<=_than x )
let x be Element of L; ::_thesis: for X being Subset of L holds
( X c= downarrow x iff X is_<=_than x )
let X be Subset of L; ::_thesis: ( X c= downarrow x iff X is_<=_than x )
hereby ::_thesis: ( X is_<=_than x implies X c= downarrow x )
assume A1: X c= downarrow x ; ::_thesis: X is_<=_than x
thus X is_<=_than x ::_thesis: verum
proof
let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in X or a <= x )
assume a in X ; ::_thesis: a <= x
hence a <= x by A1, WAYBEL_0:17; ::_thesis: verum
end;
end;
assume A2: for a being Element of L st a in X holds
a <= x ; :: according to LATTICE3:def_9 ::_thesis: X c= downarrow x
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in downarrow x )
assume A3: a in X ; ::_thesis: a in downarrow x
then reconsider a = a as Element of L ;
a <= x by A2, A3;
hence a in downarrow x by WAYBEL_0:17; ::_thesis: verum
end;
theorem :: YELLOW_2:2
for L being non empty RelStr
for x being Element of L
for X being Subset of L holds
( X c= uparrow x iff x is_<=_than X )
proof
let L be non empty RelStr ; ::_thesis: for x being Element of L
for X being Subset of L holds
( X c= uparrow x iff x is_<=_than X )
let x be Element of L; ::_thesis: for X being Subset of L holds
( X c= uparrow x iff x is_<=_than X )
let X be Subset of L; ::_thesis: ( X c= uparrow x iff x is_<=_than X )
hereby ::_thesis: ( x is_<=_than X implies X c= uparrow x )
assume A1: X c= uparrow x ; ::_thesis: x is_<=_than X
thus x is_<=_than X ::_thesis: verum
proof
let a be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not a in X or x <= a )
assume a in X ; ::_thesis: x <= a
hence x <= a by A1, WAYBEL_0:18; ::_thesis: verum
end;
end;
assume A2: for a being Element of L st a in X holds
x <= a ; :: according to LATTICE3:def_8 ::_thesis: X c= uparrow x
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in uparrow x )
assume A3: a in X ; ::_thesis: a in uparrow x
then reconsider a = a as Element of L ;
x <= a by A2, A3;
hence a in uparrow x by WAYBEL_0:18; ::_thesis: verum
end;
theorem :: YELLOW_2:3
for L being transitive antisymmetric with_suprema RelStr
for X, Y being set st ex_sup_of X,L & ex_sup_of Y,L holds
( ex_sup_of X \/ Y,L & "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) )
proof
let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for X, Y being set st ex_sup_of X,L & ex_sup_of Y,L holds
( ex_sup_of X \/ Y,L & "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) )
let X, Y be set ; ::_thesis: ( ex_sup_of X,L & ex_sup_of Y,L implies ( ex_sup_of X \/ Y,L & "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) ) )
assume that
A1: ex_sup_of X,L and
A2: ex_sup_of Y,L ; ::_thesis: ( ex_sup_of X \/ Y,L & "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) )
set a = ("\/" (X,L)) "\/" ("\/" (Y,L));
A3: X \/ Y is_<=_than ("\/" (X,L)) "\/" ("\/" (Y,L))
proof
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X \/ Y or x <= ("\/" (X,L)) "\/" ("\/" (Y,L)) )
assume A4: x in X \/ Y ; ::_thesis: x <= ("\/" (X,L)) "\/" ("\/" (Y,L))
percases ( x in X or x in Y ) by A4, XBOOLE_0:def_3;
supposeA5: x in X ; ::_thesis: x <= ("\/" (X,L)) "\/" ("\/" (Y,L))
X is_<=_than "\/" (X,L) by A1, YELLOW_0:30;
then A6: x <= "\/" (X,L) by A5, LATTICE3:def_9;
"\/" (X,L) <= ("\/" (X,L)) "\/" ("\/" (Y,L)) by YELLOW_0:22;
hence x <= ("\/" (X,L)) "\/" ("\/" (Y,L)) by A6, ORDERS_2:3; ::_thesis: verum
end;
supposeA7: x in Y ; ::_thesis: x <= ("\/" (X,L)) "\/" ("\/" (Y,L))
Y is_<=_than "\/" (Y,L) by A2, YELLOW_0:30;
then A8: x <= "\/" (Y,L) by A7, LATTICE3:def_9;
"\/" (Y,L) <= ("\/" (X,L)) "\/" ("\/" (Y,L)) by YELLOW_0:22;
hence x <= ("\/" (X,L)) "\/" ("\/" (Y,L)) by A8, ORDERS_2:3; ::_thesis: verum
end;
end;
end;
for b being Element of L st X \/ Y is_<=_than b holds
("\/" (X,L)) "\/" ("\/" (Y,L)) <= b
proof
let b be Element of L; ::_thesis: ( X \/ Y is_<=_than b implies ("\/" (X,L)) "\/" ("\/" (Y,L)) <= b )
assume A9: X \/ Y is_<=_than b ; ::_thesis: ("\/" (X,L)) "\/" ("\/" (Y,L)) <= b
Y c= X \/ Y by XBOOLE_1:7;
then Y is_<=_than b by A9, YELLOW_0:9;
then A10: "\/" (Y,L) <= b by A2, YELLOW_0:30;
X c= X \/ Y by XBOOLE_1:7;
then X is_<=_than b by A9, YELLOW_0:9;
then "\/" (X,L) <= b by A1, YELLOW_0:30;
hence ("\/" (X,L)) "\/" ("\/" (Y,L)) <= b by A10, YELLOW_0:22; ::_thesis: verum
end;
hence ( ex_sup_of X \/ Y,L & "\/" ((X \/ Y),L) = ("\/" (X,L)) "\/" ("\/" (Y,L)) ) by A3, YELLOW_0:30; ::_thesis: verum
end;
theorem :: YELLOW_2:4
for L being transitive antisymmetric with_infima RelStr
for X, Y being set st ex_inf_of X,L & ex_inf_of Y,L holds
( ex_inf_of X \/ Y,L & "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) )
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for X, Y being set st ex_inf_of X,L & ex_inf_of Y,L holds
( ex_inf_of X \/ Y,L & "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) )
let X, Y be set ; ::_thesis: ( ex_inf_of X,L & ex_inf_of Y,L implies ( ex_inf_of X \/ Y,L & "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) ) )
assume that
A1: ex_inf_of X,L and
A2: ex_inf_of Y,L ; ::_thesis: ( ex_inf_of X \/ Y,L & "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) )
set a = ("/\" (X,L)) "/\" ("/\" (Y,L));
A3: X \/ Y is_>=_than ("/\" (X,L)) "/\" ("/\" (Y,L))
proof
let x be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not x in X \/ Y or ("/\" (X,L)) "/\" ("/\" (Y,L)) <= x )
assume A4: x in X \/ Y ; ::_thesis: ("/\" (X,L)) "/\" ("/\" (Y,L)) <= x
percases ( x in X or x in Y ) by A4, XBOOLE_0:def_3;
supposeA5: x in X ; ::_thesis: ("/\" (X,L)) "/\" ("/\" (Y,L)) <= x
X is_>=_than "/\" (X,L) by A1, YELLOW_0:31;
then A6: x >= "/\" (X,L) by A5, LATTICE3:def_8;
"/\" (X,L) >= ("/\" (X,L)) "/\" ("/\" (Y,L)) by YELLOW_0:23;
hence ("/\" (X,L)) "/\" ("/\" (Y,L)) <= x by A6, ORDERS_2:3; ::_thesis: verum
end;
supposeA7: x in Y ; ::_thesis: ("/\" (X,L)) "/\" ("/\" (Y,L)) <= x
Y is_>=_than "/\" (Y,L) by A2, YELLOW_0:31;
then A8: x >= "/\" (Y,L) by A7, LATTICE3:def_8;
"/\" (Y,L) >= ("/\" (X,L)) "/\" ("/\" (Y,L)) by YELLOW_0:23;
hence ("/\" (X,L)) "/\" ("/\" (Y,L)) <= x by A8, ORDERS_2:3; ::_thesis: verum
end;
end;
end;
for b being Element of L st X \/ Y is_>=_than b holds
("/\" (X,L)) "/\" ("/\" (Y,L)) >= b
proof
let b be Element of L; ::_thesis: ( X \/ Y is_>=_than b implies ("/\" (X,L)) "/\" ("/\" (Y,L)) >= b )
assume A9: X \/ Y is_>=_than b ; ::_thesis: ("/\" (X,L)) "/\" ("/\" (Y,L)) >= b
Y c= X \/ Y by XBOOLE_1:7;
then Y is_>=_than b by A9, YELLOW_0:9;
then A10: "/\" (Y,L) >= b by A2, YELLOW_0:31;
X c= X \/ Y by XBOOLE_1:7;
then X is_>=_than b by A9, YELLOW_0:9;
then "/\" (X,L) >= b by A1, YELLOW_0:31;
hence ("/\" (X,L)) "/\" ("/\" (Y,L)) >= b by A10, YELLOW_0:23; ::_thesis: verum
end;
hence ( ex_inf_of X \/ Y,L & "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) ) by A3, YELLOW_0:31; ::_thesis: verum
end;
begin
theorem Th5: :: YELLOW_2:5
for R being Relation
for X, Y being set st X c= Y holds
R |_2 X c= R |_2 Y
proof
let R be Relation; ::_thesis: for X, Y being set st X c= Y holds
R |_2 X c= R |_2 Y
let X, Y be set ; ::_thesis: ( X c= Y implies R |_2 X c= R |_2 Y )
assume A1: X c= Y ; ::_thesis: R |_2 X c= R |_2 Y
then X |` R c= Y |` R by RELAT_1:100;
then A2: (X |` R) | X c= (Y |` R) | X by RELAT_1:76;
(Y |` R) | X c= (Y |` R) | Y by A1, RELAT_1:75;
then (X |` R) | X c= (Y |` R) | Y by A2, XBOOLE_1:1;
then R |_2 X c= (Y |` R) | Y by WELLORD1:10;
hence R |_2 X c= R |_2 Y by WELLORD1:10; ::_thesis: verum
end;
theorem :: YELLOW_2:6
for L being RelStr
for S, T being full SubRelStr of L st the carrier of S c= the carrier of T holds
the InternalRel of S c= the InternalRel of T
proof
let L be RelStr ; ::_thesis: for S, T being full SubRelStr of L st the carrier of S c= the carrier of T holds
the InternalRel of S c= the InternalRel of T
let S1, S2 be full SubRelStr of L; ::_thesis: ( the carrier of S1 c= the carrier of S2 implies the InternalRel of S1 c= the InternalRel of S2 )
( the InternalRel of S1 = the InternalRel of L |_2 the carrier of S1 & the InternalRel of S2 = the InternalRel of L |_2 the carrier of S2 ) by YELLOW_0:def_14;
hence ( the carrier of S1 c= the carrier of S2 implies the InternalRel of S1 c= the InternalRel of S2 ) by Th5; ::_thesis: verum
end;
theorem Th7: :: YELLOW_2:7
for X being set
for L being non empty RelStr
for S being non empty SubRelStr of L holds
( ( X is directed Subset of S implies X is directed Subset of L ) & ( X is filtered Subset of S implies X is filtered Subset of L ) )
proof
let X be set ; ::_thesis: for L being non empty RelStr
for S being non empty SubRelStr of L holds
( ( X is directed Subset of S implies X is directed Subset of L ) & ( X is filtered Subset of S implies X is filtered Subset of L ) )
let L be non empty RelStr ; ::_thesis: for S being non empty SubRelStr of L holds
( ( X is directed Subset of S implies X is directed Subset of L ) & ( X is filtered Subset of S implies X is filtered Subset of L ) )
let S be non empty SubRelStr of L; ::_thesis: ( ( X is directed Subset of S implies X is directed Subset of L ) & ( X is filtered Subset of S implies X is filtered Subset of L ) )
thus ( X is directed Subset of S implies X is directed Subset of L ) ::_thesis: ( X is filtered Subset of S implies X is filtered Subset of L )
proof
assume A1: X is directed Subset of S ; ::_thesis: X is directed Subset of L
the carrier of S c= the carrier of L by YELLOW_0:def_13;
then reconsider X = X as Subset of L by A1, XBOOLE_1: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 )
proof
let x, y be Element of L; ::_thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & x <= z & y <= z ) )
assume A2: ( x in X & y in X ) ; ::_thesis: ex z being Element of L st
( z in X & x <= z & y <= z )
then reconsider x9 = x, y9 = y as Element of S by A1;
consider z being Element of S such that
A3: ( z in X & x9 <= z & y9 <= z ) by A1, A2, WAYBEL_0:def_1;
reconsider z = z as Element of L by YELLOW_0:58;
take z ; ::_thesis: ( z in X & x <= z & y <= z )
thus ( z in X & x <= z & y <= z ) by A3, YELLOW_0:59; ::_thesis: verum
end;
hence X is directed Subset of L by WAYBEL_0:def_1; ::_thesis: verum
end;
thus ( X is filtered Subset of S implies X is filtered Subset of L ) ::_thesis: verum
proof
assume A4: X is filtered Subset of S ; ::_thesis: X is filtered Subset of L
the carrier of S c= the carrier of L by YELLOW_0:def_13;
then reconsider X = X as Subset of L by A4, XBOOLE_1: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 & z <= x & z <= y )
proof
let x, y be Element of L; ::_thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & z <= x & z <= y ) )
assume A5: ( x in X & y in X ) ; ::_thesis: ex z being Element of L st
( z in X & z <= x & z <= y )
then reconsider x9 = x, y9 = y as Element of S by A4;
consider z being Element of S such that
A6: ( z in X & z <= x9 & z <= y9 ) by A4, A5, WAYBEL_0:def_2;
reconsider z = z as Element of L by YELLOW_0:58;
take z ; ::_thesis: ( z in X & z <= x & z <= y )
thus ( z in X & z <= x & z <= y ) by A6, YELLOW_0:59; ::_thesis: verum
end;
hence X is filtered Subset of L by WAYBEL_0:def_2; ::_thesis: verum
end;
end;
theorem :: YELLOW_2:8
for L being non empty RelStr
for S, T being non empty full SubRelStr of L st the carrier of S c= the carrier of T holds
for X being Subset of S holds
( X is Subset of T & ( for Y being Subset of T st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) )
proof
let L be non empty RelStr ; ::_thesis: for S, T being non empty full SubRelStr of L st the carrier of S c= the carrier of T holds
for X being Subset of S holds
( X is Subset of T & ( for Y being Subset of T st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) )
let S1, S2 be non empty full SubRelStr of L; ::_thesis: ( the carrier of S1 c= the carrier of S2 implies for X being Subset of S1 holds
( X is Subset of S2 & ( for Y being Subset of S2 st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) ) )
assume A1: the carrier of S1 c= the carrier of S2 ; ::_thesis: for X being Subset of S1 holds
( X is Subset of S2 & ( for Y being Subset of S2 st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) )
let X be Subset of S1; ::_thesis: ( X is Subset of S2 & ( for Y being Subset of S2 st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) ) ) )
thus X is Subset of S2 by A1, XBOOLE_1:1; ::_thesis: for Y being Subset of S2 st X = Y holds
( ( X is filtered implies Y is filtered ) & ( X is directed implies Y is directed ) )
let X2 be Subset of S2; ::_thesis: ( X = X2 implies ( ( X is filtered implies X2 is filtered ) & ( X is directed implies X2 is directed ) ) )
assume A2: X = X2 ; ::_thesis: ( ( X is filtered implies X2 is filtered ) & ( X is directed implies X2 is directed ) )
hereby ::_thesis: ( X is directed implies X2 is directed )
assume A3: X is filtered ; ::_thesis: X2 is filtered
thus X2 is filtered ::_thesis: verum
proof
let x, y be Element of S2; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in X2 or not y in X2 or ex b1 being Element of the carrier of S2 st
( b1 in X2 & b1 <= x & b1 <= y ) )
assume A4: ( x in X2 & y in X2 ) ; ::_thesis: ex b1 being Element of the carrier of S2 st
( b1 in X2 & b1 <= x & b1 <= y )
then reconsider x9 = x, y9 = y as Element of S1 by A2;
consider z being Element of S1 such that
A5: z in X and
A6: ( z <= x9 & z <= y9 ) by A2, A3, A4, WAYBEL_0:def_2;
reconsider x1 = x, y1 = y, z1 = z as Element of L by YELLOW_0:58;
reconsider z = z as Element of S2 by A2, A5;
take z ; ::_thesis: ( z in X2 & z <= x & z <= y )
( z1 <= x1 & z1 <= y1 ) by A6, YELLOW_0:59;
hence ( z in X2 & z <= x & z <= y ) by A2, A5, YELLOW_0:60; ::_thesis: verum
end;
end;
assume A7: X is directed ; ::_thesis: X2 is directed
let x, y be Element of S2; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in X2 or not y in X2 or ex b1 being Element of the carrier of S2 st
( b1 in X2 & x <= b1 & y <= b1 ) )
assume A8: ( x in X2 & y in X2 ) ; ::_thesis: ex b1 being Element of the carrier of S2 st
( b1 in X2 & x <= b1 & y <= b1 )
then reconsider x9 = x, y9 = y as Element of S1 by A2;
consider z being Element of S1 such that
A9: z in X and
A10: ( x9 <= z & y9 <= z ) by A2, A7, A8, WAYBEL_0:def_1;
reconsider x1 = x, y1 = y, z1 = z as Element of L by YELLOW_0:58;
reconsider z = z as Element of S2 by A2, A9;
take z ; ::_thesis: ( z in X2 & x <= z & y <= z )
( x1 <= z1 & y1 <= z1 ) by A10, YELLOW_0:59;
hence ( z in X2 & x <= z & y <= z ) by A2, A9, YELLOW_0:60; ::_thesis: verum
end;
begin
definition
let J be set ;
let L be RelStr ;
let f, g be Function of J, the carrier of L;
predf <= g means :Def1: :: YELLOW_2:def 1
for j being set st j in J holds
ex a, b being Element of L st
( a = f . j & b = g . j & a <= b );
end;
:: deftheorem Def1 defines <= YELLOW_2:def_1_:_
for J being set
for L being RelStr
for f, g being Function of J, the carrier of L holds
( f <= g iff for j being set st j in J holds
ex a, b being Element of L st
( a = f . j & b = g . j & a <= b ) );
notation
let J be set ;
let L be RelStr ;
let f, g be Function of J, the carrier of L;
synonym g >= f for f <= g;
end;
theorem :: YELLOW_2:9
for L, M being non empty RelStr
for f, g being Function of L,M holds
( f <= g iff for x being Element of L holds f . x <= g . x )
proof
let L, M be non empty RelStr ; ::_thesis: for f, g being Function of L,M holds
( f <= g iff for x being Element of L holds f . x <= g . x )
let f, g be Function of L,M; ::_thesis: ( f <= g iff for x being Element of L holds f . x <= g . x )
hereby ::_thesis: ( ( for x being Element of L holds f . x <= g . x ) implies f <= g )
assume A1: f <= g ; ::_thesis: for x being Element of L holds f . x <= g . x
let x be Element of L; ::_thesis: f . x <= g . x
ex m1, m2 being Element of M st
( m1 = f . x & m2 = g . x & m1 <= m2 ) by A1, Def1;
hence f . x <= g . x ; ::_thesis: verum
end;
assume A2: for x being Element of L holds f . x <= g . x ; ::_thesis: f <= g
let x be set ; :: according to YELLOW_2:def_1 ::_thesis: ( x in the carrier of L implies ex a, b being Element of M st
( a = f . x & b = g . x & a <= b ) )
assume x in the carrier of L ; ::_thesis: ex a, b being Element of M st
( a = f . x & b = g . x & a <= b )
then reconsider x = x as Element of L ;
take f . x ; ::_thesis: ex b being Element of M st
( f . x = f . x & b = g . x & f . x <= b )
take g . x ; ::_thesis: ( f . x = f . x & g . x = g . x & f . x <= g . x )
thus ( f . x = f . x & g . x = g . x & f . x <= g . x ) by A2; ::_thesis: verum
end;
begin
definition
let L, M be non empty RelStr ;
let f be Function of L,M;
func Image f -> strict full SubRelStr of M equals :: YELLOW_2:def 2
subrelstr (rng f);
correctness
coherence
subrelstr (rng f) is strict full SubRelStr of M;
;
end;
:: deftheorem defines Image YELLOW_2:def_2_:_
for L, M being non empty RelStr
for f being Function of L,M holds Image f = subrelstr (rng f);
theorem :: YELLOW_2:10
for L, M being non empty RelStr
for f being Function of L,M
for y being Element of (Image f) ex x being Element of L st f . x = y
proof
let L1, L2 be non empty RelStr ; ::_thesis: for f being Function of L1,L2
for y being Element of (Image f) ex x being Element of L1 st f . x = y
let g be Function of L1,L2; ::_thesis: for y being Element of (Image g) ex x being Element of L1 st g . x = y
let s be Element of (Image g); ::_thesis: ex x being Element of L1 st g . x = s
dom g = the carrier of L1 by FUNCT_2:def_1;
then A1: not rng g is empty by RELAT_1:42;
rng g = the carrier of (Image g) by YELLOW_0:def_15;
then consider l being set such that
A2: l in dom g and
A3: s = g . l by A1, FUNCT_1:def_3;
reconsider l = l as Element of L1 by A2;
take l ; ::_thesis: g . l = s
thus g . l = s by A3; ::_thesis: verum
end;
registration
let L be non empty RelStr ;
let X be non empty Subset of L;
cluster subrelstr X -> non empty ;
coherence
not subrelstr X is empty by YELLOW_0:def_15;
end;
registration
let L, M be non empty RelStr ;
let f be Function of L,M;
cluster Image f -> non empty strict full ;
coherence
not Image f is empty
proof
dom f = the carrier of L by FUNCT_2:def_1;
then not rng f is empty by RELAT_1:42;
hence not Image f is empty ; ::_thesis: verum
end;
end;
begin
theorem :: YELLOW_2:11
for L being non empty RelStr holds id L is monotone
proof
let L be non empty RelStr ; ::_thesis: id L is monotone
let l1, l2 be Element of L; :: according to ORDERS_3:def_5 ::_thesis: ( not l1 <= l2 or for b1, b2 being Element of the carrier of L holds
( not b1 = (id L) . l1 or not b2 = (id L) . l2 or b1 <= b2 ) )
assume l1 <= l2 ; ::_thesis: for b1, b2 being Element of the carrier of L holds
( not b1 = (id L) . l1 or not b2 = (id L) . l2 or b1 <= b2 )
then l1 <= (id L) . l2 by FUNCT_1:18;
hence for b1, b2 being Element of the carrier of L holds
( not b1 = (id L) . l1 or not b2 = (id L) . l2 or b1 <= b2 ) by FUNCT_1:18; ::_thesis: verum
end;
theorem :: YELLOW_2:12
for L, M, N being non empty RelStr
for f being Function of L,M
for g being Function of M,N st f is monotone & g is monotone holds
g * f is monotone
proof
let L1, L2, L3 be non empty RelStr ; ::_thesis: for f being Function of L1,L2
for g being Function of L2,L3 st f is monotone & g is monotone holds
g * f is monotone
let g1 be Function of L1,L2; ::_thesis: for g being Function of L2,L3 st g1 is monotone & g is monotone holds
g * g1 is monotone
let g2 be Function of L2,L3; ::_thesis: ( g1 is monotone & g2 is monotone implies g2 * g1 is monotone )
assume that
A1: g1 is monotone and
A2: g2 is monotone ; ::_thesis: g2 * g1 is monotone
let s1, s2 be Element of L1; :: according to ORDERS_3:def_5 ::_thesis: ( not s1 <= s2 or for b1, b2 being Element of the carrier of L3 holds
( not b1 = (g2 * g1) . s1 or not b2 = (g2 * g1) . s2 or b1 <= b2 ) )
assume s1 <= s2 ; ::_thesis: for b1, b2 being Element of the carrier of L3 holds
( not b1 = (g2 * g1) . s1 or not b2 = (g2 * g1) . s2 or b1 <= b2 )
then g1 . s1 <= g1 . s2 by A1, ORDERS_3:def_5;
then g2 . (g1 . s1) <= g2 . (g1 . s2) by A2, ORDERS_3:def_5;
then (g2 * g1) . s1 <= g2 . (g1 . s2) by FUNCT_2:15;
hence for b1, b2 being Element of the carrier of L3 holds
( not b1 = (g2 * g1) . s1 or not b2 = (g2 * g1) . s2 or b1 <= b2 ) by FUNCT_2:15; ::_thesis: verum
end;
theorem :: YELLOW_2:13
for L, M being non empty RelStr
for f being Function of L,M
for X being Subset of L
for x being Element of L st f is monotone & x is_<=_than X holds
f . x is_<=_than f .: X
proof
let L1, L2 be non empty RelStr ; ::_thesis: for f being Function of L1,L2
for X being Subset of L1
for x being Element of L1 st f is monotone & x is_<=_than X holds
f . x is_<=_than f .: X
let g be Function of L1,L2; ::_thesis: for X being Subset of L1
for x being Element of L1 st g is monotone & x is_<=_than X holds
g . x is_<=_than g .: X
let X be Subset of L1; ::_thesis: for x being Element of L1 st g is monotone & x is_<=_than X holds
g . x is_<=_than g .: X
let x be Element of L1; ::_thesis: ( g is monotone & x is_<=_than X implies g . x is_<=_than g .: X )
assume that
A1: g is monotone and
A2: x is_<=_than X ; ::_thesis: g . x is_<=_than g .: X
let y2 be Element of L2; :: according to LATTICE3:def_8 ::_thesis: ( not y2 in g .: X or g . x <= y2 )
assume y2 in g .: X ; ::_thesis: g . x <= y2
then consider x2 being Element of L1 such that
A3: x2 in X and
A4: y2 = g . x2 by FUNCT_2:65;
reconsider x2 = x2 as Element of L1 ;
x <= x2 by A2, A3, LATTICE3:def_8;
hence g . x <= y2 by A1, A4, ORDERS_3:def_5; ::_thesis: verum
end;
theorem :: YELLOW_2:14
for L, M being non empty RelStr
for f being Function of L,M
for X being Subset of L
for x being Element of L st f is monotone & X is_<=_than x holds
f .: X is_<=_than f . x
proof
let L1, L2 be non empty RelStr ; ::_thesis: for f being Function of L1,L2
for X being Subset of L1
for x being Element of L1 st f is monotone & X is_<=_than x holds
f .: X is_<=_than f . x
let g be Function of L1,L2; ::_thesis: for X being Subset of L1
for x being Element of L1 st g is monotone & X is_<=_than x holds
g .: X is_<=_than g . x
let X be Subset of L1; ::_thesis: for x being Element of L1 st g is monotone & X is_<=_than x holds
g .: X is_<=_than g . x
let x be Element of L1; ::_thesis: ( g is monotone & X is_<=_than x implies g .: X is_<=_than g . x )
assume that
A1: g is monotone and
A2: x is_>=_than X ; ::_thesis: g .: X is_<=_than g . x
let y2 be Element of L2; :: according to LATTICE3:def_9 ::_thesis: ( not y2 in g .: X or y2 <= g . x )
assume y2 in g .: X ; ::_thesis: y2 <= g . x
then consider x2 being Element of L1 such that
A3: x2 in X and
A4: y2 = g . x2 by FUNCT_2:65;
reconsider x2 = x2 as Element of L1 ;
x >= x2 by A2, A3, LATTICE3:def_9;
hence y2 <= g . x by A1, A4, ORDERS_3:def_5; ::_thesis: verum
end;
theorem :: YELLOW_2:15
for S, T being non empty RelStr
for f being Function of S,T
for X being directed Subset of S st f is monotone holds
f .: X is directed
proof
let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T
for X being directed Subset of S st f is monotone holds
f .: X is directed
let f be Function of S,T; ::_thesis: for X being directed Subset of S st f is monotone holds
f .: X is directed
let X be directed Subset of S; ::_thesis: ( f is monotone implies f .: X is directed )
set Y = f .: X;
assume A1: f is monotone ; ::_thesis: f .: X is directed
for y1, y2 being Element of T st y1 in f .: X & y2 in f .: X holds
ex z being Element of T st
( z in f .: X & y1 <= z & y2 <= z )
proof
let y1, y2 be Element of T; ::_thesis: ( y1 in f .: X & y2 in f .: X implies ex z being Element of T st
( z in f .: X & y1 <= z & y2 <= z ) )
assume that
A2: y1 in f .: X and
A3: y2 in f .: X ; ::_thesis: ex z being Element of T st
( z in f .: X & y1 <= z & y2 <= z )
consider x1 being set such that
x1 in dom f and
A4: x1 in X and
A5: y1 = f . x1 by A2, FUNCT_1:def_6;
consider x2 being set such that
x2 in dom f and
A6: x2 in X and
A7: y2 = f . x2 by A3, FUNCT_1:def_6;
reconsider x1 = x1, x2 = x2 as Element of S by A4, A6;
consider z being Element of S such that
A8: z in X and
A9: ( x1 <= z & x2 <= z ) by A4, A6, WAYBEL_0:def_1;
take f . z ; ::_thesis: ( f . z in f .: X & y1 <= f . z & y2 <= f . z )
thus f . z in f .: X by A8, FUNCT_2:35; ::_thesis: ( y1 <= f . z & y2 <= f . z )
thus ( y1 <= f . z & y2 <= f . z ) by A1, A5, A7, A9, ORDERS_3:def_5; ::_thesis: verum
end;
hence f .: X is directed by WAYBEL_0:def_1; ::_thesis: verum
end;
theorem Th16: :: YELLOW_2:16
for L being with_suprema Poset
for f being Function of L,L st f is directed-sups-preserving holds
f is monotone
proof
let L be with_suprema Poset; ::_thesis: for f being Function of L,L st f is directed-sups-preserving holds
f is monotone
let f be Function of L,L; ::_thesis: ( f is directed-sups-preserving implies f is monotone )
assume A1: f is directed-sups-preserving ; ::_thesis: f is monotone
let x, y be Element of L; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 ) )
assume A2: x <= y ; ::_thesis: for b1, b2 being Element of the carrier of L holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 )
A3: y = y "\/" x by A2, YELLOW_0:24;
for a, b being Element of L st a in {x,y} & b in {x,y} holds
ex z being Element of L st
( z in {x,y} & a <= z & b <= z )
proof
let a, b be Element of L; ::_thesis: ( a in {x,y} & b in {x,y} implies ex z being Element of L st
( z in {x,y} & a <= z & b <= z ) )
assume A4: ( a in {x,y} & b in {x,y} ) ; ::_thesis: ex z being Element of L st
( z in {x,y} & a <= z & b <= z )
take y ; ::_thesis: ( y in {x,y} & a <= y & b <= y )
thus y in {x,y} by TARSKI:def_2; ::_thesis: ( a <= y & b <= y )
thus ( a <= y & b <= y ) by A2, A4, TARSKI:def_2; ::_thesis: verum
end;
then ( {x,y} is directed & not {x,y} is empty ) by WAYBEL_0:def_1;
then A5: f preserves_sup_of {x,y} by A1, WAYBEL_0:def_37;
A6: dom f = the carrier of L by FUNCT_2:def_1;
y <= y ;
then A7: {x,y} is_<=_than y by A2, YELLOW_0:8;
for b being Element of L st {x,y} is_<=_than b holds
y <= b by YELLOW_0:8;
then ex_sup_of {x,y},L by A7, YELLOW_0:30;
then sup (f .: {x,y}) = f . (sup {x,y}) by A5, WAYBEL_0:def_31
.= f . y by A3, YELLOW_0:41 ;
then A8: f . y = sup {(f . x),(f . y)} by A6, FUNCT_1:60
.= (f . y) "\/" (f . x) by YELLOW_0:41 ;
let afx, bfy be Element of L; ::_thesis: ( not afx = f . x or not bfy = f . y or afx <= bfy )
assume ( afx = f . x & bfy = f . y ) ; ::_thesis: afx <= bfy
hence afx <= bfy by A8, YELLOW_0:22; ::_thesis: verum
end;
theorem :: YELLOW_2:17
for L being with_infima Poset
for f being Function of L,L st f is filtered-infs-preserving holds
f is monotone
proof
let L be with_infima Poset; ::_thesis: for f being Function of L,L st f is filtered-infs-preserving holds
f is monotone
let f be Function of L,L; ::_thesis: ( f is filtered-infs-preserving implies f is monotone )
assume A1: f is filtered-infs-preserving ; ::_thesis: f is monotone
let x, y be Element of L; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of L holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 ) )
assume A2: x <= y ; ::_thesis: for b1, b2 being Element of the carrier of L holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 )
A3: x = x "/\" y by A2, YELLOW_0:25;
for c, d being Element of L st c in {x,y} & d in {x,y} holds
ex z being Element of L st
( z in {x,y} & z <= c & z <= d )
proof
let c, d be Element of L; ::_thesis: ( c in {x,y} & d in {x,y} implies ex z being Element of L st
( z in {x,y} & z <= c & z <= d ) )
assume A4: ( c in {x,y} & d in {x,y} ) ; ::_thesis: ex z being Element of L st
( z in {x,y} & z <= c & z <= d )
take x ; ::_thesis: ( x in {x,y} & x <= c & x <= d )
thus x in {x,y} by TARSKI:def_2; ::_thesis: ( x <= c & x <= d )
thus ( x <= c & x <= d ) by A2, A4, TARSKI:def_2; ::_thesis: verum
end;
then ( {x,y} is filtered & not {x,y} is empty ) by WAYBEL_0:def_2;
then A5: f preserves_inf_of {x,y} by A1, WAYBEL_0:def_36;
A6: dom f = the carrier of L by FUNCT_2:def_1;
x <= x ;
then A7: x is_<=_than {x,y} by A2, YELLOW_0:8;
for c being Element of L st c is_<=_than {x,y} holds
c <= x by YELLOW_0:8;
then ex_inf_of {x,y},L by A7, YELLOW_0:31;
then inf (f .: {x,y}) = f . (inf {x,y}) by A5, WAYBEL_0:def_30
.= f . x by A3, YELLOW_0:40 ;
then A8: f . x = inf {(f . x),(f . y)} by A6, FUNCT_1:60
.= (f . x) "/\" (f . y) by YELLOW_0:40 ;
let a, b be Element of L; ::_thesis: ( not a = f . x or not b = f . y or a <= b )
assume ( a = f . x & b = f . y ) ; ::_thesis: a <= b
hence a <= b by A8, YELLOW_0:23; ::_thesis: verum
end;
begin
theorem :: YELLOW_2:18
for S being non empty 1-sorted
for f being Function of S,S st f is idempotent holds
for x being Element of S holds f . (f . x) = f . x
proof
let L be non empty 1-sorted ; ::_thesis: for f being Function of L,L st f is idempotent holds
for x being Element of L holds f . (f . x) = f . x
let p be Function of L,L; ::_thesis: ( p is idempotent implies for x being Element of L holds p . (p . x) = p . x )
assume A1: p * p = p ; :: according to QUANTAL1:def_9 ::_thesis: for x being Element of L holds p . (p . x) = p . x
let l be Element of L; ::_thesis: p . (p . l) = p . l
thus p . (p . l) = p . l by A1, FUNCT_2:15; ::_thesis: verum
end;
theorem Th19: :: YELLOW_2:19
for S being non empty 1-sorted
for f being Function of S,S st f is idempotent holds
rng f = { x where x is Element of S : x = f . x }
proof
let S be non empty 1-sorted ; ::_thesis: for f being Function of S,S st f is idempotent holds
rng f = { x where x is Element of S : x = f . x }
let f be Function of S,S; ::_thesis: ( f is idempotent implies rng f = { x where x is Element of S : x = f . x } )
set M = { x where x is Element of S : x = f . x } ;
assume A1: f = f * f ; :: according to QUANTAL1:def_9 ::_thesis: rng f = { x where x is Element of S : x = f . x }
A2: rng f c= { x where x is Element of S : x = f . x }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in { x where x is Element of S : x = f . x } )
assume A3: y in rng f ; ::_thesis: y in { x where x is Element of S : x = f . x }
then reconsider y9 = y as Element of S ;
ex x being set st
( x in dom f & y = f . x ) by A3, FUNCT_1:def_3;
then y9 = f . y9 by A1, FUNCT_1:13;
hence y in { x where x is Element of S : x = f . x } ; ::_thesis: verum
end;
{ x where x is Element of S : x = f . x } c= rng f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { x where x is Element of S : x = f . x } or y in rng f )
assume y in { x where x is Element of S : x = f . x } ; ::_thesis: y in rng f
then A4: ex y9 being Element of S st
( y9 = y & y9 = f . y9 ) ;
dom f = the carrier of S by FUNCT_2:def_1;
hence y in rng f by A4, FUNCT_1:def_3; ::_thesis: verum
end;
hence rng f = { x where x is Element of S : x = f . x } by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th20: :: YELLOW_2:20
for X being set
for S being non empty 1-sorted
for f being Function of S,S st f is idempotent & X c= rng f holds
f .: X = X
proof
let X be set ; ::_thesis: for S being non empty 1-sorted
for f being Function of S,S st f is idempotent & X c= rng f holds
f .: X = X
let S be non empty 1-sorted ; ::_thesis: for f being Function of S,S st f is idempotent & X c= rng f holds
f .: X = X
let f be Function of S,S; ::_thesis: ( f is idempotent & X c= rng f implies f .: X = X )
assume A1: f is idempotent ; ::_thesis: ( not X c= rng f or f .: X = X )
set M = { x where x is Element of S : x = f . x } ;
assume X c= rng f ; ::_thesis: f .: X = X
then A2: X c= { x where x is Element of S : x = f . x } by A1, Th19;
A3: f .: X c= X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: X or y in X )
assume y in f .: X ; ::_thesis: y in X
then consider x being set such that
x in dom f and
A4: x in X and
A5: y = f . x by FUNCT_1:def_6;
x in { x where x is Element of S : x = f . x } by A2, A4;
then ex x9 being Element of S st
( x9 = x & x9 = f . x9 ) ;
hence y in X by A4, A5; ::_thesis: verum
end;
X c= f .: X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in f .: X )
assume A6: y in X ; ::_thesis: y in f .: X
then y in { x where x is Element of S : x = f . x } by A2;
then ex x being Element of S st
( x = y & x = f . x ) ;
hence y in f .: X by A6, FUNCT_2:35; ::_thesis: verum
end;
hence f .: X = X by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: YELLOW_2:21
for L being non empty RelStr holds id L is idempotent
proof
let L be non empty RelStr ; ::_thesis: id L is idempotent
thus (id L) * (id L) = id ( the carrier of L /\ the carrier of L) by FUNCT_1:22
.= id L ; :: according to QUANTAL1:def_9 ::_thesis: verum
end;
begin
theorem Th22: :: YELLOW_2:22
for X being set
for L being complete LATTICE
for a being Element of L st a in X holds
( a <= "\/" (X,L) & "/\" (X,L) <= a )
proof
let X be set ; ::_thesis: for L being complete LATTICE
for a being Element of L st a in X holds
( a <= "\/" (X,L) & "/\" (X,L) <= a )
let L be complete LATTICE; ::_thesis: for a being Element of L st a in X holds
( a <= "\/" (X,L) & "/\" (X,L) <= a )
let a be Element of L; ::_thesis: ( a in X implies ( a <= "\/" (X,L) & "/\" (X,L) <= a ) )
assume A1: a in X ; ::_thesis: ( a <= "\/" (X,L) & "/\" (X,L) <= a )
X is_<=_than "\/" (X,L) by YELLOW_0:32;
hence a <= "\/" (X,L) by A1, LATTICE3:def_9; ::_thesis: "/\" (X,L) <= a
X is_>=_than "/\" (X,L) by YELLOW_0:33;
hence "/\" (X,L) <= a by A1, LATTICE3:def_8; ::_thesis: verum
end;
theorem Th23: :: YELLOW_2:23
for L being non empty RelStr holds
( ( for X being set holds ex_sup_of X,L ) iff for Y being set holds ex_inf_of Y,L )
proof
let L be non empty RelStr ; ::_thesis: ( ( for X being set holds ex_sup_of X,L ) iff for Y being set holds ex_inf_of Y,L )
hereby ::_thesis: ( ( for Y being set holds ex_inf_of Y,L ) implies for X being set holds ex_sup_of X,L )
assume A1: for X being set holds ex_sup_of X,L ; ::_thesis: for Y being set holds ex_inf_of Y,L
let Y be set ; ::_thesis: ex_inf_of Y,L
set X = { x where x is Element of L : x is_<=_than Y } ;
ex_sup_of { x where x is Element of L : x is_<=_than Y } ,L by A1;
then consider a being Element of L such that
A2: { x where x is Element of L : x is_<=_than Y } is_<=_than a and
A3: for b being Element of L st { x where x is Element of L : x is_<=_than Y } is_<=_than b holds
b >= a and
A4: for c being Element of L st { x where x is Element of L : x is_<=_than Y } is_<=_than c & ( for b being Element of L st { x where x is Element of L : x is_<=_than Y } is_<=_than b holds
b >= c ) holds
c = a by YELLOW_0:def_7;
A5: a is_<=_than Y
proof
let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in Y or a <= b )
assume A6: b in Y ; ::_thesis: a <= b
b is_>=_than { x where x is Element of L : x is_<=_than Y }
proof
let c be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not c in { x where x is Element of L : x is_<=_than Y } or c <= b )
assume c in { x where x is Element of L : x is_<=_than Y } ; ::_thesis: c <= b
then ex x being Element of L st
( c = x & x is_<=_than Y ) ;
hence c <= b by A6, LATTICE3:def_8; ::_thesis: verum
end;
hence a <= b by A3; ::_thesis: verum
end;
A7: for c being Element of L st Y is_>=_than c & ( for b being Element of L st Y is_>=_than b holds
b <= c ) holds
c = a
proof
let c be Element of L; ::_thesis: ( Y is_>=_than c & ( for b being Element of L st Y is_>=_than b holds
b <= c ) implies c = a )
assume that
A8: Y is_>=_than c and
A9: for b being Element of L st Y is_>=_than b holds
b <= c ; ::_thesis: c = a
A10: for b being Element of L st { x where x is Element of L : x is_<=_than Y } is_<=_than b holds
b >= c
proof
let b be Element of L; ::_thesis: ( { x where x is Element of L : x is_<=_than Y } is_<=_than b implies b >= c )
assume A11: { x where x is Element of L : x is_<=_than Y } is_<=_than b ; ::_thesis: b >= c
c in { x where x is Element of L : x is_<=_than Y } by A8;
hence b >= c by A11, LATTICE3:def_9; ::_thesis: verum
end;
{ x where x is Element of L : x is_<=_than Y } is_<=_than c
proof
let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in { x where x is Element of L : x is_<=_than Y } or b <= c )
assume b in { x where x is Element of L : x is_<=_than Y } ; ::_thesis: b <= c
then ex x being Element of L st
( b = x & x is_<=_than Y ) ;
hence b <= c by A9; ::_thesis: verum
end;
hence c = a by A4, A10; ::_thesis: verum
end;
for b being Element of L st Y is_>=_than b holds
a >= b
proof
let b be Element of L; ::_thesis: ( Y is_>=_than b implies a >= b )
assume b is_<=_than Y ; ::_thesis: a >= b
then b in { x where x is Element of L : x is_<=_than Y } ;
hence a >= b by A2, LATTICE3:def_9; ::_thesis: verum
end;
hence ex_inf_of Y,L by A5, A7, YELLOW_0:def_8; ::_thesis: verum
end;
assume A12: for Y being set holds ex_inf_of Y,L ; ::_thesis: for X being set holds ex_sup_of X,L
let X be set ; ::_thesis: ex_sup_of X,L
set Y = { y where y is Element of L : X is_<=_than y } ;
ex_inf_of { y where y is Element of L : X is_<=_than y } ,L by A12;
then consider a being Element of L such that
A13: { y where y is Element of L : X is_<=_than y } is_>=_than a and
A14: for b being Element of L st { y where y is Element of L : X is_<=_than y } is_>=_than b holds
b <= a and
A15: for c being Element of L st { y where y is Element of L : X is_<=_than y } is_>=_than c & ( for b being Element of L st { y where y is Element of L : X is_<=_than y } is_>=_than b holds
b <= c ) holds
c = a by YELLOW_0:def_8;
A16: X is_<=_than a
proof
let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in X or b <= a )
assume A17: b in X ; ::_thesis: b <= a
b is_<=_than { y where y is Element of L : X is_<=_than y }
proof
let c be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not c in { y where y is Element of L : X is_<=_than y } or b <= c )
assume c in { y where y is Element of L : X is_<=_than y } ; ::_thesis: b <= c
then ex y being Element of L st
( c = y & X is_<=_than y ) ;
hence b <= c by A17, LATTICE3:def_9; ::_thesis: verum
end;
hence b <= a by A14; ::_thesis: verum
end;
A18: 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
proof
let c be Element of L; ::_thesis: ( X is_<=_than c & ( for b being Element of L st X is_<=_than b holds
b >= c ) implies c = a )
assume that
A19: X is_<=_than c and
A20: for b being Element of L st X is_<=_than b holds
b >= c ; ::_thesis: c = a
A21: for b being Element of L st { y where y is Element of L : X is_<=_than y } is_>=_than b holds
b <= c
proof
let b be Element of L; ::_thesis: ( { y where y is Element of L : X is_<=_than y } is_>=_than b implies b <= c )
assume A22: { y where y is Element of L : X is_<=_than y } is_>=_than b ; ::_thesis: b <= c
c in { y where y is Element of L : X is_<=_than y } by A19;
hence b <= c by A22, LATTICE3:def_8; ::_thesis: verum
end;
{ y where y is Element of L : X is_<=_than y } is_>=_than c
proof
let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in { y where y is Element of L : X is_<=_than y } or c <= b )
assume b in { y where y is Element of L : X is_<=_than y } ; ::_thesis: c <= b
then ex x being Element of L st
( b = x & x is_>=_than X ) ;
hence c <= b by A20; ::_thesis: verum
end;
hence c = a by A15, A21; ::_thesis: verum
end;
for b being Element of L st X is_<=_than b holds
a <= b
proof
let b be Element of L; ::_thesis: ( X is_<=_than b implies a <= b )
assume X is_<=_than b ; ::_thesis: a <= b
then b in { y where y is Element of L : X is_<=_than y } ;
hence a <= b by A13, LATTICE3:def_8; ::_thesis: verum
end;
hence ex_sup_of X,L by A16, A18, YELLOW_0:def_7; ::_thesis: verum
end;
theorem Th24: :: YELLOW_2:24
for L being non empty RelStr st ( for X being set holds ex_sup_of X,L ) holds
L is complete
proof
let L be non empty RelStr ; ::_thesis: ( ( for X being set holds ex_sup_of X,L ) implies L is complete )
assume A1: for X being set holds ex_sup_of X,L ; ::_thesis: L is complete
L is complete
proof
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 ) ) )
take a = "\/" (X,L); ::_thesis: ( X is_<=_than a & ( for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or a <= b1 ) ) )
A2: ex_sup_of X,L by A1;
hence X is_<=_than a by YELLOW_0:def_9; ::_thesis: for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or a <= b1 )
thus for b1 being Element of the carrier of L holds
( not X is_<=_than b1 or a <= b1 ) by A2, YELLOW_0:def_9; ::_thesis: verum
end;
hence L is complete ; ::_thesis: verum
end;
theorem Th25: :: YELLOW_2:25
for L being non empty RelStr st ( for X being set holds ex_inf_of X,L ) holds
L is complete
proof
let L be non empty RelStr ; ::_thesis: ( ( for X being set holds ex_inf_of X,L ) implies L is complete )
assume for X being set holds ex_inf_of X,L ; ::_thesis: L is complete
then for X being set holds ex_sup_of X,L by Th23;
hence L is complete by Th24; ::_thesis: verum
end;
theorem Th26: :: YELLOW_2:26
for L being non empty RelStr st ( for A being Subset of L holds ex_inf_of A,L ) holds
for X being set holds
( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) )
proof
let L be non empty RelStr ; ::_thesis: ( ( for A being Subset of L holds ex_inf_of A,L ) implies for X being set holds
( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) ) )
assume A1: for A being Subset of L holds ex_inf_of A,L ; ::_thesis: for X being set holds
( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) )
let X be set ; ::_thesis: ( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) )
set Y = X /\ the carrier of L;
set a = "/\" ((X /\ the carrier of L),L);
reconsider Y = X /\ the carrier of L as Subset of L by XBOOLE_1:17;
A2: ex_inf_of Y,L by A1;
A3: "/\" ((X /\ the carrier of L),L) is_<=_than X
proof
let x be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not x in X or "/\" ((X /\ the carrier of L),L) <= x )
assume x in X ; ::_thesis: "/\" ((X /\ the carrier of L),L) <= x
then A4: x in Y by XBOOLE_0:def_4;
"/\" ((X /\ the carrier of L),L) is_<=_than Y by A2, YELLOW_0:def_10;
hence "/\" ((X /\ the carrier of L),L) <= x by A4, LATTICE3:def_8; ::_thesis: verum
end;
A5: for b being Element of L st b is_<=_than X holds
b <= "/\" ((X /\ the carrier of L),L)
proof
let b be Element of L; ::_thesis: ( b is_<=_than X implies b <= "/\" ((X /\ the carrier of L),L) )
A6: Y c= X by XBOOLE_1:17;
assume b is_<=_than X ; ::_thesis: b <= "/\" ((X /\ the carrier of L),L)
then b is_<=_than Y by A6, YELLOW_0:9;
hence b <= "/\" ((X /\ the carrier of L),L) by A2, YELLOW_0:def_10; ::_thesis: verum
end;
ex_inf_of X,L by A2, YELLOW_0:50;
hence ( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) ) by A3, A5, YELLOW_0:def_10; ::_thesis: verum
end;
theorem :: YELLOW_2:27
for L being non empty RelStr st ( for A being Subset of L holds ex_sup_of A,L ) holds
for X being set holds
( ex_sup_of X,L & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) )
proof
let L be non empty RelStr ; ::_thesis: ( ( for A being Subset of L holds ex_sup_of A,L ) implies for X being set holds
( ex_sup_of X,L & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) ) )
assume A1: for A being Subset of L holds ex_sup_of A,L ; ::_thesis: for X being set holds
( ex_sup_of X,L & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) )
let X be set ; ::_thesis: ( ex_sup_of X,L & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) )
set Y = X /\ the carrier of L;
set a = "\/" ((X /\ the carrier of L),L);
reconsider Y = X /\ the carrier of L as Subset of L by XBOOLE_1:17;
A2: ex_sup_of Y,L by A1;
A3: X is_<=_than "\/" ((X /\ the carrier of L),L)
proof
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= "\/" ((X /\ the carrier of L),L) )
assume x in X ; ::_thesis: x <= "\/" ((X /\ the carrier of L),L)
then A4: x in Y by XBOOLE_0:def_4;
Y is_<=_than "\/" ((X /\ the carrier of L),L) by A2, YELLOW_0:def_9;
hence x <= "\/" ((X /\ the carrier of L),L) by A4, LATTICE3:def_9; ::_thesis: verum
end;
A5: for b being Element of L st X is_<=_than b holds
"\/" ((X /\ the carrier of L),L) <= b
proof
let b be Element of L; ::_thesis: ( X is_<=_than b implies "\/" ((X /\ the carrier of L),L) <= b )
A6: Y c= X by XBOOLE_1:17;
assume X is_<=_than b ; ::_thesis: "\/" ((X /\ the carrier of L),L) <= b
then Y is_<=_than b by A6, YELLOW_0:9;
hence "\/" ((X /\ the carrier of L),L) <= b by A2, YELLOW_0:def_9; ::_thesis: verum
end;
ex_sup_of X,L by A2, YELLOW_0:50;
hence ( ex_sup_of X,L & "\/" (X,L) = "\/" ((X /\ the carrier of L),L) ) by A3, A5, YELLOW_0:def_9; ::_thesis: verum
end;
theorem Th28: :: YELLOW_2:28
for L being non empty RelStr st ( for A being Subset of L holds ex_inf_of A,L ) holds
L is complete
proof
let L be non empty RelStr ; ::_thesis: ( ( for A being Subset of L holds ex_inf_of A,L ) implies L is complete )
assume for A being Subset of L holds ex_inf_of A,L ; ::_thesis: L is complete
then for X being set holds ex_inf_of X,L by Th26;
hence L is complete by Th25; ::_thesis: verum
end;
registration
cluster non empty reflexive transitive antisymmetric upper-bounded up-complete /\-complete -> non empty complete for RelStr ;
correctness
coherence
for b1 being non empty Poset st b1 is up-complete & b1 is /\-complete & b1 is upper-bounded holds
b1 is complete ;
;
end;
theorem Th29: :: YELLOW_2:29
for L being complete LATTICE
for f being Function of L,L st f is monotone holds
for M being Subset of L st M = { x where x is Element of L : x = f . x } holds
subrelstr M is complete LATTICE
proof
let L be complete LATTICE; ::_thesis: for f being Function of L,L st f is monotone holds
for M being Subset of L st M = { x where x is Element of L : x = f . x } holds
subrelstr M is complete LATTICE
let f be Function of L,L; ::_thesis: ( f is monotone implies for M being Subset of L st M = { x where x is Element of L : x = f . x } holds
subrelstr M is complete LATTICE )
assume A1: f is monotone ; ::_thesis: for M being Subset of L st M = { x where x is Element of L : x = f . x } holds
subrelstr M is complete LATTICE
let M be Subset of L; ::_thesis: ( M = { x where x is Element of L : x = f . x } implies subrelstr M is complete LATTICE )
assume A2: M = { x where x is Element of L : x = f . x } ; ::_thesis: subrelstr M is complete LATTICE
set S = subrelstr M;
A3: for X being Subset of (subrelstr M)
for Y being Subset of L st Y = { y where y is Element of L : ( X is_<=_than f . y & f . y <= y ) } holds
inf Y in M
proof
let X be Subset of (subrelstr M); ::_thesis: for Y being Subset of L st Y = { y where y is Element of L : ( X is_<=_than f . y & f . y <= y ) } holds
inf Y in M
let Y be Subset of L; ::_thesis: ( Y = { y where y is Element of L : ( X is_<=_than f . y & f . y <= y ) } implies inf Y in M )
assume A4: Y = { y where y is Element of L : ( X is_<=_than f . y & f . y <= y ) } ; ::_thesis: inf Y in M
set z = inf Y;
A5: f . (inf Y) is_<=_than Y
proof
let u be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not u in Y or f . (inf Y) <= u )
assume A6: u in Y ; ::_thesis: f . (inf Y) <= u
then consider y being Element of L such that
A7: y = u and
X is_<=_than f . y and
A8: f . y <= y by A4;
inf Y <= u by A6, Th22;
then f . (inf Y) <= f . y by A1, A7, ORDERS_3:def_5;
hence f . (inf Y) <= u by A7, A8, ORDERS_2:3; ::_thesis: verum
end;
A9: X is_<=_than f . (f . (inf Y))
proof
let m be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not m in X or m <= f . (f . (inf Y)) )
assume A10: m in X ; ::_thesis: m <= f . (f . (inf Y))
m is_<=_than Y
proof
let u be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not u in Y or m <= u )
assume u in Y ; ::_thesis: m <= u
then consider y being Element of L such that
A11: y = u and
A12: X is_<=_than f . y and
A13: f . y <= y by A4;
m <= f . y by A10, A12, LATTICE3:def_9;
hence m <= u by A11, A13, ORDERS_2:3; ::_thesis: verum
end;
then m <= inf Y by YELLOW_0:33;
then A14: f . m <= f . (inf Y) by A1, ORDERS_3:def_5;
X c= the carrier of (subrelstr M) ;
then X c= M by YELLOW_0:def_15;
then m in M by A10;
then ex x being Element of L st
( x = m & x = f . x ) by A2;
hence m <= f . (f . (inf Y)) by A1, A14, ORDERS_3:def_5; ::_thesis: verum
end;
ex_inf_of Y,L by YELLOW_0:17;
then A15: f . (inf Y) <= inf Y by A5, YELLOW_0:31;
then f . (f . (inf Y)) <= f . (inf Y) by A1, ORDERS_3:def_5;
then f . (inf Y) in Y by A4, A9;
then inf Y <= f . (inf Y) by Th22;
then inf Y = f . (inf Y) by A15, ORDERS_2:2;
hence inf Y in M by A2; ::_thesis: verum
end;
M c= the carrier of (subrelstr M) by YELLOW_0:def_15;
then reconsider M = M as Subset of (subrelstr M) ;
defpred S1[ Element of L] means ( M is_<=_than f . $1 & f . $1 <= $1 );
reconsider Y = { y where y is Element of L : S1[y] } as Subset of L from DOMAIN_1:sch_7();
inf Y in M by A3;
then reconsider S = subrelstr M as non empty Poset ;
for X being Subset of S holds ex_sup_of X,S
proof
let X be Subset of S; ::_thesis: ex_sup_of X,S
defpred S2[ Element of L] means ( X is_<=_than f . $1 & f . $1 <= $1 );
reconsider Y = { y where y is Element of L : S2[y] } as Subset of L from DOMAIN_1:sch_7();
set z = inf Y;
inf Y in M by A3;
then reconsider z = inf Y as Element of S ;
A16: X is_<=_than z
proof
let x be Element of S; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= z )
x in the carrier of S ;
then x in M by YELLOW_0:def_15;
then consider m being Element of L such that
A17: x = m and
m = f . m by A2;
assume A18: x in X ; ::_thesis: x <= z
m is_<=_than Y
proof
let u be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not u in Y or m <= u )
assume u in Y ; ::_thesis: m <= u
then consider y being Element of L such that
A19: y = u and
A20: X is_<=_than f . y and
A21: f . y <= y ;
m <= f . y by A18, A17, A20, LATTICE3:def_9;
hence m <= u by A19, A21, ORDERS_2:3; ::_thesis: verum
end;
then m <= inf Y by YELLOW_0:33;
hence x <= z by A17, YELLOW_0:60; ::_thesis: verum
end;
for b being Element of S st X is_<=_than b holds
z <= b
proof
let b be Element of S; ::_thesis: ( X is_<=_than b implies z <= b )
b in the carrier of S ;
then b in M by YELLOW_0:def_15;
then consider x being Element of L such that
A22: x = b and
A23: x = f . x by A2;
assume X is_<=_than b ; ::_thesis: z <= b
then X is_<=_than f . x by A22, A23, YELLOW_0:62;
then x in Y by A23;
hence z <= b by A22, Th22, YELLOW_0:60; ::_thesis: verum
end;
hence ex_sup_of X,S by A16, YELLOW_0:30; ::_thesis: verum
end;
then reconsider S = S as non empty complete Poset by YELLOW_0:53;
S is complete LATTICE ;
hence subrelstr M is complete LATTICE ; ::_thesis: verum
end;
theorem Th30: :: YELLOW_2:30
for L being complete LATTICE
for S being non empty full infs-inheriting SubRelStr of L holds S is complete LATTICE
proof
let L be complete LATTICE; ::_thesis: for S being non empty full infs-inheriting SubRelStr of L holds S is complete LATTICE
let S be non empty full infs-inheriting SubRelStr of L; ::_thesis: S is complete LATTICE
for X being Subset of S holds ex_inf_of X,S
proof
let X be Subset of S; ::_thesis: ex_inf_of X,S
A1: ex_inf_of X,L by YELLOW_0:17;
then "/\" (X,L) in the carrier of S by YELLOW_0:def_18;
hence ex_inf_of X,S by A1, YELLOW_0:63; ::_thesis: verum
end;
then S is complete by Th28;
hence S is complete LATTICE ; ::_thesis: verum
end;
theorem Th31: :: YELLOW_2:31
for L being complete LATTICE
for S being non empty full sups-inheriting SubRelStr of L holds S is complete LATTICE
proof
let L be complete LATTICE; ::_thesis: for S being non empty full sups-inheriting SubRelStr of L holds S is complete LATTICE
let S be non empty full sups-inheriting SubRelStr of L; ::_thesis: S is complete LATTICE
for X being Subset of S holds ex_sup_of X,S
proof
let X be Subset of S; ::_thesis: ex_sup_of X,S
A1: ex_sup_of X,L by YELLOW_0:17;
then "\/" (X,L) in the carrier of S by YELLOW_0:def_19;
hence ex_sup_of X,S by A1, YELLOW_0:64; ::_thesis: verum
end;
then S is complete by YELLOW_0:53;
hence S is complete LATTICE ; ::_thesis: verum
end;
theorem Th32: :: YELLOW_2:32
for L being complete LATTICE
for M being non empty RelStr
for f being Function of L,M st f is sups-preserving holds
Image f is sups-inheriting
proof
let L be complete LATTICE; ::_thesis: for M being non empty RelStr
for f being Function of L,M st f is sups-preserving holds
Image f is sups-inheriting
let M be non empty RelStr ; ::_thesis: for f being Function of L,M st f is sups-preserving holds
Image f is sups-inheriting
let f be Function of L,M; ::_thesis: ( f is sups-preserving implies Image f is sups-inheriting )
assume A1: f is sups-preserving ; ::_thesis: Image f is sups-inheriting
set S = subrelstr (rng f);
for Y being Subset of (subrelstr (rng f)) st ex_sup_of Y,M holds
"\/" (Y,M) in the carrier of (subrelstr (rng f))
proof
let Y be Subset of (subrelstr (rng f)); ::_thesis: ( ex_sup_of Y,M implies "\/" (Y,M) in the carrier of (subrelstr (rng f)) )
assume ex_sup_of Y,M ; ::_thesis: "\/" (Y,M) in the carrier of (subrelstr (rng f))
A2: ( f preserves_sup_of f " Y & ex_sup_of f " Y,L ) by A1, WAYBEL_0:def_33, YELLOW_0:17;
Y c= the carrier of (subrelstr (rng f)) ;
then Y c= rng f by YELLOW_0:def_15;
then "\/" (Y,M) = sup (f .: (f " Y)) by FUNCT_1:77
.= f . (sup (f " Y)) by A2, WAYBEL_0:def_31 ;
then "\/" (Y,M) in rng f by FUNCT_2:4;
hence "\/" (Y,M) in the carrier of (subrelstr (rng f)) by YELLOW_0:def_15; ::_thesis: verum
end;
hence Image f is sups-inheriting by YELLOW_0:def_19; ::_thesis: verum
end;
theorem Th33: :: YELLOW_2:33
for L being complete LATTICE
for M being non empty RelStr
for f being Function of L,M st f is infs-preserving holds
Image f is infs-inheriting
proof
let L be complete LATTICE; ::_thesis: for M being non empty RelStr
for f being Function of L,M st f is infs-preserving holds
Image f is infs-inheriting
let M be non empty RelStr ; ::_thesis: for f being Function of L,M st f is infs-preserving holds
Image f is infs-inheriting
let f be Function of L,M; ::_thesis: ( f is infs-preserving implies Image f is infs-inheriting )
assume A1: f is infs-preserving ; ::_thesis: Image f is infs-inheriting
set S = subrelstr (rng f);
for Y being Subset of (subrelstr (rng f)) st ex_inf_of Y,M holds
"/\" (Y,M) in the carrier of (subrelstr (rng f))
proof
let Y be Subset of (subrelstr (rng f)); ::_thesis: ( ex_inf_of Y,M implies "/\" (Y,M) in the carrier of (subrelstr (rng f)) )
assume ex_inf_of Y,M ; ::_thesis: "/\" (Y,M) in the carrier of (subrelstr (rng f))
A2: ( f preserves_inf_of f " Y & ex_inf_of f " Y,L ) by A1, WAYBEL_0:def_32, YELLOW_0:17;
Y c= the carrier of (subrelstr (rng f)) ;
then Y c= rng f by YELLOW_0:def_15;
then "/\" (Y,M) = inf (f .: (f " Y)) by FUNCT_1:77
.= f . (inf (f " Y)) by A2, WAYBEL_0:def_30 ;
then "/\" (Y,M) in rng f by FUNCT_2:4;
hence "/\" (Y,M) in the carrier of (subrelstr (rng f)) by YELLOW_0:def_15; ::_thesis: verum
end;
hence Image f is infs-inheriting by YELLOW_0:def_18; ::_thesis: verum
end;
theorem :: YELLOW_2:34
for L, M being complete LATTICE
for f being Function of L,M st ( f is sups-preserving or f is infs-preserving ) holds
Image f is complete LATTICE
proof
let L, M be complete LATTICE; ::_thesis: for f being Function of L,M st ( f is sups-preserving or f is infs-preserving ) holds
Image f is complete LATTICE
let f be Function of L,M; ::_thesis: ( ( f is sups-preserving or f is infs-preserving ) implies Image f is complete LATTICE )
assume A1: ( f is sups-preserving or f is infs-preserving ) ; ::_thesis: Image f is complete LATTICE
percases ( f is sups-preserving or f is infs-preserving ) by A1;
suppose f is sups-preserving ; ::_thesis: Image f is complete LATTICE
then Image f is sups-inheriting by Th32;
hence Image f is complete LATTICE by Th31; ::_thesis: verum
end;
suppose f is infs-preserving ; ::_thesis: Image f is complete LATTICE
then Image f is infs-inheriting by Th33;
hence Image f is complete LATTICE by Th30; ::_thesis: verum
end;
end;
end;
theorem :: YELLOW_2:35
for L being complete LATTICE
for f being Function of L,L st f is idempotent & f is directed-sups-preserving holds
( Image f is directed-sups-inheriting & Image f is complete LATTICE )
proof
let L be complete LATTICE; ::_thesis: for f being Function of L,L st f is idempotent & f is directed-sups-preserving holds
( Image f is directed-sups-inheriting & Image f is complete LATTICE )
let f be Function of L,L; ::_thesis: ( f is idempotent & f is directed-sups-preserving implies ( Image f is directed-sups-inheriting & Image f is complete LATTICE ) )
set S = subrelstr (rng f);
set a = the Element of L;
dom f = the carrier of L by FUNCT_2:def_1;
then f . the Element of L in rng f by FUNCT_1:def_3;
then reconsider S9 = subrelstr (rng f) as non empty full SubRelStr of L ;
assume A1: ( f is idempotent & f is directed-sups-preserving ) ; ::_thesis: ( Image f is directed-sups-inheriting & Image f is complete LATTICE )
for X being directed Subset of (subrelstr (rng f)) st X <> {} & ex_sup_of X,L holds
"\/" (X,L) in the carrier of (subrelstr (rng f))
proof
let X be directed Subset of (subrelstr (rng f)); ::_thesis: ( X <> {} & ex_sup_of X,L implies "\/" (X,L) in the carrier of (subrelstr (rng f)) )
X c= the carrier of (subrelstr (rng f)) ;
then A2: X c= rng f by YELLOW_0:def_15;
assume X <> {} ; ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr (rng f)) )
then X is non empty directed Subset of S9 ;
then reconsider X9 = X as non empty directed Subset of L by Th7;
assume A3: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (subrelstr (rng f))
f preserves_sup_of X9 by A1, WAYBEL_0:def_37;
then sup (f .: X9) = f . (sup X9) by A3, WAYBEL_0:def_31;
then sup X9 = f . (sup X9) by A1, A2, Th20;
then "\/" (X,L) in rng f by FUNCT_2:4;
hence "\/" (X,L) in the carrier of (subrelstr (rng f)) by YELLOW_0:def_15; ::_thesis: verum
end;
hence Image f is directed-sups-inheriting by WAYBEL_0:def_4; ::_thesis: Image f is complete LATTICE
rng f = { x where x is Element of L : x = f . x } by A1, Th19;
hence Image f is complete LATTICE by A1, Th16, Th29; ::_thesis: verum
end;
begin
theorem Th36: :: YELLOW_2:36
for L being RelStr
for F being Subset-Family of L st ( for X being Subset of L st X in F holds
X is lower ) holds
meet F is lower Subset of L
proof
let L be RelStr ; ::_thesis: for F being Subset-Family of L st ( for X being Subset of L st X in F holds
X is lower ) holds
meet F is lower Subset of L
let F be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in F holds
X is lower ) implies meet F is lower Subset of L )
reconsider F9 = F as Subset-Family of L ;
assume A1: for X being Subset of L st X in F holds
X is lower ; ::_thesis: meet F is lower Subset of L
reconsider M = meet F9 as Subset of L ;
percases ( F = {} or F <> {} ) ;
suppose F = {} ; ::_thesis: meet F is lower Subset of L
then for x, y being Element of L st x in M & y <= x holds
y in M by SETFAM_1:def_1;
hence meet F is lower Subset of L by WAYBEL_0:def_19; ::_thesis: verum
end;
supposeA2: F <> {} ; ::_thesis: meet F is lower Subset of L
for x, y being Element of L st x in M & y <= x holds
y in M
proof
let x, y be Element of L; ::_thesis: ( x in M & y <= x implies y in M )
assume that
A3: x in M and
A4: y <= x ; ::_thesis: y in M
for Y being set st Y in F holds
y in Y
proof
let Y be set ; ::_thesis: ( Y in F implies y in Y )
assume A5: Y in F ; ::_thesis: y in Y
then reconsider X = Y as Subset of L ;
( X is lower & x in X ) by A1, A3, A5, SETFAM_1:def_1;
hence y in Y by A4, WAYBEL_0:def_19; ::_thesis: verum
end;
hence y in M by A2, SETFAM_1:def_1; ::_thesis: verum
end;
hence meet F is lower Subset of L by WAYBEL_0:def_19; ::_thesis: verum
end;
end;
end;
theorem :: YELLOW_2:37
for L being RelStr
for F being Subset-Family of L st ( for X being Subset of L st X in F holds
X is upper ) holds
meet F is upper Subset of L
proof
let L be RelStr ; ::_thesis: for F being Subset-Family of L st ( for X being Subset of L st X in F holds
X is upper ) holds
meet F is upper Subset of L
let F be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in F holds
X is upper ) implies meet F is upper Subset of L )
reconsider F9 = F as Subset-Family of L ;
assume A1: for X being Subset of L st X in F holds
X is upper ; ::_thesis: meet F is upper Subset of L
reconsider M = meet F9 as Subset of L ;
percases ( F = {} or F <> {} ) ;
suppose F = {} ; ::_thesis: meet F is upper Subset of L
then for x, y being Element of L st x in M & x <= y holds
y in M by SETFAM_1:def_1;
hence meet F is upper Subset of L by WAYBEL_0:def_20; ::_thesis: verum
end;
supposeA2: F <> {} ; ::_thesis: meet F is upper Subset of L
for x, y being Element of L st x in M & x <= y holds
y in M
proof
let x, y be Element of L; ::_thesis: ( x in M & x <= y implies y in M )
assume that
A3: x in M and
A4: x <= y ; ::_thesis: y in M
for Y being set st Y in F holds
y in Y
proof
let Y be set ; ::_thesis: ( Y in F implies y in Y )
assume A5: Y in F ; ::_thesis: y in Y
then reconsider X = Y as Subset of L ;
( X is upper & x in X ) by A1, A3, A5, SETFAM_1:def_1;
hence y in Y by A4, WAYBEL_0:def_20; ::_thesis: verum
end;
hence y in M by A2, SETFAM_1:def_1; ::_thesis: verum
end;
hence meet F is upper Subset of L by WAYBEL_0:def_20; ::_thesis: verum
end;
end;
end;
theorem Th38: :: YELLOW_2:38
for L being antisymmetric with_suprema RelStr
for F being Subset-Family of L st ( for X being Subset of L st X in F holds
( X is lower & X is directed ) ) holds
meet F is directed Subset of L
proof
let L be antisymmetric with_suprema RelStr ; ::_thesis: for F being Subset-Family of L st ( for X being Subset of L st X in F holds
( X is lower & X is directed ) ) holds
meet F is directed Subset of L
let F be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in F holds
( X is lower & X is directed ) ) implies meet F is directed Subset of L )
assume A1: for X being Subset of L st X in F holds
( X is lower & X is directed ) ; ::_thesis: meet F is directed Subset of L
reconsider F9 = F as Subset-Family of L ;
reconsider M = meet F9 as Subset of L ;
percases ( F = {} or F <> {} ) ;
supposeA2: F = {} ; ::_thesis: meet F is directed Subset of L
M is directed
proof
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in M or not y in M or ex b1 being Element of the carrier of L st
( b1 in M & x <= b1 & y <= b1 ) )
assume that
A3: x in M and
y in M ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in M & x <= b1 & y <= b1 )
thus ex b1 being Element of the carrier of L st
( b1 in M & x <= b1 & y <= b1 ) by A2, A3, SETFAM_1:def_1; ::_thesis: verum
end;
hence meet F is directed Subset of L ; ::_thesis: verum
end;
supposeA4: F <> {} ; ::_thesis: meet F is directed Subset of L
M is directed
proof
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in M or not y in M or ex b1 being Element of the carrier of L st
( b1 in M & x <= b1 & y <= b1 ) )
assume that
A5: x in M and
A6: y in M ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in M & x <= b1 & y <= b1 )
take z = x "\/" y; ::_thesis: ( z in M & x <= z & y <= z )
for Y being set st Y in F holds
z in Y
proof
let Y be set ; ::_thesis: ( Y in F implies z in Y )
assume A7: Y in F ; ::_thesis: z in Y
then reconsider X = Y as Subset of L ;
A8: y in X by A6, A7, SETFAM_1:def_1;
( X is lower & X is directed & x in X ) by A1, A5, A7, SETFAM_1:def_1;
hence z in Y by A8, WAYBEL_0:40; ::_thesis: verum
end;
hence z in M by A4, SETFAM_1:def_1; ::_thesis: ( x <= z & y <= z )
thus ( x <= z & y <= z ) by YELLOW_0:22; ::_thesis: verum
end;
hence meet F is directed Subset of L ; ::_thesis: verum
end;
end;
end;
theorem :: YELLOW_2:39
for L being antisymmetric with_infima RelStr
for F being Subset-Family of L st ( for X being Subset of L st X in F holds
( X is upper & X is filtered ) ) holds
meet F is filtered Subset of L
proof
let L be antisymmetric with_infima RelStr ; ::_thesis: for F being Subset-Family of L st ( for X being Subset of L st X in F holds
( X is upper & X is filtered ) ) holds
meet F is filtered Subset of L
let F be Subset-Family of L; ::_thesis: ( ( for X being Subset of L st X in F holds
( X is upper & X is filtered ) ) implies meet F is filtered Subset of L )
assume A1: for X being Subset of L st X in F holds
( X is upper & X is filtered ) ; ::_thesis: meet F is filtered Subset of L
reconsider F9 = F as Subset-Family of L ;
reconsider M = meet F9 as Subset of L ;
percases ( F = {} or F <> {} ) ;
supposeA2: F = {} ; ::_thesis: meet F is filtered Subset of L
M is filtered
proof
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in M or not y in M or ex b1 being Element of the carrier of L st
( b1 in M & b1 <= x & b1 <= y ) )
assume that
A3: x in M and
y in M ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in M & b1 <= x & b1 <= y )
thus ex b1 being Element of the carrier of L st
( b1 in M & b1 <= x & b1 <= y ) by A2, A3, SETFAM_1:def_1; ::_thesis: verum
end;
hence meet F is filtered Subset of L ; ::_thesis: verum
end;
supposeA4: F <> {} ; ::_thesis: meet F is filtered Subset of L
M is filtered
proof
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in M or not y in M or ex b1 being Element of the carrier of L st
( b1 in M & b1 <= x & b1 <= y ) )
assume that
A5: x in M and
A6: y in M ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in M & b1 <= x & b1 <= y )
take z = x "/\" y; ::_thesis: ( z in M & z <= x & z <= y )
for Y being set st Y in F holds
z in Y
proof
let Y be set ; ::_thesis: ( Y in F implies z in Y )
assume A7: Y in F ; ::_thesis: z in Y
then reconsider X = Y as Subset of L ;
A8: y in X by A6, A7, SETFAM_1:def_1;
( X is upper & X is filtered & x in X ) by A1, A5, A7, SETFAM_1:def_1;
hence z in Y by A8, WAYBEL_0:41; ::_thesis: verum
end;
hence z in M by A4, SETFAM_1:def_1; ::_thesis: ( z <= x & z <= y )
thus ( z <= x & z <= y ) by YELLOW_0:23; ::_thesis: verum
end;
hence meet F is filtered Subset of L ; ::_thesis: verum
end;
end;
end;
theorem Th40: :: YELLOW_2:40
for L being with_infima Poset
for I, J being Ideal of L holds I /\ J is Ideal of L
proof
let L be with_infima Poset; ::_thesis: for I, J being Ideal of L holds I /\ J is Ideal of L
let I, J be Ideal of L; ::_thesis: I /\ J is Ideal of L
set i = the Element of I;
set j = the Element of J;
set a = the Element of I "/\" the Element of J;
the Element of I "/\" the Element of J <= the Element of J by YELLOW_0:23;
then A1: the Element of I "/\" the Element of J in J by WAYBEL_0:def_19;
the Element of I "/\" the Element of J <= the Element of I by YELLOW_0:23;
then the Element of I "/\" the Element of J in I by WAYBEL_0:def_19;
hence I /\ J is Ideal of L by A1, WAYBEL_0:27, WAYBEL_0:44, XBOOLE_0:def_4; ::_thesis: verum
end;
registration
let L be non empty reflexive transitive RelStr ;
cluster Ids L -> non empty ;
correctness
coherence
not Ids L is empty ;
proof
set x = the Element of L;
downarrow the Element of L in { Y where Y is Ideal of L : verum } ;
hence not Ids L is empty ; ::_thesis: verum
end;
end;
theorem Th41: :: YELLOW_2:41
for x being set
for L being non empty reflexive transitive RelStr holds
( x is Element of (InclPoset (Ids L)) iff x is Ideal of L )
proof
let x be set ; ::_thesis: for L being non empty reflexive transitive RelStr holds
( x is Element of (InclPoset (Ids L)) iff x is Ideal of L )
let L be non empty reflexive transitive RelStr ; ::_thesis: ( x is Element of (InclPoset (Ids L)) iff x is Ideal of L )
hereby ::_thesis: ( x is Ideal of L implies x is Element of (InclPoset (Ids L)) )
assume x is Element of (InclPoset (Ids L)) ; ::_thesis: x is Ideal of L
then x in the carrier of (InclPoset (Ids L)) ;
then x in Ids L by YELLOW_1:1;
then ex J being Ideal of L st J = x ;
hence x is Ideal of L ; ::_thesis: verum
end;
assume x is Ideal of L ; ::_thesis: x is Element of (InclPoset (Ids L))
then x in { Y where Y is Ideal of L : verum } ;
hence x is Element of (InclPoset (Ids L)) by YELLOW_1:1; ::_thesis: verum
end;
theorem Th42: :: YELLOW_2:42
for x being set
for L being non empty reflexive transitive RelStr
for I being Element of (InclPoset (Ids L)) st x in I holds
x is Element of L
proof
let x be set ; ::_thesis: for L being non empty reflexive transitive RelStr
for I being Element of (InclPoset (Ids L)) st x in I holds
x is Element of L
let L be non empty reflexive transitive RelStr ; ::_thesis: for I being Element of (InclPoset (Ids L)) st x in I holds
x is Element of L
let I be Element of (InclPoset (Ids L)); ::_thesis: ( x in I implies x is Element of L )
reconsider I9 = I as non empty Subset of L by Th41;
assume x in I ; ::_thesis: x is Element of L
then reconsider x9 = x as Element of I9 ;
x9 in the carrier of L ;
hence x is Element of L ; ::_thesis: verum
end;
theorem :: YELLOW_2:43
for L being with_infima Poset
for x, y being Element of (InclPoset (Ids L)) holds x "/\" y = x /\ y
proof
let L be with_infima Poset; ::_thesis: for x, y being Element of (InclPoset (Ids L)) holds x "/\" y = x /\ y
let x, y be Element of (InclPoset (Ids L)); ::_thesis: x "/\" y = x /\ y
reconsider x9 = x, y9 = y as Ideal of L by Th41;
x9 /\ y9 is Ideal of L by Th40;
then x9 /\ y9 in { X where X is Ideal of L : verum } ;
hence x "/\" y = x /\ y by YELLOW_1:9; ::_thesis: verum
end;
registration
let L be with_infima Poset;
cluster InclPoset (Ids L) -> with_infima ;
correctness
coherence
InclPoset (Ids L) is with_infima ;
proof
for x, y being set st x in Ids L & y in Ids L holds
x /\ y in Ids L
proof
let x, y be set ; ::_thesis: ( x in Ids L & y in Ids L implies x /\ y in Ids L )
assume that
A1: x in Ids L and
A2: y in Ids L ; ::_thesis: x /\ y in Ids L
consider I being Ideal of L such that
A3: I = x by A1;
consider J being Ideal of L such that
A4: J = y by A2;
I /\ J is Ideal of L by Th40;
hence x /\ y in Ids L by A3, A4; ::_thesis: verum
end;
hence InclPoset (Ids L) is with_infima by YELLOW_1:12; ::_thesis: verum
end;
end;
theorem Th44: :: YELLOW_2:44
for L being with_suprema Poset
for x, y being Element of (InclPoset (Ids L)) ex Z being Subset of L st
( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st
( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z )
proof
let L be with_suprema Poset; ::_thesis: for x, y being Element of (InclPoset (Ids L)) ex Z being Subset of L st
( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st
( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z )
set P = InclPoset (Ids L);
let x, y be Element of (InclPoset (Ids L)); ::_thesis: ex Z being Subset of L st
( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st
( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z )
defpred S1[ Element of L] means ( $1 in x or $1 in y or ex a, b being Element of L st
( a in x & b in y & $1 = a "\/" b ) );
reconsider Z = { z where z is Element of L : S1[z] } as Subset of L from DOMAIN_1:sch_7();
take Z ; ::_thesis: ( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st
( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z )
reconsider x9 = x, y9 = y as Ideal of L by Th41;
set z = the Element of x9;
the Element of x9 in Z ;
then reconsider Z = Z as non empty Subset of L ;
set DZ = downarrow Z;
for u, v being Element of L st u in Z & v in Z holds
ex z being Element of L st
( z in Z & u <= z & v <= z )
proof
A1: for p, q being Element of L st p in y & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) holds
ex z being Element of L st
( z in Z & p <= z & q <= z )
proof
let p, q be Element of L; ::_thesis: ( p in y & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) implies ex z being Element of L st
( z in Z & p <= z & q <= z ) )
assume that
A2: p in y and
A3: ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ; ::_thesis: ex z being Element of L st
( z in Z & p <= z & q <= z )
consider a, b being Element of L such that
A4: a in x and
A5: b in y and
A6: q = a "\/" b by A3;
reconsider c = b "\/" p as Element of L ;
take z = a "\/" c; ::_thesis: ( z in Z & p <= z & q <= z )
c in y9 by A2, A5, WAYBEL_0:40;
hence z in Z by A4; ::_thesis: ( p <= z & q <= z )
A7: c <= z by YELLOW_0:22;
A8: ( p <= c & a <= z ) by YELLOW_0:22;
b <= c by YELLOW_0:22;
then b <= z by A7, ORDERS_2:3;
hence ( p <= z & q <= z ) by A6, A7, A8, ORDERS_2:3, YELLOW_0:22; ::_thesis: verum
end;
A9: for p, q being Element of L st p in x & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) holds
ex z being Element of L st
( z in Z & p <= z & q <= z )
proof
let p, q be Element of L; ::_thesis: ( p in x & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) implies ex z being Element of L st
( z in Z & p <= z & q <= z ) )
assume that
A10: p in x and
A11: ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ; ::_thesis: ex z being Element of L st
( z in Z & p <= z & q <= z )
consider a, b being Element of L such that
A12: a in x and
A13: b in y and
A14: q = a "\/" b by A11;
reconsider c = a "\/" p as Element of L ;
take z = c "\/" b; ::_thesis: ( z in Z & p <= z & q <= z )
c in x9 by A10, A12, WAYBEL_0:40;
hence z in Z by A13; ::_thesis: ( p <= z & q <= z )
A15: c <= z by YELLOW_0:22;
A16: ( p <= c & b <= z ) by YELLOW_0:22;
a <= c by YELLOW_0:22;
then a <= z by A15, ORDERS_2:3;
hence ( p <= z & q <= z ) by A14, A15, A16, ORDERS_2:3, YELLOW_0:22; ::_thesis: verum
end;
let u, v be Element of L; ::_thesis: ( u in Z & v in Z implies ex z being Element of L st
( z in Z & u <= z & v <= z ) )
assume that
A17: u in Z and
A18: v in Z ; ::_thesis: ex z being Element of L st
( z in Z & u <= z & v <= z )
consider p being Element of L such that
A19: p = u and
A20: ( p in x or p in y or ex a, b being Element of L st
( a in x & b in y & p = a "\/" b ) ) by A17;
consider q being Element of L such that
A21: q = v and
A22: ( q in x or q in y or ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ) by A18;
percases ( ( p in x & q in x ) or ( p in x & q in y ) or ( p in x & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ) or ( p in y & q in x ) or ( p in y & q in y ) or ( p in y & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ) or ( q in x & ex a, b being Element of L st
( a in x & b in y & p = a "\/" b ) ) or ( q in y & ex a, b being Element of L st
( a in x & b in y & p = a "\/" b ) ) or ( ex a, b being Element of L st
( a in x & b in y & p = a "\/" b ) & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ) ) by A20, A22;
suppose ( p in x & q in x ) ; ::_thesis: ex z being Element of L st
( z in Z & u <= z & v <= z )
then consider z being Element of L such that
A23: ( z in x9 & p <= z & q <= z ) by WAYBEL_0:def_1;
take z ; ::_thesis: ( z in Z & u <= z & v <= z )
thus ( z in Z & u <= z & v <= z ) by A19, A21, A23; ::_thesis: verum
end;
supposeA24: ( p in x & q in y ) ; ::_thesis: ex z being Element of L st
( z in Z & u <= z & v <= z )
take p "\/" q ; ::_thesis: ( p "\/" q in Z & u <= p "\/" q & v <= p "\/" q )
thus ( p "\/" q in Z & u <= p "\/" q & v <= p "\/" q ) by A19, A21, A24, YELLOW_0:22; ::_thesis: verum
end;
suppose ( p in x & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ) ; ::_thesis: ex z being Element of L st
( z in Z & u <= z & v <= z )
then consider z being Element of L such that
A25: ( z in Z & p <= z & q <= z ) by A9;
take z ; ::_thesis: ( z in Z & u <= z & v <= z )
thus ( z in Z & u <= z & v <= z ) by A19, A21, A25; ::_thesis: verum
end;
supposeA26: ( p in y & q in x ) ; ::_thesis: ex z being Element of L st
( z in Z & u <= z & v <= z )
take q "\/" p ; ::_thesis: ( q "\/" p in Z & u <= q "\/" p & v <= q "\/" p )
thus ( q "\/" p in Z & u <= q "\/" p & v <= q "\/" p ) by A19, A21, A26, YELLOW_0:22; ::_thesis: verum
end;
suppose ( p in y & q in y ) ; ::_thesis: ex z being Element of L st
( z in Z & u <= z & v <= z )
then consider z being Element of L such that
A27: ( z in y9 & p <= z & q <= z ) by WAYBEL_0:def_1;
take z ; ::_thesis: ( z in Z & u <= z & v <= z )
thus ( z in Z & u <= z & v <= z ) by A19, A21, A27; ::_thesis: verum
end;
suppose ( p in y & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ) ; ::_thesis: ex z being Element of L st
( z in Z & u <= z & v <= z )
then consider z being Element of L such that
A28: ( z in Z & p <= z & q <= z ) by A1;
take z ; ::_thesis: ( z in Z & u <= z & v <= z )
thus ( z in Z & u <= z & v <= z ) by A19, A21, A28; ::_thesis: verum
end;
suppose ( q in x & ex a, b being Element of L st
( a in x & b in y & p = a "\/" b ) ) ; ::_thesis: ex z being Element of L st
( z in Z & u <= z & v <= z )
then consider z being Element of L such that
A29: ( z in Z & q <= z & p <= z ) by A9;
take z ; ::_thesis: ( z in Z & u <= z & v <= z )
thus ( z in Z & u <= z & v <= z ) by A19, A21, A29; ::_thesis: verum
end;
suppose ( q in y & ex a, b being Element of L st
( a in x & b in y & p = a "\/" b ) ) ; ::_thesis: ex z being Element of L st
( z in Z & u <= z & v <= z )
then consider z being Element of L such that
A30: ( z in Z & q <= z & p <= z ) by A1;
take z ; ::_thesis: ( z in Z & u <= z & v <= z )
thus ( z in Z & u <= z & v <= z ) by A19, A21, A30; ::_thesis: verum
end;
suppose ( ex a, b being Element of L st
( a in x & b in y & p = a "\/" b ) & ex a, b being Element of L st
( a in x & b in y & q = a "\/" b ) ) ; ::_thesis: ex z being Element of L st
( z in Z & u <= z & v <= z )
then consider a, b, c, d being Element of L such that
A31: ( a in x & b in y ) and
A32: p = a "\/" b and
A33: ( c in x & d in y ) and
A34: q = c "\/" d ;
reconsider ac = a "\/" c, bd = b "\/" d as Element of L ;
take z = ac "\/" bd; ::_thesis: ( z in Z & u <= z & v <= z )
( ac in x9 & bd in y9 ) by A31, A33, WAYBEL_0:40;
hence z in Z ; ::_thesis: ( u <= z & v <= z )
A35: ac <= z by YELLOW_0:22;
A36: bd <= z by YELLOW_0:22;
b <= bd by YELLOW_0:22;
then A37: b <= z by A36, ORDERS_2:3;
a <= ac by YELLOW_0:22;
then a <= z by A35, ORDERS_2:3;
hence u <= z by A19, A32, A37, YELLOW_0:22; ::_thesis: v <= z
d <= bd by YELLOW_0:22;
then A38: d <= z by A36, ORDERS_2:3;
c <= ac by YELLOW_0:22;
then c <= z by A35, ORDERS_2:3;
hence v <= z by A21, A34, A38, YELLOW_0:22; ::_thesis: verum
end;
end;
end;
then Z is directed by WAYBEL_0:def_1;
then reconsider DZ = downarrow Z as Element of (InclPoset (Ids L)) by Th41;
A39: for d being Element of (InclPoset (Ids L)) st d >= x & d >= y holds
DZ <= d
proof
let d be Element of (InclPoset (Ids L)); ::_thesis: ( d >= x & d >= y implies DZ <= d )
assume that
A40: x <= d and
A41: y <= d ; ::_thesis: DZ <= d
A42: y c= d by A41, YELLOW_1:3;
A43: x c= d by A40, YELLOW_1:3;
DZ c= d
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in DZ or p in d )
assume p in DZ ; ::_thesis: p in d
then p in { q where q is Element of L : ex u being Element of L st
( q <= u & u in Z ) } by WAYBEL_0:14;
then consider p9 being Element of L such that
A44: p9 = p and
A45: ex u being Element of L st
( p9 <= u & u in Z ) ;
consider u being Element of L such that
A46: p9 <= u and
A47: u in Z by A45;
consider z being Element of L such that
A48: z = u and
A49: ( z in x or z in y or ex a, b being Element of L st
( a in x & b in y & z = a "\/" b ) ) by A47;
percases ( z in x or z in y or ex a, b being Element of L st
( a in x & b in y & z = a "\/" b ) ) by A49;
suppose z in x ; ::_thesis: p in d
then p in x9 by A44, A46, A48, WAYBEL_0:def_19;
hence p in d by A43; ::_thesis: verum
end;
suppose z in y ; ::_thesis: p in d
then p in y9 by A44, A46, A48, WAYBEL_0:def_19;
hence p in d by A42; ::_thesis: verum
end;
supposeA50: ex a, b being Element of L st
( a in x & b in y & z = a "\/" b ) ; ::_thesis: p in d
reconsider d9 = d as Ideal of L by Th41;
u in d9 by A43, A42, A48, A50, WAYBEL_0:40;
hence p in d by A44, A46, WAYBEL_0:def_19; ::_thesis: verum
end;
end;
end;
hence DZ <= d by YELLOW_1:3; ::_thesis: verum
end;
y c= DZ
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in y or a in DZ )
A51: Z c= DZ by WAYBEL_0:16;
assume A52: a in y ; ::_thesis: a in DZ
then reconsider a9 = a as Element of L by Th42;
a9 in Z by A52;
hence a in DZ by A51; ::_thesis: verum
end;
then A53: y <= DZ by YELLOW_1:3;
x c= DZ
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in x or a in DZ )
A54: Z c= DZ by WAYBEL_0:16;
assume A55: a in x ; ::_thesis: a in DZ
then reconsider a9 = a as Element of L by Th42;
a9 in Z by A55;
hence a in DZ by A54; ::_thesis: verum
end;
then x <= DZ by YELLOW_1:3;
hence ( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st
( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z ) by A53, A39, YELLOW_0:18; ::_thesis: verum
end;
registration
let L be with_suprema Poset;
cluster InclPoset (Ids L) -> with_suprema ;
correctness
coherence
InclPoset (Ids L) is with_suprema ;
proof
set P = InclPoset (Ids L);
for x, y being Element of (InclPoset (Ids L)) ex z being Element of (InclPoset (Ids L)) st
( x <= z & y <= z & ( for z9 being Element of (InclPoset (Ids L)) st x <= z9 & y <= z9 holds
z <= z9 ) )
proof
let x, y be Element of (InclPoset (Ids L)); ::_thesis: ex z being Element of (InclPoset (Ids L)) st
( x <= z & y <= z & ( for z9 being Element of (InclPoset (Ids L)) st x <= z9 & y <= z9 holds
z <= z9 ) )
take x "\/" y ; ::_thesis: ( x <= x "\/" y & y <= x "\/" y & ( for z9 being Element of (InclPoset (Ids L)) st x <= z9 & y <= z9 holds
x "\/" y <= z9 ) )
ex Z being Subset of L st
( Z = { z where z is Element of L : ( z in x or z in y or ex a, b being Element of L st
( a in x & b in y & z = a "\/" b ) ) } & ex_sup_of {x,y}, InclPoset (Ids L) & x "\/" y = downarrow Z ) by Th44;
hence ( x <= x "\/" y & y <= x "\/" y & ( for z9 being Element of (InclPoset (Ids L)) st x <= z9 & y <= z9 holds
x "\/" y <= z9 ) ) by YELLOW_0:18; ::_thesis: verum
end;
hence InclPoset (Ids L) is with_suprema by LATTICE3:def_10; ::_thesis: verum
end;
end;
theorem Th45: :: YELLOW_2:45
for L being lower-bounded sup-Semilattice
for X being non empty Subset of (Ids L) holds meet X is Ideal of L
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for X being non empty Subset of (Ids L) holds meet X is Ideal of L
let X be non empty Subset of (Ids L); ::_thesis: meet X is Ideal of L
A1: for J being set st J in X holds
J is Ideal of L
proof
let J be set ; ::_thesis: ( J in X implies J is Ideal of L )
assume J in X ; ::_thesis: J is Ideal of L
then J in Ids L ;
then ex Y being Ideal of L st Y = J ;
hence J is Ideal of L ; ::_thesis: verum
end;
X c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in bool the carrier of L )
assume x in X ; ::_thesis: x in bool the carrier of L
then x is Ideal of L by A1;
hence x in bool the carrier of L ; ::_thesis: verum
end;
then reconsider F = X as Subset-Family of L ;
for J being Subset of L st J in F holds
J is lower by A1;
then reconsider I = meet X as lower Subset of L by Th36;
for J being set st J in X holds
Bottom L in J
proof
let J be set ; ::_thesis: ( J in X implies Bottom L in J )
assume J in X ; ::_thesis: Bottom L in J
then reconsider J9 = J as Ideal of L by A1;
set j = the Element of J9;
Bottom L <= the Element of J9 by YELLOW_0:44;
hence Bottom L in J by WAYBEL_0:def_19; ::_thesis: verum
end;
then reconsider I = I as non empty lower Subset of L by SETFAM_1:def_1;
for J being Subset of L st J in F holds
( J is lower & J is directed ) by A1;
then I is Ideal of L by Th38;
hence meet X is Ideal of L ; ::_thesis: verum
end;
theorem Th46: :: YELLOW_2:46
for L being lower-bounded sup-Semilattice
for A being non empty Subset of (InclPoset (Ids L)) holds
( ex_inf_of A, InclPoset (Ids L) & inf A = meet A )
proof
let L be lower-bounded sup-Semilattice; ::_thesis: for A being non empty Subset of (InclPoset (Ids L)) holds
( ex_inf_of A, InclPoset (Ids L) & inf A = meet A )
let A be non empty Subset of (InclPoset (Ids L)); ::_thesis: ( ex_inf_of A, InclPoset (Ids L) & inf A = meet A )
set P = InclPoset (Ids L);
reconsider A9 = A as non empty Subset of (Ids L) by YELLOW_1:1;
meet A9 is Ideal of L by Th45;
then reconsider I = meet A as Element of (InclPoset (Ids L)) by Th41;
A1: for b being Element of (InclPoset (Ids L)) st b is_<=_than A holds
I >= b
proof
let b be Element of (InclPoset (Ids L)); ::_thesis: ( b is_<=_than A implies I >= b )
assume A2: A is_>=_than b ; ::_thesis: I >= b
A3: for J being set st J in A holds
b c= J
proof
let J be set ; ::_thesis: ( J in A implies b c= J )
assume A4: J in A ; ::_thesis: b c= J
then reconsider y = J as Element of (InclPoset (Ids L)) ;
b <= y by A2, A4, LATTICE3:def_8;
hence b c= J by YELLOW_1:3; ::_thesis: verum
end;
b c= I
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in b or c in I )
assume A5: c in b ; ::_thesis: c in I
for J being set st J in A holds
c in J
proof
let J be set ; ::_thesis: ( J in A implies c in J )
assume J in A ; ::_thesis: c in J
then b c= J by A3;
hence c in J by A5; ::_thesis: verum
end;
hence c in I by SETFAM_1:def_1; ::_thesis: verum
end;
hence I >= b by YELLOW_1:3; ::_thesis: verum
end;
I is_<=_than A
proof
let y be Element of (InclPoset (Ids L)); :: according to LATTICE3:def_8 ::_thesis: ( not y in A or I <= y )
assume A6: y in A ; ::_thesis: I <= y
I c= y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in I or x in y )
assume x in I ; ::_thesis: x in y
hence x in y by A6, SETFAM_1:def_1; ::_thesis: verum
end;
hence I <= y by YELLOW_1:3; ::_thesis: verum
end;
hence ( ex_inf_of A, InclPoset (Ids L) & inf A = meet A ) by A1, YELLOW_0:31; ::_thesis: verum
end;
theorem Th47: :: YELLOW_2:47
for L being with_suprema Poset holds
( ex_inf_of {} , InclPoset (Ids L) & "/\" ({},(InclPoset (Ids L))) = [#] L )
proof
let L be with_suprema Poset; ::_thesis: ( ex_inf_of {} , InclPoset (Ids L) & "/\" ({},(InclPoset (Ids L))) = [#] L )
set P = InclPoset (Ids L);
reconsider I = [#] L as Element of (InclPoset (Ids L)) by Th41;
A1: for b being Element of (InclPoset (Ids L)) st b is_<=_than {} holds
I >= b
proof
let b be Element of (InclPoset (Ids L)); ::_thesis: ( b is_<=_than {} implies I >= b )
reconsider b9 = b as Ideal of L by Th41;
assume {} is_>=_than b ; ::_thesis: I >= b
b9 c= [#] L ;
hence I >= b by YELLOW_1:3; ::_thesis: verum
end;
I is_<=_than {}
proof
let y be Element of (InclPoset (Ids L)); :: according to LATTICE3:def_8 ::_thesis: ( not y in {} or I <= y )
assume y in {} ; ::_thesis: I <= y
hence I <= y ; ::_thesis: verum
end;
hence ( ex_inf_of {} , InclPoset (Ids L) & "/\" ({},(InclPoset (Ids L))) = [#] L ) by A1, YELLOW_0:31; ::_thesis: verum
end;
theorem Th48: :: YELLOW_2:48
for L being lower-bounded sup-Semilattice holds InclPoset (Ids L) is complete
proof
let L be lower-bounded sup-Semilattice; ::_thesis: InclPoset (Ids L) is complete
set P = InclPoset (Ids L);
for A being Subset of (InclPoset (Ids L)) holds ex_inf_of A, InclPoset (Ids L)
proof
let A be Subset of (InclPoset (Ids L)); ::_thesis: ex_inf_of A, InclPoset (Ids L)
percases ( A = {} or A <> {} ) ;
suppose A = {} ; ::_thesis: ex_inf_of A, InclPoset (Ids L)
hence ex_inf_of A, InclPoset (Ids L) by Th47; ::_thesis: verum
end;
suppose A <> {} ; ::_thesis: ex_inf_of A, InclPoset (Ids L)
hence ex_inf_of A, InclPoset (Ids L) by Th46; ::_thesis: verum
end;
end;
end;
hence InclPoset (Ids L) is complete by Th28; ::_thesis: verum
end;
registration
let L be lower-bounded sup-Semilattice;
cluster InclPoset (Ids L) -> complete ;
correctness
coherence
InclPoset (Ids L) is complete ;
by Th48;
end;
begin
definition
let L be non empty Poset;
func SupMap L -> Function of (InclPoset (Ids L)),L means :Def3: :: YELLOW_2:def 3
for I being Ideal of L holds it . I = sup I;
existence
ex b1 being Function of (InclPoset (Ids L)),L st
for I being Ideal of L holds b1 . I = sup I
proof
deffunc H1( set ) -> Element of the carrier of L = "\/" ($1,L);
set P = InclPoset (Ids L);
A1: for I being set st I in the carrier of (InclPoset (Ids L)) holds
H1(I) in the carrier of L ;
ex f being Function of the carrier of (InclPoset (Ids L)), the carrier of L st
for I being set st I in the carrier of (InclPoset (Ids L)) holds
f . I = H1(I) from FUNCT_2:sch_2(A1);
then consider f being Function of the carrier of (InclPoset (Ids L)), the carrier of L such that
A2: for I being set st I in the carrier of (InclPoset (Ids L)) holds
f . I = "\/" (I,L) ;
reconsider f = f as Function of (InclPoset (Ids L)),L ;
take f ; ::_thesis: for I being Ideal of L holds f . I = sup I
for I being Ideal of L holds f . I = sup I
proof
let I be Ideal of L; ::_thesis: f . I = sup I
I in the carrier of RelStr(# (Ids L),(RelIncl (Ids L)) #) ;
then I in the carrier of (InclPoset (Ids L)) by YELLOW_1:def_1;
hence f . I = sup I by A2; ::_thesis: verum
end;
hence for I being Ideal of L holds f . I = sup I ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (InclPoset (Ids L)),L st ( for I being Ideal of L holds b1 . I = sup I ) & ( for I being Ideal of L holds b2 . I = sup I ) holds
b1 = b2
proof
set P = InclPoset (Ids L);
let f, g be Function of (InclPoset (Ids L)),L; ::_thesis: ( ( for I being Ideal of L holds f . I = sup I ) & ( for I being Ideal of L holds g . I = sup I ) implies f = g )
assume that
A3: for I being Ideal of L holds f . I = sup I and
A4: for I being Ideal of L holds g . I = sup I ; ::_thesis: f = g
A5: the carrier of (InclPoset (Ids L)) = the carrier of RelStr(# (Ids L),(RelIncl (Ids L)) #) by YELLOW_1:def_1
.= Ids L ;
A6: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(InclPoset_(Ids_L))_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in the carrier of (InclPoset (Ids L)) implies f . x = g . x )
assume x in the carrier of (InclPoset (Ids L)) ; ::_thesis: f . x = g . x
then ex I being Ideal of L st x = I by A5;
then reconsider I = x as Ideal of L ;
f . I = sup I by A3;
hence f . x = g . x by A4; ::_thesis: verum
end;
( dom f = the carrier of (InclPoset (Ids L)) & dom g = the carrier of (InclPoset (Ids L)) ) by FUNCT_2:def_1;
hence f = g by A6, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines SupMap YELLOW_2:def_3_:_
for L being non empty Poset
for b2 being Function of (InclPoset (Ids L)),L holds
( b2 = SupMap L iff for I being Ideal of L holds b2 . I = sup I );
theorem Th49: :: YELLOW_2:49
for L being non empty Poset holds
( dom (SupMap L) = Ids L & rng (SupMap L) is Subset of L )
proof
let L be non empty Poset; ::_thesis: ( dom (SupMap L) = Ids L & rng (SupMap L) is Subset of L )
set P = InclPoset (Ids L);
thus dom (SupMap L) = the carrier of (InclPoset (Ids L)) by FUNCT_2:def_1
.= the carrier of RelStr(# (Ids L),(RelIncl (Ids L)) #) by YELLOW_1:def_1
.= Ids L ; ::_thesis: rng (SupMap L) is Subset of L
thus rng (SupMap L) is Subset of L ; ::_thesis: verum
end;
theorem :: YELLOW_2:50
for x being set
for L being non empty Poset holds
( x in dom (SupMap L) iff x is Ideal of L )
proof
let x be set ; ::_thesis: for L being non empty Poset holds
( x in dom (SupMap L) iff x is Ideal of L )
let L be non empty Poset; ::_thesis: ( x in dom (SupMap L) iff x is Ideal of L )
hereby ::_thesis: ( x is Ideal of L implies x in dom (SupMap L) )
assume x in dom (SupMap L) ; ::_thesis: x is Ideal of L
then x in Ids L by Th49;
then ex I being Ideal of L st x = I ;
hence x is Ideal of L ; ::_thesis: verum
end;
assume x is Ideal of L ; ::_thesis: x in dom (SupMap L)
then x in { X where X is Ideal of L : verum } ;
hence x in dom (SupMap L) by Th49; ::_thesis: verum
end;
theorem Th51: :: YELLOW_2:51
for L being non empty up-complete Poset holds SupMap L is monotone
proof
let L be non empty up-complete Poset; ::_thesis: SupMap L is monotone
set P = InclPoset (Ids L);
set f = SupMap L;
for x, y being Element of (InclPoset (Ids L)) st x <= y holds
for a, b being Element of L st a = (SupMap L) . x & b = (SupMap L) . y holds
a <= b
proof
let x, y be Element of (InclPoset (Ids L)); ::_thesis: ( x <= y implies for a, b being Element of L st a = (SupMap L) . x & b = (SupMap L) . y holds
a <= b )
assume A1: x <= y ; ::_thesis: for a, b being Element of L st a = (SupMap L) . x & b = (SupMap L) . y holds
a <= b
reconsider I = x, J = y as Ideal of L by Th41;
A2: I c= J by A1, YELLOW_1:3;
A3: ( ex_sup_of I,L & ex_sup_of J,L ) by WAYBEL_0:75;
A4: ( (SupMap L) . x = sup I & (SupMap L) . y = sup J ) by Def3;
let a, b be Element of L; ::_thesis: ( a = (SupMap L) . x & b = (SupMap L) . y implies a <= b )
assume ( a = (SupMap L) . x & b = (SupMap L) . y ) ; ::_thesis: a <= b
hence a <= b by A3, A2, A4, YELLOW_0:34; ::_thesis: verum
end;
hence SupMap L is monotone by ORDERS_3:def_5; ::_thesis: verum
end;
registration
let L be non empty up-complete Poset;
cluster SupMap L -> monotone ;
correctness
coherence
SupMap L is monotone ;
by Th51;
end;
definition
let L be non empty Poset;
func IdsMap L -> Function of L,(InclPoset (Ids L)) means :Def4: :: YELLOW_2:def 4
for x being Element of L holds it . x = downarrow x;
existence
ex b1 being Function of L,(InclPoset (Ids L)) st
for x being Element of L holds b1 . x = downarrow x
proof
deffunc H1( Element of L) -> Element of bool the carrier of L = downarrow $1;
A1: for x being Element of L holds H1(x) is Element of (InclPoset (Ids L)) by Th41;
thus ex m being Function of L,(InclPoset (Ids L)) st
for x being Element of L holds m . x = H1(x) from FUNCT_2:sch_9(A1); ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of L,(InclPoset (Ids L)) st ( for x being Element of L holds b1 . x = downarrow x ) & ( for x being Element of L holds b2 . x = downarrow x ) holds
b1 = b2
proof
let f1, f2 be Function of L,(InclPoset (Ids L)); ::_thesis: ( ( for x being Element of L holds f1 . x = downarrow x ) & ( for x being Element of L holds f2 . x = downarrow x ) implies f1 = f2 )
assume that
A2: for x being Element of L holds f1 . x = downarrow x and
A3: for x being Element of L holds f2 . x = downarrow x ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_Element_of_L_holds_f1_._x_=_f2_._x
let x be Element of L; ::_thesis: f1 . x = f2 . x
thus f1 . x = downarrow x by A2
.= f2 . x by A3 ; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines IdsMap YELLOW_2:def_4_:_
for L being non empty Poset
for b2 being Function of L,(InclPoset (Ids L)) holds
( b2 = IdsMap L iff for x being Element of L holds b2 . x = downarrow x );
theorem Th52: :: YELLOW_2:52
for L being non empty Poset holds IdsMap L is monotone
proof
let L be non empty Poset; ::_thesis: IdsMap L is monotone
let x1, x2 be Element of L; :: according to ORDERS_3:def_5 ::_thesis: ( not x1 <= x2 or for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (IdsMap L) . x1 or not b2 = (IdsMap L) . x2 or b1 <= b2 ) )
assume x1 <= x2 ; ::_thesis: for b1, b2 being Element of the carrier of (InclPoset (Ids L)) holds
( not b1 = (IdsMap L) . x1 or not b2 = (IdsMap L) . x2 or b1 <= b2 )
then downarrow x1 c= downarrow x2 by WAYBEL_0:21;
then (IdsMap L) . x1 c= downarrow x2 by Def4;
then A1: (IdsMap L) . x1 c= (IdsMap L) . x2 by Def4;
let a, b be Element of (InclPoset (Ids L)); ::_thesis: ( not a = (IdsMap L) . x1 or not b = (IdsMap L) . x2 or a <= b )
assume ( a = (IdsMap L) . x1 & b = (IdsMap L) . x2 ) ; ::_thesis: a <= b
hence a <= b by A1, YELLOW_1:3; ::_thesis: verum
end;
registration
let L be non empty Poset;
cluster IdsMap L -> monotone ;
correctness
coherence
IdsMap L is monotone ;
by Th52;
end;
begin
definition
let L be non empty RelStr ;
let F be Relation;
func \\/ (F,L) -> Element of L equals :: YELLOW_2:def 5
"\/" ((rng F),L);
coherence
"\/" ((rng F),L) is Element of L ;
func //\ (F,L) -> Element of L equals :: YELLOW_2:def 6
"/\" ((rng F),L);
coherence
"/\" ((rng F),L) is Element of L ;
end;
:: deftheorem defines \\/ YELLOW_2:def_5_:_
for L being non empty RelStr
for F being Relation holds \\/ (F,L) = "\/" ((rng F),L);
:: deftheorem defines //\ YELLOW_2:def_6_:_
for L being non empty RelStr
for F being Relation holds //\ (F,L) = "/\" ((rng F),L);
notation
let J be set ;
let L be non empty RelStr ;
let F be Function of J, the carrier of L;
synonym Sup F for \\/ (L,J);
synonym Inf F for //\ (L,J);
end;
theorem :: YELLOW_2:53
for L being complete LATTICE
for J being non empty set
for j being Element of J
for F being Function of J, the carrier of L holds
( F . j <= Sup & Inf <= F . j )
proof
let L be complete LATTICE; ::_thesis: for J being non empty set
for j being Element of J
for F being Function of J, the carrier of L holds
( F . j <= Sup & Inf <= F . j )
let J be non empty set ; ::_thesis: for j being Element of J
for F being Function of J, the carrier of L holds
( F . j <= Sup & Inf <= F . j )
let j be Element of J; ::_thesis: for F being Function of J, the carrier of L holds
( F . j <= Sup & Inf <= F . j )
let F be Function of J, the carrier of L; ::_thesis: ( F . j <= Sup & Inf <= F . j )
F . j in rng F by FUNCT_2:4;
hence ( F . j <= Sup & Inf <= F . j ) by Th22; ::_thesis: verum
end;
theorem :: YELLOW_2:54
for L being complete LATTICE
for a being Element of L
for J being non empty set
for F being Function of J, the carrier of L st ( for j being Element of J holds F . j <= a ) holds
Sup <= a
proof
let L be complete LATTICE; ::_thesis: for a being Element of L
for J being non empty set
for F being Function of J, the carrier of L st ( for j being Element of J holds F . j <= a ) holds
Sup <= a
let a be Element of L; ::_thesis: for J being non empty set
for F being Function of J, the carrier of L st ( for j being Element of J holds F . j <= a ) holds
Sup <= a
let J be non empty set ; ::_thesis: for F being Function of J, the carrier of L st ( for j being Element of J holds F . j <= a ) holds
Sup <= a
let F be Function of J, the carrier of L; ::_thesis: ( ( for j being Element of J holds F . j <= a ) implies Sup <= a )
assume A1: for j being Element of J holds F . j <= a ; ::_thesis: Sup <= a
now__::_thesis:_for_c_being_Element_of_L_st_c_in_rng_F_holds_
c_<=_a
let c be Element of L; ::_thesis: ( c in rng F implies c <= a )
assume c in rng F ; ::_thesis: c <= a
then consider j being set such that
A2: j in dom F and
A3: c = F . j by FUNCT_1:def_3;
reconsider j = j as Element of J by A2;
c = F . j by A3;
hence c <= a by A1; ::_thesis: verum
end;
then rng F is_<=_than a by LATTICE3:def_9;
hence Sup <= a by YELLOW_0:32; ::_thesis: verum
end;
theorem :: YELLOW_2:55
for L being complete LATTICE
for a being Element of L
for J being non empty set
for F being Function of J, the carrier of L st ( for j being Element of J holds a <= F . j ) holds
a <= Inf
proof
let L be complete LATTICE; ::_thesis: for a being Element of L
for J being non empty set
for F being Function of J, the carrier of L st ( for j being Element of J holds a <= F . j ) holds
a <= Inf
let a be Element of L; ::_thesis: for J being non empty set
for F being Function of J, the carrier of L st ( for j being Element of J holds a <= F . j ) holds
a <= Inf
let J be non empty set ; ::_thesis: for F being Function of J, the carrier of L st ( for j being Element of J holds a <= F . j ) holds
a <= Inf
let F be Function of J, the carrier of L; ::_thesis: ( ( for j being Element of J holds a <= F . j ) implies a <= Inf )
assume A1: for j being Element of J holds a <= F . j ; ::_thesis: a <= Inf
now__::_thesis:_for_c_being_Element_of_L_st_c_in_rng_F_holds_
a_<=_c
let c be Element of L; ::_thesis: ( c in rng F implies a <= c )
assume c in rng F ; ::_thesis: a <= c
then consider j being set such that
A2: j in dom F and
A3: c = F . j by FUNCT_1:def_3;
reconsider j = j as Element of J by A2;
c = F . j by A3;
hence a <= c by A1; ::_thesis: verum
end;
then a is_<=_than rng F by LATTICE3:def_8;
hence a <= Inf by YELLOW_0:33; ::_thesis: verum
end;