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

diff 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
line wrap: on
line diff
--- a/src/filter.agda	Sat Apr 02 08:37:17 2022 +0900
+++ b/src/filter.agda	Sun Apr 03 07:59:55 2022 +0900
@@ -173,3 +173,15 @@
        genf : Filter LP
        generic : (D : Dense LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )
 
+open import zorn
+
+record MaximumFilter {L P : HOD} (LP : L ⊆ Power P) : Set (suc n) where
+    field
+       mf : Filter LP
+       proper  : ¬ (filter mf ∋ od∅)
+       is-maximum : ( f : Filter LP ) →  filter f  ⊆ filter mf
+
+max→ultra : {L P : HOD} (LP : L ⊆ Power P) → (mx : MaximumFilter LP ) → ultra-filter ( MaximumFilter.mf mx )
+max→ultra {L} {P} LP mx = record { proper = {!!} ; ultra = {!!} }
+
+