# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674436855 -32400
# Node ID 4b2f49a5a1d5843500662c658daaf24dcddec70a
# Parent  f4bccbe80540a222f1e486ba21daa624ce9424d1
...

diff -r f4bccbe80540 -r 4b2f49a5a1d5 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Sun Jan 22 22:41:13 2023 +0900
+++ b/src/Tychonoff.agda	Mon Jan 23 10:20:55 2023 +0900
@@ -192,19 +192,42 @@
          pq⊆F : {p q : HOD} → Neighbor TP (& p) (UFLP.limit uflp) → Neighbor TP (& q) (UFLP.limit uflq) → ? ⊆ filter F 
          pq⊆F = ?
          isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → * v ⊆ filter F 
-         isL {v} npq {x} fx = filter2 F ? ? ? where
-             neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F 
-             neip = ?
-             neiq : {q : Ordinal } → ( bq : BaseQ P TQ q ) → * q ⊆ filter F 
-             neiq = ?
+         isL {v} npq {x} fx = ? where 
              bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u npq) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
              bpq = Neighbor.ou npq (Neighbor.ux npq)
              pqb : Subbase (pbase TP TQ) (Base.b bpq )
              pqb = Base.sb bpq 
-             base⊆F : {b : Ordinal } →  Subbase (pbase TP TQ) b → * b ⊆ filter F
-             base⊆F (gi (case1 px)) bx = ?
-             base⊆F (gi (case2 qx)) bx = ?
-             base⊆F (g∩ b1 b2) bx = filter1 F ? ? ?
+             pqb⊆opq : * (Base.b bpq) ⊆ * ( Neighbor.u npq )
+             pqb⊆opq = Base.b⊆u bpq
+             base⊆F : {b : Ordinal } →  Subbase (pbase TP TQ) b → * b ⊆  * (Neighbor.u npq) → * b ⊆ filter F
+             base⊆F (gi (case1 px)) b⊆u {z} bz = fz  where
+                 -- F contains no od∅, because it projection contains no od∅
+                 --    x is an element of BaseP, which is a subset of Neighbor npq
+                 --    x is also an elment of Proj1 F because Proj1 F has UFLP (uflp)
+                 --    BaseP ∩ F is not empty
+                 --    (Base P ∩ F) ⊆ F , (Base P ) ⊆ F , 
+                 il1 : odef (Power P) z ∧ ZProj1 (filter F) z
+                 il1 = UFLP.is-limit uflp ? bz 
+                 nei1 : HOD
+                 nei1 = Proj1 (* (Neighbor.u npq)) (Power P) (Power Q)
+                 plimit : Ordinal
+                 plimit = UFLP.limit uflp ? 
+                 nproper : {b : Ordinal } →  * b ⊆ nei1 → o∅ o< b
+                 nproper = ?
+                 b∋z : odef nei1 z
+                 b∋z = ?
+                 bp : BaseP {P} TP Q z
+                 bp = record { b = ? ; op = ? ; prod = ? }
+                 neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F 
+                 neip = ?
+                 il2 : * z ⊆ ZFP (Power P) (Power Q)
+                 il2 = ?
+                 il3 : filter F ∋ ? 
+                 il3 = ?
+                 fz : odef (filter F) z
+                 fz = subst (λ k → odef (filter F) k) &iso (filter1 F ? ? ?)
+             base⊆F (gi (case2 qx)) b⊆u {z} bz = ?
+             base⊆F (g∩ b1 b2) b⊆u {z} bz = ?