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

comparison filter.agda @ 271:2169d948159b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix incl
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Dec 2019 23:45:59 +0900
parents fc3d4bc1dc5e
children 985a1af11bce
comparison
equal deleted inserted replaced
270:fc3d4bc1dc5e 271:2169d948159b
108 108
109 record Filter ( L : OD ) : Set (suc n) where 109 record Filter ( L : OD ) : Set (suc n) where
110 field 110 field
111 filter : OD 111 filter : OD
112 proper : ¬ ( filter ∋ od∅ ) 112 proper : ¬ ( filter ∋ od∅ )
113 inL : { x : OD} → _⊆_ filter L {x} 113 inL : filter ⊆ L
114 filter1 : { p q : OD } → ( {x : OD} → _⊆_ q L {x} ) → filter ∋ p → ({ x : OD} → _⊆_ p q {x} ) → filter ∋ q 114 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
115 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) 115 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q)
116 116
117 open Filter 117 open Filter
118 118
119 L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L 119 L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L
133 filter-lemma2 {L} P prime p with prime {!!} 133 filter-lemma2 {L} P prime p with prime {!!}
134 ... | t = {!!} 134 ... | t = {!!}
135 135
136 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) 136 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
137 generated-filter {L} P p = record { 137 generated-filter {L} P p = record {
138 proper = {!!} ;
138 filter = {!!} ; inL = {!!} ; 139 filter = {!!} ; inL = {!!} ;
139 filter1 = {!!} ; filter2 = {!!} 140 filter1 = {!!} ; filter2 = {!!}
140 } 141 }
141 142
142 record Dense (P : OD ) : Set (suc n) where 143 record Dense (P : OD ) : Set (suc n) where
143 field 144 field
144 dense : OD 145 dense : OD
145 incl : { x : OD} → _⊆_ dense P {x} 146 incl : dense ⊆ P
146 dense-f : OD → OD 147 dense-f : OD → OD
147 dense-p : { p x : OD} → P ∋ p → _⊆_ p (dense-f p) {x} 148 dense-p : { p : OD} → P ∋ p → p ⊆ (dense-f p)
148 149
149 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω)) 150 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
150 151
151 infinite = ZF.infinite OD→ZF 152 infinite = ZF.infinite OD→ZF
152 153