let f be Function; :: thesis: ( dom f is subset-closed & dom f is d.union-closed implies ( f is U-stable iff ( f is c=-monotone & ( for a, y being set st a in dom f & y in f . a holds
ex b being set st
( b is finite & b c= a & y in f . b & ( for c being set st c c= a & y in f . c holds
b c= c ) ) ) ) ) )
assume A1: ( dom f is subset-closed & dom f is d.union-closed ) ; :: thesis: ( f is U-stable iff ( f is c=-monotone & ( for a, y being set st a in dom f & y in f . a holds
ex b being set st
( b is finite & b c= a & y in f . b & ( for c being set st c c= a & y in f . c holds
b c= c ) ) ) ) )
reconsider C = dom f as subset-closed d.union-closed set by A1;
hereby :: thesis: ( f is c=-monotone & ( for a, y being set st a in dom f & y in f . a holds
ex b being set st
( b is finite & b c= a & y in f . b & ( for c being set st c c= a & y in f . c holds
b c= c ) ) ) implies f is U-stable )
assume f is U-stable ; :: thesis: ( f is c=-monotone & ( for a, y being set st a in dom f & y in f . a holds
ex c being set st
( c is finite & c c= a & y in f . c & ( for d being set st d c= a & y in f . d holds
c c= d ) ) ) )
then reconsider f9 = f as U-stable Function ;
dom f9 is multiplicative ;
hence f is c=-monotone ; :: thesis: for a, y being set st a in dom f & y in f . a holds
ex c being set st
( c is finite & c c= a & y in f . c & ( for d being set st d c= a & y in f . d holds
c c= d ) )
defpred S1[ set , set ] means $1 c= $2;
let a, y be set ; :: thesis: ( a in dom f & y in f . a implies ex c being set st
( c is finite & c c= a & y in f . c & ( for d being set st d c= a & y in f . d holds
c c= d ) ) )
set C = dom f9;
assume that
A2: a in dom f and
A3: y in f . a ; :: thesis: ex c being set st
( c is finite & c c= a & y in f . c & ( for d being set st d c= a & y in f . d holds
c c= d ) )
consider b being set such that
A4: b is finite and
A5: b c= a and
A6: y in f9 . b by A1, A2, A3, Th21;
b c= b ;
then b in { c where c is Subset of b : y in f . c } by A6;
then reconsider A = { c where c is Subset of b : y in f . c } as non empty set ;
A7: ( bool b is finite & A c= bool b )
proof
thus bool b is finite by A4; :: thesis: A c= bool b
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in bool b )
assume x in A ; :: thesis: x in bool b
then ex c being Subset of b st
( x = c & y in f . c ) ;
hence x in bool b ; :: thesis: verum
end;
A8: for x, y, z being set st S1[x,y] & S1[y,z] holds
S1[x,z] by XBOOLE_1:1;
A9: for x, y being set st S1[x,y] & S1[y,x] holds
x = y ;
reconsider A = A as non empty finite set by A7;
A10: A <> {} ;
consider c being set such that
A11: ( c in A & ( for y being set st y in A & y <> c holds
not S1[y,c] ) ) from CARD_2:sch 3(A10, A9, A8);
 ex d being Subset of b st
( c = d & y in f . d ) by A11;
then reconsider c9 = c as Subset of b ;
reconsider c9 = c9 as finite Subset of b by A4;
take c = c; :: thesis: ( c is finite & c c= a & y in f . c & ( for d being set st d c= a & y in f . d holds
c c= d ) )
A12: ex d being Subset of b st
( c = d & y in f . d ) by A11;
hence A13: ( c is finite & c c= a & y in f . c ) by A4, A5; :: thesis: for d being set st d c= a & y in f . d holds
c c= d
then A14: c9 in dom f9 by A1, A2;
let d be set ; :: thesis: ( d c= a & y in f . d implies c c= d )
assume that
A15: d c= a and
A16: y in f . d ; :: thesis: c c= d
A17: d in dom f9 by A1, A2, A15;
c \/ d c= a by A13, A15, XBOOLE_1:8;
then A18: c \/ d in dom f by A1, A2;
A19: c /\ d c= c9 by XBOOLE_1:17;
then c /\ d in dom f by A1, A14;
then dom f includes_lattice_of c,d by A14, A17, A18, Th16;
then f . (c /\ d) = (f . c) /\ (f . d) by A14, Def12;
then A20: y in f . (c /\ d) by A12, A16, XBOOLE_0:def 4;
c /\ d is finite Subset of b by A19, XBOOLE_1:1;
then ( c /\ d c= d & c /\ d in A ) by A20, XBOOLE_1:17;
hence c c= d by A11, XBOOLE_1:17; :: thesis: verum
end;
assume that
A21: f is c=-monotone and
A22: for a, y being set st a in dom f & y in f . a holds
ex b being set st
( b is finite & b c= a & y in f . b & ( for c being set st c c= a & y in f . c holds
b c= c ) ) ; :: thesis: f is U-stable
C is subset-closed set ;
hence dom f is multiplicative ; :: according to COHSP_1:def 14 :: thesis: ( f is U-continuous & f is cap-distributive )
now :: thesis: for a, y being set st a in dom f & y in f . a holds
ex b being set st
( b is finite & b c= a & y in f . b )
let a, y be set ; :: thesis: ( a in dom f & y in f . a implies ex b being set st
( b is finite & b c= a & y in f . b ) )
assume ( a in dom f & y in f . a ) ; :: thesis: ex b being set st
( b is finite & b c= a & y in f . b )
then ex b being set st
( b is finite & b c= a & y in f . b & ( for c being set st c c= a & y in f . c holds
b c= c ) ) by A22;
hence ex b being set st
( b is finite & b c= a & y in f . b ) ; :: thesis: verum
end;
hence f is U-continuous by A1, A21, Th21; :: thesis: f is cap-distributive
thus f is cap-distributive :: thesis: verum
proof
let a, b be set ; :: according to COHSP_1:def 12 :: thesis: ( dom f includes_lattice_of a,b implies f . (a /\ b) = (f . a) /\ (f . b) )
A23: a /\ b c= b by XBOOLE_1:17;
assume A24: dom f includes_lattice_of a,b ; :: thesis: f . (a /\ b) = (f . a) /\ (f . b)
then A25: a /\ b in dom f by Th16;
b in dom f by A24, Th16;
then A26: f . (a /\ b) c= f . b by A21, A25, A23;
A27: a in dom f by A24, Th16;
a /\ b c= a by XBOOLE_1:17;
then f . (a /\ b) c= f . a by A21, A27, A25;
hence f . (a /\ b) c= (f . a) /\ (f . b) by A26, XBOOLE_1:19; :: according to XBOOLE_0:def 10 :: thesis: (f . a) /\ (f . b) c= f . (a /\ b)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (f . a) /\ (f . b) or x in f . (a /\ b) )
assume A28: x in (f . a) /\ (f . b) ; :: thesis: x in f . (a /\ b)
then A29: x in f . a by XBOOLE_0:def 4;
A30: a \/ b in dom f by A24, Th16;
a c= a \/ b by XBOOLE_1:7;
then f . a c= f . (a \/ b) by A21, A27, A30;
then consider c being set such that
c is finite and
c c= a \/ b and
A31: x in f . c and
A32: for d being set st d c= a \/ b & x in f . d holds
c c= d by A22, A30, A29;
A33: c c= a by A29, A32, XBOOLE_1:7;
x in f . b by A28, XBOOLE_0:def 4;
then c c= b by A32, XBOOLE_1:7;
then A34: c c= a /\ b by A33, XBOOLE_1:19;
C = dom f ;
then c in dom f by A27, A33, CLASSES1:def 1;
then f . c c= f . (a /\ b) by A21, A25, A34;
hence x in f . (a /\ b) by A31; :: thesis: verum
end;