# HG changeset patch # User Shinji KONO # Date 1592212548 -32400 # Node ID 42f89e5efb00569c5edce3ea795853e91386dc32 # Parent 822b50091a2665078fe320ae7299a5fd50c976a9 if Filter contains L, prime filter is ultra diff -r 822b50091a26 -r 42f89e5efb00 filter.agda --- a/filter.agda Mon Jun 15 09:53:18 2020 +0900 +++ b/filter.agda Mon Jun 15 18:15:48 2020 +0900 @@ -104,8 +104,20 @@ -- if Filter contains L, prime filter is ultra -- -filter-lemma2 : {L : OD} → (P : Filter L) → prime-filter P → ultra-filter P -filter-lemma2 {L} P prime = {!!} +filter-lemma2 : {L : OD} → (P : Filter L) → filter P ∋ L → prime-filter P → ultra-filter P +filter-lemma2 {L} P f∋L prime = record { + proper = prime-filter.proper prime + ; ultra = λ {p} p⊆L → prime-filter.prime prime (lemma p p⊆L) + } where + open _==_ + p+1-p=1 : {p : OD} → p ⊆ L → L == (p ∪ (L ＼ p)) + eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (def p x) + eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x + eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p }) + 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 )) + eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p + lemma : (p : OD) → p ⊆ L → filter P ∋ (p ∪ (L ＼ p)) + lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) generated-filter {L} P p = {!!}