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

comparison filter.agda @ 422:44a484f17f26

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
syntax *, &, ⟪ , ⟫
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 01 Aug 2020 11:06:29 +0900
parents 19687f3304c9
children 9984cdd88da3
comparison
equal deleted inserted replaced
421:cb067605fea0 422:44a484f17f26
75 lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) 75 lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
76 lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) ) 76 lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
77 ... | case1 p∈P = case1 p∈P 77 ... | case1 p∈P = case1 p∈P
78 ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where 78 ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
79 lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h= (q ∩ (L ＼ p)) 79 lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h= (q ∩ (L ＼ p))
80 lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt } 80 lemma5 = record { eq→ = λ {x} lt → ⟪ lemma4 x lt , proj2 lt ⟫
81 ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt } 81 ; eq← = λ {x} lt → ⟪ case2 (proj1 lt) , proj2 lt ⟫
82 } where 82 } where
83 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x 83 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x
84 lemma4 x lt with proj1 lt 84 lemma4 x lt with proj1 lt
85 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px ) 85 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
86 lemma4 x lt | case2 qx = qx 86 lemma4 x lt | case2 qx = qx
103 } where 103 } where
104 open _==_ 104 open _==_
105 p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) 105 p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p))
106 eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x) 106 eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x)
107 eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x 107 eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
108 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p }) 108 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫
109 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 )) 109 eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) &iso (incl p⊆L ( subst (λ k → odef p k) (sym &iso) p∋x ))
110 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p 110 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p
111 lemma : (p : HOD) → p ⊆ L → filter P ∋ (p ∪ (L ＼ p)) 111 lemma : (p : HOD) → p ⊆ L → filter P ∋ (p ∪ (L ＼ p))
112 lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L 112 lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
113 113
114 record Dense (P : HOD ) : Set (suc n) where 114 record Dense (P : HOD ) : Set (suc n) where