let L be lower-bounded continuous LATTICE; L is meet-continuous
now for D being non empty directed Subset of L
for x being Element of L st x <= sup D holds
x = sup ({x} "/\" D)let D be non
empty directed Subset of
L;
for x being Element of L st x <= sup D holds
x = sup ({x} "/\" D)let x be
Element of
L;
( x <= sup D implies x = sup ({x} "/\" D) )assume A1:
x <= sup D
;
x = sup ({x} "/\" D)A2:
ex_sup_of waybelow x,
L
by YELLOW_0:17;
A3:
ex_sup_of downarrow (sup ({x} "/\" D)),
L
by YELLOW_0:17;
waybelow x c= downarrow (sup ({x} "/\" D))
proof
let q be
object ;
TARSKI:def 3 ( not q in waybelow x or q in downarrow (sup ({x} "/\" D)) )
assume
q in waybelow x
;
q in downarrow (sup ({x} "/\" D))
then
q in { y where y is Element of L : y << x }
by WAYBEL_3:def 3;
then consider q9 being
Element of
L such that A4:
q9 = q
and A5:
q9 << x
;
A6:
q9 <= x
by A5, WAYBEL_3:1;
consider d being
Element of
L such that A7:
d in D
and A8:
q9 <= d
by A1, A5, WAYBEL_3:def 1;
x in {x}
by TARSKI:def 1;
then
x "/\" d in { (a "/\" b) where a, b is Element of L : ( a in {x} & b in D ) }
by A7;
then A9:
x "/\" d in {x} "/\" D
by YELLOW_4:def 4;
ex_inf_of {x,d},
L
by YELLOW_0:17;
then A10:
q9 <= x "/\" d
by A6, A8, YELLOW_0:19;
sup ({x} "/\" D) is_>=_than {x} "/\" D
by YELLOW_0:32;
then
x "/\" d <= sup ({x} "/\" D)
by A9;
then
q9 <= sup ({x} "/\" D)
by A10, ORDERS_2:3;
hence
q in downarrow (sup ({x} "/\" D))
by A4, WAYBEL_0:17;
verum
end; then
sup (waybelow x) <= sup (downarrow (sup ({x} "/\" D)))
by A2, A3, YELLOW_0:34;
then
sup (waybelow x) <= sup ({x} "/\" D)
by WAYBEL_0:34;
then A11:
x <= sup ({x} "/\" D)
by WAYBEL_3:def 5;
sup ({x} "/\" D) <= x
by Lm11;
hence
x = sup ({x} "/\" D)
by A11, ORDERS_2:2;
verum end;
then
for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D)
;
hence
L is meet-continuous
by WAYBEL_2:52; verum