Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison filter.agda @ 292:773e03dfd6ed

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 13 Jun 2020 15:59:10 +0900
parents ef93c56ad311
children 9972bd4a0d6f
comparison
equal deleted inserted replaced
291:ef93c56ad311 292:773e03dfd6ed
31 31
32 _＼_ : ( A B : OD ) → OD 32 _＼_ : ( A B : OD ) → OD
33 A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) } 33 A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) }
34 34
35 35
36 -- Kunen p.76 and p.53
36 record Filter ( L : OD ) : Set (suc n) where 37 record Filter ( L : OD ) : Set (suc n) where
37 field 38 field
38 filter : OD 39 filter : OD
39 ¬f∋∅ : ¬ ( filter ∋ od∅ )
40 f∋L : filter ∋ L
41 f⊆PL : filter ⊆ Power L 40 f⊆PL : filter ⊆ Power L
42 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q 41 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
43 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) 42 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
44 43
44 open Filter
45
46 proper-filter : {L : OD} → (P : Filter L ) → {p : OD} → Set n
47 proper-filter {L} P {p} = filter P ∋ L
48
49 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n
50 prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
51
45 record Ideal ( L : OD ) : Set (suc n) where 52 record Ideal ( L : OD ) : Set (suc n) where
46 field 53 field
47 ideal : OD 54 ideal : OD
48 i∋∅ : ideal ∋ od∅
49 ¬i∋L : ¬ ( ideal ∋ L )
50 i⊆PL : ideal ⊆ Power L 55 i⊆PL : ideal ⊆ Power L
51 ideal1 : { p q : OD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q 56 ideal1 : { p q : OD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q
52 ideal2 : { p q : OD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) 57 ideal2 : { p q : OD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q)
53 58
54 open Filter
55 open Ideal 59 open Ideal
56 60
57 L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L 61 proper-ideal : {L : OD} → (P : Ideal L ) → {p : OD} → Set n
58 L-filter {L} P {p} lt = {!!} -- filter1 P {p} {L} {!!} lt {!!} 62 proper-ideal {L} P {p} = ideal P ∋ od∅
59 63
60 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n 64 prime-ideal : {L : OD} → Ideal L → ∀ {p q : OD } → Set n
61 prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) 65 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
66
62 67
63 ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set n 68 ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set n
64 ultra-filter {L} P {p} = L ∋ p → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) ) 69 ultra-filter {L} P {p} = L ∋ p → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) )
65 70
66 71