:: Filters - Part I. Implicative Lattices
:: by Grzegorz Bancerek
::
:: Received July 3, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: FILTER_0:1
theorem :: FILTER_0:2
theorem :: FILTER_0:3
theorem Th4: :: FILTER_0:4
theorem Th5: :: FILTER_0:5
theorem Th6: :: FILTER_0:6
theorem Th7: :: FILTER_0:7
:: deftheorem Def1 defines Filter FILTER_0:def 1 :
theorem :: FILTER_0:8
canceled;
theorem Th9: :: FILTER_0:9
theorem Th10: :: FILTER_0:10
theorem Th11: :: FILTER_0:11
theorem Th12: :: FILTER_0:12
theorem :: FILTER_0:13
theorem :: FILTER_0:14
theorem Th15: :: FILTER_0:15
:: deftheorem defines <. FILTER_0:def 2 :
:: deftheorem defines <. FILTER_0:def 3 :
theorem :: FILTER_0:16
canceled;
theorem :: FILTER_0:17
canceled;
theorem Th18: :: FILTER_0:18
theorem Th19: :: FILTER_0:19
theorem Th20: :: FILTER_0:20
:: deftheorem Def4 defines being_ultrafilter FILTER_0:def 4 :
theorem :: FILTER_0:21
canceled;
theorem Th22: :: FILTER_0:22
theorem Th23: :: FILTER_0:23
theorem Th24: :: FILTER_0:24
:: deftheorem Def5 defines <. FILTER_0:def 5 :
theorem :: FILTER_0:25
canceled;
theorem Th26: :: FILTER_0:26
theorem Th27: :: FILTER_0:27
theorem :: FILTER_0:28
canceled;
theorem Th29: :: FILTER_0:29
theorem Th30: :: FILTER_0:30
theorem Th31: :: FILTER_0:31
theorem Th32: :: FILTER_0:32
:: deftheorem defines prime FILTER_0:def 6 :
theorem :: FILTER_0:33
canceled;
theorem Th34: :: FILTER_0:34
:: deftheorem Def7 defines implicative FILTER_0:def 7 :
:: deftheorem Def8 defines => FILTER_0:def 8 :
theorem :: FILTER_0:35
canceled;
theorem :: FILTER_0:36
canceled;
theorem Th37: :: FILTER_0:37
theorem Th38: :: FILTER_0:38
theorem Th39: :: FILTER_0:39
theorem Th40: :: FILTER_0:40
theorem Th41: :: FILTER_0:41
theorem Th42: :: FILTER_0:42
:: deftheorem defines "/\" FILTER_0:def 9 :
theorem :: FILTER_0:43
canceled;
theorem :: FILTER_0:44
theorem :: FILTER_0:45
theorem Th46: :: FILTER_0:46
theorem Th47: :: FILTER_0:47
theorem :: FILTER_0:48
theorem Th49: :: FILTER_0:49
theorem Th50: :: FILTER_0:50
theorem Th51: :: FILTER_0:51
theorem :: FILTER_0:52
theorem Th53: :: FILTER_0:53
theorem Th54: :: FILTER_0:54
theorem Th55: :: FILTER_0:55
theorem Th56: :: FILTER_0:56
theorem Th57: :: FILTER_0:57
theorem :: FILTER_0:58
theorem Th59: :: FILTER_0:59
theorem :: FILTER_0:60
definition
let L be
Lattice;
let F be
Filter of
L;
func latt F -> Lattice means :
Def10:
:: FILTER_0:def 10
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 #) )
end;
:: deftheorem Def10 defines latt FILTER_0:def 10 :
theorem :: FILTER_0:61
canceled;
theorem :: FILTER_0:62
theorem Th63: :: FILTER_0:63
theorem Th64: :: FILTER_0:64
theorem Th65: :: FILTER_0:65
theorem Th66: :: FILTER_0:66
theorem :: FILTER_0:67
theorem Th68: :: FILTER_0:68
theorem :: FILTER_0:69
theorem Th70: :: FILTER_0:70
theorem Th71: :: FILTER_0:71
theorem Th72: :: FILTER_0:72
theorem Th73: :: FILTER_0:73
theorem Th74: :: FILTER_0:74
theorem :: FILTER_0:75
:: deftheorem defines <=> FILTER_0:def 11 :
theorem :: FILTER_0:76
canceled;
theorem :: FILTER_0:77
theorem Th78: :: FILTER_0:78
:: deftheorem Def12 defines equivalence_wrt FILTER_0:def 12 :
theorem :: FILTER_0:79
canceled;
theorem Th80: :: FILTER_0:80
theorem Th81: :: FILTER_0:81
theorem Th82: :: FILTER_0:82
theorem Th83: :: FILTER_0:83
theorem Th84: :: FILTER_0:84
theorem :: FILTER_0:85
:: deftheorem Def13 defines are_equivalence_wrt FILTER_0:def 13 :
theorem :: FILTER_0:86
canceled;
theorem :: FILTER_0:87
theorem :: FILTER_0:88
theorem :: FILTER_0:89
theorem :: FILTER_0:90
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 ) )
theorem :: FILTER_0:91
theorem :: FILTER_0:92