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

comparison filter.agda @ 296:42f89e5efb00

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
if Filter contains L, prime filter is ultra
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 15 Jun 2020 18:15:48 +0900
parents 822b50091a26
children e70980bd80c7
comparison
equal deleted inserted replaced
295:822b50091a26 296:42f89e5efb00
102 ----- 102 -----
103 -- 103 --
104 -- if Filter contains L, prime filter is ultra 104 -- if Filter contains L, prime filter is ultra
105 -- 105 --
106 106
107 filter-lemma2 : {L : OD} → (P : Filter L) → prime-filter P → ultra-filter P 107 filter-lemma2 : {L : OD} → (P : Filter L) → filter P ∋ L → prime-filter P → ultra-filter P
108 filter-lemma2 {L} P prime = {!!} 108 filter-lemma2 {L} P f∋L prime = record {
109 proper = prime-filter.proper prime
110 ; ultra = λ {p} p⊆L → prime-filter.prime prime (lemma p p⊆L)
111 } where
112 open _==_
113 p+1-p=1 : {p : OD} → p ⊆ L → L == (p ∪ (L ＼ p))
114 eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (def p x)
115 eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
116 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p })
117 eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → def L k ) diso (incl p⊆L ( subst (λ k → def p k) (sym diso) p∋x ))
118 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p
119 lemma : (p : OD) → p ⊆ L → filter P ∋ (p ∪ (L ＼ p))
120 lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
109 121
110 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) 122 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
111 generated-filter {L} P p = {!!} 123 generated-filter {L} P p = {!!}
112 124
113 record Dense (P : OD ) : Set (suc n) where 125 record Dense (P : OD ) : Set (suc n) where