let f be Function; ( dom f is subset-closed implies ( f is U-continuous iff ( dom f is d.union-closed & 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 ) ) ) ) )
assume A1:
dom f is subset-closed
; ( f is U-continuous iff ( dom f is d.union-closed & 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 ) ) ) )
hereby ( dom f is d.union-closed & 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 ) ) implies f is U-continuous )
assume A2:
f is
U-continuous
;
( dom f is d.union-closed & f is c=-monotone & ( for a, y being set st a in dom f & y in f . a holds
ex bb being set st
( bb is finite & bb c= a & y in f . bb ) ) )hence
(
dom f is
d.union-closed &
f is
c=-monotone )
;
for a, y being set st a in dom f & y in f . a holds
ex bb being set st
( bb is finite & bb c= a & y in f . bb )reconsider C =
dom f as
subset-closed d.union-closed set by A1, A2;
let a,
y be
set ;
( a in dom f & y in f . a implies ex bb being set st
( bb is finite & bb c= a & y in f . bb ) )assume that A3:
a in dom f
and A4:
y in f . a
;
ex bb being set st
( bb is finite & bb c= a & y in f . bb )reconsider A =
{ b where b is Subset of a : b is finite } as
set ;
A5:
A is
c=directed
A7:
union A = a
A10:
A c= C
then
union A in C
by A5, Def6;
then
f . (union A) = union (f .: A)
by A2, A5, A10, Def10;
then consider B being
set such that A11:
y in B
and A12:
B in f .: A
by A4, A7, TARSKI:def 4;
consider b being
object such that
b in dom f
and A13:
b in A
and A14:
B = f . b
by A12, FUNCT_1:def 6;
reconsider bb =
b as
set by TARSKI:1;
take bb =
bb;
( bb is finite & bb c= a & y in f . bb )
ex
c being
Subset of
a st
(
b = c &
c is
finite )
by A13;
hence
(
bb is
finite &
bb c= a &
y in f . bb )
by A11, A14;
verum
end;
assume
dom f is d.union-closed
; ( not f is c=-monotone or ex a, y being set st
( a in dom f & y in f . a & ( for b being set holds
( not b is finite or not b c= a or not y in f . b ) ) ) or f is U-continuous )
then reconsider C = dom f as d.union-closed set ;
assume that
A15:
for a, b being set st a in dom f & b in dom f & a c= b holds
f . a c= f . b
and
A16:
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 )
; COHSP_1:def 11 f is U-continuous
C is d.union-closed
;
hence
dom f is d.union-closed
; COHSP_1:def 13 f is d.union-distributive
thus
f is d.union-distributive
verumproof
let A be
Subset of
(dom f);
COHSP_1:def 10 ( A is c=directed & union A in dom f implies f . (union A) = union (f .: A) )
assume that A17:
A is
c=directed
and A18:
union A in dom f
;
f . (union A) = union (f .: A)
reconsider A9 =
A as
Subset of
C ;
thus
f . (union A) c= union (f .: A)
XBOOLE_0:def 10 union (f .: A) c= f . (union A)proof
let x be
object ;
TARSKI:def 3 ( not x in f . (union A) or x in union (f .: A) )
assume
x in f . (union A)
;
x in union (f .: A)
then consider b being
set such that A19:
(
b is
finite &
b c= union A9 )
and A20:
x in f . b
by A16, A18;
consider c being
set such that A21:
c in A
and A22:
b c= c
by A17, A19, Th13;
b in C
by A1, A21, A22;
then A23:
f . b c= f . c
by A15, A21, A22;
f . c in f .: A
by A21, FUNCT_1:def 6;
hence
x in union (f .: A)
by A20, A23, TARSKI:def 4;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in union (f .: A) or x in f . (union A) )
assume
x in union (f .: A)
;
x in f . (union A)
then consider B being
set such that A24:
x in B
and A25:
B in f .: A
by TARSKI:def 4;
ex
b being
object st
(
b in dom f &
b in A &
B = f . b )
by A25, FUNCT_1:def 6;
then
B c= f . (union A9)
by A15, A18, ZFMISC_1:74;
hence
x in f . (union A)
by A24;
verum
end;