let L be LATTICE; for l being Element of L holds
( l is prime iff for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) )
let l be Element of L; ( l is prime iff for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) )
thus
( l is prime implies for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) )
( ( for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) ) implies l is prime )proof
assume A1:
l is
prime
;
for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving )
let x be
set ;
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving )let f be
Function of
L,
(BoolePoset {x});
( ( for p being Element of L holds
( f . p = {} iff p <= l ) ) implies ( f is meet-preserving & f is join-preserving ) )
assume A2:
for
p being
Element of
L holds
(
f . p = {} iff
p <= l )
;
( f is meet-preserving & f is join-preserving )
A3: the
carrier of
(BoolePoset {x}) =
the
carrier of
(InclPoset (bool {x}))
by YELLOW_1:4
.=
bool {x}
by YELLOW_1:1
.=
{{},{x}}
by ZFMISC_1:24
;
A4:
dom f = the
carrier of
L
by FUNCT_2:def 1;
for
z,
y being
Element of
L holds
f preserves_inf_of {z,y}
proof
let z,
y be
Element of
L;
f preserves_inf_of {z,y}
A5:
f .: {z,y} = {(f . z),(f . y)}
by A4, FUNCT_1:60;
then A6:
(
ex_inf_of {z,y},
L implies
ex_inf_of f .: {z,y},
BoolePoset {x} )
by YELLOW_0:21;
inf (f .: {z,y}) =
(f . z) "/\" (f . y)
by A5, YELLOW_0:40
.=
f . (inf {z,y})
by A7, YELLOW_0:40
;
hence
f preserves_inf_of {z,y}
by A6;
verum
end;
hence
f is
meet-preserving
;
f is join-preserving
for
z,
y being
Element of
L holds
f preserves_sup_of {z,y}
proof
let z,
y be
Element of
L;
f preserves_sup_of {z,y}
A16:
f .: {z,y} = {(f . z),(f . y)}
by A4, FUNCT_1:60;
then A17:
(
ex_sup_of {z,y},
L implies
ex_sup_of f .: {z,y},
BoolePoset {x} )
by YELLOW_0:20;
sup (f .: {z,y}) =
(f . z) "\/" (f . y)
by A16, YELLOW_0:41
.=
f . (sup {z,y})
by A18, YELLOW_0:41
;
hence
f preserves_sup_of {z,y}
by A17;
verum
end;
hence
f is
join-preserving
;
verum
end;
thus
( ( for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) ) implies l is prime )
verumproof
defpred S1[
Element of
L,
set ]
means ( $1
<= l iff $2
= {} );
assume A27:
for
x being
set for
f being
Function of
L,
(BoolePoset {x}) st ( for
p being
Element of
L holds
(
f . p = {} iff
p <= l ) ) holds
(
f is
meet-preserving &
f is
join-preserving )
;
l is prime
let z,
y be
Element of
L;
WAYBEL_6:def 6 ( not z "/\" y <= l or z <= l or y <= l )
A28: the
carrier of
(BoolePoset {{}}) =
the
carrier of
(InclPoset (bool {{}}))
by YELLOW_1:4
.=
bool {{}}
by YELLOW_1:1
.=
{{},{{}}}
by ZFMISC_1:24
;
A29:
for
a being
Element of
L ex
b being
Element of
(BoolePoset {{}}) st
S1[
a,
b]
consider f being
Function of
L,
(BoolePoset {{}}) such that A32:
for
p being
Element of
L holds
S1[
p,
f . p]
from FUNCT_2:sch 3(A29);
f is
meet-preserving
by A27, A32;
then A33:
(
ex_inf_of {z,y},
L &
f preserves_inf_of {z,y} )
by YELLOW_0:21;
dom f = the
carrier of
L
by FUNCT_2:def 1;
then A34:
f .: {z,y} = {(f . z),(f . y)}
by FUNCT_1:60;
assume
z "/\" y <= l
;
( z <= l or y <= l )
then A35:
{} =
f . (z "/\" y)
by A32
.=
f . (inf {z,y})
by YELLOW_0:40
.=
inf {(f . z),(f . y)}
by A34, A33
.=
(f . z) "/\" (f . y)
by YELLOW_0:40
.=
(f . z) /\ (f . y)
by YELLOW_1:17
;
hence
(
z <= l or
y <= l )
by A32;
verum
end;