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

comparison filter.agda @ 301:b012a915bbb5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
contradiction found ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 24 Jun 2020 14:05:38 +0900
parents e70980bd80c7
children 5544f4921a44
comparison
equal deleted inserted replaced
300:e70980bd80c7 301:b012a915bbb5
127 dense-d : { p : OD} → P ∋ p → dense ∋ 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) 128 dense-p : { p : OD} → P ∋ p → p ⊆ (dense-f p)
129 129
130 -- the set of finite partial functions from ω to 2 130 -- the set of finite partial functions from ω to 2
131 -- 131 --
132 -- ph2 : Nat → Set → 2
133 -- ph2 : Nat → Maybe 2
134 --
132 -- Hω2 : Filter (Power (Power infinite)) 135 -- Hω2 : Filter (Power (Power infinite))
133
134 136
135 record Ideal ( L : OD ) : Set (suc n) where 137 record Ideal ( L : OD ) : Set (suc n) where
136 field 138 field
137 ideal : OD 139 ideal : OD
138 i⊆PL : ideal ⊆ Power L 140 i⊆PL : ideal ⊆ Power L