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

comparison src/Tychonoff.agda @ 1173:4b2f49a5a1d5

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 Mon, 23 Jan 2023 10:20:55 +0900
parents f4bccbe80540
children 375615f9d60f
comparison
equal deleted inserted replaced
1172:f4bccbe80540 1173:4b2f49a5a1d5
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 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
193 pq⊆F = ? 193 pq⊆F = ?
194 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
195 isL {v} npq {x} fx = filter2 F ? ? ? where 195 isL {v} npq {x} fx = ? where
196 neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F
197 neip = ?
198 neiq : {q : Ordinal } → ( bq : BaseQ P TQ q ) → * q ⊆ filter F
199 neiq = ?
200 bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u npq) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) 196 bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u npq) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
201 bpq = Neighbor.ou npq (Neighbor.ux npq) 197 bpq = Neighbor.ou npq (Neighbor.ux npq)
202 pqb : Subbase (pbase TP TQ) (Base.b bpq ) 198 pqb : Subbase (pbase TP TQ) (Base.b bpq )
203 pqb = Base.sb bpq 199 pqb = Base.sb bpq
204 base⊆F : {b : Ordinal } → Subbase (pbase TP TQ) b → * b ⊆ filter F 200 pqb⊆opq : * (Base.b bpq) ⊆ * ( Neighbor.u npq )
205 base⊆F (gi (case1 px)) bx = ? 201 pqb⊆opq = Base.b⊆u bpq
206 base⊆F (gi (case2 qx)) bx = ? 202 base⊆F : {b : Ordinal } → Subbase (pbase TP TQ) b → * b ⊆ * (Neighbor.u npq) → * b ⊆ filter F
207 base⊆F (g∩ b1 b2) bx = filter1 F ? ? ? 203 base⊆F (gi (case1 px)) b⊆u {z} bz = fz where
208 204 -- F contains no od∅, because it projection contains no od∅
209 205 -- x is an element of BaseP, which is a subset of Neighbor npq
210 206 -- x is also an elment of Proj1 F because Proj1 F has UFLP (uflp)
211 207 -- BaseP ∩ F is not empty
212 208 -- (Base P ∩ F) ⊆ F , (Base P ) ⊆ F ,
213 209 il1 : odef (Power P) z ∧ ZProj1 (filter F) z
210 il1 = UFLP.is-limit uflp ? bz
211 nei1 : HOD
212 nei1 = Proj1 (* (Neighbor.u npq)) (Power P) (Power Q)
213 plimit : Ordinal
214 plimit = UFLP.limit uflp ?
215 nproper : {b : Ordinal } → * b ⊆ nei1 → o∅ o< b
216 nproper = ?
217 b∋z : odef nei1 z
218 b∋z = ?
219 bp : BaseP {P} TP Q z
220 bp = record { b = ? ; op = ? ; prod = ? }
221 neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F
222 neip = ?
223 il2 : * z ⊆ ZFP (Power P) (Power Q)
224 il2 = ?
225 il3 : filter F ∋ ?
226 il3 = ?
227 fz : odef (filter F) z
228 fz = subst (λ k → odef (filter F) k) &iso (filter1 F ? ? ?)
229 base⊆F (gi (case2 qx)) b⊆u {z} bz = ?
230 base⊆F (g∩ b1 b2) b⊆u {z} bz = ?
231
232
233
234
235
236