let L be lower-bounded continuous LATTICE; :: thesis: for x, y being Element of L st x << y holds
ex F being Open Filter of L st
( y in F & F c= wayabove x )
let x, y be Element of L; :: thesis: ( x << y implies ex F being Open Filter of L st
( y in F & F c= wayabove x ) )
assume A1:
x << y
; :: thesis: ex F being Open Filter of L st
( y in F & F c= wayabove x )
then A2:
y in wayabove x
by WAYBEL_3:8;
reconsider W = wayabove x as non empty Subset of L by A1, WAYBEL_3:8;
defpred S1[ Element of L, Element of L] means $2 << $1;
A3:
for z being Element of L st z in W holds
ex z1 being Element of L st
( z1 in W & S1[z,z1] )
consider f being Function of W,W such that
A5:
for z being Element of L st z in W holds
ex z1 being Element of L st
( z1 in W & z1 = f . z & S1[z,z1] )
from WAYBEL_6:sch 1(A3);
dom f = W
by FUNCT_2:def 1;
then A6:
y in (dom f) \/ (rng f)
by A2, XBOOLE_0:def 3;
set F = union { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter f,n) . y } ;
then reconsider F = union { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter f,n) . y } as Subset of L by TARSKI:def 3;
y <= y
;
then A11:
y in uparrow y
by WAYBEL_0:18;
(iter f,0 ) . y =
(id ((dom f) \/ (rng f))) . y
by FUNCT_7:70
.=
y
by A6, FUNCT_1:35
;
then A12:
uparrow y in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter f,n) . y }
;
set V = { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter f,n) . y } ;
then reconsider V = { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter f,n) . y } as Subset-Family of L by TARSKI:def 3;
A14:
for X being Subset of L st X in V holds
X is upper
A16:
for X being Subset of L st X in V holds
X is filtered
A18:
for X, Y being Subset of L st X in V & Y in V holds
ex Z being Subset of L st
( Z in V & X \/ Y c= Z )
proof
let X,
Y be
Subset of
L;
:: thesis: ( X in V & Y in V implies ex Z being Subset of L st
( Z in V & X \/ Y c= Z ) )
assume A19:
(
X in V &
Y in V )
;
:: thesis: ex Z being Subset of L st
( Z in V & X \/ Y c= Z )
then consider z1 being
Element of
L such that A20:
X = uparrow z1
and A21:
ex
n being
Element of
NAT st
z1 = (iter f,n) . y
;
consider n1 being
Element of
NAT such that A22:
z1 = (iter f,n1) . y
by A21;
consider z2 being
Element of
L such that A23:
Y = uparrow z2
and A24:
ex
n being
Element of
NAT st
z2 = (iter f,n) . y
by A19;
consider n2 being
Element of
NAT such that A25:
z2 = (iter f,n2) . y
by A24;
reconsider y1 =
y as
Element of
W by A1, WAYBEL_3:8;
A26:
for
n,
k being
Element of
NAT holds
(iter f,(n + k)) . y1 <= (iter f,n) . y1
proof
let n be
Element of
NAT ;
:: thesis: for k being Element of NAT holds (iter f,(n + k)) . y1 <= (iter f,n) . y1
defpred S2[
Element of
NAT ]
means (iter f,(n + $1)) . y1 <= (iter f,n) . y1;
A27:
S2[
0 ]
;
A28:
for
k being
Element of
NAT st
S2[
k] holds
S2[
k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S2[k] implies S2[k + 1] )
assume A29:
(iter f,(n + k)) . y1 <= (iter f,n) . y1
;
:: thesis: S2[k + 1]
set nk =
(iter f,(n + k)) . y1;
(iter f,(n + k)) . y1 in W
by FUNCT_2:7;
then consider znk being
Element of
L such that A30:
(
znk in W &
znk = f . ((iter f,(n + k)) . y1) &
znk << (iter f,(n + k)) . y1 )
by A5;
dom (iter f,(n + k)) = W
by FUNCT_2:def 1;
then A31:
znk =
(f * (iter f,(n + k))) . y1
by A30, FUNCT_1:23
.=
(iter f,((n + k) + 1)) . y1
by FUNCT_7:73
.=
(iter f,(n + (k + 1))) . y1
;
znk <= (iter f,(n + k)) . y1
by A30, WAYBEL_3:1;
hence
S2[
k + 1]
by A29, A31, ORDERS_2:26;
:: thesis: verum
end;
for
k being
Element of
NAT holds
S2[
k]
from NAT_1:sch 1(A27, A28);
hence
for
k being
Element of
NAT holds
(iter f,(n + k)) . y1 <= (iter f,n) . y1
;
:: thesis: verum
end;
set z =
z1 "/\" z2;
(
z1 "/\" z2 <= z1 &
z1 "/\" z2 <= z2 )
by YELLOW_0:23;
then
(
uparrow z1 c= uparrow (z1 "/\" z2) &
uparrow z2 c= uparrow (z1 "/\" z2) )
by WAYBEL_0:22;
hence
ex
Z being
Subset of
L st
(
Z in V &
X \/ Y c= Z )
by A20, A23, A32, XBOOLE_1:8;
:: thesis: verum
end;
now let u1 be
Element of
L;
:: thesis: ( u1 in F implies ex g being Element of L st
( g in F & g << u1 ) )assume
u1 in F
;
:: thesis: ex g being Element of L st
( g in F & g << u1 )then consider Y being
set such that A35:
u1 in Y
and A36:
Y in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter f,n) . y }
by TARSKI:def 4;
consider z being
Element of
L such that A37:
Y = uparrow z
and A38:
ex
n being
Element of
NAT st
z = (iter f,n) . y
by A36;
consider n being
Element of
NAT such that A39:
z = (iter f,n) . y
by A38;
reconsider z1 =
{z} as
Subset of
L ;
u1 in { a where a is Element of L : ex b being Element of L st
( a >= b & b in z1 ) }
by A35, A37, WAYBEL_0:15;
then consider a being
Element of
L such that A40:
a = u1
and A41:
ex
b being
Element of
L st
(
a >= b &
b in z1 )
;
consider b being
Element of
L such that A42:
(
a >= b &
b in z1 )
by A41;
A43:
b = z
by A42, TARSKI:def 1;
z in W
by A2, A39, FUNCT_2:7;
then consider z' being
Element of
L such that A44:
(
z' in W &
z' = f . z &
z' << z )
by A5;
z' <= z'
;
then A45:
z' in uparrow z'
by WAYBEL_0:18;
dom (iter f,n) = W
by FUNCT_2:def 1;
then z' =
(f * (iter f,n)) . y
by A2, A39, A44, FUNCT_1:23
.=
(iter f,(n + 1)) . y
by FUNCT_7:73
;
then
uparrow z' in { (uparrow p) where p is Element of L : ex n being Element of NAT st p = (iter f,n) . y }
;
then
z' in F
by A45, TARSKI:def 4;
hence
ex
g being
Element of
L st
(
g in F &
g << u1 )
by A40, A42, A43, A44, WAYBEL_3:2;
:: thesis: verum end;
then reconsider F = F as Open Filter of L by A11, A12, A14, A16, A18, Def1, TARSKI:def 4, WAYBEL_0:28, WAYBEL_0:47;
take
F
; :: thesis: ( y in F & F c= wayabove x )
hence
( y in F & F c= wayabove x )
by A11, A12, TARSKI:def 3, TARSKI:def 4; :: thesis: verum