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

comparison src/Tychonoff.agda @ 1172:f4bccbe80540

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, 22 Jan 2023 22:41:13 +0900
parents a839fccdef47
children 4b2f49a5a1d5
comparison
equal deleted inserted replaced
1171:a839fccdef47 1172:f4bccbe80540
187 uflq : UFLP TQ FQ UFQ 187 uflq : UFLP TQ FQ UFQ
188 uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ 188 uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ
189 189
190 Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) 190 Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
191 Pf = ? 191 Pf = ?
192 neip : {v : Ordinal} → {p q : HOD} → Neighbor (ProductTopology TP TQ) (& < p , q >) v → Neighbor TP (& p) ?
193 neip = ?
194 neiq : {v : Ordinal} → {p q : HOD} → Neighbor (ProductTopology TP TQ) (& < p , q >) v → Neighbor TQ (& q) ?
195 neiq = ?
196 pq⊆F : {p q : HOD} → Neighbor TP (& p) (UFLP.limit uflp) → Neighbor TP (& q) (UFLP.limit uflq) → ? ⊆ filter F 192 pq⊆F : {p q : HOD} → Neighbor TP (& p) (UFLP.limit uflp) → Neighbor TP (& q) (UFLP.limit uflq) → ? ⊆ filter F
197 pq⊆F = ? 193 pq⊆F = ?
198 isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → * v ⊆ filter F 194 isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → * v ⊆ filter F
199 isL {v} npq {x} fx = ? 195 isL {v} npq {x} fx = filter2 F ? ? ? where
200 196 neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F
201 197 neip = ?
202 198 neiq : {q : Ordinal } → ( bq : BaseQ P TQ q ) → * q ⊆ filter F
203 199 neiq = ?
204 200 bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u npq) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
205 201 bpq = Neighbor.ou npq (Neighbor.ux npq)
202 pqb : Subbase (pbase TP TQ) (Base.b bpq )
203 pqb = Base.sb bpq
204 base⊆F : {b : Ordinal } → Subbase (pbase TP TQ) b → * b ⊆ filter F
205 base⊆F (gi (case1 px)) bx = ?
206 base⊆F (gi (case2 qx)) bx = ?
207 base⊆F (g∩ b1 b2) bx = filter1 F ? ? ?
208
209
210
211
212
213