:: Ideals
:: by Grzegorz Bancerek
::
:: Received October 24, 1994
:: Copyright (c) 1994-2011 Association of Mizar Users

begin

theorem Th1: :: FILTER_2:1

for D being non empty set
for S being non empty Subset of D
for f being BinOp of D
for g being BinOp of S st g = f || S holds
( ( f is commutative implies g is commutative ) & ( f is idempotent implies g is idempotent ) & ( f is associative implies g is associative ) )

proof end;

theorem :: FILTER_2:2

for D being non empty set
for S being non empty Subset of D
for f being BinOp of D
for g being BinOp of S
for d being Element of D
for d9 being Element of S st g = f || S & d9 = d holds
( ( d is_a_left_unity_wrt f implies d9 is_a_left_unity_wrt g ) & ( d is_a_right_unity_wrt f implies d9 is_a_right_unity_wrt g ) & ( d is_a_unity_wrt f implies d9 is_a_unity_wrt g ) )

proof end;

theorem Th3: :: FILTER_2:3

for D being non empty set
for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S holds
( ( f1 is_left_distributive_wrt f2 implies g1 is_left_distributive_wrt g2 ) & ( f1 is_right_distributive_wrt f2 implies g1 is_right_distributive_wrt g2 ) )

proof end;

theorem :: FILTER_2:4

for D being non empty set
for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 is_distributive_wrt f2 holds
g1 is_distributive_wrt g2

proof end;

theorem Th5: :: FILTER_2:5

for D being non empty set
for S being non empty Subset of D
for f1, f2 being BinOp of D
for g1, g2 being BinOp of S st g1 = f1 || S & g2 = f2 || S & f1 absorbs f2 holds
g1 absorbs g2

proof end;

begin

definition

let D be non empty set ;
let X1, X2 be Subset of D;
:: original: =
redefine pred X1 = X2 means :: FILTER_2:def 1
for x being Element of D holds
( x in X1 iff x in X2 );
compatibility
( X1 = X2 iff for x being Element of D holds
( x in X1 iff x in X2 ) ) by SUBSET_1:8;

end;

:: deftheorem defines = FILTER_2:def 1 :
for D being non empty set
for X1, X2 being Subset of D holds
( X1 = X2 iff for x being Element of D holds
( x in X1 iff x in X2 ) );

deffunc H₁( LattStr ) -> set = the carrier of $1;

deffunc H₂( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_join of $1;

deffunc H₃( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_meet of $1;

theorem :: FILTER_2:6

for L1, L2 being LattStr st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
L1 .: = L2 .: ;

theorem :: FILTER_2:7

for L being Lattice holds (L .:) .: = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) ;

theorem :: FILTER_2:8

for L1, L2 being non empty LattStr st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
( a1 "\/" b1 = a2 "\/" b2 & a1 "/\" b1 = a2 "/\" b2 & ( a1 [= b1 implies a2 [= b2 ) & ( a2 [= b2 implies a1 [= b1 ) )

proof end;

theorem Th9: :: FILTER_2:9

for L1, L2 being 0_Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
Bottom L1 = Bottom L2

proof end;

theorem Th10: :: FILTER_2:10

for L1, L2 being 1_Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
Top L1 = Top L2

proof end;

theorem Th11: :: FILTER_2:11

for L1, L2 being C_Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 & a1 is_a_complement_of b1 holds
a2 is_a_complement_of b2

proof end;

theorem :: FILTER_2:12

for L1, L2 being B_Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
for a being Element of L1
for b being Element of L2 st a = b holds
a ` = b `

proof end;

theorem :: FILTER_2:13

for L being Lattice
for X being Subset of L st ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "/\" q in X ) ) holds
X is ClosedSubset of L

proof end;

theorem :: FILTER_2:14

for L being Lattice
for X being Subset of L st ( for p, q being Element of L holds
( ( p in X & q in X ) iff p "\/" q in X ) ) holds
X is ClosedSubset of L

proof end;

definition

let L be Lattice;
canceled;
canceled;
mode Ideal of L is non empty initial join-closed Subset of L;

end;

:: deftheorem FILTER_2:def 2 :
canceled;

:: deftheorem FILTER_2:def 3 :
canceled;

Lm1: for L being Lattice
for S being non empty Subset of L holds
( S is Ideal of L iff for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) )

proof end;

theorem :: FILTER_2:15

canceled;

theorem Th16: :: FILTER_2:16

for L1, L2 being Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
for x being set st x is Filter of L1 holds
x is Filter of L2

proof end;

theorem Th17: :: FILTER_2:17

for L1, L2 being Lattice st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) holds
for x being set st x is Ideal of L1 holds
x is Ideal of L2

proof end;

definition

let L be Lattice;
let p be Element of L;
func p .: -> Element of (L .:) equals :: FILTER_2:def 4
p;
coherence
p is Element of (L .:) ;

end;

:: deftheorem defines .: FILTER_2:def 4 :
for L being Lattice
for p being Element of L holds p .: = p;

definition

let L be Lattice;
let p be Element of (L .:);
func .: p -> Element of L equals :: FILTER_2:def 5
p;
coherence
p is Element of L ;

end;

:: deftheorem defines .: FILTER_2:def 5 :
for L being Lattice
for p being Element of (L .:) holds .: p = p;

theorem :: FILTER_2:18

for L being Lattice
for p being Element of L
for p9 being Element of (L .:) holds
( .: (p .:) = p & (.: p9) .: = p9 ) ;

theorem :: FILTER_2:19

for L being Lattice
for p, q being Element of L
for p9, q9 being Element of (L .:) holds
( p "/\" q = (p .:) "\/" (q .:) & p "\/" q = (p .:) "/\" (q .:) & p9 "/\" q9 = (.: p9) "\/" (.: q9) & p9 "\/" q9 = (.: p9) "/\" (.: q9) ) ;

theorem :: FILTER_2:20

for L being Lattice
for p, q being Element of L
for p9, q9 being Element of (L .:) holds
( ( p [= q implies q .: [= p .: ) & ( q .: [= p .: implies p [= q ) & ( p9 [= q9 implies .: q9 [= .: p9 ) & ( .: q9 [= .: p9 implies p9 [= q9 ) ) by LATTICE2:53, LATTICE2:54;

definition

let L be Lattice;
let X be Subset of L;
func X .: -> Subset of (L .:) equals :: FILTER_2:def 6
X;
coherence
X is Subset of (L .:) ;

end;

:: deftheorem defines .: FILTER_2:def 6 :
for L being Lattice
for X being Subset of L holds X .: = X;

definition

let L be Lattice;
let X be Subset of (L .:);
func .: X -> Subset of L equals :: FILTER_2:def 7
X;
coherence
X is Subset of L ;

end;

:: deftheorem defines .: FILTER_2:def 7 :
for L being Lattice
for X being Subset of (L .:) holds .: X = X;

registration

let L be Lattice;
let D be non empty Subset of L;
cluster D .: -> non empty ;
coherence
not D .: is empty ;

end;

registration

let L be Lattice;
let D be non empty Subset of (L .:);
cluster .: D -> non empty ;
coherence
not .: D is empty ;

end;

registration

let L be Lattice;
let S be meet-closed Subset of L;
cluster S .: -> join-closed Subset of (L .:);
coherence
for b₁ being Subset of (L .:) st b₁ = S .: holds
b₁ is join-closed

proof end;

end;

registration

let L be Lattice;
let S be join-closed Subset of L;
cluster S .: -> meet-closed Subset of (L .:);
coherence
for b₁ being Subset of (L .:) st b₁ = S .: holds
b₁ is meet-closed

proof end;

end;

registration

let L be Lattice;
let S be meet-closed Subset of (L .:);
cluster .: S -> join-closed Subset of L;
coherence
for b₁ being Subset of L st b₁ = .: S holds
b₁ is join-closed

proof end;

end;

registration

let L be Lattice;
let S be join-closed Subset of (L .:);
cluster .: S -> meet-closed Subset of L;
coherence
for b₁ being Subset of L st b₁ = .: S holds
b₁ is meet-closed

proof end;

end;

registration

let L be Lattice;
let F be final Subset of L;
cluster F .: -> initial Subset of (L .:);
coherence
for b₁ being Subset of (L .:) st b₁ = F .: holds
b₁ is initial

proof end;

end;

registration

let L be Lattice;
let F be initial Subset of L;
cluster F .: -> final Subset of (L .:);
coherence
for b₁ being Subset of (L .:) st b₁ = F .: holds
b₁ is final

proof end;

end;

registration

let L be Lattice;
let F be final Subset of (L .:);
cluster .: F -> initial Subset of L;
coherence
for b₁ being Subset of L st b₁ = .: F holds
b₁ is initial

proof end;

end;

registration

let L be Lattice;
let F be initial Subset of (L .:);
cluster F .: -> final Subset of L;
coherence
for b₁ being Subset of L st b₁ = F .: holds
b₁ is final

proof end;

end;

theorem Th21: :: FILTER_2:21

for L being Lattice
for x being set holds
( x is Ideal of L iff x is Filter of (L .:) )

proof end;

theorem Th22: :: FILTER_2:22

for L being Lattice
for D being non empty Subset of L holds
( D is Ideal of L iff ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) ) )

proof end;

theorem Th23: :: FILTER_2:23

for L being Lattice
for p, q being Element of L
for I being Ideal of L st p in I holds
( p "/\" q in I & q "/\" p in I )

proof end;

theorem :: FILTER_2:24

for L being Lattice
for I being Ideal of L ex p being Element of L st p in I

proof end;

theorem :: FILTER_2:25

for L being Lattice
for I being Ideal of L st L is lower-bounded holds
Bottom L in I

proof end;

theorem :: FILTER_2:26

for L being Lattice st L is lower-bounded holds
{(Bottom L)} is Ideal of L

proof end;

theorem :: FILTER_2:27

for L being Lattice
for p being Element of L st {p} is Ideal of L holds
L is lower-bounded

proof end;

begin

theorem Th28: :: FILTER_2:28

for L being Lattice holds the carrier of L is Ideal of L

proof end;

definition

let L be Lattice;
func (.L.> -> Ideal of L equals :: FILTER_2:def 8
the carrier of L;
coherence
the carrier of L is Ideal of L by Th28;

end;

:: deftheorem defines (. FILTER_2:def 8 :
for L being Lattice holds (.L.> = the carrier of L;

definition

let L be Lattice;
let p be Element of L;
func (.p.> -> Ideal of L equals :: FILTER_2:def 9
{ q where q is Element of L : q [= p } ;
coherence
{ q where q is Element of L : q [= p } is Ideal of L

proof end;

end;

:: deftheorem defines (. FILTER_2:def 9 :
for L being Lattice
for p being Element of L holds (.p.> = { q where q is Element of L : q [= p } ;

theorem Th29: :: FILTER_2:29

for L being Lattice
for q, p being Element of L holds
( q in (.p.> iff q [= p )

proof end;

theorem Th30: :: FILTER_2:30

for L being Lattice
for p being Element of L holds
( (.p.> = <.(p .:).) & (.(p .:).> = <.p.) )

proof end;

theorem :: FILTER_2:31

for L being Lattice
for p, q being Element of L holds
( p in (.p.> & p "/\" q in (.p.> & q "/\" p in (.p.> )

proof end;

theorem :: FILTER_2:32

for L being Lattice st L is upper-bounded holds
(.L.> = (.(Top L).>

proof end;

definition

let L be Lattice;
let I be Ideal of L;
pred I is_max-ideal means :: FILTER_2:def 10
( I <> the carrier of L & ( for J being Ideal of L st I c= J & J <> the carrier of L holds
I = J ) );

end;

:: deftheorem defines is_max-ideal FILTER_2:def 10 :
for L being Lattice
for I being Ideal of L holds
( I is_max-ideal iff ( I <> the carrier of L & ( for J being Ideal of L st I c= J & J <> the carrier of L holds
I = J ) ) );

theorem Th33: :: FILTER_2:33

for L being Lattice
for I being Ideal of L holds
( I is_max-ideal iff I .: is being_ultrafilter )

proof end;

theorem :: FILTER_2:34

for L being Lattice st L is upper-bounded holds
for I being Ideal of L st I <> the carrier of L holds
ex J being Ideal of L st
( I c= J & J is_max-ideal )

proof end;

theorem :: FILTER_2:35

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 end;

theorem :: FILTER_2:36

for L being Lattice
for p being Element of L st L is upper-bounded & p <> Top L holds
ex I being Ideal of L st
( p in I & I is_max-ideal )

proof end;

definition

let L be Lattice;
let D be non empty Subset of L;
func (.D.> -> Ideal of L means :Def11: :: FILTER_2:def 11
( D c= it & ( for I being Ideal of L st D c= I holds
it c= I ) );
existence
ex b₁ being Ideal of L st
( D c= b₁ & ( for I being Ideal of L st D c= I holds
b₁ c= I ) )

proof end;

uniqueness
for b₁, b₂ being Ideal of L st D c= b₁ & ( for I being Ideal of L st D c= I holds
b₁ c= I ) & D c= b₂ & ( for I being Ideal of L st D c= I holds
b₂ c= I ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines (. FILTER_2:def 11 :
for L being Lattice
for D being non empty Subset of L
for b₃ being Ideal of L holds
( b₃ = (.D.> iff ( D c= b₃ & ( for I being Ideal of L st D c= I holds
b₃ c= I ) ) );

Lm2: for L1, L2 being Lattice
for D1 being non empty Subset of L1
for D2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 holds
( <.D1.) = <.D2.) & (.D1.> = (.D2.> )

proof end;

theorem Th37: :: FILTER_2:37

for L being Lattice
for D being non empty Subset of L
for D9 being non empty Subset of (L .:) holds
( <.(D .:).) = (.D.> & <.D.) = (.(D .:).> & <.(.: D9).) = (.D9.> & <.D9.) = (.(.: D9).> )

proof end;

theorem Th38: :: FILTER_2:38

for L being Lattice
for I being Ideal of L holds (.I.> = I

proof end;

theorem :: FILTER_2:39

for L being Lattice
for D, D1, D2 being non empty Subset of L holds
( ( D1 c= D2 implies (.D1.> c= (.D2.> ) & (.(.D.>.> c= (.D.> )

proof end;

theorem :: FILTER_2:40

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 end;

theorem :: FILTER_2:41

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 end;

theorem Th42: :: FILTER_2:42

for L being Lattice
for D being non empty Subset of L st L is upper-bounded & Top L in D holds
( (.D.> = (.L.> & (.D.> = the carrier of L )

proof end;

theorem :: FILTER_2:43

for L being Lattice
for I being Ideal of L st L is upper-bounded & Top L in I holds
( I = (.L.> & I = the carrier of L )

proof end;

definition

let L be Lattice;
let I be Ideal of L;
attr I is prime means :: FILTER_2:def 12
for p, q being Element of L holds
( p "/\" q in I iff ( p in I or q in I ) );

end;

:: deftheorem defines prime FILTER_2:def 12 :
for L being Lattice
for I being Ideal of L holds
( I is prime iff for p, q being Element of L holds
( p "/\" q in I iff ( p in I or q in I ) ) );

theorem Th44: :: FILTER_2:44

for L being Lattice
for I being Ideal of L holds
( I is prime iff I .: is prime )

proof end;

definition

let L be Lattice;
let D1, D2 be non empty Subset of L;
func D1 "\/" D2 -> Subset of L equals :: FILTER_2:def 13
{ (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 end;

end;

:: deftheorem defines "\/" FILTER_2:def 13 :
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;
cluster D1 "\/" D2 -> non empty ;
coherence
not D1 "\/" D2 is empty

proof end;

end;

Lm3: for L1, L2 being Lattice
for D1, E1 being non empty Subset of L1
for D2, E2 being non empty Subset of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & D1 = D2 & E1 = E2 holds
D1 "/\" E1 = D2 "/\" E2

proof end;

theorem Th45: :: FILTER_2:45

for L being Lattice
for D1, D2 being non empty Subset of L
for D19, D29 being non empty Subset of (L .:) holds
( D1 "\/" D2 = (D1 .:) "/\" (D2 .:) & (D1 .:) "\/" (D2 .:) = D1 "/\" D2 & D19 "\/" D29 = (.: D19) "/\" (.: D29) & (.: D19) "\/" (.: D29) = D19 "/\" D29 )

proof end;

theorem :: FILTER_2:46

for L being Lattice
for p, q being Element of L
for D1, D2 being non empty Subset of L st p in D1 & q in D2 holds
( p "\/" q in D1 "\/" D2 & q "\/" p in D1 "\/" D2 ) ;

theorem :: FILTER_2:47

for L being Lattice
for x being set
for D1, D2 being non empty Subset of L st x in D1 "\/" D2 holds
ex p, q being Element of L st
( x = p "\/" q & p in D1 & q in D2 ) ;

theorem :: FILTER_2:48

for L being Lattice
for D1, D2 being non empty Subset of L holds D1 "\/" D2 = D2 "\/" D1

proof end;

registration

let L be D_Lattice;
let I1, I2 be Ideal of L;
cluster I1 "\/" I2 -> initial join-closed ;
coherence
( I1 "\/" I2 is initial & I1 "\/" I2 is join-closed )

proof end;

end;

theorem :: FILTER_2:49

for L being Lattice
for D1, D2 being non empty Subset of L holds
( (.(D1 \/ D2).> = (.((.D1.> \/ D2).> & (.(D1 \/ D2).> = (.(D1 \/ (.D2.>).> )

proof end;

theorem :: FILTER_2:50

for L being Lattice
for I, J being Ideal of L holds (.(I \/ J).> = { r where r is Element of L : ex p, q being Element of L st
( r [= p "\/" q & p in I & q in J ) }

proof end;

theorem :: FILTER_2:51

for L being Lattice
for I, J being Ideal of L holds
( I c= I "\/" J & J c= I "\/" J )

proof end;

theorem :: FILTER_2:52

for L being Lattice
for I, J being Ideal of L holds (.(I \/ J).> = (.(I "\/" J).>

proof end;

theorem Th53: :: FILTER_2:53

for L being Lattice holds
( L is C_Lattice iff L .: is C_Lattice )

proof end;

theorem Th54: :: FILTER_2:54

for L being Lattice holds
( L is B_Lattice iff L .: is B_Lattice )

proof end;

registration

let B be B_Lattice;
cluster B .: -> Lattice-like Boolean ;
coherence
( B .: is Boolean & B .: is Lattice-like ) by Th54;

end;

Lm4: for B being B_Lattice
for a being Element of B holds (a .:) ` = a `

proof end;

theorem Th55: :: FILTER_2:55

for B being B_Lattice
for a being Element of B
for a9 being Element of (B .:) holds
( (a .:) ` = a ` & (.: a9) ` = a9 ` )

proof end;

theorem :: FILTER_2:56

for B being B_Lattice
for IB, JB being Ideal of B holds (.(IB \/ JB).> = IB "\/" JB

proof end;

theorem :: FILTER_2:57

for B being B_Lattice
for IB being Ideal of B holds
( IB is_max-ideal iff ( IB <> the carrier of B & ( for a being Element of B holds
( a in IB or a ` in IB ) ) ) )

proof end;

theorem :: FILTER_2:58

for B being B_Lattice
for IB being Ideal of B holds
( ( IB <> (.B.> & IB is prime ) iff IB is_max-ideal )

proof end;

theorem :: FILTER_2:59

for B being B_Lattice
for IB being Ideal of B st IB is_max-ideal holds
for a being Element of B holds
( a in IB iff not a ` in IB )

proof end;

theorem :: FILTER_2:60

for B being B_Lattice
for a, b being Element of B st a <> b holds
ex IB being Ideal of B st
( IB is_max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) )

proof end;

theorem Th61: :: FILTER_2:61

for L being Lattice
for P being non empty ClosedSubset of L holds
( the L_join of L || P is BinOp of P & the L_meet of L || P is BinOp of P )

proof end;

theorem Th62: :: FILTER_2:62

for L being Lattice
for P being non empty ClosedSubset of L
for o1, o2 being BinOp of P st o1 = the L_join of L || P & o2 = the L_meet of L || P holds
( o1 is commutative & o1 is associative & o2 is commutative & o2 is associative & o1 absorbs o2 & o2 absorbs o1 )

proof end;

definition

let L be Lattice;
let p, q be Element of L;
assume A1: p [= q ;
func [#p,q#] -> non empty ClosedSubset of L equals :Def14: :: FILTER_2:def 14
{ r where r is Element of L : ( p [= r & r [= q ) } ;
coherence
{ r where r is Element of L : ( p [= r & r [= q ) } is non empty ClosedSubset of L

proof end;

end;

:: deftheorem Def14 defines [# FILTER_2:def 14 :
for L being Lattice
for p, q being Element of L st p [= q holds
[#p,q#] = { r where r is Element of L : ( p [= r & r [= q ) } ;

theorem Th63: :: FILTER_2:63

for L being Lattice
for p, q, r being Element of L st p [= q holds
( r in [#p,q#] iff ( p [= r & r [= q ) )

proof end;

theorem :: FILTER_2:64

for L being Lattice
for p, q being Element of L st p [= q holds
( p in [#p,q#] & q in [#p,q#] ) by Th63;

theorem :: FILTER_2:65

for L being Lattice
for p being Element of L holds [#p,p#] = {p}

proof end;

theorem :: FILTER_2:66

for L being Lattice
for p being Element of L st L is upper-bounded holds
<.p.) = [#p,(Top L)#]

proof end;

theorem :: FILTER_2:67

for L being Lattice
for p being Element of L st L is lower-bounded holds
(.p.> = [#(Bottom L),p#]

proof end;

theorem :: FILTER_2:68

for L1, L2 being Lattice
for F1 being Filter of L1
for F2 being Filter of L2 st LattStr(# the carrier of L1, the L_join of L1, the L_meet of L1 #) = LattStr(# the carrier of L2, the L_join of L2, the L_meet of L2 #) & F1 = F2 holds
latt F1 = latt F2

proof end;

begin

notation

let L be Lattice;
synonym Sublattice of L for SubLattice of L;

end;

definition

let L be Lattice;
redefine mode SubLattice of L means :Def15: :: FILTER_2:def 15
ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of it, the L_join of it, the L_meet of it #) = LattStr(# P,o1,o2 #) );
compatibility
for b₁ being LattStr holds
( b₁ is Sublattice of L iff ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of b₁, the L_join of b₁, the L_meet of b₁ #) = LattStr(# P,o1,o2 #) ) )

proof end;

end;

:: deftheorem Def15 defines Sublattice FILTER_2:def 15 :
for L being Lattice
for b₂ being LattStr holds
( b₂ is Sublattice of L iff ex P being non empty ClosedSubset of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & LattStr(# the carrier of b₂, the L_join of b₂, the L_meet of b₂ #) = LattStr(# P,o1,o2 #) ) );

theorem Th69: :: FILTER_2:69

for L being Lattice
for K being Sublattice of L
for a being Element of K holds a is Element of L

proof end;

definition

let L be Lattice;
let P be non empty ClosedSubset of L;
func latt (L,P) -> Sublattice of L means :Def16: :: FILTER_2:def 16
ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & it = LattStr(# P,o1,o2 #) );
existence
ex b₁ being Sublattice of L ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & b₁ = LattStr(# P,o1,o2 #) )

proof end;

uniqueness
for b₁, b₂ being Sublattice of L st ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & b₁ = LattStr(# P,o1,o2 #) ) & ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & b₂ = LattStr(# P,o1,o2 #) ) holds
b₁ = b₂ ;

end;

:: deftheorem Def16 defines latt FILTER_2:def 16 :
for L being Lattice
for P being non empty ClosedSubset of L
for b₃ being Sublattice of L holds
( b₃ = latt (L,P) iff ex o1, o2 being BinOp of P st
( o1 = the L_join of L || P & o2 = the L_meet of L || P & b₃ = LattStr(# P,o1,o2 #) ) );

registration

let L be Lattice;
let P be non empty ClosedSubset of L;
cluster latt (L,P) -> strict ;
coherence
latt (L,P) is strict

proof end;

end;

definition

let L be Lattice;
let l be Sublattice of L;
:: original: .:
redefine func l .: -> strict Sublattice of L .: ;
coherence
l .: is strict Sublattice of L .:

proof end;

end;

theorem Th70: :: FILTER_2:70

for L being Lattice
for F being Filter of L holds latt F = latt (L,F)

proof end;

theorem Th71: :: FILTER_2:71

for L being Lattice
for P being non empty ClosedSubset of L holds latt (L,P) = (latt ((L .:),(P .:))) .:

proof end;

theorem :: FILTER_2:72

for L being Lattice holds
( latt (L,(.L.>) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & latt (L,<.L.)) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) )

proof end;

theorem Th73: :: FILTER_2:73

for L being Lattice
for P being non empty ClosedSubset of L holds
( the carrier of (latt (L,P)) = P & the L_join of (latt (L,P)) = the L_join of L || P & the L_meet of (latt (L,P)) = the L_meet of L || P )

proof end;

theorem Th74: :: FILTER_2:74

for L being Lattice
for P being non empty ClosedSubset of L
for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )

proof end;

theorem Th75: :: FILTER_2:75

for L being Lattice
for P being non empty ClosedSubset of L
for p, q being Element of L
for p9, q9 being Element of (latt (L,P)) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )

proof end;

theorem :: FILTER_2:76

for L being Lattice
for I being Ideal of L st L is lower-bounded holds
latt (L,I) is lower-bounded

proof end;

theorem :: FILTER_2:77

for L being Lattice
for P being non empty ClosedSubset of L st L is modular holds
latt (L,P) is modular

proof end;

theorem Th78: :: FILTER_2:78

for L being Lattice
for P being non empty ClosedSubset of L st L is distributive holds
latt (L,P) is distributive

proof end;

theorem :: FILTER_2:79

for L being Lattice
for p, q being Element of L st L is implicative & p [= q holds
latt (L,[#p,q#]) is implicative

proof end;

theorem :: FILTER_2:80

canceled;

registration

let L be Lattice;
let p be Element of L;
cluster latt (L,(.p.>) -> upper-bounded ;
coherence
latt (L,(.p.>) is upper-bounded

proof end;

end;

theorem Th81: :: FILTER_2:81

for L being Lattice
for p being Element of L holds Top (latt (L,(.p.>)) = p

proof end;

theorem Th82: :: FILTER_2:82

for L being Lattice
for p being Element of L st L is lower-bounded holds
( latt (L,(.p.>) is lower-bounded & Bottom (latt (L,(.p.>)) = Bottom L )

proof end;

theorem Th83: :: FILTER_2:83

for L being Lattice
for p being Element of L st L is lower-bounded holds
latt (L,(.p.>) is bounded

proof end;

theorem Th84: :: FILTER_2:84

for L being Lattice
for p, q being Element of L st p [= q holds
( latt (L,[#p,q#]) is bounded & Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p )

proof end;

theorem :: FILTER_2:85

for L being Lattice
for p being Element of L st L is C_Lattice & L is modular holds
latt (L,(.p.>) is C_Lattice

proof end;

theorem Th86: :: FILTER_2:86

for L being Lattice
for p, q being Element of L st L is C_Lattice & L is modular & p [= q holds
latt (L,[#p,q#]) is C_Lattice

proof end;

theorem :: FILTER_2:87

for L being Lattice
for p, q being Element of L st L is B_Lattice & p [= q holds
latt (L,[#p,q#]) is B_Lattice

proof end;

theorem :: FILTER_2:88

for L being Lattice
for S being non empty Subset of L holds
( S is Ideal of L iff for p, q being Element of L holds
( ( p in S & q in S ) iff p "\/" q in S ) ) by Lm1;