let L be complete Lattice; :: thesis: for D being Subset of L holds
( D is infimum-dense iff D % is order-generating )
let D be Subset of L; :: thesis: ( D is infimum-dense iff D % is order-generating )
A1: now :: thesis: ( D % is order-generating implies D is infimum-dense )
assume A2: D % is order-generating ; :: thesis: D is infimum-dense
for a being Element of L ex D9 being Subset of D st a = "/\" (D9,L)
proof
let a be Element of L; :: thesis: ex D9 being Subset of D st a = "/\" (D9,L)
consider Y being Subset of (D %) such that
A3: a % = "/\" (Y,(LattPOSet L)) by A2, WAYBEL_6:15;
A4: for x being object st x in Y holds
x in the carrier of (LattPOSet L)
proof
let x be object ; :: thesis: ( x in Y implies x in the carrier of (LattPOSet L) )
assume x in Y ; :: thesis: x in the carrier of (LattPOSet L)
then x in D % ;
hence x in the carrier of (LattPOSet L) ; :: thesis: verum
end;
A5: a % is_<=_than Y by A3, YELLOW_0:33;
reconsider Y = Y as Subset of (LattPOSet L) by A4, TARSKI:def 3;
A6: for b being Element of L st b is_less_than % Y holds
b [= a
proof
let b be Element of L; :: thesis: ( b is_less_than % Y implies b [= a )
assume A7: b is_less_than % Y ; :: thesis: b [= a
for u being Element of (LattPOSet L) st u in Y holds
b % <= u
proof
let u be Element of (LattPOSet L); :: thesis: ( u in Y implies b % <= u )
assume u in Y ; :: thesis: b % <= u
then % u in { (% d) where d is Element of (LattPOSet L) : d in Y } ;
then A8: b [= % u by A7, LATTICE3:def 16;
(% u) % = % u by LATTICE3:def 3
.= u by LATTICE3:def 4 ;
hence b % <= u by A8, LATTICE3:7; :: thesis: verum
end;
then b % is_<=_than Y by LATTICE3:def 8;
then b % <= a % by A3, YELLOW_0:33;
hence b [= a by LATTICE3:7; :: thesis: verum
end;
for x being object st x in % Y holds
x in D
proof
let x be object ; :: thesis: ( x in % Y implies x in D )
assume x in % Y ; :: thesis: x in D
then consider x9 being Element of (LattPOSet L) such that
A9: x = % x9 and
A10: x9 in Y ;
x9 in D % by A10;
then consider y being Element of L such that
A11: x9 = y % and
A12: y in D ;
x = y % by A9, A11, LATTICE3:def 4
.= y by LATTICE3:def 3 ;
hence x in D by A12; :: thesis: verum
end;
then A13: % Y is Subset of D by TARSKI:def 3;
for q being Element of L st q in % Y holds
a [= q
proof
let q be Element of L; :: thesis: ( q in % Y implies a [= q )
assume q in % Y ; :: thesis: a [= q
then consider q9 being Element of (LattPOSet L) such that
A14: q = % q9 and
A15: q9 in Y ;
A16: q9 = % q9 by LATTICE3:def 4
.= (% q9) % by LATTICE3:def 3 ;
a % <= q9 by A5, A15, LATTICE3:def 8;
hence a [= q by A14, A16, LATTICE3:7; :: thesis: verum
end;
then a is_less_than % Y by LATTICE3:def 16;
then a = "/\" ((% Y),L) by A6, LATTICE3:34;
hence ex D9 being Subset of D st a = "/\" (D9,L) by A13; :: thesis: verum
end;
hence D is infimum-dense ; :: thesis: verum
end;
now :: thesis: ( D is infimum-dense implies D % is order-generating )
assume A17: D is infimum-dense ; :: thesis: D % is order-generating
for a being Element of (LattPOSet L) ex Y being Subset of (D %) st a = "/\" (Y,(LattPOSet L))
proof
let a be Element of (LattPOSet L); :: thesis: ex Y being Subset of (D %) st a = "/\" (Y,(LattPOSet L))
consider D9 being Subset of D such that
A18: % a = "/\" (D9,L) by A17;
A19: for x being object st x in D9 holds
x in the carrier of L
proof
let x be object ; :: thesis: ( x in D9 implies x in the carrier of L )
assume x in D9 ; :: thesis: x in the carrier of L
then x in D ;
hence x in the carrier of L ; :: thesis: verum
end;
A20: % a is_less_than D9 by A18, LATTICE3:34;
reconsider D9 = D9 as Subset of L by A19, TARSKI:def 3;
A21: for b being Element of (LattPOSet L) st D9 % is_>=_than b holds
b <= a
proof
let b be Element of (LattPOSet L); :: thesis: ( D9 % is_>=_than b implies b <= a )
A22: b = % b by LATTICE3:def 4
.= (% b) % by LATTICE3:def 3 ;
assume A23: D9 % is_>=_than b ; :: thesis: b <= a
for u being Element of L st u in D9 holds
% b [= u
proof
let u be Element of L; :: thesis: ( u in D9 implies % b [= u )
assume u in D9 ; :: thesis: % b [= u
then u % in { (d %) where d is Element of L : d in D9 } ;
then b <= u % by A23, LATTICE3:def 8;
hence % b [= u by A22, LATTICE3:7; :: thesis: verum
end;
then % b is_less_than D9 by LATTICE3:def 16;
then A24: % b [= % a by A18, LATTICE3:34;
a = % a by LATTICE3:def 4
.= (% a) % by LATTICE3:def 3 ;
hence b <= a by A22, A24, LATTICE3:7; :: thesis: verum
end;
for x being object st x in D9 % holds
x in D %
proof
let x be object ; :: thesis: ( x in D9 % implies x in D % )
assume x in D9 % ; :: thesis: x in D %
then ex x9 being Element of L st
( x = x9 % & x9 in D9 ) ;
hence x in D % ; :: thesis: verum
end;
then A25: D9 % is Subset of (D %) by TARSKI:def 3;
for u being Element of (LattPOSet L) st u in D9 % holds
a <= u
proof
let u be Element of (LattPOSet L); :: thesis: ( u in D9 % implies a <= u )
A26: (% a) % = % a by LATTICE3:def 3
.= a by LATTICE3:def 4 ;
assume u in D9 % ; :: thesis: a <= u
then consider u9 being Element of L such that
A27: u = u9 % and
A28: u9 in D9 ;
% a [= u9 by A20, A28, LATTICE3:def 16;
hence a <= u by A27, A26, LATTICE3:7; :: thesis: verum
end;
then D9 % is_>=_than a by LATTICE3:def 8;
then a = "/\" ((D9 %),(LattPOSet L)) by A21, YELLOW_0:33;
hence ex Y being Subset of (D %) st a = "/\" (Y,(LattPOSet L)) by A25; :: thesis: verum
end;
hence D % is order-generating by WAYBEL_6:15; :: thesis: verum
end;
hence ( D is infimum-dense iff D % is order-generating ) by A1; :: thesis: verum