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

changeset 1134:4c85ce2794e9

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 07:37:27 +0900
parents c2c0cf7f2d7e
children 464efeeb988e
files src/Topology.agda src/filter.agda
diffstat 2 files changed, 41 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Thu Jan 12 20:52:47 2023 +0900
+++ b/src/Topology.agda	Fri Jan 13 07:37:27 2023 +0900
@@ -286,6 +286,10 @@
 
 -- Ultra Filter has limit point
 
+--- 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∅))
+--      → ultra-filter ( MaximumFilter.mf (F→Maximum {L} {P} LP NEG CAP F 0<L 0<F proper )
+
 record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP )  
       (FL : filter F ∋ P) : Set (suc (suc n)) where
    field
@@ -299,8 +303,12 @@
    →  {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
-      uf : ultra-filter {L} {P} {LP} F
-      uf = {!!}
+      MX : MaximumFilter ? 
+      MX = F→Maximum {L} {P} LP ? ? F ? ? ? 
+      MF : Filter LP
+      MF = MaximumFilter.mf MX
+      uf : ultra-filter {L} {P} {LP} MF
+      uf = F→ultra {L} {P} LP ? ? F ? ? ?
       fip03 : {z : HOD} → filter F ∋ z → z ⊆ P
       fip03 {z} fz {x} zx = LP ( f⊆L F fz ) x (subst (λ k → odef k x) (sym *iso) zx  )
       CF : Ordinal
@@ -315,14 +323,14 @@
       fip01 {C} {x} CCF (gi Cx) = {!!} -- filter is proper .i.e it contains no od∅
       fip01 {C} {.(& (* _ ∩ * _))} CCF (g∩ sb sb₁) = {!!}
       fip02 : {o : Ordinal} → odef (OS TP) o → odef (* o) (FIP.limit fip fip00 CFP fip01) → * o ⊆ filter F
-      fip02 {p} oo ol {x} ox = fip06 where
+      fip02 {p} oo ol {x} ox = ? where
          fip04 : odef {!!} (FIP.limit fip fip00 CFP fip01) 
          fip04 = FIP.is-limit fip fip00 CFP fip01 {!!}
-         fip05 : ( filter F ∋ (* x) ) ∨ (  filter F ∋ ( P ＼ (* x))  )
+         fip05 : ( filter MF ∋ (* x) ) ∨ (  filter MF ∋ ( P ＼ (* x))  )
          fip05  = ultra-filter.ultra uf {!!} {!!} 
-         fip06 : odef (filter F) x
+         fip06 : odef (filter MF) x
          fip06 with fip05
-         ... | case1 lt = subst (λ k → odef (filter F) k ) &iso lt
+         ... | case1 lt = subst (λ k → odef (filter MF) k ) &iso lt
          ... | case2 nlt = {!!}
 
 
--- a/src/filter.agda	Thu Jan 12 20:52:47 2023 +0900
+++ b/src/filter.agda	Fri Jan 13 07:37:27 2023 +0900
@@ -312,16 +312,39 @@
       fx00 : {x : Ordinal } → is-filter LP x ∧ filter F ⊆ * x → x o< osuc (& L)
       fx00 {x} lt = subst (λ k → k o< osuc (& L)) &iso ( ⊆→o≤ (is-filter.f⊆L (proj1 lt ))  )
 
-MaximumFilterExist : {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→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 
-MaximumFilterExist {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = {!!} ; proper = {!!} ; is-maximum = {!!} }  where
+F→Maximum {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = mf
+         ; proper = subst (λ k → ¬ ( odef (filter mf ) k)) (sym ord-od∅) ( is-filter.proper imf)  ; is-maximum = {!!} }  where
       FX : HOD
       FX = F⊆X {L} {P} LP F
       FX∋F : odef FX (& (filter F))
       FX∋F = ⟪ record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) (f⊆L F) ; filter1 = ? ; filter2 = ? ; proper = ? }  , subst (λ k → filter F ⊆ k ) (sym *iso) ( λ x → x ) ⟫ 
       SUP⊆ : (B : HOD) → B ⊆ FX → IsTotalOrderSet B → SUP FX B
       SUP⊆ B B⊆FX OB = record { sup = Union B ; isSUP = record { ax = ? ; x≤sup = ?  } }
-      mf01 : Maximal  FX
-      mf01 = Zorn-lemma (∈∅< FX∋F) SUP⊆  
+      mx : Maximal  FX
+      mx = Zorn-lemma (∈∅< FX∋F) SUP⊆  
+      imf : is-filter {L} {P} LP (& (Maximal.maximal mx))
+      imf = proj1 (Maximal.as mx)
+      mf00 : (* (& (Maximal.maximal mx))) ⊆ L
+      mf00 = is-filter.f⊆L imf   
+      mf01 : { p q : HOD } →  L ∋ q → (* (& (Maximal.maximal mx))) ∋ p →  p ⊆ q  → (* (& (Maximal.maximal mx))) ∋ q
+      mf01 {p} {q} Lq Fq p⊆q = is-filter.filter1 imf Lq Fq 
+              (λ {x} lt → subst (λ k → odef k x) (sym *iso) ( p⊆q (subst (λ k → odef k x) *iso lt ) ))
+      mf02 : { p q : HOD } → (* (& (Maximal.maximal mx))) ∋ p → (* (& (Maximal.maximal mx)))  ∋ q  → L ∋ (p ∩ q) 
+          → (* (& (Maximal.maximal mx))) ∋ (p ∩ q)
+      mf02 {p} {q} Fp Fq Lpq = subst₂ (λ j k → odef (* (& (Maximal.maximal mx))) (& (j ∩ k ))) *iso *iso (
+          is-filter.filter2 imf Fp Fq (subst₂ (λ j k → odef L (& (j ∩ k ))) (sym *iso) (sym *iso) Lpq ))
+      mf : Filter {L} {P} LP
+      mf = record { filter = * (& (Maximal.maximal mx)) ; f⊆L = mf00  
+         ; filter1 = mf01  
+         ; filter2 = mf02 }
+          
+
+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∅)) 
+      → 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→Maximum {L} {P} LP NEG CAP F 0<L 0<F proper ) 
+     {& (filter F)} ? -- (MaximumFilter.proper (F→Maximum {L} {P} LP NEG CAP F 0<L 0<F proper ))