Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff filter.agda @ 331:12071f79f3cf
HOD done
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 05 Jul 2020 16:56:21 +0900 |
parents | 5544f4921a44 |
children | aad9249d1e8f |
line wrap: on
line diff
--- a/filter.agda Sun Jul 05 15:49:00 2020 +0900 +++ b/filter.agda Sun Jul 05 16:56:21 2020 +0900 @@ -54,7 +54,7 @@ trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) } power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A -power→⊆ A t PA∋t = record { incl = λ {x} t∋x → HODC.double-neg-eilm O (t1 t∋x) } where +power→⊆ A t PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) t1 = zf.IsZF.power→ isZF A t PA∋t @@ -70,6 +70,10 @@ q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q q∩q⊆q = record { incl = λ lt → proj1 lt } +open HOD +_=h=_ : (x y : HOD) → Set n +x =h= y = od x == od y + ----- -- -- ultra filter is prime @@ -84,11 +88,11 @@ lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) ) ... | case1 p∈P = case1 p∈P ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L \ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where - lemma5 : ((p ∪ q ) ∩ (L \ p)) == (q ∩ (L \ p)) + lemma5 : ((p ∪ q ) ∩ (L \ p)) =h= (q ∩ (L \ p)) lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt } ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt } } where - lemma4 : (x : Ordinal ) → def ((p ∪ q) ∩ (L \ p)) x → def q x + lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L \ p)) x → odef q x lemma4 x lt with proj1 lt lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px ) lemma4 x lt | case2 qx = qx @@ -110,11 +114,11 @@ ; ultra = λ {p} p⊆L → prime-filter.prime prime (lemma p p⊆L) } where open _==_ - p+1-p=1 : {p : HOD} → p ⊆ L → L == (p ∪ (L \ p)) - eq→ (p+1-p=1 {p} p⊆L) {x} lt with HODC.decp O (def p x) + p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L \ p)) + eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef 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} ( case1 p∋x ) = subst (λ k → odef L k ) diso (incl p⊆L ( subst (λ k → odef p k) (sym diso) p∋x )) eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p lemma : (p : HOD) → 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