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

changeset 1136:181ffd308ab5

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 Fri, 13 Jan 2023 08:22:20 +0900
parents 464efeeb988e
children d618788852e5
files src/Topology.agda src/filter.agda
diffstat 2 files changed, 14 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Fri Jan 13 08:00:28 2023 +0900
+++ b/src/Topology.agda	Fri Jan 13 08:22:20 2023 +0900
@@ -303,8 +303,8 @@
    →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P)  → UFLP TP LP F FP 
 FIP→UFLP {P} TP fip {L} LP F FP = record { limit = FIP.limit fip fip00 CFP fip01  ; P∋limit = FIP.L∋limit fip fip00 CFP fip01 ; is-limit = fip02 }
     where
-      MX : MaximumFilter ? 
-      MX = F→Maximum {L} {P} LP ? ? F ? ? ? 
+      MX : MaximumFilter LP F
+      MX = F→Maximum {L} {P} LP ? ? F ? FP ? 
       MF : Filter LP
       MF = MaximumFilter.mf MX
       uf : ultra-filter {L} {P} {LP} MF
--- a/src/filter.agda	Fri Jan 13 08:00:28 2023 +0900
+++ b/src/filter.agda	Fri Jan 13 08:22:20 2023 +0900
@@ -172,7 +172,7 @@
 record MaximumFilter {L P : HOD} (LP : L ⊆ Power P) (F : Filter {L} {P} LP) : Set (suc n) where
     field
        mf : Filter {L} {P} LP
-       F⊆mf : filter F ⊂ filter mf
+       F⊆mf : filter F ⊆ filter mf
        proper  : ¬ (filter mf ∋ od∅)
        is-maximum : ( f : Filter {L} {P} LP ) →  ¬ (filter f ∋ od∅)  →  ¬ ( filter mf  ⊂ filter f  )
 
@@ -184,9 +184,9 @@
 
 max→ultra : {L P : HOD} (LP : L ⊆ Power P) 
        → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
-       → (F0 : Filter {L} {P} LP) 
+       → (F0 : Filter {L} {P} LP) → {y : Ordinal } → odef (filter F0) y 
        → (mx : MaximumFilter {L} {P} LP F0 ) → ultra-filter ( MaximumFilter.mf mx )
-max→ultra {L} {P} LP CAP F0 mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where
+max→ultra {L} {P} LP CAP F0 {y} mfy 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 ODC.∋-p O (filter mf) p 
@@ -224,11 +224,13 @@
              mu03 : (* x ＼ * (& p)) ⊆ * x
              mu03 {z} ⟪ xz , _ ⟫ = xz
          F∋P-p : F ∋ (P ＼ p )
-         F∋P-p = ⟪ Lnp , record { y = ? ; mfy = ? ; y-p⊂x = mu30 }  ⟫  where
-             mu30 : (* ? ＼ * (& p)) ⊆ * (& (P ＼ p))
+         F∋P-p = ⟪ Lnp , record { y = y ; mfy = mxy ; y-p⊂x = mu30 }  ⟫  where
+             mxy : odef (filter (MaximumFilter.mf mx)) y
+             mxy = MaximumFilter.F⊆mf mx mfy
+             mu30 : (* y ＼ * (& p)) ⊆ * (& (P ＼ p))
              mu30 {z} ⟪ yz , ¬pz ⟫ = subst (λ k → odef k z) (sym *iso) ( ⟪ Pz , (λ pz → ¬pz (subst (λ k → odef k z) (sym *iso) pz ))  ⟫  ) where
                  Pz : odef P z
-                 Pz = LP (f⊆L mf ? ) _ yz
+                 Pz = LP (f⊆L mf mxy ) _ yz
          FisProper : ¬ (filter FisFilter ∋ od∅)    -- if F contains p, p is in mf which contract np
          FisProper ⟪ L0 , record { y = z ; mfy = mfz ; y-p⊂x = z-p⊂x } ⟫ = 
            ⊥-elim ( np (filter1 mf Lp (subst (λ k → odef (filter mf) k) (sym &iso) mfz) mu31) ) where
@@ -248,7 +250,7 @@
        → L ∋ p → L ∋ ( P ＼ p)) 
        → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
        → (U : Filter {L} {P} LP) → ultra-filter U → MaximumFilter LP U
-ultra→max {L} {P} LP NG CAP U u  = record { mf = U ; F⊆mf = ? ; proper = ultra-filter.proper u ; is-maximum = is-maximum } where 
+ultra→max {L} {P} LP NG CAP U u  = record { mf = U ; F⊆mf = λ x → x ; proper = ultra-filter.proper u ; is-maximum = is-maximum } where 
   is-maximum : (F : Filter {L} {P} LP) → (¬ (filter F ∋ od∅)) → (U⊂F : filter U  ⊂ filter F ) → ⊥
   is-maximum F Prop ⟪ U<F , U⊆F ⟫   = Prop f0 where
      GT : HOD
@@ -315,7 +317,7 @@
       fx00 {x} lt = subst (λ k → k o< osuc (& L)) &iso ( ⊆→o≤ (is-filter.f⊆L (proj1 lt ))  )
 
 F→Maximum : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
-      → (F : Filter {L} {P} LP) → o∅ o< & L →  o∅ o< & (filter F)  →  (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP F
+      → (F : Filter {L} {P} LP) → o∅ o< & L →  {y : Ordinal } → odef (filter F) y →  (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP F
 F→Maximum {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = mf ; F⊆mf = ? 
          ; proper = subst (λ k → ¬ ( odef (filter mf ) k)) (sym ord-od∅) ( is-filter.proper imf)  ; is-maximum = {!!} }  where
       FX : HOD
@@ -344,8 +346,8 @@
           
 
 F→ultra : {L P : HOD} (LP : L ⊆ Power P) → (NEG : {p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
-      → (F : Filter {L} {P} LP) → (0<L : o∅ o< & L) →  (0<F : o∅ o< & (filter F))  →  (proper : ¬ (filter F ∋ od∅)) 
+      → (F : Filter {L} {P} LP) → (0<L : o∅ o< & L) →  {y : Ordinal} →  (0<F : odef (filter F) y) →  (proper : ¬ (filter F ∋ od∅)) 
       → ultra-filter ( MaximumFilter.mf (F→Maximum {L} {P} LP NEG CAP F 0<L 0<F proper ))
-F→ultra {L} {P} LP NEG CAP F 0<L 0<F proper = max→ultra {L} {P} LP CAP F (F→Maximum {L} {P} LP NEG CAP F 0<L 0<F proper ) 
+F→ultra {L} {P} LP NEG CAP F 0<L 0<F proper = max→ultra {L} {P} LP CAP F 0<F (F→Maximum {L} {P} LP NEG CAP F 0<L 0<F proper )