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

changeset 1166:4e0a1f41910f

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 Sat, 21 Jan 2023 13:16:27 +0900
parents 70bcb775115a
children fee9249a2f50
files src/Topology.agda
diffstat 1 files changed, 21 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Sat Jan 21 12:11:36 2023 +0900
+++ b/src/Topology.agda	Sat Jan 21 13:16:27 2023 +0900
@@ -538,9 +538,9 @@
      uf00 {X} CSX fp = UFLP.limit ( uflp (λ x → x)
          ( MaximumFilter.mf (maxf CSX fp) )
          (F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc CSX fp) (proper CSX fp)))
-     uf01 :  {X : Ordinal} (CX : * X ⊆ CS TP) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
-            {x : Ordinal} → odef (* X) x → odef (* x) (uf00 CX fip)
-     uf01 = ?
+     uf01 :  {X : Ordinal} (CSX : * X ⊆ CS TP) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
+            {x : Ordinal} → odef (* X) x → odef (* x) (uf00 CSX fip)
+     uf01 {X} CSX fp {x} xx = ?
 
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
    →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F UF
@@ -567,7 +567,7 @@
      -- Product of UFL has limit point
      uflPQ : {L : HOD} → (LPQ : L ⊆ Power (ZFP P Q )) (F : Filter {L} LPQ)  (UF : ultra-filter F)
              → UFLP (ProductTopology TP TQ) LPQ F UF
-     uflPQ {L} LPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , {!!} >  ; P∋limit = {!!} ; is-limit = {!!} } where
+     uflPQ {L} LPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) >  ; P∋limit = Pf ; is-limit = isL } where
          LP : HOD  -- proj1 of LPQ
          LP = Proj1 L (Power P) (Power Q)
          LPP : LP ⊆ Power P
@@ -582,5 +582,22 @@
          uflp : UFLP TP LPP FP UFP
          uflp = FIP→UFLP TP (Compact→FIP TP CP) LPP FP UFP
 
+         LQ : HOD  -- proj1 of LPQ
+         LQ = Proj2 L (Power P) (Power Q)
+         LQP : LQ ⊆ Power Q
+         LQP {x} ⟪ Qx , q1 ⟫ = Qx
+         FQ : Filter {LQ} {Q} LQP
+         FQ = record { filter = Proj2 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
+             ty00 :  Proj2 (filter F) (Power P) (Power Q) ⊆ LQ
+             ty00 {x} ⟪ QPx , ppf ⟫ = ⟪ QPx , ( λ y → record { pq = ZProj2.pq (ppf y)
+                 ; opq = ZProj2.opq (ppf y) ; Lpq = f⊆L F (ZProj2.Lpq (ppf y)) ; x=pi2 = ZProj2.x=pi2 (ppf y) } )  ⟫
+         UFQ : ultra-filter FQ
+         UFQ = record { proper = ? ; ultra = ? }
+         uflq : UFLP TQ LQP FQ UFQ
+         uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) LQP FQ UFQ
 
+         Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
+         Pf = ?
+         isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → filter F ⊆ * v
+         isL {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; o⊆u = o⊆u } {x} fx = ?