:: FILTER_2 semantic presentation
begin
theorem Th1: :: FILTER_2:1
for D being non empty set
for S being non empty Subset of D
for f being BinOp of D
for g being BinOp of S st g = f || S holds
( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) )
proof
let D be non empty set ; ::_thesis: for S being non empty Subset of D
for f being BinOp of D
for g being BinOp of S st g = f || S holds
( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) )
let S be non empty Subset of D; ::_thesis: for f being BinOp of D
for g being BinOp of S st g = f || S holds
( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) )
let f be BinOp of D; ::_thesis: for g being BinOp of S st g = f || S holds
( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) )
let g be BinOp of S; ::_thesis: ( g = f || S implies ( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) ) )
A1: dom g = [:S,S:] by FUNCT_2:def_1;
assume A2: g = f || S ; ::_thesis: ( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) )
thus ( f is commutative implies g is commutative ) ::_thesis: ( ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) )
proof
assume A3: for a, b being Element of D holds f . (a,b) = f . (b,a) ; :: according to BINOP_1:def_2 ::_thesis: g is commutative
let a, b be Element of S; :: according to BINOP_1:def_2 ::_thesis: g . (a,b) = g . (b,a)
reconsider a9 = a, b9 = b as Element of S ;
reconsider a9 = a9, b9 = b9 as Element of D ;
thus g . (a,b) = f . [a,b] by A2, A1, FUNCT_1:47
.= f . (a9,b9)
.= f . (b9,a9) by A3
.= g . [b,a] by A2, A1, FUNCT_1:47
.= g . (b,a) ; ::_thesis: verum
end;
thus ( f is idempotent implies g is idempotent ) ::_thesis: ( f is associative implies g is associative )
proof
assume A4: for a being Element of D holds f . (a,a) = a ; :: according to BINOP_1:def_4 ::_thesis: g is idempotent
let a be Element of S; :: according to BINOP_1:def_4 ::_thesis: g . (a,a) = a
thus g . (a,a) = f . [a,a] by A2, A1, FUNCT_1:47
.= f . (a,a)
.= a by A4 ; ::_thesis: verum
end;
assume A5: for a, b, c being Element of D holds f . ((f . (a,b)),c) = f . (a,(f . (b,c))) ; :: according to BINOP_1:def_3 ::_thesis: g is associative
let a, b, c be Element of S; :: according to BINOP_1:def_3 ::_thesis: g . (a,(g . (b,c))) = g . ((g . (a,b)),c)
reconsider a9 = a, b9 = b, c9 = c as Element of S ;
reconsider a9 = a9, b9 = b9, c9 = c9 as Element of D ;
thus g . ((g . (a,b)),c) = f . [(g . (a,b)),c] by A2, A1, FUNCT_1:47
.= f . [(f . [a,b]),c] by A2, A1, FUNCT_1:47
.= f . ((f . (a,b)),c)
.= f . (a9,(f . (b9,c9))) by A5
.= f . (a,(g . [b,c])) by A2, A1, FUNCT_1:47
.= f . [a,(g . (b,c))]
.= g . (a,(g . (b,c))) by A2, A1, FUNCT_1:47 ; ::_thesis: verum
end;
theorem :: FILTER_2:2
for D being non empty set
for S being non empty Subset of D
for f being BinOp of D
for g being BinOp of S
for d being Element of D
for d9 being Element of S st g = f || S & d9 = d holds
( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
proof
let D be non empty set ; ::_thesis: for S being non empty Subset of D
for f being BinOp of D
for g being BinOp of S
for d being Element of D
for d9 being Element of S st g = f || S & d9 = d holds
( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
let S be non empty Subset of D; ::_thesis: for f being BinOp of D
for g being BinOp of S
for d being Element of D
for d9 being Element of S st g = f || S & d9 = d holds
( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
let f be BinOp of D; ::_thesis: for g being BinOp of S
for d being Element of D
for d9 being Element of S st g = f || S & d9 = d holds
( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
let g be BinOp of S; ::_thesis: for d being Element of D
for d9 being Element of S st g = f || S & d9 = d holds
( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
let d be Element of D; ::_thesis: for d9 being Element of S st g = f || S & d9 = d holds
( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
let d9 be Element of S; ::_thesis: ( g = f || S & d9 = d implies ( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) ) )
assume that
A1: g = f || S and
A2: d9 = d ; ::_thesis: ( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
A3: dom g = [:S,S:] by FUNCT_2:def_1;
thus ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) ::_thesis: ( ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )
proof
assume A4: for a being Element of D holds f . (d,a) = a ; :: according to BINOP_1:def_16 ::_thesis: d9 is_a_left_unity_wrt g
let a be Element of S; :: according to BINOP_1:def_16 ::_thesis: g . (d9,a) = a
thus g . (d9,a) = f . [d9,a] by A1, A3, FUNCT_1:47
.= f . (d,a) by A2
.= a by A4 ; ::_thesis: verum
end;
thus ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) ::_thesis: ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g )
proof
assume A5: for a being Element of D holds f . (a,d) = a ; :: according to BINOP_1:def_17 ::_thesis: d9 is_a_right_unity_wrt g
let a be Element of S; :: according to BINOP_1:def_17 ::_thesis: g . (a,d9) = a
thus g . (a,d9) = f . [a,d9] by A1, A3, FUNCT_1:47
.= f . (a,d) by A2
.= a by A5 ; ::_thesis: verum
end;
assume A6: d is_a_unity_wrt f ; ::_thesis: d9 is_a_unity_wrt g
now__::_thesis:_for_s_being_Element_of_S_holds_
(_g_._(d9,s)_=_s_&_g_._(s,d9)_=_s_)
let s be Element of S; ::_thesis: ( g . (d9,s) = s & g . (s,d9) = s )
reconsider s9 = s as Element of D ;
A7: dom g = [:S,S:] by FUNCT_2:def_1;
[d9,s] in [:S,S:] ;
hence g . (d9,s) = f . (d,s9) by A1, A2, A7, FUNCT_1:47
.= s by A6, BINOP_1:3 ;
::_thesis: g . (s,d9) = s
[s,d9] in [:S,S:] ;
hence g . (s,d9) = f . (s9,d) by A1, A2, A7, FUNCT_1:47
.= s by A6, BINOP_1:3 ;
::_thesis: verum
end;
hence d9 is_a_unity_wrt g by BINOP_1:3; ::_thesis: verum
end;
theorem Th3: :: FILTER_2:3
for D being non empty set
for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S holds
( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) )
proof
let D be non empty set ; ::_thesis: for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S holds
( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) )
let S be non empty Subset of D; ::_thesis: for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S holds
( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) )
let f1, f2 be BinOp of D; ::_thesis: for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S holds
( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) )
let g1, g2 be BinOp of S; ::_thesis: ( g1 = f1 || S & g2 = f2 || S implies ( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) ) )
assume that
A1: g1 = f1 || S and
A2: g2 = f2 || S ; ::_thesis: ( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) )
thus ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) ::_thesis: ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 )
proof
assume A3: for a, b, c being Element of D holds f1 . (a,(f2 . (b,c))) = f2 . ((f1 . (a,b)),(f1 . (a,c))) ; :: according to BINOP_1:def_18 ::_thesis: g1 is_left_distributive_wrt g2
let a, b, c be Element of S; :: according to BINOP_1:def_18 ::_thesis: g1 . (a,(g2 . (b,c))) = g2 . ((g1 . (a,b)),(g1 . (a,c)))
set ab = g1 . (a,b);
set ac = g1 . (a,c);
set bc = g2 . (b,c);
reconsider a9 = a, b9 = b, c9 = c as Element of D ;
A4: ( f2 . [b9,c9] = f2 . (b9,c9) & f1 . [a9,b9] = f1 . (a9,b9) ) ;
A5: ( f1 . [a9,c9] = f1 . (a9,c9) & f1 . [a,(g2 . (b,c))] = f1 . (a,(g2 . (b,c))) ) ;
dom g2 = [:S,S:] by FUNCT_2:def_1;
then A6: ( g2 . [b,c] = f2 . [b,c] & g2 . [(g1 . (a,b)),(g1 . (a,c))] = f2 . [(g1 . (a,b)),(g1 . (a,c))] ) by A2, FUNCT_1:47;
A7: f2 . [(g1 . (a,b)),(g1 . (a,c))] = f2 . ((g1 . (a,b)),(g1 . (a,c))) ;
A8: dom g1 = [:S,S:] by FUNCT_2:def_1;
then A9: g1 . [a,(g2 . (b,c))] = f1 . [a,(g2 . (b,c))] by A1, FUNCT_1:47;
( g1 . [a,b] = f1 . [a,b] & g1 . [a,c] = f1 . [a,c] ) by A1, A8, FUNCT_1:47;
hence g1 . (a,(g2 . (b,c))) = g2 . ((g1 . (a,b)),(g1 . (a,c))) by A3, A4, A9, A5, A6, A7; ::_thesis: verum
end;
assume A10: for a, b, c being Element of D holds f1 . ((f2 . (a,b)),c) = f2 . ((f1 . (a,c)),(f1 . (b,c))) ; :: according to BINOP_1:def_19 ::_thesis: g1 is_right_distributive_wrt g2
let a, b, c be Element of S; :: according to BINOP_1:def_19 ::_thesis: g1 . ((g2 . (a,b)),c) = g2 . ((g1 . (a,c)),(g1 . (b,c)))
set ab = g2 . (a,b);
set ac = g1 . (a,c);
set bc = g1 . (b,c);
A11: f2 . [(g1 . (a,c)),(g1 . (b,c))] = f2 . ((g1 . (a,c)),(g1 . (b,c))) ;
A12: dom g1 = [:S,S:] by FUNCT_2:def_1;
then A13: g1 . [(g2 . (a,b)),c] = f1 . [(g2 . (a,b)),c] by A1, FUNCT_1:47;
dom g2 = [:S,S:] by FUNCT_2:def_1;
then A14: ( g2 . [a,b] = f2 . [a,b] & g2 . [(g1 . (a,c)),(g1 . (b,c))] = f2 . [(g1 . (a,c)),(g1 . (b,c))] ) by A2, FUNCT_1:47;
reconsider a9 = a, b9 = b, c9 = c as Element of D ;
A15: ( f1 . [b9,c9] = f1 . (b9,c9) & f2 . [a9,b9] = f2 . (a9,b9) ) ;
A16: ( f1 . [a9,c9] = f1 . (a9,c9) & f1 . [(g2 . (a,b)),c] = f1 . ((g2 . (a,b)),c) ) ;
( g1 . [b,c] = f1 . [b,c] & g1 . [a,c] = f1 . [a,c] ) by A1, A12, FUNCT_1:47;
hence g1 . ((g2 . (a,b)),c) = g2 . ((g1 . (a,c)),(g1 . (b,c))) by A10, A15, A13, A16, A14, A11; ::_thesis: verum
end;
theorem :: FILTER_2:4
for D being non empty set
for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 holds
g1 is_distributive_wrt g2
proof
let D be non empty set ; ::_thesis: for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 holds
g1 is_distributive_wrt g2
let S be non empty Subset of D; ::_thesis: for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 holds
g1 is_distributive_wrt g2
let f1, f2 be BinOp of D; ::_thesis: for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 holds
g1 is_distributive_wrt g2
let g1, g2 be BinOp of S; ::_thesis: ( g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 implies g1 is_distributive_wrt g2 )
assume ( g1 = f1 || S & g2 = f2 || S & f1 is_left_distributive_wrt f2 & f1 is_right_distributive_wrt f2 ) ; :: according to BINOP_1:def_11 ::_thesis: g1 is_distributive_wrt g2
hence ( g1 is_left_distributive_wrt g2 & g1 is_right_distributive_wrt g2 ) by Th3; :: according to BINOP_1:def_11 ::_thesis: verum
end;
theorem Th5: :: FILTER_2:5
for D being non empty set
for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 holds
g1 absorbs g2
proof
let D be non empty set ; ::_thesis: for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 holds
g1 absorbs g2
let S be non empty Subset of D; ::_thesis: for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 holds
g1 absorbs g2
let f1, f2 be BinOp of D; ::_thesis: for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 holds
g1 absorbs g2
let g1, g2 be BinOp of S; ::_thesis: ( g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 implies g1 absorbs g2 )
assume that
A1: g1 = f1 || S and
A2: g2 = f2 || S ; ::_thesis: ( not f1 absorbs f2 or g1 absorbs g2 )
assume A3: for a, b being Element of D holds f1 . (a,(f2 . (a,b))) = a ; :: according to LATTICE2:def_1 ::_thesis: g1 absorbs g2
let a, b be Element of S; :: according to LATTICE2:def_1 ::_thesis: g1 . (a,(g2 . (a,b))) = a
A4: dom g2 = [:S,S:] by FUNCT_2:def_1;
dom g1 = [:S,S:] by FUNCT_2:def_1;
hence g1 . (a,(g2 . (a,b))) = f1 . [a,(g2 . (a,b))] by A1, FUNCT_1:47
.= f1 . [a,(f2 . [a,b])] by A2, A4, FUNCT_1:47
.= f1 . (a,(f2 . (a,b)))
.= a by A3 ;
::_thesis: verum
end;
begin
definition
let D be non empty set ;
let X1, X2 be Subset of D;
:: original: =
redefine predX1 = X2 means :: FILTER_2:def 1
for x being Element of D holds
( x in X1 iff x in X2 );
compatibility
( X1 = X2 iff for x being Element of D holds
( x in X1 iff x in X2 ) ) by SUBSET_1:3;
end;
:: deftheorem defines = FILTER_2:def_1_:_
for D being non empty set
for X1, X2 being Subset of D holds
( X1 = X2 iff for x being Element of D holds
( x in X1 iff x in X2 ) );
deffunc H1( LattStr ) -> set = the carrier of $1;
deffunc H2( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_join of $1;
deffunc H3( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_meet of $1;
theorem :: FILTER_2:6
for L1, L2 being LattStr st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
L1 .: = L2 .: ;
theorem :: FILTER_2:7
for L being Lattice holds (L .:) .: = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) ;
theorem :: FILTER_2:8
for L1, L2 being non empty LattStr st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
proof
let L1, L2 be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) )
assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
let a1, b1 be Element of L1; ::_thesis: for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
let a2, b2 be Element of L2; ::_thesis: ( a1 = a2 & b1 = b2 implies ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) )
assume A2: ( a1 = a2 & b1 = b2 ) ; ::_thesis: ( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
thus a1 "\/" b1 = a2 "\/" b2 by A1, A2; ::_thesis: ( a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
thus a1 "/\" b1 = a2 "/\" b2 by A1, A2; ::_thesis: ( ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )
A3: ( a2 "\/" b2 = b2 iff a2 [= b2 ) by LATTICES:def_3;
( a1 [= b1 iff a1 "\/" b1 = b1 ) by LATTICES:def_3;
hence ( ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) ) by A1, A2, A3; ::_thesis: verum
end;
theorem Th9: :: FILTER_2:9
for L1, L2 being 0_Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
Bottom L1 = Bottom L2
proof
let L1, L2 be 0_Lattice; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies Bottom L1 = Bottom L2 )
assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: Bottom L1 = Bottom L2
then reconsider c = Bottom L1 as Element of L2 ;
now__::_thesis:_for_a_being_Element_of_L2_holds_
(_c_"/\"_a_=_c_&_a_"/\"_c_=_c_)
let a be Element of L2; ::_thesis: ( c "/\" a = c & a "/\" c = c )
reconsider b = a as Element of L1 by A1;
(Bottom L1) "/\" b = Bottom L1 ;
hence c "/\" a = c by A1; ::_thesis: a "/\" c = c
hence a "/\" c = c ; ::_thesis: verum
end;
hence Bottom L1 = Bottom L2 by LATTICES:def_16; ::_thesis: verum
end;
theorem Th10: :: FILTER_2:10
for L1, L2 being 1_Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
Top L1 = Top L2
proof
let L1, L2 be 1_Lattice; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies Top L1 = Top L2 )
assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: Top L1 = Top L2
then reconsider c = Top L1 as Element of L2 ;
now__::_thesis:_for_a_being_Element_of_L2_holds_
(_c_"\/"_a_=_c_&_a_"\/"_c_=_c_)
let a be Element of L2; ::_thesis: ( c "\/" a = c & a "\/" c = c )
reconsider b = a as Element of L1 by A1;
(Top L1) "\/" b = Top L1 ;
hence c "\/" a = c by A1; ::_thesis: a "\/" c = c
hence a "\/" c = c ; ::_thesis: verum
end;
hence Top L1 = Top L2 by LATTICES:def_17; ::_thesis: verum
end;
theorem Th11: :: FILTER_2:11
for L1, L2 being C_Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds
a2 is_a_complement_of b2
proof
let L1, L2 be C_Lattice; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds
a2 is_a_complement_of b2 )
assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds
a2 is_a_complement_of b2
let a1, b1 be Element of L1; ::_thesis: for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds
a2 is_a_complement_of b2
let a2, b2 be Element of L2; ::_thesis: ( a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 implies a2 is_a_complement_of b2 )
assume ( a1 = a2 & b1 = b2 ) ; ::_thesis: ( not a1 is_a_complement_of b1 or a2 is_a_complement_of b2 )
then A2: ( a2 "\/" b2 = a1 "\/" b1 & a2 "/\" b2 = a1 "/\" b1 ) by A1;
assume a1 is_a_complement_of b1 ; ::_thesis: a2 is_a_complement_of b2
then ( a1 "\/" b1 = Top L1 & a1 "/\" b1 = Bottom L1 ) by LATTICES:def_18;
hence ( a2 "\/" b2 = Top L2 & b2 "\/" a2 = Top L2 & a2 "/\" b2 = Bottom L2 & b2 "/\" a2 = Bottom L2 ) by A1, A2, Th9, Th10; :: according to LATTICES:def_18 ::_thesis: verum
end;
theorem :: FILTER_2:12
for L1, L2 being B_Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
for a being Element of L1
for b being Element of L2 st a = b holds
a ` = b `
proof
let L1, L2 be B_Lattice; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies for a being Element of L1
for b being Element of L2 st a = b holds
a ` = b ` )
assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: for a being Element of L1
for b being Element of L2 st a = b holds
a ` = b `
let a be Element of L1; ::_thesis: for b being Element of L2 st a = b holds
a ` = b `
let b be Element of L2; ::_thesis: ( a = b implies a ` = b ` )
assume A2: a = b ; ::_thesis: a ` = b `
reconsider b9 = a ` as Element of L2 by A1;
a ` is_a_complement_of a by LATTICES:def_21;
then b9 is_a_complement_of b by A1, A2, Th11;
hence a ` = b ` by LATTICES:def_21; ::_thesis: verum
end;
theorem :: FILTER_2:13
for L being Lattice
for X being Subset of L st ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "/\" q in X ) ) holds
X is ClosedSubset of L
proof
let L be Lattice; ::_thesis: for X being Subset of L st ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "/\" q in X ) ) holds
X is ClosedSubset of L
let X be Subset of L; ::_thesis: ( ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "/\" q in X ) ) implies X is ClosedSubset of L )
assume A1: for p, q being Element of L holds
( ( p in X & q in X ) iff p "/\" q in X ) ; ::_thesis: X is ClosedSubset of L
for p, q being Element of L st p in X & q in X holds
p "\/" q in X
proof
let p, q be Element of L; ::_thesis: ( p in X & q in X implies p "\/" q in X )
p "/\" (p "\/" q) = p by LATTICES:def_9;
hence ( p in X & q in X implies p "\/" q in X ) by A1; ::_thesis: verum
end;
hence X is ClosedSubset of L by A1, LATTICES:def_24, LATTICES:def_25; ::_thesis: verum
end;
theorem :: FILTER_2:14
for L being Lattice
for X being Subset of L st ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "\/" q in X ) ) holds
X is ClosedSubset of L
proof
let L be Lattice; ::_thesis: for X being Subset of L st ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "\/" q in X ) ) holds
X is ClosedSubset of L
let X be Subset of L; ::_thesis: ( ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "\/" q in X ) ) implies X is ClosedSubset of L )
assume A1: for p, q being Element of L holds
( ( p in X & q in X ) iff p "\/" q in X ) ; ::_thesis: X is ClosedSubset of L
for p, q being Element of L st p in X & q in X holds
p "/\" q in X
proof
let p, q be Element of L; ::_thesis: ( p in X & q in X implies p "/\" q in X )
(p "/\" q) "\/" q = q by LATTICES:def_8;
hence ( p in X & q in X implies p "/\" q in X ) by A1; ::_thesis: verum
end;
hence X is ClosedSubset of L by A1, LATTICES:def_24, LATTICES:def_25; ::_thesis: verum
end;
definition
let L be Lattice;
mode Ideal of L is non empty initial join-closed Subset of L;
end;
Lm1: for L being Lattice
for S being non empty Subset of L holds
( S is Ideal of L iff for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) )
proof
let L be Lattice; ::_thesis: for S being non empty Subset of L holds
( S is Ideal of L iff for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) )
let S be non empty Subset of L; ::_thesis: ( S is Ideal of L iff for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) )
thus ( S is Ideal of L implies for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) ) ::_thesis: ( ( for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) ) implies S is Ideal of L )
proof
assume A1: S is Ideal of L ; ::_thesis: for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S )
let p, q be Element of L; ::_thesis: ( ( p in S & q in S ) iff p "\/" q in S )
thus ( p in S & q in S implies p "\/" q in S ) by A1, LATTICES:def_25; ::_thesis: ( p "\/" q in S implies ( p in S & q in S ) )
assume A2: p "\/" q in S ; ::_thesis: ( p in S & q in S )
( p [= p "\/" q & q [= p "\/" q ) by LATTICES:5;
hence ( p in S & q in S ) by A1, A2, LATTICES:def_22; ::_thesis: verum
end;
assume A3: for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) ; ::_thesis: S is Ideal of L
S is initial
proof
let p, q be Element of L; :: according to LATTICES:def_22 ::_thesis: ( not p [= q or not q in S or p in S )
assume that
A4: p [= q and
A5: q in S ; ::_thesis: p in S
p "\/" q = q by A4, LATTICES:def_3;
hence p in S by A3, A5; ::_thesis: verum
end;
hence S is Ideal of L by A3, LATTICES:def_25; ::_thesis: verum
end;
theorem Th15: :: FILTER_2:15
for L1, L2 being Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
for x being set st x is Filter of L1 holds
x is Filter of L2
proof
let L1, L2 be Lattice; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies for x being set st x is Filter of L1 holds
x is Filter of L2 )
assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: for x being set st x is Filter of L1 holds
x is Filter of L2
let x be set ; ::_thesis: ( x is Filter of L1 implies x is Filter of L2 )
assume x is Filter of L1 ; ::_thesis: x is Filter of L2
then reconsider F = x as Filter of L1 ;
now__::_thesis:_for_a,_b_being_Element_of_L2_holds_
(_(_a_in_F_&_b_in_F_)_iff_a_"/\"_b_in_F_)
let a, b be Element of L2; ::_thesis: ( ( a in F & b in F ) iff a "/\" b in F )
reconsider a9 = a, b9 = b as Element of L1 by A1;
a "/\" b = a9 "/\" b9 by A1;
hence ( ( a in F & b in F ) iff a "/\" b in F ) by FILTER_0:8; ::_thesis: verum
end;
hence x is Filter of L2 by A1, FILTER_0:8; ::_thesis: verum
end;
theorem Th16: :: FILTER_2:16
for L1, L2 being Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
for x being set st x is Ideal of L1 holds
x is Ideal of L2
proof
let L1, L2 be Lattice; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) implies for x being set st x is Ideal of L1 holds
x is Ideal of L2 )
assume A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) ; ::_thesis: for x being set st x is Ideal of L1 holds
x is Ideal of L2
let x be set ; ::_thesis: ( x is Ideal of L1 implies x is Ideal of L2 )
assume x is Ideal of L1 ; ::_thesis: x is Ideal of L2
then reconsider F = x as Ideal of L1 ;
now__::_thesis:_for_a,_b_being_Element_of_L2_holds_
(_(_a_in_F_&_b_in_F_)_iff_a_"\/"_b_in_F_)
let a, b be Element of L2; ::_thesis: ( ( a in F & b in F ) iff a "\/" b in F )
reconsider a9 = a, b9 = b as Element of L1 by A1;
a "\/" b = a9 "\/" b9 by A1;
hence ( ( a in F & b in F ) iff a "\/" b in F ) by Lm1; ::_thesis: verum
end;
hence x is Ideal of L2 by A1, Lm1; ::_thesis: verum
end;
definition
let L be Lattice;
let p be Element of L;
funcp .: -> Element of (L .:) equals :: FILTER_2:def 2
p;
coherence
p is Element of (L .:) ;
end;
:: deftheorem defines .: FILTER_2:def_2_:_
for L being Lattice
for p being Element of L holds p .: = p;
definition
let L be Lattice;
let p be Element of (L .:);
func .: p -> Element of L equals :: FILTER_2:def 3
p;
coherence
p is Element of L ;
end;
:: deftheorem defines .: FILTER_2:def_3_:_
for L being Lattice
for p being Element of (L .:) holds .: p = p;
theorem :: FILTER_2:17
for L being Lattice
for p being Element of L
for p9 being Element of (L .:) holds
( .: (p .:) = p & (.: p9) .: = p9 ) ;
theorem :: FILTER_2:18
for L being Lattice
for p, q being Element of L
for p9, q9 being Element of (L .:) holds
( p "/\" q = (p .:) "\/" (q .:) & p "\/" q = (p .:) "/\" (q .:) & p9 "/\" q9 = (.: p9) "\/" (.: q9) & p9 "\/" q9 = (.: p9) "/\" (.: q9) ) ;
theorem :: FILTER_2:19
for L being Lattice
for p, q being Element of L
for p9, q9 being Element of (L .:) holds
( ( p [= q implies q .: [= p .: ) & ( q .: [= p .: implies p [= q ) & ( p9 [= q9 implies .: q9 [= .: p9 ) & ( .: q9 [= .: p9 implies p9 [= q9 ) ) by LATTICE2:38, LATTICE2:39;
definition
let L be Lattice;
let X be Subset of L;
funcX .: -> Subset of (L .:) equals :: FILTER_2:def 4
X;
coherence
X is Subset of (L .:) ;
end;
:: deftheorem defines .: FILTER_2:def_4_:_
for L being Lattice
for X being Subset of L holds X .: = X;
definition
let L be Lattice;
let X be Subset of (L .:);
func .: X -> Subset of L equals :: FILTER_2:def 5
X;
coherence
X is Subset of L ;
end;
:: deftheorem defines .: FILTER_2:def_5_:_
for L being Lattice
for X being Subset of (L .:) holds .: X = X;
registration
let L be Lattice;
let D be non empty Subset of L;
clusterD .: -> non empty ;
coherence
not D .: is empty ;
end;
registration
let L be Lattice;
let D be non empty Subset of (L .:);
cluster .: D -> non empty ;
coherence
not .: D is empty ;
end;
registration
let L be Lattice;
let S be meet-closed Subset of L;
clusterS .: -> join-closed for Subset of (L .:);
coherence
for b1 being Subset of (L .:) st b1 = S .: holds
b1 is join-closed
proof
S .: is join-closed
proof
let p9 be Element of (L .:); :: according to LATTICES:def_25 ::_thesis: for b1 being Element of the carrier of (L .:) holds
( not p9 in S .: or not b1 in S .: or p9 "\/" b1 in S .: )
let q9 be Element of (L .:); ::_thesis: ( not p9 in S .: or not q9 in S .: or p9 "\/" q9 in S .: )
p9 "\/" q9 = (.: p9) "/\" (.: q9) ;
hence ( not p9 in S .: or not q9 in S .: or p9 "\/" q9 in S .: ) by LATTICES:def_24; ::_thesis: verum
end;
hence for b1 being Subset of (L .:) st b1 = S .: holds
b1 is join-closed ; ::_thesis: verum
end;
end;
registration
let L be Lattice;
let S be join-closed Subset of L;
clusterS .: -> meet-closed for Subset of (L .:);
coherence
for b1 being Subset of (L .:) st b1 = S .: holds
b1 is meet-closed
proof
S .: is meet-closed
proof
let p9 be Element of (L .:); :: according to LATTICES:def_24 ::_thesis: for b1 being Element of the carrier of (L .:) holds
( not p9 in S .: or not b1 in S .: or p9 "/\" b1 in S .: )
let q9 be Element of (L .:); ::_thesis: ( not p9 in S .: or not q9 in S .: or p9 "/\" q9 in S .: )
p9 "/\" q9 = (.: p9) "\/" (.: q9) ;
hence ( not p9 in S .: or not q9 in S .: or p9 "/\" q9 in S .: ) by LATTICES:def_25; ::_thesis: verum
end;
hence for b1 being Subset of (L .:) st b1 = S .: holds
b1 is meet-closed ; ::_thesis: verum
end;
end;
registration
let L be Lattice;
let S be meet-closed Subset of (L .:);
cluster .: S -> join-closed for Subset of L;
coherence
for b1 being Subset of L st b1 = .: S holds
b1 is join-closed
proof
.: S is join-closed
proof
let p be Element of L; :: according to LATTICES:def_25 ::_thesis: for b1 being Element of the carrier of L holds
( not p in .: S or not b1 in .: S or p "\/" b1 in .: S )
let q be Element of L; ::_thesis: ( not p in .: S or not q in .: S or p "\/" q in .: S )
p "\/" q = (p .:) "/\" (q .:) ;
hence ( not p in .: S or not q in .: S or p "\/" q in .: S ) by LATTICES:def_24; ::_thesis: verum
end;
hence for b1 being Subset of L st b1 = .: S holds
b1 is join-closed ; ::_thesis: verum
end;
end;
registration
let L be Lattice;
let S be join-closed Subset of (L .:);
cluster .: S -> meet-closed for Subset of L;
coherence
for b1 being Subset of L st b1 = .: S holds
b1 is meet-closed
proof
.: S is meet-closed
proof
let p be Element of L; :: according to LATTICES:def_24 ::_thesis: for b1 being Element of the carrier of L holds
( not p in .: S or not b1 in .: S or p "/\" b1 in .: S )
let q be Element of L; ::_thesis: ( not p in .: S or not q in .: S or p "/\" q in .: S )
p "/\" q = (p .:) "\/" (q .:) ;
hence ( not p in .: S or not q in .: S or p "/\" q in .: S ) by LATTICES:def_25; ::_thesis: verum
end;
hence for b1 being Subset of L st b1 = .: S holds
b1 is meet-closed ; ::_thesis: verum
end;
end;
registration
let L be Lattice;
let F be final Subset of L;
clusterF .: -> initial for Subset of (L .:);
coherence
for b1 being Subset of (L .:) st b1 = F .: holds
b1 is initial
proof
F .: is initial
proof
let p9 be Element of (L .:); :: according to LATTICES:def_22 ::_thesis: for b1 being Element of the carrier of (L .:) holds
( not p9 [= b1 or not b1 in F .: or p9 in F .: )
let q9 be Element of (L .:); ::_thesis: ( not p9 [= q9 or not q9 in F .: or p9 in F .: )
assume that
A1: p9 [= q9 and
A2: q9 in F .: ; ::_thesis: p9 in F .:
reconsider p = p9 .: , q = q9 .: as Element of L ;
q [= p by A1, LATTICE2:39;
hence p9 in F .: by A2, LATTICES:def_23; ::_thesis: verum
end;
hence for b1 being Subset of (L .:) st b1 = F .: holds
b1 is initial ; ::_thesis: verum
end;
end;
registration
let L be Lattice;
let F be initial Subset of L;
clusterF .: -> final for Subset of (L .:);
coherence
for b1 being Subset of (L .:) st b1 = F .: holds
b1 is final
proof
F .: is final
proof
let p9 be Element of (L .:); :: according to LATTICES:def_23 ::_thesis: for b1 being Element of the carrier of (L .:) holds
( not p9 [= b1 or not p9 in F .: or b1 in F .: )
let q9 be Element of (L .:); ::_thesis: ( not p9 [= q9 or not p9 in F .: or q9 in F .: )
assume that
A1: p9 [= q9 and
A2: p9 in F .: ; ::_thesis: q9 in F .:
reconsider p = p9 .: , q = q9 .: as Element of L ;
q [= p by A1, LATTICE2:39;
hence q9 in F .: by A2, LATTICES:def_22; ::_thesis: verum
end;
hence for b1 being Subset of (L .:) st b1 = F .: holds
b1 is final ; ::_thesis: verum
end;
end;
registration
let L be Lattice;
let F be final Subset of (L .:);
cluster .: F -> initial for Subset of L;
coherence
for b1 being Subset of L st b1 = .: F holds
b1 is initial
proof
.: F is initial
proof
let p be Element of L; :: according to LATTICES:def_22 ::_thesis: for b1 being Element of the carrier of L holds
( not p [= b1 or not b1 in .: F or p in .: F )
let q be Element of L; ::_thesis: ( not p [= q or not q in .: F or p in .: F )
assume that
A1: p [= q and
A2: q in .: F ; ::_thesis: p in .: F
reconsider p9 = p .: , q9 = q .: as Element of (L .:) ;
q9 [= p9 by A1, LATTICE2:38;
hence p in .: F by A2, LATTICES:def_23; ::_thesis: verum
end;
hence for b1 being Subset of L st b1 = .: F holds
b1 is initial ; ::_thesis: verum
end;
end;
registration
let L be Lattice;
let F be initial Subset of (L .:);
clusterF .: -> final for Subset of L;
coherence
for b1 being Subset of L st b1 = F .: holds
b1 is final
proof
.: F is final
proof
let p be Element of L; :: according to LATTICES:def_23 ::_thesis: for b1 being Element of the carrier of L holds
( not p [= b1 or not p in .: F or b1 in .: F )
let q be Element of L; ::_thesis: ( not p [= q or not p in .: F or q in .: F )
assume that
A1: p [= q and
A2: p in .: F ; ::_thesis: q in .: F
reconsider p9 = p .: , q9 = q .: as Element of (L .:) ;
q9 [= p9 by A1, LATTICE2:38;
hence q in .: F by A2, LATTICES:def_22; ::_thesis: verum
end;
hence for b1 being Subset of L st b1 = F .: holds
b1 is final ; ::_thesis: verum
end;
end;
theorem Th20: :: FILTER_2:20
for L being Lattice
for x being set holds
( x is Ideal of L iff x is Filter of (L .:) )
proof
let L be Lattice; ::_thesis: for x being set holds
( x is Ideal of L iff x is Filter of (L .:) )
let x be set ; ::_thesis: ( x is Ideal of L iff x is Filter of (L .:) )
thus ( x is Ideal of L implies x is Filter of (L .:) ) ::_thesis: ( x is Filter of (L .:) implies x is Ideal of L )
proof
assume x is Ideal of L ; ::_thesis: x is Filter of (L .:)
then reconsider I = x as Ideal of L ;
reconsider I = I as non empty Subset of (L .:) ;
I is Filter of (L .:)
proof
now__::_thesis:_for_p9,_q9_being_Element_of_(L_.:)_holds_
(_(_p9_in_I_&_q9_in_I_)_iff_p9_"/\"_q9_in_I_)
let p9, q9 be Element of (L .:); ::_thesis: ( ( p9 in I & q9 in I ) iff p9 "/\" q9 in I )
p9 "/\" q9 = (.: p9) "\/" (.: q9) ;
hence ( ( p9 in I & q9 in I ) iff p9 "/\" q9 in I ) by Lm1; ::_thesis: verum
end;
hence I is Filter of (L .:) by FILTER_0:8; ::_thesis: verum
end;
hence x is Filter of (L .:) ; ::_thesis: verum
end;
assume x is Filter of (L .:) ; ::_thesis: x is Ideal of L
then reconsider F = x as Filter of (L .:) ;
reconsider F = F as non empty Subset of L ;
now__::_thesis:_for_p,_q_being_Element_of_L_holds_
(_(_p_in_F_&_q_in_F_)_iff_p_"\/"_q_in_F_)
let p, q be Element of L; ::_thesis: ( ( p in F & q in F ) iff p "\/" q in F )
(p .:) "/\" (q .:) = p "\/" q ;
hence ( ( p in F & q in F ) iff p "\/" q in F ) by FILTER_0:8; ::_thesis: verum
end;
hence x is Ideal of L by Lm1; ::_thesis: verum
end;
theorem Th21: :: FILTER_2:21
for L being Lattice
for D being non empty Subset of L holds
( D is Ideal of L iff ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) ) )
proof
let L be Lattice; ::_thesis: for D being non empty Subset of L holds
( D is Ideal of L iff ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) ) )
let D be non empty Subset of L; ::_thesis: ( D is Ideal of L iff ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) ) )
thus ( D is Ideal of L implies ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) ) ) ::_thesis: ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) implies D is Ideal of L )
proof
assume A1: D is Ideal of L ; ::_thesis: ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) )
hence for p, q being Element of L st p in D & q in D holds
p "\/" q in D by Lm1; ::_thesis: for p, q being Element of L st p in D & q [= p holds
q in D
let p, q be Element of L; ::_thesis: ( p in D & q [= p implies q in D )
assume ( p in D & q [= p ) ; ::_thesis: q in D
then q "\/" p in D by LATTICES:def_3;
hence q in D by A1, Lm1; ::_thesis: verum
end;
assume A2: ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) ) ; ::_thesis: D is Ideal of L
now__::_thesis:_for_p,_q_being_Element_of_L_holds_
(_(_p_in_D_&_q_in_D_)_iff_p_"\/"_q_in_D_)
let p, q be Element of L; ::_thesis: ( ( p in D & q in D ) iff p "\/" q in D )
( p [= p "\/" q & q [= q "\/" p ) by LATTICES:5;
hence ( ( p in D & q in D ) iff p "\/" q in D ) by A2; ::_thesis: verum
end;
hence D is Ideal of L by Lm1; ::_thesis: verum
end;
theorem Th22: :: FILTER_2:22
for L being Lattice
for p, q being Element of L
for I being Ideal of L st p in I holds
( p "/\" q in I & q "/\" p in I )
proof
let L be Lattice; ::_thesis: for p, q being Element of L
for I being Ideal of L st p in I holds
( p "/\" q in I & q "/\" p in I )
let p, q be Element of L; ::_thesis: for I being Ideal of L st p in I holds
( p "/\" q in I & q "/\" p in I )
let I be Ideal of L; ::_thesis: ( p in I implies ( p "/\" q in I & q "/\" p in I ) )
p "/\" q [= p by LATTICES:6;
hence ( p in I implies ( p "/\" q in I & q "/\" p in I ) ) by Th21; ::_thesis: verum
end;
theorem :: FILTER_2:23
for L being Lattice
for I being Ideal of L ex p being Element of L st p in I
proof
let L be Lattice; ::_thesis: for I being Ideal of L ex p being Element of L st p in I
let I be Ideal of L; ::_thesis: ex p being Element of L st p in I
set i = the Element of I;
the Element of I is Element of L ;
hence ex p being Element of L st p in I ; ::_thesis: verum
end;
theorem :: FILTER_2:24
for L being Lattice
for I being Ideal of L st L is lower-bounded holds
Bottom L in I
proof
let L be Lattice; ::_thesis: for I being Ideal of L st L is lower-bounded holds
Bottom L in I
let I be Ideal of L; ::_thesis: ( L is lower-bounded implies Bottom L in I )
assume L is lower-bounded ; ::_thesis: Bottom L in I
then ( Top (L .:) = Bottom L & L .: is upper-bounded ) by LATTICE2:48, LATTICE2:61;
then Bottom L in I .: by FILTER_0:11;
hence Bottom L in I ; ::_thesis: verum
end;
theorem :: FILTER_2:25
for L being Lattice st L is lower-bounded holds
{(Bottom L)} is Ideal of L
proof
let L be Lattice; ::_thesis: ( L is lower-bounded implies {(Bottom L)} is Ideal of L )
assume L is lower-bounded ; ::_thesis: {(Bottom L)} is Ideal of L
then ( Top (L .:) = Bottom L & L .: is upper-bounded ) by LATTICE2:48, LATTICE2:61;
then {(Bottom L)} is Filter of (L .:) by FILTER_0:12;
hence {(Bottom L)} is Ideal of L by Th20; ::_thesis: verum
end;
theorem :: FILTER_2:26
for L being Lattice
for p being Element of L st {p} is Ideal of L holds
L is lower-bounded
proof
let L be Lattice; ::_thesis: for p being Element of L st {p} is Ideal of L holds
L is lower-bounded
let p be Element of L; ::_thesis: ( {p} is Ideal of L implies L is lower-bounded )
assume {p} is Ideal of L ; ::_thesis: L is lower-bounded
then {p} is Filter of (L .:) by Th20;
then L .: is upper-bounded by FILTER_0:13;
hence L is lower-bounded by LATTICE2:48; ::_thesis: verum
end;
begin
theorem Th27: :: FILTER_2:27
for L being Lattice holds the carrier of L is Ideal of L
proof
let L be Lattice; ::_thesis: the carrier of L is Ideal of L
H1(L) is Filter of (L .:) by FILTER_0:14;
hence the carrier of L is Ideal of L by Th20; ::_thesis: verum
end;
definition
let L be Lattice;
func(.L.> -> Ideal of L equals :: FILTER_2:def 6
the carrier of L;
coherence
the carrier of L is Ideal of L by Th27;
end;
:: deftheorem defines (. FILTER_2:def_6_:_
for L being Lattice holds (.L.> = the carrier of L;
definition
let L be Lattice;
let p be Element of L;
func(.p.> -> Ideal of L equals :: FILTER_2:def 7
{ q where q is Element of L : q [= p } ;
coherence
{ q where q is Element of L : q [= p } is Ideal of L
proof
set X = { q where q is Element of L : q [= p } ;
p in { q where q is Element of L : q [= p } ;
then reconsider X = { q where q is Element of L : q [= p } as non empty set ;
X c= H1(L)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in H1(L) )
assume x in X ; ::_thesis: x in H1(L)
then ex q being Element of L st
( x = q & q [= p ) ;
hence x in H1(L) ; ::_thesis: verum
end;
then reconsider X = X as non empty Subset of L ;
now__::_thesis:_for_q,_r_being_Element_of_L_holds_
(_(_q_in_X_&_r_in_X_implies_q_"\/"_r_in_X_)_&_(_q_"\/"_r_in_X_implies_(_q_in_X_&_r_in_X_)_)_)
let q, r be Element of L; ::_thesis: ( ( q in X & r in X implies q "\/" r in X ) & ( q "\/" r in X implies ( q in X & r in X ) ) )
thus ( q in X & r in X implies q "\/" r in X ) ::_thesis: ( q "\/" r in X implies ( q in X & r in X ) )
proof
assume ( q in X & r in X ) ; ::_thesis: q "\/" r in X
then ( ex r being Element of L st
( q = r & r [= p ) & ex q being Element of L st
( r = q & q [= p ) ) ;
then q "\/" r [= p by FILTER_0:6;
hence q "\/" r in X ; ::_thesis: verum
end;
assume q "\/" r in X ; ::_thesis: ( q in X & r in X )
then A1: ex s being Element of L st
( q "\/" r = s & s [= p ) ;
q [= q "\/" r by LATTICES:5;
then A2: q [= p by A1, LATTICES:7;
r [= r "\/" q by LATTICES:5;
then r [= p by A1, LATTICES:7;
hence ( q in X & r in X ) by A2; ::_thesis: verum
end;
hence { q where q is Element of L : q [= p } is Ideal of L by Lm1; ::_thesis: verum
end;
end;
:: deftheorem defines (. FILTER_2:def_7_:_
for L being Lattice
for p being Element of L holds (.p.> = { q where q is Element of L : q [= p } ;
theorem Th28: :: FILTER_2:28
for L being Lattice
for q, p being Element of L holds
( q in (.p.> iff q [= p )
proof
let L be Lattice; ::_thesis: for q, p being Element of L holds
( q in (.p.> iff q [= p )
let q, p be Element of L; ::_thesis: ( q in (.p.> iff q [= p )
( q in (.p.> iff ex r being Element of L st
( q = r & r [= p ) ) ;
hence ( q in (.p.> iff q [= p ) ; ::_thesis: verum
end;
theorem Th29: :: FILTER_2:29
for L being Lattice
for p being Element of L holds
( (.p.> = <.(p .:).) & (.(p .:).> = <.p.) )
proof
let L be Lattice; ::_thesis: for p being Element of L holds
( (.p.> = <.(p .:).) & (.(p .:).> = <.p.) )
let p be Element of L; ::_thesis: ( (.p.> = <.(p .:).) & (.(p .:).> = <.p.) )
(.p.> = .: <.(p .:).)
proof
let q be Element of L; :: according to FILTER_2:def_1 ::_thesis: ( q in (.p.> iff q in .: <.(p .:).) )
A1: ( q .: in <.(p .:).) iff p .: [= q .: ) by FILTER_0:15;
( q in (.p.> iff q [= p ) by Th28;
hence ( q in (.p.> iff q in .: <.(p .:).) ) by A1, LATTICE2:38, LATTICE2:39; ::_thesis: verum
end;
hence (.p.> = <.(p .:).) ; ::_thesis: (.(p .:).> = <.p.)
.: (.(p .:).> = <.p.)
proof
let q be Element of L; :: according to FILTER_2:def_1 ::_thesis: ( q in .: (.(p .:).> iff q in <.p.) )
A2: ( q in <.p.) iff p [= q ) by FILTER_0:15;
( q .: in (.(p .:).> iff q .: [= p .: ) by Th28;
hence ( q in .: (.(p .:).> iff q in <.p.) ) by A2, LATTICE2:38, LATTICE2:39; ::_thesis: verum
end;
hence (.(p .:).> = <.p.) ; ::_thesis: verum
end;
theorem :: FILTER_2:30
for L being Lattice
for p, q being Element of L holds
( p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.> )
proof
let L be Lattice; ::_thesis: for p, q being Element of L holds
( p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.> )
let p, q be Element of L; ::_thesis: ( p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.> )
p "/\" q [= p by LATTICES:6;
hence ( p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.> ) ; ::_thesis: verum
end;
theorem :: FILTER_2:31
for L being Lattice st L is upper-bounded holds
(.L.> = (.(Top L).>
proof
let L be Lattice; ::_thesis: ( L is upper-bounded implies (.L.> = (.(Top L).> )
assume A1: L is upper-bounded ; ::_thesis: (.L.> = (.(Top L).>
then L .: is lower-bounded by LATTICE2:49;
then A2: <.(L .:).) = <.(Bottom (L .:)).) by FILTER_0:17;
Bottom (L .:) = (Top L) .: by A1, LATTICE2:62;
hence (.L.> = (.(Top L).> by A2, Th29; ::_thesis: verum
end;
definition
let L be Lattice;
let I be Ideal of L;
predI is_max-ideal means :: FILTER_2:def 8
( I <> the carrier of L & ( for J being Ideal of L st I c= J & J <> the carrier of L holds
I = J ) );
end;
:: deftheorem defines is_max-ideal FILTER_2:def_8_:_
for L being Lattice
for I being Ideal of L holds
( I is_max-ideal iff ( I <> the carrier of L & ( for J being Ideal of L st I c= J & J <> the carrier of L holds
I = J ) ) );
theorem Th32: :: FILTER_2:32
for L being Lattice
for I being Ideal of L holds
( I is_max-ideal iff I .: is being_ultrafilter )
proof
let L be Lattice; ::_thesis: for I being Ideal of L holds
( I is_max-ideal iff I .: is being_ultrafilter )
let I be Ideal of L; ::_thesis: ( I is_max-ideal iff I .: is being_ultrafilter )
thus ( I is_max-ideal implies I .: is being_ultrafilter ) ::_thesis: ( I .: is being_ultrafilter implies I is_max-ideal )
proof
assume that
A1: I <> H1(L) and
A2: for J being Ideal of L st I c= J & J <> H1(L) holds
I = J ; :: according to FILTER_2:def_8 ::_thesis: I .: is being_ultrafilter
thus I .: <> H1(L .: ) by A1; :: according to FILTER_0:def_3 ::_thesis: for b1 being Element of bool the carrier of (L .:) holds
( not I .: c= b1 or b1 = the carrier of (L .:) or I .: = b1 )
let F be Filter of (L .:); ::_thesis: ( not I .: c= F or F = the carrier of (L .:) or I .: = F )
.: F = F ;
hence ( not I .: c= F or F = the carrier of (L .:) or I .: = F ) by A2; ::_thesis: verum
end;
assume that
A3: I .: <> H1(L .: ) and
A4: for F being Filter of (L .:) st I .: c= F & F <> H1(L .: ) holds
I .: = F ; :: according to FILTER_0:def_3 ::_thesis: I is_max-ideal
thus I <> H1(L) by A3; :: according to FILTER_2:def_8 ::_thesis: for J being Ideal of L st I c= J & J <> the carrier of L holds
I = J
let J be Ideal of L; ::_thesis: ( I c= J & J <> the carrier of L implies I = J )
J .: = J ;
hence ( I c= J & J <> the carrier of L implies I = J ) by A4; ::_thesis: verum
end;
theorem :: FILTER_2:33
for L being Lattice st L is upper-bounded holds
for I being Ideal of L st I <> the carrier of L holds
ex J being Ideal of L st
( I c= J & J is_max-ideal )
proof
let L be Lattice; ::_thesis: ( L is upper-bounded implies for I being Ideal of L st I <> the carrier of L holds
ex J being Ideal of L st
( I c= J & J is_max-ideal ) )
assume L is upper-bounded ; ::_thesis: for I being Ideal of L st I <> the carrier of L holds
ex J being Ideal of L st
( I c= J & J is_max-ideal )
then A1: L .: is lower-bounded by LATTICE2:49;
let I be Ideal of L; ::_thesis: ( I <> the carrier of L implies ex J being Ideal of L st
( I c= J & J is_max-ideal ) )
assume I <> H1(L) ; ::_thesis: ex J being Ideal of L st
( I c= J & J is_max-ideal )
then consider F being Filter of (L .:) such that
A2: ( I .: c= F & F is being_ultrafilter ) by A1, FILTER_0:18;
take .: F ; ::_thesis: ( I c= .: F & .: F is_max-ideal )
(.: F) .: = .: F ;
hence ( I c= .: F & .: F is_max-ideal ) by A2, Th32; ::_thesis: verum
end;
theorem :: FILTER_2:34
for L being Lattice
for p being Element of L st ex r being Element of L st p "\/" r <> p holds
(.p.> <> the carrier of L
proof
let L be Lattice; ::_thesis: for p being Element of L st ex r being Element of L st p "\/" r <> p holds
(.p.> <> the carrier of L
let p be Element of L; ::_thesis: ( ex r being Element of L st p "\/" r <> p implies (.p.> <> the carrier of L )
given r being Element of L such that A1: p "\/" r <> p ; ::_thesis: (.p.> <> the carrier of L
p "\/" r = (p .:) "/\" (r .:) ;
then <.(p .:).) <> H1(L .: ) by A1, FILTER_0:19;
hence (.p.> <> the carrier of L by Th29; ::_thesis: verum
end;
theorem :: FILTER_2:35
for L being Lattice
for p being Element of L st L is upper-bounded & p <> Top L holds
ex I being Ideal of L st
( p in I & I is_max-ideal )
proof
let L be Lattice; ::_thesis: for p being Element of L st L is upper-bounded & p <> Top L holds
ex I being Ideal of L st
( p in I & I is_max-ideal )
let p be Element of L; ::_thesis: ( L is upper-bounded & p <> Top L implies ex I being Ideal of L st
( p in I & I is_max-ideal ) )
assume L is upper-bounded ; ::_thesis: ( not p <> Top L or ex I being Ideal of L st
( p in I & I is_max-ideal ) )
then A1: ( L .: is lower-bounded & Bottom (L .:) = Top L ) by LATTICE2:49, LATTICE2:62;
assume p <> Top L ; ::_thesis: ex I being Ideal of L st
( p in I & I is_max-ideal )
then consider F being Filter of (L .:) such that
A2: ( p .: in F & F is being_ultrafilter ) by A1, FILTER_0:20;
take .: F ; ::_thesis: ( p in .: F & .: F is_max-ideal )
(.: F) .: = .: F ;
hence ( p in .: F & .: F is_max-ideal ) by A2, Th32; ::_thesis: verum
end;
definition
let L be Lattice;
let D be non empty Subset of L;
func(.D.> -> Ideal of L means :Def9: :: FILTER_2:def 9
( D c= it & ( for I being Ideal of L st D c= I holds
it c= I ) );
existence
ex b1 being Ideal of L st
( D c= b1 & ( for I being Ideal of L st D c= I holds
b1 c= I ) )
proof
take I = .: <.(D .:).); ::_thesis: ( D c= I & ( for I being Ideal of L st D c= I holds
I c= I ) )
thus D c= I by FILTER_0:def_4; ::_thesis: for I being Ideal of L st D c= I holds
I c= I
let J be Ideal of L; ::_thesis: ( D c= J implies I c= J )
J .: = J ;
hence ( D c= J implies I c= J ) by FILTER_0:def_4; ::_thesis: verum
end;
uniqueness
for b1, b2 being Ideal of L st D c= b1 & ( for I being Ideal of L st D c= I holds
b1 c= I ) & D c= b2 & ( for I being Ideal of L st D c= I holds
b2 c= I ) holds
b1 = b2
proof
let I1, I2 be Ideal of L; ::_thesis: ( D c= I1 & ( for I being Ideal of L st D c= I holds
I1 c= I ) & D c= I2 & ( for I being Ideal of L st D c= I holds
I2 c= I ) implies I1 = I2 )
assume ( D c= I1 & ( for I being Ideal of L st D c= I holds
I1 c= I ) & D c= I2 & ( for I being Ideal of L st D c= I holds
I2 c= I ) ) ; ::_thesis: I1 = I2
then ( I1 c= I2 & I2 c= I1 ) ;
hence I1 = I2 by XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines (. FILTER_2:def_9_:_
for L being Lattice
for D being non empty Subset of L
for b3 being Ideal of L holds
( b3 = (.D.> iff ( D c= b3 & ( for I being Ideal of L st D c= I holds
b3 c= I ) ) );
Lm2: for L1, L2 being Lattice
for D1 being non empty Subset of L1
for D2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 holds
( <.D1.) = <.D2.) & (.D1.> = (.D2.> )
proof
let L1, L2 be Lattice; ::_thesis: for D1 being non empty Subset of L1
for D2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 holds
( <.D1.) = <.D2.) & (.D1.> = (.D2.> )
let D1 be non empty Subset of L1; ::_thesis: for D2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 holds
( <.D1.) = <.D2.) & (.D1.> = (.D2.> )
let D2 be non empty Subset of L2; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 implies ( <.D1.) = <.D2.) & (.D1.> = (.D2.> ) )
assume that
A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) and
A2: D1 = D2 ; ::_thesis: ( <.D1.) = <.D2.) & (.D1.> = (.D2.> )
A3: ( D1 c= <.D1.) & D2 c= <.D2.) ) by FILTER_0:def_4;
( <.D1.) is Filter of L2 & <.D2.) is Filter of L1 ) by A1, Th15;
hence ( <.D1.) c= <.D2.) & <.D2.) c= <.D1.) ) by A2, A3, FILTER_0:def_4; :: according to XBOOLE_0:def_10 ::_thesis: (.D1.> = (.D2.>
A4: ( D1 c= (.D1.> & D2 c= (.D2.> ) by Def9;
( (.D1.> is Ideal of L2 & (.D2.> is Ideal of L1 ) by A1, Th16;
hence ( (.D1.> c= (.D2.> & (.D2.> c= (.D1.> ) by A2, A4, Def9; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
theorem Th36: :: FILTER_2:36
for L being Lattice
for D being non empty Subset of L
for D9 being non empty Subset of (L .:) holds
( <.(D .:).) = (.D.> & <.D.) = (.(D .:).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> )
proof
let L be Lattice; ::_thesis: for D being non empty Subset of L
for D9 being non empty Subset of (L .:) holds
( <.(D .:).) = (.D.> & <.D.) = (.(D .:).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> )
let D be non empty Subset of L; ::_thesis: for D9 being non empty Subset of (L .:) holds
( <.(D .:).) = (.D.> & <.D.) = (.(D .:).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> )
let D9 be non empty Subset of (L .:); ::_thesis: ( <.(D .:).) = (.D.> & <.D.) = (.(D .:).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> )
A1: for L being Lattice
for D being non empty Subset of L holds <.(D .:).) = (.D.>
proof
let L be Lattice; ::_thesis: for D being non empty Subset of L holds <.(D .:).) = (.D.>
let D be non empty Subset of L; ::_thesis: <.(D .:).) = (.D.>
(.D.> .: = (.D.> ;
then A2: ( D c= (.D.> implies <.(D .:).) c= (.D.> ) by FILTER_0:def_4;
.: <.(D .:).) = <.(D .:).) ;
then ( D c= <.(D .:).) implies (.D.> c= <.(D .:).) ) by Def9;
hence <.(D .:).) = (.D.> by A2, Def9, FILTER_0:def_4, XBOOLE_0:def_10; ::_thesis: verum
end;
( <.((D .:) .:).) = <.D.) & <.(((.: D9) .:) .:).) = <.(.: D9).) ) by Lm2;
hence ( <.(D .:).) = (.D.> & <.D.) = (.(D .:).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> ) by A1; ::_thesis: verum
end;
theorem Th37: :: FILTER_2:37
for L being Lattice
for I being Ideal of L holds (.I.> = I
proof
let L be Lattice; ::_thesis: for I being Ideal of L holds (.I.> = I
let I be Ideal of L; ::_thesis: (.I.> = I
( (.I.> c= I & I c= (.I.> ) by Def9;
hence (.I.> = I by XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: FILTER_2:38
for L being Lattice
for D, D1, D2 being non empty Subset of L holds
( ( D1 c= D2 implies (.D1.> c= (.D2.> ) & (.(.D.>.> c= (.D.> )
proof
let L be Lattice; ::_thesis: for D, D1, D2 being non empty Subset of L holds
( ( D1 c= D2 implies (.D1.> c= (.D2.> ) & (.(.D.>.> c= (.D.> )
let D, D1, D2 be non empty Subset of L; ::_thesis: ( ( D1 c= D2 implies (.D1.> c= (.D2.> ) & (.(.D.>.> c= (.D.> )
D2 c= (.D2.> by Def9;
then ( D1 c= D2 implies D1 c= (.D2.> ) by XBOOLE_1:1;
hence ( ( D1 c= D2 implies (.D1.> c= (.D2.> ) & (.(.D.>.> c= (.D.> ) by Def9; ::_thesis: verum
end;
theorem :: FILTER_2:39
for L being Lattice
for p being Element of L
for D being non empty Subset of L st p in D holds
(.p.> c= (.D.>
proof
let L be Lattice; ::_thesis: for p being Element of L
for D being non empty Subset of L st p in D holds
(.p.> c= (.D.>
let p be Element of L; ::_thesis: for D being non empty Subset of L st p in D holds
(.p.> c= (.D.>
let D be non empty Subset of L; ::_thesis: ( p in D implies (.p.> c= (.D.> )
( <.(p .:).) = (.p.> & <.(D .:).) = (.D.> ) by Th29, Th36;
hence ( p in D implies (.p.> c= (.D.> ) by FILTER_0:23; ::_thesis: verum
end;
theorem :: FILTER_2:40
for L being Lattice
for p being Element of L
for D being non empty Subset of L st D = {p} holds
(.D.> = (.p.>
proof
let L be Lattice; ::_thesis: for p being Element of L
for D being non empty Subset of L st D = {p} holds
(.D.> = (.p.>
let p be Element of L; ::_thesis: for D being non empty Subset of L st D = {p} holds
(.D.> = (.p.>
let D be non empty Subset of L; ::_thesis: ( D = {p} implies (.D.> = (.p.> )
( <.(p .:).) = (.p.> & <.(D .:).) = (.D.> ) by Th29, Th36;
hence ( D = {p} implies (.D.> = (.p.> ) by FILTER_0:24; ::_thesis: verum
end;
theorem Th41: :: FILTER_2:41
for L being Lattice
for D being non empty Subset of L st L is upper-bounded & Top L in D holds
( (.D.> = (.L.> & (.D.> = the carrier of L )
proof
let L be Lattice; ::_thesis: for D being non empty Subset of L st L is upper-bounded & Top L in D holds
( (.D.> = (.L.> & (.D.> = the carrier of L )
let D be non empty Subset of L; ::_thesis: ( L is upper-bounded & Top L in D implies ( (.D.> = (.L.> & (.D.> = the carrier of L ) )
assume L is upper-bounded ; ::_thesis: ( not Top L in D or ( (.D.> = (.L.> & (.D.> = the carrier of L ) )
then A1: ( L .: is lower-bounded & Bottom (L .:) = Top L ) by LATTICE2:49, LATTICE2:62;
assume Top L in D ; ::_thesis: ( (.D.> = (.L.> & (.D.> = the carrier of L )
then <.(D .:).) = <.(L .:).) by A1, FILTER_0:25;
hence ( (.D.> = (.L.> & (.D.> = the carrier of L ) by Th36; ::_thesis: verum
end;
theorem :: FILTER_2:42
for L being Lattice
for I being Ideal of L st L is upper-bounded & Top L in I holds
( I = (.L.> & I = the carrier of L )
proof
let L be Lattice; ::_thesis: for I being Ideal of L st L is upper-bounded & Top L in I holds
( I = (.L.> & I = the carrier of L )
let I be Ideal of L; ::_thesis: ( L is upper-bounded & Top L in I implies ( I = (.L.> & I = the carrier of L ) )
(.I.> = I by Th37;
hence ( L is upper-bounded & Top L in I implies ( I = (.L.> & I = the carrier of L ) ) by Th41; ::_thesis: verum
end;
definition
let L be Lattice;
let I be Ideal of L;
attrI is prime means :: FILTER_2:def 10
for p, q being Element of L holds
( p "/\" q in I iff ( p in I or q in I ) );
end;
:: deftheorem defines prime FILTER_2:def_10_:_
for L being Lattice
for I being Ideal of L holds
( I is prime iff for p, q being Element of L holds
( p "/\" q in I iff ( p in I or q in I ) ) );
theorem Th43: :: FILTER_2:43
for L being Lattice
for I being Ideal of L holds
( I is prime iff I .: is prime )
proof
let L be Lattice; ::_thesis: for I being Ideal of L holds
( I is prime iff I .: is prime )
let I be Ideal of L; ::_thesis: ( I is prime iff I .: is prime )
thus ( I is prime implies I .: is prime ) ::_thesis: ( I .: is prime implies I is prime )
proof
assume A1: for p, q being Element of L holds
( p "/\" q in I iff ( p in I or q in I ) ) ; :: according to FILTER_2:def_10 ::_thesis: I .: is prime
let p9 be Element of (L .:); :: according to FILTER_0:def_5 ::_thesis: for b1 being Element of the carrier of (L .:) holds
( ( not p9 "\/" b1 in I .: or p9 in I .: or b1 in I .: ) & ( ( not p9 in I .: & not b1 in I .: ) or p9 "\/" b1 in I .: ) )
let q9 be Element of (L .:); ::_thesis: ( ( not p9 "\/" q9 in I .: or p9 in I .: or q9 in I .: ) & ( ( not p9 in I .: & not q9 in I .: ) or p9 "\/" q9 in I .: ) )
p9 "\/" q9 = (.: p9) "/\" (.: q9) ;
hence ( ( not p9 "\/" q9 in I .: or p9 in I .: or q9 in I .: ) & ( ( not p9 in I .: & not q9 in I .: ) or p9 "\/" q9 in I .: ) ) by A1; ::_thesis: verum
end;
assume A2: for p9, q9 being Element of (L .:) holds
( p9 "\/" q9 in I .: iff ( p9 in I .: or q9 in I .: ) ) ; :: according to FILTER_0:def_5 ::_thesis: I is prime
let p be Element of L; :: according to FILTER_2:def_10 ::_thesis: for q being Element of L holds
( p "/\" q in I iff ( p in I or q in I ) )
let q be Element of L; ::_thesis: ( p "/\" q in I iff ( p in I or q in I ) )
(p .:) "\/" (q .:) = p "/\" q ;
hence ( p "/\" q in I iff ( p in I or q in I ) ) by A2; ::_thesis: verum
end;
definition
let L be Lattice;
let D1, D2 be non empty Subset of L;
funcD1 "\/" D2 -> Subset of L equals :: FILTER_2:def 11
{ (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ;
coherence
{ (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } is Subset of L
proof
set X = { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ;
{ (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } c= H1(L)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } or x in H1(L) )
assume x in { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ; ::_thesis: x in H1(L)
then ex p, q being Element of L st
( x = p "\/" q & p in D1 & q in D2 ) ;
hence x in H1(L) ; ::_thesis: verum
end;
hence { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } is Subset of L ; ::_thesis: verum
end;
end;
:: deftheorem defines "\/" FILTER_2:def_11_:_
for L being Lattice
for D1, D2 being non empty Subset of L holds D1 "\/" D2 = { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ;
registration
let L be Lattice;
let D1, D2 be non empty Subset of L;
clusterD1 "\/" D2 -> non empty ;
coherence
not D1 "\/" D2 is empty
proof
set X = { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ;
set p1 = the Element of D1;
set p2 = the Element of D2;
the Element of D1 "\/" the Element of D2 in { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ;
then reconsider X = { (p "\/" q) where p, q is Element of L : ( p in D1 & q in D2 ) } as non empty set ;
X = D1 "\/" D2 ;
hence not D1 "\/" D2 is empty ; ::_thesis: verum
end;
end;
Lm3: for L1, L2 being Lattice
for D1, E1 being non empty Subset of L1
for D2, E2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 & E1 = E2 holds
D1 "/\" E1 = D2 "/\" E2
proof
let L1, L2 be Lattice; ::_thesis: for D1, E1 being non empty Subset of L1
for D2, E2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 & E1 = E2 holds
D1 "/\" E1 = D2 "/\" E2
let D1, E1 be non empty Subset of L1; ::_thesis: for D2, E2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 & E1 = E2 holds
D1 "/\" E1 = D2 "/\" E2
let D2, E2 be non empty Subset of L2; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 & E1 = E2 implies D1 "/\" E1 = D2 "/\" E2 )
assume that
A1: LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) and
A2: ( D1 = D2 & E1 = E2 ) ; ::_thesis: D1 "/\" E1 = D2 "/\" E2
thus D1 "/\" E1 c= D2 "/\" E2 :: according to XBOOLE_0:def_10 ::_thesis: D2 "/\" E2 c= D1 "/\" E1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 "/\" E1 or x in D2 "/\" E2 )
assume x in D1 "/\" E1 ; ::_thesis: x in D2 "/\" E2
then consider a, b being Element of L1 such that
A3: x = a "/\" b and
A4: ( a in D1 & b in E1 ) ;
reconsider a9 = a, b9 = b as Element of L2 by A1;
x = a9 "/\" b9 by A1, A3;
hence x in D2 "/\" E2 by A2, A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D2 "/\" E2 or x in D1 "/\" E1 )
assume x in D2 "/\" E2 ; ::_thesis: x in D1 "/\" E1
then consider a, b being Element of L2 such that
A5: x = a "/\" b and
A6: ( a in D2 & b in E2 ) ;
reconsider a9 = a, b9 = b as Element of L1 by A1;
x = a9 "/\" b9 by A1, A5;
hence x in D1 "/\" E1 by A2, A6; ::_thesis: verum
end;
theorem Th44: :: FILTER_2:44
for L being Lattice
for D1, D2 being non empty Subset of L
for D19, D29 being non empty Subset of (L .:) holds
( D1 "\/" D2 = (D1 .:) "/\" (D2 .:) & (D1 .:) "\/" (D2 .:) = D1 "/\" D2 & D19 "\/" D29 = (.: D19) "/\" (.: D29) & (.: D19) "\/" (.: D29) = D19 "/\" D29 )
proof
let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L
for D19, D29 being non empty Subset of (L .:) holds
( D1 "\/" D2 = (D1 .:) "/\" (D2 .:) & (D1 .:) "\/" (D2 .:) = D1 "/\" D2 & D19 "\/" D29 = (.: D19) "/\" (.: D29) & (.: D19) "\/" (.: D29) = D19 "/\" D29 )
let D1, D2 be non empty Subset of L; ::_thesis: for D19, D29 being non empty Subset of (L .:) holds
( D1 "\/" D2 = (D1 .:) "/\" (D2 .:) & (D1 .:) "\/" (D2 .:) = D1 "/\" D2 & D19 "\/" D29 = (.: D19) "/\" (.: D29) & (.: D19) "\/" (.: D29) = D19 "/\" D29 )
let D19, D29 be non empty Subset of (L .:); ::_thesis: ( D1 "\/" D2 = (D1 .:) "/\" (D2 .:) & (D1 .:) "\/" (D2 .:) = D1 "/\" D2 & D19 "\/" D29 = (.: D19) "/\" (.: D29) & (.: D19) "\/" (.: D29) = D19 "/\" D29 )
A1: for L being Lattice
for D1, D2 being non empty Subset of L holds D1 "\/" D2 = (D1 .:) "/\" (D2 .:)
proof
let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L holds D1 "\/" D2 = (D1 .:) "/\" (D2 .:)
let D1, D2 be non empty Subset of L; ::_thesis: D1 "\/" D2 = (D1 .:) "/\" (D2 .:)
thus D1 "\/" D2 c= (D1 .:) "/\" (D2 .:) :: according to XBOOLE_0:def_10 ::_thesis: (D1 .:) "/\" (D2 .:) c= D1 "\/" D2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 "\/" D2 or x in (D1 .:) "/\" (D2 .:) )
assume x in D1 "\/" D2 ; ::_thesis: x in (D1 .:) "/\" (D2 .:)
then consider p, q being Element of L such that
A2: ( x = p "\/" q & p in D1 & q in D2 ) ;
p "\/" q = (p .:) "/\" (q .:) ;
hence x in (D1 .:) "/\" (D2 .:) by A2; ::_thesis: verum
end;
thus (D1 .:) "/\" (D2 .:) c= D1 "\/" D2 ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (D1 .:) "/\" (D2 .:) or x in D1 "\/" D2 )
assume x in (D1 .:) "/\" (D2 .:) ; ::_thesis: x in D1 "\/" D2
then consider p9, q9 being Element of (L .:) such that
A3: ( x = p9 "/\" q9 & p9 in D1 & q9 in D2 ) ;
(.: p9) "\/" (.: q9) = p9 "/\" q9 ;
hence x in D1 "\/" D2 by A3; ::_thesis: verum
end;
end;
A4: ( (.: D19) .: = .: D19 & (.: D29) .: = .: D29 ) ;
( ((D1 .:) .:) "/\" ((D2 .:) .:) = D1 "/\" D2 & (D19 .:) "/\" (D29 .:) = (.: D19) "/\" (.: D29) ) by Lm3;
hence ( D1 "\/" D2 = (D1 .:) "/\" (D2 .:) & (D1 .:) "\/" (D2 .:) = D1 "/\" D2 & D19 "\/" D29 = (.: D19) "/\" (.: D29) & (.: D19) "\/" (.: D29) = D19 "/\" D29 ) by A1, A4; ::_thesis: verum
end;
theorem :: FILTER_2:45
for L being Lattice
for p, q being Element of L
for D1, D2 being non empty Subset of L st p in D1 & q in D2 holds
( p "\/" q in D1 "\/" D2 & q "\/" p in D1 "\/" D2 ) ;
theorem :: FILTER_2:46
for L being Lattice
for x being set
for D1, D2 being non empty Subset of L st x in D1 "\/" D2 holds
ex p, q being Element of L st
( x = p "\/" q & p in D1 & q in D2 ) ;
theorem :: FILTER_2:47
for L being Lattice
for D1, D2 being non empty Subset of L holds D1 "\/" D2 = D2 "\/" D1
proof
let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L holds D1 "\/" D2 = D2 "\/" D1
let D1, D2 be non empty Subset of L; ::_thesis: D1 "\/" D2 = D2 "\/" D1
let r be Element of L; :: according to FILTER_2:def_1 ::_thesis: ( r in D1 "\/" D2 iff r in D2 "\/" D1 )
thus ( r in D1 "\/" D2 implies r in D2 "\/" D1 ) ::_thesis: ( r in D2 "\/" D1 implies r in D1 "\/" D2 )
proof
assume r in D1 "\/" D2 ; ::_thesis: r in D2 "\/" D1
then ex p, q being Element of L st
( r = p "\/" q & p in D1 & q in D2 ) ;
hence r in D2 "\/" D1 ; ::_thesis: verum
end;
assume r in D2 "\/" D1 ; ::_thesis: r in D1 "\/" D2
then ex p, q being Element of L st
( r = p "\/" q & p in D2 & q in D1 ) ;
hence r in D1 "\/" D2 ; ::_thesis: verum
end;
registration
let L be D_Lattice;
let I1, I2 be Ideal of L;
clusterI1 "\/" I2 -> initial join-closed ;
coherence
( I1 "\/" I2 is initial & I1 "\/" I2 is join-closed )
proof
reconsider K = L .: as D_Lattice by LATTICE2:50;
reconsider J1 = I1 .: , J2 = I2 .: as Filter of K ;
( I1 "\/" I2 = (I1 .:) "/\" (I2 .:) & J1 "/\" J2 = (J1 "/\" J2) .: ) by Th44;
hence ( I1 "\/" I2 is initial & I1 "\/" I2 is join-closed ) by Th16; ::_thesis: verum
end;
end;
theorem :: FILTER_2:48
for L being Lattice
for D1, D2 being non empty Subset of L holds
( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> )
proof
let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L holds
( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> )
let D1, D2 be non empty Subset of L; ::_thesis: ( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> )
A1: ( (.(D1 \/ (.D2.>).> = <.((D1 \/ (.D2.>) .:).) & (.D2.> = <.(D2 .:).) ) by Th36;
A2: (.(D1 \/ D2).> = <.((D1 \/ D2) .:).) by Th36;
( (.((.D1.> \/ D2).> = <.(((.D1.> \/ D2) .:).) & (.D1.> = <.(D1 .:).) ) by Th36;
hence ( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> ) by A1, A2, FILTER_0:34; ::_thesis: verum
end;
theorem :: FILTER_2:49
for L being Lattice
for I, J being Ideal of L holds (.(I \/ J).> = { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) }
proof
let L be Lattice; ::_thesis: for I, J being Ideal of L holds (.(I \/ J).> = { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) }
let I, J be Ideal of L; ::_thesis: (.(I \/ J).> = { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) }
A1: J .: = J ;
( (.(I \/ J).> = <.((I \/ J) .:).) & I .: = I ) by Th36;
then A2: (.(I \/ J).> = { r9 where r9 is Element of (L .:) : ex p9, q9 being Element of (L .:) st
( p9 "/\" q9 [= r9 & p9 in I & q9 in J ) } by A1, FILTER_0:35;
thus (.(I \/ J).> c= { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) } :: according to XBOOLE_0:def_10 ::_thesis: { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) } c= (.(I \/ J).>
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (.(I \/ J).> or x in { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) } )
assume x in (.(I \/ J).> ; ::_thesis: x in { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) }
then consider r9 being Element of (L .:) such that
A3: x = r9 and
A4: ex p9, q9 being Element of (L .:) st
( p9 "/\" q9 [= r9 & p9 in I & q9 in J ) by A2;
consider p9, q9 being Element of (L .:) such that
A5: p9 "/\" q9 [= r9 and
A6: ( p9 in I & q9 in J ) by A4;
A7: p9 "/\" q9 = (.: p9) "\/" (.: q9) ;
.: r9 [= .: (p9 "/\" q9) by A5, LATTICE2:39;
hence x in { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) } by A3, A6, A7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) } or x in (.(I \/ J).> )
assume x in { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) } ; ::_thesis: x in (.(I \/ J).>
then consider r being Element of L such that
A8: x = r and
A9: ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) ;
consider p, q being Element of L such that
A10: r [= p "\/" q and
A11: ( p in I & q in J ) by A9;
A12: p "\/" q = (p .:) "/\" (q .:) ;
(p "\/" q) .: [= r .: by A10, LATTICE2:38;
hence x in (.(I \/ J).> by A2, A8, A11, A12; ::_thesis: verum
end;
theorem :: FILTER_2:50
for L being Lattice
for I, J being Ideal of L holds
( I c= I "\/" J & J c= I "\/" J )
proof
let L be Lattice; ::_thesis: for I, J being Ideal of L holds
( I c= I "\/" J & J c= I "\/" J )
let I, J be Ideal of L; ::_thesis: ( I c= I "\/" J & J c= I "\/" J )
I "\/" J = (I .:) "/\" (J .:) by Th44;
hence ( I c= I "\/" J & J c= I "\/" J ) by FILTER_0:36; ::_thesis: verum
end;
theorem :: FILTER_2:51
for L being Lattice
for I, J being Ideal of L holds (.(I \/ J).> = (.(I "\/" J).>
proof
let L be Lattice; ::_thesis: for I, J being Ideal of L holds (.(I \/ J).> = (.(I "\/" J).>
let I, J be Ideal of L; ::_thesis: (.(I \/ J).> = (.(I "\/" J).>
A1: (.(I "\/" J).> = <.((I "\/" J) .:).) by Th36;
( (.(I \/ J).> = <.((I \/ J) .:).) & (I .:) "/\" (J .:) = I "\/" J ) by Th36, Th44;
hence (.(I \/ J).> = (.(I "\/" J).> by A1, FILTER_0:37; ::_thesis: verum
end;
theorem Th52: :: FILTER_2:52
for L being Lattice holds
( L is C_Lattice iff L .: is C_Lattice )
proof
let L be Lattice; ::_thesis: ( L is C_Lattice iff L .: is C_Lattice )
A1: ( L is upper-bounded iff L .: is lower-bounded ) by LATTICE2:49;
A2: ( L is lower-bounded iff L .: is upper-bounded ) by LATTICE2:48;
thus ( L is C_Lattice implies L .: is C_Lattice ) ::_thesis: ( L .: is C_Lattice implies L is C_Lattice )
proof
assume A3: L is C_Lattice ; ::_thesis: L .: is C_Lattice
now__::_thesis:_for_p9_being_Element_of_(L_.:)_ex_r_being_Element_of_(L_.:)_st_r_is_a_complement_of_p9
let p9 be Element of (L .:); ::_thesis: ex r being Element of (L .:) st r is_a_complement_of p9
consider q being Element of L such that
A4: q is_a_complement_of .: p9 by A3, LATTICES:def_19;
take r = q .: ; ::_thesis: r is_a_complement_of p9
q "\/" (.: p9) = Top L by A4, LATTICES:def_18;
then A5: (q .:) "/\" p9 = Top L ;
q "/\" (.: p9) = Bottom L by A4, LATTICES:def_18;
then A6: (q .:) "\/" p9 = Bottom L ;
( Top (L .:) = Bottom L & Bottom (L .:) = Top L ) by A3, LATTICE2:61, LATTICE2:62;
hence r is_a_complement_of p9 by A5, A6, LATTICES:def_18; ::_thesis: verum
end;
hence L .: is C_Lattice by A2, A1, A3, LATTICES:def_19; ::_thesis: verum
end;
assume A7: L .: is C_Lattice ; ::_thesis: L is C_Lattice
now__::_thesis:_for_p_being_Element_of_L_ex_r_being_Element_of_L_st_r_is_a_complement_of_p
let p be Element of L; ::_thesis: ex r being Element of L st r is_a_complement_of p
consider q9 being Element of (L .:) such that
A8: q9 is_a_complement_of p .: by A7, LATTICES:def_19;
q9 "\/" (p .:) = Top (L .:) by A8, LATTICES:def_18;
then A9: (.: q9) "/\" p = Top (L .:) ;
take r = .: q9; ::_thesis: r is_a_complement_of p
L is upper-bounded by A7, LATTICE2:49;
then A10: Bottom (L .:) = Top L by LATTICE2:62;
q9 "/\" (p .:) = Bottom (L .:) by A8, LATTICES:def_18;
then A11: (.: q9) "\/" p = Bottom (L .:) ;
L is lower-bounded by A7, LATTICE2:48;
then Top (L .:) = Bottom L by LATTICE2:61;
hence r is_a_complement_of p by A9, A11, A10, LATTICES:def_18; ::_thesis: verum
end;
hence L is C_Lattice by A2, A1, A7, LATTICES:def_19; ::_thesis: verum
end;
theorem Th53: :: FILTER_2:53
for L being Lattice holds
( L is B_Lattice iff L .: is B_Lattice )
proof
let L be Lattice; ::_thesis: ( L is B_Lattice iff L .: is B_Lattice )
A1: ( L is distributive iff L .: is distributive ) by LATTICE2:50;
( L is C_Lattice iff L .: is C_Lattice ) by Th52;
hence ( L is B_Lattice iff L .: is B_Lattice ) by A1; ::_thesis: verum
end;
registration
let B be B_Lattice;
clusterB .: -> Lattice-like Boolean ;
coherence
( B .: is Boolean & B .: is Lattice-like ) by Th53;
end;
Lm4: for B being B_Lattice
for a being Element of B holds (a .:) ` = a `
proof
let B be B_Lattice; ::_thesis: for a being Element of B holds (a .:) ` = a `
let a be Element of B; ::_thesis: (a .:) ` = a `
((a .:) `) "/\" (a .:) = Bottom (B .:) by LATTICES:20;
then A1: (.: ((a .:) `)) "\/" (.: (a .:)) = Top B by LATTICE2:62;
((a .:) `) "\/" (a .:) = Top (B .:) by LATTICES:21;
then (.: ((a .:) `)) "/\" (.: (a .:)) = Bottom B by LATTICE2:61;
then .: ((a .:) `) is_a_complement_of a by A1, LATTICES:def_18;
hence (a .:) ` = a ` by LATTICES:def_21; ::_thesis: verum
end;
theorem Th54: :: FILTER_2:54
for B being B_Lattice
for a being Element of B
for a9 being Element of (B .:) holds
( (a .:) ` = a ` & (.: a9) ` = a9 ` )
proof
let B be B_Lattice; ::_thesis: for a being Element of B
for a9 being Element of (B .:) holds
( (a .:) ` = a ` & (.: a9) ` = a9 ` )
let a be Element of B; ::_thesis: for a9 being Element of (B .:) holds
( (a .:) ` = a ` & (.: a9) ` = a9 ` )
let a9 be Element of (B .:); ::_thesis: ( (a .:) ` = a ` & (.: a9) ` = a9 ` )
(.: a9) .: = .: a9 ;
hence ( (a .:) ` = a ` & (.: a9) ` = a9 ` ) by Lm4; ::_thesis: verum
end;
theorem :: FILTER_2:55
for B being B_Lattice
for IB, JB being Ideal of B holds (.(IB \/ JB).> = IB "\/" JB
proof
let B be B_Lattice; ::_thesis: for IB, JB being Ideal of B holds (.(IB \/ JB).> = IB "\/" JB
let IB, JB be Ideal of B; ::_thesis: (.(IB \/ JB).> = IB "\/" JB
reconsider FB = IB .: , GB = JB .: as Filter of (B .:) ;
thus (.(IB \/ JB).> = <.((IB \/ JB) .:).) by Th36
.= FB "/\" GB by FILTER_0:39
.= IB "\/" JB by Th44 ; ::_thesis: verum
end;
theorem :: FILTER_2:56
for B being B_Lattice
for IB being Ideal of B holds
( IB is_max-ideal iff ( IB <> the carrier of B & ( for a being Element of B holds
( a in IB or a ` in IB ) ) ) )
proof
let B be B_Lattice; ::_thesis: for IB being Ideal of B holds
( IB is_max-ideal iff ( IB <> the carrier of B & ( for a being Element of B holds
( a in IB or a ` in IB ) ) ) )
let IB be Ideal of B; ::_thesis: ( IB is_max-ideal iff ( IB <> the carrier of B & ( for a being Element of B holds
( a in IB or a ` in IB ) ) ) )
reconsider FB = IB .: as Filter of (B .:) ;
A1: ( FB is being_ultrafilter iff ( FB <> H1(B .: ) & ( for a being Element of (B .:) holds
( a in FB or a ` in FB ) ) ) ) by FILTER_0:44;
thus ( IB is_max-ideal implies ( IB <> H1(B) & ( for a being Element of B holds
( a in IB or a ` in IB ) ) ) ) ::_thesis: ( IB <> the carrier of B & ( for a being Element of B holds
( a in IB or a ` in IB ) ) implies IB is_max-ideal )
proof
assume A2: IB is_max-ideal ; ::_thesis: ( IB <> H1(B) & ( for a being Element of B holds
( a in IB or a ` in IB ) ) )
hence IB <> H1(B) by A1, Th32; ::_thesis: for a being Element of B holds
( a in IB or a ` in IB )
let a be Element of B; ::_thesis: ( a in IB or a ` in IB )
reconsider b = a as Element of (B .:) ;
( b in FB or ( b ` in FB & (a .:) ` = a ` ) ) by A1, A2, Th32, Th54;
hence ( a in IB or a ` in IB ) ; ::_thesis: verum
end;
assume that
A3: IB <> H1(B) and
A4: for a being Element of B holds
( a in IB or a ` in IB ) ; ::_thesis: IB is_max-ideal
now__::_thesis:_for_a_being_Element_of_(B_.:)_holds_
(_a_in_FB_or_a_`_in_FB_)
let a be Element of (B .:); ::_thesis: ( a in FB or a ` in FB )
reconsider b = a as Element of B ;
( b in FB or ( b ` in FB & (.: a) ` = a ` ) ) by A4, Th54;
hence ( a in FB or a ` in FB ) ; ::_thesis: verum
end;
hence IB is_max-ideal by A1, A3, Th32; ::_thesis: verum
end;
theorem :: FILTER_2:57
for B being B_Lattice
for IB being Ideal of B holds
( ( IB <> (.B.> & IB is prime ) iff IB is_max-ideal )
proof
let B be B_Lattice; ::_thesis: for IB being Ideal of B holds
( ( IB <> (.B.> & IB is prime ) iff IB is_max-ideal )
let IB be Ideal of B; ::_thesis: ( ( IB <> (.B.> & IB is prime ) iff IB is_max-ideal )
reconsider F = IB .: as Filter of (B .:) ;
<.(B .:).) = (.B.> ;
then ( ( F <> (.B.> & F is prime ) iff F is being_ultrafilter ) by FILTER_0:45;
hence ( ( IB <> (.B.> & IB is prime ) iff IB is_max-ideal ) by Th32, Th43; ::_thesis: verum
end;
theorem :: FILTER_2:58
for B being B_Lattice
for IB being Ideal of B st IB is_max-ideal holds
for a being Element of B holds
( a in IB iff not a ` in IB )
proof
let B be B_Lattice; ::_thesis: for IB being Ideal of B st IB is_max-ideal holds
for a being Element of B holds
( a in IB iff not a ` in IB )
let IB be Ideal of B; ::_thesis: ( IB is_max-ideal implies for a being Element of B holds
( a in IB iff not a ` in IB ) )
reconsider FB = IB .: as Filter of (B .:) ;
assume IB is_max-ideal ; ::_thesis: for a being Element of B holds
( a in IB iff not a ` in IB )
then A1: FB is being_ultrafilter by Th32;
let a be Element of B; ::_thesis: ( a in IB iff not a ` in IB )
(a .:) ` = a ` by Lm4;
hence ( a in IB iff not a ` in IB ) by A1, FILTER_0:46; ::_thesis: verum
end;
theorem :: FILTER_2:59
for B being B_Lattice
for a, b being Element of B st a <> b holds
ex IB being Ideal of B st
( IB is_max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) )
proof
let B be B_Lattice; ::_thesis: for a, b being Element of B st a <> b holds
ex IB being Ideal of B st
( IB is_max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) )
let a, b be Element of B; ::_thesis: ( a <> b implies ex IB being Ideal of B st
( IB is_max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) ) )
assume a <> b ; ::_thesis: ex IB being Ideal of B st
( IB is_max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) )
then consider FB being Filter of (B .:) such that
A1: FB is being_ultrafilter and
A2: ( ( a .: in FB & not b .: in FB ) or ( not a .: in FB & b .: in FB ) ) by FILTER_0:47;
take IB = .: FB; ::_thesis: ( IB is_max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) )
IB .: = FB ;
hence IB is_max-ideal by A1, Th32; ::_thesis: ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) )
thus ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) by A2; ::_thesis: verum
end;
theorem Th60: :: FILTER_2:60
for L being Lattice
for P being non empty ClosedSubset of L holds
( the L_join of L || P is BinOp of P & the L_meet of L || P is BinOp of P )
proof
let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L holds
( the L_join of L || P is BinOp of P & the L_meet of L || P is BinOp of P )
let P be non empty ClosedSubset of L; ::_thesis: ( the L_join of L || P is BinOp of P & the L_meet of L || P is BinOp of P )
dom H2(L) = [:H1(L),H1(L):] by FUNCT_2:def_1;
then A1: dom (H2(L) || P) = [:P,P:] by RELAT_1:62;
rng (H2(L) || P) c= P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (H2(L) || P) or x in P )
assume x in rng (H2(L) || P) ; ::_thesis: x in P
then consider y being set such that
A2: y in [:P,P:] and
A3: x = (H2(L) || P) . y by A1, FUNCT_1:def_3;
consider p1, p2 being Element of P such that
A4: y = [p1,p2] by A2, DOMAIN_1:1;
x = p1 "\/" p2 by A1, A3, A4, FUNCT_1:47;
hence x in P by LATTICES:def_25; ::_thesis: verum
end;
hence H2(L) || P is BinOp of P by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: the L_meet of L || P is BinOp of P
dom H3(L) = [:H1(L),H1(L):] by FUNCT_2:def_1;
then A5: dom (H3(L) || P) = [:P,P:] by RELAT_1:62;
rng (H3(L) || P) c= P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (H3(L) || P) or x in P )
assume x in rng (H3(L) || P) ; ::_thesis: x in P
then consider y being set such that
A6: y in [:P,P:] and
A7: x = (H3(L) || P) . y by A5, FUNCT_1:def_3;
consider p1, p2 being Element of P such that
A8: y = [p1,p2] by A6, DOMAIN_1:1;
x = p1 "/\" p2 by A5, A7, A8, FUNCT_1:47;
hence x in P by LATTICES:def_24; ::_thesis: verum
end;
hence the L_meet of L || P is BinOp of P by A5, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
theorem Th61: :: FILTER_2:61
for L being Lattice
for P being non empty ClosedSubset of L
for o1, o2 being BinOp of P st o1 = the L_join of L || P & o2 = the L_meet of L || P holds
( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 )
proof
let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L
for o1, o2 being BinOp of P st o1 = the L_join of L || P & o2 = the L_meet of L || P holds
( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 )
let P be non empty ClosedSubset of L; ::_thesis: for o1, o2 being BinOp of P st o1 = the L_join of L || P & o2 = the L_meet of L || P holds
( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 )
let o1, o2 be BinOp of P; ::_thesis: ( o1 = the L_join of L || P & o2 = the L_meet of L || P implies ( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 ) )
( H2(L) absorbs H3(L) & H3(L) absorbs H2(L) ) by LATTICE2:26, LATTICE2:27;
hence ( o1 = the L_join of L || P & o2 = the L_meet of L || P implies ( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 ) ) by Th1, Th5; ::_thesis: verum
end;
definition
let L be Lattice;
let p, q be Element of L;
assume A1: p [= q ;
func[#p,q#] -> non empty ClosedSubset of L equals :Def12: :: FILTER_2:def 12
{ r where r is Element of L : ( p [= r & r [= q ) } ;
coherence
{ r where r is Element of L : ( p [= r & r [= q ) } is non empty ClosedSubset of L
proof
set P = { r where r is Element of L : ( p [= r & r [= q ) } ;
p in { r where r is Element of L : ( p [= r & r [= q ) } by A1;
then reconsider P = { r where r is Element of L : ( p [= r & r [= q ) } as non empty set ;
P c= H1(L)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in H1(L) )
assume x in P ; ::_thesis: x in H1(L)
then ex r being Element of L st
( x = r & p [= r & r [= q ) ;
hence x in H1(L) ; ::_thesis: verum
end;
then reconsider P = P as non empty Subset of L ;
now__::_thesis:_for_p1,_p2_being_Element_of_L_st_p1_in_P_&_p2_in_P_holds_
(_p1_"/\"_p2_in_P_&_p1_"\/"_p2_in_P_)
let p1, p2 be Element of L; ::_thesis: ( p1 in P & p2 in P implies ( p1 "/\" p2 in P & p1 "\/" p2 in P ) )
assume that
A2: p1 in P and
A3: p2 in P ; ::_thesis: ( p1 "/\" p2 in P & p1 "\/" p2 in P )
A4: ex r being Element of L st
( p1 = r & p [= r & r [= q ) by A2;
then A5: ( p [= p1 "\/" p2 & p1 "/\" p2 [= q ) by FILTER_0:2, FILTER_0:3;
ex r being Element of L st
( p2 = r & p [= r & r [= q ) by A3;
then ( p [= p1 "/\" p2 & p1 "\/" p2 [= q ) by A4, FILTER_0:6, FILTER_0:7;
hence ( p1 "/\" p2 in P & p1 "\/" p2 in P ) by A5; ::_thesis: verum
end;
then ( ( for p1, p2 being Element of L st p1 in P & p2 in P holds
p1 "/\" p2 in P ) & ( for p1, p2 being Element of L st p1 in P & p2 in P holds
p1 "\/" p2 in P ) ) ;
hence { r where r is Element of L : ( p [= r & r [= q ) } is non empty ClosedSubset of L by LATTICES:def_24, LATTICES:def_25; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines [# FILTER_2:def_12_:_
for L being Lattice
for p, q being Element of L st p [= q holds
[#p,q#] = { r where r is Element of L : ( p [= r & r [= q ) } ;
theorem Th62: :: FILTER_2:62
for L being Lattice
for p, q, r being Element of L st p [= q holds
( r in [#p,q#] iff ( p [= r & r [= q ) )
proof
let L be Lattice; ::_thesis: for p, q, r being Element of L st p [= q holds
( r in [#p,q#] iff ( p [= r & r [= q ) )
let p, q, r be Element of L; ::_thesis: ( p [= q implies ( r in [#p,q#] iff ( p [= r & r [= q ) ) )
assume p [= q ; ::_thesis: ( r in [#p,q#] iff ( p [= r & r [= q ) )
then [#p,q#] = { s where s is Element of L : ( p [= s & s [= q ) } by Def12;
then ( r in [#p,q#] iff ex s being Element of L st
( r = s & p [= s & s [= q ) ) ;
hence ( r in [#p,q#] iff ( p [= r & r [= q ) ) ; ::_thesis: verum
end;
theorem :: FILTER_2:63
for L being Lattice
for p, q being Element of L st p [= q holds
( p in [#p,q#] & q in [#p,q#] ) by Th62;
theorem :: FILTER_2:64
for L being Lattice
for p being Element of L holds [#p,p#] = {p}
proof
let L be Lattice; ::_thesis: for p being Element of L holds [#p,p#] = {p}
let p be Element of L; ::_thesis: [#p,p#] = {p}
let q be Element of L; :: according to FILTER_2:def_1 ::_thesis: ( q in [#p,p#] iff q in {p} )
hereby ::_thesis: ( q in {p} implies q in [#p,p#] )
assume q in [#p,p#] ; ::_thesis: q in {p}
then ( p [= q & q [= p ) by Th62;
then q = p by LATTICES:8;
hence q in {p} by TARSKI:def_1; ::_thesis: verum
end;
p in [#p,p#] by Th62;
hence ( q in {p} implies q in [#p,p#] ) by TARSKI:def_1; ::_thesis: verum
end;
theorem :: FILTER_2:65
for L being Lattice
for p being Element of L st L is upper-bounded holds
<.p.) = [#p,(Top L)#]
proof
let L be Lattice; ::_thesis: for p being Element of L st L is upper-bounded holds
<.p.) = [#p,(Top L)#]
let p be Element of L; ::_thesis: ( L is upper-bounded implies <.p.) = [#p,(Top L)#] )
assume A1: L is upper-bounded ; ::_thesis: <.p.) = [#p,(Top L)#]
let q be Element of L; :: according to FILTER_2:def_1 ::_thesis: ( q in <.p.) iff q in [#p,(Top L)#] )
A2: ( q in <.p.) iff p [= q ) by FILTER_0:15;
( p [= Top L & q [= Top L ) by A1, LATTICES:19;
hence ( q in <.p.) iff q in [#p,(Top L)#] ) by A2, Th62; ::_thesis: verum
end;
theorem :: FILTER_2:66
for L being Lattice
for p being Element of L st L is lower-bounded holds
(.p.> = [#(Bottom L),p#]
proof
let L be Lattice; ::_thesis: for p being Element of L st L is lower-bounded holds
(.p.> = [#(Bottom L),p#]
let p be Element of L; ::_thesis: ( L is lower-bounded implies (.p.> = [#(Bottom L),p#] )
assume A1: L is lower-bounded ; ::_thesis: (.p.> = [#(Bottom L),p#]
let q be Element of L; :: according to FILTER_2:def_1 ::_thesis: ( q in (.p.> iff q in [#(Bottom L),p#] )
A2: ( q in (.p.> iff q [= p ) by Th28;
( Bottom L [= p & Bottom L [= q ) by A1, LATTICES:16;
hence ( q in (.p.> iff q in [#(Bottom L),p#] ) by A2, Th62; ::_thesis: verum
end;
theorem :: FILTER_2:67
for L1, L2 being Lattice
for F1 being Filter of L1
for F2 being Filter of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 holds
latt F1 = latt F2
proof
let L1, L2 be Lattice; ::_thesis: for F1 being Filter of L1
for F2 being Filter of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 holds
latt F1 = latt F2
let F1 be Filter of L1; ::_thesis: for F2 being Filter of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 holds
latt F1 = latt F2
let F2 be Filter of L2; ::_thesis: ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 implies latt F1 = latt F2 )
ex o1, o2 being BinOp of F1 st
( o1 = the L_join of L1 || F1 & o2 = the L_meet of L1 || F1 & latt F1 = LattStr(# F1,o1,o2 #) ) by FILTER_0:def_9;
hence ( LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 implies latt F1 = latt F2 ) by FILTER_0:def_9; ::_thesis: verum
end;
begin
notation
let L be Lattice;
synonym Sublattice of L for SubLattice of L;
end;
definition
let L be Lattice;
redefine mode SubLattice of L means :Def13: :: FILTER_2:def 13
ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of it, the L_join of it, the L_meet of it #) = LattStr(# P,o1,o2 #) );
compatibility
for b1 being LattStr holds
( b1 is Sublattice of L iff ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of b1, the L_join of b1, the L_meet of b1 #) = LattStr(# P,o1,o2 #) ) )
proof
let K be Lattice; ::_thesis: ( K is Sublattice of L iff ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) )
thus ( K is SubLattice of L implies ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) ) ::_thesis: ( ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) implies K is Sublattice of L )
proof
assume A1: K is SubLattice of L ; ::_thesis: ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) )
then A2: H3(K) = H3(L) || H1(K) by NAT_LAT:def_12;
reconsider P = H1(K) as non empty Subset of L by A1, NAT_LAT:def_12;
A3: H2(K) = H2(L) || H1(K) by A1, NAT_LAT:def_12;
now__::_thesis:_for_p,_q_being_Element_of_L_st_p_in_P_&_q_in_P_holds_
(_p_"/\"_q_in_P_&_p_"\/"_q_in_P_)
let p, q be Element of L; ::_thesis: ( p in P & q in P implies ( p "/\" q in P & p "\/" q in P ) )
assume ( p in P & q in P ) ; ::_thesis: ( p "/\" q in P & p "\/" q in P )
then A4: [p,q] in [:P,P:] by ZFMISC_1:87;
dom H3(K) = [:P,P:] by FUNCT_2:def_1;
then A5: H3(L) . [p,q] = H3(K) . [p,q] by A2, A4, FUNCT_1:47;
dom H2(K) = [:P,P:] by FUNCT_2:def_1;
then H2(L) . [p,q] = H2(K) . [p,q] by A3, A4, FUNCT_1:47;
hence ( p "/\" q in P & p "\/" q in P ) by A4, A5, FUNCT_2:5; ::_thesis: verum
end;
then ( ( for p1, p2 being Element of L st p1 in P & p2 in P holds
p1 "/\" p2 in P ) & ( for p1, p2 being Element of L st p1 in P & p2 in P holds
p1 "\/" p2 in P ) ) ;
then reconsider P = P as non empty ClosedSubset of L by LATTICES:def_24, LATTICES:def_25;
take P ; ::_thesis: ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) )
reconsider o1 = H2(K), o2 = H3(K) as BinOp of P ;
take o1 ; ::_thesis: ex o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) )
take o2 ; ::_thesis: ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) )
thus ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) by A1, NAT_LAT:def_12; ::_thesis: verum
end;
given P being non empty ClosedSubset of L, o1, o2 being BinOp of P such that A6: ( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# P,o1,o2 #) ) ; ::_thesis: K is Sublattice of L
thus K is Sublattice of L by A6, NAT_LAT:def_12; ::_thesis: verum
end;
end;
:: deftheorem Def13 defines Sublattice FILTER_2:def_13_:_
for L being Lattice
for b2 being LattStr holds
( b2 is Sublattice of L iff ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of b2, the L_join of b2, the L_meet of b2 #) = LattStr(# P,o1,o2 #) ) );
theorem Th68: :: FILTER_2:68
for L being Lattice
for K being Sublattice of L
for a being Element of K holds a is Element of L
proof
let L be Lattice; ::_thesis: for K being Sublattice of L
for a being Element of K holds a is Element of L
let K be Sublattice of L; ::_thesis: for a being Element of K holds a is Element of L
H1(K) c= H1(L) by NAT_LAT:def_12;
hence for a being Element of K holds a is Element of L by TARSKI:def_3; ::_thesis: verum
end;
definition
let L be Lattice;
let P be non empty ClosedSubset of L;
func latt (L,P) -> Sublattice of L means :Def14: :: FILTER_2:def 14
ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & it = LattStr(# P,o1,o2 #) );
existence
ex b1 being Sublattice of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & b1 = LattStr(# P,o1,o2 #) )
proof
reconsider o1 = H2(L) || P, o2 = H3(L) || P as BinOp of P by Th60;
o1 = H2(L) || P ;
then A1: ( o2 is commutative & o2 is associative ) by Th61;
o2 = H3(L) || P ;
then A2: ( o1 is commutative & o1 is associative ) by Th61;
( o1 absorbs o2 & o2 absorbs o1 ) by Th61;
then reconsider K = LattStr(# P,o1,o2 #) as strict Lattice by A2, A1, LATTICE2:11;
reconsider K = K as strict Sublattice of L by NAT_LAT:def_12;
take K ; ::_thesis: ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & K = LattStr(# P,o1,o2 #) )
take o1 ; ::_thesis: ex o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & K = LattStr(# P,o1,o2 #) )
take o2 ; ::_thesis: ( o1 = the L_join of L || P & o2 = the L_meet of L || P & K = LattStr(# P,o1,o2 #) )
thus ( o1 = the L_join of L || P & o2 = the L_meet of L || P & K = LattStr(# P,o1,o2 #) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Sublattice of L st ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & b1 = LattStr(# P,o1,o2 #) ) & ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & b2 = LattStr(# P,o1,o2 #) ) holds
b1 = b2 ;
end;
:: deftheorem Def14 defines latt FILTER_2:def_14_:_
for L being Lattice
for P being non empty ClosedSubset of L
for b3 being Sublattice of L holds
( b3 = latt (L,P) iff ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & b3 = LattStr(# P,o1,o2 #) ) );
registration
let L be Lattice;
let P be non empty ClosedSubset of L;
cluster latt (L,P) -> strict ;
coherence
latt (L,P) is strict
proof
ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & latt (L,P) = LattStr(# P,o1,o2 #) ) by Def14;
hence latt (L,P) is strict ; ::_thesis: verum
end;
end;
definition
let L be Lattice;
let l be Sublattice of L;
:: original: .:
redefine funcl .: -> strict Sublattice of L .: ;
coherence
l .: is strict Sublattice of L .:
proof
consider P being non empty ClosedSubset of L, o1, o2 being BinOp of P such that
A1: ( o1 = H2(L) || P & o2 = H3(L) || P & LattStr(# the carrier of l, the L_join of l, the L_meet of l #) = LattStr(# P,o1,o2 #) ) by Def13;
l .: is Sublattice of L .:
proof
take P .: ; :: according to FILTER_2:def_13 ::_thesis: ex o1, o2 being BinOp of (P .:) st
( o1 = the L_join of (L .:) || (P .:) & o2 = the L_meet of (L .:) || (P .:) & LattStr(# the carrier of (l .:), the L_join of (l .:), the L_meet of (l .:) #) = LattStr(# (P .:),o1,o2 #) )
thus ex o1, o2 being BinOp of (P .:) st
( o1 = the L_join of (L .:) || (P .:) & o2 = the L_meet of (L .:) || (P .:) & LattStr(# the carrier of (l .:), the L_join of (l .:), the L_meet of (l .:) #) = LattStr(# (P .:),o1,o2 #) ) by A1; ::_thesis: verum
end;
hence l .: is strict Sublattice of L .: ; ::_thesis: verum
end;
end;
theorem Th69: :: FILTER_2:69
for L being Lattice
for F being Filter of L holds latt F = latt (L,F)
proof
let L be Lattice; ::_thesis: for F being Filter of L holds latt F = latt (L,F)
let F be Filter of L; ::_thesis: latt F = latt (L,F)
ex o1, o2 being BinOp of F st
( o1 = H2(L) || F & o2 = H3(L) || F & latt (L,F) = LattStr(# F,o1,o2 #) ) by Def14;
hence latt F = latt (L,F) by FILTER_0:def_9; ::_thesis: verum
end;
theorem Th70: :: FILTER_2:70
for L being Lattice
for P being non empty ClosedSubset of L holds latt (L,P) = (latt ((L .:),(P .:))) .:
proof
let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L holds latt (L,P) = (latt ((L .:),(P .:))) .:
let P be non empty ClosedSubset of L; ::_thesis: latt (L,P) = (latt ((L .:),(P .:))) .:
( ex o1, o2 being BinOp of P st
( o1 = H2(L) || P & o2 = H3(L) || P & latt (L,P) = LattStr(# P,o1,o2 #) ) & ex o3, o4 being BinOp of (P .:) st
( o3 = H2(L .: ) || (P .:) & o4 = H3(L .: ) || (P .:) & latt ((L .:),(P .:)) = LattStr(# (P .:),o3,o4 #) ) ) by Def14;
hence latt (L,P) = (latt ((L .:),(P .:))) .: ; ::_thesis: verum
end;
theorem :: FILTER_2:71
for L being Lattice holds
( latt (L,(.L.>) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & latt (L,<.L.)) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) )
proof
let L be Lattice; ::_thesis: ( latt (L,(.L.>) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & latt (L,<.L.)) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) )
A1: ( dom H3(L) = [:H1(L),H1(L):] & H2(L) | (dom H2(L)) = H2(L) ) by FUNCT_2:def_1, RELAT_1:68;
( ex o1, o2 being BinOp of (.L.> st
( o1 = the L_join of L || (.L.> & o2 = the L_meet of L || (.L.> & latt (L,(.L.>) = LattStr(# (.L.>,o1,o2 #) ) & dom H2(L) = [:H1(L),H1(L):] ) by Def14, FUNCT_2:def_1;
hence ( latt (L,(.L.>) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & latt (L,<.L.)) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) ) by A1, RELAT_1:68; ::_thesis: verum
end;
theorem Th72: :: FILTER_2:72
for L being Lattice
for P being non empty ClosedSubset of L holds
( the carrier of (latt (L,P)) = P & the L_join of (latt (L,P)) = the L_join of L || P & the L_meet of (latt (L,P)) = the L_meet of L || P )
proof
let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L holds
( the carrier of (latt (L,P)) = P & the L_join of (latt (L,P)) = the L_join of L || P & the L_meet of (latt (L,P)) = the L_meet of L || P )
let P be non empty ClosedSubset of L; ::_thesis: ( the carrier of (latt (L,P)) = P & the L_join of (latt (L,P)) = the L_join of L || P & the L_meet of (latt (L,P)) = the L_meet of L || P )
ex o1, o2 being BinOp of P st
( o1 = H2(L) || P & o2 = H3(L) || P & latt (L,P) = LattStr(# P,o1,o2 #) ) by Def14;
hence ( the carrier of (latt (L,P)) = P & the L_join of (latt (L,P)) = the L_join of L || P & the L_meet of (latt (L,P)) = the L_meet of L || P ) ; ::_thesis: verum
end;
theorem Th73: :: FILTER_2:73
for L being Lattice
for P being non empty ClosedSubset of L
for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
proof
let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L
for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let P be non empty ClosedSubset of L; ::_thesis: for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let p, q be Element of L; ::_thesis: for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let p9, q9 be Element of (latt (L,P)); ::_thesis: ( p = p9 & q = q9 implies ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) )
assume A1: ( p = p9 & q = q9 ) ; ::_thesis: ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
consider o1, o2 being BinOp of P such that
A2: o1 = H2(L) || P and
A3: o2 = H3(L) || P and
A4: latt (L,P) = LattStr(# P,o1,o2 #) by Def14;
A5: [p9,q9] in [:P,P:] by A4;
dom o1 = [:P,P:] by FUNCT_2:def_1;
hence p "\/" q = p9 "\/" q9 by A1, A2, A4, A5, FUNCT_1:47; ::_thesis: p "/\" q = p9 "/\" q9
dom o2 = [:P,P:] by FUNCT_2:def_1;
hence p "/\" q = p9 "/\" q9 by A1, A3, A4, A5, FUNCT_1:47; ::_thesis: verum
end;
theorem Th74: :: FILTER_2:74
for L being Lattice
for P being non empty ClosedSubset of L
for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
proof
let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L
for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
let P be non empty ClosedSubset of L; ::_thesis: for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
let p, q be Element of L; ::_thesis: for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
let p9, q9 be Element of (latt (L,P)); ::_thesis: ( p = p9 & q = q9 implies ( p [= q iff p9 [= q9 ) )
assume A1: ( p = p9 & q = q9 ) ; ::_thesis: ( p [= q iff p9 [= q9 )
thus ( p [= q implies p9 [= q9 ) ::_thesis: ( p9 [= q9 implies p [= q )
proof
assume p "\/" q = q ; :: according to LATTICES:def_3 ::_thesis: p9 [= q9
hence p9 "\/" q9 = q9 by A1, Th73; :: according to LATTICES:def_3 ::_thesis: verum
end;
assume p9 "\/" q9 = q9 ; :: according to LATTICES:def_3 ::_thesis: p [= q
hence p "\/" q = q by A1, Th73; :: according to LATTICES:def_3 ::_thesis: verum
end;
theorem :: FILTER_2:75
for L being Lattice
for I being Ideal of L st L is lower-bounded holds
latt (L,I) is lower-bounded
proof
let L be Lattice; ::_thesis: for I being Ideal of L st L is lower-bounded holds
latt (L,I) is lower-bounded
let I be Ideal of L; ::_thesis: ( L is lower-bounded implies latt (L,I) is lower-bounded )
set b9 = the Element of (latt (L,I));
reconsider b = the Element of (latt (L,I)) as Element of L by Th68;
given c being Element of L such that A1: for a being Element of L holds
( c "/\" a = c & a "/\" c = c ) ; :: according to LATTICES:def_13 ::_thesis: latt (L,I) is lower-bounded
A2: H1( latt (L,I)) = I by Th72;
c "/\" b = c by A1;
then reconsider c9 = c as Element of (latt (L,I)) by A2, Th22;
take c9 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (latt (L,I)) holds
( c9 "/\" b1 = c9 & b1 "/\" c9 = c9 )
let a9 be Element of (latt (L,I)); ::_thesis: ( c9 "/\" a9 = c9 & a9 "/\" c9 = c9 )
reconsider a = a9 as Element of L by Th68;
thus c9 "/\" a9 = c "/\" a by Th73
.= c9 by A1 ; ::_thesis: a9 "/\" c9 = c9
hence a9 "/\" c9 = c9 ; ::_thesis: verum
end;
theorem :: FILTER_2:76
for L being Lattice
for P being non empty ClosedSubset of L st L is modular holds
latt (L,P) is modular
proof
let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L st L is modular holds
latt (L,P) is modular
let P be non empty ClosedSubset of L; ::_thesis: ( L is modular implies latt (L,P) is modular )
assume A1: for a, b, c being Element of L st a [= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c ; :: according to LATTICES:def_12 ::_thesis: latt (L,P) is modular
let a9, b9, c9 be Element of (latt (L,P)); :: according to LATTICES:def_12 ::_thesis: ( not a9 [= c9 or a9 "\/" (b9 "/\" c9) = (a9 "\/" b9) "/\" c9 )
reconsider a = a9, b = b9, c = c9, bc = b9 "/\" c9, ab = a9 "\/" b9 as Element of L by Th68;
assume a9 [= c9 ; ::_thesis: a9 "\/" (b9 "/\" c9) = (a9 "\/" b9) "/\" c9
then A2: a [= c by Th74;
thus a9 "\/" (b9 "/\" c9) = a "\/" bc by Th73
.= a "\/" (b "/\" c) by Th73
.= (a "\/" b) "/\" c by A1, A2
.= ab "/\" c by Th73
.= (a9 "\/" b9) "/\" c9 by Th73 ; ::_thesis: verum
end;
theorem Th77: :: FILTER_2:77
for L being Lattice
for P being non empty ClosedSubset of L st L is distributive holds
latt (L,P) is distributive
proof
let L be Lattice; ::_thesis: for P being non empty ClosedSubset of L st L is distributive holds
latt (L,P) is distributive
let P be non empty ClosedSubset of L; ::_thesis: ( L is distributive implies latt (L,P) is distributive )
assume A1: for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) ; :: according to LATTICES:def_11 ::_thesis: latt (L,P) is distributive
let a9, b9, c9 be Element of (latt (L,P)); :: according to LATTICES:def_11 ::_thesis: a9 "/\" (b9 "\/" c9) = (a9 "/\" b9) "\/" (a9 "/\" c9)
reconsider a = a9, b = b9, c = c9, bc = b9 "\/" c9, ab = a9 "/\" b9, ac = a9 "/\" c9 as Element of L by Th68;
thus a9 "/\" (b9 "\/" c9) = a "/\" bc by Th73
.= a "/\" (b "\/" c) by Th73
.= (a "/\" b) "\/" (a "/\" c) by A1
.= ab "\/" (a "/\" c) by Th73
.= ab "\/" ac by Th73
.= (a9 "/\" b9) "\/" (a9 "/\" c9) by Th73 ; ::_thesis: verum
end;
theorem :: FILTER_2:78
for L being Lattice
for p, q being Element of L st L is implicative & p [= q holds
latt (L,[#p,q#]) is implicative
proof
let L be Lattice; ::_thesis: for p, q being Element of L st L is implicative & p [= q holds
latt (L,[#p,q#]) is implicative
let p, q be Element of L; ::_thesis: ( L is implicative & p [= q implies latt (L,[#p,q#]) is implicative )
assume A1: L is implicative ; ::_thesis: ( not p [= q or latt (L,[#p,q#]) is implicative )
set P = [#p,q#];
set K = latt (L,[#p,q#]);
assume A2: p [= q ; ::_thesis: latt (L,[#p,q#]) is implicative
let a9, b9 be Element of (latt (L,[#p,q#])); :: according to FILTER_0:def_6 ::_thesis: ex b1 being Element of the carrier of (latt (L,[#p,q#])) st
( a9 "/\" b1 [= b9 & ( for b2 being Element of the carrier of (latt (L,[#p,q#])) holds
( not a9 "/\" b2 [= b9 or b2 [= b1 ) ) )
reconsider a = a9, b = b9 as Element of L by Th68;
set c = a => b;
A3: H1( latt (L,[#p,q#])) = [#p,q#] by Th72;
then p [= a by A2, Th62;
then A4: p "\/" ((a => b) "/\" a) = (p "\/" (a => b)) "/\" a by A1, LATTICES:def_12;
A5: a "/\" (a => b) [= b by A1, FILTER_0:def_7;
p [= b by A2, A3, Th62;
then p "\/" (a "/\" (a => b)) [= b by A5, FILTER_0:6;
then A6: (p "\/" (a "/\" (a => b))) "/\" q [= b by FILTER_0:2;
set d = ((a => b) "\/" p) "/\" q;
p [= (a => b) "\/" p by LATTICES:5;
then ( ((a => b) "\/" p) "/\" q [= q & p [= ((a => b) "\/" p) "/\" q ) by A2, FILTER_0:7, LATTICES:6;
then reconsider d9 = ((a => b) "\/" p) "/\" q as Element of (latt (L,[#p,q#])) by A2, A3, Th62;
take d9 ; ::_thesis: ( a9 "/\" d9 [= b9 & ( for b1 being Element of the carrier of (latt (L,[#p,q#])) holds
( not a9 "/\" b1 [= b9 or b1 [= d9 ) ) )
( ((p "\/" (a => b)) "/\" a) "/\" q = a "/\" (((a => b) "\/" p) "/\" q) & a "/\" (((a => b) "\/" p) "/\" q) = a9 "/\" d9 ) by Th73, LATTICES:def_7;
hence a9 "/\" d9 [= b9 by A4, A6, Th74; ::_thesis: for b1 being Element of the carrier of (latt (L,[#p,q#])) holds
( not a9 "/\" b1 [= b9 or b1 [= d9 )
let e9 be Element of (latt (L,[#p,q#])); ::_thesis: ( not a9 "/\" e9 [= b9 or e9 [= d9 )
reconsider e = e9, ae = a9 "/\" e9 as Element of L by Th68;
e [= q by A2, A3, Th62;
then A7: e = e "/\" q by LATTICES:4;
assume a9 "/\" e9 [= b9 ; ::_thesis: e9 [= d9
then ae [= b by Th74;
then a "/\" e [= b by Th73;
then A8: e [= a => b by A1, FILTER_0:def_7;
p [= e by A2, A3, Th62;
then e = e "\/" p by LATTICES:def_3;
then e [= (a => b) "\/" p by A8, FILTER_0:1;
then e [= ((a => b) "\/" p) "/\" q by A7, LATTICES:9;
hence e9 [= d9 by Th74; ::_thesis: verum
end;
registration
let L be Lattice;
let p be Element of L;
cluster latt (L,(.p.>) -> upper-bounded ;
coherence
latt (L,(.p.>) is upper-bounded
proof
latt (L,(.p.>) = (latt ((L .:),((.p.> .:))) .: by Th70
.= (latt ((L .:),<.(p .:).))) .: by Th29
.= (latt <.(p .:).)) .: by Th69 ;
hence latt (L,(.p.>) is upper-bounded by LATTICE2:48; ::_thesis: verum
end;
end;
theorem Th79: :: FILTER_2:79
for L being Lattice
for p being Element of L holds Top (latt (L,(.p.>)) = p
proof
let L be Lattice; ::_thesis: for p being Element of L holds Top (latt (L,(.p.>)) = p
let p be Element of L; ::_thesis: Top (latt (L,(.p.>)) = p
latt (L,(.p.>) = (latt ((L .:),((.p.> .:))) .: by Th70
.= (latt ((L .:),<.(p .:).))) .: by Th29
.= (latt <.(p .:).)) .: by Th69 ;
hence Top (latt (L,(.p.>)) = Bottom (latt <.(p .:).)) by LATTICE2:61
.= p by FILTER_0:56 ;
::_thesis: verum
end;
theorem Th80: :: FILTER_2:80
for L being Lattice
for p being Element of L st L is lower-bounded holds
( latt (L,(.p.>) is lower-bounded & Bottom (latt (L,(.p.>)) = Bottom L )
proof
let L be Lattice; ::_thesis: for p being Element of L st L is lower-bounded holds
( latt (L,(.p.>) is lower-bounded & Bottom (latt (L,(.p.>)) = Bottom L )
let p be Element of L; ::_thesis: ( L is lower-bounded implies ( latt (L,(.p.>) is lower-bounded & Bottom (latt (L,(.p.>)) = Bottom L ) )
assume A1: L is lower-bounded ; ::_thesis: ( latt (L,(.p.>) is lower-bounded & Bottom (latt (L,(.p.>)) = Bottom L )
then A2: L .: is upper-bounded by LATTICE2:48;
then A3: latt <.(p .:).) is upper-bounded by FILTER_0:52;
A4: latt (L,(.p.>) = (latt ((L .:),((.p.> .:))) .: by Th70
.= (latt ((L .:),<.(p .:).))) .: by Th29
.= (latt <.(p .:).)) .: by Th69 ;
hence latt (L,(.p.>) is lower-bounded by A3, LATTICE2:49; ::_thesis: Bottom (latt (L,(.p.>)) = Bottom L
Top (latt <.(p .:).)) = Top (L .:) by A2, FILTER_0:57;
hence Bottom (latt (L,(.p.>)) = Top (L .:) by A4, A3, LATTICE2:62
.= Bottom L by A1, LATTICE2:61 ;
::_thesis: verum
end;
theorem Th81: :: FILTER_2:81
for L being Lattice
for p being Element of L st L is lower-bounded holds
latt (L,(.p.>) is bounded
proof
let L be Lattice; ::_thesis: for p being Element of L st L is lower-bounded holds
latt (L,(.p.>) is bounded
let p be Element of L; ::_thesis: ( L is lower-bounded implies latt (L,(.p.>) is bounded )
assume L is lower-bounded ; ::_thesis: latt (L,(.p.>) is bounded
then latt (L,(.p.>) is lower-bounded upper-bounded Lattice by Th80;
hence latt (L,(.p.>) is bounded ; ::_thesis: verum
end;
theorem Th82: :: FILTER_2:82
for L being Lattice
for p, q being Element of L st p [= q holds
( latt (L,[#p,q#]) is bounded & Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p )
proof
let L be Lattice; ::_thesis: for p, q being Element of L st p [= q holds
( latt (L,[#p,q#]) is bounded & Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p )
let p, q be Element of L; ::_thesis: ( p [= q implies ( latt (L,[#p,q#]) is bounded & Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p ) )
assume A1: p [= q ; ::_thesis: ( latt (L,[#p,q#]) is bounded & Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p )
A2: H1( latt (L,[#p,q#])) = [#p,q#] by Th72;
then reconsider p9 = p, q9 = q as Element of (latt (L,[#p,q#])) by A1, Th62;
A3: now__::_thesis:_for_a9_being_Element_of_(latt_(L,[#p,q#]))_holds_
(_q9_"\/"_a9_=_q9_&_a9_"\/"_q9_=_q9_)
let a9 be Element of (latt (L,[#p,q#])); ::_thesis: ( q9 "\/" a9 = q9 & a9 "\/" q9 = q9 )
reconsider a = a9 as Element of L by Th68;
A4: a [= q by A1, A2, Th62;
thus q9 "\/" a9 = q "\/" a by Th73
.= q9 by A4, LATTICES:def_3 ; ::_thesis: a9 "\/" q9 = q9
hence a9 "\/" q9 = q9 ; ::_thesis: verum
end;
A5: now__::_thesis:_for_a9_being_Element_of_(latt_(L,[#p,q#]))_holds_
(_p9_"/\"_a9_=_p9_&_a9_"/\"_p9_=_p9_)
let a9 be Element of (latt (L,[#p,q#])); ::_thesis: ( p9 "/\" a9 = p9 & a9 "/\" p9 = p9 )
reconsider a = a9 as Element of L by Th68;
A6: p [= a by A1, A2, Th62;
thus p9 "/\" a9 = p "/\" a by Th73
.= p9 by A6, LATTICES:4 ; ::_thesis: a9 "/\" p9 = p9
hence a9 "/\" p9 = p9 ; ::_thesis: verum
end;
then A7: latt (L,[#p,q#]) is lower-bounded upper-bounded Lattice by A3, LATTICES:def_13, LATTICES:def_14;
hence latt (L,[#p,q#]) is bounded ; ::_thesis: ( Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p )
thus ( Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p ) by A5, A3, A7, LATTICES:def_16, LATTICES:def_17; ::_thesis: verum
end;
theorem :: FILTER_2:83
for L being Lattice
for p being Element of L st L is C_Lattice & L is modular holds
latt (L,(.p.>) is C_Lattice
proof
let L be Lattice; ::_thesis: for p being Element of L st L is C_Lattice & L is modular holds
latt (L,(.p.>) is C_Lattice
let p be Element of L; ::_thesis: ( L is C_Lattice & L is modular implies latt (L,(.p.>) is C_Lattice )
assume that
A1: L is C_Lattice and
A2: L is modular ; ::_thesis: latt (L,(.p.>) is C_Lattice
reconsider K = latt (L,(.p.>) as bounded Lattice by A1, Th81;
K is complemented
proof
let b9 be Element of K; :: according to LATTICES:def_19 ::_thesis: ex b1 being Element of the carrier of K st b1 is_a_complement_of b9
reconsider b = b9 as Element of L by Th68;
consider a being Element of L such that
A3: a is_a_complement_of b by A1, LATTICES:def_19;
A4: a "\/" b = Top L by A3, LATTICES:def_18;
A5: H1(K) = (.p.> by Th72;
then A6: b [= p by Th28;
p "/\" a [= p by LATTICES:6;
then reconsider a9 = p "/\" a as Element of K by A5, Th28;
take a9 ; ::_thesis: a9 is_a_complement_of b9
thus a9 "\/" b9 = (p "/\" a) "\/" b by Th73
.= (b "\/" a) "/\" p by A2, A6, LATTICES:def_12
.= p by A1, A4, LATTICES:17
.= Top K by Th79 ; :: according to LATTICES:def_18 ::_thesis: ( b9 "\/" a9 = Top K & a9 "/\" b9 = Bottom K & b9 "/\" a9 = Bottom K )
hence b9 "\/" a9 = Top K ; ::_thesis: ( a9 "/\" b9 = Bottom K & b9 "/\" a9 = Bottom K )
A7: a "/\" b = Bottom L by A3, LATTICES:def_18;
thus a9 "/\" b9 = (p "/\" a) "/\" b by Th73
.= p "/\" (Bottom L) by A7, LATTICES:def_7
.= Bottom L by A1
.= Bottom K by A1, Th80 ; ::_thesis: b9 "/\" a9 = Bottom K
hence b9 "/\" a9 = Bottom K ; ::_thesis: verum
end;
hence latt (L,(.p.>) is C_Lattice ; ::_thesis: verum
end;
theorem Th84: :: FILTER_2:84
for L being Lattice
for p, q being Element of L st L is C_Lattice & L is modular & p [= q holds
latt (L,[#p,q#]) is C_Lattice
proof
let L be Lattice; ::_thesis: for p, q being Element of L st L is C_Lattice & L is modular & p [= q holds
latt (L,[#p,q#]) is C_Lattice
let p, q be Element of L; ::_thesis: ( L is C_Lattice & L is modular & p [= q implies latt (L,[#p,q#]) is C_Lattice )
assume that
A1: L is C_Lattice and
A2: L is modular and
A3: p [= q ; ::_thesis: latt (L,[#p,q#]) is C_Lattice
reconsider K = latt (L,[#p,q#]) as bounded Lattice by A3, Th82;
K is complemented
proof
let b9 be Element of K; :: according to LATTICES:def_19 ::_thesis: ex b1 being Element of the carrier of K st b1 is_a_complement_of b9
reconsider b = b9 as Element of L by Th68;
consider a being Element of L such that
A4: a is_a_complement_of b by A1, LATTICES:def_19;
A5: a "/\" b = Bottom L by A4, LATTICES:def_18;
A6: a "\/" b = Top L by A4, LATTICES:def_18;
A7: H1(K) = [#p,q#] by Th72;
then A8: b [= q by A3, Th62;
a "/\" q [= q by LATTICES:6;
then ( p [= p "\/" (a "/\" q) & p "\/" (a "/\" q) [= q ) by A3, FILTER_0:6, LATTICES:5;
then reconsider a9 = p "\/" (a "/\" q) as Element of K by A3, A7, Th62;
take a9 ; ::_thesis: a9 is_a_complement_of b9
A9: p [= b by A3, A7, Th62;
thus a9 "\/" b9 = (p "\/" (a "/\" q)) "\/" b by Th73
.= (b "\/" p) "\/" (a "/\" q) by LATTICES:def_5
.= b "\/" (a "/\" q) by A9, LATTICES:def_3
.= (Top L) "/\" q by A2, A6, A8, LATTICES:def_12
.= q by A1
.= Top K by A3, Th82 ; :: according to LATTICES:def_18 ::_thesis: ( b9 "\/" a9 = Top K & a9 "/\" b9 = Bottom K & b9 "/\" a9 = Bottom K )
hence b9 "\/" a9 = Top K ; ::_thesis: ( a9 "/\" b9 = Bottom K & b9 "/\" a9 = Bottom K )
thus a9 "/\" b9 = (p "\/" (a "/\" q)) "/\" b by Th73
.= p "\/" ((a "/\" q) "/\" b) by A2, A9, LATTICES:def_12
.= p "\/" (q "/\" (Bottom L)) by A5, LATTICES:def_7
.= p "\/" (Bottom L) by A1
.= p by A1
.= Bottom K by A3, Th82 ; ::_thesis: b9 "/\" a9 = Bottom K
hence b9 "/\" a9 = Bottom K ; ::_thesis: verum
end;
hence latt (L,[#p,q#]) is C_Lattice ; ::_thesis: verum
end;
theorem :: FILTER_2:85
for L being Lattice
for p, q being Element of L st L is B_Lattice & p [= q holds
latt (L,[#p,q#]) is B_Lattice
proof
let L be Lattice; ::_thesis: for p, q being Element of L st L is B_Lattice & p [= q holds
latt (L,[#p,q#]) is B_Lattice
let p, q be Element of L; ::_thesis: ( L is B_Lattice & p [= q implies latt (L,[#p,q#]) is B_Lattice )
assume ( L is B_Lattice & p [= q ) ; ::_thesis: latt (L,[#p,q#]) is B_Lattice
then latt (L,[#p,q#]) is distributive bounded complemented Lattice by Th77, Th84;
hence latt (L,[#p,q#]) is B_Lattice ; ::_thesis: verum
end;
theorem :: FILTER_2:86
for L being Lattice
for S being non empty Subset of L holds
( S is Ideal of L iff for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) ) by Lm1;