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

comparison filter.agda @ 300:e70980bd80c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
-- the set of finite partial functions from ω to 2
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Jun 2020 15:12:43 +0900
parents 42f89e5efb00
children b012a915bbb5
comparison
equal deleted inserted replaced
296:42f89e5efb00 300:e70980bd80c7
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 )) 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 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)) 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 120 lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
121 121
122 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
123 generated-filter {L} P p = {!!}
124
125 record Dense (P : OD ) : Set (suc n) where 122 record Dense (P : OD ) : Set (suc n) where
126 field 123 field
127 dense : OD 124 dense : OD
128 incl : dense ⊆ P 125 incl : dense ⊆ P
129 dense-f : OD → OD 126 dense-f : OD → OD
130 dense-p : { p : OD} → P ∋ p → p ⊆ (dense-f p) 127 dense-d : { p : OD} → P ∋ p → dense ∋ dense-f p
128 dense-p : { p : OD} → P ∋ p → p ⊆ (dense-f p)
131 129
132 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω)) 130 -- the set of finite partial functions from ω to 2
133 131 --
134 infinite = ZF.infinite OD→ZF 132 -- Hω2 : Filter (Power (Power infinite))
135
136 module in-countable-ordinal {n : Level} where
137
138 import ordinal
139
140 -- open ordinal.C-Ordinal-with-choice
141
142 Hω2 : Filter (Power (Power infinite))
143 Hω2 = {!!}
144 133
145 134
146 record Ideal ( L : OD ) : Set (suc n) where 135 record Ideal ( L : OD ) : Set (suc n) where
147 field 136 field
148 ideal : OD 137 ideal : OD