Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison filter.agda @ 271:2169d948159b
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 |