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

comparison src/Tychonoff.agda @ 1208:151f4c971a50

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, 03 Mar 2023 19:44:29 +0900
parents 56d501cf0318
children 09e4b32ece2e
comparison
equal deleted inserted replaced
1207:56d501cf0318 1208:151f4c971a50
204 ... | ⟪ xz , ⟪ Pz , ¬xz ⟫ ⟫ = Pz 204 ... | ⟪ xz , ⟪ Pz , ¬xz ⟫ ⟫ = Pz
205 uf11 : filter (MaximumFilter.mf (maxf CSX fp)) ∋ od∅ 205 uf11 : filter (MaximumFilter.mf (maxf CSX fp)) ∋ od∅
206 uf11 = subst (λ k → odef (filter (MaximumFilter.mf (maxf CSX fp))) k ) uf13 206 uf11 = subst (λ k → odef (filter (MaximumFilter.mf (maxf CSX fp))) k ) uf13
207 ( filter2 (MaximumFilter.mf (maxf CSX fp)) uf05 uf06 uf12 ) 207 ( filter2 (MaximumFilter.mf (maxf CSX fp)) uf05 uf06 uf12 )
208 208
209 x⊆Clx : {P : HOD} (TP : Topology P) → {x : HOD} → x ⊆ P → x ⊆ Cl TP x
210 x⊆Clx {P} TP {x} x<p {y} xy = ⟪ x<p xy , (λ c csc x<c → x<c xy ) ⟫
211 P⊆Clx : {P : HOD} (TP : Topology P) → {x : HOD} → x ⊆ P → Cl TP x ⊆ P
212 P⊆Clx {P} TP {x} x<p {y} xy = proj1 xy
213
209 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP 214 FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP
210 → (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF 215 → (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF
211 FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? ; P∋limit = ? ; is-limit = ufl00 } where 216 FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ; P∋limit = ? ; is-limit = ufl00 } where
212 -- 217 --
213 -- take closure of given filter elements 218 -- take closure of given filter elements
214 -- 219 --
215 CF : HOD 220 CF : HOD
216 CF = Replace (filter F) (λ x → Cl TP x ) 221 CF = Replace (filter F) (λ x → Cl TP x )
217 CF⊆CS : CF ⊆ CS TP 222 CF⊆CS : CF ⊆ CS TP
218 CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z)) 223 CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z))
219 -- 224 --
220 -- it is set of closed set and has FIP ( F is proper ) 225 -- it is set of closed set and has FIP ( F is proper )
221 -- 226 --
227 ufl08 : {z : Ordinal} → odef (Power P) (& (Cl TP (* z)))
228 ufl08 {z} w zw with subst (λ k → odef k w ) *iso zw
229 ... | t = proj1 t
230 fx→px : {x : Ordinal} → odef (filter F) x → Power P ∋ * x
231 fx→px {x} fx z xz = f⊆L F fx _ (subst (λ k → odef k z) *iso xz )
232 F∋sb : {x : Ordinal} → Subbase CF x → odef (filter F) x
233 F∋sb {x} (gi record { z = z ; az = az ; x=ψz = x=ψz }) = ufl07 where
234 ufl09 : * z ⊆ P
235 ufl09 {y} zy = f⊆L F az _ zy
236 ufl07 : odef (filter F) x
237 ufl07 = subst (λ k → odef (filter F) k) &iso ( filter1 F (subst (λ k → odef (Power P) k) (trans (sym x=ψz) (sym &iso)) ufl08 )
238 (subst (λ k → odef (filter F) k) (sym &iso) az)
239 (subst (λ k → * z ⊆ k ) (trans (sym *iso) (sym (cong (*) x=ψz)) ) (x⊆Clx TP {* z} ufl09 ) ))
240 F∋sb (g∩ {x} {y} sx sy) = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sx))
241 (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sy))
242 (λ z xz → fx→px (F∋sb sx) _ (subst (λ k → odef k _) (sym *iso) (proj1 (subst (λ k → odef k z) *iso xz) )))
222 ufl01 : {x : Ordinal} → Subbase (* (& CF)) x → o∅ o< x 243 ufl01 : {x : Ordinal} → Subbase (* (& CF)) x → o∅ o< x
223 ufl01 = ? 244 ufl01 {x} sb = ufl04 where
245 ufl04 : o∅ o< x
246 ufl04 with trio< o∅ x
247 ... | tri< a ¬b ¬c = a
248 ... | tri≈ ¬a b ¬c = ⊥-elim ( ultra-filter.proper UF (subst (λ k → odef (filter F) k) (
249 begin
250 x ≡⟨ sym b ⟩
251 o∅ ≡⟨ sym ord-od∅ ⟩
252 & od∅ ∎ ) (F∋sb (subst (λ k → Subbase k x) *iso sb )) )) where open ≡-Reasoning
253 ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
224 -- 254 --
225 -- so we have a limit 255 -- so we have a limit
226 -- 256 --
227 limit : Ordinal 257 limit : Ordinal
228 limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? -- ufl01 258 limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01
229 ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit 259 ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit
230 ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? -- ufl01 260 ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01
231 -- 261 --
232 -- Neigbor of limit ⊆ Filter 262 -- Neigbor of limit ⊆ Filter
233 -- 263 --
234 ufl03 : {f v : Ordinal } → odef (filter F) f → Neighbor TP limit v → ¬ ( * f ∩ * v ) =h= od∅ -- because limit is in CF which is a closure 264 ufl03 : {f v : Ordinal } → odef (filter F) f → Neighbor TP limit v → ¬ ( * f ∩ * v ) =h= od∅ -- because limit is in CF
235 ufl03 {f} {v} ff nei fv=0 = ? 265 ufl03 {f} {v} ff nei fv=0 = ?
236 pp : {v x : Ordinal} → Neighbor TP limit v → odef (* v) x → Power P ∋ (* x) 266 pp : {v x : Ordinal} → Neighbor TP limit v → odef (* v) x → Power P ∋ (* x)
237 pp {v} {x} nei vx z pz = ? 267 pp {v} {x} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; u⊆v = u⊆v } vx z pz = v⊆P ?
238 ufl00 : {v : Ordinal} → Neighbor TP limit v → * v ⊆ filter F 268 ufl00 : {v : Ordinal} → Neighbor TP limit v → * v ⊆ filter F
239 ufl00 {v} nei {x} fx with ultra-filter.ultra UF (pp nei fx) (NEG P (pp nei fx)) 269 ufl00 {v} nei {x} fx with ultra-filter.ultra UF (pp nei fx) (NEG P (pp nei fx))
240 ... | case1 fv = subst (λ k → odef (filter F) k) &iso fv 270 ... | case1 fv = subst (λ k → odef (filter F) k) &iso fv
241 ... | case2 nfv = ? -- will contradicts ufl03 271 ... | case2 nfv = ? -- will contradicts ufl03
242 272