let L be lower-bounded continuous LATTICE; 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; ( x << y implies ex F being Open Filter of L st
( y in F & F c= wayabove x ) )
defpred S1[ Element of L, Element of L] means $2 << $1;
assume A1:
x << y
; ex F being Open Filter of L st
( y in F & F c= wayabove x )
then reconsider W = wayabove x as non empty Subset of L by WAYBEL_3:8;
A2:
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(A2);
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;
A6:
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
reconsider y1 =
y as
Element of
W by A1, WAYBEL_3:8;
let X,
Y be
Subset of
L;
( X in V & Y in V implies ex Z being Subset of L st
( Z in V & X \/ Y c= Z ) )
assume that A7:
X in V
and A8:
Y in V
;
ex Z being Subset of L st
( Z in V & X \/ Y c= Z )
consider z2 being
Element of
L such that A9:
Y = uparrow z2
and A10:
ex
n being
Element of
NAT st
z2 = (iter (f,n)) . y
by A8;
consider n2 being
Element of
NAT such that A11:
z2 = (iter (f,n2)) . y
by A10;
consider z1 being
Element of
L such that A12:
X = uparrow z1
and A13:
ex
n being
Element of
NAT st
z1 = (iter (f,n)) . y
by A7;
set z =
z1 "/\" z2;
consider n1 being
Element of
NAT such that A14:
z1 = (iter (f,n1)) . y
by A13;
A15:
for
n,
k being
Element of
NAT holds
(iter (f,(n + k))) . y1 <= (iter (f,n)) . y1
proof
let n be
Element of
NAT ;
for k being Element of NAT holds (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1
defpred S2[
Nat]
means (iter (f,(n + (In ($1,NAT))))) . y1 <= (iter (f,n)) . y1;
A16:
for
k being
Nat st
S2[
k] holds
S2[
k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume A17:
(iter (f,(n + (In (k,NAT))))) . y1 <= (iter (f,n)) . y1
;
S2[k + 1]
set nk =
(iter (f,(n + (In (k,NAT))))) . y1;
(iter (f,(n + (In (k,NAT))))) . y1 in W
by FUNCT_2:5;
then consider znk being
Element of
L such that
znk in W
and A18:
znk = f . ((iter (f,(n + (In (k,NAT))))) . y1)
and A19:
znk << (iter (f,(n + (In (k,NAT))))) . y1
by A5;
dom (iter (f,(n + (In (k,NAT))))) = W
by FUNCT_2:def 1;
then A20:
znk =
(f * (iter (f,(n + k)))) . y1
by A18, FUNCT_1:13
.=
(iter (f,((n + k) + 1))) . y1
by FUNCT_7:71
.=
(iter (f,(n + (k + 1)))) . y1
;
znk <= (iter (f,(n + (In (k,NAT))))) . y1
by A19, WAYBEL_3:1;
hence
S2[
k + 1]
by A17, A20, ORDERS_2:3;
verum
end;
A21:
S2[
0 ]
;
let k be
Element of
NAT ;
(iter (f,(n + k))) . y1 <= (iter (f,n)) . y1
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(A21, A16);
then
S2[
k]
;
hence
(iter (f,(n + k))) . y1 <= (iter (f,n)) . y1
;
verum
end;
z1 "/\" z2 <= z2
by YELLOW_0:23;
then A25:
uparrow z2 c= uparrow (z1 "/\" z2)
by WAYBEL_0:22;
z1 "/\" z2 <= z1
by YELLOW_0:23;
then
uparrow z1 c= uparrow (z1 "/\" z2)
by WAYBEL_0:22;
hence
ex
Z being
Subset of
L st
(
Z in V &
X \/ Y c= Z )
by A12, A9, A22, A25, XBOOLE_1:8;
verum
end;
A26:
for X being Subset of L st X in V holds
X is filtered
y <= y
;
then A27:
y in uparrow y
by WAYBEL_0:18;
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;
A31:
y in wayabove x
by A1, WAYBEL_3:8;
A32:
now for u1 being Element of L st u1 in F holds
ex g being Element of L st
( g in F & g << u1 )let u1 be
Element of
L;
( u1 in F implies ex g being Element of L st
( g in F & g << u1 ) )assume
u1 in F
;
ex g being Element of L st
( g in F & g << u1 )then consider Y being
set such that A33:
u1 in Y
and A34:
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 A35:
Y = uparrow z
and A36:
ex
n being
Element of
NAT st
z = (iter (f,n)) . y
by A34;
consider n being
Element of
NAT such that A37:
z = (iter (f,n)) . y
by A36;
z in W
by A31, A37, FUNCT_2:5;
then consider z9 being
Element of
L such that
z9 in W
and A38:
z9 = f . z
and A39:
z9 << z
by A5;
z9 <= z9
;
then A40:
z9 in uparrow z9
by WAYBEL_0:18;
dom (iter (f,n)) = W
by FUNCT_2:def 1;
then z9 =
(f * (iter (f,n))) . y
by A31, A37, A38, FUNCT_1:13
.=
(iter (f,(n + 1))) . y
by FUNCT_7:71
;
then
uparrow z9 in { (uparrow p) where p is Element of L : ex n being Element of NAT st p = (iter (f,n)) . y }
;
then A41:
z9 in F
by A40, TARSKI:def 4;
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 A33, A35, WAYBEL_0:15;
then consider a being
Element of
L such that A42:
a = u1
and A43:
ex
b being
Element of
L st
(
a >= b &
b in z1 )
;
consider b being
Element of
L such that A44:
a >= b
and A45:
b in z1
by A43;
b = z
by A45, TARSKI:def 1;
hence
ex
g being
Element of
L st
(
g in F &
g << u1 )
by A42, A44, A39, A41, WAYBEL_3:2;
verum end;
dom f = W
by FUNCT_2:def 1;
then A46:
y in field f
by A31, XBOOLE_0:def 3;
(iter (f,0)) . y =
(id (field f)) . y
by FUNCT_7:68
.=
y
by A46, FUNCT_1:18
;
then A47:
uparrow y in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y }
;
for X being Subset of L st X in V holds
X is upper
then reconsider F = F as Open Filter of L by A27, A47, A26, A6, A32, Def1, TARSKI:def 4, WAYBEL_0:28, WAYBEL_0:47;
take
F
; ( y in F & F c= wayabove x )
hence
( y in F & F c= wayabove x )
by A27, A47, TARSKI:def 4; verum