:: FILTER_2 semantic presentation

theorem Th1: :: FILTER_2:1

for b₁ being non empty set
for b₂ being non empty Subset of b₁
for b₃ being BinOp of b₁
for b₄ being BinOp of b₂ st b₄ = b₃ || b₂ holds
( ( b₃ is commutative implies b₄ is commutative ) & ( b₃ is idempotent implies b₄ is idempotent ) & ( b₃ is associative implies b₄ is associative ) )

proof end;

theorem Th2: :: FILTER_2:2

for b₁ being non empty set
for b₂ being non empty Subset of b₁
for b₃ being BinOp of b₁
for b₄ being BinOp of b₂
for b₅ being Element of b₁
for b₆ being Element of b₂ st b₄ = b₃ || b₂ & b₆ = b₅ holds
( ( b₅ is_a_left_unity_wrt b₃ implies b₆ is_a_left_unity_wrt b₄ ) & ( b₅ is_a_right_unity_wrt b₃ implies b₆ is_a_right_unity_wrt b₄ ) & ( b₅ is_a_unity_wrt b₃ implies b₆ is_a_unity_wrt b₄ ) )

proof end;

theorem Th3: :: FILTER_2:3

for b₁ being non empty set
for b₂ being non empty Subset of b₁
for b₃, b₄ being BinOp of b₁
for b₅, b₆ being BinOp of b₂ st b₅ = b₃ || b₂ & b₆ = b₄ || b₂ holds
( ( b₃ is_left_distributive_wrt b₄ implies b₅ is_left_distributive_wrt b₆ ) & ( b₃ is_right_distributive_wrt b₄ implies b₅ is_right_distributive_wrt b₆ ) )

proof end;

theorem Th4: :: FILTER_2:4

for b₁ being non empty set
for b₂ being non empty Subset of b₁
for b₃, b₄ being BinOp of b₁
for b₅, b₆ being BinOp of b₂ st b₅ = b₃ || b₂ & b₆ = b₄ || b₂ & b₃ is_distributive_wrt b₄ holds
b₅ is_distributive_wrt b₆

proof end;

theorem Th5: :: FILTER_2:5

for b₁ being non empty set
for b₂ being non empty Subset of b₁
for b₃, b₄ being BinOp of b₁
for b₅, b₆ being BinOp of b₂ st b₅ = b₃ || b₂ & b₆ = b₄ || b₂ & b₃ absorbs b₄ holds
b₅ absorbs b₆

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Subset of c₁;
redefine pred = as c₂ = c₃ means :: FILTER_2:def 1
for b₁ being Element of a₁ holds
( b₁ in a₂ iff b₁ in a₃ );
compatibility by SUBSET_1:8;

end;

:: deftheorem Def1 defines = FILTER_2:def 1 :

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

deffunc H₂( LattStr ) -> Relation of [:the carrier of a₁,the carrier of a₁:],the carrier of a₁ = the L_join of a₁;

deffunc H₃( LattStr ) -> Relation of [:the carrier of a₁,the carrier of a₁:],the carrier of a₁ = the L_meet of a₁;

theorem Th6: :: FILTER_2:6

for b₁, b₂ being LattStr st LattStr(# the carrier of b₁,the L_join of b₁,the L_meet of b₁ #) = LattStr(# the carrier of b₂,the L_join of b₂,the L_meet of b₂ #) holds
b₁ .: = b₂ .: ;

theorem Th7: :: FILTER_2:7

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

theorem Th8: :: FILTER_2:8

for b₁, b₂ being non empty LattStr st LattStr(# the carrier of b₁,the L_join of b₁,the L_meet of b₁ #) = LattStr(# the carrier of b₂,the L_join of b₂,the L_meet of b₂ #) holds
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st b₃ = b₅ & b₄ = b₆ holds
( b₃ "\/" b₄ = b₅ "\/" b₆ & b₃ "/\" b₄ = b₅ "/\" b₆ & ( b₃ [= b₄ implies b₅ [= b₆ ) & ( b₅ [= b₆ implies b₃ [= b₄ ) )

proof end;

theorem Th9: :: FILTER_2:9

for b₁, b₂ being 0_Lattice st LattStr(# the carrier of b₁,the L_join of b₁,the L_meet of b₁ #) = LattStr(# the carrier of b₂,the L_join of b₂,the L_meet of b₂ #) holds
Bottom b₁ = Bottom b₂

proof end;

theorem Th10: :: FILTER_2:10

for b₁, b₂ being 1_Lattice st LattStr(# the carrier of b₁,the L_join of b₁,the L_meet of b₁ #) = LattStr(# the carrier of b₂,the L_join of b₂,the L_meet of b₂ #) holds
Top b₁ = Top b₂

proof end;

theorem Th11: :: FILTER_2:11

for b₁, b₂ being C_Lattice st LattStr(# the carrier of b₁,the L_join of b₁,the L_meet of b₁ #) = LattStr(# the carrier of b₂,the L_join of b₂,the L_meet of b₂ #) holds
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st b₃ = b₅ & b₄ = b₆ & b₃ is_a_complement_of b₄ holds
b₅ is_a_complement_of b₆

proof end;

theorem Th12: :: FILTER_2:12

for b₁, b₂ being B_Lattice st LattStr(# the carrier of b₁,the L_join of b₁,the L_meet of b₁ #) = LattStr(# the carrier of b₂,the L_join of b₂,the L_meet of b₂ #) holds
for b₃ being Element of b₁
for b₄ being Element of b₂ st b₃ = b₄ holds
b₃ ` = b₄ `

proof end;

theorem Th13: :: FILTER_2:13

for b₁ being Lattice
for b₂ being Subset of b₁ st ( for b₃, b₄ being Element of b₁ holds
( ( b₃ in b₂ & b₄ in b₂ ) iff b₃ "/\" b₄ in b₂ ) ) holds
b₂ is ClosedSubset of b₁

proof end;

theorem Th14: :: FILTER_2:14

for b₁ being Lattice
for b₂ being Subset of b₁ st ( for b₃, b₄ being Element of b₁ holds
( ( b₃ in b₂ & b₄ in b₂ ) iff b₃ "\/" b₄ in b₂ ) ) holds
b₂ is ClosedSubset of b₁

proof end;

definition

let c₁ be Lattice;
redefine mode Filter as Filter of c₁ -> non empty ClosedSubset of a₁;
coherence by LATTICE4:11;

end;

definition

let c₁ be Lattice;
redefine func <. as <.c₁.) -> Filter of a₁;
coherence ;
let c₂ be Element of c₁;
redefine func <. as <.c₂.) -> Filter of a₁;
coherence ;

end;

definition

let c₁ be Lattice;
let c₂ be non empty Subset of c₁;
redefine func <. as <.c₂.) -> Filter of a₁;
coherence ;

end;

definition

let c₁ be D_Lattice;
let c₂, c₃ be Filter of c₁;
redefine func "/\" as c₂ "/\" c₃ -> Filter of a₁;
coherence

proof end;

end;

definition

let c₁ be Lattice;
canceled;
mode Ideal of c₁ -> non empty ClosedSubset of a₁ means :Def3: :: FILTER_2:def 3
for b₁, b₂ being Element of a₁ holds
( ( b₁ in a₂ & b₂ in a₂ ) iff b₁ "\/" b₂ in a₂ );
existence

proof end;

end;

:: deftheorem Def2 FILTER_2:def 2 :

:: deftheorem Def3 defines Ideal FILTER_2:def 3 :

theorem Th15: :: FILTER_2:15

for b₁ being Lattice
for b₂ being non empty Subset of b₁ st ( for b₃, b₄ being Element of b₁ holds
( ( b₃ in b₂ & b₄ in b₂ ) iff b₃ "\/" b₄ in b₂ ) ) holds
b₂ is Ideal of b₁

proof end;

theorem Th16: :: FILTER_2:16

for b₁, b₂ being Lattice st LattStr(# the carrier of b₁,the L_join of b₁,the L_meet of b₁ #) = LattStr(# the carrier of b₂,the L_join of b₂,the L_meet of b₂ #) holds
for b₃ being set st b₃ is Filter of b₁ holds
b₃ is Filter of b₂

proof end;

theorem Th17: :: FILTER_2:17

proof end;

definition

let c₁ be Lattice;
let c₂ be Element of c₁;
func c₂ .: -> Element of (a₁ .: ) equals :: FILTER_2:def 4
a₂;
coherence ;

end;

:: deftheorem Def4 defines .: FILTER_2:def 4 :

definition

let c₁ be Lattice;
let c₂ be Element of (c₁ .: );
func .: c₂ -> Element of a₁ equals :: FILTER_2:def 5
a₂;
coherence ;

end;

:: deftheorem Def5 defines .: FILTER_2:def 5 :

theorem Th18: :: FILTER_2:18

for b₁ being Lattice
for b₂ being Element of b₁
for b₃ being Element of (b₁ .: ) holds
( .: (b₂ .: ) = b₂ & (.: b₃) .: = b₃ ) ;

theorem Th19: :: FILTER_2:19

for b₁ being Lattice
for b₂, b₃ being Element of b₁
for b₄, b₅ being Element of (b₁ .: ) holds
( b₂ "/\" b₃ = (b₂ .: ) "\/" (b₃ .: ) & b₂ "\/" b₃ = (b₂ .: ) "/\" (b₃ .: ) & b₄ "/\" b₅ = (.: b₄) "\/" (.: b₅) & b₄ "\/" b₅ = (.: b₄) "/\" (.: b₅) ) ;

theorem Th20: :: FILTER_2:20

for b₁ being Lattice
for b₂, b₃ being Element of b₁
for b₄, b₅ being Element of (b₁ .: ) holds
( ( b₂ [= b₃ implies b₃ .: [= b₂ .: ) & ( b₃ .: [= b₂ .: implies b₂ [= b₃ ) & ( b₄ [= b₅ implies .: b₅ [= .: b₄ ) & ( .: b₅ [= .: b₄ implies b₄ [= b₅ ) ) by LATTICE2:53, LATTICE2:54;

theorem Th21: :: FILTER_2:21

for b₁ being Lattice
for b₂ being set holds
( b₂ is Ideal of b₁ iff b₂ is Filter of b₁ .: )

proof end;

definition

let c₁ be Lattice;
let c₂ be Subset of c₁;
func c₂ .: -> Subset of (a₁ .: ) equals :: FILTER_2:def 6
a₂;
coherence ;

end;

:: deftheorem Def6 defines .: FILTER_2:def 6 :

definition

let c₁ be Lattice;
let c₂ be Subset of (c₁ .: );
func .: c₂ -> Subset of a₁ equals :: FILTER_2:def 7
a₂;
coherence ;

end;

:: deftheorem Def7 defines .: FILTER_2:def 7 :

registration

let c₁ be Lattice;
let c₂ be non empty Subset of c₁;
cluster a₂ .: -> non empty ;
coherence ;

end;

registration

let c₁ be Lattice;
let c₂ be non empty Subset of (c₁ .: );
cluster .: a₂ -> non empty ;
coherence ;

end;

definition

let c₁ be Lattice;
let c₂ be ClosedSubset of c₁;
redefine func .: as c₂ .: -> ClosedSubset of a₁ .: ;
coherence

proof end;

end;

definition

let c₁ be Lattice;
let c₂ be non empty ClosedSubset of c₁;
redefine func .: as c₂ .: -> non empty ClosedSubset of a₁ .: ;
coherence

proof end;

end;

definition

let c₁ be Lattice;
let c₂ be ClosedSubset of c₁ .: ;
redefine func .: as .: c₂ -> ClosedSubset of a₁;
coherence

proof end;

end;

definition

let c₁ be Lattice;
let c₂ be non empty ClosedSubset of c₁ .: ;
redefine func .: as .: c₂ -> non empty ClosedSubset of a₁;
coherence

proof end;

end;

definition

let c₁ be Lattice;
let c₂ be Filter of c₁;
redefine func .: as c₂ .: -> Ideal of a₁ .: ;
coherence

proof end;

end;

definition

let c₁ be Lattice;
let c₂ be Filter of c₁ .: ;
redefine func .: as .: c₂ -> Ideal of a₁;
coherence

proof end;

end;

definition

let c₁ be Lattice;
let c₂ be Ideal of c₁;
redefine func .: as c₂ .: -> Filter of a₁ .: ;
coherence

proof end;

end;

definition

let c₁ be Lattice;
let c₂ be Ideal of c₁ .: ;
redefine func .: as .: c₂ -> Filter of a₁;
coherence

proof end;

end;

theorem Th22: :: FILTER_2:22

for b₁ being Lattice
for b₂ being non empty Subset of b₁ holds
( b₂ is Ideal of b₁ iff ( ( for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ "\/" b₄ in b₂ ) & ( for b₃, b₄ being Element of b₁ st b₃ in b₂ & b₄ [= b₃ holds
b₄ in b₂ ) ) )

proof end;

theorem Th23: :: FILTER_2:23

for b₁ being Lattice
for b₂, b₃ being Element of b₁
for b₄ being Ideal of b₁ st b₂ in b₄ holds
( b₂ "/\" b₃ in b₄ & b₃ "/\" b₂ in b₄ )

proof end;

theorem Th24: :: FILTER_2:24

for b₁ being Lattice
for b₂ being Ideal of b₁ ex b₃ being Element of b₁ st b₃ in b₂

proof end;

theorem Th25: :: FILTER_2:25

for b₁ being Lattice
for b₂ being Ideal of b₁ st b₁ is lower-bounded holds
Bottom b₁ in b₂

proof end;

theorem Th26: :: FILTER_2:26

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

proof end;

theorem Th27: :: FILTER_2:27

for b₁ being Lattice
for b₂ being Element of b₁ st {b₂} is Ideal of b₁ holds
b₁ is lower-bounded

proof end;

theorem Th28: :: FILTER_2:28

for b₁ being Lattice holds the carrier of b₁ is Ideal of b₁

proof end;

definition

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

end;

:: deftheorem Def8 defines (. FILTER_2:def 8 :

definition

let c₁ be Lattice;
let c₂ be Element of c₁;
func (.c₂.> -> Ideal of a₁ equals :: FILTER_2:def 9
{ b₁ where B is Element of a₁ : b₁ [= a₂ } ;
coherence

proof end;

end;

:: deftheorem Def9 defines (. FILTER_2:def 9 :

theorem Th29: :: FILTER_2:29

for b₁ being Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ in (.b₃.> iff b₂ [= b₃ )

proof end;

theorem Th30: :: FILTER_2:30

for b₁ being Lattice
for b₂ being Element of b₁ holds
( (.b₂.> = <.(b₂ .: ).) & (.(b₂ .: ).> = <.b₂.) )

proof end;

theorem Th31: :: FILTER_2:31

for b₁ being Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ in (.b₂.> & b₂ "/\" b₃ in (.b₂.> & b₃ "/\" b₂ in (.b₂.> )

proof end;

theorem Th32: :: FILTER_2:32

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

proof end;

definition

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

end;

:: deftheorem Def10 defines is_max-ideal FILTER_2:def 10 :

theorem Th33: :: FILTER_2:33

for b₁ being Lattice
for b₂ being Ideal of b₁ holds
( b₂ is_max-ideal iff b₂ .: is_ultrafilter )

proof end;

theorem Th34: :: FILTER_2:34

for b₁ being Lattice st b₁ is upper-bounded holds
for b₂ being Ideal of b₁ st b₂ <> the carrier of b₁ holds
ex b₃ being Ideal of b₁ st
( b₂ c= b₃ & b₃ is_max-ideal )

proof end;

theorem Th35: :: FILTER_2:35

for b₁ being Lattice
for b₂ being Element of b₁ st ex b₃ being Element of b₁ st b₂ "\/" b₃ <> b₂ holds
(.b₂.> <> the carrier of b₁

proof end;

theorem Th36: :: FILTER_2:36

for b₁ being Lattice
for b₂ being Element of b₁ st b₁ is upper-bounded & b₂ <> Top b₁ holds
ex b₃ being Ideal of b₁ st
( b₂ in b₃ & b₃ is_max-ideal )

proof end;

definition

let c₁ be Lattice;
let c₂ be non empty Subset of c₁;
func (.c₂.> -> Ideal of a₁ means :Def11: :: FILTER_2:def 11
( a₂ c= a₃ & ( for b₁ being Ideal of a₁ st a₂ c= b₁ holds
a₃ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines (. FILTER_2:def 11 :

Lemma21: for b₁, b₂ being Lattice
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂ st LattStr(# the carrier of b₁,the L_join of b₁,the L_meet of b₁ #) = LattStr(# the carrier of b₂,the L_join of b₂,the L_meet of b₂ #) & b₃ = b₄ holds
( <.b₃.) = <.b₄.) & (.b₃.> = (.b₄.> )

proof end;

theorem Th37: :: FILTER_2:37

for b₁ being Lattice
for b₂ being non empty Subset of b₁
for b₃ being non empty Subset of (b₁ .: ) holds
( <.(b₂ .: ).) = (.b₂.> & <.b₂.) = (.(b₂ .: ).> & <.(.: b₃).) = (.b₃.> & <.b₃.) = (.(.: b₃).> )

proof end;

theorem Th38: :: FILTER_2:38

for b₁ being Lattice
for b₂ being Ideal of b₁ holds (.b₂.> = b₂

proof end;

theorem Th39: :: FILTER_2:39

for b₁ being Lattice
for b₂, b₃, b₄ being non empty Subset of b₁ holds
( ( b₃ c= b₄ implies (.b₃.> c= (.b₄.> ) & (.(.b₂.>.> c= (.b₂.> )

proof end;

theorem Th40: :: FILTER_2:40

for b₁ being Lattice
for b₂ being Element of b₁
for b₃ being non empty Subset of b₁ st b₂ in b₃ holds
(.b₂.> c= (.b₃.>

proof end;

theorem Th41: :: FILTER_2:41

for b₁ being Lattice
for b₂ being Element of b₁
for b₃ being non empty Subset of b₁ st b₃ = {b₂} holds
(.b₃.> = (.b₂.>

proof end;

theorem Th42: :: FILTER_2:42

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

proof end;

theorem Th43: :: FILTER_2:43

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

proof end;

definition

let c₁ be Lattice;
let c₂ be Ideal of c₁;
attr a₂ is prime means :: FILTER_2:def 12
for b₁, b₂ being Element of a₁ holds
( b₁ "/\" b₂ in a₂ iff ( b₁ in a₂ or b₂ in a₂ ) );

end;

:: deftheorem Def12 defines prime FILTER_2:def 12 :

theorem Th44: :: FILTER_2:44

for b₁ being Lattice
for b₂ being Ideal of b₁ holds
( b₂ is prime iff b₂ .: is prime )

proof end;

definition

let c₁ be Lattice;
let c₂, c₃ be non empty Subset of c₁;
func c₂ "\/" c₃ -> Subset of a₁ equals :: FILTER_2:def 13
{ (b₁ "\/" b₂) where B is Element of a₁, B is Element of a₁ : ( b₁ in a₂ & b₂ in a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def13 defines "\/" FILTER_2:def 13 :

registration

let c₁ be Lattice;
let c₂, c₃ be non empty Subset of c₁;
cluster a₂ "\/" a₃ -> non empty ;
coherence

proof end;

end;

Lemma26: for b₁, b₂ being Lattice
for b₃, b₄ being non empty Subset of b₁
for b₅, b₆ being non empty Subset of b₂ st LattStr(# the carrier of b₁,the L_join of b₁,the L_meet of b₁ #) = LattStr(# the carrier of b₂,the L_join of b₂,the L_meet of b₂ #) & b₃ = b₅ & b₄ = b₆ holds
b₃ "/\" b₄ = b₅ "/\" b₆

proof end;

theorem Th45: :: FILTER_2:45

for b₁ being Lattice
for b₂, b₃ being non empty Subset of b₁
for b₄, b₅ being non empty Subset of (b₁ .: ) holds
( b₂ "\/" b₃ = (b₂ .: ) "/\" (b₃ .: ) & (b₂ .: ) "\/" (b₃ .: ) = b₂ "/\" b₃ & b₄ "\/" b₅ = (.: b₄) "/\" (.: b₅) & (.: b₄) "\/" (.: b₅) = b₄ "/\" b₅ )

proof end;

theorem Th46: :: FILTER_2:46

for b₁ being Lattice
for b₂, b₃ being Element of b₁
for b₄, b₅ being non empty Subset of b₁ st b₂ in b₄ & b₃ in b₅ holds
( b₂ "\/" b₃ in b₄ "\/" b₅ & b₃ "\/" b₂ in b₄ "\/" b₅ ) ;

theorem Th47: :: FILTER_2:47

for b₁ being Lattice
for b₂ being set
for b₃, b₄ being non empty Subset of b₁ st b₂ in b₃ "\/" b₄ holds
ex b₅, b₆ being Element of b₁ st
( b₂ = b₅ "\/" b₆ & b₅ in b₃ & b₆ in b₄ ) ;

theorem Th48: :: FILTER_2:48

for b₁ being Lattice
for b₂, b₃ being non empty Subset of b₁ holds b₂ "\/" b₃ = b₃ "\/" b₂

proof end;

definition

let c₁ be D_Lattice;
let c₂, c₃ be Ideal of c₁;
redefine func "\/" as c₂ "\/" c₃ -> Ideal of a₁;
coherence

proof end;

end;

theorem Th49: :: FILTER_2:49

for b₁ being Lattice
for b₂, b₃ being non empty Subset of b₁ holds
( (.(b₂ \/ b₃).> = (.((.b₂.> \/ b₃).> & (.(b₂ \/ b₃).> = (.(b₂ \/ (.b₃.>).> )

proof end;

theorem Th50: :: FILTER_2:50

for b₁ being Lattice
for b₂, b₃ being Ideal of b₁ holds (.(b₂ \/ b₃).> = { b₄ where B is Element of b₁ : ex b₁, b₂ being Element of b₁ st
( b₄ [= b₅ "\/" b₆ & b₅ in b₂ & b₆ in b₃ ) }

proof end;

theorem Th51: :: FILTER_2:51

for b₁ being Lattice
for b₂, b₃ being Ideal of b₁ holds
( b₂ c= b₂ "\/" b₃ & b₃ c= b₂ "\/" b₃ )

proof end;

theorem Th52: :: FILTER_2:52

for b₁ being Lattice
for b₂, b₃ being Ideal of b₁ holds (.(b₂ \/ b₃).> = (.(b₂ "\/" b₃).>

proof end;

theorem Th53: :: FILTER_2:53

for b₁ being Lattice holds
( b₁ is C_Lattice iff b₁ .: is C_Lattice )

proof end;

theorem Th54: :: FILTER_2:54

for b₁ being Lattice holds
( b₁ is B_Lattice iff b₁ .: is B_Lattice )

proof end;

registration

let c₁ be B_Lattice;
cluster a₁ .: -> Lattice-like Boolean ;
coherence by Th54;

end;

Lemma30: for b₁ being B_Lattice
for b₂ being Element of b₁ holds (b₂ .: ) ` = b₂ `

proof end;

theorem Th55: :: FILTER_2:55

for b₁ being B_Lattice
for b₂ being Element of b₁
for b₃ being Element of (b₁ .: ) holds
( (b₂ .: ) ` = b₂ ` & (.: b₃) ` = b₃ ` )

proof end;

theorem Th56: :: FILTER_2:56

for b₁ being B_Lattice
for b₂, b₃ being Ideal of b₁ holds (.(b₂ \/ b₃).> = b₂ "\/" b₃

proof end;

theorem Th57: :: FILTER_2:57

for b₁ being B_Lattice
for b₂ being Ideal of b₁ holds
( b₂ is_max-ideal iff ( b₂ <> the carrier of b₁ & ( for b₃ being Element of b₁ holds
( b₃ in b₂ or b₃ ` in b₂ ) ) ) )

proof end;

theorem Th58: :: FILTER_2:58

for b₁ being B_Lattice
for b₂ being Ideal of b₁ holds
( ( b₂ <> (.b₁.> & b₂ is prime ) iff b₂ is_max-ideal )

proof end;

theorem Th59: :: FILTER_2:59

for b₁ being B_Lattice
for b₂ being Ideal of b₁ st b₂ is_max-ideal holds
for b₃ being Element of b₁ holds
( b₃ in b₂ iff not b₃ ` in b₂ )

proof end;

theorem Th60: :: FILTER_2:60

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄ being Ideal of b₁ st
( b₄ is_max-ideal & ( ( b₂ in b₄ & not b₃ in b₄ ) or ( not b₂ in b₄ & b₃ in b₄ ) ) )

proof end;

theorem Th61: :: FILTER_2:61

for b₁ being Lattice
for b₂ being non empty ClosedSubset of b₁ holds
( the L_join of b₁ || b₂ is BinOp of b₂ & the L_meet of b₁ || b₂ is BinOp of b₂ )

proof end;

theorem Th62: :: FILTER_2:62

for b₁ being Lattice
for b₂ being non empty ClosedSubset of b₁
for b₃, b₄ being BinOp of b₂ st b₃ = the L_join of b₁ || b₂ & b₄ = the L_meet of b₁ || b₂ holds
( b₃ is commutative & b₃ is associative & b₄ is commutative & b₄ is associative & b₃ absorbs b₄ & b₄ absorbs b₃ )

proof end;

definition

let c₁ be Lattice;
let c₂, c₃ be Element of c₁;
assume E34: c₂ [= c₃ ;
func [#c₂,c₃#] -> non empty ClosedSubset of a₁ equals :Def14: :: FILTER_2:def 14
{ b₁ where B is Element of a₁ : ( a₂ [= b₁ & b₁ [= a₃ ) } ;
coherence

proof end;

end;

:: deftheorem Def14 defines [# FILTER_2:def 14 :

theorem Th63: :: FILTER_2:63

for b₁ being Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ holds
( b₄ in [#b₂,b₃#] iff ( b₂ [= b₄ & b₄ [= b₃ ) )

proof end;

theorem Th64: :: FILTER_2:64

for b₁ being Lattice
for b₂, b₃ being Element of b₁ st b₂ [= b₃ holds
( b₂ in [#b₂,b₃#] & b₃ in [#b₂,b₃#] ) by Th63;

theorem Th65: :: FILTER_2:65

for b₁ being Lattice
for b₂ being Element of b₁ holds [#b₂,b₂#] = {b₂}

proof end;

theorem Th66: :: FILTER_2:66

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

proof end;

theorem Th67: :: FILTER_2:67

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

proof end;

theorem Th68: :: FILTER_2:68

for b₁, b₂ being Lattice
for b₃ being Filter of b₁
for b₄ being Filter of b₂ st LattStr(# the carrier of b₁,the L_join of b₁,the L_meet of b₁ #) = LattStr(# the carrier of b₂,the L_join of b₂,the L_meet of b₂ #) & b₃ = b₄ holds
latt b₃ = latt b₄

proof end;

notation

let c₁ be Lattice;
synonym Sublattice of c₁ for SubLattice of c₁;

end;

definition

let c₁ be Lattice;
redefine mode SubLattice of c₁ -> LattStr means :Def15: :: FILTER_2:def 15
ex b₁ being non empty ClosedSubset of a₁ex b₂, b₃ being BinOp of b₁ st
( b₂ = the L_join of a₁ || b₁ & b₃ = the L_meet of a₁ || b₁ & LattStr(# the carrier of a₂,the L_join of a₂,the L_meet of a₂ #) = LattStr(# b₁,b₂,b₃ #) );
compatibility

proof end;

end;

:: deftheorem Def15 defines Sublattice FILTER_2:def 15 :

theorem Th69: :: FILTER_2:69

for b₁ being Lattice
for b₂ being Sublattice of b₁
for b₃ being Element of b₂ holds b₃ is Element of b₁

proof end;

definition

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

proof end;

uniqueness ;

end;

:: deftheorem Def16 defines latt FILTER_2:def 16 :

registration

let c₁ be Lattice;
let c₂ be non empty ClosedSubset of c₁;
cluster latt a₁,a₂ -> strict ;
coherence

proof end;

end;

definition

let c₁ be Lattice;
let c₂ be Sublattice of c₁;
redefine func .: as c₂ .: -> strict Sublattice of a₁ .: ;
coherence

proof end;

end;

theorem Th70: :: FILTER_2:70

for b₁ being Lattice
for b₂ being Filter of b₁ holds latt b₂ = latt b₁,b₂

proof end;

theorem Th71: :: FILTER_2:71

for b₁ being Lattice
for b₂ being non empty ClosedSubset of b₁ holds latt b₁,b₂ = (latt (b₁ .: ),(b₂ .: )) .:

proof end;

theorem Th72: :: FILTER_2:72

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

proof end;

theorem Th73: :: FILTER_2:73

for b₁ being Lattice
for b₂ being non empty ClosedSubset of b₁ holds
( the carrier of (latt b₁,b₂) = b₂ & the L_join of (latt b₁,b₂) = the L_join of b₁ || b₂ & the L_meet of (latt b₁,b₂) = the L_meet of b₁ || b₂ )

proof end;

theorem Th74: :: FILTER_2:74

for b₁ being Lattice
for b₂ being non empty ClosedSubset of b₁
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of (latt b₁,b₂) st b₃ = b₅ & b₄ = b₆ holds
( b₃ "\/" b₄ = b₅ "\/" b₆ & b₃ "/\" b₄ = b₅ "/\" b₆ )

proof end;

theorem Th75: :: FILTER_2:75

for b₁ being Lattice
for b₂ being non empty ClosedSubset of b₁
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of (latt b₁,b₂) st b₃ = b₅ & b₄ = b₆ holds
( b₃ [= b₄ iff b₅ [= b₆ )

proof end;

theorem Th76: :: FILTER_2:76

for b₁ being Lattice
for b₂ being Ideal of b₁ st b₁ is lower-bounded holds
latt b₁,b₂ is lower-bounded

proof end;

theorem Th77: :: FILTER_2:77

for b₁ being Lattice
for b₂ being non empty ClosedSubset of b₁ st b₁ is modular holds
latt b₁,b₂ is modular

proof end;

theorem Th78: :: FILTER_2:78

for b₁ being Lattice
for b₂ being non empty ClosedSubset of b₁ st b₁ is distributive holds
latt b₁,b₂ is distributive

proof end;

theorem Th79: :: FILTER_2:79

for b₁ being Lattice
for b₂, b₃ being Element of b₁ st b₁ is implicative & b₂ [= b₃ holds
latt b₁,[#b₂,b₃#] is implicative

proof end;

theorem Th80: :: FILTER_2:80

for b₁ being Lattice
for b₂ being Element of b₁ holds latt b₁,(.b₂.> is upper-bounded

proof end;

theorem Th81: :: FILTER_2:81

for b₁ being Lattice
for b₂ being Element of b₁ holds Top (latt b₁,(.b₂.>) = b₂

proof end;

theorem Th82: :: FILTER_2:82

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

proof end;

theorem Th83: :: FILTER_2:83

for b₁ being Lattice
for b₂ being Element of b₁ st b₁ is lower-bounded holds
latt b₁,(.b₂.> is bounded

proof end;

theorem Th84: :: FILTER_2:84

for b₁ being Lattice
for b₂, b₃ being Element of b₁ st b₂ [= b₃ holds
( latt b₁,[#b₂,b₃#] is bounded & Top (latt b₁,[#b₂,b₃#]) = b₃ & Bottom (latt b₁,[#b₂,b₃#]) = b₂ )

proof end;

theorem Th85: :: FILTER_2:85

for b₁ being Lattice
for b₂ being Element of b₁ st b₁ is C_Lattice & b₁ is modular holds
latt b₁,(.b₂.> is C_Lattice

proof end;

theorem Th86: :: FILTER_2:86

for b₁ being Lattice
for b₂, b₃ being Element of b₁ st b₁ is C_Lattice & b₁ is modular & b₂ [= b₃ holds
latt b₁,[#b₂,b₃#] is C_Lattice

proof end;

theorem Th87: :: FILTER_2:87

for b₁ being Lattice
for b₂, b₃ being Element of b₁ st b₁ is B_Lattice & b₂ [= b₃ holds
latt b₁,[#b₂,b₃#] is B_Lattice

proof end;