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

changeset 479:fea0c2454b85

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 11:34:01 +0900
parents c6346d92f1a1
children 6c22ee73ff06
files src/filter.agda
diffstat 1 files changed, 21 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/filter.agda	Sun Apr 03 07:59:55 2022 +0900
+++ b/src/filter.agda	Sun Apr 03 11:34:01 2022 +0900
@@ -179,9 +179,28 @@
     field
        mf : Filter LP
        proper  : ¬ (filter mf ∋ od∅)
-       is-maximum : ( f : Filter LP ) →  filter f  ⊆ filter mf
+       is-maximum : ( f : Filter LP ) →  ¬ ( filter mf  ⊆ filter f )
 
 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 = {!!} }
+max→ultra {L} {P} LP mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where
+    mf = MaximumFilter.mf mx
+    ultra : {p : HOD} → L ∋ p → L ∋ (P ＼ p) → (filter mf ∋ p) ∨ (filter mf ∋ (P ＼ p))
+    ultra {p} lp lnp with ∋-p (filter mf) p
+    ... | yes y = case1 y
+    ... | no np with ∋-p (filter mf) (P ＼ p) 
+    ... | yes y = case2 y
+    ... | no n-p = ⊥-elim (MaximumFilter.is-maximum mx FisFilter {!!} ) where
+         Y : (y : Ordinal) → (my : odef (filter mf) y ) → HOD
+         Y y my = record { od = record { def = λ x → (x ≡ y) ∨ (x ≡ & p) } ; odmax = & L ; <odmax = {!!} }
+         F : HOD
+         F = record { od = record { def = λ x → (x ≡ & p) ∨ ((y : Ordinal) → (my : odef (filter mf) y ) → x ≡ & (Y y my) )  } ; odmax = & L ; <odmax = {!!} }
+         FisFilter : Filter LP
+         FisFilter = record { filter = F ; f⊆L = {!!} ; filter1 = {!!} ; filter2 = {!!} }
 
+ultra→max : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → (F U : Filter LP)  → ultra-filter U → ¬ filter U ⊆ filter F 
+ultra→max {L} {P} LP NG F U u U⊆F = {!!} where
+     max : {x : HOD} → filter F ∋ x → filter U ∋ x
+     max {x} fx with ultra-filter.ultra u {x} (incl (f⊆L F) fx) (NG (incl (f⊆L F) fx))
+     ... | case1 ux = ux
+     ... | case2 u-x = {!!}