:: FILTER_0 semantic presentation
begin
theorem Th1: :: FILTER_0:1
for L being non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr
for p, q, r being Element of L st p [= q holds
r "\/" p [= r "\/" q
proof
let L be non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr ; ::_thesis: for p, q, r being Element of L st p [= q holds
r "\/" p [= r "\/" q
let p, q, r be Element of L; ::_thesis: ( p [= q implies r "\/" p [= r "\/" q )
assume A1: p "\/" q = q ; :: according to LATTICES:def_3 ::_thesis: r "\/" p [= r "\/" q
thus (r "\/" p) "\/" (r "\/" q) = (r "\/" (r "\/" p)) "\/" q by LATTICES:def_5
.= ((r "\/" r) "\/" p) "\/" q by LATTICES:def_5
.= (r "\/" p) "\/" q
.= r "\/" q by A1, LATTICES:def_5 ; :: according to LATTICES:def_3 ::_thesis: verum
end;
theorem :: FILTER_0:2
for L being Lattice
for p, r, q being Element of L st p [= r holds
p "/\" q [= r
proof
let L be Lattice; ::_thesis: for p, r, q being Element of L st p [= r holds
p "/\" q [= r
let p, r, q be Element of L; ::_thesis: ( p [= r implies p "/\" q [= r )
assume p [= r ; ::_thesis: p "/\" q [= r
then A1: p "/\" q [= r "/\" q by LATTICES:9;
r "/\" q [= r by LATTICES:6;
hence p "/\" q [= r by A1, LATTICES:7; ::_thesis: verum
end;
theorem :: FILTER_0:3
for L being Lattice
for p, r, q being Element of L st p [= r holds
p [= q "\/" r
proof
let L be Lattice; ::_thesis: for p, r, q being Element of L st p [= r holds
p [= q "\/" r
let p, r, q be Element of L; ::_thesis: ( p [= r implies p [= q "\/" r )
assume p [= r ; ::_thesis: p [= q "\/" r
then A1: p "\/" q [= r "\/" q by Th1;
p [= p "\/" q by LATTICES:5;
hence p [= q "\/" r by A1, LATTICES:7; ::_thesis: verum
end;
theorem Th4: :: FILTER_0:4
for L being non empty join-commutative join-associative join-absorbing LattStr
for a, b, c, d being Element of L st a [= b & c [= d holds
a "\/" c [= b "\/" d
proof
let L be non empty join-commutative join-associative join-absorbing LattStr ; ::_thesis: for a, b, c, d being Element of L st a [= b & c [= d holds
a "\/" c [= b "\/" d
let a, b, c, d be Element of L; ::_thesis: ( a [= b & c [= d implies a "\/" c [= b "\/" d )
assume a [= b ; ::_thesis: ( not c [= d or a "\/" c [= b "\/" d )
then A1: b = a "\/" b by LATTICES:def_3;
assume c [= d ; ::_thesis: a "\/" c [= b "\/" d
then b "\/" d = (a "\/" b) "\/" (c "\/" d) by A1, LATTICES:def_3
.= ((b "\/" a) "\/" c) "\/" d by LATTICES:def_5
.= (b "\/" (a "\/" c)) "\/" d by LATTICES:def_5
.= (a "\/" c) "\/" (b "\/" d) by LATTICES:def_5 ;
hence a "\/" c [= b "\/" d by LATTICES:def_3; ::_thesis: verum
end;
theorem Th5: :: FILTER_0:5
for L being non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr
for a, b, c, d being Element of L st a [= b & c [= d holds
a "/\" c [= b "/\" d
proof
let L be non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr ; ::_thesis: for a, b, c, d being Element of L st a [= b & c [= d holds
a "/\" c [= b "/\" d
let a, b, c, d be Element of L; ::_thesis: ( a [= b & c [= d implies a "/\" c [= b "/\" d )
assume a [= b ; ::_thesis: ( not c [= d or a "/\" c [= b "/\" d )
then A1: a "/\" b = a by LATTICES:4;
assume c [= d ; ::_thesis: a "/\" c [= b "/\" d
then a "/\" c = (a "/\" b) "/\" (c "/\" d) by A1, LATTICES:4
.= ((a "/\" b) "/\" c) "/\" d by LATTICES:def_7
.= (b "/\" (a "/\" c)) "/\" d by LATTICES:def_7
.= (a "/\" c) "/\" (b "/\" d) by LATTICES:def_7 ;
hence a "/\" c [= b "/\" d by LATTICES:4; ::_thesis: verum
end;
theorem Th6: :: FILTER_0:6
for L being non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr
for a, b, c being Element of L st a [= c & b [= c holds
a "\/" b [= c
proof
let L be non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr ; ::_thesis: for a, b, c being Element of L st a [= c & b [= c holds
a "\/" b [= c
let a, b, c be Element of L; ::_thesis: ( a [= c & b [= c implies a "\/" b [= c )
c "\/" c = c ;
hence ( a [= c & b [= c implies a "\/" b [= c ) by Th4; ::_thesis: verum
end;
theorem Th7: :: FILTER_0:7
for L being non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr
for a, b, c being Element of L st a [= b & a [= c holds
a [= b "/\" c
proof
let L be non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr ; ::_thesis: for a, b, c being Element of L st a [= b & a [= c holds
a [= b "/\" c
let a, b, c be Element of L; ::_thesis: ( a [= b & a [= c implies a [= b "/\" c )
a "/\" a = a ;
hence ( a [= b & a [= c implies a [= b "/\" c ) by Th5; ::_thesis: verum
end;
definition
let L be Lattice;
mode Filter of L is non empty final meet-closed Subset of L;
end;
theorem Th8: :: FILTER_0:8
for L being Lattice
for S being non empty Subset of L holds
( S is Filter 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 Filter 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 Filter 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 Filter 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 Filter of L )
proof
assume A1: S is Filter 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_24; ::_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 "/\" q [= p & p "/\" q [= q ) by LATTICES:6;
hence ( p in S & q in S ) by A1, A2, LATTICES:def_23; ::_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 Filter of L
S is final
proof
let p, q be Element of L; :: according to LATTICES:def_23 ::_thesis: ( not p [= q or not p in S or q in S )
assume that
A4: p [= q and
A5: p in S ; ::_thesis: q in S
p "/\" q = p by A4, LATTICES:4;
hence q in S by A3, A5; ::_thesis: verum
end;
hence S is Filter of L by A3, LATTICES:def_24; ::_thesis: verum
end;
theorem Th9: :: FILTER_0:9
for L being Lattice
for D being non empty Subset of L holds
( D is Filter 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 & p [= q holds
q in D ) ) )
proof
let L be Lattice; ::_thesis: for D being non empty Subset of L holds
( D is Filter 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 & p [= q holds
q in D ) ) )
let D be non empty Subset of L; ::_thesis: ( D is Filter 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 & p [= q holds
q in D ) ) )
thus ( D is Filter 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 & p [= q holds
q in D ) ) ) by LATTICES:def_23, LATTICES:def_24; ::_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 & p [= q holds
q in D ) implies D is Filter of L )
assume A1: ( ( 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 & p [= q holds
q in D ) ) ; ::_thesis: D is Filter of L
then for p, q being Element of L st p [= q & p in D holds
q in D ;
hence D is Filter of L by A1, LATTICES:def_23, LATTICES:def_24; ::_thesis: verum
end;
theorem Th10: :: FILTER_0:10
for L being Lattice
for p, q being Element of L
for H being Filter of L st p in H holds
( p "\/" q in H & q "\/" p in H )
proof
let L be Lattice; ::_thesis: for p, q being Element of L
for H being Filter of L st p in H holds
( p "\/" q in H & q "\/" p in H )
let p, q be Element of L; ::_thesis: for H being Filter of L st p in H holds
( p "\/" q in H & q "\/" p in H )
let H be Filter of L; ::_thesis: ( p in H implies ( p "\/" q in H & q "\/" p in H ) )
p [= p "\/" q by LATTICES:5;
hence ( p in H implies ( p "\/" q in H & q "\/" p in H ) ) by Th9; ::_thesis: verum
end;
theorem Th11: :: FILTER_0:11
for L being Lattice
for H being Filter of L st L is 1_Lattice holds
Top L in H
proof
let L be Lattice; ::_thesis: for H being Filter of L st L is 1_Lattice holds
Top L in H
let H be Filter of L; ::_thesis: ( L is 1_Lattice implies Top L in H )
assume L is 1_Lattice ; ::_thesis: Top L in H
then reconsider L = L as 1_Lattice ;
consider p being Element of L such that
A1: p in H by SUBSET_1:4;
p [= Top L by LATTICES:19;
hence Top L in H by A1, Th9; ::_thesis: verum
end;
theorem :: FILTER_0:12
for L being Lattice st L is 1_Lattice holds
{(Top L)} is Filter of L
proof
let L be Lattice; ::_thesis: ( L is 1_Lattice implies {(Top L)} is Filter of L )
assume L is 1_Lattice ; ::_thesis: {(Top L)} is Filter of L
then reconsider K = L as 1_Lattice ;
now__::_thesis:_for_p,_q_being_Element_of_K_holds_
(_(_p_in_{(Top_K)}_&_q_in_{(Top_K)}_implies_p_"/\"_q_in_{(Top_K)}_)_&_(_p_"/\"_q_in_{(Top_K)}_implies_(_p_in_{(Top_K)}_&_q_in_{(Top_K)}_)_)_)
let p, q be Element of K; ::_thesis: ( ( p in {(Top K)} & q in {(Top K)} implies p "/\" q in {(Top K)} ) & ( p "/\" q in {(Top K)} implies ( p in {(Top K)} & q in {(Top K)} ) ) )
A1: ( p [= Top K & q [= Top K ) by LATTICES:19;
A2: ( p in {(Top K)} iff p = Top K ) by TARSKI:def_1;
hence ( p in {(Top K)} & q in {(Top K)} implies p "/\" q in {(Top K)} ) by LATTICES:17; ::_thesis: ( p "/\" q in {(Top K)} implies ( p in {(Top K)} & q in {(Top K)} ) )
assume p "/\" q in {(Top K)} ; ::_thesis: ( p in {(Top K)} & q in {(Top K)} )
then A3: p "/\" q = Top K by TARSKI:def_1;
( p "/\" q [= p & q "/\" p [= q ) by LATTICES:6;
hence ( p in {(Top K)} & q in {(Top K)} ) by A2, A3, A1, LATTICES:8; ::_thesis: verum
end;
hence {(Top L)} is Filter of L by Th8; ::_thesis: verum
end;
theorem :: FILTER_0:13
for L being Lattice
for p being Element of L st {p} is Filter of L holds
L is upper-bounded
proof
let L be Lattice; ::_thesis: for p being Element of L st {p} is Filter of L holds
L is upper-bounded
let p be Element of L; ::_thesis: ( {p} is Filter of L implies L is upper-bounded )
assume {p} is Filter of L ; ::_thesis: L is upper-bounded
then reconsider F = {p} as Filter of L ;
take p ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of L holds
( p "\/" b1 = p & b1 "\/" p = p )
let q be Element of L; ::_thesis: ( p "\/" q = p & q "\/" p = p )
p in F by TARSKI:def_1;
then p "\/" q in F by Th10;
hence ( p "\/" q = p & q "\/" p = p ) by TARSKI:def_1; ::_thesis: verum
end;
theorem Th14: :: FILTER_0:14
for L being Lattice holds the carrier of L is Filter of L
proof
let L be Lattice; ::_thesis: the carrier of L is Filter of L
the carrier of L = [#] L ;
hence the carrier of L is Filter of L ; ::_thesis: verum
end;
definition
let L be Lattice;
func<.L.) -> Filter of L equals :: FILTER_0:def 1
the carrier of L;
coherence
the carrier of L is Filter of L by Th14;
end;
:: deftheorem defines <. FILTER_0:def_1_:_
for L being Lattice holds <.L.) = the carrier of L;
definition
let L be Lattice;
let p be Element of L;
func<.p.) -> Filter of L equals :: FILTER_0:def 2
{ q where q is Element of L : p [= q } ;
coherence
{ q where q is Element of L : p [= q } is Filter of L
proof
set D = { q where q is Element of L : p [= q } ;
p in { q where q is Element of L : p [= q } ;
then reconsider F = { q where q is Element of L : p [= q } as non empty set ;
F c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in the carrier of L )
assume x in F ; ::_thesis: x in the carrier of L
then ex q being Element of L st
( x = q & p [= q ) ;
hence x in the carrier of L ; ::_thesis: verum
end;
then reconsider F = F as non empty Subset of L ;
A1: now__::_thesis:_for_r,_q_being_Element_of_L_st_r_in_F_&_q_in_F_holds_
r_"/\"_q_in_F
let r, q be Element of L; ::_thesis: ( r in F & q in F implies r "/\" q in F )
assume r in F ; ::_thesis: ( q in F implies r "/\" q in F )
then ex r1 being Element of L st
( r = r1 & p [= r1 ) ;
then A2: p "/\" p [= r "/\" p by LATTICES:9;
assume q in F ; ::_thesis: r "/\" q in F
then ex q1 being Element of L st
( q = q1 & p [= q1 ) ;
then A3: p "/\" r [= q "/\" r by LATTICES:9;
p [= r "/\" q by A3, A2, LATTICES:7;
hence r "/\" q in F ; ::_thesis: verum
end;
now__::_thesis:_for_r,_q_being_Element_of_L_st_r_in_F_&_r_[=_q_holds_
q_in_F
let r, q be Element of L; ::_thesis: ( r in F & r [= q implies q in F )
assume r in F ; ::_thesis: ( r [= q implies q in F )
then A4: ex r1 being Element of L st
( r = r1 & p [= r1 ) ;
assume r [= q ; ::_thesis: q in F
then p [= q by A4, LATTICES:7;
hence q in F ; ::_thesis: verum
end;
hence { q where q is Element of L : p [= q } is Filter of L by A1, Th9; ::_thesis: verum
end;
end;
:: deftheorem defines <. FILTER_0:def_2_:_
for L being Lattice
for p being Element of L holds <.p.) = { q where q is Element of L : p [= q } ;
theorem Th15: :: FILTER_0:15
for L being Lattice
for q, p being Element of L holds
( q in <.p.) iff p [= q )
proof
let L be Lattice; ::_thesis: for q, p being Element of L holds
( q in <.p.) iff p [= q )
let q, p be Element of L; ::_thesis: ( q in <.p.) iff p [= q )
( q in <.p.) iff ex r being Element of L st
( q = r & p [= r ) ) ;
hence ( q in <.p.) iff p [= q ) ; ::_thesis: verum
end;
theorem Th16: :: FILTER_0:16
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 [= p "\/" q by LATTICES:5;
hence ( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) ) ; ::_thesis: verum
end;
theorem Th17: :: FILTER_0:17
for L being Lattice st L is 0_Lattice holds
<.L.) = <.(Bottom L).)
proof
let L be Lattice; ::_thesis: ( L is 0_Lattice implies <.L.) = <.(Bottom L).) )
assume L is 0_Lattice ; ::_thesis: <.L.) = <.(Bottom L).)
then reconsider L9 = L as 0_Lattice ;
thus <.L.) c= <.(Bottom L).) :: according to XBOOLE_0:def_10 ::_thesis: <.(Bottom L).) c= <.L.)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in <.L.) or x in <.(Bottom L).) )
assume x in <.L.) ; ::_thesis: x in <.(Bottom L).)
then reconsider x = x as Element of L9 ;
( Bottom L in <.(Bottom L).) & x "/\" (Bottom L9) = Bottom L9 ) ;
hence x in <.(Bottom L).) by Th8; ::_thesis: verum
end;
thus <.(Bottom L).) c= <.L.) ; ::_thesis: verum
end;
definition
let L be Lattice;
let F be Filter of L;
attrF is being_ultrafilter means :Def3: :: FILTER_0:def 3
( F <> the carrier of L & ( for H being Filter of L st F c= H & H <> the carrier of L holds
F = H ) );
end;
:: deftheorem Def3 defines being_ultrafilter FILTER_0:def_3_:_
for L being Lattice
for F being Filter of L holds
( F is being_ultrafilter iff ( F <> the carrier of L & ( for H being Filter of L st F c= H & H <> the carrier of L holds
F = H ) ) );
theorem Th18: :: FILTER_0:18
for L being Lattice st L is lower-bounded holds
for F being Filter of L st F <> the carrier of L holds
ex H being Filter of L st
( F c= H & H is being_ultrafilter )
proof
let L be Lattice; ::_thesis: ( L is lower-bounded implies for F being Filter of L st F <> the carrier of L holds
ex H being Filter of L st
( F c= H & H is being_ultrafilter ) )
given r being Element of L such that A1: for p being Element of L holds
( r "/\" p = r & p "/\" r = r ) ; :: according to LATTICES:def_13 ::_thesis: for F being Filter of L st F <> the carrier of L holds
ex H being Filter of L st
( F c= H & H is being_ultrafilter )
A2: for H being Filter of L st r in H holds
H = the carrier of L
proof
let H be Filter of L; ::_thesis: ( r in H implies H = the carrier of L )
assume A3: r in H ; ::_thesis: H = the carrier of L
thus H c= the carrier of L ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of L c= H
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of L or x in H )
assume x in the carrier of L ; ::_thesis: x in H
then reconsider p = x as Element of L ;
r "/\" p = r by A1;
then r [= p by LATTICES:4;
hence x in H by A3, Th9; ::_thesis: verum
end;
let F be Filter of L; ::_thesis: ( F <> the carrier of L implies ex H being Filter of L st
( F c= H & H is being_ultrafilter ) )
assume A4: F <> the carrier of L ; ::_thesis: ex H being Filter of L st
( F c= H & H is being_ultrafilter )
set X = { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } ;
A5: for x being set st x in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } holds
( x is Subset of L & x is Filter of L )
proof
let x be set ; ::_thesis: ( x in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } implies ( x is Subset of L & x is Filter of L ) )
assume x in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } ; ::_thesis: ( x is Subset of L & x is Filter of L )
then ex A being Subset of L st
( x = A & F c= A & A is Filter of L & A <> the carrier of L ) ;
hence ( x is Subset of L & x is Filter of L ) ; ::_thesis: verum
end;
A6: for X1 being set st X1 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } holds
( F,X1 are_c=-comparable & X1 <> the carrier of L )
proof
let X1 be set ; ::_thesis: ( X1 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } implies ( F,X1 are_c=-comparable & X1 <> the carrier of L ) )
assume X1 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } ; ::_thesis: ( F,X1 are_c=-comparable & X1 <> the carrier of L )
then ex A being Subset of L st
( X1 = A & F c= A & A is Filter of L & A <> the carrier of L ) ;
hence ( F,X1 are_c=-comparable & X1 <> the carrier of L ) by XBOOLE_0:def_9; ::_thesis: verum
end;
A7: for Z being set st Z c= { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & Z is c=-linear holds
ex Y being set st
( Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
proof
set x = the Element of F;
let Z be set ; ::_thesis: ( Z c= { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & Z is c=-linear implies ex Y being set st
( Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )
assume that
A8: Z c= { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } and
A9: Z is c=-linear ; ::_thesis: ex Y being set st
( Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
take Y = union (Z \/ {F}); ::_thesis: ( Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
F in {F} by TARSKI:def_1;
then A10: F in Z \/ {F} by XBOOLE_0:def_3;
the Element of F in F ;
then reconsider V = Y as non empty set by A10, TARSKI:def_4;
V c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V or x in the carrier of L )
assume x in V ; ::_thesis: x in the carrier of L
then consider X1 being set such that
A11: x in X1 and
A12: X1 in Z \/ {F} by TARSKI:def_4;
( X1 in Z or X1 in {F} ) by A12, XBOOLE_0:def_3;
then X1 is Subset of L by A5, A8;
hence x in the carrier of L by A11; ::_thesis: verum
end;
then reconsider V = V as non empty Subset of L ;
now__::_thesis:_for_p,_q_being_Element_of_L_holds_
(_(_p_in_V_&_q_in_V_implies_p_"/\"_q_in_V_)_&_(_p_"/\"_q_in_V_implies_(_p_in_V_&_q_in_V_)_)_)
let p, q be Element of L; ::_thesis: ( ( p in V & q in V implies p "/\" q in V ) & ( p "/\" q in V implies ( p in V & q in V ) ) )
thus ( p in V & q in V implies p "/\" q in V ) ::_thesis: ( p "/\" q in V implies ( p in V & q in V ) )
proof
assume p in V ; ::_thesis: ( not q in V or p "/\" q in V )
then consider X1 being set such that
A13: p in X1 and
A14: X1 in Z \/ {F} by TARSKI:def_4;
A15: ( X1 in Z or X1 in {F} ) by A14, XBOOLE_0:def_3;
then A16: ( ( X1 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & X1 in Z ) or X1 = F ) by A8, TARSKI:def_1;
assume q in V ; ::_thesis: p "/\" q in V
then consider X2 being set such that
A17: q in X2 and
A18: X2 in Z \/ {F} by TARSKI:def_4;
A19: ( X2 in Z or X2 in {F} ) by A18, XBOOLE_0:def_3;
then ( ( X2 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & X2 in Z ) or X2 = F ) by A8, TARSKI:def_1;
then X1,X2 are_c=-comparable by A6, A9, A16, ORDINAL1:def_8;
then A20: ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9;
A21: X1 is Filter of L by A5, A8, A15, TARSKI:def_1;
X2 is Filter of L by A5, A8, A19, TARSKI:def_1;
then ( p "/\" q in X1 or p "/\" q in X2 ) by A13, A17, A20, A21, Th9;
hence p "/\" q in V by A14, A18, TARSKI:def_4; ::_thesis: verum
end;
assume p "/\" q in V ; ::_thesis: ( p in V & q in V )
then consider X1 being set such that
A22: p "/\" q in X1 and
A23: X1 in Z \/ {F} by TARSKI:def_4;
( X1 in Z or X1 in {F} ) by A23, XBOOLE_0:def_3;
then X1 is Filter of L by A5, A8, TARSKI:def_1;
then ( p in X1 & q in X1 ) by A22, Th8;
hence ( p in V & q in V ) by A23, TARSKI:def_4; ::_thesis: verum
end;
then reconsider V = V as Filter of L by Th8;
now__::_thesis:_not_r_in_V
assume r in V ; ::_thesis: contradiction
then consider X1 being set such that
A24: r in X1 and
A25: X1 in Z \/ {F} by TARSKI:def_4;
( X1 in Z or X1 in {F} ) by A25, XBOOLE_0:def_3;
then ( X1 in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } or X1 = F ) by A8, TARSKI:def_1;
then ex A being Subset of L st
( X1 = A & F c= A & A is Filter of L & A <> the carrier of L ) by A4;
hence contradiction by A2, A24; ::_thesis: verum
end;
then A26: V <> the carrier of L ;
F c= V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in V )
thus ( not x in F or x in V ) by A10, TARSKI:def_4; ::_thesis: verum
end;
hence Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } by A26; ::_thesis: for X1 being set st X1 in Z holds
X1 c= Y
let X1 be set ; ::_thesis: ( X1 in Z implies X1 c= Y )
assume X1 in Z ; ::_thesis: X1 c= Y
then X1 in Z \/ {F} by XBOOLE_0:def_3;
hence X1 c= Y by ZFMISC_1:74; ::_thesis: verum
end;
F in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } by A4;
then consider Y being set such that
A27: Y in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } and
A28: for Z being set st Z in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } & Z <> Y holds
not Y c= Z by A7, ORDERS_1:65;
consider H being Subset of L such that
A29: Y = H and
A30: F c= H and
A31: H is Filter of L and
A32: H <> the carrier of L by A27;
reconsider H = H as Filter of L by A31;
take H ; ::_thesis: ( F c= H & H is being_ultrafilter )
thus ( F c= H & H <> the carrier of L ) by A30, A32; :: according to FILTER_0:def_3 ::_thesis: for H being Filter of L st H c= H & H <> the carrier of L holds
H = H
let G be Filter of L; ::_thesis: ( H c= G & G <> the carrier of L implies H = G )
assume that
A33: H c= G and
A34: G <> the carrier of L ; ::_thesis: H = G
F c= G by A30, A33, XBOOLE_1:1;
then G in { A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L ) } by A34;
hence H = G by A28, A29, A33; ::_thesis: verum
end;
theorem Th19: :: FILTER_0:19
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 by LATTICES:6;
then not p [= p "/\" r by A1, LATTICES:8;
hence <.p.) <> the carrier of L by Th15; ::_thesis: verum
end;
theorem Th20: :: FILTER_0:20
for L being Lattice
for p being Element of L st L is 0_Lattice & p <> Bottom L holds
ex H being Filter of L st
( p in H & H is being_ultrafilter )
proof
let L be Lattice; ::_thesis: for p being Element of L st L is 0_Lattice & p <> Bottom L holds
ex H being Filter of L st
( p in H & H is being_ultrafilter )
let p be Element of L; ::_thesis: ( L is 0_Lattice & p <> Bottom L implies ex H being Filter of L st
( p in H & H is being_ultrafilter ) )
assume that
A1: L is 0_Lattice and
A2: p <> Bottom L ; ::_thesis: ex H being Filter of L st
( p in H & H is being_ultrafilter )
reconsider L9 = L as 0_Lattice by A1;
reconsider p9 = p as Element of L9 ;
p9 "/\" (Bottom L9) = Bottom L9 ;
then consider H being Filter of L such that
A3: ( <.p.) c= H & H is being_ultrafilter ) by A2, Th18, Th19;
take H ; ::_thesis: ( p in H & H is being_ultrafilter )
p in <.p.) ;
hence ( p in H & H is being_ultrafilter ) by A3; ::_thesis: verum
end;
definition
let L be Lattice;
let D be non empty Subset of L;
func<.D.) -> Filter of L means :Def4: :: FILTER_0:def 4
( D c= it & ( for F being Filter of L st D c= F holds
it c= F ) );
existence
ex b1 being Filter of L st
( D c= b1 & ( for F being Filter of L st D c= F holds
b1 c= F ) )
proof
set x = the Element of D;
defpred S1[ set ] means ( $1 is Filter of L & D c= $1 );
consider X being set such that
A1: for Z being set holds
( Z in X iff ( Z in bool the carrier of L & S1[Z] ) ) from XBOOLE_0:sch_1();
reconsider x = the Element of D as Element of L ;
<.L.) = the carrier of L ;
then A2: X <> {} by A1;
now__::_thesis:_for_Z_being_set_st_Z_in_X_holds_
x_in_Z
let Z be set ; ::_thesis: ( Z in X implies x in Z )
assume Z in X ; ::_thesis: x in Z
then D c= Z by A1;
hence x in Z by TARSKI:def_3; ::_thesis: verum
end;
then reconsider F = meet X as non empty set by A2, SETFAM_1:def_1;
A3: <.L.) in X by A1;
F c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in the carrier of L )
thus ( not x in F or x in the carrier of L ) by A3, SETFAM_1:def_1; ::_thesis: verum
end;
then 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_implies_p_"/\"_q_in_F_)_&_(_p_"/\"_q_in_F_implies_(_p_in_F_&_q_in_F_)_)_)
let p, q be Element of L; ::_thesis: ( ( p in F & q in F implies p "/\" q in F ) & ( p "/\" q in F implies ( p in F & q in F ) ) )
thus ( p in F & q in F implies p "/\" q in F ) ::_thesis: ( p "/\" q in F implies ( p in F & q in F ) )
proof
assume A4: ( p in F & q in F ) ; ::_thesis: p "/\" q in F
for Z being set st Z in X holds
p "/\" q in Z
proof
let Z be set ; ::_thesis: ( Z in X implies p "/\" q in Z )
assume A5: Z in X ; ::_thesis: p "/\" q in Z
then reconsider Z9 = Z as Filter of L by A1;
( p in Z9 & q in Z9 ) by A4, A5, SETFAM_1:def_1;
hence p "/\" q in Z by Th8; ::_thesis: verum
end;
hence p "/\" q in F by A2, SETFAM_1:def_1; ::_thesis: verum
end;
assume A6: p "/\" q in F ; ::_thesis: ( p in F & q in F )
now__::_thesis:_for_Z_being_set_st_Z_in_X_holds_
p_in_Z
let Z be set ; ::_thesis: ( Z in X implies p in Z )
assume A7: Z in X ; ::_thesis: p in Z
then reconsider Z9 = Z as Filter of L by A1;
p "/\" q in Z9 by A6, A7, SETFAM_1:def_1;
hence p in Z by Th8; ::_thesis: verum
end;
hence p in F by A2, SETFAM_1:def_1; ::_thesis: q in F
now__::_thesis:_for_Z_being_set_st_Z_in_X_holds_
q_in_Z
let Z be set ; ::_thesis: ( Z in X implies q in Z )
assume A8: Z in X ; ::_thesis: q in Z
then reconsider Z9 = Z as Filter of L by A1;
p "/\" q in Z9 by A6, A8, SETFAM_1:def_1;
hence q in Z by Th8; ::_thesis: verum
end;
hence q in F by A2, SETFAM_1:def_1; ::_thesis: verum
end;
then reconsider F = F as Filter of L by Th8;
take F ; ::_thesis: ( D c= F & ( for F being Filter of L st D c= F holds
F c= F ) )
for Z being set st Z in X holds
D c= Z by A1;
hence D c= F by A2, SETFAM_1:5; ::_thesis: for F being Filter of L st D c= F holds
F c= F
let H be Filter of L; ::_thesis: ( D c= H implies F c= H )
assume D c= H ; ::_thesis: F c= H
then H in X by A1;
hence F c= H by SETFAM_1:3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Filter of L st D c= b1 & ( for F being Filter of L st D c= F holds
b1 c= F ) & D c= b2 & ( for F being Filter of L st D c= F holds
b2 c= F ) holds
b1 = b2
proof
let F1, F2 be Filter of L; ::_thesis: ( D c= F1 & ( for F being Filter of L st D c= F holds
F1 c= F ) & D c= F2 & ( for F being Filter of L st D c= F holds
F2 c= F ) implies F1 = F2 )
assume ( D c= F1 & ( for F being Filter of L st D c= F holds
F1 c= F ) & D c= F2 & ( for F being Filter of L st D c= F holds
F2 c= F ) ) ; ::_thesis: F1 = F2
hence ( F1 c= F2 & F2 c= F1 ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
end;
:: deftheorem Def4 defines <. FILTER_0:def_4_:_
for L being Lattice
for D being non empty Subset of L
for b3 being Filter of L holds
( b3 = <.D.) iff ( D c= b3 & ( for F being Filter of L st D c= F holds
b3 c= F ) ) );
theorem Th21: :: FILTER_0:21
for L being Lattice
for F being Filter of L holds <.F.) = F
proof
let L be Lattice; ::_thesis: for F being Filter of L holds <.F.) = F
let F be Filter of L; ::_thesis: <.F.) = F
for H being Filter of L st F c= H holds
F c= H ;
hence <.F.) = F by Def4; ::_thesis: verum
end;
theorem Th22: :: FILTER_0:22
for L being Lattice
for D1, D2 being non empty Subset of L st D1 c= D2 holds
<.D1.) c= <.D2.)
proof
let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L st D1 c= D2 holds
<.D1.) c= <.D2.)
let D1, D2 be non empty Subset of L; ::_thesis: ( D1 c= D2 implies <.D1.) c= <.D2.) )
assume A1: D1 c= D2 ; ::_thesis: <.D1.) c= <.D2.)
D2 c= <.D2.) by Def4;
then D1 c= <.D2.) by A1, XBOOLE_1:1;
hence <.D1.) c= <.D2.) by Def4; ::_thesis: verum
end;
theorem Th23: :: FILTER_0:23
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.) )
assume A1: p in D ; ::_thesis: <.p.) c= <.D.)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in <.p.) or x in <.D.) )
A2: D c= <.D.) by Def4;
assume x in <.p.) ; ::_thesis: x in <.D.)
then ex q being Element of L st
( x = q & p [= q ) ;
hence x in <.D.) by A1, A2, Th9; ::_thesis: verum
end;
theorem Th24: :: FILTER_0:24
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.) )
assume A1: D = {p} ; ::_thesis: <.D.) = <.p.)
D c= <.p.)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in <.p.) )
assume x in D ; ::_thesis: x in <.p.)
then x = p by A1, TARSKI:def_1;
hence x in <.p.) ; ::_thesis: verum
end;
hence <.D.) c= <.p.) by Def4; :: according to XBOOLE_0:def_10 ::_thesis: <.p.) c= <.D.)
p in D by A1, TARSKI:def_1;
hence <.p.) c= <.D.) by Th23; ::_thesis: verum
end;
theorem Th25: :: FILTER_0:25
for L being Lattice
for D being non empty Subset of L st L is 0_Lattice & Bottom 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 0_Lattice & Bottom L in D holds
( <.D.) = <.L.) & <.D.) = the carrier of L )
let D be non empty Subset of L; ::_thesis: ( L is 0_Lattice & Bottom L in D implies ( <.D.) = <.L.) & <.D.) = the carrier of L ) )
assume that
A1: L is 0_Lattice and
A2: Bottom L in D ; ::_thesis: ( <.D.) = <.L.) & <.D.) = the carrier of L )
A3: <.(Bottom L).) = <.L.) by A1, Th17;
hence ( <.D.) c= <.L.) & <.L.) c= <.D.) ) by A2, Th23; :: according to XBOOLE_0:def_10 ::_thesis: <.D.) = the carrier of L
thus ( <.D.) c= the carrier of L & the carrier of L c= <.D.) ) by A2, A3, Th23; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
theorem Th26: :: FILTER_0:26
for L being Lattice
for F being Filter of L st L is 0_Lattice & Bottom L in F holds
( F = <.L.) & F = the carrier of L )
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is 0_Lattice & Bottom L in F holds
( F = <.L.) & F = the carrier of L )
let F be Filter of L; ::_thesis: ( L is 0_Lattice & Bottom L in F implies ( F = <.L.) & F = the carrier of L ) )
F = <.F.) by Th21;
hence ( L is 0_Lattice & Bottom L in F implies ( F = <.L.) & F = the carrier of L ) ) by Th25; ::_thesis: verum
end;
definition
let L be Lattice;
let F be Filter of L;
attrF is prime means :: FILTER_0:def 5
for p, q being Element of L holds
( p "\/" q in F iff ( p in F or q in F ) );
end;
:: deftheorem defines prime FILTER_0:def_5_:_
for L being Lattice
for F being Filter of L holds
( F is prime iff for p, q being Element of L holds
( p "\/" q in F iff ( p in F or q in F ) ) );
theorem Th27: :: FILTER_0:27
for L being Lattice st L is B_Lattice holds
for p, q being Element of L holds
( p "/\" ((p `) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds
r [= (p `) "\/" q ) )
proof
let L be Lattice; ::_thesis: ( L is B_Lattice implies for p, q being Element of L holds
( p "/\" ((p `) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds
r [= (p `) "\/" q ) ) )
assume L is B_Lattice ; ::_thesis: for p, q being Element of L holds
( p "/\" ((p `) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds
r [= (p `) "\/" q ) )
then reconsider S = L as B_Lattice ;
reconsider J = S as 1_Lattice ;
reconsider K = S as 0_Lattice ;
let p, q be Element of L; ::_thesis: ( p "/\" ((p `) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds
r [= (p `) "\/" q ) )
set r = (p `) "\/" q;
reconsider p9 = p, q9 = q as Element of K ;
reconsider p99 = p as Element of S ;
A1: ( p99 "/\" (p99 `) = Bottom L & (Bottom K) "\/" (p9 "/\" q9) = p9 "/\" q9 ) by LATTICES:20;
reconsider K = S as D_Lattice ;
reconsider p9 = p, q9 = q, r9 = (p `) "\/" q as Element of K ;
p9 "/\" r9 = (p9 "/\" (p9 `)) "\/" (p9 "/\" q9) by LATTICES:def_11;
hence p "/\" ((p `) "\/" q) [= q by A1, LATTICES:6; ::_thesis: for r being Element of L st p "/\" r [= q holds
r [= (p `) "\/" q
let r1 be Element of L; ::_thesis: ( p "/\" r1 [= q implies r1 [= (p `) "\/" q )
reconsider r19 = r1 as Element of K ;
reconsider pp = p, r99 = r1 as Element of J ;
A2: ( (p99 `) "\/" p99 = Top L & (Top J) "/\" ((pp `) "\/" r99) = (pp `) "\/" r99 ) by LATTICES:21;
assume p "/\" r1 [= q ; ::_thesis: r1 [= (p `) "\/" q
then A3: (p `) "\/" (p "/\" r1) [= (p `) "\/" q by Th1;
( (p9 `) "\/" (p9 "/\" r19) = ((p9 `) "\/" p9) "/\" ((p9 `) "\/" r19) & r1 [= r1 "\/" (p `) ) by LATTICES:5, LATTICES:11;
hence r1 [= (p `) "\/" q by A3, A2, LATTICES:7; ::_thesis: verum
end;
definition
let IT be non empty LattStr ;
attrIT is implicative means :Def6: :: FILTER_0:def 6
for p, q being Element of IT ex r being Element of IT st
( p "/\" r [= q & ( for r1 being Element of IT st p "/\" r1 [= q holds
r1 [= r ) );
end;
:: deftheorem Def6 defines implicative FILTER_0:def_6_:_
for IT being non empty LattStr holds
( IT is implicative iff for p, q being Element of IT ex r being Element of IT st
( p "/\" r [= q & ( for r1 being Element of IT st p "/\" r1 [= q holds
r1 [= r ) ) );
registration
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like implicative for LattStr ;
existence
ex b1 being Lattice st
( b1 is strict & b1 is implicative )
proof
set L = the strict B_Lattice;
now__::_thesis:_for_p,_q_being_Element_of_the_strict_B_Lattice_ex_r_being_Element_of_the_strict_B_Lattice_st_
(_p_"/\"_r_[=_q_&_(_for_r1_being_Element_of_the_strict_B_Lattice_st_p_"/\"_r1_[=_q_holds_
r1_[=_r_)_)
let p, q be Element of the strict B_Lattice; ::_thesis: ex r being Element of the strict B_Lattice st
( p "/\" r [= q & ( for r1 being Element of the strict B_Lattice st p "/\" r1 [= q holds
r1 [= r ) )
reconsider r = (p `) "\/" q as Element of the strict B_Lattice ;
take r = r; ::_thesis: ( p "/\" r [= q & ( for r1 being Element of the strict B_Lattice st p "/\" r1 [= q holds
r1 [= r ) )
thus ( p "/\" r [= q & ( for r1 being Element of the strict B_Lattice st p "/\" r1 [= q holds
r1 [= r ) ) by Th27; ::_thesis: verum
end;
then the strict B_Lattice is implicative by Def6;
hence ex b1 being Lattice st
( b1 is strict & b1 is implicative ) ; ::_thesis: verum
end;
end;
definition
mode I_Lattice is implicative Lattice;
end;
definition
let L be Lattice;
let p, q be Element of L;
assume A1: L is I_Lattice ;
funcp => q -> Element of L means :Def7: :: FILTER_0:def 7
( p "/\" it [= q & ( for r being Element of L st p "/\" r [= q holds
r [= it ) );
existence
ex b1 being Element of L st
( p "/\" b1 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= b1 ) ) by A1, Def6;
correctness
uniqueness
for b1, b2 being Element of L st p "/\" b1 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= b1 ) & p "/\" b2 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= b2 ) holds
b1 = b2;
proof
let r1, r2 be Element of L; ::_thesis: ( p "/\" r1 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= r1 ) & p "/\" r2 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= r2 ) implies r1 = r2 )
assume ( p "/\" r1 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= r1 ) & p "/\" r2 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= r2 ) ) ; ::_thesis: r1 = r2
then ( r1 [= r2 & r2 [= r1 ) ;
hence r1 = r2 by LATTICES:8; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines => FILTER_0:def_7_:_
for L being Lattice
for p, q being Element of L st L is I_Lattice holds
for b4 being Element of L holds
( b4 = p => q iff ( p "/\" b4 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= b4 ) ) );
registration
cluster non empty Lattice-like implicative -> upper-bounded for LattStr ;
coherence
for b1 being I_Lattice holds b1 is upper-bounded
proof
let I be I_Lattice; ::_thesis: I is upper-bounded
set i = the Element of I;
take k = the Element of I => the Element of I; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of I holds
( k "\/" b1 = k & b1 "\/" k = k )
let j be Element of I; ::_thesis: ( k "\/" j = k & j "\/" k = k )
the Element of I "/\" j [= the Element of I by LATTICES:6;
then A1: j [= k by Def7;
j "\/" k = k "\/" j ;
hence ( k "\/" j = k & j "\/" k = k ) by A1, LATTICES:def_3; ::_thesis: verum
end;
end;
theorem Th28: :: FILTER_0:28
for I being I_Lattice
for i being Element of I holds i => i = Top I
proof
let I be I_Lattice; ::_thesis: for i being Element of I holds i => i = Top I
let i be Element of I; ::_thesis: i => i = Top I
now__::_thesis:_for_j_being_Element_of_I_holds_j_"\/"_(i_=>_i)_=_i_=>_i
let j be Element of I; ::_thesis: j "\/" (i => i) = i => i
i "/\" j [= i by LATTICES:6;
then j [= i => i by Def7;
hence j "\/" (i => i) = i => i by LATTICES:def_3; ::_thesis: verum
end;
hence i => i = Top I by RLSUB_2:65; ::_thesis: verum
end;
registration
cluster non empty Lattice-like implicative -> distributive for LattStr ;
coherence
for b1 being I_Lattice holds b1 is distributive
proof
let I be I_Lattice; ::_thesis: I is distributive
let i be Element of I; :: according to LATTICES:def_11 ::_thesis: for b1, b2 being Element of the carrier of I holds i "/\" (b1 "\/" b2) = (i "/\" b1) "\/" (i "/\" b2)
let j, k be Element of I; ::_thesis: i "/\" (j "\/" k) = (i "/\" j) "\/" (i "/\" k)
i "/\" k [= (i "/\" k) "\/" (i "/\" j) by LATTICES:5;
then A1: k [= i => ((i "/\" j) "\/" (i "/\" k)) by Def7;
i "/\" j [= (i "/\" j) "\/" (i "/\" k) by LATTICES:5;
then j [= i => ((i "/\" j) "\/" (i "/\" k)) by Def7;
then j "\/" k [= i => ((i "/\" j) "\/" (i "/\" k)) by A1, Th6;
then A2: i "/\" (j "\/" k) [= i "/\" (i => ((i "/\" j) "\/" (i "/\" k))) by LATTICES:9;
( i "/\" j [= i "/\" (j "\/" k) & i "/\" k [= i "/\" (j "\/" k) ) by LATTICES:5, LATTICES:9;
then A3: (i "/\" j) "\/" (i "/\" k) [= i "/\" (j "\/" k) by Th6;
i "/\" (i => ((i "/\" j) "\/" (i "/\" k))) [= (i "/\" j) "\/" (i "/\" k) by Def7;
then i "/\" (j "\/" k) [= (i "/\" j) "\/" (i "/\" k) by A2, LATTICES:7;
hence i "/\" (j "\/" k) = (i "/\" j) "\/" (i "/\" k) by A3, LATTICES:8; ::_thesis: verum
end;
end;
registration
cluster non empty Lattice-like Boolean -> implicative for LattStr ;
coherence
for b1 being B_Lattice holds b1 is implicative
proof
let B be B_Lattice; ::_thesis: B is implicative
let p, q be Element of B; :: according to FILTER_0:def_6 ::_thesis: ex r being Element of B st
( p "/\" r [= q & ( for r1 being Element of B st p "/\" r1 [= q holds
r1 [= r ) )
take r = (p `) "\/" q; ::_thesis: ( p "/\" r [= q & ( for r1 being Element of B st p "/\" r1 [= q holds
r1 [= r ) )
thus ( p "/\" r [= q & ( for r1 being Element of B st p "/\" r1 [= q holds
r1 [= r ) ) by Th27; ::_thesis: verum
end;
end;
registration
cluster non empty Lattice-like implicative -> distributive for LattStr ;
coherence
for b1 being Lattice st b1 is implicative holds
b1 is distributive ;
end;
theorem Th29: :: FILTER_0:29
for I being I_Lattice
for i, j being Element of I
for FI being Filter of I st i in FI & i => j in FI holds
j in FI
proof
let I be I_Lattice; ::_thesis: for i, j being Element of I
for FI being Filter of I st i in FI & i => j in FI holds
j in FI
let i, j be Element of I; ::_thesis: for FI being Filter of I st i in FI & i => j in FI holds
j in FI
let FI be Filter of I; ::_thesis: ( i in FI & i => j in FI implies j in FI )
assume ( i in FI & i => j in FI ) ; ::_thesis: j in FI
then A1: i "/\" (i => j) in FI by Th8;
i "/\" (i => j) [= j by Def7;
hence j in FI by A1, Th9; ::_thesis: verum
end;
theorem Th30: :: FILTER_0:30
for I being I_Lattice
for j, i being Element of I
for FI being Filter of I st j in FI holds
i => j in FI
proof
let I be I_Lattice; ::_thesis: for j, i being Element of I
for FI being Filter of I st j in FI holds
i => j in FI
let j, i be Element of I; ::_thesis: for FI being Filter of I st j in FI holds
i => j in FI
let FI be Filter of I; ::_thesis: ( j in FI implies i => j in FI )
j "/\" i [= j by LATTICES:6;
then j [= i => j by Def7;
hence ( j in FI implies i => j in FI ) by Th9; ::_thesis: verum
end;
definition
let L be Lattice;
let D1, D2 be non empty Subset of L;
funcD1 "/\" D2 -> Subset of L equals :: FILTER_0:def 8
{ (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 = the Element of D1;
set y = the Element of D2;
reconsider x = the Element of D1, y = the Element of D2 as Element of L ;
x "/\" y in { (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ;
then reconsider D = { (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 ) } as non empty set ;
D c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in the carrier of L )
assume x in D ; ::_thesis: x in the carrier of L
then ex p, q being Element of L st
( x = p "/\" q & p in D1 & q in D2 ) ;
hence x in the carrier of 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_0:def_8_:_
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 = the Element of D1;
set y = the Element of D2;
reconsider x = the Element of D1, y = the Element of D2 as Element of L ;
x "/\" y in { (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ;
hence not D1 "/\" D2 is empty ; ::_thesis: verum
end;
end;
theorem :: FILTER_0:31
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_0:32
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 Th33: :: FILTER_0:33
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
now__::_thesis:_for_D1,_D2_being_non_empty_Subset_of_L_holds_D1_"/\"_D2_c=_D2_"/\"_D1
let D1, D2 be non empty Subset of L; ::_thesis: D1 "/\" D2 c= D2 "/\" D1
thus D1 "/\" D2 c= D2 "/\" D1 ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 "/\" D2 or x in D2 "/\" D1 )
assume x in D1 "/\" D2 ; ::_thesis: x in D2 "/\" D1
then ex p, q being Element of L st
( x = p "/\" q & p in D1 & q in D2 ) ;
hence x in D2 "/\" D1 ; ::_thesis: verum
end;
end;
hence ( D1 "/\" D2 c= D2 "/\" D1 & D2 "/\" D1 c= D1 "/\" D2 ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
registration
let L be D_Lattice;
let F1, F2 be Filter of L;
clusterF1 "/\" F2 -> final meet-closed ;
coherence
( F1 "/\" F2 is final & F1 "/\" F2 is meet-closed )
proof
now__::_thesis:_for_p,_q_being_Element_of_L_holds_
(_(_p_in_F1_"/\"_F2_&_q_in_F1_"/\"_F2_implies_p_"/\"_q_in_F1_"/\"_F2_)_&_(_p_"/\"_q_in_F1_"/\"_F2_implies_(_p_in_F1_"/\"_F2_&_q_in_F1_"/\"_F2_)_)_)
let p, q be Element of L; ::_thesis: ( ( p in F1 "/\" F2 & q in F1 "/\" F2 implies p "/\" q in F1 "/\" F2 ) & ( p "/\" q in F1 "/\" F2 implies ( p in F1 "/\" F2 & q in F1 "/\" F2 ) ) )
A1: ( p = p "\/" (p "/\" q) & q = q "\/" (p "/\" q) ) by LATTICES:def_8;
thus ( p in F1 "/\" F2 & q in F1 "/\" F2 implies p "/\" q in F1 "/\" F2 ) ::_thesis: ( p "/\" q in F1 "/\" F2 implies ( p in F1 "/\" F2 & q in F1 "/\" F2 ) )
proof
assume p in F1 "/\" F2 ; ::_thesis: ( not q in F1 "/\" F2 or p "/\" q in F1 "/\" F2 )
then consider p1, p2 being Element of L such that
A2: p = p1 "/\" p2 and
A3: ( p1 in F1 & p2 in F2 ) ;
assume q in F1 "/\" F2 ; ::_thesis: p "/\" q in F1 "/\" F2
then consider q1, q2 being Element of L such that
A4: q = q1 "/\" q2 and
A5: ( q1 in F1 & q2 in F2 ) ;
A6: p "/\" q = ((p1 "/\" p2) "/\" q1) "/\" q2 by A2, A4, LATTICES:def_7
.= ((p1 "/\" q1) "/\" p2) "/\" q2 by LATTICES:def_7
.= (p1 "/\" q1) "/\" (p2 "/\" q2) by LATTICES:def_7 ;
( p1 "/\" q1 in F1 & p2 "/\" q2 in F2 ) by A3, A5, Th8;
hence p "/\" q in F1 "/\" F2 by A6; ::_thesis: verum
end;
assume p "/\" q in F1 "/\" F2 ; ::_thesis: ( p in F1 "/\" F2 & q in F1 "/\" F2 )
then consider p1, q1 being Element of L such that
A7: p "/\" q = p1 "/\" q1 and
A8: ( p1 in F1 & q1 in F2 ) ;
A9: ( q "\/" p1 in F1 & q "\/" q1 in F2 ) by A8, Th10;
A10: ( p "\/" (p1 "/\" q1) = (p "\/" p1) "/\" (p "\/" q1) & q "\/" (p1 "/\" q1) = (q "\/" p1) "/\" (q "\/" q1) ) by LATTICES:11;
( p "\/" p1 in F1 & p "\/" q1 in F2 ) by A8, Th10;
hence ( p in F1 "/\" F2 & q in F1 "/\" F2 ) by A7, A1, A10, A9; ::_thesis: verum
end;
hence ( F1 "/\" F2 is final & F1 "/\" F2 is meet-closed ) by Th8; ::_thesis: verum
end;
end;
theorem Th34: :: FILTER_0:34
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.)).) )
now__::_thesis:_for_D1,_D2_being_non_empty_Subset_of_L_holds_
(_<.(D1_\/_D2).)_c=_<.(<.D1.)_\/_D2).)_&_<.(<.D1.)_\/_D2).)_c=_<.(D1_\/_D2).)_)
let D1, D2 be non empty Subset of L; ::_thesis: ( <.(D1 \/ D2).) c= <.(<.D1.) \/ D2).) & <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).) )
( D2 c= D1 \/ D2 & D1 \/ D2 c= <.(D1 \/ D2).) ) by Def4, XBOOLE_1:7;
then A1: D2 c= <.(D1 \/ D2).) by XBOOLE_1:1;
D1 c= <.D1.) by Def4;
then D1 \/ D2 c= <.D1.) \/ D2 by XBOOLE_1:9;
hence <.(D1 \/ D2).) c= <.(<.D1.) \/ D2).) by Th22; ::_thesis: <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).)
<.D1.) c= <.(D1 \/ D2).) by Th22, XBOOLE_1:7;
then <.D1.) \/ D2 c= <.(D1 \/ D2).) by A1, XBOOLE_1:8;
hence <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).) by Def4; ::_thesis: verum
end;
hence ( <.(D1 \/ D2).) c= <.(<.D1.) \/ D2).) & <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).) & <.(D1 \/ D2).) c= <.(D1 \/ <.D2.)).) & <.(D1 \/ <.D2.)).) c= <.(D1 \/ D2).) ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
theorem :: FILTER_0:35
for L being Lattice
for F, H being Filter of L holds <.(F \/ H).) = { r where r is Element of L : ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H ) }
proof
let L be Lattice; ::_thesis: for F, H being Filter of L holds <.(F \/ H).) = { r where r is Element of L : ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H ) }
let F, H be Filter of L; ::_thesis: <.(F \/ H).) = { r where r is Element of L : ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H ) }
set X = { r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) } ;
consider p1 being Element of L such that
A1: p1 in F by SUBSET_1:4;
consider q1 being Element of L such that
A2: q1 in H by SUBSET_1:4;
p1 "/\" q1 in { r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) } by A1, A2;
then reconsider D = { r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) } as non empty set ;
D c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in the carrier of L )
assume x in D ; ::_thesis: x in the carrier of L
then ex r1 being Element of L st
( x = r1 & ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) ) ;
hence x in the carrier of L ; ::_thesis: verum
end;
then reconsider D = D as non empty Subset of L ;
A3: for p, q being Element of L st p in D & p [= q holds
q in D
proof
let p, q be Element of L; ::_thesis: ( p in D & p [= q implies q in D )
assume p in D ; ::_thesis: ( not p [= q or q in D )
then ex r1 being Element of L st
( p = r1 & ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) ) ;
then consider p1, q1 being Element of L such that
A4: p1 "/\" q1 [= p and
A5: ( p1 in F & q1 in H ) ;
assume p [= q ; ::_thesis: q in D
then p1 "/\" q1 [= q by A4, LATTICES:7;
hence q in D by A5; ::_thesis: verum
end;
for p, q being Element of L st p in D & q in D holds
p "/\" q in D
proof
let p, q be Element of L; ::_thesis: ( p in D & q in D implies p "/\" q in D )
assume p in D ; ::_thesis: ( not q in D or p "/\" q in D )
then ex r1 being Element of L st
( p = r1 & ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) ) ;
then consider p1, q1 being Element of L such that
A6: p1 "/\" q1 [= p and
A7: ( p1 in F & q1 in H ) ;
assume q in D ; ::_thesis: p "/\" q in D
then ex r2 being Element of L st
( q = r2 & ex p, q being Element of L st
( p "/\" q [= r2 & p in F & q in H ) ) ;
then consider p2, q2 being Element of L such that
A8: p2 "/\" q2 [= q and
A9: ( p2 in F & q2 in H ) ;
A10: p "/\" (p2 "/\" q2) [= p "/\" q by A8, LATTICES:9;
(p1 "/\" q1) "/\" (p2 "/\" q2) [= p "/\" (p2 "/\" q2) by A6, LATTICES:9;
then A11: (p1 "/\" q1) "/\" (p2 "/\" q2) [= p "/\" q by A10, LATTICES:7;
A12: (p1 "/\" q1) "/\" (p2 "/\" q2) = ((p1 "/\" q1) "/\" p2) "/\" q2 by LATTICES:def_7
.= ((p1 "/\" p2) "/\" q1) "/\" q2 by LATTICES:def_7
.= (p1 "/\" p2) "/\" (q1 "/\" q2) by LATTICES:def_7 ;
( p1 "/\" p2 in F & q1 "/\" q2 in H ) by A7, A9, Th8;
hence p "/\" q in D by A12, A11; ::_thesis: verum
end;
then reconsider D = D as Filter of L by A3, Th9;
A13: H c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H or x in D )
assume x in H ; ::_thesis: x in D
then reconsider q = x as Element of H ;
q "/\" p1 [= q by LATTICES:6;
hence x in D by A1; ::_thesis: verum
end;
F c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in D )
assume x in F ; ::_thesis: x in D
then reconsider p = x as Element of F ;
p "/\" q1 [= p by LATTICES:6;
hence x in D by A2; ::_thesis: verum
end;
then F \/ H c= D by A13, XBOOLE_1:8;
hence <.(F \/ H).) c= { r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) } by Def4; :: according to XBOOLE_0:def_10 ::_thesis: { r where r is Element of L : ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H ) } c= <.(F \/ H).)
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
( p "/\" q [= r & p in F & q in H ) } or x in <.(F \/ H).) )
assume x in { r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) } ; ::_thesis: x in <.(F \/ H).)
then consider r being Element of L such that
A14: x = r and
A15: ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H ) ;
A16: F \/ H c= <.(F \/ H).) by Def4;
H c= F \/ H by XBOOLE_1:7;
then A17: H c= <.(F \/ H).) by A16, XBOOLE_1:1;
consider p, q being Element of L such that
A18: p "/\" q [= r and
A19: ( p in F & q in H ) by A15;
F c= F \/ H by XBOOLE_1:7;
then F c= <.(F \/ H).) by A16, XBOOLE_1:1;
then p "/\" q in <.(F \/ H).) by A19, A17, Th8;
hence x in <.(F \/ H).) by A14, A18, Th9; ::_thesis: verum
end;
theorem Th36: :: FILTER_0:36
for L being Lattice
for F, H being Filter of L holds
( F c= F "/\" H & H c= F "/\" H )
proof
let L be Lattice; ::_thesis: for F, H being Filter of L holds
( F c= F "/\" H & H c= F "/\" H )
let F, H be Filter of L; ::_thesis: ( F c= F "/\" H & H c= F "/\" H )
A1: now__::_thesis:_for_F,_H_being_Filter_of_L_holds_F_c=_F_"/\"_H
let F, H be Filter of L; ::_thesis: F c= F "/\" H
thus F c= F "/\" H ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in F "/\" H )
assume A2: x in F ; ::_thesis: x in F "/\" H
then reconsider i = x as Element of L ;
consider p being Element of L such that
A3: p in H by SUBSET_1:4;
i [= i "\/" p by LATTICES:5;
then A4: i "/\" (i "\/" p) = i by LATTICES:4;
p [= p "\/" i by LATTICES:5;
then i "\/" p in H by A3, Th9;
hence x in F "/\" H by A2, A4; ::_thesis: verum
end;
end;
F "/\" H = H "/\" F by Th33;
hence ( F c= F "/\" H & H c= F "/\" H ) by A1; ::_thesis: verum
end;
theorem Th37: :: FILTER_0:37
for L being Lattice
for F, H being Filter of L holds <.(F \/ H).) = <.(F "/\" H).)
proof
let L be Lattice; ::_thesis: for F, H being Filter of L holds <.(F \/ H).) = <.(F "/\" H).)
let F, H be Filter of L; ::_thesis: <.(F \/ H).) = <.(F "/\" H).)
( F c= F "/\" H & H c= F "/\" H ) by Th36;
then F \/ H c= F "/\" H by XBOOLE_1:8;
hence <.(F \/ H).) c= <.(F "/\" H).) by Th22; :: according to XBOOLE_0:def_10 ::_thesis: <.(F "/\" H).) c= <.(F \/ H).)
F "/\" H c= <.(F \/ H).)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F "/\" H or x in <.(F \/ H).) )
assume x in F "/\" H ; ::_thesis: x in <.(F \/ H).)
then consider p, q being Element of L such that
A1: x = p "/\" q and
A2: p in F and
A3: q in H ;
H c= F \/ H by XBOOLE_1:7;
then A4: q in F \/ H by A3;
A5: F \/ H c= <.(F \/ H).) by Def4;
F c= F \/ H by XBOOLE_1:7;
then p in F \/ H by A2;
hence x in <.(F \/ H).) by A1, A4, A5, Th9; ::_thesis: verum
end;
then <.(F "/\" H).) c= <.<.(F \/ H).).) by Th22;
hence <.(F "/\" H).) c= <.(F \/ H).) by Th21; ::_thesis: verum
end;
theorem Th38: :: FILTER_0:38
for I being I_Lattice
for F1, F2 being Filter of I holds <.(F1 \/ F2).) = F1 "/\" F2
proof
let I be I_Lattice; ::_thesis: for F1, F2 being Filter of I holds <.(F1 \/ F2).) = F1 "/\" F2
let F1, F2 be Filter of I; ::_thesis: <.(F1 \/ F2).) = F1 "/\" F2
F1 "/\" F2 = <.(F1 "/\" F2).) by Th21;
hence <.(F1 \/ F2).) = F1 "/\" F2 by Th37; ::_thesis: verum
end;
theorem :: FILTER_0:39
for B being B_Lattice
for FB, HB being Filter of B holds <.(FB \/ HB).) = FB "/\" HB
proof
let B be B_Lattice; ::_thesis: for FB, HB being Filter of B holds <.(FB \/ HB).) = FB "/\" HB
let FB, HB be Filter of B; ::_thesis: <.(FB \/ HB).) = FB "/\" HB
FB "/\" HB = <.(FB "/\" HB).) by Th21;
hence <.(FB \/ HB).) = FB "/\" HB by Th37; ::_thesis: verum
end;
theorem Th40: :: FILTER_0:40
for I being I_Lattice
for j, i being Element of I
for DI being non empty Subset of I st j in <.(DI \/ {i}).) holds
i => j in <.DI.)
proof
let I be I_Lattice; ::_thesis: for j, i being Element of I
for DI being non empty Subset of I st j in <.(DI \/ {i}).) holds
i => j in <.DI.)
let j, i be Element of I; ::_thesis: for DI being non empty Subset of I st j in <.(DI \/ {i}).) holds
i => j in <.DI.)
let DI be non empty Subset of I; ::_thesis: ( j in <.(DI \/ {i}).) implies i => j in <.DI.) )
assume A1: j in <.(DI \/ {i}).) ; ::_thesis: i => j in <.DI.)
<.(DI \/ {i}).) = <.(<.DI.) \/ {i}).) by Th34
.= <.(<.DI.) \/ <.{i}.)).) by Th34
.= <.(<.DI.) \/ <.i.)).) by Th24
.= <.DI.) "/\" <.i.) by Th38 ;
then consider i1, i2 being Element of I such that
A2: j = i1 "/\" i2 and
A3: i1 in <.DI.) and
A4: i2 in <.i.) by A1;
i [= i2 by A4, Th15;
then i1 "/\" i [= i1 "/\" i2 by LATTICES:9;
then i1 [= i => j by A2, Def7;
hence i => j in <.DI.) by A3, Th9; ::_thesis: verum
end;
theorem Th41: :: FILTER_0:41
for I being I_Lattice
for i, j, k being Element of I
for FI being Filter of I st i => j in FI & j => k in FI holds
i => k in FI
proof
let I be I_Lattice; ::_thesis: for i, j, k being Element of I
for FI being Filter of I st i => j in FI & j => k in FI holds
i => k in FI
let i, j, k be Element of I; ::_thesis: for FI being Filter of I st i => j in FI & j => k in FI holds
i => k in FI
let FI be Filter of I; ::_thesis: ( i => j in FI & j => k in FI implies i => k in FI )
assume that
A1: i => j in FI and
A2: j => k in FI ; ::_thesis: i => k in FI
A3: FI \/ {i} c= <.(FI \/ {i}).) by Def4;
{i} c= FI \/ {i} by XBOOLE_1:7;
then A4: {i} c= <.(FI \/ {i}).) by A3, XBOOLE_1:1;
FI c= FI \/ {i} by XBOOLE_1:7;
then A5: FI c= <.(FI \/ {i}).) by A3, XBOOLE_1:1;
i in {i} by TARSKI:def_1;
then j in <.(FI \/ {i}).) by A1, A5, A4, Th29;
then A6: k in <.(FI \/ {i}).) by A2, A5, Th29;
<.FI.) = FI by Th21;
hence i => k in FI by A6, Th40; ::_thesis: verum
end;
theorem Th42: :: FILTER_0:42
for B being B_Lattice
for a, b being Element of B holds a => b = (a `) "\/" b
proof
let B be B_Lattice; ::_thesis: for a, b being Element of B holds a => b = (a `) "\/" b
let a, b be Element of B; ::_thesis: a => b = (a `) "\/" b
( a "/\" ((a `) "\/" b) [= b & ( for c being Element of B st a "/\" c [= b holds
c [= (a `) "\/" b ) ) by Th27;
hence a => b = (a `) "\/" b by Def7; ::_thesis: verum
end;
theorem Th43: :: FILTER_0:43
for B being B_Lattice
for a, b being Element of B holds
( a [= b iff a "/\" (b `) = Bottom B )
proof
let B be B_Lattice; ::_thesis: for a, b being Element of B holds
( a [= b iff a "/\" (b `) = Bottom B )
let a, b be Element of B; ::_thesis: ( a [= b iff a "/\" (b `) = Bottom B )
reconsider B9 = B as 0_Lattice ;
reconsider B99 = B as 1_Lattice ;
reconsider D = B as D_Lattice ;
reconsider a9 = a, b9 = b, c9 = a "/\" (b `) as Element of B9 ;
reconsider a99 = a, b99 = b as Element of B99 ;
reconsider a1 = a, b1 = b as Element of D ;
thus ( a [= b implies a "/\" (b `) = Bottom B ) ::_thesis: ( a "/\" (b `) = Bottom B implies a [= b )
proof
assume a [= b ; ::_thesis: a "/\" (b `) = Bottom B
then a = a "/\" b by LATTICES:4;
hence a "/\" (b `) = a "/\" (b "/\" (b `)) by LATTICES:def_7
.= a9 "/\" (Bottom B9) by LATTICES:20
.= Bottom B ;
::_thesis: verum
end;
assume a "/\" (b `) = Bottom B ; ::_thesis: a [= b
then b = b9 "\/" c9 by LATTICES:14
.= (b1 "\/" a1) "/\" (b1 "\/" (b1 `)) by LATTICES:11
.= (b99 "\/" a99) "/\" (Top B99) by LATTICES:21
.= a "\/" b ;
hence a [= b by LATTICES:def_3; ::_thesis: verum
end;
theorem Th44: :: FILTER_0:44
for B being B_Lattice
for FB being Filter of B holds
( FB is being_ultrafilter iff ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) ) )
proof
let B be B_Lattice; ::_thesis: for FB being Filter of B holds
( FB is being_ultrafilter iff ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) ) )
let FB be Filter of B; ::_thesis: ( FB is being_ultrafilter iff ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) ) )
thus ( FB is being_ultrafilter implies ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) ) ) ::_thesis: ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) implies FB is being_ultrafilter )
proof
reconsider I = B as I_Lattice ;
assume that
A1: FB <> the carrier of B and
A2: for HB being Filter of B st FB c= HB & HB <> the carrier of B holds
FB = HB ; :: according to FILTER_0:def_3 ::_thesis: ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) )
thus FB <> the carrier of B by A1; ::_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 )
assume A3: not a in FB ; ::_thesis: a ` in FB
A4: a in <.a.) ;
A5: FB \/ <.a.) c= <.(FB \/ <.a.)).) by Def4;
<.a.) c= FB \/ <.a.) by XBOOLE_1:7;
then <.a.) c= <.(FB \/ <.a.)).) by A5, XBOOLE_1:1;
then ( FB c= FB \/ <.a.) & FB <> <.(FB \/ <.a.)).) ) by A3, A4, XBOOLE_1:7;
then <.(FB \/ <.a.)).) = the carrier of B by A2, A5, XBOOLE_1:1;
then A6: a ` in <.(FB \/ <.a.)).) ;
reconsider a9 = a as Element of I ;
reconsider FI = FB as Filter of I ;
A7: a => (a `) = (a `) "\/" (a `) by Th42;
<.{a}.) = <.a.) by Th24;
then A8: a9 ` in <.(FI \/ {a9}).) by A6, Th34;
FB = <.FB.) by Th21;
then a => (a `) in FB by A8, Th40;
hence a ` in FB by A7; ::_thesis: verum
end;
assume that
A9: FB <> the carrier of B and
A10: for a being Element of B holds
( a in FB or a ` in FB ) ; ::_thesis: FB is being_ultrafilter
thus FB <> the carrier of B by A9; :: according to FILTER_0:def_3 ::_thesis: for H being Filter of B st FB c= H & H <> the carrier of B holds
FB = H
let HB be Filter of B; ::_thesis: ( FB c= HB & HB <> the carrier of B implies FB = HB )
assume that
A11: FB c= HB and
A12: HB <> the carrier of B and
A13: FB <> HB ; ::_thesis: contradiction
not for x being set holds
( x in FB iff x in HB ) by A13, TARSKI:1;
then consider x being set such that
A14: x in HB and
A15: not x in FB by A11;
reconsider x = x as Element of HB by A14;
x ` in FB by A10, A15;
then (x `) "/\" x in HB by A11, Th8;
then A16: Bottom B in HB by LATTICES:20;
HB = <.HB.) by Th21;
hence contradiction by A12, A16, Th25; ::_thesis: verum
end;
theorem :: FILTER_0:45
for B being B_Lattice
for FB being Filter of B holds
( ( FB <> <.B.) & FB is prime ) iff FB is being_ultrafilter )
proof
let B be B_Lattice; ::_thesis: for FB being Filter of B holds
( ( FB <> <.B.) & FB is prime ) iff FB is being_ultrafilter )
let FB be Filter of B; ::_thesis: ( ( FB <> <.B.) & FB is prime ) iff FB is being_ultrafilter )
thus ( FB <> <.B.) & FB is prime implies FB is being_ultrafilter ) ::_thesis: ( FB is being_ultrafilter implies ( FB <> <.B.) & FB is prime ) )
proof
assume that
A1: FB <> <.B.) and
A2: for a, b being Element of B holds
( a "\/" b in FB iff ( a in FB or b in FB ) ) ; :: according to FILTER_0:def_5 ::_thesis: FB is being_ultrafilter
now__::_thesis:_for_a_being_Element_of_B_st_not_a_in_FB_holds_
a_`_in_FB
let a be Element of B; ::_thesis: ( not a in FB implies a ` in FB )
assume A3: not a in FB ; ::_thesis: a ` in FB
a "\/" (a `) = Top B by LATTICES:21;
then a "\/" (a `) in FB by Th11;
hence a ` in FB by A2, A3; ::_thesis: verum
end;
hence FB is being_ultrafilter by A1, Th44; ::_thesis: verum
end;
assume A4: FB is being_ultrafilter ; ::_thesis: ( FB <> <.B.) & FB is prime )
hence FB <> <.B.) by Th44; ::_thesis: FB is prime
let a be Element of B; :: according to FILTER_0:def_5 ::_thesis: for q being Element of B holds
( a "\/" q in FB iff ( a in FB or q in FB ) )
let b be Element of B; ::_thesis: ( a "\/" b in FB iff ( a in FB or b in FB ) )
A5: FB <> the carrier of B by A4, Th44;
thus ( not a "\/" b in FB or a in FB or b in FB ) ::_thesis: ( ( a in FB or b in FB ) implies a "\/" b in FB )
proof
assume that
A6: a "\/" b in FB and
A7: ( not a in FB & not b in FB ) ; ::_thesis: contradiction
( a ` in FB & b ` in FB ) by A4, A7, Th44;
then (a `) "/\" (b `) in FB by Th8;
then (a "\/" b) ` in FB by LATTICES:24;
then (a "\/" b) "/\" ((a "\/" b) `) in FB by A6, Th8;
then A8: Bottom B in FB by LATTICES:20;
FB = <.FB.) by Th21;
hence contradiction by A5, A8, Th25; ::_thesis: verum
end;
thus ( ( a in FB or b in FB ) implies a "\/" b in FB ) by Th10; ::_thesis: verum
end;
theorem Th46: :: FILTER_0:46
for B being B_Lattice
for FB being Filter of B st FB is being_ultrafilter holds
for a being Element of B holds
( a in FB iff not a ` in FB )
proof
let B be B_Lattice; ::_thesis: for FB being Filter of B st FB is being_ultrafilter holds
for a being Element of B holds
( a in FB iff not a ` in FB )
let FB be Filter of B; ::_thesis: ( FB is being_ultrafilter implies for a being Element of B holds
( a in FB iff not a ` in FB ) )
assume A1: FB is being_ultrafilter ; ::_thesis: for a being Element of B holds
( a in FB iff not a ` in FB )
let a be Element of B; ::_thesis: ( a in FB iff not a ` in FB )
thus ( a in FB implies not a ` in FB ) ::_thesis: ( not a ` in FB implies a in FB )
proof
assume ( a in FB & a ` in FB ) ; ::_thesis: contradiction
then a "/\" (a `) in FB by Th8;
then Bottom B in FB by LATTICES:20;
then FB = the carrier of B by Th26;
hence contradiction by A1, Def3; ::_thesis: verum
end;
thus ( not a ` in FB implies a in FB ) by A1, Th44; ::_thesis: verum
end;
theorem :: FILTER_0:47
for B being B_Lattice
for a, b being Element of B st a <> b holds
ex FB being Filter of B st
( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) )
proof
let B be B_Lattice; ::_thesis: for a, b being Element of B st a <> b holds
ex FB being Filter of B st
( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) )
let a, b be Element of B; ::_thesis: ( a <> b implies ex FB being Filter of B st
( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) ) )
assume a <> b ; ::_thesis: ex FB being Filter of B st
( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) )
then ( not a [= b or not b [= a ) by LATTICES:8;
then ( a "/\" (b `) <> Bottom B or b "/\" (a `) <> Bottom B ) by Th43;
then ( ex FB being Filter of B st
( a "/\" (b `) in FB & FB is being_ultrafilter ) or ex FB being Filter of B st
( b "/\" (a `) in FB & FB is being_ultrafilter ) ) by Th20;
then consider FB being Filter of B such that
A1: FB is being_ultrafilter and
A2: ( a "/\" (b `) in FB or b "/\" (a `) in FB ) ;
take FB ; ::_thesis: ( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) )
thus FB is being_ultrafilter by A1; ::_thesis: ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) )
( ( a in FB & b ` in FB ) or ( b in FB & a ` in FB ) ) by A2, Th8;
hence ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) by A1, Th46; ::_thesis: verum
end;
definition
let L be Lattice;
let F be Filter of L;
func latt F -> Lattice means :Def9: :: FILTER_0:def 9
ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & it = LattStr(# F,o1,o2 #) );
uniqueness
for b1, b2 being Lattice st ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & b1 = LattStr(# F,o1,o2 #) ) & ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & b2 = LattStr(# F,o1,o2 #) ) holds
b1 = b2 ;
existence
ex b1 being Lattice ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & b1 = LattStr(# F,o1,o2 #) )
proof
reconsider o1 = the L_join of L || F, o2 = the L_meet of L || F as Function of [:F,F:], the carrier of L by FUNCT_2:32;
A1: dom o1 = [:F,F:] by FUNCT_2:def_1;
rng o1 c= F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng o1 or y in F )
assume y in rng o1 ; ::_thesis: y in F
then consider x being set such that
A2: x in dom o1 and
A3: y = o1 . x by FUNCT_1:def_3;
reconsider p = x `1 , q = x `2 as Element of F by A2, MCART_1:10;
x = [(x `1),(x `2)] by A2, MCART_1:21;
then o1 . x = p "\/" q by A2, FUNCT_1:47;
hence y in F by A3, Th10; ::_thesis: verum
end;
then reconsider o1 = o1 as Function of [:F,F:],F by A1, FUNCT_2:def_1, RELSET_1:4;
A4: dom o2 = [:F,F:] by FUNCT_2:def_1;
rng o2 c= F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng o2 or y in F )
assume y in rng o2 ; ::_thesis: y in F
then consider x being set such that
A5: x in dom o2 and
A6: y = o2 . x by FUNCT_1:def_3;
reconsider p = x `1 , q = x `2 as Element of F by A5, MCART_1:10;
x = [(x `1),(x `2)] by A5, MCART_1:21;
then o2 . x = p "/\" q by A5, FUNCT_1:47;
hence y in F by A6, Th8; ::_thesis: verum
end;
then reconsider o2 = o2 as Function of [:F,F:],F by A4, FUNCT_2:def_1, RELSET_1:4;
reconsider K = LattStr(# F,o1,o2 #) as non empty LattStr ;
A7: for a, b being Element of K holds
( the L_join of K . (a,b) = the L_join of L . (a,b) & the L_meet of K . (a,b) = the L_meet of L . (a,b) )
proof
let a, b be Element of K; ::_thesis: ( the L_join of K . (a,b) = the L_join of L . (a,b) & the L_meet of K . (a,b) = the L_meet of L . (a,b) )
the L_join of K . (a,b) = the L_join of K . [a,b] ;
hence ( the L_join of K . (a,b) = the L_join of L . (a,b) & the L_meet of K . (a,b) = the L_meet of L . (a,b) ) by A1, A4, FUNCT_1:47; ::_thesis: verum
end;
A8: for a, b, c being Element of K holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let a, b, c be Element of K; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider a9 = a, b9 = b, c9 = c as Element of F ;
thus a "/\" (b "/\" c) = the L_meet of L . (a,(b "/\" c)) by A7
.= a9 "/\" (b9 "/\" c9) by A7
.= (a9 "/\" b9) "/\" c9 by LATTICES:def_7
.= the L_meet of L . ((a "/\" b),c) by A7
.= (a "/\" b) "/\" c by A7 ; ::_thesis: verum
end;
A9: for a, b being Element of K holds a "/\" (a "\/" b) = a
proof
let a, b be Element of K; ::_thesis: a "/\" (a "\/" b) = a
reconsider a9 = a, b9 = b as Element of F ;
thus a "/\" (a "\/" b) = the L_meet of L . (a,(a "\/" b)) by A7
.= a9 "/\" (a9 "\/" b9) by A7
.= a by LATTICES:def_9 ; ::_thesis: verum
end;
A10: for a, b being Element of K holds a "/\" b = b "/\" a
proof
let a, b be Element of K; ::_thesis: a "/\" b = b "/\" a
reconsider a9 = a, b9 = b as Element of F ;
thus a "/\" b = the L_meet of L . (a9,b9) by A7
.= b9 "/\" a9 by LATTICES:def_2
.= b "/\" a by A7 ; ::_thesis: verum
end;
A11: for a, b being Element of K holds (a "/\" b) "\/" b = b
proof
let a, b be Element of K; ::_thesis: (a "/\" b) "\/" b = b
reconsider a9 = a, b9 = b as Element of F ;
thus (a "/\" b) "\/" b = the L_join of L . ((a "/\" b),b) by A7
.= (a9 "/\" b9) "\/" b9 by A7
.= b by LATTICES:def_8 ; ::_thesis: verum
end;
A12: for a, b being Element of K holds a "\/" b = b "\/" a
proof
let a, b be Element of K; ::_thesis: a "\/" b = b "\/" a
reconsider a9 = a, b9 = b as Element of F ;
thus a "\/" b = the L_join of L . (a9,b9) by A7
.= b9 "\/" a9 by LATTICES:def_1
.= b "\/" a by A7 ; ::_thesis: verum
end;
for a, b, c being Element of K holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let a, b, c be Element of K; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider a9 = a, b9 = b, c9 = c as Element of F ;
thus a "\/" (b "\/" c) = the L_join of L . (a,(b "\/" c)) by A7
.= a9 "\/" (b9 "\/" c9) by A7
.= (a9 "\/" b9) "\/" c9 by LATTICES:def_5
.= the L_join of L . ((a "\/" b),c) by A7
.= (a "\/" b) "\/" c by A7 ; ::_thesis: verum
end;
then ( K is join-commutative & K is join-associative & K is meet-absorbing & K is meet-commutative & K is meet-associative & K is join-absorbing ) by A12, A11, A10, A8, A9, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
then reconsider Q = K as Lattice ;
take Q ; ::_thesis: ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & Q = LattStr(# F,o1,o2 #) )
take o1 ; ::_thesis: ex o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & Q = LattStr(# F,o1,o2 #) )
take o2 ; ::_thesis: ( o1 = the L_join of L || F & o2 = the L_meet of L || F & Q = LattStr(# F,o1,o2 #) )
thus ( o1 = the L_join of L || F & o2 = the L_meet of L || F & Q = LattStr(# F,o1,o2 #) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines latt FILTER_0:def_9_:_
for L being Lattice
for F being Filter of L
for b3 being Lattice holds
( b3 = latt F iff ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & b3 = LattStr(# F,o1,o2 #) ) );
registration
let L be Lattice;
let F be Filter of L;
cluster latt F -> strict ;
coherence
latt F is strict
proof
ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & latt F = LattStr(# F,o1,o2 #) ) by Def9;
hence latt F is strict ; ::_thesis: verum
end;
end;
theorem :: FILTER_0:48
for L being strict Lattice holds latt <.L.) = L
proof
let L be strict Lattice; ::_thesis: latt <.L.) = L
dom the L_meet of L = [: the carrier of L, the carrier of L:] by FUNCT_2:def_1;
then A1: the L_meet of L = the L_meet of L || the carrier of L by RELAT_1:68;
dom the L_join of L = [: the carrier of L, the carrier of L:] by FUNCT_2:def_1;
then the L_join of L = the L_join of L || the carrier of L by RELAT_1:68;
hence latt <.L.) = L by A1, Def9; ::_thesis: verum
end;
theorem Th49: :: FILTER_0:49
for L being Lattice
for F being Filter of L holds
( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F )
proof
let L be Lattice; ::_thesis: for F being Filter of L holds
( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F )
let F be Filter of L; ::_thesis: ( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F )
ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & latt F = LattStr(# F,o1,o2 #) ) by Def9;
hence ( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F ) ; ::_thesis: verum
end;
theorem Th50: :: FILTER_0:50
for L being Lattice
for p, q being Element of L
for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
proof
let L be Lattice; ::_thesis: for p, q being Element of L
for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let p, q be Element of L; ::_thesis: for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let F be Filter of L; ::_thesis: for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let p9, q9 be Element of (latt F); ::_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 F such that
A2: o1 = the L_join of L || F and
A3: o2 = the L_meet of L || F and
A4: latt F = LattStr(# F,o1,o2 #) by Def9;
dom o1 = [:F,F:] by FUNCT_2:def_1;
then [p,q] in dom o1 by A1, A4, ZFMISC_1:87;
hence p "\/" q = p9 "\/" q9 by A1, A2, A4, FUNCT_1:47; ::_thesis: p "/\" q = p9 "/\" q9
dom o2 = [:F,F:] by FUNCT_2:def_1;
then [p,q] in dom o2 by A1, A4, ZFMISC_1:87;
hence p "/\" q = p9 "/\" q9 by A1, A3, A4, FUNCT_1:47; ::_thesis: verum
end;
theorem Th51: :: FILTER_0:51
for L being Lattice
for p, q being Element of L
for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
proof
let L be Lattice; ::_thesis: for p, q being Element of L
for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
let p, q be Element of L; ::_thesis: for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
let F be Filter of L; ::_thesis: for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
let p9, q9 be Element of (latt F); ::_thesis: ( p = p9 & q = q9 implies ( p [= q iff p9 [= q9 ) )
A1: ( p [= q iff p "\/" q = q ) by LATTICES:def_3;
A2: ( p9 [= q9 iff p9 "\/" q9 = q9 ) by LATTICES:def_3;
assume ( p = p9 & q = q9 ) ; ::_thesis: ( p [= q iff p9 [= q9 )
hence ( p [= q iff p9 [= q9 ) by A1, A2, Th50; ::_thesis: verum
end;
theorem Th52: :: FILTER_0:52
for L being Lattice
for F being Filter of L st L is upper-bounded holds
latt F is upper-bounded
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is upper-bounded holds
latt F is upper-bounded
let F be Filter of L; ::_thesis: ( L is upper-bounded implies latt F is upper-bounded )
given p being Element of L such that A1: for q being Element of L holds
( p "\/" q = p & q "\/" p = p ) ; :: according to LATTICES:def_14 ::_thesis: latt F is upper-bounded
consider q being Element of L such that
A2: q in F by SUBSET_1:4;
A3: ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & latt F = LattStr(# F,o1,o2 #) ) by Def9;
p "\/" q = p by A1;
then reconsider p9 = p as Element of (latt F) by A2, A3, Th10;
take p9 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (latt F) holds
( p9 "\/" b1 = p9 & b1 "\/" p9 = p9 )
let r be Element of (latt F); ::_thesis: ( p9 "\/" r = p9 & r "\/" p9 = p9 )
reconsider r9 = r as Element of F by A3;
thus p9 "\/" r = p "\/" r9 by Th50
.= p9 by A1 ; ::_thesis: r "\/" p9 = p9
hence r "\/" p9 = p9 ; ::_thesis: verum
end;
theorem :: FILTER_0:53
for L being Lattice
for F being Filter of L st L is modular holds
latt F is modular
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is modular holds
latt F is modular
let F be Filter of L; ::_thesis: ( L is modular implies latt F 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 F is modular
let a, b, c be Element of (latt F); :: according to LATTICES:def_12 ::_thesis: ( not a [= c or a "\/" (b "/\" c) = (a "\/" b) "/\" c )
assume A2: a [= c ; ::_thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" c
reconsider p = a, q = b, r = c as Element of F by Th49;
b "/\" c = q "/\" r by Th50;
then A3: a "\/" (b "/\" c) = p "\/" (q "/\" r) by Th50;
a "\/" b = p "\/" q by Th50;
then A4: (a "\/" b) "/\" c = (p "\/" q) "/\" r by Th50;
p [= r by A2, Th51;
hence a "\/" (b "/\" c) = (a "\/" b) "/\" c by A1, A3, A4; ::_thesis: verum
end;
theorem Th54: :: FILTER_0:54
for L being Lattice
for F being Filter of L st L is distributive holds
latt F is distributive
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is distributive holds
latt F is distributive
let F be Filter of L; ::_thesis: ( L is distributive implies latt F is distributive )
assume A1: for p, q, r being Element of L holds p "/\" (q "\/" r) = (p "/\" q) "\/" (p "/\" r) ; :: according to LATTICES:def_11 ::_thesis: latt F is distributive
let p9, q9, r9 be Element of (latt F); :: according to LATTICES:def_11 ::_thesis: p9 "/\" (q9 "\/" r9) = (p9 "/\" q9) "\/" (p9 "/\" r9)
reconsider p = p9, q = q9, r = r9, qr = q9 "\/" r9 as Element of F by Th49;
A2: ( p9 "/\" q9 = p "/\" q & p9 "/\" r9 = p "/\" r ) by Th50;
thus p9 "/\" (q9 "\/" r9) = p "/\" qr by Th50
.= p "/\" (q "\/" r) by Th50
.= (p "/\" q) "\/" (p "/\" r) by A1
.= (p9 "/\" q9) "\/" (p9 "/\" r9) by A2, Th50 ; ::_thesis: verum
end;
theorem :: FILTER_0:55
for L being Lattice
for F being Filter of L st L is I_Lattice holds
latt F is implicative
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds
latt F is implicative
let F be Filter of L; ::_thesis: ( L is I_Lattice implies latt F is implicative )
assume A1: L is I_Lattice ; ::_thesis: latt F is implicative
then reconsider I = L as I_Lattice ;
reconsider FI = F as Filter of I ;
let p9, q9 be Element of (latt F); :: according to FILTER_0:def_6 ::_thesis: ex r being Element of (latt F) st
( p9 "/\" r [= q9 & ( for r1 being Element of (latt F) st p9 "/\" r1 [= q9 holds
r1 [= r ) )
reconsider p = p9, q = q9 as Element of F by Th49;
consider r being Element of L such that
A2: p "/\" r [= q and
A3: for r1 being Element of L st p "/\" r1 [= q holds
r1 [= r by A1, Def6;
reconsider i = p, j = q as Element of I ;
A4: i => j in FI by Th30;
i => j = r by A2, A3, Def7;
then reconsider r9 = r as Element of (latt F) by A4, Th49;
take r9 ; ::_thesis: ( p9 "/\" r9 [= q9 & ( for r1 being Element of (latt F) st p9 "/\" r1 [= q9 holds
r1 [= r9 ) )
p "/\" r = p9 "/\" r9 by Th50;
hence p9 "/\" r9 [= q9 by A2, Th51; ::_thesis: for r1 being Element of (latt F) st p9 "/\" r1 [= q9 holds
r1 [= r9
let s9 be Element of (latt F); ::_thesis: ( p9 "/\" s9 [= q9 implies s9 [= r9 )
assume A5: p9 "/\" s9 [= q9 ; ::_thesis: s9 [= r9
reconsider s = s9 as Element of F by Th49;
p "/\" s = p9 "/\" s9 by Th50;
then p "/\" s [= q by A5, Th51;
then s [= r by A3;
hence s9 [= r9 by Th51; ::_thesis: verum
end;
registration
let L be Lattice;
let p be Element of L;
cluster latt <.p.) -> lower-bounded ;
coherence
latt <.p.) is lower-bounded
proof
the carrier of (latt <.p.)) = <.p.) by Th49;
then reconsider p9 = p as Element of (latt <.p.)) by Th16;
take p9 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (latt <.p.)) holds
( p9 "/\" b1 = p9 & b1 "/\" p9 = p9 )
let q9 be Element of (latt <.p.)); ::_thesis: ( p9 "/\" q9 = p9 & q9 "/\" p9 = p9 )
reconsider q = q9 as Element of <.p.) by Th49;
p [= q by Th15;
then p "/\" q = p by LATTICES:4;
hence ( p9 "/\" q9 = p9 & q9 "/\" p9 = p9 ) by Th50; ::_thesis: verum
end;
end;
theorem Th56: :: FILTER_0:56
for L being Lattice
for p being Element of L holds Bottom (latt <.p.)) = p
proof
let L be Lattice; ::_thesis: for p being Element of L holds Bottom (latt <.p.)) = p
let p be Element of L; ::_thesis: Bottom (latt <.p.)) = p
consider q9 being Element of (latt <.p.)) such that
A1: for r9 being Element of (latt <.p.)) holds
( q9 "/\" r9 = q9 & r9 "/\" q9 = q9 ) by LATTICES:def_13;
the carrier of (latt <.p.)) = <.p.) by Th49;
then reconsider p9 = p as Element of (latt <.p.)) by Th16;
reconsider q = q9 as Element of <.p.) by Th49;
q9 "/\" p9 = q9 by A1;
then q9 [= p9 by LATTICES:4;
then A2: q [= p by Th51;
A3: p [= q by Th15;
q9 = Bottom (latt <.p.)) by A1, RLSUB_2:64;
hence Bottom (latt <.p.)) = p by A2, A3, LATTICES:8; ::_thesis: verum
end;
theorem Th57: :: FILTER_0:57
for L being Lattice
for p being Element of L st L is upper-bounded holds
Top (latt <.p.)) = Top L
proof
let L be Lattice; ::_thesis: for p being Element of L st L is upper-bounded holds
Top (latt <.p.)) = Top L
let p be Element of L; ::_thesis: ( L is upper-bounded implies Top (latt <.p.)) = Top L )
given q being Element of L such that A1: for r being Element of L holds
( q "\/" r = q & r "\/" q = q ) ; :: according to LATTICES:def_14 ::_thesis: Top (latt <.p.)) = Top L
L is 1_Lattice by A1, LATTICES:def_14;
then Top L in <.p.) by Th11;
then reconsider q9 = Top L as Element of (latt <.p.)) by Th49;
A2: q = Top L by A1, RLSUB_2:65;
now__::_thesis:_for_r9_being_Element_of_(latt_<.p.))_holds_r9_"\/"_q9_=_q9
let r9 be Element of (latt <.p.)); ::_thesis: r9 "\/" q9 = q9
reconsider r = r9 as Element of <.p.) by Th49;
thus r9 "\/" q9 = q "\/" r by A2, Th50
.= q9 by A1, A2 ; ::_thesis: verum
end;
hence Top (latt <.p.)) = Top L by RLSUB_2:65; ::_thesis: verum
end;
theorem Th58: :: FILTER_0:58
for L being Lattice
for p being Element of L st L is 1_Lattice holds
latt <.p.) is bounded
proof
let L be Lattice; ::_thesis: for p being Element of L st L is 1_Lattice holds
latt <.p.) is bounded
let p be Element of L; ::_thesis: ( L is 1_Lattice implies latt <.p.) is bounded )
assume L is 1_Lattice ; ::_thesis: latt <.p.) is bounded
hence ( latt <.p.) is lower-bounded & latt <.p.) is upper-bounded ) by Th52; :: according to LATTICES:def_15 ::_thesis: verum
end;
theorem Th59: :: FILTER_0:59
for L being Lattice
for p being Element of L st L is C_Lattice & L is M_Lattice holds
latt <.p.) is C_Lattice
proof
let L be Lattice; ::_thesis: for p being Element of L st L is C_Lattice & L is M_Lattice holds
latt <.p.) is C_Lattice
let p be Element of L; ::_thesis: ( L is C_Lattice & L is M_Lattice implies latt <.p.) is C_Lattice )
assume that
A1: L is C_Lattice and
A2: L is M_Lattice ; ::_thesis: latt <.p.) is C_Lattice
reconsider B = L as C_Lattice by A1;
reconsider M = latt <.p.) as 01_Lattice by A1, Th58;
M is complemented
proof
let r9 be Element of M; :: according to LATTICES:def_19 ::_thesis: ex b1 being Element of the carrier of M st b1 is_a_complement_of r9
reconsider r = r9 as Element of <.p.) by Th49;
reconsider p1 = p as Element of B ;
consider q being Element of L such that
A3: q is_a_complement_of r by A1, LATTICES:def_19;
the carrier of (latt <.p.)) = <.p.) by Th49;
then reconsider q9 = p "\/" q as Element of M by Th16;
take q9 ; ::_thesis: q9 is_a_complement_of r9
thus q9 "\/" r9 = (p "\/" q) "\/" r by Th50
.= p "\/" (q "\/" r) by LATTICES:def_5
.= p1 "\/" (Top B) by A3, LATTICES:def_18
.= Top L
.= Top M by A1, Th57 ; :: according to LATTICES:def_18 ::_thesis: ( r9 "\/" q9 = Top M & q9 "/\" r9 = Bottom M & r9 "/\" q9 = Bottom M )
hence r9 "\/" q9 = Top M ; ::_thesis: ( q9 "/\" r9 = Bottom M & r9 "/\" q9 = Bottom M )
p [= r by Th15;
then (p "\/" q) "/\" r = p "\/" (q "/\" r) by A2, LATTICES:def_12;
hence q9 "/\" r9 = p "\/" (q "/\" r) by Th50
.= p1 "\/" (Bottom B) by A3, LATTICES:def_18
.= p
.= Bottom M by Th56 ;
::_thesis: r9 "/\" q9 = Bottom M
hence r9 "/\" q9 = Bottom M ; ::_thesis: verum
end;
hence latt <.p.) is C_Lattice ; ::_thesis: verum
end;
theorem :: FILTER_0:60
for L being Lattice
for p being Element of L st L is B_Lattice holds
latt <.p.) is B_Lattice
proof
let L be Lattice; ::_thesis: for p being Element of L st L is B_Lattice holds
latt <.p.) is B_Lattice
let p be Element of L; ::_thesis: ( L is B_Lattice implies latt <.p.) is B_Lattice )
assume L is B_Lattice ; ::_thesis: latt <.p.) is B_Lattice
then latt <.p.) is distributive bounded complemented Lattice by Th54, Th59;
hence latt <.p.) is B_Lattice ; ::_thesis: verum
end;
definition
let L be Lattice;
let p, q be Element of L;
funcp <=> q -> Element of L equals :: FILTER_0:def 10
(p => q) "/\" (q => p);
correctness
coherence
(p => q) "/\" (q => p) is Element of L;
;
end;
:: deftheorem defines <=> FILTER_0:def_10_:_
for L being Lattice
for p, q being Element of L holds p <=> q = (p => q) "/\" (q => p);
theorem :: FILTER_0:61
for L being Lattice
for p, q being Element of L holds p <=> q = q <=> p ;
theorem Th62: :: FILTER_0:62
for I being I_Lattice
for i, j, k being Element of I
for FI being Filter of I st i <=> j in FI & j <=> k in FI holds
i <=> k in FI
proof
let I be I_Lattice; ::_thesis: for i, j, k being Element of I
for FI being Filter of I st i <=> j in FI & j <=> k in FI holds
i <=> k in FI
let i, j, k be Element of I; ::_thesis: for FI being Filter of I st i <=> j in FI & j <=> k in FI holds
i <=> k in FI
let FI be Filter of I; ::_thesis: ( i <=> j in FI & j <=> k in FI implies i <=> k in FI )
assume A1: ( i <=> j in FI & j <=> k in FI ) ; ::_thesis: i <=> k in FI
then ( j => i in FI & k => j in FI ) by Th8;
then A2: k => i in FI by Th41;
( i => j in FI & j => k in FI ) by A1, Th8;
then i => k in FI by Th41;
hence i <=> k in FI by A2, Th8; ::_thesis: verum
end;
definition
let L be Lattice;
let F be Filter of L;
func equivalence_wrt F -> Relation means :Def11: :: FILTER_0:def 11
( field it c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in it iff p <=> q in F ) ) );
existence
ex b1 being Relation st
( field b1 c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in b1 iff p <=> q in F ) ) )
proof
defpred S1[ set , set ] means ex p, q being Element of L st
( $1 = p & $2 = q & p <=> q in F );
consider R being Relation such that
A1: for x, y being set holds
( [x,y] in R iff ( x in the carrier of L & y in the carrier of L & S1[x,y] ) ) from RELAT_1:sch_1();
take R ; ::_thesis: ( field R c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in R iff p <=> q in F ) ) )
thus field R c= the carrier of L ::_thesis: for p, q being Element of L holds
( [p,q] in R iff p <=> q in F )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in field R or x in the carrier of L )
assume x in field R ; ::_thesis: x in the carrier of L
then ex y being set st
( [x,y] in R or [y,x] in R ) by WELLSET1:1;
hence x in the carrier of L by A1; ::_thesis: verum
end;
let p, q be Element of L; ::_thesis: ( [p,q] in R iff p <=> q in F )
thus ( [p,q] in R implies p <=> q in F ) ::_thesis: ( p <=> q in F implies [p,q] in R )
proof
assume [p,q] in R ; ::_thesis: p <=> q in F
then ex p1, q1 being Element of L st
( p = p1 & q = q1 & p1 <=> q1 in F ) by A1;
hence p <=> q in F ; ::_thesis: verum
end;
thus ( p <=> q in F implies [p,q] in R ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Relation st field b1 c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in b1 iff p <=> q in F ) ) & field b2 c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in b2 iff p <=> q in F ) ) holds
b1 = b2
proof
let R1, R2 be Relation; ::_thesis: ( field R1 c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in R1 iff p <=> q in F ) ) & field R2 c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in R2 iff p <=> q in F ) ) implies R1 = R2 )
assume that
A2: field R1 c= the carrier of L and
A3: for p, q being Element of L holds
( [p,q] in R1 iff p <=> q in F ) and
A4: field R2 c= the carrier of L and
A5: for p, q being Element of L holds
( [p,q] in R2 iff p <=> q in F ) ; ::_thesis: R1 = R2
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in R1 or [x,b1] in R2 ) & ( not [x,b1] in R2 or [x,b1] in R1 ) )
let y be set ; ::_thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) )
thus ( [x,y] in R1 implies [x,y] in R2 ) ::_thesis: ( not [x,y] in R2 or [x,y] in R1 )
proof
assume A6: [x,y] in R1 ; ::_thesis: [x,y] in R2
then ( x in field R1 & y in field R1 ) by RELAT_1:15;
then reconsider p = x, q = y as Element of L by A2;
p <=> q in F by A3, A6;
hence [x,y] in R2 by A5; ::_thesis: verum
end;
assume A7: [x,y] in R2 ; ::_thesis: [x,y] in R1
then ( x in field R2 & y in field R2 ) by RELAT_1:15;
then reconsider p = x, q = y as Element of L by A4;
p <=> q in F by A5, A7;
hence [x,y] in R1 by A3; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines equivalence_wrt FILTER_0:def_11_:_
for L being Lattice
for F being Filter of L
for b3 being Relation holds
( b3 = equivalence_wrt F iff ( field b3 c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in b3 iff p <=> q in F ) ) ) );
theorem Th63: :: FILTER_0:63
for L being Lattice
for F being Filter of L holds equivalence_wrt F is Relation of the carrier of L
proof
let L be Lattice; ::_thesis: for F being Filter of L holds equivalence_wrt F is Relation of the carrier of L
let F be Filter of L; ::_thesis: equivalence_wrt F is Relation of the carrier of L
equivalence_wrt F c= [: the carrier of L, the carrier of L:]
proof
let y be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [y,b1] in equivalence_wrt F or [y,b1] in [: the carrier of L, the carrier of L:] )
let z be set ; ::_thesis: ( not [y,z] in equivalence_wrt F or [y,z] in [: the carrier of L, the carrier of L:] )
assume [y,z] in equivalence_wrt F ; ::_thesis: [y,z] in [: the carrier of L, the carrier of L:]
then A1: ( y in field (equivalence_wrt F) & z in field (equivalence_wrt F) ) by RELAT_1:15;
field (equivalence_wrt F) c= the carrier of L by Def11;
hence [y,z] in [: the carrier of L, the carrier of L:] by A1, ZFMISC_1:87; ::_thesis: verum
end;
hence equivalence_wrt F is Relation of the carrier of L ; ::_thesis: verum
end;
theorem Th64: :: FILTER_0:64
for L being Lattice
for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is_reflexive_in the carrier of L
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is_reflexive_in the carrier of L
let F be Filter of L; ::_thesis: ( L is I_Lattice implies equivalence_wrt F is_reflexive_in the carrier of L )
assume A1: L is I_Lattice ; ::_thesis: equivalence_wrt F is_reflexive_in the carrier of L
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in the carrier of L or [x,x] in equivalence_wrt F )
assume x in the carrier of L ; ::_thesis: [x,x] in equivalence_wrt F
then reconsider p = x as Element of L ;
p => p = Top L by A1, Th28;
then p <=> p = Top L ;
then p <=> p in F by A1, Th11;
hence [x,x] in equivalence_wrt F by Def11; ::_thesis: verum
end;
theorem Th65: :: FILTER_0:65
for L being Lattice
for F being Filter of L holds equivalence_wrt F is_symmetric_in the carrier of L
proof
let L be Lattice; ::_thesis: for F being Filter of L holds equivalence_wrt F is_symmetric_in the carrier of L
let F be Filter of L; ::_thesis: equivalence_wrt F is_symmetric_in the carrier of L
let x be set ; :: according to RELAT_2:def_3 ::_thesis: for b1 being set holds
( not x in the carrier of L or not b1 in the carrier of L or not [x,b1] in equivalence_wrt F or [b1,x] in equivalence_wrt F )
let y be set ; ::_thesis: ( not x in the carrier of L or not y in the carrier of L or not [x,y] in equivalence_wrt F or [y,x] in equivalence_wrt F )
assume ( x in the carrier of L & y in the carrier of L ) ; ::_thesis: ( not [x,y] in equivalence_wrt F or [y,x] in equivalence_wrt F )
then reconsider p = x, q = y as Element of L ;
assume [x,y] in equivalence_wrt F ; ::_thesis: [y,x] in equivalence_wrt F
then p <=> q in F by Def11;
then q <=> p in F ;
hence [y,x] in equivalence_wrt F by Def11; ::_thesis: verum
end;
theorem Th66: :: FILTER_0:66
for L being Lattice
for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is_transitive_in the carrier of L
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is_transitive_in the carrier of L
let F be Filter of L; ::_thesis: ( L is I_Lattice implies equivalence_wrt F is_transitive_in the carrier of L )
assume A1: L is I_Lattice ; ::_thesis: equivalence_wrt F is_transitive_in the carrier of L
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in the carrier of L or not b1 in the carrier of L or not b2 in the carrier of L or not [x,b1] in equivalence_wrt F or not [b1,b2] in equivalence_wrt F or [x,b2] in equivalence_wrt F )
let y, z be set ; ::_thesis: ( not x in the carrier of L or not y in the carrier of L or not z in the carrier of L or not [x,y] in equivalence_wrt F or not [y,z] in equivalence_wrt F or [x,z] in equivalence_wrt F )
assume ( x in the carrier of L & y in the carrier of L & z in the carrier of L ) ; ::_thesis: ( not [x,y] in equivalence_wrt F or not [y,z] in equivalence_wrt F or [x,z] in equivalence_wrt F )
then reconsider p = x, q = y, r = z as Element of L ;
assume ( [x,y] in equivalence_wrt F & [y,z] in equivalence_wrt F ) ; ::_thesis: [x,z] in equivalence_wrt F
then ( p <=> q in F & q <=> r in F ) by Def11;
then p <=> r in F by A1, Th62;
hence [x,z] in equivalence_wrt F by Def11; ::_thesis: verum
end;
theorem Th67: :: FILTER_0:67
for L being Lattice
for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is Equivalence_Relation of the carrier of L
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is Equivalence_Relation of the carrier of L
let F be Filter of L; ::_thesis: ( L is I_Lattice implies equivalence_wrt F is Equivalence_Relation of the carrier of L )
reconsider R = equivalence_wrt F as Relation of the carrier of L by Th63;
A1: R is_symmetric_in the carrier of L by Th65;
assume A2: L is I_Lattice ; ::_thesis: equivalence_wrt F is Equivalence_Relation of the carrier of L
then R is_reflexive_in the carrier of L by Th64;
then A3: ( field R = the carrier of L & dom R = the carrier of L ) by ORDERS_1:13;
R is_transitive_in the carrier of L by A2, Th66;
hence equivalence_wrt F is Equivalence_Relation of the carrier of L by A3, A1, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum
end;
theorem :: FILTER_0:68
for L being Lattice
for F being Filter of L st L is I_Lattice holds
field (equivalence_wrt F) = the carrier of L
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds
field (equivalence_wrt F) = the carrier of L
let F be Filter of L; ::_thesis: ( L is I_Lattice implies field (equivalence_wrt F) = the carrier of L )
assume L is I_Lattice ; ::_thesis: field (equivalence_wrt F) = the carrier of L
then equivalence_wrt F is Equivalence_Relation of the carrier of L by Th67;
hence field (equivalence_wrt F) = the carrier of L by ORDERS_1:12; ::_thesis: verum
end;
definition
let I be I_Lattice;
let FI be Filter of I;
:: original: equivalence_wrt
redefine func equivalence_wrt FI -> Equivalence_Relation of the carrier of I;
coherence
equivalence_wrt FI is Equivalence_Relation of the carrier of I by Th67;
end;
definition
let B be B_Lattice;
let FB be Filter of B;
:: original: equivalence_wrt
redefine func equivalence_wrt FB -> Equivalence_Relation of the carrier of B;
coherence
equivalence_wrt FB is Equivalence_Relation of the carrier of B by Th67;
end;
definition
let L be Lattice;
let F be Filter of L;
let p, q be Element of L;
predp,q are_equivalence_wrt F means :Def12: :: FILTER_0:def 12
p <=> q in F;
end;
:: deftheorem Def12 defines are_equivalence_wrt FILTER_0:def_12_:_
for L being Lattice
for F being Filter of L
for p, q being Element of L holds
( p,q are_equivalence_wrt F iff p <=> q in F );
theorem :: FILTER_0:69
for L being Lattice
for p, q being Element of L
for F being Filter of L holds
( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F )
proof
let L be Lattice; ::_thesis: for p, q being Element of L
for F being Filter of L holds
( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F )
let p, q be Element of L; ::_thesis: for F being Filter of L holds
( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F )
let F be Filter of L; ::_thesis: ( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F )
( p,q are_equivalence_wrt F iff p <=> q in F ) by Def12;
hence ( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F ) by Def11; ::_thesis: verum
end;
theorem :: FILTER_0:70
for B being B_Lattice
for FB being Filter of B
for I being I_Lattice
for i being Element of I
for FI being Filter of I
for a being Element of B holds
( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
proof
let B be B_Lattice; ::_thesis: for FB being Filter of B
for I being I_Lattice
for i being Element of I
for FI being Filter of I
for a being Element of B holds
( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
let FB be Filter of B; ::_thesis: for I being I_Lattice
for i being Element of I
for FI being Filter of I
for a being Element of B holds
( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
let I be I_Lattice; ::_thesis: for i being Element of I
for FI being Filter of I
for a being Element of B holds
( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
let i be Element of I; ::_thesis: for FI being Filter of I
for a being Element of B holds
( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
let FI be Filter of I; ::_thesis: for a being Element of B holds
( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
let a be Element of B; ::_thesis: ( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
A2: a => a = Top B by Th28;
( i => i = Top I & (Top I) "/\" (Top I) = Top I ) by Th28;
hence ( i <=> i in FI & a <=> a in FB ) by A2, Th11; :: according to FILTER_0:def_12 ::_thesis: verum
end;
theorem :: FILTER_0:71
for L being Lattice
for p, q being Element of L
for F being Filter of L st p,q are_equivalence_wrt F holds
q,p are_equivalence_wrt F
proof
let L be Lattice; ::_thesis: for p, q being Element of L
for F being Filter of L st p,q are_equivalence_wrt F holds
q,p are_equivalence_wrt F
let p, q be Element of L; ::_thesis: for F being Filter of L st p,q are_equivalence_wrt F holds
q,p are_equivalence_wrt F
let F be Filter of L; ::_thesis: ( p,q are_equivalence_wrt F implies q,p are_equivalence_wrt F )
assume p <=> q in F ; :: according to FILTER_0:def_12 ::_thesis: q,p are_equivalence_wrt F
hence q <=> p in F ; :: according to FILTER_0:def_12 ::_thesis: verum
end;
theorem :: FILTER_0:72
for B being B_Lattice
for FB being Filter of B
for I being I_Lattice
for i, j, k being Element of I
for FI being Filter of I
for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
proof
let B be B_Lattice; ::_thesis: for FB being Filter of B
for I being I_Lattice
for i, j, k being Element of I
for FI being Filter of I
for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let FB be Filter of B; ::_thesis: for I being I_Lattice
for i, j, k being Element of I
for FI being Filter of I
for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let I be I_Lattice; ::_thesis: for i, j, k being Element of I
for FI being Filter of I
for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let i, j, k be Element of I; ::_thesis: for FI being Filter of I
for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let FI be Filter of I; ::_thesis: for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let a, b, c be Element of B; ::_thesis: ( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
thus ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) ::_thesis: ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB )
proof
assume ( i <=> j in FI & j <=> k in FI ) ; :: according to FILTER_0:def_12 ::_thesis: i,k are_equivalence_wrt FI
hence i <=> k in FI by Th62; :: according to FILTER_0:def_12 ::_thesis: verum
end;
assume ( a <=> b in FB & b <=> c in FB ) ; :: according to FILTER_0:def_12 ::_thesis: a,c are_equivalence_wrt FB
hence a <=> c in FB by Th62; :: according to FILTER_0:def_12 ::_thesis: verum
end;
begin
theorem :: FILTER_0:73
for L being non empty join-commutative meet-commutative meet-associative meet-absorbing join-absorbing LattStr
for x, y, z being Element of L st z [= x & z [= y & ( for z9 being Element of L st z9 [= x & z9 [= y holds
z9 [= z ) holds
z = x "/\" y
proof
let L be non empty join-commutative meet-commutative meet-associative meet-absorbing join-absorbing LattStr ; ::_thesis: for x, y, z being Element of L st z [= x & z [= y & ( for z9 being Element of L st z9 [= x & z9 [= y holds
z9 [= z ) holds
z = x "/\" y
let x, y, z be Element of L; ::_thesis: ( z [= x & z [= y & ( for z9 being Element of L st z9 [= x & z9 [= y holds
z9 [= z ) implies z = x "/\" y )
assume that
A1: ( z [= x & z [= y ) and
A2: for z9 being Element of L st z9 [= x & z9 [= y holds
z9 [= z ; ::_thesis: z = x "/\" y
( x "/\" y [= x & x "/\" y [= y ) by LATTICES:6;
then A3: x "/\" y [= z by A2;
z [= x "/\" y by A1, Th7;
hence z = x "/\" y by A3, LATTICES:8; ::_thesis: verum
end;
theorem :: FILTER_0:74
for L being non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr
for x, y, z being Element of L st x [= z & y [= z & ( for z9 being Element of L st x [= z9 & y [= z9 holds
z [= z9 ) holds
z = x "\/" y
proof
let L be non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr ; ::_thesis: for x, y, z being Element of L st x [= z & y [= z & ( for z9 being Element of L st x [= z9 & y [= z9 holds
z [= z9 ) holds
z = x "\/" y
let x, y, z be Element of L; ::_thesis: ( x [= z & y [= z & ( for z9 being Element of L st x [= z9 & y [= z9 holds
z [= z9 ) implies z = x "\/" y )
assume that
A1: ( x [= z & y [= z ) and
A2: for z9 being Element of L st x [= z9 & y [= z9 holds
z [= z9 ; ::_thesis: z = x "\/" y
( x [= x "\/" y & y [= x "\/" y ) by LATTICES:5;
then A3: z [= x "\/" y by A2;
x "\/" y [= z by A1, Th6;
hence z = x "\/" y by A3, LATTICES:8; ::_thesis: verum
end;