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

comparison src/filter.agda @ 478:c6346d92f1a1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 03 Apr 2022 07:59:55 +0900
parents 0e018784bed3
children fea0c2454b85
comparison
equal deleted inserted replaced
477:24b4b854b310 478:c6346d92f1a1
171 record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (suc n) where 171 record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (suc n) where
172 field 172 field
173 genf : Filter LP 173 genf : Filter LP
174 generic : (D : Dense LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ ) 174 generic : (D : Dense LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )
175 175
176 open import zorn
177
178 record MaximumFilter {L P : HOD} (LP : L ⊆ Power P) : Set (suc n) where
179 field
180 mf : Filter LP
181 proper : ¬ (filter mf ∋ od∅)
182 is-maximum : ( f : Filter LP ) → filter f ⊆ filter mf
183
184 max→ultra : {L P : HOD} (LP : L ⊆ Power P) → (mx : MaximumFilter LP ) → ultra-filter ( MaximumFilter.mf mx )
185 max→ultra {L} {P} LP mx = record { proper = {!!} ; ultra = {!!} }
186
187